summaryrefslogtreecommitdiff
path: root/src/Inky
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky')
-rw-r--r--src/Inky/Term.idr384
-rw-r--r--src/Inky/Term/Parser.idr147
-rw-r--r--src/Inky/Term/Pretty.idr260
3 files changed, 539 insertions, 252 deletions
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 88665ba..454c096 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -5,6 +5,7 @@ import public Inky.Type
import Control.Function
import Data.List.Quantifiers
+import Data.Singleton
import Data.These
import Inky.Data.SnocList.Quantifiers
import Inky.Decidable
@@ -17,25 +18,43 @@ import Inky.Decidable.Maybe
--------------------------------------------------------------------------------
public export
-data Term : (tyCtx, tmCtx : SnocList String) -> Type where
- Annot : Term tyCtx tmCtx -> Ty tyCtx -> Term tyCtx tmCtx
- Var : Var tmCtx -> Term tyCtx tmCtx
- Let : Term tyCtx tmCtx -> (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx
- LetTy : Ty tyCtx -> (x ** Term (tyCtx :< x) tmCtx) -> Term tyCtx tmCtx
- Abs : (bound ** Term tyCtx (tmCtx <>< bound)) -> Term tyCtx tmCtx
- App : Term tyCtx tmCtx -> List (Term tyCtx tmCtx) -> Term tyCtx tmCtx
- Tup : Row (Term tyCtx tmCtx) -> Term tyCtx tmCtx
- Prj : Term tyCtx tmCtx -> (l : String) -> Term tyCtx tmCtx
- Inj : (l : String) -> Term tyCtx tmCtx -> Term tyCtx tmCtx
- Case : Term tyCtx tmCtx -> Row (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx
- Roll : Term tyCtx tmCtx -> Term tyCtx tmCtx
- Unroll : Term tyCtx tmCtx -> Term tyCtx tmCtx
- Fold : Term tyCtx tmCtx -> (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx
- Map : (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term tyCtx tmCtx
- GetChildren : (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Term tyCtx tmCtx
+data Term : (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
+ Annot : (meta : m) -> Term m tyCtx tmCtx -> Ty tyCtx -> Term m tyCtx tmCtx
+ Var : (meta : m) -> Var tmCtx -> Term m tyCtx tmCtx
+ Let : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
+ LetTy : (meta : m) -> Ty tyCtx -> (x ** Term m (tyCtx :< x) tmCtx) -> Term m tyCtx tmCtx
+ Abs : (meta : m) -> (bound ** Term m tyCtx (tmCtx <>< bound)) -> Term m tyCtx tmCtx
+ App : (meta : m) -> Term m tyCtx tmCtx -> List (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
+ Tup : (meta : m) -> Row (Term m tyCtx tmCtx) -> Term m tyCtx tmCtx
+ Prj : (meta : m) -> Term m tyCtx tmCtx -> (l : String) -> Term m tyCtx tmCtx
+ Inj : (meta : m) -> (l : String) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
+ Case : (meta : m) -> Term m tyCtx tmCtx -> Row (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
+ Roll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
+ Unroll : (meta : m) -> Term m tyCtx tmCtx -> Term m tyCtx tmCtx
+ Fold : (meta : m) -> Term m tyCtx tmCtx -> (x ** Term m tyCtx (tmCtx :< x)) -> Term m tyCtx tmCtx
+ Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term m tyCtx tmCtx
+ GetChildren : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Term m tyCtx tmCtx
%name Term e, f, t, u
+export
+(.meta) : Term m tyCtx tmCtx -> m
+(Annot meta _ _).meta = meta
+(Var meta _).meta = meta
+(Let meta _ _).meta = meta
+(LetTy meta _ _).meta = meta
+(Abs meta _).meta = meta
+(App meta _ _).meta = meta
+(Tup meta _).meta = meta
+(Prj meta _ _).meta = meta
+(Inj meta _ _).meta = meta
+(Case meta _ _).meta = meta
+(Roll meta _).meta = meta
+(Unroll meta _).meta = meta
+(Fold meta _ _).meta = meta
+(Map meta _ _ _).meta = meta
+(GetChildren meta _ _).meta = meta
+
--------------------------------------------------------------------------------
-- Well Formed -----------------------------------------------------------------
--------------------------------------------------------------------------------
@@ -67,6 +86,13 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
%name NotFunction contra
export
+isFunctionRecompute :
+ {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod)
+isFunctionRecompute Done = (Val _, Val _)
+isFunctionRecompute (Step {a} prf) =
+ mapFst (\case Val _ => Val _) $ isFunctionRecompute prf
+
+export
isFunctionUnique :
IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod')
isFunctionUnique Done Done = (Refl, Refl)
@@ -102,40 +128,40 @@ isFunction (x :: bound) a =
namespace Modes
public export
- data SynthsOnly : Term tyCtx tmCtx -> Type where
- Annot : SynthsOnly (Annot t a)
- Var : SynthsOnly (Var i)
- App : SynthsOnly (App f ts)
- Prj : SynthsOnly (Prj e l)
- Unroll : SynthsOnly (Unroll e)
- Map : SynthsOnly (Map (x ** a) b c)
- GetChildren : SynthsOnly (GetChildren (x ** a) b)
+ data SynthsOnly : Term m tyCtx tmCtx -> Type where
+ Annot : SynthsOnly (Annot _ t a)
+ Var : SynthsOnly (Var _ i)
+ App : SynthsOnly (App _ f ts)
+ Prj : SynthsOnly (Prj _ e l)
+ Unroll : SynthsOnly (Unroll _ e)
+ Map : SynthsOnly (Map _ (x ** a) b c)
+ GetChildren : SynthsOnly (GetChildren _ (x ** a) b)
public export
- data ChecksOnly : Term tyCtx tmCtx -> Type where
- Abs : ChecksOnly (Abs (bounds ** t))
- Inj : ChecksOnly (Inj l t)
- Case : ChecksOnly (Case e ts)
- Roll : ChecksOnly (Roll t)
- Fold : ChecksOnly (Fold e (x ** t))
+ data ChecksOnly : Term m tyCtx tmCtx -> Type where
+ Abs : ChecksOnly (Abs _ (bounds ** t))
+ Inj : ChecksOnly (Inj _ l t)
+ Case : ChecksOnly (Case _ e ts)
+ Roll : ChecksOnly (Roll _ t)
+ Fold : ChecksOnly (Fold _ e (x ** t))
public export
data Synths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Term tyCtx tmCtx -> Ty [<] -> Type
+ Term m tyCtx tmCtx -> Ty [<] -> Type
public export
data Checks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> Term tyCtx tmCtx -> Type
+ Ty [<] -> Term m tyCtx tmCtx -> Type
namespace Spine
public export
data CheckSpine :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> List (Term tyCtx tmCtx) -> Ty [<] -> Type
+ Ty [<] -> List (Term m tyCtx tmCtx) -> Ty [<] -> Type
where
Nil : CheckSpine tyEnv tmEnv a [] a
(::) :
@@ -150,7 +176,7 @@ namespace Synths
data AllSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- (ts : Context (Term tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type
+ (ts : Context (Term m tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type
where
Lin : AllSynths tyEnv tmEnv [<] [<]
(:<) :
@@ -165,7 +191,7 @@ namespace Checks
data AllChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
where
Base : AllChecks tyEnv tmEnv [<] [<]
Step :
@@ -181,7 +207,7 @@ namespace Branches
data AllBranches :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
where
Base : AllBranches tyEnv tmEnv [<] a [<]
Step :
@@ -196,43 +222,43 @@ data Synths where
AnnotS :
Not (IllFormed a) ->
Checks tyEnv tmEnv (sub tyEnv a) t ->
- Synths tyEnv tmEnv (Annot t a) (sub tyEnv a)
+ Synths tyEnv tmEnv (Annot meta t a) (sub tyEnv a)
VarS :
- Synths tyEnv tmEnv (Var i) (indexAll i.pos tmEnv).extract
+ Synths tyEnv tmEnv (Var meta i) (indexAll i.pos tmEnv).extract
LetS :
Synths tyEnv tmEnv e a ->
Synths tyEnv (tmEnv :< (a `Over` Id)) f b ->
- Synths tyEnv tmEnv (Let e (x ** f)) b
+ Synths tyEnv tmEnv (Let meta e (x ** f)) b
LetTyS :
Not (IllFormed a) ->
Synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e b ->
- Synths tyEnv tmEnv (LetTy a (x ** e)) b
+ Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
AppS :
Synths tyEnv tmEnv f a ->
CheckSpine tyEnv tmEnv a ts b ->
- Synths tyEnv tmEnv (App f ts) b
+ Synths tyEnv tmEnv (App meta f ts) b
TupS :
AllSynths tyEnv tmEnv es.context as ->
- Synths tyEnv tmEnv (Tup es) (TProd (fromAll es as))
+ Synths tyEnv tmEnv (Tup meta es) (TProd (fromAll es as))
PrjS :
Synths tyEnv tmEnv e (TProd as) ->
Elem (l :- a) as.context ->
- Synths tyEnv tmEnv (Prj e l) a
+ Synths tyEnv tmEnv (Prj meta e l) a
UnrollS :
Synths tyEnv tmEnv e (TFix x a) ->
- Synths tyEnv tmEnv (Unroll e) (sub [<TFix x a `Over` Id] a)
+ Synths tyEnv tmEnv (Unroll meta e) (sub [<TFix x a `Over` Id] a)
MapS :
Not (IllFormed (TFix x a)) ->
Not (IllFormed b) ->
Not (IllFormed c) ->
- Synths tyEnv tmEnv (Map (x ** a) b c)
+ Synths tyEnv tmEnv (Map meta (x ** a) b c)
(TArrow (TArrow (sub tyEnv b) (sub tyEnv c))
(TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
(sub (tyEnv :< (sub tyEnv c `Over` Id)) a)))
GetChildrenS :
Not (IllFormed (TFix x a)) ->
Not (IllFormed b) ->
- Synths tyEnv tmEnv (GetChildren (x ** a) b)
+ Synths tyEnv tmEnv (GetChildren meta (x ** a) b)
(TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a)
(TProd
[<"Children" :- sub tyEnv b
@@ -247,33 +273,33 @@ data Checks where
LetC :
Synths tyEnv tmEnv e a ->
Checks tyEnv (tmEnv :< (a `Over` Id)) b t ->
- Checks tyEnv tmEnv b (Let e (x ** t))
+ Checks tyEnv tmEnv b (Let meta e (x ** t))
LetTyC :
Not (IllFormed a) ->
Checks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t ->
- Checks tyEnv tmEnv b (LetTy a (x ** t))
+ Checks tyEnv tmEnv b (LetTy meta a (x ** t))
AbsC :
IsFunction bound a dom cod ->
Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
- Checks tyEnv tmEnv a (Abs (bound ** t))
+ Checks tyEnv tmEnv a (Abs meta (bound ** t))
TupC :
AllChecks tyEnv tmEnv as.context ts.context ->
- Checks tyEnv tmEnv (TProd as) (Tup ts)
+ Checks tyEnv tmEnv (TProd as) (Tup meta ts)
InjC :
Elem (l :- a) as.context ->
Checks tyEnv tmEnv a t ->
- Checks tyEnv tmEnv (TSum as) (Inj l t)
+ Checks tyEnv tmEnv (TSum as) (Inj meta l t)
CaseC :
Synths tyEnv tmEnv e (TSum as) ->
AllBranches tyEnv tmEnv as.context a ts.context ->
- Checks tyEnv tmEnv a (Case e ts)
+ Checks tyEnv tmEnv a (Case meta e ts)
RollC :
Checks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
- Checks tyEnv tmEnv (TFix x a) (Roll t)
+ Checks tyEnv tmEnv (TFix x a) (Roll meta t)
FoldC :
Synths tyEnv tmEnv e (TFix x a) ->
Checks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
- Checks tyEnv tmEnv b (Fold e (y ** t))
+ Checks tyEnv tmEnv b (Fold meta e (y ** t))
%name Synths prf
%name Checks prf
@@ -282,19 +308,19 @@ public export
data NotSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Term tyCtx tmCtx -> Type
+ Term m tyCtx tmCtx -> Type
public export
data NotChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> Term tyCtx tmCtx -> Type
+ Ty [<] -> Term m tyCtx tmCtx -> Type
namespace Spine
public export
data NotCheckSpine :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Ty [<] -> List (Term tyCtx tmCtx) -> Type
+ Ty [<] -> List (Term m tyCtx tmCtx) -> Type
where
Step1 :
((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
@@ -310,7 +336,7 @@ namespace Synths
data AnyNotSynths :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- (ts : Context (Term tyCtx tmCtx)) -> Type
+ (ts : Context (Term m tyCtx tmCtx)) -> Type
where
Step :
These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
@@ -323,7 +349,7 @@ namespace Checks
data AnyNotChecks :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type
where
Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
Step1 :
@@ -341,7 +367,7 @@ namespace Branches
data AnyNotBranches :
All (const $ Thinned Ty [<]) tyCtx ->
All (const $ Thinned Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type
where
Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
Step1 :
@@ -362,51 +388,51 @@ data NotSynths where
NotSynths tyEnv tmEnv t
AnnotNS :
These (IllFormed a) (NotChecks tyEnv tmEnv (sub tyEnv a) t) ->
- NotSynths tyEnv tmEnv (Annot t a)
+ NotSynths tyEnv tmEnv (Annot meta t a)
LetNS1 :
NotSynths tyEnv tmEnv e ->
- NotSynths tyEnv tmEnv (Let e (x ** f))
+ NotSynths tyEnv tmEnv (Let meta e (x ** f))
LetNS2 :
Synths tyEnv tmEnv e a ->
NotSynths tyEnv (tmEnv :< (a `Over` Id)) f ->
- NotSynths tyEnv tmEnv (Let e (x ** f))
+ NotSynths tyEnv tmEnv (Let meta e (x ** f))
LetTyNS :
These (IllFormed a) (NotSynths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e) ->
- NotSynths tyEnv tmEnv (LetTy a (x ** e))
+ NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
AppNS1 :
NotSynths tyEnv tmEnv f ->
- NotSynths tyEnv tmEnv (App f ts)
+ NotSynths tyEnv tmEnv (App meta f ts)
AppNS2 :
Synths tyEnv tmEnv f a ->
NotCheckSpine tyEnv tmEnv a ts ->
- NotSynths tyEnv tmEnv (App f ts)
+ NotSynths tyEnv tmEnv (App meta f ts)
TupNS :
AnyNotSynths tyEnv tmEnv es.context ->
- NotSynths tyEnv tmEnv (Tup es)
+ NotSynths tyEnv tmEnv (Tup meta es)
PrjNS1 :
NotSynths tyEnv tmEnv e ->
- NotSynths tyEnv tmEnv (Prj e l)
+ NotSynths tyEnv tmEnv (Prj meta e l)
PrjNS2 :
Synths tyEnv tmEnv e a ->
((as : Row (Ty [<])) -> Not (a = TProd as)) ->
- NotSynths tyEnv tmEnv (Prj e l)
+ NotSynths tyEnv tmEnv (Prj meta e l)
PrjNS3 :
Synths tyEnv tmEnv e (TProd as) ->
((a : Ty [<]) -> Not (Elem (l :- a) as.context)) ->
- NotSynths tyEnv tmEnv (Prj e l)
+ NotSynths tyEnv tmEnv (Prj meta e l)
UnrollNS1 :
NotSynths tyEnv tmEnv e ->
- NotSynths tyEnv tmEnv (Unroll e)
+ NotSynths tyEnv tmEnv (Unroll meta e)
UnrollNS2 :
Synths tyEnv tmEnv e a ->
((x : String) -> (b : Ty [<x]) -> Not (a = TFix x b)) ->
- NotSynths tyEnv tmEnv (Unroll e)
+ NotSynths tyEnv tmEnv (Unroll meta e)
MapNS :
These (IllFormed (TFix x a)) (These (IllFormed b) (IllFormed c)) ->
- NotSynths tyEnv tmEnv (Map (x ** a) b c)
+ NotSynths tyEnv tmEnv (Map meta (x ** a) b c)
GetChildrenNS :
These (IllFormed (TFix x a)) (IllFormed b) ->
- NotSynths tyEnv tmEnv (GetChildren (x ** a) b)
+ NotSynths tyEnv tmEnv (GetChildren meta (x ** a) b)
data NotChecks where
EmbedNC1 :
@@ -420,76 +446,112 @@ data NotChecks where
NotChecks tyEnv tmEnv b e
LetNC1 :
NotSynths tyEnv tmEnv e ->
- NotChecks tyEnv tmEnv b (Let e (x ** t))
+ NotChecks tyEnv tmEnv b (Let meta e (x ** t))
LetNC2 :
Synths tyEnv tmEnv e a ->
NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t ->
- NotChecks tyEnv tmEnv b (Let e (x ** t))
+ NotChecks tyEnv tmEnv b (Let meta e (x ** t))
LetTyNC :
These (IllFormed a) (NotChecks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t) ->
- NotChecks tyEnv tmEnv b (LetTy a (x ** t))
+ NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
AbsNC1 :
NotFunction bound a ->
- NotChecks tyEnv tmEnv a (Abs (bound ** t))
+ NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
AbsNC2 :
IsFunction bound a dom cod ->
NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t ->
- NotChecks tyEnv tmEnv a (Abs (bound ** t))
+ NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
TupNC1 :
((as : Row (Ty [<])) -> Not (a = TProd as)) ->
- NotChecks tyEnv tmEnv a (Tup ts)
+ NotChecks tyEnv tmEnv a (Tup meta ts)
TupNC2 :
AnyNotChecks tyEnv tmEnv as.context ts.context ->
- NotChecks tyEnv tmEnv (TProd as) (Tup ts)
+ NotChecks tyEnv tmEnv (TProd as) (Tup meta ts)
InjNC1 :
((as : Row (Ty [<])) -> Not (a = TSum as)) ->
- NotChecks tyEnv tmEnv a (Inj l t)
+ NotChecks tyEnv tmEnv a (Inj meta l t)
InjNC2 :
((a : Ty [<]) -> Not (Elem (l :- a) as.context)) ->
- NotChecks tyEnv tmEnv (TSum as) (Inj l t)
+ NotChecks tyEnv tmEnv (TSum as) (Inj meta l t)
InjNC3 :
Elem (l :- a) as.context ->
NotChecks tyEnv tmEnv a t ->
- NotChecks tyEnv tmEnv (TSum as) (Inj l t)
+ NotChecks tyEnv tmEnv (TSum as) (Inj meta l t)
CaseNC1 :
NotSynths tyEnv tmEnv e ->
- NotChecks tyEnv tmEnv a (Case e ts)
+ NotChecks tyEnv tmEnv a (Case meta e ts)
CaseNC2 :
Synths tyEnv tmEnv e b ->
((as : Row (Ty [<])) -> Not (b = TSum as)) ->
- NotChecks tyEnv tmEnv a (Case e ts)
+ NotChecks tyEnv tmEnv a (Case meta e ts)
CaseNC3 :
Synths tyEnv tmEnv e (TSum as) ->
AnyNotBranches tyEnv tmEnv as.context a ts.context ->
- NotChecks tyEnv tmEnv a (Case e ts)
+ NotChecks tyEnv tmEnv a (Case meta e ts)
RollNC1 :
((x : String) -> (b : Ty [<x]) -> Not (a = TFix x b)) ->
- NotChecks tyEnv tmEnv a (Roll t)
+ NotChecks tyEnv tmEnv a (Roll meta t)
RollNC2 :
NotChecks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t ->
- NotChecks tyEnv tmEnv (TFix x a) (Roll t)
+ NotChecks tyEnv tmEnv (TFix x a) (Roll meta t)
FoldNC1 :
NotSynths tyEnv tmEnv e ->
- NotChecks tyEnv tmEnv b (Fold e (y ** t))
+ NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
FoldNC2 :
Synths tyEnv tmEnv e a ->
((x : String) -> (c : Ty [<x]) -> Not (a = TFix x c)) ->
- NotChecks tyEnv tmEnv b (Fold e (y ** t))
+ NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
FoldNC3 :
Synths tyEnv tmEnv e (TFix x a) ->
NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t ->
- NotChecks tyEnv tmEnv b (Fold e (y ** t))
+ NotChecks tyEnv tmEnv b (Fold meta e (y ** t))
%name NotSynths contra
%name NotChecks contra
-Uninhabited (NotSynths tyEnv tmEnv (Var i)) where
+Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where
uninhabited (ChecksNS Abs) impossible
uninhabited (ChecksNS Inj) impossible
uninhabited (ChecksNS Case) impossible
uninhabited (ChecksNS Roll) impossible
uninhabited (ChecksNS Fold) impossible
+-- Can recompute type from synthesis proof
+
+export
+synthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
+ Synths tyEnv tmEnv e a -> Singleton a
+checkSpineRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {a : _} ->
+ CheckSpine tyEnv tmEnv a ts b -> Singleton b
+allSynthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
+ {0 as : All (const $ Ty [<]) es.names} ->
+ AllSynths tyEnv tmEnv es as -> Singleton as
+
+synthsRecompute (AnnotS wf prf) = Val _
+synthsRecompute VarS = Val _
+synthsRecompute (LetS prf1 prf2) with (synthsRecompute prf1)
+ _ | Val _ = synthsRecompute prf2
+synthsRecompute (LetTyS wf prf) = synthsRecompute prf
+synthsRecompute (AppS prf prfs) with (synthsRecompute prf)
+ _ | Val _ = checkSpineRecompute prfs
+synthsRecompute (TupS prfs) with (allSynthsRecompute prfs)
+ _ | Val _ = Val _
+synthsRecompute (PrjS prf i) with (synthsRecompute prf)
+ _ | Val _ = [| (nameOf i).value |]
+synthsRecompute (UnrollS prf) with (synthsRecompute prf)
+ _ | Val _ = Val _
+synthsRecompute (MapS f g h) = Val _
+synthsRecompute (GetChildrenS f g) = Val _
+
+checkSpineRecompute [] = Val _
+checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
+
+allSynthsRecompute [<] = Val _
+allSynthsRecompute (prfs :< prf) = [| allSynthsRecompute prfs :< synthsRecompute prf |]
+
-- Synthesis gives unique types
synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
@@ -658,58 +720,58 @@ fallbackCheck prf p a =
synths :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (e : Term tyCtx tmCtx) ->
+ (e : Term m tyCtx tmCtx) ->
Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e)
export
checks :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (a : Ty [<]) -> (t : Term tyCtx tmCtx) ->
+ (a : Ty [<]) -> (t : Term m tyCtx tmCtx) ->
LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t)
checkSpine :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (a : Ty [<]) -> (ts : List (Term tyCtx tmCtx)) ->
+ (a : Ty [<]) -> (ts : List (Term m tyCtx tmCtx)) ->
Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts)
allSynths :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (es : Context (Term tyCtx tmCtx)) ->
+ (es : Context (Term m tyCtx tmCtx)) ->
Proof (All (const $ Ty [<]) es.names) (AllSynths tyEnv tmEnv es) (AnyNotSynths tyEnv tmEnv es)
allChecks :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (as : Context (Ty [<])) -> (ts : Context (Term tyCtx tmCtx)) ->
+ (as : Context (Ty [<])) -> (ts : Context (Term m tyCtx tmCtx)) ->
LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts)
allBranches :
(tyEnv : All (const $ Thinned Ty [<]) tyCtx) ->
(tmEnv : All (const $ Thinned Ty [<]) tmCtx) ->
- (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term tyCtx (tmCtx :< x))) ->
+ (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term m tyCtx (tmCtx :< x))) ->
LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
-synths tyEnv tmEnv (Annot t a) =
+synths tyEnv tmEnv (Annot _ t a) =
pure (sub tyEnv a) $
map (uncurry AnnotS) AnnotNS $
all (not $ illFormed a) (checks tyEnv tmEnv (sub tyEnv a) t)
-synths tyEnv tmEnv (Var i) = Just (indexAll i.pos tmEnv).extract `Because` VarS
-synths tyEnv tmEnv (Let e (x ** f)) =
+synths tyEnv tmEnv (Var _ i) = Just (indexAll i.pos tmEnv).extract `Because` VarS
+synths tyEnv tmEnv (Let _ e (x ** f)) =
map snd
(\(_, _), (prf1, prf2) => LetS prf1 prf2)
(either LetNS1 (\xPrfs => uncurry LetNS2 (snd xPrfs))) $
(a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (a `Over` Id)) f
-synths tyEnv tmEnv (LetTy a (x ** e)) =
+synths tyEnv tmEnv (LetTy _ a (x ** e)) =
map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $
all (not $ illFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e)
-synths tyEnv tmEnv (Abs (bound ** t)) = Nothing `Because` ChecksNS Abs
-synths tyEnv tmEnv (App e ts) =
+synths tyEnv tmEnv (Abs _ (bound ** t)) = Nothing `Because` ChecksNS Abs
+synths tyEnv tmEnv (App _ e ts) =
map snd
(\(_, _), (prf1, prf2) => AppS prf1 prf2)
(either AppNS1 (\xPrfs => uncurry AppNS2 (snd xPrfs))) $
(a := synths tyEnv tmEnv e) >=> checkSpine tyEnv tmEnv a ts
-synths tyEnv tmEnv (Tup (MkRow es fresh)) =
+synths tyEnv tmEnv (Tup _ (MkRow es fresh)) =
map (TProd . fromAll (MkRow es fresh)) (\_ => TupS) TupNS $
allSynths tyEnv tmEnv es
-synths tyEnv tmEnv (Prj e l) =
+synths tyEnv tmEnv (Prj meta e l) =
map (snd . snd) true false $
(a := synths tyEnv tmEnv e) >=>
(as := isProd a) >=>
@@ -718,7 +780,7 @@ synths tyEnv tmEnv (Prj e l) =
true :
(x : (Ty [<], Row (Ty [<]), Ty [<])) ->
(Synths tyEnv tmEnv e (fst x), uncurry (\x, yz => (x = TProd (fst yz), uncurry (\y,z => Elem (l :- z) y.context) yz)) x) ->
- Synths tyEnv tmEnv (Prj e l) (snd $ snd x)
+ Synths tyEnv tmEnv (Prj meta e l) (snd $ snd x)
true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i
false :
@@ -728,14 +790,14 @@ synths tyEnv tmEnv (Prj e l) =
Either
((as : Row (Ty [<])) -> Not (a = TProd as))
(as : Row (Ty [<]) ** (a = TProd as, (b : Ty [<]) -> Not (Elem (l :- b) as.context))))) ->
- NotSynths tyEnv tmEnv (Prj e l)
+ NotSynths tyEnv tmEnv (Prj meta e l)
false (Left contra) = PrjNS1 contra
false (Right (a ** (prf1, Left contra))) = PrjNS2 prf1 contra
false (Right (.(TProd as) ** (prf1, Right (as ** (Refl, contra))))) = PrjNS3 prf1 contra
-synths tyEnv tmEnv (Inj l t) = Nothing `Because` ChecksNS Inj
-synths tyEnv tmEnv (Case e (MkRow ts _)) = Nothing `Because` ChecksNS Case
-synths tyEnv tmEnv (Roll t) = Nothing `Because` ChecksNS Roll
-synths tyEnv tmEnv (Unroll e) =
+synths tyEnv tmEnv (Inj _ l t) = Nothing `Because` ChecksNS Inj
+synths tyEnv tmEnv (Case _ e (MkRow ts _)) = Nothing `Because` ChecksNS Case
+synths tyEnv tmEnv (Roll _ t) = Nothing `Because` ChecksNS Roll
+synths tyEnv tmEnv (Unroll _ e) =
map f true false $
synths tyEnv tmEnv e `andThen` isFix
where
@@ -745,37 +807,37 @@ synths tyEnv tmEnv (Unroll e) =
true :
(axb : _) ->
(Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) axb) ->
- Synths tyEnv tmEnv (Unroll e) (f axb)
+ Synths tyEnv tmEnv (Unroll meta e) (f axb)
true (.(TFix x a), (x ** a)) (prf, Refl) = UnrollS prf
false :
Either
(NotSynths tyEnv tmEnv e)
(a ** (Synths tyEnv tmEnv e a, (x : _) -> (b : _) -> Not (a = TFix x b))) ->
- NotSynths tyEnv tmEnv (Unroll e)
+ NotSynths tyEnv tmEnv (Unroll meta e)
false (Left contra) = UnrollNS1 contra
false (Right (a ** (prf, contra))) = UnrollNS2 prf contra
-synths tyEnv tmEnv (Fold e (x ** t)) = Nothing `Because` ChecksNS Fold
-synths tyEnv tmEnv (Map (x ** a) b c) =
+synths tyEnv tmEnv (Fold _ e (x ** t)) = Nothing `Because` ChecksNS Fold
+synths tyEnv tmEnv (Map _ (x ** a) b c) =
pure _ $
map (\(wf1, wf2, wf3) => MapS wf1 wf2 wf3) MapNS $
all (not $ illFormed (TFix x a)) (all (not $ illFormed b) (not $ illFormed c))
-synths tyEnv tmEnv (GetChildren (x ** a) b) =
+synths tyEnv tmEnv (GetChildren _ (x ** a) b) =
pure _ $
map (uncurry GetChildrenS) GetChildrenNS $
all (not $ illFormed (TFix x a)) (not $ illFormed b)
-checks tyEnv tmEnv a (Annot t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot t b) a
-checks tyEnv tmEnv a (Var i) = fallbackCheck Var (synths tyEnv tmEnv $ Var i) a
-checks tyEnv tmEnv a (Let e (x ** t)) =
+checks tyEnv tmEnv a (Annot meta t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot meta t b) a
+checks tyEnv tmEnv a (Var meta i) = fallbackCheck Var (synths tyEnv tmEnv $ Var meta i) a
+checks tyEnv tmEnv a (Let _ e (x ** t)) =
map
(\(_ ** (prf1, prf2)) => LetC prf1 prf2)
(either LetNC1 (\xPrfs => uncurry LetNC2 $ snd xPrfs)) $
(b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (b `Over` Id)) a t
-checks tyEnv tmEnv a (LetTy b (x ** t)) =
+checks tyEnv tmEnv a (LetTy _ b (x ** t)) =
map (uncurry LetTyC) LetTyNC $
all (not $ illFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t)
-checks tyEnv tmEnv a (Abs (bound ** t)) =
+checks tyEnv tmEnv a (Abs meta (bound ** t)) =
map
(\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2)
(either AbsNC1 false) $
@@ -784,17 +846,17 @@ checks tyEnv tmEnv a (Abs (bound ** t)) =
where
false :
(x ** (uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst x)) (snd x) t)) ->
- NotChecks tyEnv tmEnv a (Abs (bound ** t))
+ NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
false ((_,_) ** prf) = uncurry AbsNC2 prf
-checks tyEnv tmEnv a (App f ts) = fallbackCheck App (synths tyEnv tmEnv $ App f ts) a
-checks tyEnv tmEnv a (Tup (MkRow ts fresh')) =
+checks tyEnv tmEnv a (App meta f ts) = fallbackCheck App (synths tyEnv tmEnv $ App meta f ts) a
+checks tyEnv tmEnv a (Tup _ (MkRow ts fresh')) =
map true false $
(as := isProd a) >=> allChecks tyEnv tmEnv as.context ts
where
true :
forall a.
(as : Row (Ty [<]) ** (a = TProd as, AllChecks tyEnv tmEnv as.context ts)) ->
- Checks tyEnv tmEnv a (Tup (MkRow ts fresh'))
+ Checks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
true (as ** (Refl, prf)) = TupC prf
false :
@@ -802,11 +864,11 @@ checks tyEnv tmEnv a (Tup (MkRow ts fresh')) =
Either
((as : Row (Ty [<])) -> Not (a = TProd as))
(as : Row (Ty [<]) ** (a = TProd as, AnyNotChecks tyEnv tmEnv as.context ts)) ->
- NotChecks tyEnv tmEnv a (Tup (MkRow ts fresh'))
+ NotChecks tyEnv tmEnv a (Tup meta (MkRow ts fresh'))
false (Left contra) = TupNC1 contra
false (Right (as ** (Refl, contra))) = TupNC2 contra
-checks tyEnv tmEnv a (Prj e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj e l) a
-checks tyEnv tmEnv a (Inj l t) =
+checks tyEnv tmEnv a (Prj meta e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj meta e l) a
+checks tyEnv tmEnv a (Inj _ l t) =
map true false $
(as := isSum a) >=>
(b := decLookup l as.context) >=>
@@ -815,7 +877,7 @@ checks tyEnv tmEnv a (Inj l t) =
true :
forall a.
(as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) ->
- Checks tyEnv tmEnv a (Inj l t)
+ Checks tyEnv tmEnv a (Inj meta l t)
true (as ** (Refl, (b ** (i, prf)))) = InjC i prf
false :
@@ -826,11 +888,11 @@ checks tyEnv tmEnv a (Inj l t) =
Either
((b : _) -> Not (Elem (l :- b) as.context))
(b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b t)))) ->
- NotChecks tyEnv tmEnv a (Inj l t)
+ NotChecks tyEnv tmEnv a (Inj meta l t)
false (Left contra) = InjNC1 contra
false (Right (as ** (Refl, Left contra))) = InjNC2 contra
false (Right (as ** (Refl, Right (b ** (i, contra))))) = InjNC3 i contra
-checks tyEnv tmEnv a (Case e (MkRow ts fresh)) =
+checks tyEnv tmEnv a (Case _ e (MkRow ts fresh)) =
map true false $
(b := synths tyEnv tmEnv e) >=>
(as := isSum b) >=>
@@ -839,7 +901,7 @@ checks tyEnv tmEnv a (Case e (MkRow ts fresh)) =
true :
forall fresh.
(b ** (Synths tyEnv tmEnv e b, (as ** (b = TSum as, AllBranches tyEnv tmEnv as.context a ts)))) ->
- Checks tyEnv tmEnv a (Case e (MkRow ts fresh))
+ Checks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs
false :
@@ -850,11 +912,11 @@ checks tyEnv tmEnv a (Case e (MkRow ts fresh)) =
Either
((as : _) -> Not (b = TSum as))
(as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) ->
- NotChecks tyEnv tmEnv a (Case e (MkRow ts fresh))
+ NotChecks tyEnv tmEnv a (Case meta e (MkRow ts fresh))
false (Left contra) = CaseNC1 contra
false (Right (b ** (prf, Left contra))) = CaseNC2 prf contra
false (Right (.(TSum as) ** (prf, Right (as ** (Refl, contras))))) = CaseNC3 prf contras
-checks tyEnv tmEnv a (Roll t) =
+checks tyEnv tmEnv a (Roll _ t) =
map true false $
(xb := isFix a) >=> checks tyEnv tmEnv (ty xb) t
where
@@ -864,7 +926,7 @@ checks tyEnv tmEnv a (Roll t) =
true :
forall a.
(xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), Checks tyEnv tmEnv (ty xb) t)) ->
- Checks tyEnv tmEnv a (Roll t)
+ Checks tyEnv tmEnv a (Roll meta t)
true ((x ** b) ** (Refl, prf)) = RollC prf
false :
@@ -872,11 +934,11 @@ checks tyEnv tmEnv a (Roll t) =
Either
((x : _) -> (b : Ty [<x]) -> Not (a = TFix x b))
(xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), NotChecks tyEnv tmEnv (ty xb) t)) ->
- NotChecks tyEnv tmEnv a (Roll t)
+ NotChecks tyEnv tmEnv a (Roll meta t)
false (Left contra) = RollNC1 contra
false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra
-checks tyEnv tmEnv a (Unroll e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll e) a
-checks tyEnv tmEnv a (Fold e (x ** t)) =
+checks tyEnv tmEnv a (Unroll meta e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll meta e) a
+checks tyEnv tmEnv a (Fold _ e (x ** t)) =
map true false $
(b := synths tyEnv tmEnv e) >=>
(yc := isFix b) >=>
@@ -888,7 +950,7 @@ checks tyEnv tmEnv a (Fold e (x ** t)) =
true :
(b ** (Synths tyEnv tmEnv e b,
(yc ** (b = TFix (fst yc) (snd yc), Checks tyEnv (tmEnv' yc) a t)))) ->
- Checks tyEnv tmEnv a (Fold e (x ** t))
+ Checks tyEnv tmEnv a (Fold meta e (x ** t))
true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2
false :
@@ -898,14 +960,14 @@ checks tyEnv tmEnv a (Fold e (x ** t)) =
Either
((y : _) -> (c : Ty [<y]) -> Not (b = TFix y c))
(yc ** (b = TFix (fst yc) (snd yc), NotChecks tyEnv (tmEnv' yc) a t)))) ->
- NotChecks tyEnv tmEnv a (Fold e (x ** t))
+ NotChecks tyEnv tmEnv a (Fold meta e (x ** t))
false (Left contra) = FoldNC1 contra
false (Right (b ** (prf1, Left contra))) = FoldNC2 prf1 contra
false (Right (.(TFix y b) ** (prf1, Right ((y ** b) ** (Refl, contra))))) = FoldNC3 prf1 contra
-checks tyEnv tmEnv a (Map (x ** b) c d) =
- fallbackCheck Map (synths tyEnv tmEnv $ Map (x ** b) c d) a
-checks tyEnv tmEnv a (GetChildren (x ** b) c) =
- fallbackCheck GetChildren (synths tyEnv tmEnv $ GetChildren (x ** b) c) a
+checks tyEnv tmEnv a (Map meta (x ** b) c d) =
+ fallbackCheck Map (synths tyEnv tmEnv $ Map meta (x ** b) c d) a
+checks tyEnv tmEnv a (GetChildren meta (x ** b) c) =
+ fallbackCheck GetChildren (synths tyEnv tmEnv $ GetChildren meta (x ** b) c) a
checkSpine tyEnv tmEnv a [] = Just a `Because` []
checkSpine tyEnv tmEnv a (t :: ts) =
@@ -961,34 +1023,36 @@ allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) =
-- Sugar -----------------------------------------------------------------------
public export
-CheckLit : Nat -> Term tyCtx tmCtx
-CheckLit 0 = Roll (Inj "Z" $ Tup [<])
-CheckLit (S n) = Roll (Inj "S" $ CheckLit n)
+CheckLit : m -> Nat -> Term m tyCtx tmCtx
+CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
+CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n)
public export
-Lit : Nat -> Term tyCtx tmCtx
-Lit n = Annot (CheckLit n) TNat
+Lit : m -> Nat -> Term m tyCtx tmCtx
+Lit meta n = Annot meta (CheckLit meta n) TNat
public export
-Suc : Term tyCtx tmCtx
-Suc = Annot (Abs (["_x"] ** Roll (Inj "S" $ Var (%% "_x")))) (TArrow TNat TNat)
+Suc : m -> Term m tyCtx tmCtx
+Suc meta =
+ Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x"))))
+ (TArrow TNat TNat)
export
-isCheckLit : Term tyCtx tmCtx -> Maybe Nat
-isCheckLit (Roll (Inj "Z" (Tup (MkRow [<] _)))) = Just 0
-isCheckLit (Roll (Inj "S" t)) = S <$> isCheckLit t
+isCheckLit : Term m tyCtx tmCtx -> Maybe Nat
+isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0
+isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t
isCheckLit _ = Nothing
export
-isLit : Term tyCtx tmCtx -> Maybe Nat
-isLit (Annot t a) =
+isLit : Term m tyCtx tmCtx -> Maybe Nat
+isLit (Annot _ t a) =
if (alpha {ctx2 = [<]} a TNat).does
then isCheckLit t
else Nothing
isLit _ = Nothing
export
-isSuc : Term tyCtx tmCtx -> Bool
-isSuc (Annot (Abs ([x] ** Roll (Inj "S" $ Var ((%%) x {pos = Here})))) a) =
+isSuc : Term m tyCtx tmCtx -> Bool
+isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) =
does (alpha {ctx2 = [<]} a (TArrow TNat TNat))
isSuc _ = False
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 90b4e08..ee122bb 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -267,12 +267,12 @@ mkVar f x =
Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
mkVar2 :
- ({tyCtx, tmCtx : _} -> Var tmCtx -> p tyCtx tmCtx) ->
+ ({tyCtx, tmCtx : _} -> WithBounds (Var tmCtx) -> p tyCtx tmCtx) ->
WithBounds String -> ParseFun 2 p
mkVar2 f x =
MkParseFun
(\tyCtx, tmCtx => case Var.lookup x.val tmCtx of
- Just i => pure (f i)
+ Just i => pure (f $ i <$ x)
Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
public export
@@ -281,7 +281,7 @@ TypeFun = ParseFun 1 Ty
public export
TermFun : Type
-TermFun = ParseFun 2 Term
+TermFun = ParseFun 2 (Term Bounds)
public export
TypeParser : SnocList String -> SnocList String -> Type
@@ -383,57 +383,58 @@ OpenTypeWf = Oh
AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AtomTerm =
OneOf
- [ mkVar2 Var <$> WithBounds (match TermIdent)
- , mkLit <$> match Lit
- , mkSuc <$ match Suc
- , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $
+ [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+ , mkLit <$> WithBounds (match Lit)
+ , mkSuc <$> WithBounds (match Suc)
+ , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
, enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
]
where
- mkLit : Nat -> TermFun
- mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k))
+ mkLit : WithBounds Nat -> TermFun
+ mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k.bounds k.val))
- mkSuc : TermFun
- mkSuc = MkParseFun (\_, _ => pure Suc)
+ mkSuc : WithBounds () -> TermFun
+ mkSuc x = MkParseFun (\_, _ => pure (Suc x.bounds))
- mkTup : List (WithBounds $ Assoc TermFun) -> TermFun
- mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup <$> tryRow2 xs tyCtx tmCtx)
+ mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun
+ mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx)
PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
PrefixTerm =
Fix "prefixTerm" $ OneOf
- [ match Tilde **> (mkRoll <$> Var (%%% "prefixTerm"))
- , match Bang **> mkUnroll <$> Var (%%% "prefixTerm")
+ [ mkRoll <$> WithBounds (match Tilde **> Var (%%% "prefixTerm"))
+ , mkUnroll <$> WithBounds (match Bang **> Var (%%% "prefixTerm"))
, rename (Drop Id) Id AtomTerm
]
where
- mkRoll : TermFun -> TermFun
- mkRoll x = MkParseFun (\tyCtx, tmCtx => [| Roll (x.try tyCtx tmCtx) |])
+ mkRoll : WithBounds TermFun -> TermFun
+ mkRoll x = MkParseFun (\tyCtx, tmCtx => pure $ Roll x.bounds !(x.val.try tyCtx tmCtx))
- mkUnroll : TermFun -> TermFun
- mkUnroll x = MkParseFun (\tyCtx, tmCtx => [| Unroll (x.try tyCtx tmCtx) |])
+ mkUnroll : WithBounds TermFun -> TermFun
+ mkUnroll x = MkParseFun (\tyCtx, tmCtx => pure $ Unroll x.bounds !(x.val.try tyCtx tmCtx))
SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
-SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> match TypeIdent) ]
+SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (match TypeIdent)) ]
where
- mkSuffix : HList [TermFun, List String] -> TermFun
+ mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun
mkSuffix [t, []] = t
mkSuffix [t, prjs] =
- MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !(t.try tyCtx tmCtx) prjs)
+ MkParseFun (\tyCtx, tmCtx =>
+ pure $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try tyCtx tmCtx) prjs)
AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AppTerm =
OneOf
[ mkInj <$> Seq
- [ match TypeIdent
+ [ WithBounds (match TypeIdent)
, weaken (S Z) SuffixTerm
]
, mkApp <$> Seq
[ OneOf {nils = [False, False, False]}
- [ SuffixTerm
+ [ WithBounds SuffixTerm
, mkMap <$> Seq
- [ match Map
+ [ WithBounds (match Map)
, enclose (match ParenOpen) (match ParenClose) $ Seq
[ match Backslash
, match TypeIdent
@@ -444,7 +445,7 @@ AppTerm =
, sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
]
, mkGetChildren <$> Seq
- [ match GetChildren
+ [ WithBounds (match GetChildren)
, enclose (match ParenOpen) (match ParenClose) $ Seq
[ match Backslash
, match TypeIdent
@@ -458,26 +459,29 @@ AppTerm =
]
]
where
- mkInj : HList [String, TermFun] -> TermFun
- mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx)
+ mkInj : HList [WithBounds String, TermFun] -> TermFun
+ mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx)
- mkMap : HList [_, HList [_, String, _, TypeFun], TypeFun, TypeFun] -> TermFun
- mkMap [_, [_, x, _, a], b, c] =
+ mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun
+ mkMap [m, [_, x, _, a], b, c] =
MkParseFun (\tyCtx, tmCtx =>
- pure $ Map (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+ pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+ <$ m
- mkGetChildren : HList [_, HList [_, String, _, TypeFun], TypeFun] -> TermFun
- mkGetChildren [_, [_, x, _, a], b] =
+ mkGetChildren : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun] -> WithBounds TermFun
+ mkGetChildren [m, [_, x, _, a], b] =
MkParseFun (\tyCtx, tmCtx =>
- pure $ GetChildren (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
+ pure $ GetChildren m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx))
+ <$ m
- mkApp : HList [TermFun, List TermFun] -> TermFun
- mkApp [t, []] = t
+ mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun
+ mkApp [t, []] = t.val
mkApp [fun, (arg :: args)] =
MkParseFun (\tyCtx, tmCtx =>
pure $
App
- !(fun.try tyCtx tmCtx)
+ fun.bounds
+ !(fun.val.try tyCtx tmCtx)
( !(arg.try tyCtx tmCtx)
:: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
@@ -485,12 +489,13 @@ AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AnnotTerm =
mkAnnot <$> Seq
[ AppTerm
- , option (match Colon **> rename Id (Drop Id) OpenType)
+ , option (match Colon **> WithBounds (rename Id (Drop Id) OpenType))
]
where
- mkAnnot : HList [TermFun, Maybe TypeFun] -> TermFun
+ mkAnnot : HList [TermFun, Maybe (WithBounds TypeFun)] -> TermFun
mkAnnot [t, Nothing] = t
- mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |])
+ mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx =>
+ pure $ Annot a.bounds !(t.try tyCtx tmCtx) !(a.val.try tyCtx))
-- Open Terms
@@ -499,12 +504,12 @@ LetTerm =
match Let **>
OneOf
[ mkLet <$> Seq
- [ match TermIdent
+ [ WithBounds (match TermIdent)
, OneOf
[ mkBound <$> Seq
[ star (enclose (match ParenOpen) (match ParenClose) $
Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ])
- , match Colon
+ , WithBounds (match Colon)
, rename Id (Drop Id) OpenType
, match Equal
, Var (%%% "openTerm")]
@@ -514,7 +519,7 @@ LetTerm =
, Var (%%% "openTerm")
]
, mkLetType <$> Seq
- [ match TypeIdent
+ [ WithBounds (match TypeIdent)
, match Equal
, rename Id (Drop Id) OpenType
, match In
@@ -522,43 +527,46 @@ LetTerm =
]
]
where
- mkLet : HList [String, TermFun, (), TermFun] -> TermFun
- mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let !(e.try tyCtx tmCtx) (x ** !(t.try tyCtx (tmCtx :< x))))
+ mkLet : HList [WithBounds String, TermFun, (), TermFun] -> TermFun
+ mkLet [x, e, _, t] =
+ MkParseFun (\tyCtx, tmCtx =>
+ pure $ Let x.bounds !(e.try tyCtx tmCtx) (x.val ** !(t.try tyCtx (tmCtx :< x.val))))
- mkLetType : HList [String, (), TypeFun, (), TermFun] -> TermFun
+ mkLetType : HList [WithBounds String, (), TypeFun, (), TermFun] -> TermFun
mkLetType [x, _, a, _, t] =
- MkParseFun (\tyCtx, tmCtx => pure $ LetTy !(a.try tyCtx) (x ** !(t.try (tyCtx :< x) tmCtx)))
+ MkParseFun (\tyCtx, tmCtx =>
+ pure $ LetTy x.bounds !(a.try tyCtx) (x.val ** !(t.try (tyCtx :< x.val) tmCtx)))
mkArrow : List TypeFun -> TypeFun -> TypeFun
mkArrow [] cod = cod
mkArrow (arg :: args) cod =
MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
- mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), TermFun] -> TermFun
- mkBound [[], _, cod, _, t] =
+ mkBound : HList [List (HList [String, (), TypeFun]), WithBounds (), TypeFun, (), TermFun] -> TermFun
+ mkBound [[], m, cod, _, t] =
MkParseFun (\tyCtx, tmCtx =>
pure $
- Annot !(t.try tyCtx tmCtx) !(cod.try tyCtx))
- mkBound [args, _, cod, _, t] =
+ Annot m.bounds !(t.try tyCtx tmCtx) !(cod.try tyCtx))
+ mkBound [args, m, cod, _, t] =
let bound = map (\[x, _, a] => x) args in
let tys = map (\[x, _, a] => a) args in
MkParseFun (\tyCtx, tmCtx =>
pure $
- Annot (Abs (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx))
+ Annot m.bounds (Abs m.bounds (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx))
AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AbsTerm =
mkAbs <$> Seq
- [ match Backslash
+ [ WithBounds (match Backslash)
, sepBy1 (match Comma) (match TermIdent)
, match DoubleArrow
, Var (%%% "openTerm")
]
where
- mkAbs : HList [(), List1 String, (), TermFun] -> TermFun
- mkAbs [_, args, _, body] =
+ mkAbs : HList [WithBounds (), List1 String, (), TermFun] -> TermFun
+ mkAbs [m, args, _, body] =
MkParseFun (\tyCtx, tmCtx =>
- pure $ Abs (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
+ pure $ Abs m.bounds (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
CaseTerm =
@@ -566,12 +574,12 @@ CaseTerm =
Seq
[ OneOf
[ mkCase <$> Seq
- [ match Case
+ [ WithBounds (match Case)
, Var (%%% "openTerm")
, match Of
]
, mkFoldCase <$> Seq
- [ match FoldCase
+ [ WithBounds (match FoldCase)
, Var (%%% "openTerm")
, match By
]
@@ -592,29 +600,30 @@ CaseTerm =
mkBranch :
HList [String, String, (), TermFun] ->
- Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term tyCtx (tmCtx :< x)))
+ Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Bounds tyCtx (tmCtx :< x)))
mkBranch [tag, bound, _, branch] =
tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
- mkCase : HList [_, TermFun, _] -> Cases -> TermFun
- mkCase [_, target, _] branches =
+ mkCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
+ mkCase [m, target, _] branches =
let branches = map (map mkBranch) branches in
MkParseFun (\tyCtx, tmCtx =>
- [| Case (target.try tyCtx tmCtx) (tryRow2 branches tyCtx tmCtx) |])
+ pure $ Case m.bounds !(target.try tyCtx tmCtx) !(tryRow2 branches tyCtx tmCtx))
- mkFoldCase : HList [_, TermFun, _] -> Cases -> TermFun
- mkFoldCase [_, target, _] branches =
+ mkFoldCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
+ mkFoldCase [m, target, _] branches =
let branches = map (map mkBranch) branches in
MkParseFun (\tyCtx, tmCtx =>
pure $
Fold
+ m.bounds
!(target.try tyCtx tmCtx)
- ("__tmp" ** Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
+ ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
FoldTerm =
mkFold <$> Seq
- [ match Fold
+ [ WithBounds (match Fold)
, Var (%%% "openTerm")
, match By
, enclose (match ParenOpen) (match ParenClose) $
@@ -626,10 +635,10 @@ FoldTerm =
]
]
where
- mkFold : HList [(), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
- mkFold [_, target, _, [_, arg, _, body]] =
+ mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
+ mkFold [m, target, _, [_, arg, _, body]] =
MkParseFun (\tyCtx, tmCtx =>
- pure $ Fold !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
+ pure $ Fold m.bounds !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
export
OpenTerm : InkyParser False [<] [<] TermFun
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 91a42b8..79e8f6c 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -1,11 +1,15 @@
module Inky.Term.Pretty
+import Data.List.Quantifiers
import Data.Singleton
import Data.String
+import Data.These
import Inky.Decidable.Maybe
import Inky.Term
import Inky.Type.Pretty
+
+import Text.Bounded
import Text.PrettyPrint.Prettyprinter
public export
@@ -43,12 +47,12 @@ Ord TermPrec where
compare Open d2 = GT
export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
+prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
+prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
+prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
prettyLet : Doc ann -> Doc ann -> Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
+lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term m tyCtx tmCtx -> TermPrec -> Doc ann
prettyTerm t d =
case isLit t <|> isCheckLit t of
@@ -65,7 +69,7 @@ prettyTermCtx [<] d = [<]
prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
prettyCases [<] = [<]
-prettyCases (ts :< (l :- (x ** Abs (bound ** t)))) =
+prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) =
prettyCases ts :<
(group $ align $
pretty l <++> pretty x <++> "=>" <++>
@@ -84,26 +88,26 @@ prettyLet binding term =
"in") <+> line <+>
term
-lessPrettyTerm (Annot t a) d =
+lessPrettyTerm (Annot _ t a) d =
group $ align $ hang 2 $ parenthesise (d < Annot) $
prettyTerm t App <++> ":" <+> line <+> prettyType a Open
-lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
-lessPrettyTerm (Let e (x ** t)) d =
+lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+lessPrettyTerm (Let _ e (x ** t)) d =
-- TODO: pretty print annotated abstraction
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyTerm e Open)
(prettyTerm t Open)
-lessPrettyTerm (LetTy a (x ** t)) d =
+lessPrettyTerm (LetTy _ a (x ** t)) d =
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyType a Open)
(prettyTerm t Open)
-lessPrettyTerm (Abs (bound ** t)) d =
+lessPrettyTerm (Abs _ (bound ** t)) d =
group $ hang 2 $ parenthesise (d < Open) $
"\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open
-lessPrettyTerm (App (Map (x ** a) b c) ts) d =
+lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "map"
@@ -111,29 +115,29 @@ lessPrettyTerm (App (Map (x ** a) b c) ts) d =
:: prettyType b Atom
:: prettyType c Atom
:: prettyAllTerm ts Suffix)
-lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
+lessPrettyTerm (App _ (GetChildren _ (x ** a) b) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "getChildren"
:: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
:: prettyType b Atom
:: prettyAllTerm ts Suffix)
-lessPrettyTerm (App f ts) d =
+lessPrettyTerm (App _ f ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
-lessPrettyTerm (Tup (MkRow ts _)) d =
+lessPrettyTerm (Tup _ (MkRow ts _)) d =
let parts = prettyTermCtx ts Open <>> [] in
group $ align $ enclose "<" ">" $
flatAlt
(neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
(concatWith (surround $ "," <++> neutral) parts)
-lessPrettyTerm (Prj e l) d =
+lessPrettyTerm (Prj _ e l) d =
group $ align $ hang 2 $ parenthesise (d < Suffix) $
prettyTerm e Suffix <+> line' <+> "." <+> pretty l
-lessPrettyTerm (Inj l t) d =
+lessPrettyTerm (Inj _ l t) d =
group $ align $ hang 2 $ parenthesise (d < App) $
pretty l <+> line <+> prettyTerm t Suffix
-lessPrettyTerm (Case e (MkRow ts _)) d =
+lessPrettyTerm (Case _ e (MkRow ts _)) d =
let parts = prettyCases ts <>> [] in
group $ align $ hang 2 $ parenthesise (d < Open) $
(group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
@@ -141,19 +145,19 @@ lessPrettyTerm (Case e (MkRow ts _)) d =
flatAlt
(neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
(concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Roll t) d =
+lessPrettyTerm (Roll _ t) d =
pretty "~" <+>
parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
-lessPrettyTerm (Unroll e) d =
+lessPrettyTerm (Unroll _ e) d =
pretty "!" <+>
parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
-lessPrettyTerm (Fold e (x ** t)) d =
+lessPrettyTerm (Fold _ e (x ** t)) d =
-- TODO: foldcase
group $ align $ hang 2 $ parenthesise (d < Open) $
"fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
(group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
-lessPrettyTerm (Map (x ** a) b c) d =
+lessPrettyTerm (Map _ (x ** a) b c) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "map"
@@ -161,10 +165,220 @@ lessPrettyTerm (Map (x ** a) b c) d =
, prettyType b Atom
, prettyType c Atom
]
-lessPrettyTerm (GetChildren (x ** a) b) d =
+lessPrettyTerm (GetChildren _ (x ** a) b) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "getChildren"
, group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
, prettyType b Atom
]
+
+-- Typing Errors ---------------------------------------------------------------
+
+Pretty (ChecksOnly t) where
+ pretty Abs = "abstraction"
+ pretty Inj = "injection"
+ pretty Case = "case split"
+ pretty Roll = "rolling"
+ pretty Fold = "fold"
+
+prettyNotSynths :
+ {tyCtx, tmCtx : SnocList String} ->
+ {e : Term m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotSynths tyEnv tmEnv e ->
+ List (m, Doc ann)
+export
+prettyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {t : Term m tyCtx tmCtx} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotChecks tyEnv tmEnv a t ->
+ List (m, Doc ann)
+prettyNotCheckSpine :
+ {tyCtx, tmCtx : SnocList String} ->
+ {a : Ty [<]} ->
+ {ts : List (Term m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ NotCheckSpine tyEnv tmEnv a ts ->
+ List (m, Doc ann)
+prettyAnyNotSynths :
+ {tyCtx, tmCtx : SnocList String} ->
+ {es : Context (Term m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} ->
+ AnyNotSynths tyEnv tmEnv es ->
+ List (m, Doc ann)
+prettyAnyNotChecks :
+ {tyCtx, tmCtx : SnocList String} ->
+ {ts : Context (Term m tyCtx tmCtx)} ->
+ {tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
+ (meta : m) ->
+ AnyNotChecks tyEnv tmEnv as ts ->
+ List (m, Doc ann)
+prettyAnyNotBranches :
+ {tyCtx, tmCtx : SnocList String} ->
+ {ts : Context (x ** Term m tyCtx (tmCtx :< x))} ->
+ {tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
+ (meta : m) ->
+ AnyNotBranches tyEnv tmEnv as a ts ->
+ List (m, Doc ann)
+
+prettyNotSynths (ChecksNS shape) =
+ [(e.meta, pretty "cannot synthesise type of" <++> pretty shape)]
+prettyNotSynths (AnnotNS {a} (This contra)) =
+ [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (AnnotNS (That contra)) = prettyNotChecks contra
+prettyNotSynths (AnnotNS {a} (Both contra1 contra2)) =
+ (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+ prettyNotChecks contra2
+prettyNotSynths (LetNS1 contra) = prettyNotSynths contra
+prettyNotSynths (LetNS2 prf contra) =
+ case synthsRecompute prf of
+ Val a => prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (This contra)) =
+ [(e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotSynths (LetTyNS (That contra)) = prettyNotSynths contra
+prettyNotSynths (LetTyNS {a} (Both contra1 contra2)) =
+ (e.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)
+ :: prettyNotSynths contra2
+prettyNotSynths (AppNS1 contra) = prettyNotSynths contra
+prettyNotSynths (AppNS2 prf contras) =
+ case synthsRecompute prf of
+ Val a => prettyNotCheckSpine contras
+prettyNotSynths (TupNS contras) = prettyAnyNotSynths contras
+prettyNotSynths (PrjNS1 contra) = prettyNotSynths contra
+prettyNotSynths (PrjNS2 prf f) =
+ case synthsRecompute prf of
+ Val a =>
+ [(e.meta
+ , pretty "cannot project non-product type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotSynths (PrjNS3 {l, as} prf contra) =
+ case synthsRecompute prf of
+ Val (TProd as) =>
+ [(e.meta
+ , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+ pretty "in product type" <+> line <+>
+ prettyType (TProd as) Open
+ )]
+prettyNotSynths (UnrollNS1 contra) = prettyNotSynths contra
+prettyNotSynths (UnrollNS2 prf contra) =
+ case synthsRecompute prf of
+ Val a =>
+ [(e.meta
+ , pretty "cannot unroll non-inductive type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotSynths (MapNS {a} {b} {c} contras) =
+ bifoldMap
+ (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
+ (bifoldMap
+ (const [(e.meta, pretty "ill-formed source" <+> line <+> prettyType b Open)])
+ (const [(e.meta, pretty "ill-formed target" <+> line <+> prettyType c Open)]))
+ contras
+prettyNotSynths (GetChildrenNS {a} {b} contras) =
+ bifoldMap
+ (const [(e.meta, pretty "ill-formed functor" <+> line <+> prettyType a Open)])
+ (const [(e.meta, pretty "ill-formed contents" <+> line <+> prettyType b Open)])
+ contras
+
+prettyNotChecks (EmbedNC1 _ contra) = prettyNotSynths contra
+prettyNotChecks (EmbedNC2 _ prf contra) =
+ case synthsRecompute prf of
+ Val b =>
+ [(t.meta
+ , pretty "cannot unify" <+> line <+>
+ prettyType a Open <+> line <+>
+ pretty "and" <+> line <+>
+ prettyType b Open
+ )]
+prettyNotChecks (LetNC1 contra) = prettyNotSynths contra
+prettyNotChecks (LetNC2 prf contra) =
+ case synthsRecompute prf of
+ Val _ => prettyNotChecks contra
+prettyNotChecks (LetTyNC {a} (This contra)) =
+ [(t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open)]
+prettyNotChecks (LetTyNC (That contra)) = prettyNotChecks contra
+prettyNotChecks (LetTyNC (Both contra1 contra2)) =
+ (t.meta, pretty "ill-formed type" <+> line <+> prettyType a Open) ::
+ prettyNotChecks contra2
+prettyNotChecks (AbsNC1 contra) =
+ [(t.meta, pretty "cannot abstract to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (AbsNC2 prf contra) =
+ case isFunctionRecompute prf of
+ (Val _, Val _) => prettyNotChecks contra
+prettyNotChecks (TupNC1 contra) =
+ [(t.meta, pretty "cannot tuple to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (TupNC2 contras) = prettyAnyNotChecks t.meta contras
+prettyNotChecks (InjNC1 contra) =
+ [(t.meta, pretty "cannot inject to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (InjNC2 {l} contra) =
+ [(t.meta
+ , pretty "unknown label" <++> enclose "'" "'" (pretty l) <+> line <+>
+ pretty "in sum type" <+> line <+>
+ prettyType a Open
+ )]
+prettyNotChecks (InjNC3 i contra) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyNotChecks (CaseNC1 contra) = prettyNotSynths contra
+prettyNotChecks (CaseNC2 prf contra) =
+ case synthsRecompute prf of
+ Val a => [(t.meta, pretty "cannot case split on type" <+> line <+> prettyType a Open)]
+prettyNotChecks (CaseNC3 prf contras) =
+ case synthsRecompute prf of
+ Val _ => prettyAnyNotBranches t.meta contras
+prettyNotChecks (RollNC1 contra) =
+ [(t.meta, pretty "cannot roll to construct type" <+> line <+> prettyType a Open)]
+prettyNotChecks (RollNC2 contra) = prettyNotChecks contra
+prettyNotChecks (FoldNC1 contra) = prettyNotSynths contra
+prettyNotChecks (FoldNC2 prf contra) =
+ case synthsRecompute prf of
+ Val a => [(t.meta, pretty "cannot fold over type" <+> line <+> prettyType a Open)]
+prettyNotChecks (FoldNC3 prf contra) =
+ case synthsRecompute prf of
+ Val _ => prettyNotChecks contra
+
+prettyNotCheckSpine (Step1 {t} contra) =
+ [(t.meta, pretty "cannot apply non-function type" <+> line <+> prettyType a Open)]
+prettyNotCheckSpine (Step2 (This contra)) = prettyNotChecks contra
+prettyNotCheckSpine (Step2 (That contra)) = prettyNotCheckSpine contra
+prettyNotCheckSpine (Step2 (Both contra1 contra2)) =
+ prettyNotChecks contra1 ++ prettyNotCheckSpine contra2
+
+prettyAnyNotSynths (Step (This contra)) = prettyNotSynths contra
+prettyAnyNotSynths (Step (That contra)) = prettyAnyNotSynths contra
+prettyAnyNotSynths (Step (Both contra1 contra2)) =
+ prettyNotSynths contra1 ++ prettyAnyNotSynths contra2
+
+prettyAnyNotChecks meta Base1 =
+ [(meta
+ , pretty "missing components" <+> line <+>
+ concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+ )]
+prettyAnyNotChecks meta (Step1 {t, l} contra) =
+ [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotChecks meta (Step2 i (This contra)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyAnyNotChecks meta (Step2 i (That contra)) = prettyAnyNotChecks meta contra
+prettyAnyNotChecks meta (Step2 i (Both contra1 contra2)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra1 ++ prettyAnyNotChecks meta contra2
+
+prettyAnyNotBranches meta Base1 =
+ [(meta
+ , pretty "missing cases" <+> line <+>
+ concatWith (surround $ "," <++> neutral) (map pretty as.names <>> [])
+ )]
+prettyAnyNotBranches meta (Step1 {t, l} contra) =
+ [(t.meta , pretty "unknown label" <++> enclose "'" "'" (pretty l))]
+prettyAnyNotBranches meta (Step2 i (This contra)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra
+prettyAnyNotBranches meta (Step2 i (That contra)) = prettyAnyNotBranches meta contra
+prettyAnyNotBranches meta (Step2 i (Both contra1 contra2)) =
+ case [| (nameOf i).value |] of
+ Val _ => prettyNotChecks contra1 ++ prettyAnyNotBranches meta contra2
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 14:06:02 +0000