From 974717f0aa46bb295d44e239594b38f63f39ceab Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 17 Sep 2024 17:09:41 +0100 Subject: Introduce names in contexts. Introduce rows for n-ary sums and products. Remove union types. --- inky.ipkg | 1 + src/Inky/Context.idr | 605 ++++++++++++++++++++++++ src/Inky/Parser.idr | 183 ++------ src/Inky/Term.idr | 991 ++++++++++++++++++++------------------- src/Inky/Term/Pretty.idr | 93 ++-- src/Inky/Thinning.idr | 202 ++++---- src/Inky/Type.idr | 1162 +++++++++++----------------------------------- src/Inky/Type/Pretty.idr | 70 +-- 8 files changed, 1612 insertions(+), 1695 deletions(-) create mode 100644 src/Inky/Context.idr diff --git a/inky.ipkg b/inky.ipkg index 22902e4..b3d274f 100644 --- a/inky.ipkg +++ b/inky.ipkg @@ -9,6 +9,7 @@ depends = contrib modules = Data.Maybe.Decidable , Data.These.Decidable + , Inky.Context , Inky.Parser , Inky.Term , Inky.Term.Pretty diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr new file mode 100644 index 0000000..b0393f3 --- /dev/null +++ b/src/Inky/Context.idr @@ -0,0 +1,605 @@ +module Inky.Context + +import public Data.Singleton +import public Data.So + +import Data.Bool.Decidable +import Data.Maybe.Decidable +import Data.DPair +import Data.Nat + +-- Contexts -------------------------------------------------------------------- + +export +infix 2 :- + +export +prefix 2 %% + +public export +record Assoc (a : Type) where + constructor (:-) + name : String + value : a + +public export +Functor Assoc where + map f x = x.name :- f x.value + +namespace Irrelevant + public export + record Assoc0 (a : Type) where + constructor (:-) + 0 name : String + value : a + + public export + Functor Assoc0 where + map f x = x.name :- f x.value + +public export +data Context : Type -> Type where + Lin : Context a + (:<) : Context a -> Assoc a -> Context a + +public export +Functor Context where + map f [<] = [<] + map f (ctx :< x) = map f ctx :< map f x + +public export +Foldable Context where + foldr f x [<] = x + foldr f x (ctx :< (_ :- y)) = foldr f (f y x) ctx + + foldl f x [<] = x + foldl f x (ctx :< (_ :- y)) = f (foldl f x ctx) y + + null [<] = True + null (ctx :< x) = False + +%name Context ctx + +public export +data Length : Context a -> Type where + Z : Length [<] + S : Length ctx -> Length (ctx :< x) + +%name Length len + +public export +(++) : Context a -> Context a -> Context a +ctx ++ [<] = ctx +ctx ++ ctx' :< x = (ctx ++ ctx') :< x + +export +lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2) +lengthAppend len1 Z = len1 +lengthAppend len1 (S len2) = S (lengthAppend len1 len2) + +length : Context a -> Nat +length [<] = 0 +length (ctx :< x) = S (length ctx) + +-- Variables ------------------------------------------------------------------- + +public export +data VarPos : Context a -> (0 x : String) -> a -> Type where + [search x] + Here : VarPos (ctx :< (x :- v)) x v + There : VarPos ctx x v -> VarPos (ctx :< y) x v + +public export +record Var (ctx : Context a) (v : a) where + constructor (%%) + 0 name : String + {auto pos : VarPos ctx name v} + +%name VarPos pos +%name Var i, j, k + +public export +toVar : VarPos ctx x v -> Var ctx v +toVar pos = (%%) x {pos} + +public export +toNat : VarPos ctx x v -> Nat +toNat Here = 0 +toNat (There pos) = S (toNat pos) + +public export +ThereVar : Var ctx v -> Var (ctx :< x) v +ThereVar i = toVar (There i.pos) + +-- Basic Properties + +export +thereCong : + {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y v} -> i = j -> + There {y = z} i = There {y = z} j +thereCong Refl = Refl + +export +toVarCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toVar i = toVar j +toVarCong Refl = Refl + +export +toNatCong : {0 i : VarPos ctx x v} -> {0 j : VarPos ctx y w} -> i = j -> toNat i = toNat j +toNatCong Refl = Refl + +export +toNatCong' : {0 i, j : Var ctx v} -> i = j -> toNat i.pos = toNat j.pos +toNatCong' Refl = Refl + +export +toNatInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y w} -> (0 _ : toNat i = toNat j) -> i = j +toNatInjective {i = Here} {j = Here} prf = Refl +toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf) + toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl + +export +toVarInjective : {i : VarPos ctx x v} -> {j : VarPos ctx y v} -> (0 _ : toVar i = toVar j) -> i = j +toVarInjective prf = toNatInjective $ toNatCong' prf + +-- Decidable Equality + +export +eq : Var ctx v -> Var ctx w -> Bool +eq i j = toNat i.pos == toNat j.pos + +public export +Eq (Var {a} ctx v) where + (==) = eq + +reflectPosEq : + (i : VarPos ctx x v) -> + (j : VarPos ctx y w) -> + (i = j) `Reflects` (toNat i == toNat j) +reflectPosEq Here Here = RTrue Refl +reflectPosEq Here (There j) = RFalse (\case Refl impossible) +reflectPosEq (There i) Here = RFalse (\case Refl impossible) +reflectPosEq (There i) (There j) with (reflectPosEq i j) | (toNat i == toNat j) + reflectPosEq (There i) (There .(i)) | RTrue Refl | _ = RTrue Refl + _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) + +export +reflectEq : (i : Var {a} ctx v) -> (j : Var ctx w) -> (i = j) `Reflects` (i `eq` j) +reflectEq ((%%) x {pos = pos1}) ((%%) y {pos = pos2}) + with (reflectPosEq pos1 pos2) | (toNat pos1 == toNat pos2) + _ | RTrue eq | _ = RTrue (toVarCong eq) + _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) + +-- Weakening + +wknLPos : VarPos ctx1 x v -> Length ctx2 -> VarPos (ctx1 ++ ctx2) x v +wknLPos pos Z = pos +wknLPos pos (S len) = There (wknLPos pos len) + +wknRPos : VarPos ctx2 x v -> VarPos (ctx1 ++ ctx2) x v +wknRPos Here = Here +wknRPos (There pos) = There (wknRPos pos) + +splitPos : Length ctx2 -> VarPos (ctx1 ++ ctx2) x v -> Either (VarPos ctx1 x v) (VarPos ctx2 x v) +splitPos Z pos = Left pos +splitPos (S len) Here = Right Here +splitPos (S len) (There pos) = mapSnd There $ splitPos len pos + +export +wknL : {auto len : Length ctx2} -> Var ctx1 v -> Var (ctx1 ++ ctx2) v +wknL i = toVar $ wknLPos i.pos len + +export +wknR : Var ctx2 v -> Var (ctx1 ++ ctx2) v +wknR i = toVar $ wknRPos i.pos + +export +split : {auto len : Length ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x) +split i = bimap toVar toVar $ splitPos len i.pos + +export +lift : + {auto len : Length ctx} -> + (forall x. Var ctx1 x -> Var ctx2 x) -> + Var (ctx1 ++ ctx) x -> Var (ctx2 ++ ctx) x +lift f = either (wknL {len} . f) wknR . split {len} + +-- Names + +nameOfPos : {ctx : Context a} -> VarPos ctx x v -> Singleton x +nameOfPos Here = Val x +nameOfPos (There pos) = nameOfPos pos + +export +nameOf : {ctx : Context a} -> (i : Var ctx v) -> Singleton i.name +nameOf i = nameOfPos i.pos + +-- Environments ---------------------------------------------------------------- + +namespace Quantifier + public export + data All : (0 p : a -> Type) -> Context a -> Type where + Lin : All p [<] + (:<) : + All p ctx -> (px : Assoc0 (p x.value)) -> + {auto 0 prf : px.name = x.name}-> + All p (ctx :< x) + + %name Quantifier.All env + + indexAllPos : VarPos ctx x v -> All p ctx -> p v + indexAllPos Here (env :< px) = px.value + indexAllPos (There pos) (env :< px) = indexAllPos pos env + + export + indexAll : Var ctx v -> All p ctx -> p v + indexAll i env = indexAllPos i.pos env + + export + mapProperty : ({0 x : a} -> p x -> q x) -> All p ctx -> All q ctx + mapProperty f [<] = [<] + mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px) + + export + (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2) + env1 ++ [<] = env1 + env1 ++ env2 :< px = (env1 ++ env2) :< px + +-- Rows ------------------------------------------------------------------------ + +namespace Row + ||| Contexts where names are unique. + public export + data Row : Type -> Type + + public export + freshIn : String -> Row a -> Bool + + data Row where + Lin : Row a + (:<) : (row : Row a) -> (x : Assoc a) -> {auto 0 fresh : So (x.name `freshIn` row)} -> Row a + + x `freshIn` [<] = True + x `freshIn` (row :< y) = x /= y.name && (x `freshIn` row) + + %name Row row + + public export + map : (a -> b) -> Row a -> Row b + export + 0 mapFresh : (f : a -> b) -> (row : Row a) -> So (x `freshIn` row) -> So (x `freshIn` map f row) + + map f [<] = [<] + map f ((:<) row x {fresh}) = (:<) (map f row) (map f x) {fresh = mapFresh f row fresh} + + mapFresh f [<] = id + mapFresh f (row :< (y :- _)) = andSo . mapSnd (mapFresh f row) . soAnd + + public export + Functor Row where + map = Row.map + + public export + Foldable Row where + foldr f x [<] = x + foldr f x (row :< (_ :- y)) = foldr f (f y x) row + + foldl f x [<] = x + foldl f x (row :< (_ :- y)) = f (foldl f x row) y + + null [<] = True + null (row :< x) = False + + ||| Forget the freshness of names. + public export + forget : Row a -> Context a + forget [<] = [<] + forget (row :< x) = forget row :< x + + -- Equality -- + + soUnique : (x, y : So b) -> x = y + soUnique Oh Oh = Refl + + export + snocCong2 : + {0 row1, row2 : Row a} -> row1 = row2 -> + {0 x, y : Assoc a} -> x = y -> + {0 fresh1 : So (x.name `freshIn` row1)} -> + {0 fresh2 : So (y.name `freshIn` row2)} -> + row1 :< x = row2 :< y + snocCong2 Refl Refl = rewrite soUnique fresh1 fresh2 in Refl + + -- Variables aren't fresh -- + + -- NOTE: cannot implement + 0 strEqReflect : (x, y : String) -> (x = y) `Reflects` (x == y) + strEqReflect x y = believe_me () + + 0 strEqRefl : (x : String) -> Not (So (x /= x)) + strEqRefl x prf with (strEqReflect x x) | (x == x) + _ | RTrue _ | _ = absurd prf + _ | RFalse neq | _ = neq Refl + + export + 0 varPosNotFresh : VarPos (forget row) x v -> Not (So (x `freshIn` row)) + varPosNotFresh {row = row :< (x :- v)} Here fresh = strEqRefl x (fst $ soAnd fresh) + varPosNotFresh {row = row :< y} (There pos) fresh = varPosNotFresh pos (snd $ soAnd fresh) + + export + varUniqueIndex : (row : Row a) -> VarPos (forget row) x v -> VarPos (forget row) x w -> v = w + varUniqueIndex (row :< (x :- _)) Here Here = Refl + varUniqueIndex ((:<) row (x :- _) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh + varUniqueIndex ((:<) row (x :- _) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh + varUniqueIndex (row :< (y :- _)) (There pos1) (There pos2) = varUniqueIndex row pos1 pos2 + + -- Equivalence -- + + export infix 6 <~> + + public export + data Step : Row a -> Row a -> Type where + Cong : + Step row1 row2 -> (0 x : Assoc a) -> + {0 fresh1 : So (x.name `freshIn` row1)} -> + {0 fresh2 : So (x.name `freshIn` row2)} -> + Step (row1 :< x) (row2 :< x) + Swap : + (0 x : Assoc a) -> (0 y : Assoc a) -> + {0 fresh1 : So (x.name `freshIn` row)} -> + {0 fresh2 : So (y.name `freshIn` row :< x)} -> + {0 fresh3 : So (y.name `freshIn` row)} -> + {0 fresh4 : So (x.name `freshIn` row :< y)} -> + Step (row :< x :< y) (row :< y :< x) + + public export + data (<~>) : Row a -> Row a -> Type where + Nil : row <~> row + (::) : Step row1 row2 -> row2 <~> row3 -> row1 <~> row3 + + %name Step step + %name (<~>) prf + + export + trans : row1 <~> row2 -> row2 <~> row3 -> row1 <~> row3 + trans [] prf = prf + trans (step :: prf1) prf2 = step :: trans prf1 prf2 + + symStep : Step row1 row2 -> Step row2 row1 + symStep (Cong step x) = Cong (symStep step) x + symStep (Swap x y) = Swap y x + + export + sym : row1 <~> row2 -> row2 <~> row1 + sym [] = [] + sym (step :: prf) = trans (sym prf) [symStep step] + + equivLengthStep : Step row1 row2 -> length (forget row1) = length (forget row2) + equivLengthStep (Cong step x) = cong S (equivLengthStep step) + equivLengthStep (Swap x y) = Refl + + equivLength : row1 <~> row2 -> length (forget row1) = length (forget row2) + equivLength [] = Refl + equivLength (step :: prf) = trans (equivLengthStep step) (equivLength prf) + + export + Uninhabited ((:<) row x {fresh} <~> [<]) where + uninhabited prf = absurd (equivLength prf) + + export + Uninhabited ([<] <~> (:<) row x {fresh}) where + uninhabited prf = absurd (equivLength prf) + + 0 equivFreshInStep : Step row1 row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2) + equivFreshInStep (Cong step y) = andSo . mapSnd (equivFreshInStep step) . soAnd + equivFreshInStep (Swap {row} (y :- v) (z :- w)) = + andSo . mapSnd andSo . + (\(prf1, prf2, prf3) => (prf2, prf1, prf3)) . + mapSnd (soAnd {a = x /= y, b = freshIn x row}) . soAnd + + 0 equivFreshIn : row1 <~> row2 -> So (x `freshIn` row1) -> So (x `freshIn` row2) + equivFreshIn [] = id + equivFreshIn (step :: prf) = equivFreshIn prf . equivFreshInStep step + + cong : + row1 <~> row2 -> (0 x : Assoc a) -> + {0 fresh1 : So (x.name `freshIn` row1)} -> + {0 fresh2 : So (x.name `freshIn` row2)} -> + row1 :< x <~> row2 :< x + cong [] x = rewrite soUnique fresh1 fresh2 in [] + cong (step :: prf) x = + let 0 fresh' = equivFreshInStep step fresh1 in + Cong step x {fresh2 = fresh'} :: cong prf x + + -- Removal -- + + public export + removePos : (row : Row a) -> VarPos (forget row) x v -> (Singleton v, Row a) + export + 0 removePosFresh : + (row : Row a) -> (pos : VarPos (forget row) x v) -> + So (y `freshIn` row) -> So (y `freshIn` snd (removePos row pos)) + + removePos (row :< (_ :- v)) Here = (Val v, row) + removePos ((:<) row x {fresh}) (There pos) = + ( fst (removePos row pos) + , (:<) (snd $ removePos row pos) x {fresh = removePosFresh row pos fresh} + ) + + removePosFresh (row :< _) Here = snd . soAnd + removePosFresh ((:<) row (z :- v) {fresh}) (There pos) = + andSo . mapSnd (removePosFresh row pos) . soAnd + + public export + remove : (row : Row a) -> Var (forget row) v -> (Singleton v, Row a) + remove row i = removePos row i.pos + + -- Reflection + + -- NOTE: cannot implement + 0 soNotSym : {x, y : String} -> So (x /= y) -> So (y /= x) + soNotSym = believe_me + + 0 freshNotPos : (row : Row a) -> VarPos (forget row) x v -> So (y `freshIn` row) -> So (y /= x) + freshNotPos (row :< _) Here = fst . soAnd + freshNotPos (row :< x) (There pos) = freshNotPos row pos . snd . soAnd + + export + 0 removedIsFresh : + (row : Row a) -> (pos : VarPos (forget row) x v) -> + So (x `freshIn` snd (removePos row pos)) + removedIsFresh ((:<) row _ {fresh}) Here = fresh + removedIsFresh ((:<) row (y :- v) {fresh}) (There pos) = + andSo (soNotSym (freshNotPos row pos fresh), removedIsFresh row pos) + + export + reflectRemovePos : + (row : Row a) -> (pos : VarPos (forget row) x v) -> + (:<) (snd $ removePos row pos) (x :- v) {fresh = removedIsFresh row pos} <~> row + reflectRemovePos ((:<) row _ {fresh}) Here = [] + reflectRemovePos ((:<) row (y :- w) {fresh}) (There pos) = + ( Swap (y :- w) (x :- v) + {fresh4 = andSo (freshNotPos row pos fresh, removePosFresh row pos fresh)} + :: cong (reflectRemovePos row pos) (y :- w)) + + -- Tracing Variables -- + + equivVarPosStep : Step row1 row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v + equivVarPosStep (Cong step _) Here = Here + equivVarPosStep (Cong step y) (There pos) = There (equivVarPosStep step pos) + equivVarPosStep (Swap y _) Here = There Here + equivVarPosStep (Swap _ z) (There Here) = Here + equivVarPosStep (Swap y z) (There (There pos)) = There (There pos) + + export + equivVarPos : row1 <~> row2 -> VarPos (forget row1) x v -> VarPos (forget row2) x v + equivVarPos [] = id + equivVarPos (step :: prf) = equivVarPos prf . equivVarPosStep step + + removePosInjectiveStep : + (prf : Step row1 row2) -> (pos : VarPos (forget row1) x v) -> + snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPosStep prf pos)) + removePosInjectiveStep (Cong step _) Here = [step] + removePosInjectiveStep (Cong step (y :- v)) (There pos) = + cong (removePosInjectiveStep step pos) (y :- v) + removePosInjectiveStep (Swap (y :- v) _) Here = cong [] (y :- v) + removePosInjectiveStep (Swap _ (z :- v)) (There Here) = cong [] (z :- v) + removePosInjectiveStep (Swap (y :- v) (z :- w)) (There (There pos)) = [Swap (y :- v) (z :- w)] + + export + removePosInjective : + (prf : row1 <~> row2) -> (pos : VarPos (forget row1) x v) -> + snd (removePos row1 pos) <~> snd (removePos row2 (equivVarPos prf pos)) + removePosInjective [] pos = [] + removePosInjective (step :: prf) pos = + trans (removePosInjectiveStep step pos) (removePosInjective prf $ equivVarPosStep step pos) + + export + equivVarUnique : + {0 fresh1 : So (x `freshIn` row1)} -> + {0 fresh2 : So (x `freshIn` row2)} -> + (prf : row1 :< (x :- v) <~> row2 :< (x :- v)) -> + equivVarPos prf Here = Here + equivVarUnique prf with (equivVarPos prf Here) + _ | Here = Refl + _ | There pos = void $ varPosNotFresh pos fresh2 + + -- Partial Removal -- + + FreshOrNothing : String -> Maybe (a, Row a) -> Type + FreshOrNothing x Nothing = () + FreshOrNothing x (Just (a, row)) = So (x `freshIn` row) + + removeHelper : + (m : Maybe (a, Row a)) -> (x : Assoc a) -> + (0 fresh : FreshOrNothing x.name m) -> + Maybe (a, Row a) + removeHelper Nothing x fresh = Nothing + removeHelper (Just (v, row)) x fresh = Just (v, row :< x) + + ||| Attempt to remove the value at name `x` from the row. + export + remove' : String -> Row a -> Maybe (a, Row a) + removeFresh : + (x : String) -> (row : Row a) -> + {y : String} -> So (y `freshIn` row) -> FreshOrNothing y (remove' x row) + + remove' x [<] = Nothing + remove' x ((:<) row (y :- v) {fresh}) = + if y == x + then Just (v, row) + else removeHelper (remove' x row) (y :- v) (removeFresh x row fresh) + + removeFresh x [<] prf = () + removeFresh x (row :< (y :- v)) {y = z} prf with (y == x) + _ | True = snd (soAnd prf) + _ | False with (removeFresh x row $ snd $ soAnd prf) | (remove' x row) + _ | _ | Nothing = () + _ | prf' | Just (v', row') = andSo (fst (soAnd prf), prf') + + -- Reflection + + notSoToSoNot : {b : Bool} -> Not (So b) -> So (not b) + notSoToSoNot {b = False} nprf = Oh + notSoToSoNot {b = True} nprf = absurd (nprf Oh) + + 0 reflectRemoveHelper : {x, y : String} -> Not (x = y) -> Not (So (x == y)) + reflectRemoveHelper neq eq with (strEqReflect x y) | (x == y) + reflectRemoveHelper neq Oh | RTrue eq | _ = neq eq + + reflectRemoveHelper' : + {0 fresh1 : So (y `freshIn` row1)} -> + (x : String) -> Not (y = x) -> + (0 fresh2 : So (x `freshIn` row2)) -> (prf : row1 :< (y :- v) <~> row2 :< (x :- v')) -> + ( pos : VarPos (forget row2) y v + ** snd (removePos (row2 :< (x :- v')) (equivVarPos prf Here)) <~> + (:<) (snd (removePos row2 pos)) (x :- v') + {fresh = removePosFresh row2 pos {y = x} fresh2}) + reflectRemoveHelper' x neq fresh2 prf with (equivVarPos prf Here) + reflectRemoveHelper' x neq fresh2 prf | Here = absurd (neq Refl) + reflectRemoveHelper' x neq fresh2 prf | There pos = + (pos ** []) + + public export + Remove : String -> Row a -> a -> Row a -> Type + Remove x row v row' = + Exists {type = So (x `freshIn` row')} (\fresh => row <~> row' :< (x :- v)) + + export + removeUnique : + (x : String) -> (row1 : Row a) -> + Remove x row1 v row2 -> Remove x row1 w row3 -> (v = w, row2 <~> row3) + removeUnique x row1 (Evidence fresh1 prf1) (Evidence fresh2 prf2) = + let eq = varUniqueIndex row1 (equivVarPos (sym prf1) Here) (equivVarPos (sym prf2) Here) in + let + prf : row2 :< (x :- v) <~> row3 :< (x :- v) + prf = trans (sym prf1) (rewrite eq in prf2) + in + ( eq + , replace + {p = \pos => row2 <~> snd (removePos (row3 :< (x :- v)) pos)} + (equivVarUnique prf) + (removePosInjective prf Here)) + + export + 0 reflectRemove : + (x : String) -> (row : Row a) -> + uncurry (Remove x row) `OnlyWhen` remove' x row + reflectRemove x [<] = RNothing (\(v, row), (Evidence _ prf) => absurd prf) + reflectRemove x ((:<) row (y :- v) {fresh}) with (strEqReflect y x) | (y == x) + _ | RTrue eq | _ = rewrite sym eq in RJust (Evidence fresh []) + _ | RFalse neq | _ with (reflectRemove x row, removeFresh x row {y}) | (remove' x row) + _ | (RJust (Evidence fresh' prf), mkFresh) | Just (v', row') = + RJust (Evidence + (andSo (notSoToSoNot (reflectRemoveHelper (\eq => neq $ sym eq)), fresh')) + (trans + (cong prf (y :- v) + {fresh2 = andSo (notSoToSoNot (reflectRemoveHelper neq), mkFresh fresh)}) + [Swap (x :- v') (y :- v)])) + _ | (RNothing nprf, mkFresh) | _ = + RNothing (\(v', row'), (Evidence fresh' prf) => + let (pos ** prf') = reflectRemoveHelper' x neq fresh' prf in + void $ + nprf (v', snd (remove row' ((%%) y {pos}))) $ + Evidence + (removePosFresh row' pos fresh') + (trans (removePosInjective prf Here) prf')) diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr index 047165c..1ad48d8 100644 --- a/src/Inky/Parser.idr +++ b/src/Inky/Parser.idr @@ -7,116 +7,9 @@ import Data.List.Elem import Data.List1 import Data.Nat import Data.So +import Inky.Context +import Text.Lexer --- Contexts -------------------------------------------------------------------- - -export -infix 2 :- - -export -prefix 2 %% - -public export -record Assoc (a : Type) where - constructor (:-) - 0 name : String - value : a - -public export -data Context : Type -> Type where - Lin : Context a - (:<) : Context a -> Assoc a -> Context a - -%name Context ctx - -public export -data Length : Context a -> Type where - Z : Length [<] - S : Length ctx -> Length (ctx :< x) - -%name Length len - -public export -(++) : Context a -> Context a -> Context a -ctx ++ [<] = ctx -ctx ++ ctx' :< x = (ctx ++ ctx') :< x - -lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2) -lengthAppend len1 Z = len1 -lengthAppend len1 (S len2) = S (lengthAppend len1 len2) - --- Variableents - -public export -data VariablePos : Context a -> (0 x : String) -> a -> Type where - [search x] - Here : VariablePos (ctx :< (x :- v)) x v - There : VariablePos ctx x v -> VariablePos (ctx :< y) x v - -public export -record Variable (ctx : Context a) (v : a) where - constructor (%%) - 0 name : String - {auto pos : VariablePos ctx name v} - -toVar : VariablePos ctx x v -> Variable ctx v -toVar pos = (%%) x {pos} - -wknLPos : VariablePos ctx1 x v -> Length ctx2 -> VariablePos (ctx1 ++ ctx2) x v -wknLPos x Z = x -wknLPos x (S len) = There (wknLPos x len) - -wknRPos : VariablePos ctx2 x v -> VariablePos (ctx1 ++ ctx2) x v -wknRPos Here = Here -wknRPos (There x) = There (wknRPos x) - -splitPos : Length ctx2 -> VariablePos (ctx1 ++ ctx2) x v -> Either (VariablePos ctx1 x v) (VariablePos ctx2 x v) -splitPos Z x = Left x -splitPos (S len) Here = Right Here -splitPos (S len) (There x) = mapSnd There $ splitPos len x - -wknL : {auto len : Length ctx2} -> Variable ctx1 v -> Variable (ctx1 ++ ctx2) v -wknL x = (%%) x.name {pos = wknLPos x.pos len} - -wknR : Variable ctx2 v -> Variable (ctx1 ++ ctx2) v -wknR x = (%%) x.name {pos = wknRPos x.pos} - -split : {auto len : Length ctx2} -> Variable (ctx1 ++ ctx2) x -> Either (Variable ctx1 x) (Variable ctx2 x) -split x = bimap toVar toVar $ splitPos len x.pos - -lift : - {auto len : Length ctx} -> - (forall x. Variable ctx1 x -> Variable ctx2 x) -> - Variable (ctx1 ++ ctx) x -> Variable (ctx2 ++ ctx) x -lift f = either (wknL {len} . f) wknR . split {len} - --- Environments - -namespace Quantifier - public export - data All : (0 p : a -> Type) -> Context a -> Type where - Lin : All p [<] - (:<) : All p ctx -> (px : p x.value) -> All p (ctx :< x) - - %name Quantifier.All env - - indexAllPos : VariablePos ctx x v -> All p ctx -> p v - indexAllPos Here (env :< px) = px - indexAllPos (There x) (env :< px) = indexAllPos x env - - export - indexAll : Variable ctx v -> All p ctx -> p v - indexAll x env = indexAllPos x.pos env - - export - mapProperty : ({0 x : a} -> p x -> q x) -> All p ctx -> All q ctx - mapProperty f [<] = [<] - mapProperty f (env :< px) = mapProperty f env :< f px - - export - (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2) - env1 ++ [<] = env1 - env1 ++ env2 :< px = (env1 ++ env2) :< px -- Parser Expressions ---------------------------------------------------------- @@ -131,10 +24,10 @@ linUnless True ctx = ctx public export data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type where - Var : (f : a -> b) -> Variable free (nil, a) -> Parser i nil locked free b + Var : (f : a -> b) -> Var free (nil, a) -> Parser i nil locked free b Fail : (msg : String) -> Parser i False locked free a Empty : (x : a) -> Parser i True locked free a - Lit : (text : i) -> (x : a) -> Parser i False locked free a + Lit : (text : i) -> (x : String -> a) -> Parser i False locked free a (<**>) : {nil1, nil2 : Bool} -> Parser i nil1 locked free (a -> b) -> @@ -158,7 +51,7 @@ Functor (Parser i nil locked free) where map f (Var g x) = Var (f . g) x map f (Fail msg) = Fail msg map f (Empty x) = Empty (f x) - map f (Lit text x) = Lit text (f x) + map f (Lit text g) = Lit text (f . g) map f ((<**>) {nil1 = True} p q) = map (f .) p <**> q map f ((<**>) {nil1 = False} p q) = map (f .) p <**> q map f (p <|> q) = map f p <|> map f q @@ -209,7 +102,7 @@ follow penv1 penv2 fenv1 fenv2 (Fix x f p) = -- Proof: -- - we always add information -- - no step depends on existing information - follow (penv1 :< peek penv2 p) penv2 (fenv1 :< empty) fenv2 p + follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p export WellTyped : @@ -246,8 +139,8 @@ WellTyped penv1 penv2 fenv1 fenv2 (p <|> q) = ) WellTyped penv1 penv2 fenv1 fenv2 (Fix x f p) = let fst = peek penv2 p in - let flw = follow (penv1 :< fst) penv2 (fenv1 :< empty) fenv2 p in - WellTyped (penv1 :< fst) penv2 (fenv1 :< flw) fenv2 p + let flw = follow (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- empty)) fenv2 p in + WellTyped (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- flw)) fenv2 p -- Parsing Function ------------------------------------------------------------ @@ -320,9 +213,9 @@ parser : (fenv1 : _) -> (fenv2 : _) -> {auto 0 wf : WellTyped penv1 penv2 fenv1 fenv2 p} -> - (xs : List i) -> - All (\x => (ys : List i) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked -> - All (\x => (ys : List i) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free -> + (xs : List (WithBounds (Token i))) -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x) locked -> + All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x) free -> M xs nil a parser (Var f x) penv1 penv2 fenv1 fenv2 xs env1 env2 = f <$> indexAll x env2 xs (Lax reflexive) @@ -330,13 +223,13 @@ parser (Fail msg) penv1 penv2 fenv1 fenv2 xs env1 env2 = Err msg parser (Empty x) penv1 penv2 fenv1 fenv2 xs env1 env2 = Ok x xs (Lax reflexive) -parser (Lit text x) penv1 penv2 fenv1 fenv2 xs env1 env2 = +parser (Lit text f) penv1 penv2 fenv1 fenv2 xs env1 env2 = case xs of [] => Err "expected \{text}, got end of file" y :: ys => - if y == text - then Ok x ys (Strict reflexive) - else Err "expected \{text}, got \{y}" + if y.val.kind == text + then Ok (f y.val.text) ys (Strict reflexive) + else Err "\{show y.bounds}: expected \{text}, got \{y.val.kind}" parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of Err msg => Err msg @@ -372,15 +265,15 @@ parser ((<|>) {nil1, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = then parser q penv1 penv2 fenv1 fenv2 [] env1 env2 else Err "unexpected end of input" x :: xs => - if elem x (peek penv2 p) + if elem x.val.kind (peek penv2 p) then wknL (parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) nil2 - else if elem x (peek penv2 q) + else if elem x.val.kind (peek penv2 q) then wknR nil1 (parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) else if nil1 then parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 else if nil2 then parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - else Err "unexpected token \{x}" + else Err "\{show x.bounds}: unexpected \{x.val.kind}" parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = let g = parser p _ _ _ _ {wf} in let @@ -390,7 +283,7 @@ parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = (\ys, rec, lte => g ys ( mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1 - :< (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte)) + :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) ) (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)) xs @@ -403,7 +296,7 @@ parse : Eq i => Interpolation i => (p : Parser i nil [<] [<] a) -> {auto 0 wf : WellTyped [<] [<] [<] [<] p} -> - (xs : List i) -> M xs nil a + (xs : List (WithBounds (Token i))) -> M xs nil a parse p xs = parser p [<] [<] [<] [<] xs [<] [<] -- Weakening ------------------------------------------------------------------- @@ -412,8 +305,8 @@ public export rename : (len1 : Length locked1) -> (len2 : Length locked2) -> - (forall x. Variable locked1 x -> Variable locked2 x) -> - (forall x. Variable free1 x -> Variable free2 x) -> + (forall x. Var locked1 x -> Var locked2 x) -> + (forall x. Var free1 x -> Var free2 x) -> Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a rename len1 len2 ren1 ren2 (Var f x) = Var f (ren2 x) rename len1 len2 ren1 ren2 (Fail msg) = Fail msg @@ -429,6 +322,27 @@ rename len1 len2 ren1 ren2 (p <|> q) = rename len1 len2 ren1 ren2 (Fix x f p) = Fix x f (rename (S len1) (S len2) (lift {len = S Z} ren1) ren2 p) +public export +weaken : + (len1 : Length free2) -> + {auto len2 : Length locked} -> + Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a +weaken len1 (Var f x) = Var f (wknL x) +weaken len1 (Fail msg) = Fail msg +weaken len1 (Empty x) = Empty x +weaken len1 (Lit text x) = Lit text x +weaken len1 ((<**>) {nil1 = False} p q) = + weaken len1 p <**> + rename Z Z + id + ( either (wknL . wknL) (either (wknL . wknR) wknR . split) + . split {len = lengthAppend len1 len2} + ) + q +weaken len1 ((<**>) {nil1 = True} p q) = weaken len1 p <**> weaken len1 q +weaken len1 (p <|> q) = weaken len1 p <|> weaken len1 q +weaken len1 (Fix x f p) = Fix x f (weaken len1 p) + public export shift : {auto len1 : Length locked1} -> @@ -465,15 +379,8 @@ public export p <** q = const <$> p <**> q public export -match : i -> Parser i False locked free () -match x = Lit x () - -public export -oneOf : (xs : List i) -> {auto 0 _ : NonEmpty xs} -> Parser i False locked free (x ** Elem x xs) -oneOf [x] = (x ** Here) <$ match x -oneOf (x :: xs@(_ :: _)) = - (x ** Here) <$ match x <|> - (\y => (y.fst ** There y.snd)) <$> oneOf xs +match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind) +match kind = Lit kind (tokValue kind) public export option : Parser i False locked free a -> Parser i True locked free (Maybe a) diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index f6e095c..d80ce77 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -2,60 +2,54 @@ module Inky.Term import Data.Bool.Decidable import Data.DPair -import Data.List.Elem import Data.Maybe.Decidable -import Data.These -import Data.Vect +import Data.List +import Inky.Context import Inky.Thinning import Inky.Type --- Redefine so I can prove stuff about it -%hide -Prelude.getAt - -getAt : Nat -> List a -> Maybe a -getAt k [] = Nothing -getAt 0 (x :: xs) = Just x -getAt (S k) (x :: xs) = getAt k xs - -------------------------------------------------------------------------------- -- Definition ------------------------------------------------------------------ -------------------------------------------------------------------------------- public export -data SynthTerm : Nat -> Nat -> Type +data SynthTerm : (tyCtx, tmCtx : Context ()) -> Type public export -data CheckTerm : Nat -> Nat -> Type +data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type data SynthTerm where - Var : Fin tm -> SynthTerm ty tm - Lit : Nat -> SynthTerm ty tm - Suc : CheckTerm ty tm -> SynthTerm ty tm - App : SynthTerm ty tm -> List1 (CheckTerm ty tm) -> SynthTerm ty tm - Prj : SynthTerm ty tm -> Nat -> SynthTerm ty tm - Expand : SynthTerm ty tm -> SynthTerm ty tm - Annot : CheckTerm ty tm -> Ty ty -> SynthTerm ty tm + Var : Var tmCtx v -> SynthTerm tyCtx tmCtx + Lit : Nat -> SynthTerm tyCtx tmCtx + Suc : CheckTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx + App : + SynthTerm tyCtx tmCtx -> + (args : List (CheckTerm tyCtx tmCtx)) -> + {auto 0 _ : NonEmpty args} -> + SynthTerm tyCtx tmCtx + Prj : SynthTerm tyCtx tmCtx -> String -> SynthTerm tyCtx tmCtx + Expand : SynthTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx + Annot : CheckTerm tyCtx tmCtx -> Ty tyCtx () -> SynthTerm tyCtx tmCtx data CheckTerm where Let : - SynthTerm ty tm -> - CheckTerm ty (S tm) -> - CheckTerm ty tm - Abs : (k : Nat) -> CheckTerm ty (S k + tm) -> CheckTerm ty tm - Inj : Nat -> CheckTerm ty tm -> CheckTerm ty tm - Tup : List (CheckTerm ty tm) -> CheckTerm ty tm + (x : String) -> SynthTerm tyCtx tmCtx -> + CheckTerm tyCtx (tmCtx :< (x :- ())) -> + CheckTerm tyCtx tmCtx + Abs : (bound : Context ()) -> CheckTerm tyCtx (tmCtx ++ bound) -> CheckTerm tyCtx tmCtx + Inj : String -> CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx + Tup : Context (CheckTerm tyCtx tmCtx) -> CheckTerm tyCtx tmCtx Case : - SynthTerm ty tm -> - List (CheckTerm ty (S tm)) -> - CheckTerm ty tm - Contract : CheckTerm ty tm -> CheckTerm ty tm + SynthTerm tyCtx tmCtx -> + Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> + CheckTerm tyCtx tmCtx + Contract : CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx Fold : - SynthTerm ty tm -> - CheckTerm ty (S tm) -> - CheckTerm ty tm + SynthTerm tyCtx tmCtx -> + (x : String) -> CheckTerm tyCtx (tmCtx :< (x :- ())) -> + CheckTerm tyCtx tmCtx Embed : - SynthTerm ty tm -> - CheckTerm ty tm + SynthTerm tyCtx tmCtx -> + CheckTerm tyCtx tmCtx %name SynthTerm e %name CheckTerm t, u, v @@ -64,639 +58,670 @@ data CheckTerm where -- Well Formed ----------------------------------------------------------------- -------------------------------------------------------------------------------- -GetAt : Nat -> List a -> a -> Type -GetAt k xs x = (n : Elem x xs ** elemToNat n = k) +-- Lookup name in a row -------------------------------------------------------- + +GetAt : String -> Row a -> a -> Type +GetAt x ys y = VarPos (forget ys) x y -CanProject : Ty ty -> List (Ty ty) -> Type -CanProject (TUnion as) bs = forget as = bs -CanProject (TProd as) bs = as = bs -CanProject _ bs = Void +getAtUnique : + (x : String) -> (ys : Row a) -> + GetAt x ys y -> GetAt x ys z -> y = z +getAtUnique x (row :< (x :- b)) Here Here = Refl +getAtUnique x ((:<) row (x :- a) {fresh}) Here (There pos2) = void $ varPosNotFresh pos2 fresh +getAtUnique x ((:<) row (x :- b) {fresh}) (There pos1) Here = void $ varPosNotFresh pos1 fresh +getAtUnique x (row :< (y :- v)) (There pos1) (There pos2) = getAtUnique x row pos1 pos2 + +getAt : String -> Row a -> Maybe a +getAt x as = fst <$> remove' x as + +0 reflectGetAt : (x : String) -> (ys : Row a) -> GetAt x ys `OnlyWhen` getAt x ys +reflectGetAt x ys with (reflectRemove x ys) | (remove' x ys) + _ | RJust (Evidence fresh prf) | Just (y, _) = RJust (equivVarPos (sym prf) Here) + _ | RNothing nprf | _ = + RNothing (\y, pos => + nprf (y, snd (removePos ys pos)) $ + Evidence (removedIsFresh ys pos) (sym $ reflectRemovePos ys pos)) + +-- Test if we have an arrow ---------------------------------------------------- + +IsArrow : Ty tyCtx () -> Ty tyCtx () -> Ty tyCtx () -> Type +IsArrow (TArrow a b) c d = (c = a, d = b) +IsArrow _ c d = Void + +isArrowUnique : (a : Ty tyCtx ()) -> IsArrow a b c -> IsArrow a d e -> (b = d, c = e) +isArrowUnique (TArrow a b) (Refl, Refl) (Refl, Refl) = (Refl, Refl) + +isArrow : Ty tyCtx () -> Maybe (Ty tyCtx (), Ty tyCtx ()) +isArrow (TArrow a b) = Just (a, b) +isArrow _ = Nothing + +reflectIsArrow : (a : Ty tyCtx ()) -> uncurry (IsArrow a) `OnlyWhen` isArrow a +reflectIsArrow (TArrow a b) = RJust (Refl, Refl) +reflectIsArrow (TVar i) = RNothing (\(_, _), x => x) +reflectIsArrow TNat = RNothing (\(_, _), x => x) +reflectIsArrow (TProd as) = RNothing (\(_, _), x => x) +reflectIsArrow (TSum as) = RNothing (\(_, _), x => x) +reflectIsArrow (TFix x a) = RNothing (\(_, _), x => x) + +-- Test if we have a product --------------------------------------------------- + +IsProduct : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type +IsProduct (TProd as) bs = bs = as +IsProduct _ bs = Void -CanInject : Ty ty -> List (Ty ty) -> Type -CanInject (TUnion as) bs = forget as = bs -CanInject (TSum as) bs = as = bs -CanInject _ bs = Void +isProductUnique : (a : Ty tyCtx ()) -> IsProduct a as -> IsProduct a bs -> as = bs +isProductUnique (TProd as) Refl Refl = Refl -IsFixpoint : Ty ty -> Ty (S ty) -> Type -IsFixpoint TNat b = b = TSum [TProd [], TVar FZ] -IsFixpoint (TFix a) b = a = b -IsFixpoint _ b = Void +isProduct : Ty tyCtx () -> Maybe (Row (Ty tyCtx ())) +isProduct (TProd as) = Just as +isProduct _ = Nothing -IsArrow : {ty : Nat} -> (k : Nat) -> Ty ty -> Vect k (Ty ty) -> Ty ty -> Type -IsArrow 0 a as b = (as = [], b = a) -IsArrow (S k) (TArrow dom cod) as b = (bs ** (as = dom :: bs, IsArrow k cod bs b)) -IsArrow (S k) _ as b = Void +reflectIsProduct : (a : Ty tyCtx ()) -> IsProduct a `OnlyWhen` isProduct a +reflectIsProduct (TVar i) = RNothing (\_, x => x) +reflectIsProduct TNat = RNothing (\_, x => x) +reflectIsProduct (TArrow a b) = RNothing (\_, x => x) +reflectIsProduct (TProd as) = RJust Refl +reflectIsProduct (TSum as) = RNothing (\_, x => x) +reflectIsProduct (TFix x a) = RNothing (\_, x => x) -IsProduct : Ty ty -> List (Ty ty) -> Type -IsProduct (TProd as) bs = as = bs -IsProduct _ bs = Void +-- Test if we have a sum ------------------------------------------------------- -IsSum : Ty ty -> List (Ty ty) -> Type -IsSum (TSum as) bs = as = bs +IsSum : Ty tyCtx () -> Row (Ty tyCtx ()) -> Type +IsSum (TSum as) bs = bs = as IsSum _ bs = Void +isSumUnique : (a : Ty tyCtx ()) -> IsSum a as -> IsSum a bs -> as = bs +isSumUnique (TSum as) Refl Refl = Refl + +isSum : Ty tyCtx () -> Maybe (Row (Ty tyCtx ())) +isSum (TSum as) = Just as +isSum _ = Nothing + +reflectIsSum : (a : Ty tyCtx ()) -> IsSum a `OnlyWhen` isSum a +reflectIsSum (TVar i) = RNothing (\_, x => x) +reflectIsSum TNat = RNothing (\_, x => x) +reflectIsSum (TArrow a b) = RNothing (\_, x => x) +reflectIsSum (TProd as) = RNothing (\_, x => x) +reflectIsSum (TSum as) = RJust Refl +reflectIsSum (TFix x a) = RNothing (\_, x => x) + +-- Test if we have a fixpoint -------------------------------------------------- + +IsFixpoint : Ty tyCtx () -> (x ** Ty (tyCtx :< (x :- ())) ()) -> Type +IsFixpoint TNat yb = (fst yb = "X", snd yb = TSum [<"Z" :- TProd [<], "S" :- TVar (%% fst yb)]) +IsFixpoint (TFix x a) yb = (prf : (fst yb = x) ** (snd yb = (rewrite prf in a))) +IsFixpoint _ yb = Void + +isFixpointUnique : (a : Ty tyCtx ()) -> IsFixpoint a xb -> IsFixpoint a yc -> xb = yc +isFixpointUnique TNat {xb = (_ ** _), yc = (_ ** _)} (Refl, Refl) (Refl, Refl) = Refl +isFixpointUnique (TFix x a) {xb = (x ** a), yc = (x ** a)} (Refl ** Refl) (Refl ** Refl) = Refl + +isFixpoint : Ty tyCtx () -> Maybe (x ** Ty (tyCtx :< (x :- ())) ()) +isFixpoint TNat = Just ("X" ** TSum [<("Z" :- TProd [<]), ("S" :- TVar (%% "X"))]) +isFixpoint (TFix x a) = Just (x ** a) +isFixpoint _ = Nothing + +reflectIsFixpoint : (a : Ty tyCtx ()) -> IsFixpoint a `OnlyWhen` isFixpoint a +reflectIsFixpoint (TVar i) = RNothing (\_, x => x) +reflectIsFixpoint TNat = RJust (Refl, Refl) +reflectIsFixpoint (TArrow a b) = RNothing (\_, x => x) +reflectIsFixpoint (TProd as) = RNothing (\_, x => x) +reflectIsFixpoint (TSum as) = RNothing (\_, x => x) +reflectIsFixpoint (TFix x a) = RJust (Refl ** Refl) + +-- Test if we have a function, collecting the bound types ---------------------- + +IsFunction : + {tyCtx : Context ()} -> + (bound : Context ()) -> (fun : Ty tyCtx ()) -> + (dom : All (const $ Ty tyCtx ()) bound) -> (cod : Ty tyCtx ()) -> + Type +IsFunction [<] fun dom cod = (dom = [<], cod = fun) +IsFunction (bound :< (x :- ())) fun dom cod = + ( b ** c ** + ( IsArrow fun b c + , ( dom' ** + ( dom = dom' :< (x :- b) + , IsFunction bound c dom' cod + )) + )) + + +isFunctionUnique : + (bound : Context ()) -> (a : Ty tyCtx ()) -> + forall dom1, dom2, cod1, cod2. + IsFunction bound a dom1 cod1 -> IsFunction bound a dom2 cod2 -> (dom1 = dom2, cod1 = cod2) +isFunctionUnique [<] a (Refl, Refl) (Refl, Refl) = (Refl, Refl) +isFunctionUnique (bound :< (x :- ())) a + (b1 ** c1 ** (isArrow1, (dom1' ** (Refl, isFunc1)))) + (b2 ** c2 ** (isArrow2, (dom2' ** (Refl, isFunc2)))) + with (isArrowUnique a isArrow1 isArrow2) + isFunctionUnique (bound :< (x :- ())) a + (b ** c ** (_, (dom1' ** (Refl, isFunc1)))) + (b ** c ** (_, (dom2' ** (Refl, isFunc2)))) + | (Refl, Refl) + with (isFunctionUnique bound c isFunc1 isFunc2) + isFunctionUnique (bound :< (x :- ())) a + (b ** c ** (_, (dom' ** (Refl, _)))) + (b ** c ** (_, (dom' ** (Refl, _)))) + | (Refl, Refl) | (Refl, Refl) = (Refl, Refl) + +isFunction : + (bound : Context ()) -> Ty tyCtx () -> + Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ()) +isFunction [<] a = Just ([<], a) +isFunction (bound :< (x :- ())) a = do + (b, c) <- isArrow a + (dom, cod) <- isFunction bound c + Just (dom :< (x :- b), cod) + +reflectIsFunction : + (bound : Context ()) -> (a : Ty tyCtx ()) -> + uncurry (IsFunction bound a) `OnlyWhen` isFunction bound a +reflectIsFunction [<] a = RJust (Refl, Refl) +reflectIsFunction (bound :< (x :- ())) a with (reflectIsArrow a) | (isArrow a) + _ | RJust isArrow | Just (b, c) with (reflectIsFunction bound c) | (isFunction bound c) + _ | RJust isFunc | Just (dom, cod) = RJust (b ** c ** (isArrow , (dom ** (Refl, isFunc)))) + _ | RNothing notFunc | _ = + RNothing (\(dom :< (x :- b'), cod), (b' ** c' ** (isArrow', (dom ** (Refl, isFunc)))) => + let (eq1, eq2) = isArrowUnique a {b, c, d = b', e = c'} isArrow isArrow' in + let isFunc = rewrite eq2 in isFunc in + notFunc (dom, cod) isFunc) + _ | RNothing notArrow | _ = + RNothing (\(dom, cod), (b ** c ** (isArrow, _)) => notArrow (b, c) isArrow) + +-- Full type checking and synthesis -------------------------------------------- + Synths : - {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> - SynthTerm ty tm -> Ty ty -> Type + {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> + SynthTerm tyCtx tmCtx -> Ty tyCtx () -> Type Checks : - {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> - Ty ty -> CheckTerm ty tm -> Type + {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> + Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Type CheckSpine : - {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> - (fun : Ty ty) -> List (CheckTerm ty tm) -> (res : Ty ty) -> Type -CheckSpine1 : - {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> - (fun : Ty ty) -> List1 (CheckTerm ty tm) -> (res : Ty ty) -> Type -AllCheck : {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> List (CheckTerm ty tm) -> Type + {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> + (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty tyCtx ()) -> Type +AllCheck : + {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> + Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Type AllCheckBinding : - {ty, tm : Nat} -> (ctx : Vect tm (Ty ty)) -> List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Type - -Synths ctx (Var i) a = (a = index i ctx) -Synths ctx (Lit k) a = (a = TNat) -Synths ctx (Suc t) a = (Checks ctx TNat t, a = TNat) -Synths ctx (App e ts) a = + {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> + Row (Ty tyCtx ()) -> Ty tyCtx () -> + Context (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> + Type + +Synths env (Var i) a = (a = indexAll i env) +Synths env (Lit k) a = (a = TNat) +Synths env (Suc t) a = (Checks env TNat t, a = TNat) +Synths env (App e ts) a = ( fun ** - ( Synths ctx e fun - , CheckSpine1 ctx fun ts a + ( Synths env e fun + , CheckSpine env fun ts a )) -Synths ctx (Prj e k) a = +Synths env (Prj e x) a = ( b ** - ( Synths ctx e b + ( Synths env e b , ( as ** - ( CanProject b as - , GetAt k as a + ( IsProduct b as + , GetAt x as a )) )) -Synths ctx (Expand e) a = +Synths env (Expand e) a = ( b ** - ( Synths ctx e b - , ( c ** - ( IsFixpoint b c - , a = sub (Base Id :< b) c)) + ( Synths env e b + , ( xc ** + ( IsFixpoint b xc + , a = sub (Base Id :< (fst xc :- b)) (snd xc) + )) )) -Synths ctx (Annot t a) b = +Synths env (Annot t a) b = ( Not (IllFormed a) - , Checks ctx a t + , Checks env a t , a = b ) -Checks ctx a (Let e t) = +Checks env a (Let x e t) = ( b ** - ( Synths ctx e b - , Checks (b :: ctx) a t + ( Synths env e b + , Checks (env :< (x :- b)) a t )) -Checks ctx a (Abs k t) = - ( as : Vect (S k) _ ** b ** - ( IsArrow (S k) a as b - , Checks (as ++ ctx) b t +Checks env a (Abs bound t) = + ( as ** b ** + ( IsFunction bound a as b + , Checks (env ++ as) b t )) -Checks ctx a (Inj k t) = +Checks env a (Inj x t) = ( as ** - ( CanInject a as + ( IsSum a as , ( b ** - ( GetAt k as b - , Checks ctx b t + ( GetAt x as b + , Checks env b t )) )) -Checks ctx a (Tup ts) = +Checks env a (Tup ts) = ( as ** ( IsProduct a as - , AllCheck ctx as ts + , AllCheck env as ts )) -Checks ctx a (Case e ts) = +Checks env a (Case e ts) = ( b ** - ( Synths ctx e b + ( Synths env e b , ( as ** ( IsSum b as - , AllCheckBinding ctx as a ts + , AllCheckBinding env as a ts )) )) -Checks ctx a (Contract t) = - ( b ** - ( IsFixpoint a b - , Checks ctx (sub (Base Id :< a) b) t +Checks env a (Contract t) = + ( xb ** + ( IsFixpoint a xb + , Checks env (sub (Base Id :< (fst xb :- a)) (snd xb)) t )) -Checks ctx a (Fold e t) = +Checks env a (Fold e x t) = ( b ** - ( Synths ctx e b - , ( c ** - ( IsFixpoint b c - , Checks (sub (Base Id :< a) c :: ctx) a t + ( Synths env e b + , ( yc ** + ( IsFixpoint b yc + , Checks (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t )) )) -Checks ctx a (Embed e) = Synths ctx e a - -CheckSpine ctx fun [] res = fun = res -CheckSpine ctx fun (t :: ts) res = - ( a ** b ** - ( IsArrow 1 fun [a] b - , Checks ctx a t - , CheckSpine ctx b ts res +Checks env a (Embed e) = + ( b ** + ( Synths env e b + , a `Eq` b )) -CheckSpine1 ctx fun (t ::: ts) res = +CheckSpine env fun [] res = fun = res +CheckSpine env fun (t :: ts) res = ( a ** b ** - ( IsArrow 1 fun [a] b - , Checks ctx a t - , CheckSpine ctx b ts res + ( IsArrow fun a b + , Checks env a t + , CheckSpine env b ts res )) -AllCheck ctx [] [] = () -AllCheck ctx [] (t :: ts) = Void -AllCheck ctx (a :: as) [] = Void -AllCheck ctx (a :: as) (t :: ts) = (Checks ctx a t, AllCheck ctx as ts) +AllCheck env as [<] = (as = [<]) +AllCheck env as (ts :< (x :- t)) = + ( a ** bs ** + ( Remove x as a bs + , Checks env a t + , AllCheck env bs ts + )) -AllCheckBinding ctx [] b [] = () -AllCheckBinding ctx [] b (t :: ts) = Void -AllCheckBinding ctx (a :: as) b [] = Void -AllCheckBinding ctx (a :: as) b (t :: ts) = (Checks (a :: ctx) b t, AllCheckBinding ctx as b ts) +AllCheckBinding env as a [<] = (as = [<]) +AllCheckBinding env as a (ts :< (x :- (y ** t))) = + ( b ** bs ** + ( Remove x as b bs + , Checks (env :< (y :- b)) a t + , AllCheckBinding env bs a ts + )) --- Uniqueness +-- Reordering -getAtUnique : - (n : Nat) -> (xs : List a) -> - GetAt n xs x -> GetAt n xs y -> x = y -getAtUnique 0 (x :: xs) (Here ** prf1) (Here ** prf2) = Refl -getAtUnique (S k) (x :: xs) (There n1 ** prf1) (There n2 ** prf2) = getAtUnique k xs (n1 ** injective prf1) (n2 ** injective prf2) -getAtUnique _ [] (n1 ** prf1) (n2 ** prf2) impossible - -canProjectUnique : (a : Ty ty) -> CanProject a as -> CanProject a bs -> as = bs -canProjectUnique (TUnion as) Refl Refl = Refl -canProjectUnique (TProd as) Refl Refl = Refl - -canInjectUnique : (a : Ty ty) -> CanInject a as -> CanInject a bs -> as = bs -canInjectUnique (TUnion as) Refl Refl = Refl -canInjectUnique (TSum as) Refl Refl = Refl - -isFixpointUnique : (a : Ty ty) -> IsFixpoint a b -> IsFixpoint a c -> b = c -isFixpointUnique TNat Refl Refl = Refl -isFixpointUnique (TFix a) Refl Refl = Refl - -isArrowUnique : - (k : Nat) -> (a : Ty ty) -> - forall bs, b, cs, c. IsArrow k a bs b -> IsArrow k a cs c -> (bs = cs, b = c) -isArrowUnique 0 a (Refl, Refl) (Refl, Refl) = (Refl, Refl) -isArrowUnique (S k) (TArrow dom cod) (as ** (Refl, prf1)) (bs ** (Refl, prf2)) = - let (eq1, eq2) = isArrowUnique k cod prf1 prf2 in - (cong (dom ::) eq1, eq2) - -isProductUnique : (a : Ty ty) -> IsProduct a as -> IsProduct a bs -> as = bs -isProductUnique (TProd as) Refl Refl = Refl +allCheckReorder : + as <~> bs -> (ts : Context (CheckTerm tyCtx tmCtx)) -> + AllCheck env as ts -> AllCheck env bs ts +allCheckReorder [] [<] Refl = Refl +allCheckReorder (_ :: _) [<] Refl impossible +allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) = + (a ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3)) -isSumUnique : (a : Ty ty) -> IsSum a as -> IsSum a bs -> as = bs -isSumUnique (TSum as) Refl Refl = Refl +allCheckBindingReorder : + as <~> bs -> (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> + AllCheckBinding env as a ts -> AllCheckBinding env bs a ts +allCheckBindingReorder [] [<] Refl = Refl +allCheckBindingReorder (_ :: _) [<] Refl impossible +allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3)) = + (b ** bs ** (Evidence prf1.fst (trans (sym prf) prf1.snd), prf2, prf3)) +-- Uniqueness synthsUnique : - (0 ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) -> - Synths ctx e a -> Synths ctx e b -> a = b + (0 env : All (const $ Ty tyCtx ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) -> + Synths env e a -> Synths env e b -> a = b checkSpineUnique : - (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) -> - CheckSpine ctx a ts b -> CheckSpine ctx a ts c -> b = c -checkSpine1Unique : - (0 ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) -> - CheckSpine1 ctx a ts b -> CheckSpine1 ctx a ts c -> b = c - -synthsUnique ctx (Var i) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique ctx (Lit k) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique ctx (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2) -synthsUnique ctx (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22)) - with (synthsUnique ctx e prf11 prf21) - synthsUnique ctx (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl = - checkSpine1Unique ctx fun ts prf12 prf22 -synthsUnique ctx (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique ctx e prf11 prf21) - synthsUnique ctx (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl - with (canProjectUnique a prf11 prf21) - synthsUnique ctx (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl = + (0 env : All (const $ Ty tyCtx ()) tmCtx) -> + (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> + CheckSpine env fun ts a -> CheckSpine env fun ts b -> a = b + +synthsUnique env (Var i) prf1 prf2 = trans prf1 (sym prf2) +synthsUnique env (Lit k) prf1 prf2 = trans prf1 (sym prf2) +synthsUnique env (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2) +synthsUnique env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22)) + with (synthsUnique env e prf11 prf21) + synthsUnique env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl = + checkSpineUnique env fun ts prf12 prf22 +synthsUnique env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22)) + with (synthsUnique env e prf11 prf21) + synthsUnique env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl + with (isProductUnique a prf11 prf21) + synthsUnique env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl = getAtUnique k as prf1 prf2 -synthsUnique ctx (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique ctx e prf11 prf21) - synthsUnique ctx (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl +synthsUnique env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22)) + with (synthsUnique env e prf11 prf21) + synthsUnique env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl with (isFixpointUnique a prf11 prf21) - synthsUnique ctx (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl = + synthsUnique env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl = trans prf1 (sym prf2) -synthsUnique ctx (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2) - -checkSpineUnique ctx a [] prf1 prf2 = trans (sym prf1) prf2 -checkSpineUnique ctx a (t :: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22)) - with (isArrowUnique 1 a prf11 prf21) - checkSpineUnique ctx a (t :: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) = - checkSpineUnique ctx c ts prf1 prf2 - -checkSpine1Unique ctx a (t ::: ts) (b ** c ** (prf11, _ , prf12)) (d ** e ** (prf21, _ , prf22)) - with (isArrowUnique 1 a prf11 prf21) - checkSpine1Unique ctx a (t ::: ts) (b ** c ** (_, _ , prf1)) (b ** c ** (_, _ , prf2)) | (Refl, Refl) = - checkSpineUnique ctx c ts prf1 prf2 - --- Decidable ------------------------------------------------------------------- - -canProject : Ty ty -> Maybe (List (Ty ty)) -canProject (TUnion as) = Just (forget as) -canProject (TProd as) = Just as -canProject _ = Nothing - -canInject : Ty ty -> Maybe (List (Ty ty)) -canInject (TUnion as) = Just (forget as) -canInject (TSum as) = Just as -canInject _ = Nothing - -isFixpoint : Ty ty -> Maybe (Ty (S ty)) -isFixpoint TNat = Just (TSum [TProd [], TVar FZ]) -isFixpoint (TFix a) = Just a -isFixpoint _ = Nothing - -isArrow : (k : Nat) -> Ty ty -> Maybe (Vect k (Ty ty), Ty ty) -isArrow 0 a = Just ([], a) -isArrow (S k) (TArrow a b) = do - (as, c) <- isArrow k b - Just (a :: as, c) -isArrow (S k) _ = Nothing +synthsUnique env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2) -isProduct : Ty ty -> Maybe (List (Ty ty)) -isProduct (TProd as) = Just as -isProduct _ = Nothing +checkSpineUnique env fun [] prf1 prf2 = trans (sym prf1) prf2 +checkSpineUnique env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22)) + with (isArrowUnique fun prf11 prf21) + checkSpineUnique env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) = + checkSpineUnique env b ts prf1 prf2 -isSum : Ty ty -> Maybe (List (Ty ty)) -isSum (TSum as) = Just as -isSum _ = Nothing +-- Decision synths : - (ctx : Vect tm (Ty ty)) -> - SynthTerm ty tm -> Maybe (Ty ty) + (env : All (const (Ty tyCtx ())) tmCtx) -> + SynthTerm tyCtx tmCtx -> Maybe (Ty tyCtx ()) checks : - (ctx : Vect tm (Ty ty)) -> - Ty ty -> CheckTerm ty tm -> Bool + (env : All (const (Ty tyCtx ())) tmCtx) -> + Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Bool checkSpine : - (ctx : Vect tm (Ty ty)) -> - Ty ty -> List (CheckTerm ty tm) -> Maybe (Ty ty) -checkSpine1 : - (ctx : Vect tm (Ty ty)) -> - Ty ty -> List1 (CheckTerm ty tm) -> Maybe (Ty ty) + (env : All (const (Ty tyCtx ())) tmCtx) -> + (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty tyCtx ()) allCheck : - (ctx : Vect tm (Ty ty)) -> - List (Ty ty) -> List (CheckTerm ty tm) -> Bool + (env : All (const (Ty tyCtx ())) tmCtx) -> + Row (Ty tyCtx ()) -> Context (CheckTerm tyCtx tmCtx) -> Bool allCheckBinding : - (ctx : Vect tm (Ty ty)) -> - List (Ty ty) -> Ty ty -> List (CheckTerm ty (S tm)) -> Bool - -synths ctx (Var i) = Just (index i ctx) -synths ctx (Lit k) = Just TNat -synths ctx (Suc t) = do - guard (checks ctx TNat t) + (env : All (const (Ty tyCtx ())) tmCtx) -> + Row (Ty tyCtx ()) -> Ty tyCtx () -> + Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> + Bool + +synths env (Var i) = Just (indexAll i env) +synths env (Lit k) = Just TNat +synths env (Suc t) = do + guard (checks env TNat t) Just TNat -synths ctx (App e ts) = do - a <- synths ctx e - checkSpine1 ctx a ts -synths ctx (Prj e k) = do - a <- synths ctx e - as <- canProject a +synths env (App e ts) = do + a <- synths env e + checkSpine env a ts +synths env (Prj e k) = do + a <- synths env e + as <- isProduct a getAt k as -synths ctx (Expand e) = do - a <- synths ctx e - b <- isFixpoint a - Just (sub (Base Id :< a) b) -synths ctx (Annot t a) = do +synths env (Expand e) = do + a <- synths env e + (x ** b) <- isFixpoint a + Just (sub (Base Id :< (x :- a)) b) +synths env (Annot t a) = do guard (not $ illFormed a) - guard (checks ctx a t) + guard (checks env a t) Just a -checks ctx a (Let e t) = - case synths ctx e of - Just b => checks (b :: ctx) a t +checks env a (Let x e t) = + case synths env e of + Just b => checks (env :< (x :- b)) a t Nothing => False -checks ctx a (Abs k t) = - case isArrow (S k) a of - Just (as, b) => checks (as ++ ctx) b t +checks env a (Abs bound t) = + case isFunction bound a of + Just (dom, cod) => checks (env ++ dom) cod t Nothing => False -checks ctx a (Inj k t) = - case canInject a of +checks env a (Inj k t) = + case isSum a of Just as => case getAt k as of - Just b => checks ctx b t + Just b => checks env b t Nothing => False Nothing => False -checks ctx a (Tup ts) = +checks env a (Tup ts) = case isProduct a of - Just as => allCheck ctx as ts + Just as => allCheck env as ts Nothing => False -checks ctx a (Case e ts) = - case synths ctx e of +checks env a (Case e ts) = + case synths env e of Just b => case isSum b of - Just as => allCheckBinding ctx as a ts + Just as => allCheckBinding env as a ts Nothing => False Nothing => False -checks ctx a (Contract t) = +checks env a (Contract t) = case isFixpoint a of - Just b => checks ctx (sub (Base Id :< a) b) t + Just (x ** b) => checks env (sub (Base Id :< (x :- a)) b) t Nothing => False -checks ctx a (Fold e t) = - case synths ctx e of +checks env a (Fold e x t) = + case synths env e of Just b => case isFixpoint b of - Just c => checks (sub (Base Id :< a) c :: ctx) a t + Just (y ** c) => checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t Nothing => False Nothing => False -checks ctx a (Embed e) = - case synths ctx e of +checks env a (Embed e) = + case synths env e of Just b => a == b Nothing => False -checkSpine ctx a [] = Just a -checkSpine ctx a (t :: ts) = do - ([dom], cod) <- isArrow 1 a - guard (checks ctx dom t) - checkSpine ctx cod ts +checkSpine env a [] = Just a +checkSpine env a (t :: ts) = do + (dom, cod) <- isArrow a + guard (checks env dom t) + checkSpine env cod ts -checkSpine1 ctx a (t ::: ts) = do - ([dom], cod) <- isArrow 1 a - guard (checks ctx dom t) - checkSpine ctx cod ts - -allCheck ctx [] [] = True -allCheck ctx [] (t :: ts) = False -allCheck ctx (a :: as) [] = False -allCheck ctx (a :: as) (t :: ts) = checks ctx a t && allCheck ctx as ts +allCheck env as [<] = null as +allCheck env as (ts :< (x :- t)) = + case remove' x as of + Just (a, bs) => checks env a t && allCheck env bs ts + Nothing => False -allCheckBinding ctx [] b [] = True -allCheckBinding ctx [] b (t :: ts) = False -allCheckBinding ctx (a :: as) b [] = False -allCheckBinding ctx (a :: as) b (t :: ts) = checks (a :: ctx) b t && allCheckBinding ctx as b ts +allCheckBinding env as a [<] = null as +allCheckBinding env as a (ts :< (x :- (y ** t))) = + case remove' x as of + Just (b, bs) => checks (env :< (y :- b)) a t && allCheckBinding env bs a ts + Nothing => False -- Proof -reflectGetAt : (k : Nat) -> (xs : List a) -> GetAt k xs `OnlyWhen` getAt k xs -reflectGetAt k [] = RNothing (\_, (n ** prf) => absurd n) -reflectGetAt 0 (x :: xs) = RJust (Here ** Refl) -reflectGetAt (S k) (x :: xs) with (reflectGetAt k xs) | (getAt k xs) - _ | RJust (n ** prf) | _ = RJust (There n ** cong S prf) - _ | RNothing not | _ = RNothing (\x => \case (There n ** prf) => not x (n ** injective prf)) - -reflectCanProject : (a : Ty ty) -> CanProject a `OnlyWhen` canProject a -reflectCanProject (TVar i) = RNothing (\x, y => y) -reflectCanProject TNat = RNothing (\x, y => y) -reflectCanProject (TArrow a b) = RNothing (\x, y => y) -reflectCanProject (TUnion as) = RJust Refl -reflectCanProject (TProd as) = RJust Refl -reflectCanProject (TSum as) = RNothing (\x, y => y) -reflectCanProject (TFix a) = RNothing (\x, y => y) - -reflectCanInject : (a : Ty ty) -> CanInject a `OnlyWhen` canInject a -reflectCanInject (TVar i) = RNothing (\x, y => y) -reflectCanInject TNat = RNothing (\x, y => y) -reflectCanInject (TArrow a b) = RNothing (\x, y => y) -reflectCanInject (TUnion as) = RJust Refl -reflectCanInject (TProd as) = RNothing (\x, y => y) -reflectCanInject (TSum as) = RJust Refl -reflectCanInject (TFix a) = RNothing (\x, y => y) - -reflectIsFixpoint : (a : Ty ty) -> IsFixpoint a `OnlyWhen` isFixpoint a -reflectIsFixpoint (TVar i) = RNothing (\x, y => y) -reflectIsFixpoint TNat = RJust Refl -reflectIsFixpoint (TArrow a b) = RNothing (\x, y => y) -reflectIsFixpoint (TUnion as) = RNothing (\x, y => y) -reflectIsFixpoint (TProd as) = RNothing (\x, y => y) -reflectIsFixpoint (TSum as) = RNothing (\x, y => y) -reflectIsFixpoint (TFix a) = RJust Refl - -reflectIsArrow : (k : Nat) -> (a : Ty ty) -> uncurry (IsArrow k a) `OnlyWhen` isArrow k a -reflectIsArrow 0 a = RJust (Refl, Refl) -reflectIsArrow (S k) (TVar i) = RNothing (\(_, _), x => x) -reflectIsArrow (S k) TNat = RNothing (\(_, _), x => x) -reflectIsArrow (S k) (TArrow a b) with (reflectIsArrow k b) | (isArrow k b) - _ | RJust arrow | Just (as, c) = RJust (as ** (Refl, arrow)) - _ | RNothing notArrow | _ = RNothing (\(a :: as, c), (as ** (Refl, prf)) => notArrow (as, c) prf) -reflectIsArrow (S k) (TUnion as) = RNothing (\(_, _), x => x) -reflectIsArrow (S k) (TProd as) = RNothing (\(_, _), x => x) -reflectIsArrow (S k) (TSum as) = RNothing (\(_, _), x => x) -reflectIsArrow (S k) (TFix a) = RNothing (\(_, _), x => x) - -reflectIsProduct : (a : Ty ty) -> IsProduct a `OnlyWhen` isProduct a -reflectIsProduct (TVar i) = RNothing (\x, y => y) -reflectIsProduct TNat = RNothing (\x, y => y) -reflectIsProduct (TArrow a b) = RNothing (\x, y => y) -reflectIsProduct (TUnion as) = RNothing (\x, y => y) -reflectIsProduct (TProd as) = RJust Refl -reflectIsProduct (TSum as) = RNothing (\x, y => y) -reflectIsProduct (TFix a) = RNothing (\x, y => y) - -reflectIsSum : (a : Ty ty) -> IsSum a `OnlyWhen` isSum a -reflectIsSum (TVar i) = RNothing (\x, y => y) -reflectIsSum TNat = RNothing (\x, y => y) -reflectIsSum (TArrow a b) = RNothing (\x, y => y) -reflectIsSum (TUnion as) = RNothing (\x, y => y) -reflectIsSum (TProd as) = RNothing (\x, y => y) -reflectIsSum (TSum as) = RJust Refl -reflectIsSum (TFix a) = RNothing (\x, y => y) - -- FIXME: these are total; the termination checker is unreasonably slow. partial -reflectSynths : - (ctx : Vect tm (Ty ty)) -> (e : SynthTerm ty tm) -> - Synths ctx e `OnlyWhen` synths ctx e -partial -reflectChecks : - (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (t : CheckTerm ty tm) -> - Checks ctx a t `Reflects` checks ctx a t +0 reflectSynths : + (env : All (const $ Ty tyCtx ()) tmCtx) -> + (e : SynthTerm tyCtx tmCtx) -> + Synths env e `OnlyWhen` synths env e partial -reflectCheckSpine : - (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty tm)) -> - CheckSpine ctx a ts `OnlyWhen` checkSpine ctx a ts +0 reflectChecks : + (env : All (const $ Ty tyCtx ()) tmCtx) -> + (a : Ty tyCtx ()) -> (t : CheckTerm tyCtx tmCtx) -> + Checks env a t `Reflects` checks env a t partial -reflectCheckSpine1 : - (ctx : Vect tm (Ty ty)) -> (a : Ty ty) -> (ts : List1 (CheckTerm ty tm)) -> - CheckSpine1 ctx a ts `OnlyWhen` checkSpine1 ctx a ts +0 reflectCheckSpine : + (env : All (const $ Ty tyCtx ()) tmCtx) -> + (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> + CheckSpine env fun ts `OnlyWhen` checkSpine env fun ts partial -reflectAllCheck : - (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (ts : List (CheckTerm ty tm)) -> - AllCheck ctx as ts `Reflects` allCheck ctx as ts +0 reflectAllCheck : + (env : All (const $ Ty tyCtx ()) tmCtx) -> + (as : Row (Ty tyCtx ())) -> (ts : Context (CheckTerm tyCtx tmCtx)) -> + AllCheck env as ts `Reflects` allCheck env as ts partial -reflectAllCheckBinding : - (ctx : Vect tm (Ty ty)) -> (as : List (Ty ty)) -> (a : Ty ty) -> (ts : List (CheckTerm ty (S tm))) -> - AllCheckBinding ctx as a ts `Reflects` allCheckBinding ctx as a ts - -reflectSynths ctx (Var i) = RJust Refl -reflectSynths ctx (Lit k) = RJust Refl -reflectSynths ctx (Suc t) with (reflectChecks ctx TNat t) | (checks ctx TNat t) +0 reflectAllCheckBinding : + (env : All (const $ Ty tyCtx ()) tmCtx) -> + (as : Row (Ty tyCtx ())) -> (a : Ty tyCtx ()) -> + (ts : Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> + AllCheckBinding env as a ts `Reflects` allCheckBinding env as a ts + +reflectSynths env (Var i) = RJust Refl +reflectSynths env (Lit k) = RJust Refl +reflectSynths env (Suc t) with (reflectChecks env TNat t) | (checks env TNat t) _ | RTrue tNat | _ = RJust (tNat, Refl) _ | RFalse tNotNat | _ = RNothing (\_, (tNat, _) => tNotNat tNat) -reflectSynths ctx (App e ts) with (reflectSynths ctx e) | (synths ctx e) - _ | RJust eTy | Just a with (reflectCheckSpine1 ctx a ts) | (checkSpine1 ctx a ts) +reflectSynths env (App e ts) with (reflectSynths env e) | (synths env e) + _ | RJust eTy | Just a with (reflectCheckSpine env a ts) | (checkSpine env a ts) _ | RJust tsSpine | Just b = RJust (a ** (eTy, tsSpine)) _ | RNothing tsBad | _ = RNothing (\c, (b ** (eTy', tsSpine)) => - let tsSpine = rewrite synthsUnique ctx e {a, b} eTy eTy' in tsSpine in + let tsSpine = rewrite synthsUnique env e {a, b} eTy eTy' in tsSpine in tsBad c tsSpine) _ | RNothing eBad | _ = RNothing (\c, (b ** (eTy, _)) => eBad b eTy) -reflectSynths ctx (Prj e k) with (reflectSynths ctx e) | (synths ctx e) - _ | RJust eTy | Just a with (reflectCanProject a) | (canProject a) - _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as) +reflectSynths env (Prj e x) with (reflectSynths env e) | (synths env e) + _ | RJust eTy | Just a with (reflectIsProduct a) | (isProduct a) + _ | RJust prf | Just as with (reflectGetAt x as) | (getAt x as) _ | RJust got | Just b = RJust (a ** (eTy, (as ** (prf, got)))) _ | RNothing not | _ = RNothing (\x, (a' ** (eTy', (as' ** (prf', got)))) => - let prf' = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf' in - let got = rewrite canProjectUnique a {as, bs = as'} prf prf' in got in + let prf' = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf' in + let got = rewrite isProductUnique a {as, bs = as'} prf prf' in got in not x got) _ | RNothing nprf | _ = RNothing (\x, (a' ** (eTy', (as' ** (prf, _)))) => - let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in + let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in nprf as' prf) _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy) -reflectSynths ctx (Expand e) with (reflectSynths ctx e) | (synths ctx e) +reflectSynths env (Expand e) with (reflectSynths env e) | (synths env e) _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a) - _ | RJust prf | Just b = RJust (a ** (eTy, (b ** (prf, Refl)))) + _ | RJust prf | Just (x ** b) = RJust (a ** (eTy, ((x ** b) ** (prf, Refl)))) _ | RNothing nprf | _ = RNothing (\x, (a' ** (eTy', (b ** (prf, eq)))) => - let prf = rewrite synthsUnique ctx e {a, b = a'} eTy eTy' in prf in + let prf = rewrite synthsUnique env e {a, b = a'} eTy eTy' in prf in nprf b prf) _ | RNothing eBad | _ = RNothing (\x, (a ** (eTy, _)) => eBad a eTy) -reflectSynths ctx (Annot t a) with (reflectIllFormed a) | (illFormed a) - _ | RFalse wf | _ with (reflectChecks ctx a t) | (checks ctx a t) +reflectSynths env (Annot t a) with (reflectIllFormed a) | (illFormed a) + _ | RFalse wf | _ with (reflectChecks env a t) | (checks env a t) _ | RTrue tTy | _ = RJust (wf, tTy, Refl) _ | RFalse tBad | _ = RNothing (\x, (_, tTy, Refl) => tBad tTy) _ | RTrue notWf | _ = RNothing (\x, (wf, _) => wf notWf) -reflectChecks ctx a (Let e t) with (reflectSynths ctx e) | (synths ctx e) - _ | RJust eTy | Just b with (reflectChecks (b :: ctx) a t) | (checks (b :: ctx) a t) +reflectChecks env a (Let x e t) with (reflectSynths env e) | (synths env e) + _ | RJust eTy | Just b with (reflectChecks (env :< (x :- b)) a t) | (checks (env :< (x :- b)) a t) _ | RTrue tTy | _ = RTrue (b ** (eTy, tTy)) _ | RFalse tBad | _ = RFalse (\(b' ** (eTy', tTy)) => - let tTy = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in tTy in + let tTy = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in tTy in tBad tTy) _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks ctx a (Abs k t) with (reflectIsArrow (S k) a) | (isArrow (S k) a) - _ | RJust prf | Just (as, b) with (reflectChecks (as ++ ctx) b t) | (checks (as ++ ctx) b t) +reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a) + _ | RJust prf | Just (as, b) with (reflectChecks (env ++ as) b t) | (checks (env ++ as) b t) _ | RTrue tTy | _ = RTrue (as ** b ** (prf, tTy)) _ | RFalse tBad | _ = RFalse (\(as' ** b' ** (prf', tTy)) => let - tTy = - rewrite fst $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in - rewrite snd $ isArrowUnique (S k) a {bs = as, b, cs = as', c = b'} prf prf' in - tTy + (eq1, eq2) = + isFunctionUnique bound a + {dom1 = as, cod1 = b, dom2 = as', cod2 = b'} + prf prf' + tTy = rewrite eq1 in rewrite eq2 in tTy in tBad tTy) _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf) -reflectChecks ctx a (Inj k t) with (reflectCanInject a) | (canInject a) +reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a) _ | RJust prf | Just as with (reflectGetAt k as) | (getAt k as) - _ | RJust got | Just b with (reflectChecks ctx b t) | (checks ctx b t) + _ | RJust got | Just b with (reflectChecks env b t) | (checks env b t) _ | RTrue tTy | _ = RTrue (as ** (prf, (b ** (got, tTy)))) _ | RFalse tBad | _ = RFalse (\(as' ** (prf', (b' ** (got', tTy)))) => - let got' = rewrite canInjectUnique a {as, bs = as'} prf prf' in got' in - let tTy = rewrite getAtUnique k as {x = b, y = b'} got got' in tTy in - tBad tTy) + let got' = rewrite isSumUnique a {as, bs = as'} prf prf' in got' in + let tTy = rewrite getAtUnique k as {y = b, z = b'} got got' in tTy in + tBad tTy + ) _ | RNothing not | _ = RFalse (\(as' ** (prf', (b ** (got, _)))) => - let got = rewrite canInjectUnique a {as, bs = as'} prf prf' in got in + let got = rewrite isSumUnique a {as, bs = as'} prf prf' in got in not b got) _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf) -reflectChecks ctx a (Tup ts) with (reflectIsProduct a) | (isProduct a) - _ | RJust prf | Just as with (reflectAllCheck ctx as ts) | (allCheck ctx as ts) +reflectChecks env a (Tup ts) with (reflectIsProduct a) | (isProduct a) + _ | RJust prf | Just as with (reflectAllCheck env as ts) | (allCheck env as ts) _ | RTrue tsTy | _ = RTrue (as ** (prf, tsTy)) _ | RFalse tsBad | _ = RFalse (\(as' ** (prf', tsTy)) => let tsTy = rewrite isProductUnique a {as, bs = as'} prf prf' in tsTy in tsBad tsTy) _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf) -reflectChecks ctx a (Case e ts) with (reflectSynths ctx e) | (synths ctx e) +reflectChecks env a (Case e ts) with (reflectSynths env e) | (synths env e) _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b) - _ | RJust prf | Just as with (reflectAllCheckBinding ctx as a ts) | (allCheckBinding ctx as a ts) + _ | RJust prf | Just as with (reflectAllCheckBinding env as a ts) | (allCheckBinding env as a ts) _ | RTrue tsTy | _ = RTrue (b ** (eTy, (as ** (prf, tsTy)))) _ | RFalse tsBad | _ = RFalse (\(b' ** (eTy', (as' ** (prf', tsTy)))) => - let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in + let prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf' in let tsTy = rewrite isSumUnique b {as, bs = as'} prf prf' in tsTy in tsBad tsTy) _ | RNothing nprf | _ = RFalse (\(b' ** (eTy', (as ** (prf, _)))) => - let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in + let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in nprf as prf) _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks ctx a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a) - _ | RJust prf | Just b with (reflectChecks ctx (sub (Base Id :< a) b) t) | (checks ctx (sub (Base Id :< a) b) t) - _ | RTrue tTy | _ = RTrue (b ** (prf, tTy)) +reflectChecks env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a) + _ | RJust prf | Just (x ** b) with (reflectChecks env (sub (Base Id :< (x :- a)) b) t) | (checks env (sub (Base Id :< (x :- a)) b) t) + _ | RTrue tTy | _ = RTrue ((x ** b) ** (prf, tTy)) _ | RFalse tBad | _ = RFalse (\(b' ** (prf', tTy)) => - let tTy = rewrite isFixpointUnique a {b, c = b'} prf prf' in tTy in + let + eq = isFixpointUnique a {xb = (x ** b), yc = b'} prf prf' + tTy = + replace {p = \xb => Checks env (sub (Base Id :< (xb.fst :- a)) xb.snd) t} + (sym eq) tTy + in tBad tTy) _ | RNothing nprf | _ = RFalse (\(b ** (prf, _)) => nprf b prf) -reflectChecks ctx a (Fold e t) with (reflectSynths ctx e) | (synths ctx e) +reflectChecks env a (Fold e x t) with (reflectSynths env e) | (synths env e) _ | RJust eTy | Just b with (reflectIsFixpoint b) | (isFixpoint b) - _ | RJust prf | Just c with (reflectChecks ((sub (Base Id :< a) c) :: ctx) a t) | (checks ((sub (Base Id :< a) c) :: ctx) a t) - _ | RTrue tTy | _ = RTrue (b ** (eTy, (c ** (prf, tTy)))) + _ | RJust prf | Just (y ** c) with (reflectChecks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) + _ | RTrue tTy | _ = RTrue (b ** (eTy, ((y ** c) ** (prf, tTy)))) _ | RFalse tBad | _ = RFalse (\(b' ** (eTy', (c' ** (prf', tTy)))) => - let prf' = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf' in - let tTy = rewrite isFixpointUnique b {b = c, c = c'} prf prf' in tTy in + let + prf' = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf' + eq = isFixpointUnique b {xb = (y ** c), yc = c'} prf prf' + tTy = + replace {p = \yc => Checks (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t} + (sym eq) tTy + in tBad tTy) _ | RNothing nprf | _ = RFalse (\(b' ** (eTy', (c ** (prf, _)))) => - let prf = rewrite synthsUnique ctx e {a = b, b = b'} eTy eTy' in prf in + let prf = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in prf in nprf c prf) _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks ctx a (Embed e) with (reflectSynths ctx e) | (synths ctx e) +reflectChecks env a (Embed e) with (reflectSynths env e) | (synths env e) _ | RJust eTy | Just b with (reflectEq a b) | (a == b) - reflectChecks ctx a (Embed e) | RJust eTy | Just .(a) | RTrue Refl | _ = RTrue eTy - _ | RFalse neq | _ = RFalse (\eTy' => neq $ synthsUnique ctx e eTy' eTy) - _ | RNothing eBad | _ = RFalse (\eTy => eBad a eTy) - -reflectCheckSpine ctx a [] = RJust Refl -reflectCheckSpine ctx a (t :: ts) with (reflectIsArrow 1 a) | (isArrow 1 a) - _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t) - _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts) - _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy)) - _ | RNothing tsBad | _ = - RNothing (\d, (_ ** c' ** (prf', _, tsTy)) => - let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in - tsBad d tsTy) - _ | RFalse tBad | _ = - RNothing (\d, (b' ** _ ** (prf', tTy, _)) => - let - tTy = - rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in - tTy - in - tBad tTy) - _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf) + _ | RTrue eq | _ = RTrue (b ** (eTy, eq)) + _ | RFalse neq | _ = + RFalse (\(b' ** (eTy', eq)) => + let eq = rewrite synthsUnique env e {a = b, b = b'} eTy eTy' in eq in + neq eq) + _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectCheckSpine1 ctx a (t ::: ts) with (reflectIsArrow 1 a) | (isArrow 1 a) - _ | RJust prf | Just ([b], c) with (reflectChecks ctx b t) | (checks ctx b t) - _ | RTrue tTy | _ with (reflectCheckSpine ctx c ts) | (checkSpine ctx c ts) +reflectCheckSpine env a [] = RJust Refl +reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a) + _ | RJust prf | Just (b, c) with (reflectChecks env b t) | (checks env b t) + _ | RTrue tTy | _ with (reflectCheckSpine env c ts) | (checkSpine env c ts) _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy)) _ | RNothing tsBad | _ = RNothing (\d, (_ ** c' ** (prf', _, tsTy)) => - let tsTy = rewrite snd $ isArrowUnique 1 a {b = c, c = c'} prf prf' in tsTy in + let (eq1, eq2) = isArrowUnique a {c, e = c'} prf prf' in + let tsTy = rewrite eq2 in tsTy in tsBad d tsTy) _ | RFalse tBad | _ = RNothing (\d, (b' ** _ ** (prf', tTy, _)) => - let - tTy = - rewrite fst $ biinj (::) $ fst $ isArrowUnique 1 a {bs = [b], cs = [b']} prf prf' in - tTy - in + let (eq1, eq2) = isArrowUnique a {b, d = b'} prf prf' in + let tTy = rewrite eq1 in tTy in tBad tTy) - _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf ([b], c) prf) - -reflectAllCheck ctx [] [] = RTrue () -reflectAllCheck ctx [] (t :: ts) = RFalse (\x => x) -reflectAllCheck ctx (a :: as) [] = RFalse (\x => x) -reflectAllCheck ctx (a :: as) (t :: ts) with (reflectChecks ctx a t) | (checks ctx a t) - _ | RTrue tTy | _ with (reflectAllCheck ctx as ts) | (allCheck ctx as ts) - _ | RTrue tsTy | _ = RTrue (tTy, tsTy) - _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy) - _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy) - -reflectAllCheckBinding ctx [] b [] = RTrue () -reflectAllCheckBinding ctx [] b (t :: ts) = RFalse (\x => x) -reflectAllCheckBinding ctx (a :: as) b [] = RFalse (\x => x) -reflectAllCheckBinding ctx (a :: as) b (t :: ts) with (reflectChecks (a :: ctx) b t) | (checks (a :: ctx) b t) - _ | RTrue tTy | _ with (reflectAllCheckBinding ctx as b ts) | (allCheckBinding ctx as b ts) - _ | RTrue tsTy | _ = RTrue (tTy, tsTy) - _ | RFalse tsBad | _ = RFalse (\(_, tsTy) => tsBad tsTy) - _ | RFalse tBad | _ = RFalse (\(tTy, _) => tBad tTy) + _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf (b, c) prf) + +reflectAllCheck env [<] [<] = RTrue Refl +reflectAllCheck env (_ :< _) [<] = RFalse (\case Refl impossible) +reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as) + _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks env a t) (reflectAllCheck env bs ts)) | (checks env a t && allCheck env bs ts) + _ | RTrue checks | _ = RTrue (a ** bs ** (prf, checks)) + _ | RFalse notChecks | _ = + RFalse (\(a' ** bs' ** (prf', checks)) => + let (eq, reorder) = removeUnique x as prf prf' in + notChecks $ + bimap (\x => rewrite eq in x) (allCheckReorder (sym reorder) ts) checks) + _ | RNothing nprf | _ = RFalse (\(a ** bs ** (prf, _)) => nprf (a, bs) prf) + +reflectAllCheckBinding env [<] a [<] = RTrue Refl +reflectAllCheckBinding env (_ :< _) a [<] = RFalse (\case Refl impossible) +reflectAllCheckBinding env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as) + _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks (env :< (y :- b)) a t) (reflectAllCheckBinding env bs a ts)) | (checks (env :< (y :- b)) a t && allCheckBinding env bs a ts) + _ | RTrue checks | _ = RTrue (b ** bs ** (prf, checks)) + _ | RFalse notChecks | _ = + RFalse (\(b' ** bs' ** (prf', checks)) => + let (eq, reorder) = removeUnique x as prf prf' in + notChecks $ + bimap (\x => rewrite eq in x) (allCheckBindingReorder (sym reorder) ts) checks) + _ | RNothing nprf | _ = RFalse (\(b ** bs ** (prf, _)) => nprf (b, bs) prf) diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index e353e50..71028ba 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -1,24 +1,10 @@ module Inky.Term.Pretty -import Data.Fin -import Data.Fin.Extra -import Data.List -import Data.String +import Inky.Context import Inky.Term import Inky.Type.Pretty import Text.PrettyPrint.Prettyprinter -asTmChar : Fin 9 -> Char -asTmChar = index' ['x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f'] - -export -termName : Nat -> String -termName n with (divMod n 9) - termName _ | Fraction _ 9 q r Refl = - strSnoc - (if q == 0 then "" else assert_total (termName $ pred q)) - (asTmChar r) - appPrec, prjPrec, expandPrec, annotPrec, letPrec, absPrec, injPrec, tupPrec, casePrec, contractPrec, foldPrec : Prec appPrec = App @@ -27,29 +13,40 @@ expandPrec = PrefixMinus annotPrec = Equal letPrec = Open absPrec = Open -injPrec = User 8 -tupPrec = User 2 +injPrec = App +tupPrec = Open casePrec = Open contractPrec = PrefixMinus foldPrec = Open export -prettySynth : {ty, tm : Nat} -> SynthTerm ty tm -> Prec -> Doc ann -prettyCheck : {ty, tm : Nat} -> CheckTerm ty tm -> Prec -> Doc ann -prettyAllCheck : {ty, tm : Nat} -> List (CheckTerm ty tm) -> Prec -> List (Doc ann) -prettyAll1Check : {ty, tm : Nat} -> List1 (CheckTerm ty tm) -> Prec -> List (Doc ann) +prettySynth : + {tyCtx, tmCtx : Context ()} -> + SynthTerm tyCtx tmCtx -> Prec -> Doc ann +prettyCheck : + {tyCtx, tmCtx : Context ()} -> + CheckTerm tyCtx tmCtx -> Prec -> Doc ann +prettyAllCheck : + {tyCtx, tmCtx : Context ()} -> + List (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) +prettyCheckCtx : + {tyCtx, tmCtx : Context ()} -> + Context (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) +prettyCheckCtxBinding : + {tyCtx, tmCtx : Context ()} -> + Context (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann) -prettySynth (Var i) d = pretty (termName $ finToNat i) +prettySynth (Var i) d = pretty (unVal $ nameOf i) prettySynth (Lit k) d = pretty k prettySynth (Suc t) d = parenthesise (d >= appPrec) $ group $ align $ hang 2 $ "suc" <+> line <+> prettyCheck t appPrec prettySynth (App e ts) d = parenthesise (d >= appPrec) $ group $ align $ hang 2 $ - concatWith (\x, y => x <+> line <+> y) (prettySynth e appPrec :: prettyAll1Check ts appPrec) -prettySynth (Prj e k) d = + concatWith (surround line) (prettySynth e appPrec :: prettyAllCheck ts appPrec) +prettySynth (Prj e x) d = parenthesise (d > prjPrec) $ group $ align $ hang 2 $ - prettySynth e prjPrec <+> "[" <+> line' <+> pretty k <+> line' <+> "]" + prettySynth e prjPrec <+> "." <+> pretty x prettySynth (Expand e) d = "!" <+> (parenthesise (d > expandPrec) $ group $ align $ hang 2 $ @@ -58,54 +55,56 @@ prettySynth (Annot t a) d = parenthesise (d > annotPrec) $ group $ align $ hang 2 $ prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec -prettyCheck (Let e t) d = +prettyCheck (Let x e t) d = parenthesise (d > letPrec) $ group $ align $ hang 2 $ "let" <++> (group $ align $ hang 2 $ - pretty (termName tm) <++> "=" <+> line <+> prettySynth e letPrec + pretty x <++> "=" <+> line <+> prettySynth e letPrec ) <++> "in" <+> line <+> prettyCheck t letPrec -prettyCheck (Abs k t) d = +prettyCheck (Abs bound t) d = parenthesise (d > absPrec) $ group $ align $ hang 2 $ - "\\" <+> concatWith (\x, y => x <+> "," <++> y) (bindings tm (S k)) <++> "=>" <+> line <+> + "\\" <+> concatWith (surround ",") (bindings bound <>> []) <++> "=>" <+> line <+> prettyCheck t absPrec where - bindings : Nat -> Nat -> List (Doc ann) - bindings tm 0 = [] - bindings tm (S k) = pretty (termName tm) :: bindings (S tm) k + bindings : Context () -> SnocList (Doc ann) + bindings [<] = [<] + bindings (bound :< (x :- ())) = bindings bound :< pretty x prettyCheck (Inj k t) d = parenthesise (d > injPrec) $ group $ align $ hang 2 $ "<" <+> line' <+> pretty k <+> line' <+> ">" <+> prettyCheck t injPrec -prettyCheck (Tup []) d = pretty "()" -prettyCheck (Tup [t]) d = - parens $ group $ align $ hang 2 $ - prettyCheck t tupPrec <+> line <+> "," prettyCheck (Tup ts) d = - parenthesise (d > tupPrec) $ group $ align $ hang 2 $ - concatWith (\x, y => x <+> "," <++> line <+> y) (prettyAllCheck ts tupPrec) + parens $ group $ align $ hang 2 $ + concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec) prettyCheck (Case e ts) d = parenthesise (d > casePrec) $ group $ align $ hang 2 $ "case" <++> prettySynth e casePrec <++> "of" <+> line <+> (braces $ align $ hang 2 $ - concatWith (\x, y => x <+> hardline <+> y) $ - map (\x => - parens $ group $ align $ hang 2 $ - "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> x) $ - prettyAllCheck ts casePrec - ) + concatWith (surround hardline) $ + map parens $ + prettyCheckCtxBinding ts casePrec) prettyCheck (Contract t) d = "~" <+> (parenthesise (d > contractPrec) $ group $ align $ hang 2 $ prettyCheck t contractPrec) -prettyCheck (Fold e t) d = +prettyCheck (Fold e x t) d = parenthesise (d > foldPrec) $ group $ align $ hang 2 $ "fold" <++> prettySynth e foldPrec <++> "by" <+> line <+> (parens $ group $ align $ hang 2 $ - "\\" <+> pretty (termName tm) <++> "=>" <+> line <+> prettyCheck t foldPrec) + "\\" <+> pretty x <++> "=>" <+> line <+> prettyCheck t foldPrec) prettyCheck (Embed e) d = prettySynth e d prettyAllCheck [] d = [] prettyAllCheck (t :: ts) d = prettyCheck t d :: prettyAllCheck ts d -prettyAll1Check (t ::: ts) d = prettyCheck t d :: prettyAllCheck ts d +prettyCheckCtx [<] d = [] +prettyCheckCtx (ts :< (x :- t)) d = + (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyCheck t d) :: + prettyCheckCtx ts d + +prettyCheckCtxBinding [<] d = [] +prettyCheckCtxBinding (ts :< (x :- (y ** t))) d = + (group $ align $ hang 2 $ + "\\" <+> pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) :: + prettyCheckCtxBinding ts d diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr index c3235c0..3d593ae 100644 --- a/src/Inky/Thinning.idr +++ b/src/Inky/Thinning.idr @@ -1,7 +1,9 @@ module Inky.Thinning -import public Data.Fin +import public Inky.Context +import Data.DPair +import Data.Nat import Control.Function -------------------------------------------------------------------------------- @@ -9,24 +11,27 @@ import Control.Function -------------------------------------------------------------------------------- public export -data Thins : Nat -> Nat -> Type where - Id : n `Thins` n - Drop : k `Thins` n -> k `Thins` S n - Keep : k `Thins` n -> S k `Thins` S n +data Thins : Context a -> Context a -> Type where + Id : ctx `Thins` ctx + Drop : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 :< x + Keep : ctx1 `Thins` ctx2 -> ctx1 :< (x :- v) `Thins` ctx2 :< (y :- v) %name Thins f, g, h -- Basics +indexPos : (f : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> Var ctx2 v +indexPos Id pos = toVar pos +indexPos (Drop f) pos = ThereVar (indexPos f pos) +indexPos (Keep f) Here = toVar Here +indexPos (Keep f) (There pos) = ThereVar (indexPos f pos) + export -index : k `Thins` n -> Fin k -> Fin n -index Id x = x -index (Drop f) x = FS (index f x) -index (Keep f) FZ = FZ -index (Keep f) (FS x) = FS (index f x) +index : ctx1 `Thins` ctx2 -> Var ctx1 v -> Var ctx2 v +index f i = indexPos f i.pos export -(.) : k `Thins` n -> j `Thins` k -> j `Thins` n +(.) : ctx2 `Thins` ctx3 -> ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx3 Id . g = g Drop f . g = Drop (f . g) Keep f . Id = Keep f @@ -35,43 +40,53 @@ Keep f . Keep g = Keep (f . g) -- Basic properties -export -indexInjective : (f : k `Thins` n) -> {x, y : Fin k} -> index f x = index f y -> x = y -indexInjective Id eq = eq -indexInjective (Drop f) eq = indexInjective f $ injective eq -indexInjective (Keep f) {x = FZ} {y = FZ} eq = Refl -indexInjective (Keep f) {x = FS x} {y = FS y} eq = cong FS $ indexInjective f $ injective eq +indexPosInjective : + (f : ctx1 `Thins` ctx2) -> {i : VarPos ctx1 x v} -> {j : VarPos ctx1 y v} -> + (0 _ : toNat (indexPos f i).pos = toNat (indexPos f j).pos) -> i = j +indexPosInjective Id prf = toNatInjective prf +indexPosInjective (Drop f) prf = indexPosInjective f (injective prf) +indexPosInjective (Keep f) {i = Here} {j = Here} prf = Refl +indexPosInjective (Keep f) {i = There i} {j = There j} prf = + thereCong (indexPosInjective f $ injective prf) export -(f : k `Thins` n) => Injective (index f) where - injective = indexInjective f +indexInjective : (f : ctx1 `Thins` ctx2) -> {i, j : Var ctx1 v} -> index f i = index f j -> i = j +indexInjective f {i = %% x, j = %% y} prf = toVarCong (indexPosInjective f $ toNatCong' prf) export -indexId : (0 x : Fin n) -> index Id x = x -indexId x = Refl +indexId : (0 i : Var ctx v) -> index Id i = i +indexId (%% x) = Refl export -indexDrop : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Drop f) x = FS (index f x) -indexDrop f x = Refl +indexDrop : (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) -> index (Drop f) i = ThereVar (index f i) +indexDrop f (%% x) = Refl export -indexKeepFZ : (0 f : k `Thins` n) -> index (Keep f) FZ = FZ -indexKeepFZ f = Refl +indexKeepHere : (0 f : ctx1 `Thins` ctx2) -> index (Keep {x, y} f) (%% x) = (%% y) +indexKeepHere f = Refl export -indexKeepFS : (0 f : k `Thins` n) -> (0 x : Fin k) -> index (Keep f) (FS x) = FS (index f x) -indexKeepFS f x = Refl +indexKeepThere : + (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) -> + index (Keep f) (ThereVar i) = ThereVar (index f i) +indexKeepThere f (%% x) = Refl + +indexPosComp : + (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> + indexPos (f . g) pos = index f (indexPos g pos) +indexPosComp Id g pos with (indexPos g pos) + _ | (%% _) = Refl +indexPosComp (Drop f) g pos = cong ThereVar (indexPosComp f g pos) +indexPosComp (Keep f) Id pos = Refl +indexPosComp (Keep f) (Drop g) pos = cong ThereVar (indexPosComp f g pos) +indexPosComp (Keep f) (Keep g) Here = Refl +indexPosComp (Keep f) (Keep g) (There pos) = cong ThereVar (indexPosComp f g pos) export indexComp : - (f : k `Thins` n) -> (g : j `Thins` k) -> (x : Fin j) -> - index (f . g) x = index f (index g x) -indexComp Id g x = Refl -indexComp (Drop f) g x = cong FS (indexComp f g x) -indexComp (Keep f) Id x = Refl -indexComp (Keep f) (Drop g) x = cong FS (indexComp f g x) -indexComp (Keep f) (Keep g) FZ = Refl -indexComp (Keep f) (Keep g) (FS x) = cong FS (indexComp f g x) + (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (i : Var ctx1 v) -> + index (f . g) i = index f (index g i) +indexComp f g i = indexPosComp f g i.pos -- Congruence ------------------------------------------------------------------ @@ -79,7 +94,7 @@ export infix 6 ~~~ public export -data (~~~) : k `Thins` n -> k `Thins` n -> Type where +data (~~~) : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 -> Type where IdId : Id ~~~ Id IdKeep : Id ~~~ f -> Id ~~~ Keep f KeepId : f ~~~ Id -> Keep f ~~~ Id @@ -88,86 +103,95 @@ data (~~~) : k `Thins` n -> k `Thins` n -> Type where %name Thinning.(~~~) prf -export -(.index) : f ~~~ g -> (x : Fin k) -> index f x = index g x -(IdId).index x = Refl -(IdKeep prf).index FZ = Refl -(IdKeep prf).index (FS x) = cong FS (prf.index x) -(KeepId prf).index FZ = Refl -(KeepId prf).index (FS x) = cong FS (prf.index x) -(DropDrop prf).index x = cong FS (prf.index x) -(KeepKeep prf).index FZ = Refl -(KeepKeep prf).index (FS x) = cong FS (prf.index x) +(.indexPos) : f ~~~ g -> (pos : VarPos ctx1 x v) -> indexPos f pos = indexPos g pos +(IdId).indexPos pos = Refl +(IdKeep prf).indexPos Here = Refl +(IdKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos +(KeepId prf).indexPos Here = Refl +(KeepId prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos +(DropDrop prf).indexPos pos = cong ThereVar $ prf.indexPos pos +(KeepKeep prf).indexPos Here = Refl +(KeepKeep prf).indexPos (There pos) = cong ThereVar $ prf.indexPos pos export -pointwise : {f, g : k `Thins` n} -> (0 _ : (x : Fin k) -> index f x = index g x) -> f ~~~ g -pointwise {f = Id} {g = Id} prf = IdId -pointwise {f = Id} {g = Drop g} prf = void $ absurd $ prf FZ -pointwise {f = Id} {g = Keep g} prf = IdKeep (pointwise $ \x => injective $ prf $ FS x) -pointwise {f = Drop f} {g = Id} prf = void $ absurd $ prf FZ -pointwise {f = Drop f} {g = Drop g} prf = DropDrop (pointwise $ \x => injective $ prf x) -pointwise {f = Drop f} {g = Keep g} prf = void $ absurd $ prf FZ -pointwise {f = Keep f} {g = Id} prf = KeepId (pointwise $ \x => injective $ prf $ FS x) -pointwise {f = Keep f} {g = Drop g} prf = void $ absurd $ prf FZ -pointwise {f = Keep f} {g = Keep g} prf = KeepKeep (pointwise $ \x => injective $ prf $ FS x) +(.index) : f ~~~ g -> (i : Var ctx1 v) -> index f i = index g i +prf.index i = prf.indexPos i.pos -------------------------------------------------------------------------------- -- Environments ---------------------------------------------------------------- -------------------------------------------------------------------------------- public export -data Env : Nat -> Nat -> Type -> Type where - Base : k `Thins` n -> Env k n a - (:<) : Env k n a -> a -> Env (S k) n a +data Env : Context a -> Context a -> (a -> Type) -> Type where + Base : {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 -> Env ctx1 ctx2 p + (:<) : + {0 ctx1, ctx2 : Context a} -> + Env ctx1 ctx2 p -> (x : Assoc0 (p v)) -> + Env (ctx1 :< (x.name :- v)) ctx2 p %name Env env +lookupPos : Env ctx1 ctx2 p -> VarPos ctx1 x v -> Either (Var ctx2 v) (p v) +lookupPos (Base f) pos = Left (indexPos f pos) +lookupPos (env :< (x :- pv)) Here = Right pv +lookupPos (env :< (x :- pv)) (There pos) = lookupPos env pos + export -lookup : Env k n a -> Fin k -> Either (Fin n) a -lookup (Base f) x = Left (index f x) -lookup (env :< v) FZ = Right v -lookup (env :< v) (FS x) = lookup env x +lookup : Env ctx1 ctx2 p -> Var ctx1 v -> Either (Var ctx2 v) (p v) +lookup env i = lookupPos env i.pos -- Properties export -lookupFZ : (0 env : Env k n a) -> (0 v : a) -> lookup (env :< v) FZ = Right v -lookupFZ env v = Refl +lookupHere : + (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> + lookup (env :< (x :- pv)) (%% x) = Right pv +lookupHere env x pv = Refl export lookupFS : - (0 env : Env k n a) -> (0 v : a) -> (0 x : Fin k) -> - lookup (env :< v) (FS x) = lookup env x -lookupFS env v x = Refl + (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> (0 i : Var ctx1 w) -> + lookup (env :< (x :- pv)) (ThereVar i) = lookup env i +lookupFS env x pv i = Refl -------------------------------------------------------------------------------- -- Renaming Coalgebras --------------------------------------------------------- -------------------------------------------------------------------------------- public export -interface Rename (0 a : Nat -> Type) where - var : Fin n -> a n - rename : k `Thins` n -> a k -> a n - 0 renameCong : {0 f, g : k `Thins` n} -> f ~~~ g -> (x : a k) -> rename f x = rename g x - 0 renameId : (x : a n) -> rename Id x = x - -export -lift : Rename a => k `Thins` n -> Env j k (a k) -> Env j n (a n) +interface Rename (0 a : Type) (0 t : Context a -> a -> Type) where + var : {0 ctx : Context a} -> {0 v : a} -> Var ctx v -> t ctx v + rename : + {0 ctx1, ctx2 : Context a} -> ctx1 `Thins` ctx2 -> + {0 v : a} -> t ctx1 v -> t ctx2 v + 0 renameCong : + {0 ctx1, ctx2 : Context a} -> {0 f, g : ctx1 `Thins` ctx2} -> f ~~~ g -> + {0 v : a} -> (x : t ctx1 v) -> rename f x = rename g x + 0 renameId : {0 ctx : Context a} -> {0 v : a} -> (x : t ctx v) -> rename Id x = x + +export +lift : Rename a t => ctx2 `Thins` ctx3 -> Env ctx1 ctx2 (t ctx2) -> Env ctx1 ctx3 (t ctx3) lift Id env = env lift f (Base g) = Base (f . g) -lift f (env :< v) = lift f env :< rename f v +lift f (env :< (x :- v)) = lift f env :< (x :- rename f v) + +lookupPosLift : + Rename a t => + (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (pos : VarPos ctx1 x v) -> + lookupPos (lift f env) pos = bimap (index f) (rename f) (lookupPos env pos) +lookupPosLift Id env pos with (lookupPos env pos) + _ | Left (%% y) = Refl + _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y +lookupPosLift (Drop f) (Base g) pos = cong Left $ indexPosComp (Drop f) g pos +lookupPosLift (Keep f) (Base g) pos = cong Left $ indexPosComp (Keep f) g pos +lookupPosLift (Drop f) (env :< (x :- v)) Here = Refl +lookupPosLift (Keep f) (env :< (x :- v)) Here = Refl +lookupPosLift (Drop f) (env :< (x :- v)) (There pos) = lookupPosLift (Drop f) env pos +lookupPosLift (Keep f) (env :< (x :- v)) (There pos) = lookupPosLift (Keep f) env pos export lookupLift : - Rename a => - (f : k `Thins` n) -> (env : Env j k (a k)) -> (x : Fin j) -> - lookup (lift f env) x = bimap (index f) (rename f) (lookup env x) -lookupLift Id env x with (lookup env x) - _ | Left y = Refl - _ | Right y = cong Right $ irrelevantEq $ sym $ renameId y -lookupLift (Drop f) (Base g) x = cong Left $ indexComp (Drop f) g x -lookupLift (Drop f) (env :< y) FZ = Refl -lookupLift (Drop f) (env :< y) (FS x) = lookupLift (Drop f) env x -lookupLift (Keep f) (Base g) x = cong Left $ indexComp (Keep f) g x -lookupLift (Keep f) (env :< y) FZ = Refl -lookupLift (Keep f) (env :< y) (FS x) = lookupLift (Keep f) env x + Rename a t => + (f : ctx2 `Thins` ctx3) -> (env : Env ctx1 ctx2 (t ctx2)) -> (i : Var ctx1 v) -> + lookup (lift f env) i = bimap (index f) (rename f) (lookup env i) +lookupLift f env i = lookupPosLift f env i.pos diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index 3021f96..e3eee12 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -1,1022 +1,408 @@ module Inky.Type -import public Data.List1 - -import Control.Function import Data.Bool.Decidable -import Data.Either +import Data.DPair +import Data.Maybe.Decidable import Data.These import Data.These.Decidable -import Decidable.Equality +import Inky.Context import Inky.Thinning --- Utilities ------------------------------------------------------------------- - -reflectFinEq : (i, j : Fin n) -> (i = j) `Reflects` (i == j) -reflectFinEq FZ FZ = RTrue Refl -reflectFinEq FZ (FS j) = RFalse absurd -reflectFinEq (FS i) FZ = RFalse absurd -reflectFinEq (FS i) (FS j) = - viaEquivalence (MkEquivalence (\prf => cong FS prf) injective) - (reflectFinEq i j) - -- Definition ------------------------------------------------------------------ public export -data Ty : Nat -> Type where - TVar : Fin n -> Ty n - TNat : Ty n - TArrow : Ty n -> Ty n -> Ty n - TUnion : List1 (Ty n) -> Ty n - TProd : List (Ty n) -> Ty n - TSum : List (Ty n) -> Ty n - TFix : Ty (S n) -> Ty n +data Ty : Context () -> () -> Type where + TVar : Var ctx v -> Ty ctx v + TNat : Ty ctx () + TArrow : Ty ctx () -> Ty ctx () -> Ty ctx () + TProd : Row (Ty ctx ()) -> Ty ctx () + TSum : Row (Ty ctx ()) -> Ty ctx () + TFix : (x : String) -> Ty (ctx :< (x :- ())) () -> Ty ctx () %name Ty a, b, c -export -Injective TVar where - injective Refl = Refl +-------------------------------------------------------------------------------- +-- Thinning -------------------------------------------------------------------- +-------------------------------------------------------------------------------- -export -Injective TUnion where - injective Refl = Refl +thin : ctx1 `Thins` ctx2 -> forall v. Ty ctx1 v -> Ty ctx2 v +thinAll : ctx1 `Thins` ctx2 -> forall v. Row (Ty ctx1 v) -> Row (Ty ctx2 v) +thinAllFresh : + (f : ctx1 `Thins` ctx2) -> (x : String) -> + forall v. (row : Row (Ty ctx1 v)) -> + So (x `freshIn` row) -> So (x `freshIn` thinAll f row) -export -Injective TProd where - injective Refl = Refl +thin f (TVar i) = TVar (index f i) +thin f TNat = TNat +thin f (TArrow a b) = TArrow (thin f a) (thin f b) +thin f (TProd as) = TProd (thinAll f as) +thin f (TSum as) = TSum (thinAll f as) +thin f (TFix x a) = TFix x (thin (Keep f) a) --- Equality -------------------------------------------------------------------- +thinAll f [<] = [<] +thinAll f ((:<) as (x :- a) {fresh}) = + (:<) (thinAll f as) (x :- thin f a) {fresh = thinAllFresh f x as fresh} + +thinAllFresh f x [<] = id +thinAllFresh f x (as :< (y :- a)) = andSo . mapSnd (thinAllFresh f x as) . soAnd + +-- Renaming Coalgebra + +thinCong : f ~~~ g -> forall v. (a : Ty ctx1 v) -> thin f a = thin g a +thinCongAll : f ~~~ g -> forall v. (as : Row (Ty ctx1 v)) -> thinAll f as = thinAll g as + +thinCong prf (TVar i) = cong TVar (prf.index i) +thinCong prf TNat = Refl +thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b) +thinCong prf (TProd as) = cong TProd (thinCongAll prf as) +thinCong prf (TSum as) = cong TSum (thinCongAll prf as) +thinCong prf (TFix x a) = cong (TFix x) (thinCong (KeepKeep prf) a) + +thinCongAll prf [<] = Refl +thinCongAll prf (as :< (x :- a)) = + snocCong2 (thinCongAll prf as) (cong (x :-) $ thinCong prf a) + +thinId : (a : Ty ctx v) -> thin Id a = a +thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as + +thinId (TVar i) = cong TVar (indexId i) +thinId TNat = Refl +thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b) +thinId (TProd as) = cong TProd (thinIdAll as) +thinId (TSum as) = cong TSum (thinIdAll as) +thinId (TFix x a) = cong (TFix x) (trans (thinCong (KeepId IdId) a) (thinId a)) + +thinIdAll [<] = Refl +thinIdAll (as :< (x :- a)) = + snocCong2 (thinIdAll as) (cong (x :-) $ thinId a) export -eq : Ty n -> Ty n -> Bool -eqAll : List (Ty n) -> List (Ty n) -> Bool -eqAll1 : List1 (Ty n) -> List1 (Ty n) -> Bool +Rename () Ty where + var = TVar + rename = thin + renameCong = thinCong + renameId = thinId -TVar i `eq` TVar j = i == j -TNat `eq` TNat = True -TArrow a b `eq` TArrow c d = (a `eq` c) && (b `eq` d) -TUnion as `eq` TUnion bs = as `eqAll1` bs -TProd as `eq` TProd bs = as `eqAll` bs -TSum as `eq` TSum bs = as `eqAll` bs -TFix a `eq` TFix b = a `eq` b -_ `eq` _ = False +-- Equality -------------------------------------------------------------------- -[] `eqAll` [] = True -(a :: as) `eqAll` (b :: bs) = (a `eq` b) && (as `eqAll` bs) -_ `eqAll` _ = False +Preeq : + {ctx2 : Context ()} -> {v : ()} -> + Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Type +PreeqAll : + {ctx2 : Context ()} -> {v : ()} -> + Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Type + +Preeq (TVar i) (TVar j) f = index f i = j +Preeq (TNat) (TNat) f = () +Preeq (TArrow a b) (TArrow c d) f = (Preeq a c f, Preeq b d f) +Preeq (TProd as) (TProd bs) f = PreeqAll as bs f +Preeq (TSum as) (TSum bs) f = PreeqAll as bs f +Preeq (TFix x a) (TFix y b) f = Preeq a b (Keep f) +Preeq _ _ f = Void + +PreeqAll [<] bs f = (bs = [<]) +PreeqAll (as :< (x :- a)) bs f = + ( b ** cs ** + ( Remove x bs b cs + , Preeq a b f + , PreeqAll as cs f + )) + +preeqAllReorder : + (as : Row (Ty ctx1 v)) -> bs <~> cs -> (f : ctx1 `Thins` ctx2) -> + PreeqAll as bs f -> PreeqAll as cs f +preeqAllReorder [<] [] f Refl = Refl +preeqAllReorder [<] (step :: prf) f Refl impossible +preeqAllReorder (as :< (x :- a)) prf f (b ** bs ** (prf', eq1, eq2)) = + (b ** bs ** (bimap id (trans (sym prf)) prf', eq1, eq2)) + +preeq : Ty ctx1 v -> Ty ctx2 v -> ctx1 `Thins` ctx2 -> Bool +preeqAll : Row (Ty ctx1 v) -> Row (Ty ctx2 v) -> ctx1 `Thins` ctx2 -> Bool + +preeq (TVar i) (TVar j) f = index f i == j +preeq TNat TNat f = True +preeq (TArrow a b) (TArrow c d) f = preeq a c f && preeq b d f +preeq (TProd as) (TProd bs) f = preeqAll as bs f +preeq (TSum as) (TSum bs) f = preeqAll as bs f +preeq (TFix x a) (TFix y b) f = preeq a b (Keep f) +preeq _ _ f = False + +preeqAll [<] bs f = null bs +preeqAll (as :< (x :- a)) bs f = + case remove' x bs of + Just (b, bs) => preeq a b f && preeqAll as bs f + Nothing => False -(a ::: as) `eqAll1` (b ::: bs) = (a `eq` b) && (as `eqAll` bs) +export +reflectAnd : a `Reflects` b1 -> b `Reflects` b2 -> (a, b) `Reflects` (b1 && b2) +reflectAnd (RTrue x) (RTrue y) = RTrue (x, y) +reflectAnd (RTrue x) (RFalse f) = RFalse (f . snd) +reflectAnd (RFalse f) _ = RFalse (f . fst) + +0 reflectPreeq : + (a : Ty ctx1 v) -> (b : Ty ctx2 v) -> (f : ctx1 `Thins` ctx2) -> + Preeq a b f `Reflects` preeq a b f +0 reflectPreeqAll : + (as : Row (Ty ctx1 v)) -> (bs : Row (Ty ctx2 v)) -> (f : ctx1 `Thins` ctx2) -> + PreeqAll as bs f `Reflects` preeqAll as bs f + +reflectPreeq (TVar i) (TVar j) f = reflectEq (index f i) j +reflectPreeq (TVar i) TNat f = RFalse id +reflectPreeq (TVar i) (TArrow a b) f = RFalse id +reflectPreeq (TVar i) (TProd as) f = RFalse id +reflectPreeq (TVar i) (TSum as) f = RFalse id +reflectPreeq (TVar i) (TFix x a) f = RFalse id +reflectPreeq TNat (TVar i) f = RFalse id +reflectPreeq TNat TNat f = RTrue () +reflectPreeq TNat (TArrow a b) f = RFalse id +reflectPreeq TNat (TProd as) f = RFalse id +reflectPreeq TNat (TSum as) f = RFalse id +reflectPreeq TNat (TFix x a) f = RFalse id +reflectPreeq (TArrow a c) (TVar i) f = RFalse id +reflectPreeq (TArrow a c) TNat f = RFalse id +reflectPreeq (TArrow a c) (TArrow b d) f = reflectAnd (reflectPreeq a b f) (reflectPreeq c d f) +reflectPreeq (TArrow a c) (TProd as) f = RFalse id +reflectPreeq (TArrow a c) (TSum as) f = RFalse id +reflectPreeq (TArrow a c) (TFix x b) f = RFalse id +reflectPreeq (TProd as) (TVar i) f = RFalse id +reflectPreeq (TProd as) TNat f = RFalse id +reflectPreeq (TProd as) (TArrow a b) f = RFalse id +reflectPreeq (TProd as) (TProd bs) f = reflectPreeqAll as bs f +reflectPreeq (TProd as) (TSum bs) f = RFalse id +reflectPreeq (TProd as) (TFix x a) f = RFalse id +reflectPreeq (TSum as) (TVar i) f = RFalse id +reflectPreeq (TSum as) TNat f = RFalse id +reflectPreeq (TSum as) (TArrow a b) f = RFalse id +reflectPreeq (TSum as) (TProd bs) f = RFalse id +reflectPreeq (TSum as) (TSum bs) f = reflectPreeqAll as bs f +reflectPreeq (TSum as) (TFix x a) f = RFalse id +reflectPreeq (TFix x a) (TVar i) f = RFalse id +reflectPreeq (TFix x a) TNat f = RFalse id +reflectPreeq (TFix x a) (TArrow b c) f = RFalse id +reflectPreeq (TFix x a) (TProd as) f = RFalse id +reflectPreeq (TFix x a) (TSum as) f = RFalse id +reflectPreeq (TFix x a) (TFix y b) f = reflectPreeq a b (Keep f) + +reflectPreeqAll [<] [<] f = RTrue Refl +reflectPreeqAll [<] (_ :< _) f = RFalse (\case Refl impossible) +reflectPreeqAll (as :< (x :- a)) bs f with (reflectRemove x bs) | (remove' x bs) + _ | RJust (Evidence fresh prf) | Just (b, cs) with (reflectAnd (reflectPreeq a b f) (reflectPreeqAll as cs f)) | (preeq a b f && preeqAll as cs f) + _ | RTrue prf' | _ = RTrue (b ** cs ** (Evidence fresh prf, prf')) + _ | RFalse nprf | _ = + RFalse (\(b' ** cs' ** (prf1, prf2)) => + let (eq, reorder) = removeUnique x bs (Evidence fresh prf) prf1 in + nprf $ + bimap + (\x => rewrite eq in x) + (preeqAllReorder as (sym reorder) f) + prf2) + _ | RNothing nprf | _ = RFalse (\(b ** cs ** (prf, _)) => nprf (b, cs) prf) public export -Eq (Ty n) where - (==) = eq +Eq (Ty ctx v) where + a == b = preeq a b Id export -reflectEq : (a, b : Ty n) -> (a = b) `Reflects` (a `eq` b) -reflectEqAll : (as, bs : List (Ty n)) -> (as = bs) `Reflects` (as `eqAll` bs) -reflectEqAll1 : (as, bs : List1 (Ty n)) -> (as = bs) `Reflects` (as `eqAll1` bs) - -reflectEq (TVar i) (TVar j) with (reflectFinEq i j) | (i == j) - _ | RTrue eq | _ = RTrue (cong TVar eq) - _ | RFalse neq | _ = RFalse (\eq => neq $ injective eq) -reflectEq (TVar i) TNat = RFalse (\case Refl impossible) -reflectEq (TVar i) (TArrow c d) = RFalse (\case Refl impossible) -reflectEq (TVar i) (TUnion c) = RFalse (\case Refl impossible) -reflectEq (TVar i) (TProd c) = RFalse (\case Refl impossible) -reflectEq (TVar i) (TSum c) = RFalse (\case Refl impossible) -reflectEq (TVar i) (TFix b) = RFalse (\case Refl impossible) -reflectEq TNat (TVar j) = RFalse (\case Refl impossible) -reflectEq TNat TNat = RTrue Refl -reflectEq TNat (TArrow c d) = RFalse (\case Refl impossible) -reflectEq TNat (TUnion c) = RFalse (\case Refl impossible) -reflectEq TNat (TProd c) = RFalse (\case Refl impossible) -reflectEq TNat (TSum c) = RFalse (\case Refl impossible) -reflectEq TNat (TFix b) = RFalse (\case Refl impossible) -reflectEq (TArrow a b) (TVar j) = RFalse (\case Refl impossible) -reflectEq (TArrow a b) TNat = RFalse (\case Refl impossible) -reflectEq (TArrow a b) (TArrow c d) with (reflectEq a c) | (a `eq` c) - _ | RTrue eq1 | _ with (reflectEq b d) | (b `eq` d) - _ | RTrue eq2 | _ = RTrue (cong2 TArrow eq1 eq2) - _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl) - _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl) -reflectEq (TArrow a b) (TUnion c) = RFalse (\case Refl impossible) -reflectEq (TArrow a b) (TProd c) = RFalse (\case Refl impossible) -reflectEq (TArrow a b) (TSum c) = RFalse (\case Refl impossible) -reflectEq (TArrow a b) (TFix c) = RFalse (\case Refl impossible) -reflectEq (TUnion as) (TVar j) = RFalse (\case Refl impossible) -reflectEq (TUnion as) TNat = RFalse (\case Refl impossible) -reflectEq (TUnion as) (TArrow c d) = RFalse (\case Refl impossible) -reflectEq (TUnion as) (TUnion c) with (reflectEqAll1 as c) | (as `eqAll1` c) - _ | RTrue eq | _ = RTrue (cong TUnion eq) - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) -reflectEq (TUnion as) (TProd c) = RFalse (\case Refl impossible) -reflectEq (TUnion as) (TSum c) = RFalse (\case Refl impossible) -reflectEq (TUnion as) (TFix b) = RFalse (\case Refl impossible) -reflectEq (TProd as) (TVar j) = RFalse (\case Refl impossible) -reflectEq (TProd as) TNat = RFalse (\case Refl impossible) -reflectEq (TProd as) (TArrow c d) = RFalse (\case Refl impossible) -reflectEq (TProd as) (TUnion c) = RFalse (\case Refl impossible) -reflectEq (TProd as) (TProd c) with (reflectEqAll as c) | (as `eqAll` c) - _ | RTrue eq | _ = RTrue (cong TProd eq) - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) -reflectEq (TProd as) (TSum c) = RFalse (\case Refl impossible) -reflectEq (TProd as) (TFix b) = RFalse (\case Refl impossible) -reflectEq (TSum as) (TVar j) = RFalse (\case Refl impossible) -reflectEq (TSum as) TNat = RFalse (\case Refl impossible) -reflectEq (TSum as) (TArrow c d) = RFalse (\case Refl impossible) -reflectEq (TSum as) (TUnion c) = RFalse (\case Refl impossible) -reflectEq (TSum as) (TProd c) = RFalse (\case Refl impossible) -reflectEq (TSum as) (TSum c) with (reflectEqAll as c) | (as `eqAll` c) - _ | RTrue eq | _ = RTrue (cong TSum eq) - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) -reflectEq (TSum as) (TFix b) = RFalse (\case Refl impossible) -reflectEq (TFix a) (TVar j) = RFalse (\case Refl impossible) -reflectEq (TFix a) TNat = RFalse (\case Refl impossible) -reflectEq (TFix a) (TArrow c d) = RFalse (\case Refl impossible) -reflectEq (TFix a) (TUnion c) = RFalse (\case Refl impossible) -reflectEq (TFix a) (TProd c) = RFalse (\case Refl impossible) -reflectEq (TFix a) (TSum c) = RFalse (\case Refl impossible) -reflectEq (TFix a) (TFix b) with (reflectEq a b) | (a `eq` b) - _ | RTrue eq | _ = RTrue (cong TFix eq) - _ | RFalse neq | _ = RFalse (\case Refl => neq Refl) - -reflectEqAll [] [] = RTrue Refl -reflectEqAll [] (b :: bs) = RFalse (\case Refl impossible) -reflectEqAll (a :: as) [] = RFalse (\case Refl impossible) -reflectEqAll (a :: as) (b :: bs) with (reflectEq a b) | (a `eq` b) - _ | RTrue eq1 | _ with (reflectEqAll as bs) | (as `eqAll` bs) - _ | RTrue eq2 | _ = RTrue (cong2 (::) eq1 eq2) - _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl) - _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl) - -reflectEqAll1 (a ::: as) (b ::: bs) with (reflectEq a b) | (a `eq` b) - _ | RTrue eq1 | _ with (reflectEqAll as bs) | (as `eqAll` bs) - _ | RTrue eq2 | _ = RTrue (cong2 (:::) eq1 eq2) - _ | RFalse neq2 | _ = RFalse (\case Refl => neq2 Refl) - _ | RFalse neq1 | _ = RFalse (\case Refl => neq1 Refl) +Eq : {ctx : Context ()} -> {v : ()} -> Ty ctx v -> Ty ctx v -> Type +Eq a b = Preeq a b Id + +export +0 reflectEq : (a, b : Ty ctx v) -> (a `Eq` b) `Reflects` (a == b) +reflectEq a b = reflectPreeq a b Id -- Occurs ---------------------------------------------------------------------- -OccursIn : Fin n -> Ty n -> Type -OccursInAny : Fin n -> List (Ty n) -> Type -OccursInAny1 : Fin n -> List1 (Ty n) -> Type +OccursIn : Var ctx v -> Ty ctx w -> Type +OccursInAny : Var ctx v -> Row (Ty ctx w) -> Type i `OccursIn` TVar j = i = j i `OccursIn` TNat = Void i `OccursIn` TArrow a b = These (i `OccursIn` a) (i `OccursIn` b) -i `OccursIn` TUnion as = i `OccursInAny1` as i `OccursIn` TProd as = i `OccursInAny` as i `OccursIn` TSum as = i `OccursInAny` as -i `OccursIn` TFix a = FS i `OccursIn` a +i `OccursIn` TFix x a = ThereVar i `OccursIn` a -i `OccursInAny` [] = Void -i `OccursInAny` a :: as = These (i `OccursIn` a) (i `OccursInAny` as) - -i `OccursInAny1` a ::: as = These (i `OccursIn` a) (i `OccursInAny` as) +i `OccursInAny` [<] = Void +i `OccursInAny` (as :< (x :- a)) = These (i `OccursIn` a) (i `OccursInAny` as) -- Decidable -occursIn : (i : Fin n) -> (a : Ty n) -> Bool -occursInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool -occursInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool +occursIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool +occursInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool -reflectOccursIn : - (i : Fin n) -> (a : Ty n) -> - (i `OccursIn` a) `Reflects` (i `occursIn` a) -reflectOccursInAny : - (i : Fin n) -> (as : List (Ty n)) -> - (i `OccursInAny` as) `Reflects` (i `occursInAny` as) -reflectOccursInAny1 : - (i : Fin n) -> (as : List1 (Ty n)) -> - (i `OccursInAny1` as) `Reflects` (i `occursInAny1` as) - -i `occursIn` (TVar j) = i == j +i `occursIn` (TVar j) = i `eq` j i `occursIn` TNat = False i `occursIn` (TArrow a b) = (i `occursIn` a) || (i `occursIn` b) -i `occursIn` (TUnion as) = i `occursInAny1` as i `occursIn` (TProd as) = i `occursInAny` as i `occursIn` (TSum as) = i `occursInAny` as -i `occursIn` (TFix a) = FS i `occursIn` a +i `occursIn` (TFix x a) = ThereVar i `occursIn` a -i `occursInAny` [] = False -i `occursInAny` (a :: as) = (i `occursIn` a) || (i `occursInAny` as) +i `occursInAny` [<] = False +i `occursInAny` (as :< (x :- a)) = (i `occursIn` a) || (i `occursInAny` as) -i `occursInAny1` (a ::: as) = (i `occursIn` a) || (i `occursInAny` as) +reflectOccursIn : + (i : Var ctx v) -> (a : Ty ctx w) -> + (i `OccursIn` a) `Reflects` (i `occursIn` a) +reflectOccursInAny : + (i : Var ctx v) -> (as : Row (Ty ctx w)) -> + (i `OccursInAny` as) `Reflects` (i `occursInAny` as) -reflectOccursIn i (TVar j) = reflectFinEq i j +reflectOccursIn i (TVar j) = reflectEq i j reflectOccursIn i TNat = RFalse id reflectOccursIn i (TArrow a b) = reflectThese (reflectOccursIn i a) (reflectOccursIn i b) -reflectOccursIn i (TUnion as) = reflectOccursInAny1 i as reflectOccursIn i (TProd as) = reflectOccursInAny i as reflectOccursIn i (TSum as) = reflectOccursInAny i as -reflectOccursIn i (TFix a) = reflectOccursIn (FS i) a - -reflectOccursInAny i [] = RFalse id -reflectOccursInAny i (a :: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) +reflectOccursIn i (TFix x a) = reflectOccursIn (ThereVar i) a -reflectOccursInAny1 i (a ::: as) = reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) +reflectOccursInAny i [<] = RFalse id +reflectOccursInAny i (as :< (x :- a)) = + reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) -- Not Strictly Positive ----------------------------------------------------------- -- We use negation so we get a cause on failure. -NotPositiveIn : Fin n -> Ty n -> Type -NotPositiveInAny : Fin n -> List (Ty n) -> Type -NotPositiveInAny1 : Fin n -> List1 (Ty n) -> Type +NotPositiveIn : Var ctx v -> Ty ctx w -> Type +NotPositiveInAny : Var ctx v -> Row (Ty ctx w) -> Type i `NotPositiveIn` TVar j = Void i `NotPositiveIn` TNat = Void -i `NotPositiveIn` TArrow a b = These (i `OccursIn` a) (i `NotPositiveIn` b) -i `NotPositiveIn` TUnion as = i `NotPositiveInAny1` as +i `NotPositiveIn` TArrow a b = + -- NOTE: forbid on right side of arrow to prevent infinite breadth. + i `OccursIn` TArrow a b i `NotPositiveIn` TProd as = i `NotPositiveInAny` as i `NotPositiveIn` TSum as = i `NotPositiveInAny` as -i `NotPositiveIn` TFix a = FS i `OccursIn` a - -- Prevent mutual recursion; - -- Can add back in without breaking things +i `NotPositiveIn` TFix x a = + -- BUG: forbid under fixpoint to prevent unbounded width + -- this is safe to add back with the complex encoding of fixpoints + ThereVar i `OccursIn` a -i `NotPositiveInAny` [] = Void -i `NotPositiveInAny` a :: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) - -i `NotPositiveInAny1` a ::: as = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) +i `NotPositiveInAny` [<] = Void +i `NotPositiveInAny` as :< (x :- a) = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) -- Not Positive implies Occurs -notPositiveToOccurs : (a : Ty k) -> i `NotPositiveIn` a -> i `OccursIn` a -notPositiveAnyToOccursAny : (as : List (Ty k)) -> i `NotPositiveInAny` as -> i `OccursInAny` as -notPositiveAny1ToOccursAny1 : (as : List1 (Ty k)) -> i `NotPositiveInAny1` as -> i `OccursInAny1` as +notPositiveToOccurs : (a : Ty ctx v) -> i `NotPositiveIn` a -> i `OccursIn` a +notPositiveAnyToOccursAny : (as : Row (Ty ctx v)) -> i `NotPositiveInAny` as -> i `OccursInAny` as notPositiveToOccurs (TVar j) = absurd notPositiveToOccurs TNat = id -notPositiveToOccurs (TArrow a b) = mapSnd (notPositiveToOccurs b) -notPositiveToOccurs (TUnion as) = notPositiveAny1ToOccursAny1 as +notPositiveToOccurs (TArrow a b) = id notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as -notPositiveToOccurs (TFix a) = id - -notPositiveAnyToOccursAny [] = id -notPositiveAnyToOccursAny (a :: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) +notPositiveToOccurs (TFix x a) = id -notPositiveAny1ToOccursAny1 (a ::: as) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) - --- Decidable +notPositiveAnyToOccursAny [<] = id +notPositiveAnyToOccursAny (as :< (x :- a)) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) -notEnvPositiveIn : (i : Fin n) -> (a : Ty n) -> Bool -notEnvPositiveInAny : (i : Fin n) -> (as : List (Ty n)) -> Bool -notEnvPositiveInAny1 : (i : Fin n) -> (as : List1 (Ty n)) -> Bool +-- -- Decidable -i `notEnvPositiveIn` (TVar j) = False -i `notEnvPositiveIn` TNat = False -i `notEnvPositiveIn` (TArrow a b) = (i `occursIn` a) || (i `notEnvPositiveIn` b) -i `notEnvPositiveIn` (TUnion as) = i `notEnvPositiveInAny1` as -i `notEnvPositiveIn` (TProd as) = i `notEnvPositiveInAny` as -i `notEnvPositiveIn` (TSum as) = i `notEnvPositiveInAny` as -i `notEnvPositiveIn` (TFix a) = FS i `occursIn` a +notPositiveIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool +notPositiveInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool -i `notEnvPositiveInAny` [] = False -i `notEnvPositiveInAny` (a :: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as) +i `notPositiveIn` (TVar j) = False +i `notPositiveIn` TNat = False +i `notPositiveIn` (TArrow a b) = i `occursIn` TArrow a b +i `notPositiveIn` (TProd as) = i `notPositiveInAny` as +i `notPositiveIn` (TSum as) = i `notPositiveInAny` as +i `notPositiveIn` (TFix x a) = ThereVar i `occursIn` a -i `notEnvPositiveInAny1` (a ::: as) = (i `notEnvPositiveIn` a) || (i `notEnvPositiveInAny` as) +i `notPositiveInAny` [<] = False +i `notPositiveInAny` (as :< (x :- a)) = (i `notPositiveIn` a) || (i `notPositiveInAny` as) reflectNotPositiveIn : - (i : Fin n) -> (a : Ty n) -> - (i `NotPositiveIn` a) `Reflects` (i `notEnvPositiveIn` a) + (i : Var ctx v) -> (a : Ty ctx w) -> + (i `NotPositiveIn` a) `Reflects` (i `notPositiveIn` a) reflectNotPositiveInAny : - (i : Fin n) -> (as : List (Ty n)) -> - (i `NotPositiveInAny` as) `Reflects` (i `notEnvPositiveInAny` as) -reflectNotPositiveInAny1 : - (i : Fin n) -> (as : List1 (Ty n)) -> - (i `NotPositiveInAny1` as) `Reflects` (i `notEnvPositiveInAny1` as) + (i : Var ctx v) -> (as : Row (Ty ctx w)) -> + (i `NotPositiveInAny` as) `Reflects` (i `notPositiveInAny` as) reflectNotPositiveIn i (TVar j) = RFalse id reflectNotPositiveIn i TNat = RFalse id -reflectNotPositiveIn i (TArrow a b) = - reflectThese (reflectOccursIn i a) (reflectNotPositiveIn i b) -reflectNotPositiveIn i (TUnion as) = reflectNotPositiveInAny1 i as +reflectNotPositiveIn i (TArrow a b) = reflectOccursIn i (TArrow a b) reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as -reflectNotPositiveIn i (TFix a) = reflectOccursIn (FS i) a +reflectNotPositiveIn i (TFix x a) = reflectOccursIn (ThereVar i) a -reflectNotPositiveInAny i [] = RFalse id -reflectNotPositiveInAny i (a :: as) = - reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) - -reflectNotPositiveInAny1 i (a ::: as) = +reflectNotPositiveInAny i [<] = RFalse id +reflectNotPositiveInAny i (as :< (x :- a)) = reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) -- Well Formed ----------------------------------------------------------------- --- Negating reflectidable properties is fun. +-- Negating decidable properties is fun. export -IllFormed : Ty n -> Type -AnyIllFormed : List (Ty n) -> Type -Any1IllFormed : List1 (Ty n) -> Type +IllFormed : Ty ctx v -> Type +AnyIllFormed : Row (Ty ctx v) -> Type IllFormed (TVar v) = Void IllFormed TNat = Void IllFormed (TArrow a b) = These (IllFormed a) (IllFormed b) -IllFormed (TUnion as) = Any1IllFormed as IllFormed (TProd as) = AnyIllFormed as IllFormed (TSum as) = AnyIllFormed as -IllFormed (TFix a) = These (FZ `NotPositiveIn` a) (IllFormed a) - -AnyIllFormed [] = Void -AnyIllFormed (a :: as) = These (IllFormed a) (AnyIllFormed as) +IllFormed (TFix x a) = These (%% x `NotPositiveIn` a) (IllFormed a) -Any1IllFormed (a ::: as) = These (IllFormed a) (AnyIllFormed as) +AnyIllFormed [<] = Void +AnyIllFormed (as :< (x :- a)) = These (IllFormed a) (AnyIllFormed as) -- Decidable export -illFormed : (a : Ty n) -> Bool -anyIllFormed : (as : List (Ty n)) -> Bool -any1IllFormed : (as : List1 (Ty n)) -> Bool - +illFormed : (a : Ty ctx v) -> Bool +anyIllFormed : (as : Row (Ty ctx v)) -> Bool illFormed (TVar j) = False illFormed TNat = False illFormed (TArrow a b) = illFormed a || illFormed b -illFormed (TUnion as) = any1IllFormed as illFormed (TProd as) = anyIllFormed as illFormed (TSum as) = anyIllFormed as -illFormed (TFix a) = (FZ `notEnvPositiveIn` a) || illFormed a - -anyIllFormed [] = False -anyIllFormed (a :: as) = illFormed a || anyIllFormed as +illFormed (TFix x a) = (%% x `notPositiveIn` a) || illFormed a -any1IllFormed (a ::: as) = illFormed a || anyIllFormed as +anyIllFormed [<] = False +anyIllFormed (as :< (x :- a)) = illFormed a || anyIllFormed as export -reflectIllFormed : (a : Ty n) -> IllFormed a `Reflects` illFormed a -reflectAnyIllFormed : (as : List (Ty n)) -> AnyIllFormed as `Reflects` anyIllFormed as -reflectAny1IllFormed : (as : List1 (Ty n)) -> Any1IllFormed as `Reflects` any1IllFormed as +reflectIllFormed : (a : Ty ctx v) -> IllFormed a `Reflects` illFormed a +reflectAnyIllFormed : (as : Row (Ty ctx v)) -> AnyIllFormed as `Reflects` anyIllFormed as reflectIllFormed (TVar j) = RFalse id reflectIllFormed TNat = RFalse id -reflectIllFormed (TArrow a b) = - reflectThese (reflectIllFormed a) (reflectIllFormed b) -reflectIllFormed (TUnion as) = reflectAny1IllFormed as +reflectIllFormed (TArrow a b) = reflectThese (reflectIllFormed a) (reflectIllFormed b) reflectIllFormed (TProd as) = reflectAnyIllFormed as reflectIllFormed (TSum as) = reflectAnyIllFormed as -reflectIllFormed (TFix a) = reflectThese (reflectNotPositiveIn FZ a) (reflectIllFormed a) - -reflectAnyIllFormed [] = RFalse id -reflectAnyIllFormed (a :: as) = - reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) +reflectIllFormed (TFix x a) = reflectThese (reflectNotPositiveIn (%% x) a) (reflectIllFormed a) -reflectAny1IllFormed (a ::: as) = +reflectAnyIllFormed [<] = RFalse id +reflectAnyIllFormed (as :< (x :- a)) = reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) --------------------------------------------------------------------------------- --- Thinning -------------------------------------------------------------------- --------------------------------------------------------------------------------- - -thin : k `Thins` n -> Ty k -> Ty n -thinAll : k `Thins` n -> List (Ty k) -> List (Ty n) -thinAll1 : k `Thins` n -> List1 (Ty k) -> List1 (Ty n) - -thin f (TVar i) = TVar (index f i) -thin f TNat = TNat -thin f (TArrow a b) = TArrow (thin f a) (thin f b) -thin f (TUnion as) = TUnion (thinAll1 f as) -thin f (TProd as) = TProd (thinAll f as) -thin f (TSum as) = TSum (thinAll f as) -thin f (TFix a) = TFix (thin (Keep f) a) - -thinAll f [] = [] -thinAll f (a :: as) = thin f a :: thinAll f as - -thinAll1 f (a ::: as) = thin f a ::: thinAll f as - --- Renaming Coalgebra - -thinCong : f ~~~ g -> (a : Ty k) -> thin f a = thin g a -thinCongAll : f ~~~ g -> (as : List (Ty k)) -> thinAll f as = thinAll g as -thinCongAll1 : f ~~~ g -> (as : List1 (Ty k)) -> thinAll1 f as = thinAll1 g as - -thinCong prf (TVar i) = cong TVar (prf.index i) -thinCong prf TNat = Refl -thinCong prf (TArrow a b) = cong2 TArrow (thinCong prf a) (thinCong prf b) -thinCong prf (TUnion as) = cong TUnion (thinCongAll1 prf as) -thinCong prf (TProd as) = cong TProd (thinCongAll prf as) -thinCong prf (TSum as) = cong TSum (thinCongAll prf as) -thinCong prf (TFix a) = cong TFix (thinCong (KeepKeep prf) a) - -thinCongAll prf [] = Refl -thinCongAll prf (a :: as) = cong2 (::) (thinCong prf a) (thinCongAll prf as) - -thinCongAll1 prf (a ::: as) = cong2 (:::) (thinCong prf a) (thinCongAll prf as) - -thinId : (a : Ty n) -> thin Id a = a -thinIdAll : (as : List (Ty n)) -> thinAll Id as = as -thinIdAll1 : (as : List1 (Ty n)) -> thinAll1 Id as = as - -thinId (TVar i) = cong TVar (indexId i) -thinId TNat = Refl -thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b) -thinId (TUnion as) = cong TUnion (thinIdAll1 as) -thinId (TProd as) = cong TProd (thinIdAll as) -thinId (TSum as) = cong TSum (thinIdAll as) -thinId (TFix a) = cong TFix (trans (thinCong (KeepId IdId) a) (thinId a)) - -thinIdAll [] = Refl -thinIdAll (a :: as) = cong2 (::) (thinId a) (thinIdAll as) - -thinIdAll1 (a ::: as) = cong2 (:::) (thinId a) (thinIdAll as) - -export -Rename Ty where - var = TVar - rename = thin - renameCong = thinCong - renameId = thinId - --- Properties ------------------------------------------------------------------ - --- Occurs -- - -thinOccursIn : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> - i `OccursIn` a -> - index f i `OccursIn` thin f a -thinOccursInAny : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) -> - i `OccursInAny` as -> - index f i `OccursInAny` thinAll f as -thinOccursInAny1 : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> - i `OccursInAny1` as -> - index f i `OccursInAny1` thinAll1 f as - -thinOccursIn f i (TVar x) = \Refl => Refl -thinOccursIn f i TNat = id -thinOccursIn f i (TArrow a b) = bimap (thinOccursIn f i a) (thinOccursIn f i b) -thinOccursIn f i (TUnion as) = thinOccursInAny1 f i as -thinOccursIn f i (TProd as) = thinOccursInAny f i as -thinOccursIn f i (TSum as) = thinOccursInAny f i as -thinOccursIn f i (TFix a) = - rewrite sym $ indexKeepFS f i in - thinOccursIn (Keep f) (FS i) a - -thinOccursInAny f i [] = id -thinOccursInAny f i (a :: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as) - -thinOccursInAny1 f i (a ::: as) = bimap (thinOccursIn f i a) (thinOccursInAny f i as) - --- Inverse - -thinOccursInInv' : - (0 f : k `Thins` n) -> (0 i : Fin n) -> - (a : Ty k) -> - i `OccursIn` thin f a -> - (j ** (index f j = i, j `OccursIn` a)) -thinOccursInAnyInv' : - (0 f : k `Thins` n) -> (0 i : Fin n) -> - (as : List (Ty k)) -> - i `OccursInAny` thinAll f as -> - (j ** (index f j = i, j `OccursInAny` as)) -thinOccursInAny1Inv' : - (0 f : k `Thins` n) -> (0 i : Fin n) -> - (as : List1 (Ty k)) -> - i `OccursInAny1` thinAll1 f as -> - (j ** (index f j = i, j `OccursInAny1` as)) - -thinOccursInInv' f i (TVar j) = \eq => (j ** (sym eq , Refl)) -thinOccursInInv' f i TNat = absurd -thinOccursInInv' f i (TArrow a b) = - these - (\occurs => - let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in - (j ** (eq, This prf))) - (\occurs => - let (j ** (eq, prf)) = thinOccursInInv' f i b occurs in - (j ** (eq, That prf))) - (\occurs1, occurs2 => - let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in - let (j2 ** (eq2, prf2)) = thinOccursInInv' f i b occurs2 in - (j1 ** (eq1, - Both prf1 $ - rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in - prf2))) -thinOccursInInv' f i (TUnion as) = thinOccursInAny1Inv' f i as -thinOccursInInv' f i (TProd as) = thinOccursInAnyInv' f i as -thinOccursInInv' f i (TSum as) = thinOccursInAnyInv' f i as -thinOccursInInv' f i (TFix a) = - \occurs => - case thinOccursInInv' (Keep f) (FS i) a occurs of - (FZ ** prf) => absurd (trans (sym $ indexKeepFZ f) (fst prf)) - (FS j ** (eq, prf)) => - (j ** (irrelevantEq (injective $ trans (sym $ indexKeepFS f j) eq), prf)) - -thinOccursInAnyInv' f i [] = absurd -thinOccursInAnyInv' f i (a :: as) = - these - (\occurs => - let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in - (j ** (eq, This prf))) - (\occurs => - let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in - (j ** (eq, That prf))) - (\occurs1, occurs2 => - let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in - let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in - (j1 ** (eq1, - Both prf1 $ - rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in - prf2))) - -thinOccursInAny1Inv' f i (a ::: as) = - these - (\occurs => - let (j ** (eq, prf)) = thinOccursInInv' f i a occurs in - (j ** (eq, This prf))) - (\occurs => - let (j ** (eq, prf)) = thinOccursInAnyInv' f i as occurs in - (j ** (eq, That prf))) - (\occurs1, occurs2 => - let (j1 ** (eq1, prf1)) = thinOccursInInv' f i a occurs1 in - let (j2 ** (eq2, prf2)) = thinOccursInAnyInv' f i as occurs2 in - (j1 ** (eq1, - Both prf1 $ - rewrite indexInjective f {x = j1, y = j2} $ trans eq1 (sym eq2) in - prf2))) - -thinOccursInInv : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> - index f i `OccursIn` thin f a -> - i `OccursIn` a -thinOccursInInv f i a occurs = - let (j ** (eq, prf)) = thinOccursInInv' f (index f i) a occurs in - rewrite indexInjective f {x = i, y = j} $ sym eq in - prf - -thinOccursInAny1Inv : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> - index f i `OccursInAny1` thinAll1 f as -> - i `OccursInAny1` as -thinOccursInAny1Inv f i as occurs = - let (j ** (eq, prf)) = thinOccursInAny1Inv' f (index f i) as occurs in - rewrite indexInjective f {x = i, y = j} $ sym eq in - prf - --- Not Positive -- - -thinNotPositiveInv : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (a : Ty k) -> - index f i `NotPositiveIn` thin f a -> i `NotPositiveIn` a -thinNotPositiveAnyInv : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List (Ty k)) -> - index f i `NotPositiveInAny` thinAll f as -> i `NotPositiveInAny` as -thinNotPositiveAny1Inv : - (0 f : k `Thins` n) -> (0 i : Fin k) -> (as : List1 (Ty k)) -> - index f i `NotPositiveInAny1` thinAll1 f as -> i `NotPositiveInAny1` as - -thinNotPositiveInv f i (TVar j) = id -thinNotPositiveInv f i TNat = id -thinNotPositiveInv f i (TArrow a b) = - bimap - (thinOccursInInv f i a) - (thinNotPositiveInv f i b) -thinNotPositiveInv f i (TUnion as) = thinNotPositiveAny1Inv f i as -thinNotPositiveInv f i (TProd as) = thinNotPositiveAnyInv f i as -thinNotPositiveInv f i (TSum as) = thinNotPositiveAnyInv f i as -thinNotPositiveInv f i (TFix a) = - \occurs => - thinOccursInInv (Keep f) (FS i) a $ - rewrite indexKeepFS f i in - occurs - -thinNotPositiveAnyInv f i [] = id -thinNotPositiveAnyInv f i (a :: as) = - bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as) - -thinNotPositiveAny1Inv f i (a ::: as) = - bimap (thinNotPositiveInv f i a) (thinNotPositiveAnyInv f i as) - --- Ill Formed -- - -thinIllFormedInv : - (0 f : k `Thins` n) -> (a : Ty k) -> - IllFormed (thin f a) -> IllFormed a -thinAnyIllFormedInv : - (0 f : k `Thins` n) -> (as : List (Ty k)) -> - AnyIllFormed (thinAll f as) -> AnyIllFormed as -thinAny1IllFormedInv : - (0 f : k `Thins` n) -> (as : List1 (Ty k)) -> - Any1IllFormed (thinAll1 f as) -> Any1IllFormed as - -thinIllFormedInv f (TVar i) = id -thinIllFormedInv f TNat = id -thinIllFormedInv f (TArrow a b) = bimap (thinIllFormedInv f a) (thinIllFormedInv f b) -thinIllFormedInv f (TUnion as) = thinAny1IllFormedInv f as -thinIllFormedInv f (TProd as) = thinAnyIllFormedInv f as -thinIllFormedInv f (TSum as) = thinAnyIllFormedInv f as -thinIllFormedInv f (TFix a) = - bimap - (\npos => thinNotPositiveInv (Keep f) FZ a $ rewrite indexKeepFZ f in npos) - (thinIllFormedInv (Keep f) a) - -thinAnyIllFormedInv f [] = id -thinAnyIllFormedInv f (a :: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as) - -thinAny1IllFormedInv f (a ::: as) = bimap (thinIllFormedInv f a) (thinAnyIllFormedInv f as) - -------------------------------------------------------------------------------- -- Substitution ---------------------------------------------------------------- -------------------------------------------------------------------------------- public export -fromVar : Either (Fin n) (Ty n) -> Ty n +fromVar : Either (Var ctx v) (Ty ctx v) -> Ty ctx v fromVar = either TVar id export -sub : Env k n (Ty n) -> Ty k -> Ty n -subAll : Env k n (Ty n) -> List (Ty k) -> List (Ty n) -subAll1 : Env k n (Ty n) -> List1 (Ty k) -> List1 (Ty n) +sub : Env ctx1 ctx2 (Ty ctx2) -> Ty ctx1 v -> Ty ctx2 v +subAll : Env ctx1 ctx2 (Ty ctx2) -> Row (Ty ctx1 v) -> Row (Ty ctx2 v) +subAllFresh : + (env : Env ctx1 ctx2 (Ty ctx2)) -> (x : String) -> + (row : Row (Ty ctx1 v)) -> + So (x `freshIn` row) -> So (x `freshIn` subAll env row) sub env (TVar i) = fromVar $ lookup env i sub env TNat = TNat sub env (TArrow a b) = TArrow (sub env a) (sub env b) -sub env (TUnion as) = TUnion (subAll1 env as) sub env (TProd as) = TProd (subAll env as) sub env (TSum as) = TSum (subAll env as) -sub env (TFix a) = TFix (sub (lift (Drop Id) env :< TVar FZ) a) - -subAll env [] = [] -subAll env (a :: as) = sub env a :: subAll env as - -subAll1 env (a ::: as) = sub env a ::: subAll env as - --- Properties ------------------------------------------------------------------ - -pushEither : - (0 f : c -> d) -> (0 g : a -> c) -> (0 h : b -> c) -> (x : Either a b) -> - f (either g h x) = either (f . g) (f . h) x -pushEither f g h (Left x) = Refl -pushEither f g h (Right x) = Refl - --- Occurs -- - -subOccursIn : - (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) -> - j `OccursIn` fromVar (lookup env i) -> - i `OccursIn` a -> - j `OccursIn` sub env a -subOccursInAny : - (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) -> - j `OccursIn` fromVar (lookup env i) -> - i `OccursInAny` as -> - j `OccursInAny` subAll env as -subOccursInAny1 : - (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) -> - j `OccursIn` fromVar (lookup env i) -> - i `OccursInAny1` as -> - j `OccursInAny1` subAll1 env as - -subOccursIn env i (TVar x) occurs = \Refl => occurs -subOccursIn env i TNat occurs = id -subOccursIn env i (TArrow a b) occurs = - bimap - (subOccursIn env i a occurs) - (subOccursIn env i b occurs) -subOccursIn env i (TUnion as) occurs = subOccursInAny1 env i as occurs -subOccursIn env i (TProd as) occurs = subOccursInAny env i as occurs -subOccursIn env i (TSum as) occurs = subOccursInAny env i as occurs -subOccursIn env i (TFix a) occurs = - subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $ - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in - rewrite lookupLift (Drop Id) env i in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in - rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in - rewrite sym $ indexId j in - rewrite sym $ indexDrop Id j in - thinOccursIn (Drop Id) j (fromVar $ lookup env i) $ - occurs - -subOccursInAny env i [] occurs = id -subOccursInAny env i (a :: as) occurs = - bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs) - -subOccursInAny1 env i (a ::: as) occurs = - bimap (subOccursIn env i a occurs) (subOccursInAny env i as occurs) - --- Inverse - -0 EnvOccursUniq : Env k n (Ty n) -> (i : Fin n) -> (j : Fin k) -> Type -EnvOccursUniq env i j = (x : Fin k) -> i `OccursIn` fromVar (lookup env x) -> j = x - -liftEnvOccursUniq : - (0 env : Env k n (Ty n)) -> - EnvOccursUniq env i j -> - EnvOccursUniq (lift (Drop Id) env :< TVar FZ) (FS i) (FS j) -liftEnvOccursUniq env prf FZ = - rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in - absurd -liftEnvOccursUniq env prf (FS x) = - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in - rewrite lookupLift (Drop Id) env x in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in - \occurs => - cong FS $ - prf x $ - thinOccursInInv (Drop Id) i (fromVar $ lookup env x) $ - rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in - rewrite indexDrop Id i in - rewrite indexId i in - occurs - -liftOccursUniqFZ : - (env : Env k n (Ty n)) -> - EnvOccursUniq (lift (Drop Id) env :< TVar FZ) FZ FZ -liftOccursUniqFZ env FZ = - rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in - const Refl -liftOccursUniqFZ env (FS x) = - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in - rewrite lookupLift (Drop Id) env x in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in - \occurs => - let - (j ** (eq, occurs')) = - thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $ - rewrite pushEither (rename (Drop Id)) TVar id (lookup env x) in - occurs - in - absurd $ trans (sym eq) (indexDrop Id j) - -subOccursInInv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvOccursUniq env i j) -> - (a : Ty k) -> - i `OccursIn` sub env a -> j `OccursIn` a -subOccursInAnyInv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvOccursUniq env i j) -> - (as : List (Ty k)) -> - i `OccursInAny` subAll env as -> j `OccursInAny` as -subOccursInAny1Inv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvOccursUniq env i j) -> - (as : List1 (Ty k)) -> - i `OccursInAny1` subAll1 env as -> j `OccursInAny1` as - -subOccursInInv env prf (TVar x) = \p => irrelevantEq $ prf x p -subOccursInInv env prf TNat = id -subOccursInInv env prf (TArrow a b) = - bimap - (subOccursInInv env prf a) - (subOccursInInv env prf b) -subOccursInInv env prf (TUnion as) = subOccursInAny1Inv env prf as -subOccursInInv env prf (TProd as) = subOccursInAnyInv env prf as -subOccursInInv env prf (TSum as) = subOccursInAnyInv env prf as -subOccursInInv env prf (TFix a) = - subOccursInInv - (lift (Drop Id) env :< TVar FZ) - (liftEnvOccursUniq env prf) - a - -subOccursInAnyInv env prf [] = id -subOccursInAnyInv env prf (a :: as) = - bimap - (subOccursInInv env prf a) - (subOccursInAnyInv env prf as) - -subOccursInAny1Inv env prf (a ::: as) = - bimap - (subOccursInInv env prf a) - (subOccursInAnyInv env prf as) - - --- Not Positive -- - -subNotPositiveIn : - (env : Env k n (Ty n)) -> (i : Fin k) -> (a : Ty k) -> - j `OccursIn` fromVar (lookup env i) -> - i `NotPositiveIn` a -> - j `NotPositiveIn` sub env a -subNotPositiveInAny : - (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List (Ty k)) -> - j `OccursIn` fromVar (lookup env i) -> - i `NotPositiveInAny` as -> - j `NotPositiveInAny` subAll env as -subNotPositiveInAny1 : - (env : Env k n (Ty n)) -> (i : Fin k) -> (as : List1 (Ty k)) -> - j `OccursIn` fromVar (lookup env i) -> - i `NotPositiveInAny1` as -> - j `NotPositiveInAny1` subAll1 env as - -subNotPositiveIn env i (TVar x) occurs = absurd -subNotPositiveIn env i TNat occurs = id -subNotPositiveIn env i (TArrow a b) occurs = - bimap - (subOccursIn env i a occurs) - (subNotPositiveIn env i b occurs) -subNotPositiveIn env i (TUnion as) occurs = subNotPositiveInAny1 env i as occurs -subNotPositiveIn env i (TProd as) occurs = subNotPositiveInAny env i as occurs -subNotPositiveIn env i (TSum as) occurs = subNotPositiveInAny env i as occurs -subNotPositiveIn env i (TFix a) occurs = - subOccursIn (lift (Drop Id) env :< TVar FZ) (FS i) a {j = FS j} $ - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) i in - rewrite lookupLift (Drop Id) env i in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (thin (Drop Id)) (lookup env i) in - rewrite sym $ pushEither (thin (Drop Id)) TVar id (lookup env i) in - rewrite sym $ indexId j in - rewrite sym $ indexDrop Id j in - thinOccursIn (Drop Id) j (fromVar $ lookup env i) $ - occurs - -subNotPositiveInAny env i [] occurs = id -subNotPositiveInAny env i (a :: as) occurs = - bimap - (subNotPositiveIn env i a occurs) - (subNotPositiveInAny env i as occurs) - -subNotPositiveInAny1 env i (a ::: as) occurs = - bimap - (subNotPositiveIn env i a occurs) - (subNotPositiveInAny env i as occurs) - --- Inverse - -0 EnvPositiveIn : Env k n (Ty n) -> (i : Fin n) -> Type -EnvPositiveIn env i = (x : Fin k) -> Not (i `NotPositiveIn` fromVar (lookup env x)) - -liftPositiveInFZ : - (env : Env k n (Ty n)) -> - EnvPositiveIn (lift (Drop Id) env :< TVar FZ) FZ -liftPositiveInFZ env FZ = - rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in - id -liftPositiveInFZ env (FS x) = - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in - rewrite lookupLift (Drop Id) env x in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in - \npos => - let - (j ** (eq, occurs)) = - thinOccursInInv' (Drop Id) FZ (fromVar $ lookup env x) $ - rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in - notPositiveToOccurs _ npos - in - absurd $ trans (sym (indexDrop Id j)) eq - -subNotPositiveInInv : - (0 env : Env k n (Ty n)) -> - (0 prf1 : EnvPositiveIn env i) -> - (0 prf2 : EnvOccursUniq env i j) -> - (a : Ty k) -> - i `NotPositiveIn` sub env a -> j `NotPositiveIn` a -subNotPositiveInAnyInv : - (0 env : Env k n (Ty n)) -> - (0 prf1 : EnvPositiveIn env i) -> - (0 prf2 : EnvOccursUniq env i j) -> - (as : List (Ty k)) -> - i `NotPositiveInAny` subAll env as -> j `NotPositiveInAny` as -subNotPositiveInAny1Inv : - (0 env : Env k n (Ty n)) -> - (0 prf1 : EnvPositiveIn env i) -> - (0 prf2 : EnvOccursUniq env i j) -> - (as : List1 (Ty k)) -> - i `NotPositiveInAny1` subAll1 env as -> j `NotPositiveInAny1` as - -subNotPositiveInInv env prf1 prf2 (TVar x) = \npos => void $ prf1 x npos -subNotPositiveInInv env prf1 prf2 TNat = id -subNotPositiveInInv env prf1 prf2 (TArrow a b) = - bimap - (subOccursInInv env prf2 a) - (subNotPositiveInInv env prf1 prf2 b) -subNotPositiveInInv env prf1 prf2 (TUnion as) = subNotPositiveInAny1Inv env prf1 prf2 as -subNotPositiveInInv env prf1 prf2 (TProd as) = subNotPositiveInAnyInv env prf1 prf2 as -subNotPositiveInInv env prf1 prf2 (TSum as) = subNotPositiveInAnyInv env prf1 prf2 as -subNotPositiveInInv env prf1 prf2 (TFix a) = - subOccursInInv - (lift (Drop Id) env :< TVar FZ) - (liftEnvOccursUniq env prf2) - a - -subNotPositiveInAnyInv env prf1 prf2 [] = id -subNotPositiveInAnyInv env prf1 prf2 (a :: as) = - bimap - (subNotPositiveInInv env prf1 prf2 a) - (subNotPositiveInAnyInv env prf1 prf2 as) - -subNotPositiveInAny1Inv env prf1 prf2 (a ::: as) = - bimap - (subNotPositiveInInv env prf1 prf2 a) - (subNotPositiveInAnyInv env prf1 prf2 as) - --- Ill Formed -- - -subIllFormed : - (env : Env k n (Ty n)) -> (a : Ty k) -> - IllFormed a -> IllFormed (sub env a) -subAnyIllFormed : - (env : Env k n (Ty n)) -> (as : List (Ty k)) -> - AnyIllFormed as -> AnyIllFormed (subAll env as) -subAny1IllFormed : - (env : Env k n (Ty n)) -> (as : List1 (Ty k)) -> - Any1IllFormed as -> Any1IllFormed (subAll1 env as) - -subIllFormed env (TVar i) = absurd -subIllFormed env TNat = id -subIllFormed env (TArrow a b) = bimap (subIllFormed env a) (subIllFormed env b) -subIllFormed env (TUnion as) = subAny1IllFormed env as -subIllFormed env (TProd as) = subAnyIllFormed env as -subIllFormed env (TSum as) = subAnyIllFormed env as -subIllFormed env (TFix a) = - bimap - (subNotPositiveIn (lift (Drop Id) env :< TVar FZ) FZ a $ - rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in - Refl) - (subIllFormed (lift (Drop Id) env :< TVar FZ) a) - -subAnyIllFormed env [] = id -subAnyIllFormed env (a :: as) = bimap (subIllFormed env a) (subAnyIllFormed env as) - -subAny1IllFormed env (a ::: as) = bimap (subIllFormed env a) (subAnyIllFormed env as) - --- Inverse +sub env (TFix x a) = TFix x (sub (lift (Drop Id) env :< (x :- TVar (%% x))) a) -export -0 EnvWellFormed : Env k n (Ty n) -> Type -EnvWellFormed env = (x : Fin k) -> Not (IllFormed $ fromVar $ lookup env x) - -liftEnvWellFormed : - (env : Env k n (Ty n)) -> - EnvWellFormed env -> - EnvWellFormed (lift (Drop Id) env :< TVar FZ) -liftEnvWellFormed env prf FZ = - rewrite lookupFZ (lift (Drop Id) env) (TVar FZ) in - id -liftEnvWellFormed env prf (FS x) = - rewrite lookupFS (lift (Drop Id) env) (TVar FZ) x in - rewrite lookupLift (Drop Id) env x in - rewrite eitherBimapFusion TVar id (index (Drop Id)) (rename (Drop Id)) (lookup env x) in - \ill => - prf x $ - thinIllFormedInv (Drop Id) (either TVar id $ lookup env x) $ - rewrite pushEither (thin (Drop Id)) TVar id (lookup env x) in - ill - -subIllFormedInv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvWellFormed env) -> - (a : Ty k) -> - IllFormed (sub env a) -> IllFormed a -subAnyIllFormedInv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvWellFormed env) -> - (as : List (Ty k)) -> - AnyIllFormed (subAll env as) -> AnyIllFormed as -subAny1IllFormedInv : - (0 env : Env k n (Ty n)) -> - (0 prf : EnvWellFormed env) -> - (as : List1 (Ty k)) -> - Any1IllFormed (subAll1 env as) -> Any1IllFormed as - -subIllFormedInv env prf (TVar i) = \ill => void $ prf i ill -subIllFormedInv env prf TNat = id -subIllFormedInv env prf (TArrow a b) = - bimap - (subIllFormedInv env prf a) - (subIllFormedInv env prf b) -subIllFormedInv env prf (TUnion as) = subAny1IllFormedInv env prf as -subIllFormedInv env prf (TProd as) = subAnyIllFormedInv env prf as -subIllFormedInv env prf (TSum as) = subAnyIllFormedInv env prf as -subIllFormedInv env prf (TFix a) = - bimap - (subNotPositiveInInv - (lift (Drop Id) env :< TVar FZ) - (liftPositiveInFZ env) - (liftOccursUniqFZ env) - a) - (subIllFormedInv - (lift (Drop Id) env :< TVar FZ) - (liftEnvWellFormed env prf) - a) - -subAnyIllFormedInv env prf [] = id -subAnyIllFormedInv env prf (a :: as) = - bimap - (subIllFormedInv env prf a) - (subAnyIllFormedInv env prf as) - -subAny1IllFormedInv env prf (a ::: as) = - bimap - (subIllFormedInv env prf a) - (subAnyIllFormedInv env prf as) - --- Equivalent +subAll env [<] = [<] +subAll env ((:<) as (x :- a) {fresh}) = + (:<) (subAll env as) (x :- sub env a) {fresh = subAllFresh env x as fresh} -export -subIllFormedEquiv : - (env : Env k n (Ty n)) -> - (0 prf : EnvWellFormed env) -> - (a : Ty k) -> - IllFormed a <=> IllFormed (sub env a) -subIllFormedEquiv env prf a = - MkEquivalence - { leftToRight = subIllFormed env a - , rightToLeft = subIllFormedInv env prf a - } +subAllFresh env x [<] = id +subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr index 074d86e..1f2d35b 100644 --- a/src/Inky/Type/Pretty.idr +++ b/src/Inky/Type/Pretty.idr @@ -1,73 +1,43 @@ module Inky.Type.Pretty -import Data.Fin -import Data.Fin.Extra -import Data.List -import Data.String +import Inky.Context import Inky.Type import Text.PrettyPrint.Prettyprinter -asTyChar : Fin 6 -> Char -asTyChar = index' ['X', 'Y', 'Z', 'A', 'B', 'C'] - -export -typeName : Nat -> String -typeName n with (divMod n 6) - typeName _ | Fraction _ 6 q r Refl = - strSnoc - (if q == 0 then "'" else assert_total (typeName $ pred q)) - (asTyChar r) - -arrowPrec, unionPrec, prodPrec, sumPrec, fixPrec : Prec +arrowPrec, prodPrec, sumPrec, fixPrec : Prec arrowPrec = Open -unionPrec = User 2 prodPrec = Open -sumPrec = User 1 +sumPrec = Open fixPrec = Open export -prettyType : {ty : Nat} -> Ty ty -> Prec -> Doc ann -prettyTypeAll : {ty : Nat} -> List (Ty ty) -> Prec -> List (Doc ann) -prettyTypeAll1 : {ty : Nat} -> List1 (Ty ty) -> Prec -> List (Doc ann) +prettyType : {ctx : Context ()} -> Ty ctx () -> Prec -> Doc ann +prettyTypeRow : {ctx : Context ()} -> Row (Ty ctx ()) -> Prec -> List (Doc ann) -prettyType (TVar i) d = pretty (typeName $ finToNat i) +prettyType (TVar i) d = pretty (unVal $ nameOf i) prettyType TNat d = pretty "Nat" prettyType (TArrow a b) d = parenthesise (d > arrowPrec) $ group $ align $ hang 2 $ let parts = stripArrow b in - concatWith (\x, y => x <++> "->" <+> line <+> y) (prettyType a arrowPrec :: parts) + concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts) where - stripArrow : Ty ty -> List (Doc ann) + stripArrow : Ty ctx () -> List (Doc ann) stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b stripArrow a = [prettyType a arrowPrec] -prettyType (TUnion (a ::: [])) d = - parens $ group $ align $ hang 2 $ - prettyType a unionPrec <++> "&" -prettyType (TUnion as) d = - parenthesise (d >= unionPrec) $ group $ align $ hang 2 $ - let parts = prettyTypeAll1 as unionPrec in - concatWith (\x, y => x <++> "&" <+> line <+> y) parts -prettyType (TProd [a]) d = - parens $ group $ align $ hang 2 $ - prettyType a prodPrec <++> "," prettyType (TProd as) d = - parens $ group $ align $ hang 2 $ - let parts = prettyTypeAll as prodPrec in - concatWith (\x, y => x <++> "," <+> line <+> y) parts -prettyType (TSum []) d = "(+)" -prettyType (TSum [a]) d = - parens $ group $ align $ hang 2 $ - prettyType a sumPrec <++> "+" + enclose "<" ">" $ group $ align $ hang 2 $ + let parts = prettyTypeRow as prodPrec in + concatWith (surround $ "," <+> line) parts prettyType (TSum as) d = - parenthesise (d >= sumPrec) $ group $ align $ hang 2 $ - let parts = prettyTypeAll as sumPrec in - concatWith (\x, y => x <++> "+" <+> line <+> y) parts -prettyType (TFix a) d = + enclose "[" "]" $ group $ align $ hang 2 $ + let parts = prettyTypeRow as prodPrec in + concatWith (surround $ "," <+> line) parts +prettyType (TFix x a) d = parens $ group $ align $ hang 2 $ - "\\" <+> pretty (typeName ty) <++> "=>" <+> line <+> + "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a fixPrec -prettyTypeAll [] d = [] -prettyTypeAll (a :: as) d = prettyType a d :: prettyTypeAll as d - -prettyTypeAll1 (a ::: as) d = prettyType a d :: prettyTypeAll as d +prettyTypeRow [<] d = [] +prettyTypeRow (as :< (x :- a)) d = + (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d) + :: prettyTypeRow as d -- cgit v1.2.3