summaryrefslogtreecommitdiff
path: root/src/Inky/Term
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Term')
-rw-r--r--src/Inky/Term/Checks.idr43
-rw-r--r--src/Inky/Term/Compile.idr316
-rw-r--r--src/Inky/Term/Desugar.idr4
-rw-r--r--src/Inky/Term/Parser.idr15
-rw-r--r--src/Inky/Term/Pretty/Error.idr5
-rw-r--r--src/Inky/Term/Recompute.idr128
-rw-r--r--src/Inky/Term/Substitution.idr2
7 files changed, 462 insertions, 51 deletions
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 6027d68..8de671c 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -5,49 +5,14 @@ import Data.DPair
import Data.List.Quantifiers
import Data.Singleton
import Data.These
-import Inky.Data.SnocList.Quantifiers
-import Inky.Decidable
-import Inky.Decidable.Maybe
+import Flap.Data.SnocList.Quantifiers
+import Flap.Decidable
+import Flap.Decidable.Maybe
import Inky.Term
+import Inky.Term.Recompute
%hide Prelude.Ops.infixl.(>=>)
--- 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 : Row (Ty [<])} ->
- 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 _
-
-checkSpineRecompute [] = Val _
-checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
-
-allSynthsRecompute [<] = Val _
-allSynthsRecompute (prfs :< prf) with (allSynthsRecompute prfs) | (synthsRecompute prf)
- _ | Val _ | Val _ = Val _
-
-- Synthesis gives unique types
synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b
diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr
new file mode 100644
index 0000000..0867cd2
--- /dev/null
+++ b/src/Inky/Term/Compile.idr
@@ -0,0 +1,316 @@
+module Inky.Term.Compile
+
+-- For DAll
+import public Inky.Type.Substitution
+
+import Data.Maybe
+import Data.List.Quantifiers
+import Data.Singleton
+import Flap.Decidable
+import Flap.Decidable.Maybe
+import Inky.Term
+import Inky.Term.Recompute
+import Text.PrettyPrint.Prettyprinter
+
+-- Utilities -------------------------------------------------------------------
+
+mkLet : (bind, val, body: Doc ann) -> Doc ann
+mkLet bind val body =
+ parens $ align $ hang 1 $
+ "let" <++> parens (group $ parens $ align $ bind <++> group val) <++>
+ group body
+
+mkAbs : (bind, body: Doc ann) -> Doc ann
+mkAbs bind body =
+ parens $ align $ hang 1 $
+ "lambda" <++> parens bind <++>
+ group body
+
+mkTup : Context (Doc ann) -> Doc ann
+mkTup parts =
+ let
+ f = \lx =>
+ group $ parens $ align $ hang 2 $
+ pretty lx.name <++> "." <++> "," <+> group lx.value
+ in
+ "`" <+> group (parens $ align $ concatWith (<++>) $ map f parts <>> [])
+
+mkPrj : Doc ann -> String -> Doc ann
+mkPrj x l =
+ parens $ align $
+ pretty "assq-ref" <++>
+ group x <++>
+ pretty "'" <+> pretty l
+
+mkInj : String -> Doc ann -> Doc ann
+mkInj l x =
+ parens $ align $
+ "cons" <++>
+ "'" <+> pretty l <++>
+ group x
+
+mkCase : Doc ann -> Context (Doc ann, Doc ann) -> Doc ann
+mkCase target branches =
+ let
+ f = \lxy =>
+ group $ parens $ align $
+ parens ("'" <+> pretty lxy.name <++> "." <++> fst lxy.value) <++>
+ group (snd lxy.value)
+ in
+ parens $ align $ hang 2 $
+ "match" <++>
+ group target <++>
+ concatWith (<++>) (map f branches <>> [])
+
+-- Create a "unique" name from a type ------------------------------------------
+
+hashType : Ty tyCtx -> String
+hashTypes : Context (Ty tyCtx) -> List String
+
+hashType (TVar i) = "V" ++ show i
+hashType (TArrow a b) = concat ["A", hashType a, hashType b]
+hashType (TProd (MkRow as _)) = concat ("P" :: hashTypes as)
+hashType (TSum (MkRow as _)) = concat ("S" :: hashTypes as)
+hashType (TFix x a) = concat ["F", hashType a]
+
+hashTypes [<] = ["N"]
+hashTypes (as :< (l :- a)) = ["L", l, hashType a] ++ hashTypes as
+
+-- Compile map and fold --------------------------------------------------------
+
+compileMap :
+ {a : Ty tyCtx} ->
+ (0 wf : WellFormed a) -> (i : Var tyCtx) ->
+ (0 prf : i `StrictlyPositiveIn` a) ->
+ (f, t : Doc ann) -> Doc ann
+eagerCompileMap :
+ {a : Ty tyCtx} ->
+ (0 wf : WellFormed a) -> (i : Var tyCtx) ->
+ (0 prf : i `StrictlyPositiveIn` a) ->
+ (f, t : Doc ann) -> Doc ann
+compileMapTuple :
+ {as : Context (Ty tyCtx)} ->
+ (0 wf : AllWellFormed as) -> (i : Var tyCtx) ->
+ (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (f, t : Doc ann) -> All (Assoc0 $ Doc ann) as.names
+compileMapCase :
+ {as : Context (Ty tyCtx)} ->
+ (0 wf : AllWellFormed as) -> (i : Var tyCtx) ->
+ (0 prfs : i `StrictlyPositiveInAll` as) ->
+ (fun : Doc ann) -> All (Assoc0 $ (Doc ann, Doc ann)) as.names
+
+compileFold :
+ {a : Ty (tyCtx :< x)} ->
+ (0 wf : WellFormed a) ->
+ (0 prf : %% x `StrictlyPositiveIn` a) ->
+ (target, bind, body : Doc ann) -> Doc ann
+
+compileMap wf i prf f t =
+ if isJust (does $ strengthen i a)
+ then t
+ else eagerCompileMap wf i prf f t
+
+eagerCompileMap (TVar {i = j}) i TVar f t with (i `decEq` j)
+ _ | True `Because` _ = parens (f <++> t)
+ _ | False `Because` _ = t
+eagerCompileMap (TArrow _ _) i (TArrow prf) f t = t
+eagerCompileMap (TProd wfs) i (TProd prfs) f t =
+ mkTup $ fromAll $ compileMapTuple wfs i prfs f t
+eagerCompileMap (TSum wfs) i (TSum prfs) f t =
+ mkCase t $ fromAll $ compileMapCase wfs i prfs f
+eagerCompileMap (TFix sp wf) i (TFix prf) f t =
+ compileFold wf sp t (pretty "_eta") $
+ eagerCompileMap wf (ThereVar i) prf f (pretty "_eta")
+
+compileMapTuple [<] i [<] f t = [<]
+compileMapTuple ((:<) wfs {n} wf) i (prfs :< prf) f t =
+ compileMapTuple wfs i prfs f t :<
+ (n :- compileMap wf i prf f (mkPrj t n))
+
+compileMapCase [<] i [<] f = [<]
+compileMapCase ((:<) wfs {n} wf) i (prfs :< prf) f =
+ compileMapCase wfs i prfs f :<
+ (n :- (pretty "_eta", mkInj n (compileMap wf i prf f $ pretty "_eta")))
+
+compileFold {a} wf prf target bind body =
+ let name = pretty "fold-" <+> pretty (hashType a) in
+ let
+ fun = parens $ align $ hang 1 $
+ "define" <++> parens (name <++> name <+> "-arg") <++>
+ group (mkLet bind (compileMap wf (%% x) prf name (name <+> "-arg")) body)
+ in
+ parens $ align $ hang 1 $
+ "begin" <++>
+ group fun <++>
+ parens (name <++> target)
+
+-- Compile any term ------------------------------------------------------------
+
+export
+compileSynths :
+ {tmCtx : SnocList String} ->
+ {t : Term mode m tyCtx tmCtx} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ (0 _ : Synths tyEnv tmEnv t a) ->
+ Doc ann
+export
+compileChecks :
+ {tmCtx : SnocList String} ->
+ {t : Term mode m tyCtx tmCtx} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ {a : Ty [<]} ->
+ (0 wf : WellFormed a) ->
+ (0 _ : Checks tyEnv tmEnv a t) ->
+ Doc ann
+compileSpine :
+ {tmCtx : SnocList String} ->
+ {ts : List (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ {a : Ty [<]} ->
+ (0 wf : WellFormed a) ->
+ (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
+ (fun : Doc ann) ->
+ Doc ann
+compileAllSynths :
+ {tmCtx : SnocList String} ->
+ {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ (0 _ : AllSynths tyEnv tmEnv ts as) ->
+ All (Assoc0 $ Doc ann) ts.names
+compileAllChecks :
+ {tmCtx : SnocList String} ->
+ {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ {as : Context (Ty [<])} ->
+ (0 fresh : AllFresh as.names) ->
+ (0 wfs : AllWellFormed as) ->
+ (0 _ : AllChecks tyEnv tmEnv as ts) ->
+ All (Assoc0 $ Doc ann) ts.names
+compileAllBranches :
+ {tmCtx : SnocList String} ->
+ {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ (0 tyWf : DAll WellFormed tyEnv) ->
+ (0 tmWf : DAll WellFormed tmEnv) ->
+ {as : Context (Ty [<])} ->
+ {a : Ty [<]} ->
+ (0 fresh : AllFresh as.names) ->
+ (0 wfs : AllWellFormed as) ->
+ (0 wf : WellFormed a) ->
+ (0 _ : AllBranches tyEnv tmEnv as a ts) ->
+ All (Assoc0 (Doc ann, Doc ann)) ts.names
+
+compileSynths tyWf tmWf (AnnotS wf prf) = compileChecks tyWf tmWf (subWf tyWf wf) prf
+compileSynths tyWf tmWf (VarS {i}) = pretty (unVal $ nameOf i.pos)
+compileSynths tyWf tmWf (LetS {x} prf1 prf2) =
+ case synthsRecompute prf1 of
+ Val _ =>
+ mkLet (pretty x)
+ (compileSynths tyWf tmWf prf1)
+ (compileSynths tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2)
+compileSynths tyWf tmWf (LetTyS {x} wf prf) =
+ compileSynths (tyWf :< (x :- subWf tyWf wf)) tmWf prf
+compileSynths tyWf tmWf (AppS prf prfs) =
+ case synthsRecompute prf of
+ Val _ => compileSpine tyWf tmWf (synthsWf tyWf tmWf prf) prfs (compileSynths tyWf tmWf prf)
+compileSynths tyWf tmWf (TupS prfs) = mkTup $ fromAll $ compileAllSynths tyWf tmWf prfs
+compileSynths tyWf tmWf (PrjS {l} prf i) = mkPrj (compileSynths tyWf tmWf prf) l
+compileSynths tyWf tmWf (UnrollS prf) = compileSynths tyWf tmWf prf
+compileSynths tyWf tmWf (MapS (TFix {x} sp wf1) wf2 wf3) =
+ mkAbs (pretty "_fun") $
+ mkAbs (pretty "_arg") $
+ compileMap wf1 (%% x) sp (pretty "_fun") (pretty "_arg")
+
+compileChecks tyWf tmWf wf (AnnotC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (VarC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (LetC {x} prf1 prf2) =
+ case synthsRecompute prf1 of
+ Val _ =>
+ mkLet (pretty x)
+ (compileSynths tyWf tmWf prf1)
+ (compileChecks tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) wf prf2)
+compileChecks tyWf tmWf wf (LetTyC wf' {x} prf) =
+ compileChecks (tyWf :< (x :- subWf tyWf wf')) tmWf wf prf
+compileChecks tyWf tmWf wf (AbsC {bound} prf1 prf2) =
+ case isFunctionRecompute prf1 of
+ (Val _, Val _) =>
+ let 0 wfs = isFunctionWf prf1 wf in
+ foldr
+ (mkAbs . pretty)
+ (compileChecks tyWf (tmWf <>< fst wfs) (snd wfs) prf2)
+ bound
+compileChecks tyWf tmWf wf (AppC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf (TProd {as = MkRow as fresh} wfs) (TupC prfs) =
+ mkTup $ fromAll $ compileAllChecks tyWf tmWf fresh wfs prfs
+compileChecks tyWf tmWf wf (PrjC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf (TSum wfs) (InjC {l, as} i prf) =
+ case lookupRecompute as i of
+ Val i => case nameOf i of
+ Val _ => mkInj l $ compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf
+compileChecks tyWf tmWf wf (CaseC {as = MkRow as fresh} prf prfs) =
+ case synthsRecompute prf of
+ Val _ =>
+ let
+ 0 wfs : AllWellFormed as
+ wfs = case synthsWf tyWf tmWf prf of TSum prfs => prfs
+ in
+ mkCase
+ (compileSynths tyWf tmWf prf)
+ (fromAll $ compileAllBranches tyWf tmWf fresh wfs wf prfs)
+compileChecks tyWf tmWf (TFix {x} sp wf) (RollC prf) =
+ compileChecks tyWf tmWf (subWf [<x :- TFix sp wf] wf) prf
+compileChecks tyWf tmWf wf (UnrollC prf1 prf2) = compileSynths tyWf tmWf prf1
+compileChecks tyWf tmWf wf (FoldC {x, a, y} prf1 prf2) =
+ case synthsRecompute prf1 of
+ Val (TFix x a) =>
+ let
+ 0 spwf : (%% x `StrictlyPositiveIn` a, WellFormed a)
+ spwf = case synthsWf tyWf tmWf prf1 of TFix sp wf => (sp, wf)
+ in
+ compileFold (snd spwf) (fst spwf)
+ (compileSynths tyWf tmWf prf1)
+ (pretty y)
+ (compileChecks tyWf (tmWf :< (y :- (subWf [<x :- wf] $ snd spwf))) wf prf2)
+compileChecks tyWf tmWf wf (MapC prf1 prf2) = compileSynths tyWf tmWf prf1
+
+compileSpine tyWf tmWf wf [] fun = fun
+compileSpine tyWf tmWf (TArrow wf1 wf2) (prf :: prfs) fun =
+ let arg = compileChecks tyWf tmWf wf1 prf in
+ let fun = compileSpine tyWf tmWf wf2 prfs fun in
+ parens $ align $ hang 1 $ group fun <++> group arg
+
+compileAllSynths tyWf tmWf [<] = [<]
+compileAllSynths tyWf tmWf ((:<) prfs {l} prf) =
+ compileAllSynths tyWf tmWf prfs :< (l :- compileSynths tyWf tmWf prf)
+
+compileAllChecks tyWf tmWf fresh wfs Base = [<]
+compileAllChecks tyWf tmWf fresh wfs (Step {l, as} i prf prfs) =
+ case lookupRecompute (MkRow as fresh) i of
+ Val i => case nameOf i of
+ Val _ =>
+ compileAllChecks tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) prfs :<
+ (l :- compileChecks tyWf tmWf (indexAllWellFormed wfs i) prf)
+
+compileAllBranches tyWf tmWf fresh wfs wf Base = [<]
+compileAllBranches tyWf tmWf fresh wfs wf (Step {l, x, as} i prf prfs) =
+ case lookupRecompute (MkRow as fresh) i of
+ Val i => case nameOf i of
+ Val _ =>
+ compileAllBranches tyWf tmWf (dropElemFresh as fresh i) (dropAllWellFormed wfs i) wf prfs :<
+ (l :- (pretty x, compileChecks tyWf (tmWf :< (x :- indexAllWellFormed wfs i)) wf prf))
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 7051e4b..4bf8f05 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -2,8 +2,8 @@ module Inky.Term.Desugar
import Data.List.Quantifiers
import Data.Maybe
-import Inky.Data.List
-import Inky.Decidable
+import Flap.Data.List
+import Flap.Decidable
import Inky.Term
import Inky.Term.Substitution
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 1c6eb58..4d68242 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -7,14 +7,15 @@ import Data.Nat
import Data.List1
import Data.String
-import Inky.Data.Context
-import Inky.Data.Context.Var
+import Flap.Data.Context
+import Flap.Data.Context.Var
+import Flap.Data.SnocList.Var
+import Flap.Data.SnocList.Thinning
+import Flap.Decidable
+import Flap.Decidable.Maybe
+import Flap.Parser
+
import Inky.Data.Row
-import Inky.Data.SnocList.Var
-import Inky.Data.SnocList.Thinning
-import Inky.Decidable
-import Inky.Decidable.Maybe
-import Inky.Parser
import Inky.Term
import Inky.Type
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index bb19b2f..651d208 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -5,9 +5,10 @@ import Data.Singleton
import Data.String
import Data.These
-import Inky.Decidable.Maybe
+import Flap.Decidable.Maybe
+
import Inky.Term
-import Inky.Term.Checks
+import Inky.Term.Recompute
import Inky.Type.Pretty
import Text.PrettyPrint.Prettyprinter
diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr
new file mode 100644
index 0000000..dd0e809
--- /dev/null
+++ b/src/Inky/Term/Recompute.idr
@@ -0,0 +1,128 @@
+module Inky.Term.Recompute
+
+import Data.List.Quantifiers
+import Data.Singleton
+import Inky.Term
+import Inky.Type.Substitution
+
+%hide Prelude.Ops.infixl.(>=>)
+
+-- Can recompute arguments and result from function
+
+export
+isFunctionRecompute :
+ {bound : List String} -> {a : Ty tyCtx} ->
+ {0 dom : All (Assoc0 $ Ty tyCtx) bound} ->
+ (0 _ : IsFunction bound a dom cod) -> (Singleton dom, Singleton cod)
+isFunctionRecompute Done = (Val _, Val _)
+isFunctionRecompute (Step {a} prf) =
+ mapFst (\case Val _ => Val _) $ isFunctionRecompute prf
+
+-- Can recompute type from synthesis proof
+
+export
+synthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {e : _} ->
+ (0 _ : Synths tyEnv tmEnv e a) -> Singleton a
+checkSpineRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {a : _} -> {ts : _} ->
+ (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
+ Singleton b
+allSynthsRecompute :
+ {tyEnv : _} -> {tmEnv : _} -> {es : Context _} ->
+ {0 as : Row (Ty [<])} ->
+ (0 _ : AllSynths tyEnv tmEnv es as) -> Singleton as
+
+synthsRecompute (AnnotS wf prf) = Val _
+synthsRecompute VarS = Val _
+synthsRecompute (LetS prf1 prf2) =
+ case synthsRecompute prf1 of
+ Val _ => synthsRecompute prf2
+synthsRecompute (LetTyS wf prf) = synthsRecompute prf
+synthsRecompute (AppS prf prfs) =
+ case synthsRecompute prf of
+ Val _ => checkSpineRecompute prfs
+synthsRecompute (TupS prfs) =
+ case allSynthsRecompute prfs of
+ Val _ => Val _
+synthsRecompute (PrjS {l, as} prf i) =
+ case synthsRecompute prf of
+ Val _ => case lookupRecompute as i of
+ Val i => [| (nameOf i).value |]
+synthsRecompute (UnrollS prf) =
+ case synthsRecompute prf of
+ Val _ => Val _
+synthsRecompute (MapS f g h) = Val _
+
+checkSpineRecompute [] = Val _
+checkSpineRecompute (prf :: prfs) = checkSpineRecompute prfs
+
+allSynthsRecompute [<] = Val _
+allSynthsRecompute (prfs :< prf) =
+ case (allSynthsRecompute prfs, synthsRecompute prf) of
+ (Val _, Val _) => Val _
+
+-- Synthesised types are well-formed
+
+export
+indexAllWellFormed : AllWellFormed as -> Elem (l :- a) as -> WellFormed a
+indexAllWellFormed (wfs :< wf) Here = wf
+indexAllWellFormed (wfs :< wf) (There i) = indexAllWellFormed wfs i
+
+export
+dropAllWellFormed : AllWellFormed as -> (i : Elem (l :- a) as) -> AllWellFormed (dropElem as i)
+dropAllWellFormed (wfs :< wf) Here = wfs
+dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf
+
+export
+synthsWf :
+ {e : Term mode m tyCtx tmCtx} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
+ Synths tyEnv tmEnv e a -> WellFormed a
+checkSpineWf :
+ CheckSpine tyEnv tmEnv a ts b ->
+ WellFormed a -> WellFormed b
+allSynthsWf :
+ {es : Context (Term mode m tyCtx tmCtx)} ->
+ {tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
+ {tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
+ DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
+ AllSynths tyEnv tmEnv es as -> AllWellFormed as.context
+
+synthsWf tyWf tmWf (AnnotS wf prf) = subWf tyWf wf
+synthsWf tyWf tmWf (VarS {i}) = indexDAll i.pos tmWf
+synthsWf tyWf tmWf (LetS {x} prf1 prf2) =
+ case synthsRecompute prf1 of
+ Val _ => synthsWf tyWf (tmWf :< (x :- synthsWf tyWf tmWf prf1)) prf2
+synthsWf tyWf tmWf (LetTyS wf {x} prf) =
+ synthsWf (tyWf :< (x :- subWf tyWf wf)) tmWf prf
+synthsWf tyWf tmWf (AppS prf prfs) = checkSpineWf prfs (synthsWf tyWf tmWf prf)
+synthsWf tyWf tmWf (TupS prfs) = TProd (allSynthsWf tyWf tmWf prfs)
+synthsWf tyWf tmWf (PrjS prf i) =
+ let TProd wfs = synthsWf tyWf tmWf prf in
+ indexAllWellFormed wfs i
+synthsWf tyWf tmWf (UnrollS {x} prf) =
+ let TFix sp wf = synthsWf tyWf tmWf prf in
+ case synthsRecompute prf of
+ Val _ => subWf [<x :- TFix sp wf] wf
+synthsWf tyWf tmWf (MapS (TFix {x} sp wf1) wf2 wf3) =
+ let wf2 = subWf tyWf wf2 in
+ let wf3 = subWf tyWf wf3 in
+ TArrow (TArrow wf2 wf3) (TArrow
+ (subWf (tyWf :< (x :- wf2)) wf1)
+ (subWf (tyWf :< (x :- wf3)) wf1))
+
+checkSpineWf [] wf = wf
+checkSpineWf (prf :: prfs) (TArrow wf1 wf2) = checkSpineWf prfs wf2
+
+allSynthsWf tyWf tmWf [<] = [<]
+allSynthsWf tyWf tmWf (prfs :< prf) = allSynthsWf tyWf tmWf prfs :< synthsWf tyWf tmWf prf
+
+export
+isFunctionWf :
+ IsFunction bound a dom cod -> WellFormed a ->
+ (DAll WellFormed dom, WellFormed cod)
+isFunctionWf Done wf = ([], wf)
+isFunctionWf (Step {x} prf) (TArrow wf1 wf2) = mapFst ((x :- wf1) ::) $ isFunctionWf prf wf2
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
index 690e38c..c99f5e6 100644
--- a/src/Inky/Term/Substitution.idr
+++ b/src/Inky/Term/Substitution.idr
@@ -1,7 +1,7 @@
module Inky.Term.Substitution
import Data.List.Quantifiers
-import Inky.Data.List
+import Flap.Data.List
import Inky.Term
public export
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 16:27:38 +0000