diff options
Diffstat (limited to 'src/Inky/Term.idr')
| -rw-r--r-- | src/Inky/Term.idr | 668 |
1 files changed, 93 insertions, 575 deletions
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 1fb50ea..8ae1223 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -3,7 +3,6 @@ module Inky.Term import public Inky.Data.Thinned import public Inky.Type -import Control.Function import Data.List.Quantifiers import Data.Singleton import Data.These @@ -18,27 +17,29 @@ import Inky.Decidable.Maybe -------------------------------------------------------------------------------- public export -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 +data Mode = Sugar | NoSugar + +public export +data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where + Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty tyCtx -> Term mode m tyCtx tmCtx + Var : (meta : m) -> Var tmCtx -> Term mode m tyCtx tmCtx + Let : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx + LetTy : (meta : m) -> Ty tyCtx -> (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx + Abs : (meta : m) -> (bound ** Term mode m tyCtx (tmCtx <>< bound)) -> Term mode m tyCtx tmCtx + App : (meta : m) -> Term mode m tyCtx tmCtx -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx + Tup : (meta : m) -> Row (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx + Prj : (meta : m) -> Term mode m tyCtx tmCtx -> (l : String) -> Term mode m tyCtx tmCtx + Inj : (meta : m) -> (l : String) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx + Case : (meta : m) -> Term mode m tyCtx tmCtx -> Row (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx + Roll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx + Unroll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx + Fold : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx + Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term Sugar m tyCtx tmCtx %name Term e, f, t, u export -(.meta) : Term m tyCtx tmCtx -> m +(.meta) : Term mode m tyCtx tmCtx -> m (Annot meta _ _).meta = meta (Var meta _).meta = meta (Let meta _ _).meta = meta @@ -53,7 +54,6 @@ export (Unroll meta _).meta = meta (Fold meta _ _).meta = meta (Map meta _ _ _).meta = meta -(GetChildren meta _ _).meta = meta -------------------------------------------------------------------------------- -- Well Formed ----------------------------------------------------------------- @@ -128,40 +128,42 @@ isFunction (x :: bound) a = namespace Modes public export - 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) + data SynthsOnly : Term mode m tyCtx tmCtx -> Type where + Annot : SynthsOnly (Annot meta t a) + Var : SynthsOnly (Var meta i) + App : SynthsOnly (App meta f ts) + Prj : SynthsOnly (Prj meta e l) + Unroll : SynthsOnly (Unroll meta e) + Map : SynthsOnly (Map meta (x ** a) b c) public export - 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)) + data ChecksOnly : Term mode m tyCtx tmCtx -> Type where + Abs : ChecksOnly (Abs meta (bounds ** t)) + Inj : ChecksOnly (Inj meta l t) + Case : ChecksOnly (Case meta e ts) + Roll : ChecksOnly (Roll meta t) + Fold : ChecksOnly (Fold meta e (x ** t)) + + %name SynthsOnly shape + %name ChecksOnly shape public export data Synths : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Term m tyCtx tmCtx -> Ty [<] -> Type + Term mode m tyCtx tmCtx -> Ty [<] -> Type public export data Checks : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Ty [<] -> Term m tyCtx tmCtx -> Type + Ty [<] -> Term mode m tyCtx tmCtx -> Type namespace Spine public export data CheckSpine : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Ty [<] -> List (Term m tyCtx tmCtx) -> Ty [<] -> Type + Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type where Nil : CheckSpine tyEnv tmEnv a [] a (::) : @@ -176,13 +178,14 @@ namespace Synths data AllSynths : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - (ts : Context (Term m tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type + Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type where Lin : AllSynths tyEnv tmEnv [<] [<] (:<) : AllSynths tyEnv tmEnv ts as -> + {auto 0 freshIn : l `FreshIn` as.names} -> Synths tyEnv tmEnv t a -> - AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< a) + AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< (l :- a)) %name AllSynths prfs @@ -191,7 +194,7 @@ namespace Checks data AllChecks : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type + Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type where Base : AllChecks tyEnv tmEnv [<] [<] Step : @@ -207,7 +210,7 @@ namespace Branches data AllBranches : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type + Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type where Base : AllBranches tyEnv tmEnv [<] a [<] Step : @@ -239,7 +242,7 @@ data Synths where Synths tyEnv tmEnv (App meta f ts) b TupS : AllSynths tyEnv tmEnv es.context as -> - Synths tyEnv tmEnv (Tup meta es) (TProd (fromAll es as)) + Synths tyEnv tmEnv (Tup meta es) (TProd as) PrjS : Synths tyEnv tmEnv e (TProd as) -> Elem (l :- a) as.context -> @@ -255,21 +258,16 @@ data Synths where (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 : - WellFormed (TFix x a) -> - WellFormed b -> - Synths tyEnv tmEnv (GetChildren meta (x ** a) b) - (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a) - (TProd - [<"Children" :- sub tyEnv b - , "Shape" :- sub (tyEnv :< (TNat `Over` Id)) a])) data Checks where - EmbedC : - SynthsOnly e -> - Synths tyEnv tmEnv e a -> + AnnotC : + Synths tyEnv tmEnv (Annot meta t a) b -> + Alpha b c -> + Checks tyEnv tmEnv c (Annot meta t a) + VarC : + Synths tyEnv tmEnv (Var {mode} meta i) a -> Alpha a b -> - Checks tyEnv tmEnv b e + Checks tyEnv tmEnv b (Var {mode} meta i) LetC : Synths tyEnv tmEnv e a -> Checks tyEnv (tmEnv :< (a `Over` Id)) b t -> @@ -282,9 +280,17 @@ data Checks where IsFunction bound a dom cod -> Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t -> Checks tyEnv tmEnv a (Abs meta (bound ** t)) + AppC : + Synths tyEnv tmEnv (App meta e ts) a -> + Alpha a b -> + Checks tyEnv tmEnv b (App meta e ts) TupC : AllChecks tyEnv tmEnv as.context ts.context -> Checks tyEnv tmEnv (TProd as) (Tup meta ts) + PrjC : + Synths tyEnv tmEnv (Prj meta e l) a -> + Alpha a b -> + Checks tyEnv tmEnv b (Prj meta e l) InjC : Elem (l :- a) as.context -> Checks tyEnv tmEnv a t -> @@ -296,10 +302,32 @@ data Checks where RollC : Checks tyEnv tmEnv (sub [<TFix x a `Over` Id] a) t -> Checks tyEnv tmEnv (TFix x a) (Roll meta t) + UnrollC : + Synths tyEnv tmEnv (Unroll meta e) a -> + Alpha a b -> + Checks tyEnv tmEnv b (Unroll meta e) 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 meta e (y ** t)) + MapC : + Synths tyEnv tmEnv (Map meta (x ** a) b c) d -> + Alpha d e -> + Checks tyEnv tmEnv e (Map meta (x ** a) b c) + +public export +%inline +EmbedC : + SynthsOnly e -> + Synths tyEnv tmEnv e a -> + Alpha a b -> + Checks tyEnv tmEnv b e +EmbedC Annot prf1 prf2 = AnnotC prf1 prf2 +EmbedC Var prf1 prf2 = VarC prf1 prf2 +EmbedC App prf1 prf2 = AppC prf1 prf2 +EmbedC Prj prf1 prf2 = PrjC prf1 prf2 +EmbedC Unroll prf1 prf2 = UnrollC prf1 prf2 +EmbedC Map prf1 prf2 = MapC prf1 prf2 %name Synths prf %name Checks prf @@ -308,19 +336,19 @@ public export data NotSynths : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Term m tyCtx tmCtx -> Type + Term mode m tyCtx tmCtx -> Type public export data NotChecks : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Ty [<] -> Term m tyCtx tmCtx -> Type + Ty [<] -> Term mode m tyCtx tmCtx -> Type namespace Spine public export data NotCheckSpine : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Ty [<] -> List (Term m tyCtx tmCtx) -> Type + Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type where Step1 : ((b, c : Ty [<]) -> Not (a = TArrow b c)) -> @@ -336,7 +364,7 @@ namespace Synths data AnyNotSynths : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - (ts : Context (Term m tyCtx tmCtx)) -> Type + (ts : Context (Term mode m tyCtx tmCtx)) -> Type where Step : These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) -> @@ -349,7 +377,7 @@ namespace Checks data AnyNotChecks : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Context (Ty [<]) -> Context (Term m tyCtx tmCtx) -> Type + Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type where Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<] Step1 : @@ -367,7 +395,7 @@ namespace Branches data AnyNotBranches : All (const $ Thinned Ty [<]) tyCtx -> All (const $ Thinned Ty [<]) tmCtx -> - Context (Ty [<]) -> Ty [<] -> Context (x ** Term m tyCtx (tmCtx :< x)) -> Type + Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type where Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<] Step1 : @@ -430,9 +458,6 @@ data NotSynths where MapNS : These (IllFormed (TFix x a)) (These (IllFormed b) (IllFormed c)) -> NotSynths tyEnv tmEnv (Map meta (x ** a) b c) - GetChildrenNS : - These (IllFormed (TFix x a)) (IllFormed b) -> - NotSynths tyEnv tmEnv (GetChildren meta (x ** a) b) data NotChecks where EmbedNC1 : @@ -516,538 +541,31 @@ Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where 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 -checkSpineUnique : CheckSpine tyEnv tmEnv a ts b -> CheckSpine tyEnv tmEnv a ts c -> b = c -allSynthsUnique : AllSynths tyEnv tmEnv es as -> AllSynths tyEnv tmEnv es bs -> as = bs - -synthsUnique (AnnotS _ _) (AnnotS _ _) = Refl -synthsUnique VarS VarS = Refl -synthsUnique (LetS prf1 prf2) (LetS prf1' prf2') = - let prf2' = rewrite synthsUnique prf1 prf1' in prf2' in - synthsUnique prf2 prf2' -synthsUnique (LetTyS _ prf) (LetTyS _ prf') = synthsUnique prf prf' -synthsUnique (AppS prf prfs) (AppS prf' prfs') = - let prfs' = rewrite synthsUnique prf prf' in prfs' in - checkSpineUnique prfs prfs' -synthsUnique (TupS {es} prfs) (TupS prfs') = - cong (TProd . fromAll es) $ allSynthsUnique prfs prfs' -synthsUnique (PrjS {as} prf i) (PrjS {as = bs} prf' j) = - let j = rewrite inj TProd $ synthsUnique prf prf' in j in - cong fst $ lookupUnique as i j -synthsUnique (UnrollS {x, a} prf) (UnrollS {x = y, a = b} prf') = - cong (\(x ** a) => sub [<TFix x a `Over` Id] a) $ - fixInjective $ - synthsUnique prf prf' -synthsUnique (MapS _ _ _) (MapS _ _ _) = Refl -synthsUnique (GetChildrenS _ _) (GetChildrenS _ _) = Refl - -checkSpineUnique [] [] = Refl -checkSpineUnique (prf :: prfs) (prf' :: prfs') = checkSpineUnique prfs prfs' - -allSynthsUnique [<] [<] = Refl -allSynthsUnique (prfs :< prf) (prfs' :< prf') = - cong2 (:<) (allSynthsUnique prfs prfs') (synthsUnique prf prf') - --- We cannot both succeed and fail - -synthsSplit : Synths tyEnv tmEnv e a -> NotSynths tyEnv tmEnv e -> Void -checksSplit : Checks tyEnv tmEnv a t -> NotChecks tyEnv tmEnv a t -> Void -checkSpineSplit : CheckSpine tyEnv tmEnv a ts b -> NotCheckSpine tyEnv tmEnv a ts -> Void -allSynthsSplit : AllSynths tyEnv tmEnv es as -> AnyNotSynths tyEnv tmEnv es -> Void -allChecksSplit : - (0 fresh : AllFresh as.names) -> - AllChecks tyEnv tmEnv as ts -> AnyNotChecks tyEnv tmEnv as ts -> Void -allBranchesSplit : - (0 fresh : AllFresh as.names) -> - AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void - -synthsSplit (AnnotS wf prf) (AnnotNS contras) = - these (wellFormedSplit wf) (checksSplit prf) (const $ checksSplit prf) contras -synthsSplit VarS contra = absurd contra -synthsSplit (LetS prf1 prf2) (LetNS1 contra) = synthsSplit prf1 contra -synthsSplit (LetS prf1 prf2) (LetNS2 prf1' contra) = - let contra = rewrite synthsUnique prf1 prf1' in contra in - synthsSplit prf2 contra -synthsSplit (LetTyS wf prf) (LetTyNS contras) = - these (wellFormedSplit wf) (synthsSplit prf) (const $ synthsSplit prf) contras -synthsSplit (AppS prf prfs) (AppNS1 contra) = synthsSplit prf contra -synthsSplit (AppS prf prfs) (AppNS2 prf' contras) = - let contras = rewrite synthsUnique prf prf' in contras in - checkSpineSplit prfs contras -synthsSplit (TupS prfs) (TupNS contras) = allSynthsSplit prfs contras -synthsSplit (PrjS prf i) (PrjNS1 contra) = synthsSplit prf contra -synthsSplit (PrjS {as} prf i) (PrjNS2 prf' contra) = - void $ contra as $ synthsUnique prf' prf -synthsSplit (PrjS {as, a} prf i) (PrjNS3 {as = bs} prf' contra) = - let i = rewrite inj TProd $ synthsUnique prf' prf in i in - void $ contra a i -synthsSplit (UnrollS prf) (UnrollNS1 contra) = synthsSplit prf contra -synthsSplit (UnrollS {x, a} prf) (UnrollNS2 prf' contra) = - void $ contra x a $ synthsUnique prf' prf -synthsSplit (MapS wf1 wf2 wf3) (MapNS contras) = - these (wellFormedSplit wf1) - (these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3)) - (const $ these (wellFormedSplit wf2) (wellFormedSplit wf3) (const $ wellFormedSplit wf3)) - contras -synthsSplit (GetChildrenS wf1 wf2) (GetChildrenNS contras) = - these (wellFormedSplit wf1) (wellFormedSplit wf2) (const $ wellFormedSplit wf2) contras - -checksSplit (EmbedC _ prf1 prf2) (EmbedNC1 _ contra) = synthsSplit prf1 contra -checksSplit (EmbedC _ prf1 prf2) (EmbedNC2 _ prf1' contra) = - let contra = rewrite synthsUnique prf1 prf1' in contra in - alphaSplit prf2 contra -checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra -checksSplit (LetC prf1 prf2) (LetNC2 prf1' contra) = - let contra = rewrite synthsUnique prf1 prf1' in contra in - checksSplit prf2 contra -checksSplit (LetTyC wf prf) (LetTyNC contras) = - these (wellFormedSplit wf) (checksSplit prf) (const $ checksSplit prf) contras -checksSplit (AbsC prf1 prf2) (AbsNC1 contra) = isFunctionSplit prf1 contra -checksSplit (AbsC prf1 prf2) (AbsNC2 prf1' contra) = - let (eq1, eq2) = isFunctionUnique prf1 prf1' in - let contra = rewrite eq1 in rewrite eq2 in contra in - checksSplit prf2 contra -checksSplit (TupC {as} prfs) (TupNC1 contra) = void $ contra as Refl -checksSplit (TupC {as} prfs) (TupNC2 contras) = allChecksSplit as.fresh prfs contras -checksSplit (InjC {as} i prf) (InjNC1 contra) = void $ contra as Refl -checksSplit (InjC {a} i prf) (InjNC2 contra) = void $ contra a i -checksSplit (InjC {as} i prf) (InjNC3 j contra) = - let contra = rewrite cong fst $ lookupUnique as i j in contra in - checksSplit prf contra -checksSplit (CaseC prf prfs) (CaseNC1 contra) = synthsSplit prf contra -checksSplit (CaseC {as} prf prfs) (CaseNC2 prf' contra) = - void $ contra as $ synthsUnique prf' prf -checksSplit (CaseC {as} prf prfs) (CaseNC3 prf' contras) = - let contras = rewrite inj TSum $ synthsUnique prf prf' in contras in - allBranchesSplit as.fresh prfs contras -checksSplit (RollC {x, a} prf) (RollNC1 contra) = void $ contra x a Refl -checksSplit (RollC prf) (RollNC2 contra) = checksSplit prf contra -checksSplit (FoldC prf1 prf2) (FoldNC1 contra) = synthsSplit prf1 contra -checksSplit (FoldC {x, a} prf1 prf2) (FoldNC2 prf1' contra) = - void $ contra x a $ synthsUnique prf1' prf1 -checksSplit (FoldC {t, b} prf1 prf2) (FoldNC3 prf1' contra) = - let - contra = - replace - {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [<b `Over` Id] a `Over` Id)) b t} - (fixInjective $ synthsUnique prf1' prf1) - contra - in - checksSplit prf2 contra - -checkSpineSplit (prf :: prfs) (Step1 contra) = void $ contra _ _ Refl -checkSpineSplit (prf :: prfs) (Step2 contras) = - these (checksSplit prf) (checkSpineSplit prfs) (const $ checkSpineSplit prfs) contras - -allSynthsSplit (prfs :< prf) (Step contras) = - these (synthsSplit prf) (allSynthsSplit prfs) (const $ allSynthsSplit prfs) contras - -allChecksSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i -allChecksSplit fresh (Step {as, t, ts} i prf prfs) (Step2 j contras) = - let - contras = - replace - {p = \(a ** i) => These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts)} - (lookupUnique (MkRow as fresh) j i) - contras - 0 fresh = dropElemFresh as fresh i - in - these (checksSplit prf) (allChecksSplit fresh prfs) (const $ allChecksSplit fresh prfs) contras - -allBranchesSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i -allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) = - let - contras = - replace - {p = \(a ** i) => - These - (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t) - (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)} - (lookupUnique (MkRow as fresh) j i) - contras - 0 fresh = dropElemFresh as fresh i - in - these (checksSplit prf) (allBranchesSplit fresh prfs) (const $ allBranchesSplit fresh prfs) contras - --- Synthesis and Checking are decidable - -fallbackCheck : - SynthsOnly e -> - Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) -> - (a : Ty [<]) -> - LazyEither (Checks tyEnv tmEnv a e) (NotChecks tyEnv tmEnv a e) -fallbackCheck prf p a = - map - (\xPrf => uncurry (EmbedC prf) $ snd xPrf) - (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $ - (b := p) >=> alpha b a - -synths : - (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> - (tmEnv : All (const $ Thinned Ty [<]) 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 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 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 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 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 m tyCtx (tmCtx :< x))) -> - LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts) - -synths tyEnv tmEnv (Annot _ t a) = - pure (sub tyEnv a) $ - map (uncurry AnnotS) AnnotNS $ - all (wellFormed 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)) = - 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)) = - map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $ - all (wellFormed 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) = - 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)) = - map (TProd . fromAll (MkRow es fresh)) (\_ => TupS) TupNS $ - allSynths tyEnv tmEnv es -synths tyEnv tmEnv (Prj meta e l) = - map (snd . snd) true false $ - (a := synths tyEnv tmEnv e) >=> - (as := isProd a) >=> - decLookup l as.context - where - 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 meta e l) (snd $ snd x) - true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i - - false : - Either - (NotSynths tyEnv tmEnv e) - (a : Ty [<] ** (Synths tyEnv tmEnv e a, - 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 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) = - map f true false $ - synths tyEnv tmEnv e `andThen` isFix - where - f : (Ty [<], (x ** Ty [<x])) -> Ty [<] - f (a, (x ** b)) = sub [<TFix x b `Over` Id] b - - true : - (axb : _) -> - (Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) 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 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) = - pure _ $ - map (\(wf1, wf2, wf3) => MapS wf1 wf2 wf3) MapNS $ - all (wellFormed (TFix x a)) (all (wellFormed b) (wellFormed c)) -synths tyEnv tmEnv (GetChildren _ (x ** a) b) = - pure _ $ - map (uncurry GetChildrenS) GetChildrenNS $ - all (wellFormed (TFix x a)) (wellFormed b) - -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)) = - map (uncurry LetTyC) LetTyNC $ - all (wellFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t) -checks tyEnv tmEnv a (Abs meta (bound ** t)) = - map - (\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2) - (either AbsNC1 false) $ - (domCod := isFunction bound a) >=> - checks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst domCod)) (snd domCod) 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 meta (bound ** t)) - false ((_,_) ** prf) = uncurry AbsNC2 prf -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 meta (MkRow ts fresh')) - true (as ** (Refl, prf)) = TupC prf - - false : - forall a. - 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 meta (MkRow ts fresh')) - false (Left contra) = TupNC1 contra - false (Right (as ** (Refl, contra))) = TupNC2 contra -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) >=> - checks tyEnv tmEnv b t - where - true : - forall a. - (as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) -> - Checks tyEnv tmEnv a (Inj meta l t) - true (as ** (Refl, (b ** (i, prf)))) = InjC i prf - - false : - forall a. - Either - ((as : _) -> Not (a = TSum as)) - (as ** (a = TSum as, - Either - ((b : _) -> Not (Elem (l :- b) as.context)) - (b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b 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)) = - map true false $ - (b := synths tyEnv tmEnv e) >=> - (as := isSum b) >=> - allBranches tyEnv tmEnv as.context a ts - where - 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 meta e (MkRow ts fresh)) - true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs - - false : - forall fresh. - Either - (NotSynths tyEnv tmEnv e) - (b ** (Synths tyEnv tmEnv e b, - Either - ((as : _) -> Not (b = TSum as)) - (as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) -> - 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) = - map true false $ - (xb := isFix a) >=> checks tyEnv tmEnv (ty xb) t - where - ty : (x ** Ty [<x]) -> Ty [<] - ty (x ** b) = sub [<TFix x b `Over` Id] b - - true : - forall a. - (xb : (x ** Ty [<x]) ** (a = TFix (fst xb) (snd xb), Checks tyEnv tmEnv (ty xb) t)) -> - Checks tyEnv tmEnv a (Roll meta t) - true ((x ** b) ** (Refl, prf)) = RollC prf - - false : - forall a. - 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 meta t) - false (Left contra) = RollNC1 contra - false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra -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) >=> - checks tyEnv (tmEnv' yc) a t - where - tmEnv' : (y ** Ty [<y]) -> All (const $ Thinned Ty [<]) (tmCtx :< x) - tmEnv' (y ** c) = tmEnv :< (sub [<a `Over` Id] c `Over` Id) - - 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 meta e (x ** t)) - true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2 - - false : - Either - (NotSynths tyEnv tmEnv e) - (b ** (Synths tyEnv tmEnv e b, - 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 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 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) = - map snd true false $ - (bc := isArrow a) >=> - all (checks tyEnv tmEnv (fst bc) t) (checkSpine tyEnv tmEnv (snd bc) ts) - where - true : - forall a. - (bcd : ((Ty [<], Ty [<]), Ty [<])) -> - ( a = TArrow (fst $ fst bcd) (snd $ fst bcd) - , uncurry (\bc,d => (Checks tyEnv tmEnv (fst bc) t, CheckSpine tyEnv tmEnv (snd bc) ts d)) bcd) -> - CheckSpine tyEnv tmEnv a (t :: ts) (snd bcd) - true ((b, c), d) (Refl, (prf1, prf2)) = prf1 :: prf2 - - false : - forall a. - Either - ((b, c : Ty [<]) -> Not (a = TArrow b c)) - (bc : (Ty [<], Ty [<]) ** (a = TArrow (fst bc) (snd bc), - These - (NotChecks tyEnv tmEnv (fst bc) t) - (NotCheckSpine tyEnv tmEnv (snd bc) ts))) -> - NotCheckSpine tyEnv tmEnv a (t :: ts) - false (Left contra) = Step1 contra - false (Right ((b, c) ** (Refl, contras))) = Step2 contras - -allSynths tyEnv tmEnv [<] = Just [<] `Because` [<] -allSynths tyEnv tmEnv (es :< (l :- e)) = - map (uncurry (flip (:<))) (\(a, as), (prf, prfs) => prfs :< prf) Step $ - all (synths tyEnv tmEnv e) (allSynths tyEnv tmEnv es) - -allChecks tyEnv tmEnv [<] [<] = True `Because` Base -allChecks tyEnv tmEnv (as :< la) [<] = False `Because` Base1 -allChecks tyEnv tmEnv as (ts :< (l :- t)) = - map - (\((a ** i) ** (prf, prfs)) => Step i prf prfs) - (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $ - (ai := (decLookup l as).forget) >=> - all (checks tyEnv tmEnv (fst ai) t) (allChecks tyEnv tmEnv (dropElem as $ snd ai) ts) - -allBranches tyEnv tmEnv [<] b [<] = True `Because` Base -allBranches tyEnv tmEnv (as :< la) b [<] = False `Because` Base1 -allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) = - map - (\((a ** i) ** (prf, prfs)) => Step i prf prfs) - (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $ - (ai := (decLookup l as).forget) >=> - all - (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t) - (allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts) - -- Sugar ----------------------------------------------------------------------- public export -CheckLit : m -> Nat -> Term m tyCtx tmCtx +CheckLit : m -> Nat -> Term mode 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 : m -> Nat -> Term m tyCtx tmCtx +Lit : m -> Nat -> Term mode m tyCtx tmCtx Lit meta n = Annot meta (CheckLit meta n) TNat public export -Suc : m -> Term m tyCtx tmCtx +Suc : m -> Term mode m tyCtx tmCtx Suc meta = Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x")))) (TArrow TNat TNat) export -isCheckLit : Term m tyCtx tmCtx -> Maybe Nat +isCheckLit : Term mode 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 m tyCtx tmCtx -> Maybe Nat +isLit : Term mode m tyCtx tmCtx -> Maybe Nat isLit (Annot _ t a) = if (alpha {ctx2 = [<]} a TNat).does then isCheckLit t @@ -1055,7 +573,7 @@ isLit (Annot _ t a) = isLit _ = Nothing export -isSuc : Term m tyCtx tmCtx -> Bool +isSuc : Term mode 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 |