Add quotation to help metaprogramming.

1 files changed, 88 insertions, 25 deletions

diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 8fd15aa..0f05f59 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -16,7 +16,23 @@ import Flap.Decidable.Maybe
 --------------------------------------------------------------------------------
 
 public export
-data Mode = Sugar | NoSugar
+data Mode : Type where
+  Quote : (tyCtx, tmCtx : SnocList String) -> Mode
+  Sugar : (qtCtx : SnocList String) -> Mode
+  NoSugar : Mode
+
+namespace Mode
+  public export
+  NotQuote : Mode -> Type
+  NotQuote (Quote _ _) = Void
+  NotQuote (Sugar _) = So True
+  NotQuote NoSugar = So True
+
+  public export
+  HasSugar : Mode -> Type
+  HasSugar (Quote _ _) = So True
+  HasSugar (Sugar _) = So True
+  HasSugar NoSugar = Void
 
 public export
 record WithDoc (a : Type) where
@@ -25,11 +41,28 @@ record WithDoc (a : Type) where
   doc : List String
 
 public export
-data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
-  Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty tyCtx -> Term mode m tyCtx tmCtx
+data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+
+public export
+Ty' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+Ty' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+Ty' (Sugar qtCtx) m tyCtx tmCtx = Ty tyCtx
+Ty' NoSugar m tyCtx tmCtx = Ty tyCtx
+
+public export
+BoundTy' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+BoundTy' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+BoundTy' (Sugar qtCtx) m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+BoundTy' NoSugar m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+
+data Term where
+  Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Var : (meta : m) -> Var tmCtx -> Term mode m tyCtx tmCtx
   Let : (meta : WithDoc m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
-  LetTy : (meta : WithDoc m) -> Ty tyCtx -> (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
+  LetTy :
+    {auto 0 notQuote : NotQuote mode} ->
+    (meta : WithDoc m) -> Ty tyCtx ->
+    (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
   Abs : (meta : m) -> (bound ** Term mode m tyCtx (tmCtx <>< bound)) -> Term mode m tyCtx tmCtx
   App : (meta : m) -> Term mode m tyCtx tmCtx -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
   Tup : (meta : m) -> Row (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
@@ -39,7 +72,29 @@ data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
   Roll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Unroll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
   Fold : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
-  Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term Sugar m tyCtx tmCtx
+  Map : (meta : m) -> BoundTy' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+  -- Quotation sugar
+  QuasiQuote : (meta : m) -> Term (Quote tyCtx tmCtx) m [<] qtCtx -> Term (Sugar qtCtx) m tyCtx tmCtx
+  Unquote : (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx -> Term (Quote tyCtx tmCtx) m [<] qtCtx
+  QAbs : (meta : m) -> (bound ** Term (Sugar (qtCtx <>< bound)) m tyCtx tmCtx) -> Term (Sugar qtCtx) m tyCtx tmCtx
+  -- Other sugar
+  Lit :
+    (meta : m) -> Nat ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Suc :
+    (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  List :
+    (meta : m) -> List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Cons :
+    (meta : m) ->
+    Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
+  Str :
+    (meta : m) -> String ->
+    Term (Sugar qtCtx) m tyCtx tmCtx
 
 %name Term e, f, t, u
 
@@ -59,6 +114,14 @@ export
 (Unroll meta _).meta = meta
 (Fold meta _ _).meta = meta
 (Map meta _ _ _).meta = meta
+(QuasiQuote meta _).meta = meta
+(Unquote meta _).meta = meta
+(QAbs meta _).meta = meta
+(Lit meta _).meta = meta
+(Suc meta _).meta = meta
+(List meta _).meta = meta
+(Cons meta _ _).meta = meta
+(Str meta _).meta = meta
 
 --------------------------------------------------------------------------------
 -- Well Formed -----------------------------------------------------------------
@@ -126,7 +189,7 @@ isFunction (x :: bound) a =
 
 namespace Modes
   public export
-  data SynthsOnly : Term mode m tyCtx tmCtx -> Type where
+  data SynthsOnly : Term NoSugar m tyCtx tmCtx -> Type where
     Annot : SynthsOnly (Annot meta t a)
     Var : SynthsOnly (Var meta i)
     App : SynthsOnly (App meta f ts)
@@ -135,7 +198,7 @@ namespace Modes
     Map : SynthsOnly (Map meta (x ** a) b c)
 
   public export
-  data ChecksOnly : Term mode m tyCtx tmCtx -> Type where
+  data ChecksOnly : Term NoSugar m tyCtx tmCtx -> Type where
     Abs : ChecksOnly (Abs meta (bounds ** t))
     Inj : ChecksOnly (Inj meta l t)
     Case : ChecksOnly (Case meta e ts)
@@ -149,19 +212,19 @@ public export
 data Synths :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Term mode m tyCtx tmCtx -> Ty [<] -> Type
+  Term NoSugar m tyCtx tmCtx -> Ty [<] -> Type
 public export
 data Checks :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Ty [<] -> Term mode m tyCtx tmCtx -> Type
+  Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
 
 namespace Spine
   public export
   data CheckSpine :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type
+    Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Ty [<] -> Type
     where
     Nil : CheckSpine tyEnv tmEnv a [] a
     (::) :
@@ -176,7 +239,7 @@ namespace Synths
   data AllSynths :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type
+    Context (Term NoSugar m tyCtx tmCtx) -> Row (Ty [<]) -> Type
     where
     Lin : AllSynths tyEnv tmEnv [<] [<]
     (:<) :
@@ -192,7 +255,7 @@ namespace Checks
   data AllChecks :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+    Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Base : AllChecks tyEnv tmEnv [<] [<]
     Step :
@@ -208,7 +271,7 @@ namespace Branches
   data AllBranches :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+    Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
     where
     Base : AllBranches tyEnv tmEnv [<] a [<]
     Step :
@@ -233,7 +296,7 @@ data Synths where
   LetTyS :
     WellFormed a ->
     Synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e b ->
-    Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
+    Synths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e)) b
   AppS :
     Synths tyEnv tmEnv f a ->
     CheckSpine tyEnv tmEnv a ts b ->
@@ -263,9 +326,9 @@ data Checks where
     Alpha b c ->
     Checks tyEnv tmEnv c (Annot meta t a)
   VarC :
-    Synths tyEnv tmEnv (Var {mode} meta i) a ->
+    Synths tyEnv tmEnv (Var meta i) a ->
     Alpha a b ->
-    Checks tyEnv tmEnv b (Var {mode} meta i)
+    Checks tyEnv tmEnv b (Var meta i)
   LetC :
     Synths tyEnv tmEnv e a ->
     Checks tyEnv (tmEnv :< (x :- a)) b t ->
@@ -273,7 +336,7 @@ data Checks where
   LetTyC :
     WellFormed a ->
     Checks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t ->
-    Checks tyEnv tmEnv b (LetTy meta a (x ** t))
+    Checks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
   AbsC :
     IsFunction bound a dom cod ->
     Checks tyEnv (tmEnv <>< dom) cod t ->
@@ -334,19 +397,19 @@ public export
 data NotSynths :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Term mode m tyCtx tmCtx -> Type
+  Term NoSugar m tyCtx tmCtx -> Type
 public export
 data NotChecks :
   All (Assoc0 $ Ty [<]) tyCtx ->
   All (Assoc0 $ Ty [<]) tmCtx ->
-  Ty [<] -> Term mode m tyCtx tmCtx -> Type
+  Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
 
 namespace Spine
   public export
   data NotCheckSpine :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type
+    Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Step1 :
       ((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
@@ -362,7 +425,7 @@ namespace Synths
   data AnyNotSynths :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    (ts : Context (Term mode m tyCtx tmCtx)) -> Type
+    (ts : Context (Term NoSugar m tyCtx tmCtx)) -> Type
     where
     Step :
       These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
@@ -375,7 +438,7 @@ namespace Checks
   data AnyNotChecks :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+    Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
     where
     Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
     Step1 :
@@ -393,7 +456,7 @@ namespace Branches
   data AnyNotBranches :
     All (Assoc0 $ Ty [<]) tyCtx ->
     All (Assoc0 $ Ty [<]) tmCtx ->
-    Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+    Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
     where
     Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
     Step1 :
@@ -429,7 +492,7 @@ data NotSynths where
     NotSynths tyEnv tmEnv (Let meta e (x ** f))
   LetTyNS :
     These (IllFormed a) (NotSynths (tyEnv :< (x :- sub tyEnv a)) tmEnv e) ->
-    NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
+    NotSynths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e))
   AppNS1 :
     NotSynths tyEnv tmEnv f ->
     NotSynths tyEnv tmEnv (App meta f ts)
@@ -486,7 +549,7 @@ data NotChecks where
     NotChecks tyEnv tmEnv b (Let meta e (x ** t))
   LetTyNC :
     These (IllFormed a) (NotChecks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t) ->
-    NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
+    NotChecks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
   AbsNC1 :
     NotFunction bound a ->
     NotChecks tyEnv tmEnv a (Abs meta (bound ** t))