From 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 21 Jun 2023 16:05:44 +0100 Subject: Add sums, vectors and arithmetic encodings. Also define pretty printing of terms. --- src/Term.idr | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) (limited to 'src/Term.idr') diff --git a/src/Term.idr b/src/Term.idr index bceecfe..e6b7466 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -340,3 +340,46 @@ substBase : -- (sub1 : Subst ctx ctx') -> -- (sub2 : Subst ctx' ctx'') -> -- subst (subst t sub1) sub2 <~> subst t ?d + +-- Utilities ------------------------------------------------------------------- + +export +countUses : Term ty ctx -> Elem ty' ctx -> Nat +fullCountUses : FullTerm ty ctx -> Elem ty' ctx -> Nat + +countUses (t `Over` thin) i = + case preimage thin i of + Just i => fullCountUses t i + Nothing => 0 + +fullCountUses Var Here = 1 +fullCountUses (Const t) i = fullCountUses t i +fullCountUses (Abs t) i = fullCountUses t (There i) +fullCountUses (App (MakePair t u _)) i = countUses t i + countUses u i +fullCountUses (Suc t) i = fullCountUses t i +fullCountUses + (Rec (MakePair + t + (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin) + _)) + i = + countUses t i + + case preimage thin i of + Just i => + (case preimage thin2 i of Just i => fullCountUses u i; Nothing => 0) + + (case preimage thin3 i of Just i => fullCountUses v i; Nothing => 0) + Nothing => 0 + +export +size : Term ty ctx -> Nat +fullSize : FullTerm ty ctx -> Nat + +size (t `Over` thin) = fullSize t + +fullSize Var = 1 +fullSize (Const t) = S (fullSize t) +fullSize (Abs t) = S (fullSize t) +fullSize (App (MakePair t u _)) = S (size t + size u) +fullSize Zero = 1 +fullSize (Suc t) = S (fullSize t) +fullSize (Rec (MakePair t (MakePair u v _ `Over` _) _)) = S (size t + size u + size v) -- cgit v1.2.3