From f2490f5ca35b528c7332791c6932045eb9d5438b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 7 Jan 2025 13:50:13 +0000
Subject: Add quotation to help metaprogramming.

---
 src/Inky/Term/Desugar.idr | 479 +++++++++++++++++++++-------------------------
 1 file changed, 218 insertions(+), 261 deletions(-)

(limited to 'src/Inky/Term/Desugar.idr')

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)
-- 
cgit v1.2.3