summaryrefslogtreecommitdiff
path: root/src/Inky/Term/Desugar.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Term/Desugar.idr')
-rw-r--r--src/Inky/Term/Desugar.idr479
1 files changed, 218 insertions, 261 deletions
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 4bf8f05..2ad87c9 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -1,269 +1,226 @@
module Inky.Term.Desugar
-import Data.List.Quantifiers
-import Data.Maybe
-import Flap.Data.List
-import Flap.Decidable
+import Control.Monad.State
+import Data.SortedMap
import Inky.Term
-import Inky.Term.Substitution
--- Desugar map -----------------------------------------------------------------
-
-desugarMap :
- (meta : m) =>
- (a : Ty tyCtx) -> (i : Var tyCtx) -> (0 prf : i `StrictlyPositiveIn` a) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (t : Term mode m tyCtx' tmCtx) ->
- Term mode m tyCtx' tmCtx
-desugarMapTuple :
- (meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (t : Term mode m tyCtx' tmCtx) ->
- Row (Term mode m tyCtx' tmCtx)
-desugarMapTupleNames :
- (0 meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (0 i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (0 f : Term mode m tyCtx' tmCtx) ->
- (0 t : Term mode m tyCtx' tmCtx) ->
- (desugarMapTuple as fresh i prfs f t).names = as.names
-desugarMapCase :
+-- Other Sugar -----------------------------------------------------------------
+
+suc : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+suc meta t = Roll meta $ Inj meta "S" t
+
+lit : m -> Nat -> Term NoSugar m tyCtx tmCtx
+lit meta 0 = Roll meta $ Inj meta "Z" $ Tup meta [<]
+lit meta (S k) = suc meta (lit meta k)
+
+cons : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+cons meta t u = Roll meta $ Inj meta "C" $ Tup meta [<"H" :- t, "T" :- u]
+
+list : m -> List (Term NoSugar m tyCtx tmCtx) -> Term NoSugar m tyCtx tmCtx
+list meta [] = Roll meta $ Inj meta "N" $ Tup meta [<]
+list meta (t :: ts) = cons meta t (list meta ts)
+
+record Cache (a : Type) where
+ constructor MkCache
+ max : Nat
+ vals : SortedMap a Nat
+
+miss : Ord a => a -> Cache a -> (Cache a, Nat)
+miss x cache =
+ let newVals = insert x cache.max cache.vals in
+ let newMax = S cache.max in
+ (MkCache newMax newVals, cache.max)
+
+lookup : Ord a => MonadState (Cache a) m => a -> m Nat
+lookup x = do
+ cache <- get
+ case lookup x cache.vals of
+ Nothing => state (miss x)
+ Just n => pure n
+
+string : MonadState (Cache String) f => m -> String -> f (Term NoSugar m tyCtx tmCtx)
+string meta str = do
+ n <- lookup str
+ pure $ lit meta n
+
+-- Desugar ---------------------------------------------------------------------
+
+desugar' :
+ MonadState (Cache String) f =>
+ Term (Sugar qtCtx) m tyCtx tmCtx -> f (Term NoSugar m tyCtx tmCtx)
+desugarAll :
+ MonadState (Cache String) f =>
+ List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+desugarCtx :
+ MonadState (Cache String) f =>
+ (ctx : Context (Term (Sugar qtCtx) m tyCtx tmCtx)) ->
+ f (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ctx.names)
+desugarBranches :
+ MonadState (Cache String) f =>
+ (ctx : Context (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x))) ->
+ f (All (Assoc0 (x ** Term NoSugar m tyCtx (tmCtx :< x))) ctx.names)
+
+quote :
+ MonadState (Cache String) f =>
+ Term (Quote tyCtx tmCtx) m [<] qtCtx ->
+ f (Term NoSugar m tyCtx tmCtx)
+quoteAll :
+ MonadState (Cache String) f =>
+ List (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+quoteCtx :
+ MonadState (Cache String) f =>
(meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- Row (x ** Term mode m tyCtx' (tmCtx :< x))
-desugarMapCaseNames :
+ Context (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+quoteBranches :
+ MonadState (Cache String) f =>
(meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (desugarMapCase as fresh i prfs f).names = as.names
-
-desugarMap (TVar j) i TVar f t with (i `decEq` j)
- _ | True `Because` _ = App meta f [t]
- _ | False `Because` _ = t
-desugarMap (TArrow a b) i (TArrow prf) f t = t
-desugarMap (TProd (MkRow as fresh)) i (TProd prfs) f t =
- Tup meta (desugarMapTuple as fresh i prfs f t)
-desugarMap (TSum (MkRow as fresh)) i (TSum prfs) f t =
- Case meta t (desugarMapCase as fresh i prfs f)
-desugarMap (TFix x a) i (TFix prf) f t =
- Fold meta t ("_eta" ** Roll meta
- (desugarMap a (ThereVar i) prf (thin (Drop Id) f) (Var meta (%% "_eta"))))
-
-desugarMapTuple [<] [<] i [<] f t = [<]
-desugarMapTuple (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
- (:<)
- (desugarMapTuple as fresh i prfs f t)
- (l :- desugarMap a i prf f (Prj meta t l))
- @{rewrite desugarMapTupleNames as fresh i prfs f t in freshIn}
-
-desugarMapTupleNames [<] [<] i [<] f t = Refl
-desugarMapTupleNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
- cong (:< l) $ desugarMapTupleNames as fresh i prfs f t
-
-desugarMapCase [<] [<] i [<] f = [<]
-desugarMapCase (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
- (:<)
- (desugarMapCase as fresh i prfs f)
- (l :- ("_eta" ** Inj meta l (desugarMap a i prf (thin (Drop Id) f) (Var meta (%% "_eta")))))
- @{rewrite desugarMapCaseNames as fresh i prfs f in freshIn}
-
-desugarMapCaseNames [<] [<] i [<] f = Refl
-desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
- cong (:< l) $ desugarMapCaseNames as fresh i prfs f
-
--- Desugar Terms ---------------------------------------------------------------
-
-desugarSynths :
- (len : LengthOf tyCtx) =>
- {t : Term Sugar m tyCtx tmCtx} ->
- (0 _ : Synths tyEnv tmEnv t a) ->
- Term NoSugar m tyCtx tmCtx
-desugarChecks :
- LengthOf tyCtx =>
- {t : Term Sugar m tyCtx tmCtx} ->
- (0 _ : Checks tyEnv tmEnv a t) ->
- Term NoSugar m tyCtx tmCtx
-desugarCheckSpine :
- LengthOf tyCtx =>
- {ts : List (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
- List (Term NoSugar m tyCtx tmCtx)
-desugarAllSynths :
- LengthOf tyCtx =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : AllSynths tyEnv tmEnv ts as) ->
- Context (Term NoSugar m tyCtx tmCtx)
-desugarAllChecks :
- LengthOf tyCtx =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : AllChecks tyEnv tmEnv as ts) ->
- Context (Term NoSugar m tyCtx tmCtx)
-desugarAllBranches :
- LengthOf tyCtx =>
- {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
- (0 _ : AllBranches tyEnv tmEnv as a ts) ->
- Context (x ** Term NoSugar m tyCtx (tmCtx :< x))
-desugarAllSynthsNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 prfs : AllSynths tyEnv tmEnv ts as) ->
- (desugarAllSynths prfs).names = ts.names
-desugarAllChecksNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 prfs : AllChecks tyEnv tmEnv as ts) ->
- (desugarAllChecks prfs).names = ts.names
-desugarAllBranchesNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
- (0 prfs : AllBranches tyEnv tmEnv as a ts) ->
- (desugarAllBranches prfs).names = ts.names
-
-desugarSynths (AnnotS {meta, a} wf prf) = Annot meta (desugarChecks prf) a
-desugarSynths (VarS {meta, i}) = Var meta i
-desugarSynths (LetS {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarSynths prf2)
-desugarSynths (LetTyS {meta, a, x} wf prf) = LetTy meta a (x ** desugarSynths prf)
-desugarSynths (AppS {meta} prf prfs) = App meta (desugarSynths prf) (desugarCheckSpine prfs)
-desugarSynths (TupS {meta, es} prfs) =
- Tup meta (MkRow (desugarAllSynths prfs) (rewrite desugarAllSynthsNames prfs in es.fresh))
-desugarSynths (PrjS {meta, l} prf i) = Prj meta (desugarSynths prf) l
-desugarSynths (UnrollS {meta} prf) = Unroll meta (desugarSynths prf)
-desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
- Annot meta
- (Abs meta
- (["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
- (TArrow (TArrow b c) (TArrow
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
-desugarChecks (VarC prf1 prf2) = desugarSynths prf1
-desugarChecks (LetC {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarChecks prf2)
-desugarChecks (LetTyC {meta, a, x} wf prf) = LetTy meta a (x ** desugarChecks prf)
-desugarChecks (AbsC {meta, bound} prf1 prf2) = Abs meta (bound ** desugarChecks prf2)
-desugarChecks (AppC prf1 prf2) = desugarSynths prf1
-desugarChecks (TupC {meta, ts} prfs) =
- Tup meta (MkRow (desugarAllChecks prfs) (rewrite desugarAllChecksNames prfs in ts.fresh))
-desugarChecks (PrjC prf1 prf2) = desugarSynths prf1
-desugarChecks (InjC {meta, l} i prf) = Inj meta l (desugarChecks prf)
-desugarChecks (CaseC {meta, ts} prf prfs) =
- Case meta (desugarSynths prf)
- (MkRow (desugarAllBranches prfs) (rewrite desugarAllBranchesNames prfs in ts.fresh))
-desugarChecks (RollC {meta} prf) = Roll meta (desugarChecks prf)
-desugarChecks (UnrollC prf1 prf2) = desugarSynths prf1
-desugarChecks (FoldC {meta, y} prf1 prf2) = Fold meta (desugarSynths prf1) (y ** desugarChecks prf2)
-desugarChecks (MapC prf1 prf2) = desugarSynths prf1
-
-desugarCheckSpine [] = []
-desugarCheckSpine (prf :: prfs) = desugarChecks prf :: desugarCheckSpine prfs
-
-desugarAllSynths [<] = [<]
-desugarAllSynths ((:<) {l} prfs prf) = desugarAllSynths prfs :< (l :- desugarSynths prf)
-
-desugarAllChecks Base = [<]
-desugarAllChecks (Step {l} i prf prfs) = desugarAllChecks prfs :< (l :- desugarChecks prf)
-
-desugarAllBranches Base = [<]
-desugarAllBranches (Step {l, x} i prf prfs) = desugarAllBranches prfs :< (l :- (x ** desugarChecks prf))
-
-desugarAllSynthsNames [<] = Refl
-desugarAllSynthsNames ((:<) {l} prfs prf) = cong (:< l) $ desugarAllSynthsNames prfs
-
-desugarAllChecksNames Base = Refl
-desugarAllChecksNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllChecksNames prfs
-
-desugarAllBranchesNames Base = Refl
-desugarAllBranchesNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllBranchesNames prfs
-
--- Fallibly Desugar Terms ------------------------------------------------------
+ Context (x ** Term (Quote tyCtx tmCtx) m [<] (qtCtx :< x)) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+
+desugar' (Annot meta t a) =
+ let f = \t => Annot meta t a in
+ [| f (desugar' t) |]
+desugar' (Var meta i) = pure (Var meta i)
+desugar' (Let meta e (x ** t)) =
+ let f = \e, t => Let meta e (x ** t) in
+ [| f (desugar' e) (desugar' t) |]
+desugar' (LetTy meta a (x ** t)) =
+ let f = \t => LetTy meta a (x ** t) in
+ [| f (desugar' t) |]
+desugar' (Abs meta (bound ** t)) =
+ let f = \t => Abs meta (bound ** t) in
+ [| f (desugar' t) |]
+desugar' (App meta e ts) =
+ let f = \e, ts => App meta e ts in
+ [| f (desugar' e) (desugarAll ts) |]
+desugar' (Tup meta (MkRow ts fresh)) =
+ let f = \ts => Tup meta (fromAll ts fresh) in
+ [| f (desugarCtx ts) |]
+desugar' (Prj meta e l) =
+ let f = \e => Prj meta e l in
+ [| f (desugar' e) |]
+desugar' (Inj meta l t) =
+ let f = Inj meta l in
+ [| f (desugar' t) |]
+desugar' (Case meta e (MkRow ts fresh)) =
+ let f = \e, ts => Case meta e (fromAll ts fresh) in
+ [| f (desugar' e) (desugarBranches ts) |]
+desugar' (Roll meta t) =
+ let f = Roll meta in
+ [| f (desugar' t) |]
+desugar' (Unroll meta e) =
+ let f = Unroll meta in
+ [| f (desugar' e) |]
+desugar' (Fold meta e (x ** t)) =
+ let f = \e, t => Fold meta e (x ** t) in
+ [| f (desugar' e) (desugar' t) |]
+desugar' (Map meta (x ** a) b c) = pure $ Map meta (x ** a) b c
+desugar' (QuasiQuote meta t) = quote t
+desugar' (QAbs meta (bound ** t)) = desugar' t
+desugar' (Lit meta k) = pure $ lit meta k
+desugar' (Suc meta t) =
+ let f = suc meta in
+ [| f (desugar' t) |]
+desugar' (List meta ts) =
+ let f = list meta in
+ [| f (desugarAll ts) |]
+desugar' (Cons meta t u) =
+ let f = cons meta in
+ [| f (desugar' t) (desugar' u) |]
+desugar' (Str meta str) = string meta str
+
+desugarAll [] = pure []
+desugarAll (t :: ts) = [| desugar' t :: desugarAll ts |]
+
+desugarCtx [<] = pure [<]
+desugarCtx (ts :< (l :- t)) =
+ let f = \ts, t => ts :< (l :- t) in
+ [| f (desugarCtx ts) (desugar' t) |]
+
+desugarBranches [<] = pure [<]
+desugarBranches (ts :< (l :- (x ** t))) =
+ let f = \ts, t => ts :< (l :- (x ** t)) in
+ [| f (desugarBranches ts) (desugar' t) |]
+
+quote (Annot meta t a) =
+ let f = \t, a => Roll meta $ Inj meta "Annot" $ Tup meta [<"Body" :- t, "Ty" :- a] in
+ [| f (quote t) (desugar' a) |]
+quote (Var meta i) = pure $ Roll meta $ Inj meta "Var" $ lit meta (elemToNat i.pos)
+quote (Let meta e (x ** t)) =
+ let
+ f = \e, t =>
+ Roll meta.value $ Inj meta.value "Let" $
+ Tup meta.value [<"Value" :- e, "Body" :- t]
+ in
+ [| f (quote e) (quote t) |]
+quote (Abs meta (bound ** t)) =
+ let
+ f = \t => Roll meta $ Inj meta "Abs" $
+ Tup meta [<"Bound" :- lit meta (length bound), "Body" :- t]
+ in
+ [| f (quote t) |]
+quote (App meta e ts) =
+ let
+ f = \e, ts =>
+ Roll meta $ Inj meta "App" $
+ Tup meta [<"Fun" :- e, "Args" :- list meta ts]
+ in
+ [| f (quote e) (quoteAll ts) |]
+quote (Tup meta (MkRow ts _)) =
+ let f = Roll meta . Inj meta "Tup" . list meta in
+ [| f (quoteCtx ts) |]
+quote (Prj meta e l) =
+ let f = \e, l => Roll meta $ Inj meta "Prj" $ Tup meta [<"Target" :- e, "Label" :- l] in
+ [| f (quote e) (string meta l) |]
+quote (Inj meta l t) =
+ let f = \t, l => Roll meta $ Inj meta "Inj" $ Tup meta [<"Value" :- t, "Label" :- l] in
+ [| f (quote t) (string meta l) |]
+quote (Case meta e (MkRow ts _)) =
+ let
+ f = \e, ts =>
+ Roll meta $ Inj meta "Case" $
+ Tup meta [<"Target" :- e, "Branches" :- list meta ts]
+ in
+ [| f (quote e) (quoteBranches ts) |]
+quote (Roll meta t) =
+ let f = Roll meta . Inj meta "Roll" in
+ [| f (quote t) |]
+quote (Unroll meta e) =
+ let f = Roll meta . Inj meta "Unroll" in
+ [| f (quote e) |]
+quote (Fold meta e (x ** t)) =
+ let f = \e, t => Roll meta $ Inj meta "Fold" $ Tup meta [<"Target" :- e, "Body" :- t] in
+ [| f (quote e) (quote t) |]
+quote (Map meta a b c) =
+ let
+ f = \a, b, c =>
+ Roll meta $ Inj meta "Map" $
+ Tup meta [<"Functor" :- a, "Source" :- b, "Target" :- c]
+ in
+ [| f (desugar' a) (desugar' b) (desugar' c) |]
+quote (Unquote meta t) = desugar' t
+
+quoteAll [] = pure []
+quoteAll (t :: ts) = [| quote t :: quoteAll ts |]
+
+quoteCtx [<] = pure []
+quoteCtx (ts :< (l :- t)) =
+ let f = \ts, l, t => Tup meta [<"Label" :- l, "Value" :- t] :: ts in
+ [| f (quoteCtx ts) (string meta l) (quote t) |]
+
+quoteBranches [<] = pure []
+quoteBranches (ts :< (l :- (x ** t))) =
+ let f = \ts, l, t => Tup meta [<"Label" :- l, "Body" :- t] :: ts in
+ [| f (quoteBranches ts) (string meta l) (quote t) |]
export
-maybeDesugar : (len : LengthOf tyCtx) => Term Sugar m tyCtx tmCtx -> Maybe (Term NoSugar m tyCtx tmCtx)
-maybeDesugarList :
- (len : LengthOf tyCtx) =>
- List (Term Sugar m tyCtx tmCtx) -> Maybe (List $ Term NoSugar m tyCtx tmCtx)
-maybeDesugarAll :
- (len : LengthOf tyCtx) =>
- (ts : Context (Term Sugar m tyCtx tmCtx)) ->
- Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
-maybeDesugarBranches :
- (len : LengthOf tyCtx) =>
- (ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
- Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
-
-maybeDesugar (Annot meta t a) = do
- t <- maybeDesugar t
- pure (Annot meta t a)
-maybeDesugar (Var meta i) = pure (Var meta i)
-maybeDesugar (Let meta e (x ** t)) = do
- e <- maybeDesugar e
- t <- maybeDesugar t
- pure (Let meta e (x ** t))
-maybeDesugar (LetTy meta a (x ** t)) = do
- t <- maybeDesugar t
- pure (LetTy meta a (x ** t))
-maybeDesugar (Abs meta (bound ** t)) = do
- t <- maybeDesugar t
- pure (Abs meta (bound ** t))
-maybeDesugar (App meta e ts) = do
- e <- maybeDesugar e
- ts <- maybeDesugarList ts
- pure (App meta e ts)
-maybeDesugar (Tup meta (MkRow ts fresh)) = do
- ts <- maybeDesugarAll ts
- pure (Tup meta (fromAll ts fresh))
-maybeDesugar (Prj meta e l) = do
- e <- maybeDesugar e
- pure (Prj meta e l)
-maybeDesugar (Inj meta l t) = do
- t <- maybeDesugar t
- pure (Inj meta l t)
-maybeDesugar (Case meta e (MkRow ts fresh)) = do
- e <- maybeDesugar e
- ts <- maybeDesugarBranches ts
- pure (Case meta e (fromAll ts fresh))
-maybeDesugar (Roll meta t) = do
- t <- maybeDesugar t
- pure (Roll meta t)
-maybeDesugar (Unroll meta e) = do
- e <- maybeDesugar e
- pure (Unroll meta e)
-maybeDesugar (Fold meta e (x ** t)) = do
- e <- maybeDesugar e
- t <- maybeDesugar t
- pure (Fold meta e (x ** t))
-maybeDesugar (Map meta (x ** a) b c) =
- case (%% x `strictlyPositiveIn` a) of
- False `Because` contra => Nothing
- True `Because` prf =>
- pure $
- Annot meta
- (Abs meta
- (["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
- (TArrow (TArrow b c) (TArrow
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-maybeDesugarList [] = pure []
-maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
-
-maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = do
- ts <- maybeDesugarAll ts
- t <- maybeDesugar t
- pure (ts :< (l :- t))
-
-maybeDesugarBranches [<] = pure [<]
-maybeDesugarBranches (ts :< (l :- (x ** t))) = do
- ts <- maybeDesugarBranches ts
- t <- maybeDesugar t
- pure (ts :< (l :- (x ** t)))
+desugar : Term (Sugar qtCtx) m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+desugar t =
+ let
+ cache : Cache String
+ cache = MkCache {max = 0, vals = empty}
+ in
+ evalState cache (desugar' t)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:51:05 +0000