diff options
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 384 |
1 files changed, 224 insertions, 160 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 |