From e258c78a5ab9529242b4c8fa168eda85430e641e Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 28 Oct 2024 15:34:16 +0000 Subject: Make everything relevant. Too few proofs were relevant. Now they are. --- src/Data/Maybe/Decidable.idr | 6 - src/Data/These/Decidable.idr | 16 - src/Inky.idr | 33 +- src/Inky/Context.idr | 646 ------------ src/Inky/Data/Assoc.idr | 26 + src/Inky/Data/Context.idr | 36 + src/Inky/Data/Context/Var.idr | 117 +++ src/Inky/Data/Fun.idr | 55 + src/Inky/Data/Irrelevant.idr | 19 + src/Inky/Data/Row.idr | 151 +++ src/Inky/Data/SnocList.idr | 43 + src/Inky/Data/SnocList/Elem.idr | 110 ++ src/Inky/Data/SnocList/Quantifiers.idr | 46 + src/Inky/Data/SnocList/Thinning.idr | 217 ++++ src/Inky/Data/SnocList/Var.idr | 90 ++ src/Inky/Data/Thinned.idr | 18 + src/Inky/Decidable.idr | 279 ++++++ src/Inky/Decidable/Either.idr | 106 ++ src/Inky/Decidable/Maybe.idr | 146 +++ src/Inky/Parser.idr | 195 ++-- src/Inky/Term.idr | 1708 ++++++++++++++++++-------------- src/Inky/Term/Parser.idr | 363 ++++--- src/Inky/Term/Pretty.idr | 182 ++-- src/Inky/Thinning.idr | 310 ------ src/Inky/Type.idr | 973 ++++++++++++------ src/Inky/Type/Pretty.idr | 44 +- 26 files changed, 3546 insertions(+), 2389 deletions(-) delete mode 100644 src/Data/Maybe/Decidable.idr delete mode 100644 src/Data/These/Decidable.idr delete mode 100644 src/Inky/Context.idr create mode 100644 src/Inky/Data/Assoc.idr create mode 100644 src/Inky/Data/Context.idr create mode 100644 src/Inky/Data/Context/Var.idr create mode 100644 src/Inky/Data/Fun.idr create mode 100644 src/Inky/Data/Irrelevant.idr create mode 100644 src/Inky/Data/Row.idr create mode 100644 src/Inky/Data/SnocList.idr create mode 100644 src/Inky/Data/SnocList/Elem.idr create mode 100644 src/Inky/Data/SnocList/Quantifiers.idr create mode 100644 src/Inky/Data/SnocList/Thinning.idr create mode 100644 src/Inky/Data/SnocList/Var.idr create mode 100644 src/Inky/Data/Thinned.idr create mode 100644 src/Inky/Decidable.idr create mode 100644 src/Inky/Decidable/Either.idr create mode 100644 src/Inky/Decidable/Maybe.idr delete mode 100644 src/Inky/Thinning.idr (limited to 'src') diff --git a/src/Data/Maybe/Decidable.idr b/src/Data/Maybe/Decidable.idr deleted file mode 100644 index e301ab1..0000000 --- a/src/Data/Maybe/Decidable.idr +++ /dev/null @@ -1,6 +0,0 @@ -module Data.Maybe.Decidable - -public export -data OnlyWhen : (p : a -> Type) -> Maybe a -> Type where - RJust : forall x. (px : p x) -> p `OnlyWhen` Just x - RNothing : (false : (x : a) -> Not (p x)) -> p `OnlyWhen` Nothing diff --git a/src/Data/These/Decidable.idr b/src/Data/These/Decidable.idr deleted file mode 100644 index c044ca4..0000000 --- a/src/Data/These/Decidable.idr +++ /dev/null @@ -1,16 +0,0 @@ -module Data.These.Decidable - -import Data.Bool.Decidable -import Data.These - -export -viaEquivalence : a <=> b -> a `Reflects` x -> b `Reflects` x -viaEquivalence eq (RTrue x) = RTrue (eq.leftToRight x) -viaEquivalence eq (RFalse f) = RFalse (f . eq.rightToLeft) - -export -reflectThese : a `Reflects` x -> b `Reflects` y -> These a b `Reflects` x || y -reflectThese (RTrue x) (RTrue y) = RTrue (Both x y) -reflectThese (RTrue x) (RFalse ny) = RTrue (This x) -reflectThese (RFalse nx) (RTrue y) = RTrue (That y) -reflectThese (RFalse nx) (RFalse ny) = RFalse (these nx ny $ const ny) diff --git a/src/Inky.idr b/src/Inky.idr index bd3975f..6a9beff 100644 --- a/src/Inky.idr +++ b/src/Inky.idr @@ -1,20 +1,23 @@ module Inky import Collie + import Control.App import Control.App.Console import Control.App.FileIO -import Inky.Context + +import Inky.Decidable +import Inky.Decidable.Maybe import Inky.Parser import Inky.Term import Inky.Term.Parser import Inky.Term.Pretty -import Inky.Thinning -import Inky.Type import Inky.Type.Pretty + import System.File.Mode import System.File.ReadWrite import System.File.Virtual + import Text.Lexer import Text.PrettyPrint.Prettyprinter import Text.PrettyPrint.Prettyprinter.Render.Terminal @@ -31,7 +34,7 @@ lexInkyString file = do | (_, line, col, rest) => throw "\{show (1 + line)}:\{show col}: unexpected character" pure (filter (\x => relevant x.val.kind) tokens) -parseType : HasErr String es => List (WithBounds InkyToken) -> App es (Ty [<] ()) +parseType : HasErr String es => List (WithBounds InkyToken) -> App es (Ty [<]) parseType toks = do let Ok res [] _ = parse @{EqI} OpenType toks | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input" @@ -40,38 +43,38 @@ parseType toks = do | Left msg => throw msg pure a -parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (CheckTerm [<] [<]) +parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term [<] [<]) parseTerm toks = do - let Ok res [] _ = parse @{EqI} OpenCheck toks + let Ok res [] _ = parse @{EqI} OpenTerm toks | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input" | Err msg => throw msg let Right t = res.try [<] [<] | Left msg => throw msg pure t -checkType : HasErr String es => Ty [<] () -> App es () +checkType : HasErr String es => Ty [<] -> App es () checkType a = do - let False = illFormed a - | True => throw "type ill-formed" + let False `Because` wf = illFormed a + | True `Because` bad => throw "type ill-formed" pure () -checkTerm : HasErr String es => Ty [<] () -> CheckTerm [<] [<] -> App es () +checkTerm : HasErr String es => Ty [<] -> Term [<] [<] -> App es () checkTerm a t = do - let True = checks [<] [<] a t - | False => throw "term ill-typed" + let True `Because` prf = checks [<] [<] a t + | False `Because` contra => throw "term ill-typed" pure () printType : PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> - Ty [<] () -> App es () + Ty [<] -> App es () printType a = do primIO $ renderIO $ layoutSmart opts $ prettyType a Open printTerm : PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> - CheckTerm [<] [<] -> App es () + Term [<] [<] -> App es () printTerm a = do - primIO $ renderIO $ layoutSmart opts $ prettyCheck a Open + primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open readFile : FileIO es => File -> App es String readFile f = do diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr deleted file mode 100644 index 586aae2..0000000 --- a/src/Inky/Context.idr +++ /dev/null @@ -1,646 +0,0 @@ -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 -import Decidable.Equality - --- Contexts -------------------------------------------------------------------- - -export -infix 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 -appendLinLeftNeutral : (ctx : Context a) -> [<] ++ ctx = ctx -appendLinLeftNeutral [<] = Refl -appendLinLeftNeutral (ctx :< x) = cong (:< x) $ appendLinLeftNeutral ctx - -public 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 ------------------------------------------------------------------- - -export prefix 2 %% - -public export -data VarPos : (ctx : Context a) -> (0 x : String) -> a -> Type where - [search ctx] - 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) - -export -Show (VarPos ctx x v) where - show i = show (toNat i) - -export -Show (Var ctx v) where - show i = show 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 - -public export -wknLPos : VarPos ctx1 x v -> Length ctx2 -> VarPos (ctx1 ++ ctx2) x v -wknLPos pos Z = pos -wknLPos pos (S len) = There (wknLPos pos len) - -public export -wknRPos : VarPos ctx2 x v -> VarPos (ctx1 ++ ctx2) x v -wknRPos Here = Here -wknRPos (There pos) = There (wknRPos pos) - -public export -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 - -public export -wknL : {auto len : Length ctx2} -> Var ctx1 v -> Var (ctx1 ++ ctx2) v -wknL i = toVar $ wknLPos i.pos len - -public export -wknR : Var ctx2 v -> Var (ctx1 ++ ctx2) v -wknR i = toVar $ wknRPos i.pos - -public 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 - --- Search - -lookupPos : (x : String) -> (ctx : Context a) -> Maybe (v ** VarPos ctx x v) -lookupPos x [<] = Nothing -lookupPos x (ctx :< (y :- v)) = - case decEq x y of - Yes Refl => Just (v ** Here) - No neq => bimap id There <$> lookupPos x ctx - -export -lookup : (x : String) -> (ctx : Context a) -> Maybe (v ** Var ctx v) -lookup x ctx = bimap id toVar <$> lookupPos x ctx - --- 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 - - public export - indexAllPos : VarPos ctx x v -> All p ctx -> p v - indexAllPos Here (env :< px) = px.value - indexAllPos (There pos) (env :< px) = indexAllPos pos env - - public 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) - - public export - (++) : All p ctx1 -> All p ctx2 -> All p (ctx1 ++ ctx2) - env1 ++ [<] = env1 - env1 ++ env2 :< px = (env1 ++ env2) :< px - - public export - split : Length ctx2 -> All p (ctx1 ++ ctx2) -> (All p ctx1, All p ctx2) - split Z env = (env, [<]) - split (S len) (env :< px) = mapSnd (:< px) $ split len env - --- 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 - - 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 - - export - extend : Row a -> Assoc a -> Maybe (Row a) - extend row (x :- v) = - case choose (x `freshIn` row) of - Left fresh => Just (row :< (x :- v)) - Right _ => Nothing - - -- 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/Data/Assoc.idr b/src/Inky/Data/Assoc.idr new file mode 100644 index 0000000..a009515 --- /dev/null +++ b/src/Inky/Data/Assoc.idr @@ -0,0 +1,26 @@ +module Inky.Data.Assoc + +export +infix 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 (0 p : a -> Type) (x : Assoc a) where + constructor (:-) + 0 name : String + {auto 0 prf : x.name = name} + value : p x.value + + public export + map : (forall x. p x -> q x) -> forall x. Assoc0 p x -> Assoc0 q x + map f (n :- px) = n :- f px diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr new file mode 100644 index 0000000..0d3df99 --- /dev/null +++ b/src/Inky/Data/Context.idr @@ -0,0 +1,36 @@ +module Inky.Data.Context + +import public Inky.Data.Assoc +import public Inky.Data.SnocList + +import Inky.Data.SnocList.Quantifiers + +-- Contexts -------------------------------------------------------------------- + +public export +Context : Type -> Type +Context a = SnocList (Assoc a) + +public export +(.names) : Context a -> SnocList String +[<].names = [<] +(ctx :< nx).names = ctx.names :< nx.name + +export +mapNames : (0 f : a -> b) -> (ctx : Context a) -> (map (map f) ctx).names = ctx.names +mapNames f [<] = Refl +mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx + +-- Construction ---------------------------------------------------------------- + +public export +fromAll : (ctx : Context a) -> All (const b) ctx.names -> Context b +fromAll [<] [<] = [<] +fromAll (ctx :< (n :- _)) (sx :< x) = fromAll ctx sx :< (n :- x) + +export +fromAllNames : + (ctx : Context a) -> (sx : All (const b) ctx.names) -> + (fromAll ctx sx).names = ctx.names +fromAllNames [<] [<] = Refl +fromAllNames (ctx :< (n :- _)) (sx :< x) = cong (:< n) $ fromAllNames ctx sx diff --git a/src/Inky/Data/Context/Var.idr b/src/Inky/Data/Context/Var.idr new file mode 100644 index 0000000..4741580 --- /dev/null +++ b/src/Inky/Data/Context/Var.idr @@ -0,0 +1,117 @@ +module Inky.Data.Context.Var + +import Data.DPair +import Data.Singleton +import Inky.Data.Context +import Inky.Data.SnocList.Elem +import Inky.Decidable +import Inky.Decidable.Maybe + +export +prefix 2 %%, %%% + +public export +record Var (ctx : Context a) (x : a) where + constructor (%%) + 0 name : String + {auto pos : Elem (name :- x) ctx} + +%name Var i, j, k + +public export +toVar : Elem (n :- x) ctx -> Var ctx x +toVar pos = (%%) n {pos} + +public export +ThereVar : Var ctx x -> Var (ctx :< ny) x +ThereVar i = toVar (There i.pos) + +export +Show (Var ctx x) where + show i = show (elemToNat i.pos) + +-- Basic Properties --------------------------------------------------------- + +export +toVarCong : + {0 n, k : String} -> {0 x, y : a} -> + {0 i : Elem (n :- x) ctx} -> {0 j : Elem (k :- y) ctx} -> + i ~=~ j -> toVar i ~=~ toVar j +toVarCong Refl = Refl + +export +posCong : {0 i : Var ctx x} -> {0 j : Var ctx y} -> i = j -> i.pos ~=~ j.pos +posCong Refl = Refl + +export +toVarInjective : + {0 n, k : String} -> {0 x, y : a} -> + {i : Elem (n :- x) ctx} -> {j : Elem (k :- y) ctx} -> + (0 _ : toVar i ~=~ toVar j) -> i ~=~ j +toVarInjective prf = toNatInjective $ toNatCong $ posCong prf + +export +posInjective : {i : Var ctx x} -> {j : Var ctx y} -> (0 _ : i.pos ~=~ j.pos) -> i ~=~ j +posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf + +-- Decidable Equality ---------------------------------------------------------- + +public export +decEq : (i : Var ctx x) -> (j : Var ctx y) -> Dec' (i ~=~ j) +decEq i j = + mapDec (\prf => irrelevantEq $ posInjective prf) posCong $ + decEq i.pos j.pos + +-- Weakening ------------------------------------------------------------------- + +public export +wknL : (len : LengthOf ctx2) => Var ctx1 x -> Var (ctx1 ++ ctx2) x +wknL i = toVar $ wknL i.pos len + +public export +wknR : Var ctx1 x -> Var (ctx2 ++ ctx1) x +wknR i = toVar $ wknR i.pos + +public export +split : {auto len : LengthOf ctx2} -> Var (ctx1 ++ ctx2) x -> Either (Var ctx1 x) (Var ctx2 x) +split i = bimap toVar toVar $ split len i.pos + +public export +lift : + {auto len : LengthOf ctx3} -> + (forall x. Var ctx1 x -> Var ctx2 x) -> + Var (ctx1 ++ ctx3) x -> Var (ctx2 ++ ctx3) x +lift f = either (wknL {len} . f) wknR . split {len} + +-- Names ----------------------------------------------------------------------- + +export +nameOf : {ctx : Context a} -> (i : Var ctx x) -> Singleton i.name +nameOf i = [| (nameOf i.pos).name |] + +-- Search ---------------------------------------------------------------------- + +export +lookup : (n : String) -> (ctx : Context a) -> Maybe (x ** Var ctx x) +lookup n ctx = + case decLookup n ctx of + Just x `Because` pos => Just (x ** toVar pos) + Nothing `Because` _ => Nothing + +namespace Search + public export + data VarPos : String -> a -> (ctx : Context a) -> Type where + [search ctx] + Here : VarPos n x (ctx :< (n :- x)) + There : VarPos n x ctx -> VarPos n x (ctx :< ky) + + %name VarPos pos + + public export + toElem : VarPos n x ctx -> Elem (n :- x) ctx + toElem Here = Here + toElem (There pos) = There (toElem pos) + + public export + (%%%) : (0 n : String) -> {auto pos : VarPos n x ctx} -> Var ctx x + (%%%) n {pos} = toVar $ toElem pos diff --git a/src/Inky/Data/Fun.idr b/src/Inky/Data/Fun.idr new file mode 100644 index 0000000..d9acb7d --- /dev/null +++ b/src/Inky/Data/Fun.idr @@ -0,0 +1,55 @@ +module Inky.Data.Fun + +import public Inky.Data.SnocList.Quantifiers +import Inky.Data.SnocList + +public export +Fun : SnocList Type -> Type -> Type +Fun [<] b = b +Fun (as :< a) b = Fun as (a -> b) + +public export +chain : (len : LengthOf as) -> (b -> c) -> Fun as b -> Fun as c +chain Z f x = f x +chain (S len) f g = chain len (f .) g + +public export +DFun : (as : SnocList Type) -> Fun as Type -> Type +DFun [<] p = p +DFun (as :< a) p = DFun as (chain (lengthOf as) (\f => (x : a) -> f x) p) + +public export +DIFun : (as : SnocList Type) -> Fun as Type -> Type +DIFun [<] p = p +DIFun (as :< a) p = DIFun as (chain (lengthOf as) (\f => {x : a} -> f x) p) + +public export +curry : (len : LengthOf as) -> (HSnocList as -> b) -> Fun as b +curry Z f = f [<] +curry (S len) f = curry len (f .: (:<)) + +public export +uncurry : Fun as b -> HSnocList as -> b +uncurry f [<] = f +uncurry f (sx :< x) = uncurry f sx x + +export +uncurryChain : + (0 g : b -> c) -> (0 f : Fun as b) -> (xs : HSnocList as) -> + uncurry (chain (lengthOf as) g f) xs = g (uncurry f xs) +uncurryChain g f [<] = Refl +uncurryChain g f (sx :< x) = cong (\f => f x) (uncurryChain (g .) f sx) + +export +dcurry : (len : LengthOf as) -> ((xs : HSnocList as) -> uncurry p xs) -> DFun as p +dcurry Z f = f [<] +dcurry (S len) f = + dcurry len (\sx => + replace {p = id} (sym $ uncurryChain (\f => (x : _) -> f x) p sx) + (\x => f (sx :< x))) + +export +duncurry : DFun as p -> (sx : HSnocList as) -> uncurry p sx +duncurry f [<] = f +duncurry f (sx :< x) = + replace {p = id} (uncurryChain (\f => (x : _) -> f x) p sx) (duncurry f sx) x diff --git a/src/Inky/Data/Irrelevant.idr b/src/Inky/Data/Irrelevant.idr new file mode 100644 index 0000000..ca72470 --- /dev/null +++ b/src/Inky/Data/Irrelevant.idr @@ -0,0 +1,19 @@ +module Inky.Data.Irrelevant + +public export +record Irrelevant (a : Type) where + constructor Forget + 0 value : a + +public export +Functor Irrelevant where + map f x = Forget (f x.value) + +public export +Applicative Irrelevant where + pure x = Forget x + f <*> x = Forget (f.value x.value) + +public export +Monad Irrelevant where + join x = Forget (x.value.value) diff --git a/src/Inky/Data/Row.idr b/src/Inky/Data/Row.idr new file mode 100644 index 0000000..ba0c5f6 --- /dev/null +++ b/src/Inky/Data/Row.idr @@ -0,0 +1,151 @@ +module Inky.Data.Row + +import public Data.So +import public Inky.Data.Context +import public Inky.Data.SnocList.Quantifiers + +import Inky.Data.SnocList.Elem +import Inky.Data.Irrelevant +import Inky.Decidable + +public export +FreshIn : String -> SnocList String -> Type +FreshIn n = All (\x => So (x /= n)) + +public export +AllFresh : SnocList String -> Type +AllFresh = Pairwise (So .: (/=)) + +public export +record Row (a : Type) where + constructor MkRow + context : Context a + 0 fresh : AllFresh context.names + +%name Row row + +public export +(.names) : Row a -> SnocList String +row.names = row.context.names + +-- Interfaces ------------------------------------------------------------------ + +public export +Functor Row where + map f row = MkRow (map (map f) row.context) (rewrite mapNames f row.context in row.fresh) + +public export +Foldable Row where + foldr f x row = foldr (\x, y => f x.value y) x row.context + foldl f x row = foldl (\x, y => f x y.value) x row.context + null row = null row.context + foldlM f x row = foldlM (\x, y => f x y.value) x row.context + foldMap f row = foldMap (f . value) row.context + +-- Equality -------------------------------------------------------------------- + +export +soUnique : (prf1, prf2 : So b) -> prf1 = prf2 +soUnique Oh Oh = Refl + +export +freshInUnique : (freshIn1, freshIn2 : x `FreshIn` sx) -> freshIn1 = freshIn2 +freshInUnique [<] [<] = Refl +freshInUnique (freshIn1 :< prf1) (freshIn2 :< prf2) = + cong2 (:<) (freshInUnique freshIn1 freshIn2) (soUnique prf1 prf2) + +export +freshUnique : (fresh1, fresh2 : AllFresh sx) -> fresh1 = fresh2 +freshUnique [<] [<] = Refl +freshUnique (fresh1 :< freshIn1) (fresh2 :< freshIn2) = + cong2 (:<) (freshUnique fresh1 fresh2) (freshInUnique freshIn1 freshIn2) + +export +rowCong : + {0 ctx1, ctx2 : Context a} -> + {0 fresh1 : AllFresh ctx1.names} -> + {0 fresh2 : AllFresh ctx2.names} -> + ctx1 = ctx2 -> MkRow ctx1 fresh1 = MkRow ctx2 fresh2 +rowCong Refl = rewrite freshUnique fresh1 fresh2 in Refl + +-- Smart Constructors ---------------------------------------------------------- + +public export +Lin : Row a +Lin = MkRow [<] [<] + +public export +(:<) : + (row : Row a) -> (x : Assoc a) -> + (0 fresh : x.name `FreshIn` row.names) => + Row a +row :< x = MkRow (row.context :< x) (row.fresh :< fresh) + +public export +fromAll : (row : Row a) -> All (const b) row.names -> Row b +fromAll row sx = MkRow (fromAll row.context sx) (rewrite fromAllNames row.context sx in row.fresh) + +-- Operations ------------------------------------------------------------------ + +export +isFresh : + (names : SnocList String) -> + (name : String) -> + Dec' (Irrelevant $ name `FreshIn` names) +isFresh names name = + map irrelevant (\contra, prfs => anyNegAll contra $ relevant names prfs.value) $ + all (\x => (decSo $ x /= name).forget) names + +export +extend : Row a -> Assoc a -> Maybe (Row a) +extend row x with (isFresh row.names x.name) + _ | True `Because` Forget prf = Just (row :< x) + _ | False `Because` _ = Nothing + +-- Search ---------------------------------------------------------------------- + +noLookupFresh : + (ctx : Context a) -> + (0 freshIn : n `FreshIn` ctx.names) -> + Not (Elem (n :- x) ctx) +noLookupFresh (sx :< (n :- x)) (freshIn :< prf) Here with ((decEq n n).reason) | ((decEq n n).does) + _ | _ | True = void $ absurd prf + _ | contra | False = void $ contra Refl +noLookupFresh (sx :< (k :- _)) (freshIn :< prf) (There i) = noLookupFresh sx freshIn i + +doLookupUnique : + (ctx : Context a) -> + (0 fresh : AllFresh ctx.names) -> + (i : Elem (n :- x) ctx) -> + (j : Elem (n :- y) ctx) -> + the (x ** Elem (n :- x) ctx) (x ** i) = (y ** j) +doLookupUnique (ctx :< (n :- x)) (fresh :< freshIn) Here Here = Refl +doLookupUnique (ctx :< (n :- x)) (fresh :< freshIn) Here (There j) = void $ noLookupFresh ctx freshIn j +doLookupUnique (ctx :< (n :- z)) (fresh :< freshIn) (There i) Here = void $ noLookupFresh ctx freshIn i +doLookupUnique (ctx :< (k :- z)) (fresh :< freshIn) (There i) (There j) = + cong (\(x ** i) => (x ** There i)) $ + doLookupUnique ctx fresh i j + +export +lookupUnique : + (row : Row a) -> + (i : Elem (n :- x) row.context) -> + (j : Elem (n :- y) row.context) -> + the (x ** Elem (n :- x) row.context) (x ** i) = (y ** j) +lookupUnique row i j = doLookupUnique row.context row.fresh i j + +-- Removal --------------------------------------------------------------------- + +dropElemFreshIn : + (ctx : Context a) -> n `FreshIn` ctx.names -> (i : Elem nx ctx) -> + n `FreshIn` (dropElem ctx i).names +dropElemFreshIn (ctx :< (n :- x)) (freshIn :< prf) Here = freshIn +dropElemFreshIn (ctx :< (n :- x)) (freshIn :< prf) (There i) = dropElemFreshIn ctx freshIn i :< prf + +export +dropElemFresh : + (ctx : Context a) -> AllFresh ctx.names -> (i : Elem nx ctx) -> + AllFresh (dropElem ctx i).names +dropElemFresh (ctx :< (n :- x)) (fresh :< freshIn) Here = fresh +dropElemFresh (ctx :< (n :- x)) (fresh :< freshIn) (There i) = + dropElemFresh ctx fresh i :< dropElemFreshIn ctx freshIn i diff --git a/src/Inky/Data/SnocList.idr b/src/Inky/Data/SnocList.idr new file mode 100644 index 0000000..494e8cc --- /dev/null +++ b/src/Inky/Data/SnocList.idr @@ -0,0 +1,43 @@ +module Inky.Data.SnocList + +import public Data.SnocList +import public Data.SnocList.Operations + +import Inky.Decidable.Maybe + +public export +data LengthOf : SnocList a -> Type where + Z : LengthOf [<] + S : LengthOf sx -> LengthOf (sx :< x) + +%name LengthOf len + +public export +lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy) +lengthOfAppend len1 Z = len1 +lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2) + +public export +lengthOf : (sx : SnocList a) -> LengthOf sx +lengthOf [<] = Z +lengthOf (sx :< x) = S (lengthOf sx) + +export +lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2 +lengthUnique Z Z = Refl +lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2 + +export +isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<]) +isSnoc [<] = Nothing `Because` Refl +isSnoc (sx :< x) = Just (sx, x) `Because` Refl + +public export +replicate : Nat -> a -> SnocList a +replicate 0 x = [<] +replicate (S n) x = replicate n x :< x + +public export +lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x) +lengthOfReplicate 0 x = Z +lengthOfReplicate (S k) x = S (lengthOfReplicate k x) diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr new file mode 100644 index 0000000..465e92c --- /dev/null +++ b/src/Inky/Data/SnocList/Elem.idr @@ -0,0 +1,110 @@ +module Inky.Data.SnocList.Elem + +import public Data.SnocList.Elem + +import Data.DPair +import Data.Nat +import Data.Singleton +import Inky.Decidable +import Inky.Decidable.Maybe +import Inky.Data.Assoc +import Inky.Data.SnocList + +export +Uninhabited (Here {sx, x} ~=~ There {sx = sy, x = z, y} i) where + uninhabited Refl impossible + +export +Uninhabited (There {sx = sy, x = z, y} i ~=~ Here {sx, x}) where + uninhabited Refl impossible + +export +thereCong : + {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> + There {y = z} i = There {y = z} j +thereCong Refl = Refl + +export +toNatCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> elemToNat i = elemToNat j +toNatCong Refl = Refl + +export +thereInjective : + {0 i : Elem x sx} -> {0 j : Elem y sx} -> There {y = z} i = There {y = z} j -> + i = j +thereInjective Refl = Refl + +export +toNatInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : elemToNat i = elemToNat 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 + +-- Decidable Equality ----------------------------------------------------------- + +public export +reflectEq : (i : Elem x sx) -> (j : Elem y sx) -> (i = j) `When` (elemToNat i == elemToNat j) +reflectEq Here Here = Refl +reflectEq Here (There j) = absurd +reflectEq (There i) Here = absurd +reflectEq (There i) (There j) = mapWhen thereCong thereInjective $ reflectEq i j + +public export +decEq : (i : Elem x sx) -> (j : Elem y sx) -> Dec' (i = j) +decEq i j = (elemToNat i == elemToNat j) `Because` reflectEq i j + +-- Weakening ------------------------------------------------------------------- + +public export +wknL : Elem x sx -> LengthOf sy -> Elem x (sx ++ sy) +wknL pos Z = pos +wknL pos (S len) = There (wknL pos len) + +public export +wknR : Elem x sx -> Elem x (sy ++ sx) +wknR Here = Here +wknR (There pos) = There (wknR pos) + +public export +split : LengthOf sy -> Elem x (sx ++ sy) -> Either (Elem x sx) (Elem x sy) +split Z pos = Left pos +split (S len) Here = Right Here +split (S len) (There pos) = mapSnd There $ split len pos + +-- Lookup ---------------------------------------------------------------------- + +export +nameOf : {sx : SnocList a} -> Elem x sx -> Singleton x +nameOf Here = Val x +nameOf (There pos) = nameOf pos + +-- Search ---------------------------------------------------------------------- + +export +lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Elem x sx) +lookup x [<] = Nothing +lookup x (sx :< y) = + case decEq x y of + True `Because` Refl => Just Here + False `Because` _ => There <$> lookup x sx + +public export +decLookup : (n : String) -> (sx : SnocList (Assoc a)) -> DecWhen a (\x => Elem (n :- x) sx) +decLookup n [<] = Nothing `Because` (\_ => absurd) +decLookup n (sx :< (k :- x)) = + map (maybe x id) leftToRight rightToLeft $ + first (decEq n k) (decLookup n sx) + where + leftToRight : + forall n. (m : Maybe a) -> + maybe (n = k) (\y => Elem (n :- y) sx) m -> + Elem (n :- maybe x Basics.id m) (sx :< (k :- x)) + leftToRight Nothing Refl = Here + leftToRight (Just _) prf = There prf + + rightToLeft : + forall n. + (Not (n = k), (y : a) -> Not (Elem (n :- y) sx)) -> + (y : a) -> Not (Elem (n :- y) (sx :< (k :- x))) + rightToLeft (neq, contra) _ Here = neq Refl + rightToLeft (neq, contra) y (There i) = contra y i diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr new file mode 100644 index 0000000..73c6551 --- /dev/null +++ b/src/Inky/Data/SnocList/Quantifiers.idr @@ -0,0 +1,46 @@ +module Inky.Data.SnocList.Quantifiers + +import public Data.SnocList.Quantifiers + +import Data.List.Quantifiers +import Inky.Data.Irrelevant +import Inky.Decidable + +public export +(<><) : All p xs -> All p sx -> All p (xs <>< sx) +sxp <>< [] = sxp +sxp <>< (px :: pxs) = (sxp :< px) <>< pxs + +public export +head : All p (sx :< x) -> p x +head (prfs :< px) = px + +public export +tail : All p (sx :< x) -> All p sx +tail (prfs :< px) = prfs + +public export +HSnocList : SnocList Type -> Type +HSnocList = All id + +public export +all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx) +all f [<] = True `Because` [<] +all f (sx :< x) = + map (\prfs => snd prfs :< fst prfs) (either Here There) $ + both (f x) (all f sx) + +public export +irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx) +irrelevant [<] = Forget [<] +irrelevant (prfs :< px) = [| irrelevant prfs :< px |] + +public export +relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx +relevant [<] _ = [<] +relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs) + +public export +data Pairwise : (a -> a -> Type) -> SnocList a -> Type where + Lin : Pairwise r [<] + (:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x) diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr new file mode 100644 index 0000000..f766069 --- /dev/null +++ b/src/Inky/Data/SnocList/Thinning.idr @@ -0,0 +1,217 @@ +module Inky.Data.SnocList.Thinning + +import Data.DPair +import Data.Nat +import Inky.Data.SnocList +import Inky.Data.SnocList.Var +import Inky.Data.SnocList.Quantifiers +import Inky.Decidable.Maybe + +-------------------------------------------------------------------------------- +-- Thinnings ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +public export +data Thins : SnocList a -> SnocList a -> Type where + Id : sx `Thins` sx + Drop : sx `Thins` sy -> sx `Thins` sy :< x + Keep : sx `Thins` sy -> sx :< x `Thins` sy :< x + +%name Thins f, g, h + +-- Basics + +public export +indexPos : (f : sx `Thins` sy) -> (pos : Elem x sx) -> Elem x sy +indexPos Id pos = pos +indexPos (Drop f) pos = There (indexPos f pos) +indexPos (Keep f) Here = Here +indexPos (Keep f) (There pos) = There (indexPos f pos) + +public export +index : (f : sx `Thins` sy) -> Var sx -> Var sy +index f i = toVar (indexPos f i.pos) + +public export +(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz +Id . g = g +Drop f . g = Drop (f . g) +Keep f . Id = Keep f +Keep f . Drop g = Drop (f . g) +Keep f . Keep g = Keep (f . g) + +-- Basic properties + +export +indexPosInjective : + (f : sx `Thins` sy) -> {i : Elem x sx} -> {j : Elem y sx} -> + (0 _ : elemToNat (indexPos f i) = elemToNat (indexPos f j)) -> 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 +indexPosComp : + (f : sy `Thins` sz) -> (g : sx `Thins` sy) -> (pos : Elem x sx) -> + indexPos (f . g) pos = indexPos f (indexPos g pos) +indexPosComp Id g pos = Refl +indexPosComp (Drop f) g pos = cong There (indexPosComp f g pos) +indexPosComp (Keep f) Id pos = Refl +indexPosComp (Keep f) (Drop g) pos = cong There (indexPosComp f g pos) +indexPosComp (Keep f) (Keep g) Here = Refl +indexPosComp (Keep f) (Keep g) (There pos) = cong There (indexPosComp f g pos) + +-- Congruence ------------------------------------------------------------------ + +export +infix 6 ~~~ + +public export +data (~~~) : sx `Thins` sy -> sx `Thins` sz -> Type where + IdId : Id ~~~ Id + IdKeep : Id ~~~ f -> Id ~~~ Keep f + KeepId : f ~~~ Id -> Keep f ~~~ Id + DropDrop : f ~~~ g -> Drop f ~~~ Drop g + KeepKeep : f ~~~ g -> Keep f ~~~ Keep g + +%name Thinning.(~~~) prf + +export +(.indexPos) : f ~~~ g -> (pos : Elem x sx) -> elemToNat (indexPos f pos) = elemToNat (indexPos g pos) +(IdId).indexPos pos = Refl +(IdKeep prf).indexPos Here = Refl +(IdKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos +(KeepId prf).indexPos Here = Refl +(KeepId prf).indexPos (There pos) = cong S $ prf.indexPos pos +(DropDrop prf).indexPos pos = cong S $ prf.indexPos pos +(KeepKeep prf).indexPos Here = Refl +(KeepKeep prf).indexPos (There pos) = cong S $ prf.indexPos pos + +export +(.index) : + {0 f, g : sx `Thins` sy} -> f ~~~ g -> (i : Var sx) -> index f i = index g i +prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.indexPos pos + +-- Useful for Parsers ---------------------------------------------------------- + +public export +dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx +dropPos Here = Drop Id +dropPos (There pos) = Keep (dropPos pos) + +public export +dropAll : LengthOf sy -> sx `Thins` sx ++ sy +dropAll Z = Id +dropAll (S len) = Drop (dropAll len) + +public export +keepAll : LengthOf sz -> sx `Thins` sy -> sx ++ sz `Thins` sy ++ sz +keepAll Z f = f +keepAll (S len) f = Keep (keepAll len f) + +public export +append : + sx `Thins` sz -> sy `Thins` sw -> + {auto len : LengthOf sw} -> + sx ++ sy `Thins` sz ++ sw +append f Id = keepAll len f +append f (Drop g) {len = S len} = Drop (append f g) +append f (Keep g) {len = S len} = Keep (append f g) + +public export +assoc : LengthOf sz -> sx ++ (sy ++ sz) `Thins` (sx ++ sy) ++ sz +assoc Z = Id +assoc (S len) = Keep (assoc len) + +public export +growLengthOf : sx `Thins` sy -> LengthOf sx -> LengthOf sy +growLengthOf Id len = len +growLengthOf (Drop f) len = S (growLengthOf f len) +growLengthOf (Keep f) (S len) = S (growLengthOf f len) + +public export +thinLengthOf : sx `Thins` sy -> LengthOf sy -> LengthOf sx +thinLengthOf Id len = len +thinLengthOf (Drop f) (S len) = thinLengthOf f len +thinLengthOf (Keep f) (S len) = S (thinLengthOf f len) + +public export +thinAll : sx `Thins` sy -> All p sy -> All p sx +thinAll Id env = env +thinAll (Drop f) (env :< px) = thinAll f env +thinAll (Keep f) (env :< px) = thinAll f env :< px + +public export +splitL : + {0 sx, sy, sz : SnocList a} -> + LengthOf sz -> + sx `Thins` sy ++ sz -> + Exists (\sxA => Exists (\sxB => (sx = sxA ++ sxB, sxA `Thins` sy, sxB `Thins` sz))) +splitL Z f = Evidence sx (Evidence [<] (Refl, f, Id)) +splitL (S len) Id = Evidence sy (Evidence sz (Refl, Id, Id)) +splitL (S len) (Drop f) = + let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in + Evidence sxA (Evidence sxB (Refl, g, Drop h)) +splitL (S len) (Keep f) = + let Evidence sxA (Evidence sxB (Refl, g, h)) = splitL len f in + Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h)) + +public export +splitR : + {0 sx, sy, sz : SnocList a} -> + LengthOf sy -> + sx ++ sy `Thins` sz -> + Exists (\sxA => Exists (\sxB => (sz = sxA ++ sxB, sx `Thins` sxA, sy `Thins` sxB))) +splitR Z f = Evidence sz (Evidence [<] (Refl, f, Id)) +splitR (S len) Id = Evidence sx (Evidence sy (Refl, Id, Id)) +splitR (S len) (Drop f) = + let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR (S len) f in + Evidence sxA (Evidence (sxB :< _) (Refl, g, Drop h)) +splitR (S len) (Keep f) = + let Evidence sxA (Evidence sxB (Refl, g, h)) = splitR len f in + Evidence sxA (Evidence (sxB :< _) (Refl, g, Keep h)) + +-- Strengthening --------------------------------------------------------------- + +public export +data Skips : sx `Thins` sy -> Elem y sy -> Type where + Here : Drop f `Skips` Here + Also : f `Skips` i -> Drop f `Skips` There i + There : f `Skips` i -> Keep f `Skips` There i + +%name Skips skips + +public export +strengthen : + (f : sx `Thins` sy) -> (i : Elem y sy) -> + Proof (Elem y sx) (\j => i = indexPos f j) (f `Skips` i) +strengthen Id i = Just i `Because` Refl +strengthen (Drop f) Here = Nothing `Because` Here +strengthen (Drop f) (There i) = + map id (\_, prf => cong There prf) Also $ + strengthen f i +strengthen (Keep f) Here = Just Here `Because` Refl +strengthen (Keep f) (There i) = + map There (\_, prf => cong There prf) There $ + strengthen f i + +export +skipsDropPos : (i : Elem x sx) -> dropPos i `Skips` j -> i ~=~ j +skipsDropPos Here Here = Refl +skipsDropPos (There i) (There skips) = thereCong (skipsDropPos i skips) + +------------------------ ------------------------------------------------------- +-- Renaming Coalgebras --------------------------------------------------------- +-------------------------------------------------------------------------------- + +public export +interface Rename (0 a : Type) (0 t : SnocList a -> Type) where + rename : + {0 sx, sy : SnocList a} -> sx `Thins` sy -> + t sx -> t sy + 0 renameCong : + {0 sx, sy : SnocList a} -> {0 f, g : sx `Thins` sy} -> f ~~~ g -> + (x : t sx) -> rename f x = rename g x + 0 renameId : {0 sx : SnocList a} -> (x : t sx) -> rename Id x = x diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr new file mode 100644 index 0000000..cc7c088 --- /dev/null +++ b/src/Inky/Data/SnocList/Var.idr @@ -0,0 +1,90 @@ +module Inky.Data.SnocList.Var + +import public Inky.Data.SnocList.Elem + +import Data.Singleton +import Inky.Data.SnocList +import Inky.Decidable + +export +prefix 2 %% + +public export +record Var (sx : SnocList a) where + constructor (%%) + 0 name : a + {auto pos : Elem name sx} + +%name Var i, j, k + +public export +toVar : Elem x sx -> Var sx +toVar pos = (%%) x {pos} + +public export +ThereVar : Var sx -> Var (sx :< x) +ThereVar i = toVar (There i.pos) + +export +Show (Var sx) where + show i = show (elemToNat i.pos) + +-- Basic Properties --------------------------------------------------------- + +export +toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j +toVarCong Refl = Refl + +export +posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos +posCong Refl = Refl + +export +toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j +toVarInjective prf = toNatInjective $ toNatCong $ posCong prf + +export +posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j +posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf + +-- Decidable Equality ---------------------------------------------------------- + +public export +DecEq' (Var {a} sx) where + does i j = (decEq i.pos j.pos).does + reason i j = + mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $ + (decEq i.pos j.pos).reason + +-- Weakening ------------------------------------------------------------------- + +public export +wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy) +wknL i = toVar $ wknL i.pos len + +public export +wknR : Var sx -> Var (sy ++ sx) +wknR i = toVar $ wknR i.pos + +public export +split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy) +split i = bimap toVar toVar $ split len i.pos + +public export +lift1 : + (Var sx -> Var sy) -> + Var (sx :< x) -> Var (sy :< y) +lift1 f ((%%) x {pos = Here}) = %% y +lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name) + +-- Names ----------------------------------------------------------------------- + +export +nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name +nameOf i = nameOf i.pos + +-- Search ---------------------------------------------------------------------- + +export +lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx) +lookup x sx = toVar <$> lookup x sx diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr new file mode 100644 index 0000000..6ee0d50 --- /dev/null +++ b/src/Inky/Data/Thinned.idr @@ -0,0 +1,18 @@ +module Inky.Data.Thinned + +import public Inky.Data.SnocList.Thinning + +public export +record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where + constructor Over + {0 support : SnocList a} + value : p support + thins : support `Thins` ctx + +public export +rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2 +rename f (value `Over` thins) = value `Over` (f . thins) + +public export +(.extract) : Rename a p => Thinned p ctx -> p ctx +(value `Over` thins).extract = rename thins value diff --git a/src/Inky/Decidable.idr b/src/Inky/Decidable.idr new file mode 100644 index 0000000..860f9e2 --- /dev/null +++ b/src/Inky/Decidable.idr @@ -0,0 +1,279 @@ +module Inky.Decidable + +import public Inky.Decidable.Either + +import Data.Bool +import Data.Either +import Data.Maybe +import Data.List +import Data.List1 +import Data.List1.Properties +import Data.Nat +import Data.SnocList +import Data.So +import Data.These +import Data.Vect + +import Decidable.Equality +import Inky.Data.Irrelevant + +public export +When : Type -> Bool -> Type +When a = Union a (Not a) + +public export +Dec' : (0 _ : Type) -> Type +Dec' a = LazyEither a (Not a) + +-- Operations ------------------------------------------------------------------ + +-- Conversion to Dec + +public export +fromDec : Dec a -> Dec' a +fromDec (Yes prf) = True `Because` prf +fromDec (No contra) = False `Because` contra + +public export +toDec : Dec' a -> Dec a +toDec (True `Because` prf) = Yes prf +toDec (False `Because` contra) = No contra + +-- So + +public export +decSo : (b : Bool) -> Dec' (So b) +decSo b = b `Because` (if b then Oh else absurd) + +-- Irrelevant + +public export +forgetWhen : {b : Bool} -> a `When` b -> Irrelevant a `When` b +forgetWhen {b = True} prf = Forget prf +forgetWhen {b = False} contra = \prf => void $ contra $ prf.value + +public export +(.forget) : Dec' a -> Dec' (Irrelevant a) +p.forget = p.does `Because` forgetWhen p.reason + +-- Negation + +public export +notWhen : {b : Bool} -> a `When` b -> Not a `When` not b +notWhen = Union.map id (\prf, contra => contra prf) . Union.not + +public export +notDec : Dec' a -> Dec' (Not a) +notDec p = not p.does `Because` notWhen p.reason + +-- Maps + +public export +mapWhen : (a -> a') -> (0 _ : a' -> a) -> {b : Bool} -> a `When` b -> a' `When` b +mapWhen f g = Union.map f (\contra, prf => void $ contra $ g prf) + +public export +mapDec : (a -> b) -> (0 _ : b -> a) -> Dec' a -> Dec' b +mapDec f g = map f (\contra, prf => void $ contra $ g prf) + +-- Conjunction + +public export +andWhen : {b1, b2 : Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> (a1, a2) `When` (b1 && b2) +andWhen x y = + Union.map {d = Not (a1, a2)} id (\x, (y, z) => either (\f => f y) (\g => g z) x) $ + Union.both x y + +public export +andDec : Dec' a -> Dec' b -> Dec' (a, b) +andDec p q = (p.does && q.does) `Because` andWhen p.reason q.reason + +-- Disjunction + +public export +elseWhen : {b1, b2 : Bool} -> a1 `When` b1 -> Lazy (a2 `When` b2) -> Either a1 a2 `When` (b1 || b2) +elseWhen x y = + Union.map {b = (Not a1, Not a2)} id (\(f, g) => either f g) $ + Union.first x y + +public export +elseDec : Dec' a -> Dec' b -> Dec' (Either a b) +elseDec p q = (p.does || q.does) `Because` elseWhen p.reason q.reason + +public export +orWhen : {b1, b2 : Bool} -> a1 `When` b1 -> a2 `When` b2 -> These a1 a2 `When` (b1 || b2) +orWhen x y = + Union.map {b = (Not a1, Not a2)} id (\(f, g) => these f g (const g)) $ + Union.any x y + +public export +orDec : Dec' a -> Dec' b -> Dec' (These a b) +orDec p q = (p.does || q.does) `Because` orWhen p.reason q.reason + +-- Dependent Versions + +public export +thenDec : + (0 b : a -> Type) -> + (0 unique : (x, y : a) -> b x -> b y) -> + Dec' a -> ((x : a) -> Dec' (b x)) -> Dec' (x ** b x) +thenDec b unique p f = + map id + (\contra, (x ** prf) => + either + (\contra => contra x) + (\yContra => void $ snd yContra $ unique x (fst yContra) prf) + contra) $ + andThen p f + +-- Equality -------------------------------------------------------------------- + +public export +interface DecEq' (0 a : Type) where + does : (x, y : a) -> Bool + reason : (x, y : a) -> (x = y) `When` (does x y) + + decEq : (x, y : a) -> Dec' (x = y) + decEq x y = does x y `Because` reason x y + +public export +whenCong : (0 _ : Injective f) => {b : Bool} -> (x = y) `When` b -> (f x = f y) `When` b +whenCong = mapWhen (\prf => cong f prf) (\prf => inj f prf) + +public export +whenCong2 : + (0 _ : Biinjective f) => + {b1, b2 : Bool} -> + (x = y) `When` b1 -> (z = w) `When` b2 -> + (f x z = f y w) `When` (b1 && b2) +whenCong2 p q = + mapWhen {a = (_, _)} (\prfs => cong2 f (fst prfs) (snd prfs)) (\prf => biinj f prf) $ + andWhen p q + +[ToEq] DecEq' a => Eq a where + x == y = does x y + +-- Instances ------------------------------------------------------------------- + +public export +DecEq' () where + does _ _ = True + reason () () = Refl + +public export +DecEq' Bool where + does b1 b2 = b1 == b2 + + reason False False = Refl + reason False True = absurd + reason True False = absurd + reason True True = Refl + +public export +DecEq' Nat where + does k n = k == n + + reason 0 0 = Refl + reason 0 (S n) = absurd + reason (S k) 0 = absurd + reason (S k) (S n) = whenCong (reason k n) + +public export +(d : DecEq' a) => DecEq' (Maybe a) where + does x y = let _ = ToEq @{d} in x == y + + reason Nothing Nothing = Refl + reason Nothing (Just y) = absurd + reason (Just x) Nothing = absurd + reason (Just x) (Just y) = whenCong (reason x y) + +public export +(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (Either a b) where + does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y + + reason (Left x) (Left y) = whenCong (reason x y) + reason (Left x) (Right y) = absurd + reason (Right x) (Left y) = absurd + reason (Right x) (Right y) = whenCong (reason x y) + + +public export +(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (These a b) where + does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y + + reason (This x) (This y) = whenCong (reason x y) + reason (That x) (That y) = whenCong (reason x y) + reason (Both x z) (Both y w) = whenCong2 (reason x y) (reason z w) + reason (This x) (That y) = \case Refl impossible + reason (This x) (Both y z) = \case Refl impossible + reason (That x) (This y) = \case Refl impossible + reason (That x) (Both y z) = \case Refl impossible + reason (Both x z) (This y) = \case Refl impossible + reason (Both x z) (That y) = \case Refl impossible + +public export +(d1 : DecEq' a) => (d2 : DecEq' b) => DecEq' (a, b) where + does x y = let _ = ToEq @{d1} in let _ = ToEq @{d2} in x == y + + reason (x, y) (z, w) = whenCong2 (reason x z) (reason y w) + +public export +(d : DecEq' a) => DecEq' (List a) where + does x y = let _ = ToEq @{d} in x == y + + reason [] [] = Refl + reason [] (y :: ys) = absurd + reason (x :: xs) [] = absurd + reason (x :: xs) (y :: ys) = whenCong2 (reason x y) (reason xs ys) + +public export +(d : DecEq' a) => DecEq' (List1 a) where + does x y = let _ = ToEq @{d} in x == y + + reason (x ::: xs) (y ::: ys) = whenCong2 (reason x y) (reason xs ys) + +public export +(d : DecEq' a) => DecEq' (SnocList a) where + does x y = let _ = ToEq @{d} in x == y + + reason [<] [<] = Refl + reason [<] (sy :< y) = absurd + reason (sx :< x) [<] = absurd + reason (sx :< x) (sy :< y) = + rewrite sym $ andCommutative (does sx sy) (does x y) in + whenCong2 (reason sx sy) (reason x y) + +-- Other Primitives + +%unsafe +public export +primitiveEq : Eq a => (x, y : a) -> (x = y) `When` (x == y) +primitiveEq x y with (x == y) + _ | True = believe_me (Refl {x}) + _ | False = \prf => believe_me {b = Void} () + +%unsafe +public export +[FromEq] Eq a => DecEq' a where + does x y = x == y + reason x y = primitiveEq x y + +public export +DecEq' Int where + does = does @{FromEq} + reason = reason @{FromEq} + +public export +DecEq' Char where + does = does @{FromEq} + reason = reason @{FromEq} + +public export +DecEq' Integer where + does = does @{FromEq} + reason = reason @{FromEq} + +public export +DecEq' String where + does = does @{FromEq} + reason = reason @{FromEq} diff --git a/src/Inky/Decidable/Either.idr b/src/Inky/Decidable/Either.idr new file mode 100644 index 0000000..9da2c72 --- /dev/null +++ b/src/Inky/Decidable/Either.idr @@ -0,0 +1,106 @@ +module Inky.Decidable.Either + +import Data.These + +public export +Union : Type -> Type -> Bool -> Type +Union a b False = b +Union a b True = a + +public export +record LazyEither (0 a, b : Type) where + constructor Because + does : Bool + reason : Lazy (Union a b does) + +%name LazyEither p, q + +namespace Union + public export + map : {tag : Bool} -> (a -> c) -> (b -> d) -> Union a b tag -> Union c d tag + map {tag = False} f g x = g x + map {tag = True} f g x = f x + + public export + not : {tag : Bool} -> Union a b tag -> Union b a (not tag) + not {tag = False} x = x + not {tag = True} x = x + + public export + both : + {tag1 : Bool} -> {tag2 : Lazy Bool} -> + Union a b tag1 -> Lazy (Union c d tag2) -> + Union (a, c) (Either b d) (tag1 && tag2) + both {tag1 = True, tag2 = True} x y = (x, y) + both {tag1 = True, tag2 = False} x y = Right y + both {tag1 = False} x y = Left x + + public export + first : + {tag1 : Bool} -> {tag2 : Lazy Bool} -> + Union a b tag1 -> Lazy (Union c d tag2) -> + Union (Either a c) (b, d) (tag1 || tag2) + first {tag1 = True} x y = Left x + first {tag1 = False, tag2 = True} x y = Right y + first {tag1 = False, tag2 = False} x y = (x, y) + + public export + all : + {tag1, tag2 : Bool} -> + Union a b tag1 -> Union c d tag2 -> + Union (a, c) (These b d) (tag1 && tag2) + all {tag1 = True, tag2 = True} x y = (x, y) + all {tag1 = True, tag2 = False} x y = That y + all {tag1 = False, tag2 = True} x y = This x + all {tag1 = False, tag2 = False} x y = Both x y + + public export + any : + {tag1, tag2 : Bool} -> + Union a b tag1 -> Union c d tag2 -> + Union (These a c) (b, d) (tag1 || tag2) + any {tag1 = True, tag2 = True} x y = Both x y + any {tag1 = True, tag2 = False} x y = This x + any {tag1 = False, tag2 = True} x y = That y + any {tag1 = False, tag2 = False} x y = (x, y) + +public export +map : (a -> c) -> (b -> d) -> LazyEither a b -> LazyEither c d +map f g p = p.does `Because` Union.map f g p.reason + +public export +not : LazyEither a b -> LazyEither b a +not p = not p.does `Because` Union.not p.reason + +public export +both : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (Either b d) +both p q = p.does && q.does `Because` Union.both p.reason q.reason + +public export +first : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (Either a c) (b, d) +first p q = p.does || q.does `Because` Union.first p.reason q.reason + +public export +all : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (a, c) (These b d) +all p q = p.does && q.does `Because` Union.all p.reason q.reason + +public export +any : LazyEither a b -> Lazy (LazyEither c d) -> LazyEither (These a c) (b, d) +any p q = p.does || q.does `Because` Union.any p.reason q.reason + +export autobind infixr 0 >=> + +public export +andThen : + {0 p, q : a -> Type} -> + LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) -> + LazyEither (x ** p x) (Either b (x ** q x)) +andThen (True `Because` x) f = map (\px => (x ** px)) (\qx => Right (x ** qx)) (f x) +andThen (False `Because` y) f = False `Because` (Left y) + +public export +(>=>) : + {0 p, q : a -> Type} -> + LazyEither a b -> ((x : a) -> LazyEither (p x) (q x)) -> + LazyEither (x ** p x) (Either b (x ** q x)) +(>=>) = andThen diff --git a/src/Inky/Decidable/Maybe.idr b/src/Inky/Decidable/Maybe.idr new file mode 100644 index 0000000..2f1d83c --- /dev/null +++ b/src/Inky/Decidable/Maybe.idr @@ -0,0 +1,146 @@ +module Inky.Decidable.Maybe + +import Data.Maybe +import Data.These +import Inky.Decidable.Either + +public export +WhenJust : (a -> Type) -> Type -> Maybe a -> Type +WhenJust p b (Just x) = p x +WhenJust p b Nothing = b + +public export +record Proof (0 a : Type) (0 p : a -> Type) (0 b : Type) where + constructor Because + does : Maybe a + reason : WhenJust p b does + +%name Proof p, q + +public export +DecWhen : (0 a : Type) -> (0 p : a -> Type) -> Type +DecWhen a p = Proof a p ((x : a) -> Not (p x)) + +-- Operations ------------------------------------------------------------------ + +public export +(.forget) : Proof a p b -> LazyEither (x ** p x) b +(Just x `Because` px).forget = True `Because` (x ** px) +(Nothing `Because` y).forget = False `Because` y + +public export +map : + (f : a -> a') -> + ((x : a) -> p x -> q (f x)) -> + (b -> b') -> + Proof a p b -> Proof a' q b' +map f g h (Just x `Because` px) = Just (f x) `Because` g x px +map f g h (Nothing `Because` y) = Nothing `Because` h y + +export autobind infixr 0 >=> + +public export +andThen : + {0 q : a -> a' -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof a' (q x) (b' x)) -> + Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) +andThen (Just x `Because` px) f = map (x,) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x +andThen (Nothing `Because` y) f = Nothing `Because` Left y + +public export +(>=>) : + {0 q : a -> a' -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof a' (q x) (b' x)) -> + Proof (a, a') (\xy => (p (fst xy), uncurry q xy)) (Either b (x ** (p x, b' x))) +(>=>) = andThen + +public export +andThen' : + {0 a' : a -> Type} -> + {0 q : (x : a) -> a' x -> Type} -> + {0 b' : a -> Type} -> + Proof a p b -> + ((x : a) -> Proof (a' x) (q x) (b' x)) -> + Proof (x ** a' x) (\xy => (p (fst xy), q (fst xy) (snd xy))) (Either b (x ** (p x, b' x))) +andThen' (Just x `Because` px) f = + map (\y => (x ** y)) (\_ => (px,)) (\y => Right (x ** (px, y))) $ f x +andThen' (Nothing `Because` y) f = Nothing `Because` Left y + +public export +all : + Proof a p b -> + Proof a' q b' -> + Proof (a, a') (\xy => (p (fst xy), q (snd xy))) (These b b') +all (Just x `Because` px) (Just y `Because` py) = Just (x, y) `Because` (px, py) +all (Just x `Because` px) (Nothing `Because` y) = Nothing `Because` That y +all (Nothing `Because` x) q = + Nothing `Because` + case q of + (Just _ `Because` _) => This x + (Nothing `Because` y) => Both x y + +public export +first : + Proof a p b -> + Lazy (Proof c q d) -> + Proof (Either a c) (either p q) (b, d) +first (Just x `Because` px) q = Just (Left x) `Because` px +first (Nothing `Because` x) (Just y `Because` py) = Just (Right y) `Because` py +first (Nothing `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) + +namespace Either + public export + andThen : + (0 c : a -> Type) -> + (0 p : (x : a) -> c x -> Type) -> + (0 d : a -> Type) -> + LazyEither a b -> ((x : a) -> Proof (c x) (p x) (d x)) -> + Proof (x ** c x) (\xy => p (fst xy) (snd xy)) (Either b (x ** d x)) + andThen _ _ _ (True `Because` x) f = map (\y => (x ** y)) (\_ => id) (\y => Right (x ** y)) (f x) + andThen _ _ _ (False `Because` y) f = Nothing `Because` Left y + + public export + first : + LazyEither a b -> + Lazy (Proof c p d) -> + Proof (Maybe c) (maybe a p) (b, d) + first (True `Because` x) q = Just Nothing `Because` x + first (False `Because` x) (Just y `Because` py) = Just (Just y) `Because` py + first (False `Because` x) (Nothing `Because` y) = Nothing `Because` (x, y) + + public export + all : LazyEither a b -> Lazy (Proof c p d) -> Proof c (\x => (a, p x)) (These b d) + all (True `Because` x) (Just y `Because` py) = Just y `Because` (x, py) + all (True `Because` x) (Nothing `Because` y) = Nothing `Because` That y + all (False `Because` x) q = + Nothing `Because` + case q of + (Just y `Because` _) => This x + (Nothing `Because` y) => Both x y + +namespace Elim + export autobind infixr 0 >=> + + public export + andThen : + {0 q, r : a -> Type} -> + Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> + LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) + andThen (Just x `Because` px) f = map (\qx => (x ** (px, qx))) (\rx => Right (x ** (px, rx))) (f x) + andThen (Nothing `Because` y) f = False `Because` Left y + + public export + (>=>) : + {0 q, r : a -> Type} -> + Proof a p b -> ((x : a) -> LazyEither (q x) (r x)) -> + LazyEither (x ** (p x, q x)) (Either b (x ** (p x, r x))) + (>=>) = andThen + +public export +pure : (x : a) -> LazyEither (b x) c -> Proof a b c +pure x (True `Because` y) = Just x `Because` y +pure x (False `Because` y) = Nothing `Because` y diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr index fc553ec..94d8eb8 100644 --- a/src/Inky/Parser.idr +++ b/src/Inky/Parser.idr @@ -1,17 +1,19 @@ module Inky.Parser import public Data.List.Quantifiers -import public Data.Nat import Control.WellFounded import Data.Bool import Data.DPair import Data.List import Data.List1 +import Data.Nat import Data.So import Data.String.Extra -import Inky.Context -import Inky.Thinning +import Inky.Data.Context +import Inky.Data.Context.Var +import Inky.Data.SnocList.Quantifiers +import Inky.Data.SnocList.Thinning import Text.Lexer export @@ -74,23 +76,24 @@ public export rename : locked1 `Thins` locked2 -> free1 `Thins` free2 -> - {auto len : Length locked2} -> + {auto len : LengthOf locked2} -> Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a public export renameChain : locked1 `Thins` locked2 -> free1 `Thins` free2 -> - {auto len : Length locked2} -> + {auto len : LengthOf locked2} -> ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a public export renameAll : locked1 `Thins` locked2 -> free1 `Thins` free2 -> - {auto len : Length locked2} -> - All.All (\nil => Parser i nil locked1 free1 a) nils -> - All.All (\nil => Parser i nil locked2 free2 a) nils + {auto len : LengthOf locked2} -> + {0 nils : List Bool} -> + All (\nil => Parser i nil locked1 free1 a) nils -> + All (\nil => Parser i nil locked2 free2 a) nils -rename f g (Var i) = Var (index g i) +rename f g (Var i) = Var (toVar $ indexPos g i.pos) rename f g (Lit text) = Lit text rename f g (Seq ps) = Seq (renameChain f g ps) rename f g (OneOf ps) = OneOf (renameAll f g ps) @@ -107,20 +110,21 @@ renameAll f g (p :: ps) = rename f g p :: renameAll f g ps public export weaken : - (len1 : Length free2) -> - {auto len2 : Length locked} -> + (len1 : LengthOf free2) -> + {auto len2 : LengthOf locked} -> Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a public export weakenChain : - (len1 : Length free2) -> - {auto len2 : Length locked} -> + (len1 : LengthOf free2) -> + {auto len2 : LengthOf locked} -> ParserChain i nil (free2 ++ locked) free1 a -> ParserChain i nil locked (free1 ++ free2) a public export weakenAll : - (len1 : Length free2) -> - {auto len2 : Length locked} -> - All.All (\nil => Parser i nil (free2 ++ locked) free1 a) nils -> - All.All (\nil => Parser i nil locked (free1 ++ free2) a) nils + (len1 : LengthOf free2) -> + {auto len2 : LengthOf locked} -> + {0 nils : List Bool} -> + All (\nil => Parser i nil (free2 ++ locked) free1 a) nils -> + All (\nil => Parser i nil locked (free1 ++ free2) a) nils weaken len1 (Var x) = Var (wknL x) weaken len1 (Lit text) = Lit text @@ -137,6 +141,50 @@ weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 p weakenAll len1 [] = [] weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps +-- Substitution ---------------------------------------------------------------- + +public export +sub : + {auto len : LengthOf locked2} -> + (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> + (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> + Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a +public export +subChain : + {auto len : LengthOf locked2} -> + (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> + (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> + ParserChain i nil locked1 free1 a -> ParserChain i nil locked2 free2 a +public export +subAll : + {auto len : LengthOf locked2} -> + (f : All (Assoc0 $ (\nilA => Parser i (fst nilA) [<] (free2 ++ locked2) (snd nilA))) locked1) -> + (g : All (Assoc0 $ (\nilA => Parser i (fst nilA) locked2 free2 (snd nilA))) free1) -> + {0 nils : List Bool} -> + All (\nil => Parser i nil locked1 free1 a) nils -> All (\nil => Parser i nil locked2 free2 a) nils + +sub f g (Var x) = (indexAll x.pos g).value +sub f g (Lit text) = Lit text +sub f g (Seq ps) = Seq (subChain f g ps) +sub f g (OneOf ps) = OneOf (subAll f g ps) +sub f g (Fix x p) = + Fix x $ + sub + (mapProperty (map $ rename Id (Drop Id)) f :< (x :- Var (%%% x))) + (mapProperty (map $ rename (Drop Id) Id) g) + p +sub f g (Map h p) = Map h (sub f g p) +sub f g (WithBounds p) = WithBounds (sub f g p) + +subChain f g [] = [] +subChain f g ((::) {nil1 = False} p ps) = + sub f g p :: + subChain [<] (mapProperty (map $ weaken len) g ++ f) ps +subChain f g ((::) {nil1 = True} p ps) = sub f g p :: subChain f g ps + +subAll f g [] = [] +subAll f g (p :: ps) = sub f g p :: subAll f g ps + -- Typing ---------------------------------------------------------------------- -- Lists are sufficient, as we assume each symbol appears once. @@ -144,19 +192,20 @@ weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps public export peek : - (env : All (const (List i)) free) -> + (env : All (Assoc0 $ const $ List i) free) -> Parser i nil locked free a -> List i public export peekChain : - (env : All (const (List i)) free) -> + (env : All (Assoc0 $ const $ List i) free) -> ParserChain i nil locked free a -> List i public export peekAll : - (env : All (const (List i)) free) -> - All.All (\nil => Parser i nil locked free a) nils -> - All.All (const $ List i) nils + (env : All (Assoc0 $ const $ List i) free) -> + {0 nils : List Bool} -> + All (\nil => Parser i nil locked free a) nils -> + All (const $ List i) nils -peek env (Var x) = indexAll x env +peek env (Var x) = (indexAll x.pos env).value peek env (Lit text) = [text] peek env (Seq ps) = peekChain env ps peek env (OneOf ps) = concat (forget $ peekAll env ps) @@ -173,27 +222,29 @@ peekAll env (p :: ps) = peek env p :: peekAll env ps public export follow : - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> Parser i nil locked free a -> List i public export followChain : - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> ParserChain i nil locked free a -> List i public export followAll : - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> - All.All (\nil => Parser i nil locked free a) nils -> List i - -follow penv1 penv2 fenv1 fenv2 (Var x) = indexAll x fenv2 + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> + {0 nils : List Bool} -> + All (\nil => Parser i nil locked free a) nils -> + List i + +follow penv1 penv2 fenv1 fenv2 (Var x) = (indexAll x.pos fenv2).value follow penv1 penv2 fenv1 fenv2 (Lit text) = [] follow penv1 penv2 fenv1 fenv2 (Seq ps) = followChain penv1 penv2 fenv1 fenv2 ps follow penv1 penv2 fenv1 fenv2 (OneOf ps) = followAll penv1 penv2 fenv1 fenv2 ps @@ -241,29 +292,30 @@ namespace WellTyped public export wellTyped : (e : Eq i) -> - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> Parser i nil locked free a -> Bool public export wellTypedChain : (e : Eq i) -> - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> ParserChain i nil locked free a -> Bool public export allWellTyped : (e : Eq i) -> - (penv1 : All (const (List i)) locked) -> - (penv2 : All (const (List i)) free) -> - (fenv1 : All (const (List i)) locked) -> - (fenv2 : All (const (List i)) free) -> - All.All (\nil => Parser i nil locked free a) nils -> + (penv1 : All (Assoc0 $ const $ List i) locked) -> + (penv2 : All (Assoc0 $ const $ List i) free) -> + (fenv1 : All (Assoc0 $ const $ List i) locked) -> + (fenv2 : All (Assoc0 $ const $ List i) free) -> + {0 nils : List Bool} -> + All (\nil => Parser i nil locked free a) nils -> Bool wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True @@ -446,8 +498,8 @@ parser : {0 fenv2 : _} -> (0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)) -> (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 -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> M xs nil a parserChain : (e : Eq i) => Interpolation i => @@ -458,8 +510,8 @@ parserChain : {0 fenv2 : _} -> (0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)) -> (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 -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> M xs nil (HList as) parserOneOf : (e : Eq i) => Interpolation i => @@ -472,12 +524,11 @@ parserOneOf : {0 fenv2 : _} -> (0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)) -> (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 -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys xs) -> uncurry (M ys) x)) locked -> + All (Assoc0 (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys xs) -> uncurry (M ys) x)) free -> M xs (any Basics.id nils) a -parser (Var x) wf xs env1 env2 = - indexAll x env2 xs (Lax reflexive) +parser (Var x) wf xs env1 env2 = (indexAll x.pos env2).value xs (Lax reflexive) parser (Lit text) wf xs env1 env2 = take [text] xs parser (Seq ps) wf xs env1 env2 = parserChain ps wf xs env1 env2 @@ -498,10 +549,10 @@ parser (Fix {a, nil} x p) wf xs env1 env2 = sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a} (\ys, rec, lte => f ys - ( mapProperty (\f, zs, 0 prf => f zs $ transX prf lte) env1 + ( mapProperty (map (\f, zs, 0 prf => f zs $ transX prf lte)) env1 :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) ) - (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)) + (mapProperty (map (\f, zs, prf => f zs $ transX prf lte)) env2)) xs (Lax reflexive) parser (Map f p) wf xs env1 env2 = f <$> parser p wf xs env1 env2 @@ -509,8 +560,8 @@ parser (WithBounds p) wf xs env1 env2 = do (irrel, bounds) <- bounds xs rewrite sym $ andTrueNeutral nil x <- parser p wf _ - (mapProperty (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search) env1) - (mapProperty (\f, zs, 0 prf => f zs $ transX prf %search) env2) + (mapProperty (map (\f, zs, 0 prf => f zs $ transX {b2 = True} prf %search)) env1) + (mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env2) pure (MkBounded x irrel bounds) parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive) @@ -521,8 +572,8 @@ parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 = y <- parserChain ps (snd wfs') _ [<] - ( mapProperty (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search) env2 - ++ mapProperty (\f, zs, 0 prf => f zs $ transX prf %search) env1 + ( mapProperty (map (\f, zs, 0 prf => f zs $ forget $ transX {b2 = False} prf %search)) env2 + ++ mapProperty (map (\f, zs, 0 prf => f zs $ transX prf %search)) env1 ) pure (x :: y) parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 = @@ -532,8 +583,8 @@ parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 = rewrite sym $ andTrueNeutral nil2 y <- parserChain ps (snd wfs') _ - (mapProperty (\f, zs, prf => f zs $ transX {b2 = True} prf %search) env1) - (mapProperty (\f, zs, prf => f zs $ transX prf %search) env2) + (mapProperty (map (\f, zs, prf => f zs $ transX {b2 = True} prf %search)) env1) + (mapProperty (map (\f, zs, prf => f zs $ transX prf %search)) env2) pure (x :: y) parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 = @@ -650,24 +701,24 @@ option p = (Just <$> p) <|> pure Nothing public export plus : - {auto len : Length locked} -> + {auto len : LengthOf locked} -> Parser i False locked free a -> Parser i False locked free (List1 a) plus p = Fix "plus" ( uncurry (:::) - <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %% "plus"))) + <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %%% "plus"))) public export star : - {auto len : Length locked} -> + {auto len : LengthOf locked} -> Parser i False locked free a -> Parser i True locked free (List a) star p = maybe [] forget <$> option (plus p) public export sepBy1 : - {auto len : Length locked} -> + {auto len : LengthOf locked} -> (sep : Parser i False locked free ()) -> Parser i False locked free a -> Parser i False locked free (List1 a) @@ -675,7 +726,7 @@ sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p)) public export sepBy : - {auto len : Length locked} -> + {auto len : LengthOf locked} -> (sep : Parser i False locked free ()) -> Parser i False locked free a -> Parser i True locked free (List a) diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 54e51ae..88665ba 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -1,766 +1,994 @@ module Inky.Term -import Data.Bool.Decidable -import Data.DPair -import Data.Maybe.Decidable -import Data.List -import Inky.Context -import Inky.Thinning -import Inky.Type +import public Inky.Data.Thinned +import public Inky.Type + +import Control.Function +import Data.List.Quantifiers +import Data.These +import Inky.Data.SnocList.Quantifiers +import Inky.Decidable +import Inky.Decidable.Maybe + +%hide Prelude.Ops.infixl.(>=>) -------------------------------------------------------------------------------- -- Definition ------------------------------------------------------------------ -------------------------------------------------------------------------------- public export -data SynthTerm : (tyCtx, tmCtx : Context ()) -> Type -public export -data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type - -data SynthTerm where - Var : Var tmCtx v -> SynthTerm tyCtx tmCtx - Lit : Nat -> SynthTerm tyCtx tmCtx - Suc : SynthTerm tyCtx tmCtx - App : - SynthTerm tyCtx tmCtx -> - (args : List (CheckTerm tyCtx tmCtx)) -> - {auto 0 prf : 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 - LetTy : - (x : String) -> Ty tyCtx () -> - CheckTerm (tyCtx :< (x :- ())) tmCtx -> - CheckTerm tyCtx tmCtx - Let : - (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 : Row (CheckTerm tyCtx tmCtx) -> CheckTerm tyCtx tmCtx - Case : - SynthTerm tyCtx tmCtx -> - Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> - CheckTerm tyCtx tmCtx - Contract : CheckTerm tyCtx tmCtx -> CheckTerm tyCtx tmCtx - Fold : - SynthTerm tyCtx tmCtx -> - (x : String) -> CheckTerm tyCtx (tmCtx :< (x :- ())) -> - CheckTerm tyCtx tmCtx - Embed : - SynthTerm tyCtx tmCtx -> - CheckTerm tyCtx tmCtx - -%name SynthTerm e -%name CheckTerm t, u, v +data Term : (tyCtx, tmCtx : SnocList String) -> Type where + Annot : Term tyCtx tmCtx -> Ty tyCtx -> Term tyCtx tmCtx + Var : Var tmCtx -> Term tyCtx tmCtx + Let : Term tyCtx tmCtx -> (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx + LetTy : Ty tyCtx -> (x ** Term (tyCtx :< x) tmCtx) -> Term tyCtx tmCtx + Abs : (bound ** Term tyCtx (tmCtx <>< bound)) -> Term tyCtx tmCtx + App : Term tyCtx tmCtx -> List (Term tyCtx tmCtx) -> Term tyCtx tmCtx + Tup : Row (Term tyCtx tmCtx) -> Term tyCtx tmCtx + Prj : Term tyCtx tmCtx -> (l : String) -> Term tyCtx tmCtx + Inj : (l : String) -> Term tyCtx tmCtx -> Term tyCtx tmCtx + Case : Term tyCtx tmCtx -> Row (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx + Roll : Term tyCtx tmCtx -> Term tyCtx tmCtx + Unroll : Term tyCtx tmCtx -> Term tyCtx tmCtx + Fold : Term tyCtx tmCtx -> (x ** Term tyCtx (tmCtx :< x)) -> Term tyCtx tmCtx + Map : (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term tyCtx tmCtx + GetChildren : (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Term tyCtx tmCtx + +%name Term e, f, t, u -------------------------------------------------------------------------------- -- Well Formed ----------------------------------------------------------------- -------------------------------------------------------------------------------- --- Lookup name in a row -------------------------------------------------------- - -GetAt : String -> Row a -> a -> Type -GetAt x ys y = VarPos (forget ys) x y - -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 - -isProductUnique : (a : Ty tyCtx ()) -> IsProduct a as -> IsProduct a bs -> as = bs -isProductUnique (TProd as) Refl Refl = Refl - -isProduct : Ty tyCtx () -> Maybe (Row (Ty tyCtx ())) -isProduct (TProd as) = Just as -isProduct _ = Nothing - -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) - --- Test if we have a sum ------------------------------------------------------- - -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 ()) -> +public export +data IsFunction : + (bound : List String) -> (a : 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 = - ( dom' ** cod' ** - ( IsFunction bound fun dom' cod' - , ( b ** - ( IsArrow cod' b cod - , dom = dom' :< (x :- b) - )) - )) + where + Done : IsFunction [] a [] a + Step : + IsFunction bound b dom cod -> + IsFunction (x :: bound) (TArrow a b) (a :: dom) cod + +public export +data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type + where + Step1 : + ((b, c : Ty tyCtx) -> Not (a = TArrow b c)) -> + NotFunction (x :: bound) a + Step2 : + NotFunction bound b -> + NotFunction (x :: bound) (TArrow a b) + +%name IsFunction prf +%name NotFunction contra +export 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 - (dom1 ** cod1 ** (isFunc1, (b1 ** (isArrow1, eq1)))) - (dom2 ** cod2 ** (isFunc2, (b2 ** (isArrow2, eq2)))) - with (isFunctionUnique bound a isFunc1 isFunc2) - isFunctionUnique (bound :< (x :- ())) a - (dom ** cod ** (_, (b1 ** (isArrow1, eq1)))) - (dom ** cod ** (_, (b2 ** (isArrow2, eq2)))) - | (Refl, Refl) - with (isArrowUnique cod isArrow1 isArrow2) - isFunctionUnique (bound :< (x :- ())) a - (dom ** cod ** (_, (b ** (isArrow1, Refl)))) - (dom ** cod ** (_, (b ** (isArrow2, Refl)))) - | (Refl, Refl) | (Refl, Refl) = (Refl, Refl) + IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod') +isFunctionUnique Done Done = (Refl, Refl) +isFunctionUnique (Step {a} prf) (Step prf') = + mapFst (\prf => cong (a ::) prf) $ isFunctionUnique prf prf' +export +isFunctionSplit : IsFunction bound a dom cod -> NotFunction bound a -> Void +isFunctionSplit (Step {a, b} prf) (Step1 contra) = void $ contra a b Refl +isFunctionSplit (Step prf) (Step2 contra) = isFunctionSplit prf contra + +export isFunction : - (bound : Context ()) -> Ty tyCtx () -> - Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ()) -isFunction [<] a = Just ([<], a) -isFunction (bound :< (x :- ())) a = do - (dom, cod) <- isFunction bound a - (b, cod) <- isArrow cod - 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 (reflectIsFunction bound a) | (isFunction bound a) - _ | RJust isFunc | Just (dom', cod') with (reflectIsArrow cod') | (isArrow cod') - _ | RJust isArrow | Just (b, cod) = RJust (dom' ** cod' ** (isFunc , (b ** (isArrow, Refl)))) - _ | RNothing notArrow | _ = - RNothing (\(dom :< (x :- b), cod), (dom ** cod'' ** (isFunc', (b ** (isArrow, Refl)))) => - let (eq1, eq2) = isFunctionUnique bound a {dom1 = dom', dom2 = dom, cod1 = cod', cod2 = cod''} isFunc isFunc' in - let isArrow = rewrite eq2 in isArrow in - notArrow (b, cod) isArrow) - _ | RNothing notFunc | _ = - RNothing (\(dom, cod), (dom' ** cod' ** (isFunc, _)) => notFunc (dom', cod') isFunc) - --- Full type checking and synthesis -------------------------------------------- - -Synths : - {tmCtx : Context ()} -> - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - SynthTerm tyCtx tmCtx -> Ty [<] () -> Type -Checks : - {tmCtx : Context ()} -> - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Ty [<] () -> CheckTerm tyCtx tmCtx -> Type -CheckSpine : - {tmCtx : Context ()} -> - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty [<] ()) -> Type -AllCheck : - {tmCtx : Context ()} -> - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Type -AllCheckBinding : - {tmCtx : Context ()} -> - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Row (Ty [<] ()) -> Ty [<] () -> - Row (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> - Type + (bound : List String) -> (a : Ty tyCtx) -> + Proof (All (const $ Ty tyCtx) bound, Ty tyCtx) + (uncurry $ IsFunction bound a) + (NotFunction bound a) +isFunction [] a = Just ([], a) `Because` Done +isFunction (x :: bound) a = + map + (\x => (fst (fst x) :: fst (snd x), snd (snd x))) + (\((a, b), (dom, cod)), (eq, prf) => rewrite eq in Step prf) + (either Step1 false) $ + (ab := isArrow a) >=> isFunction bound (snd ab) + where + false : + forall a. + (y : (Ty tyCtx, Ty tyCtx) ** (a = TArrow (fst y) (snd y), NotFunction bound (snd y))) -> + NotFunction (x :: bound) a + false ((a, b) ** (Refl, contra)) = Step2 contra + +-- Define well-formedness and ill-formedness + +namespace Modes + public export + data SynthsOnly : Term tyCtx tmCtx -> Type where + Annot : SynthsOnly (Annot t a) + Var : SynthsOnly (Var i) + App : SynthsOnly (App f ts) + Prj : SynthsOnly (Prj e l) + Unroll : SynthsOnly (Unroll e) + Map : SynthsOnly (Map (x ** a) b c) + GetChildren : SynthsOnly (GetChildren (x ** a) b) + + public export + data ChecksOnly : Term tyCtx tmCtx -> Type where + Abs : ChecksOnly (Abs (bounds ** t)) + Inj : ChecksOnly (Inj l t) + Case : ChecksOnly (Case e ts) + Roll : ChecksOnly (Roll t) + Fold : ChecksOnly (Fold e (x ** t)) -Synths tyEnv env (Var i) a = (a = indexAll i env) -Synths tyEnv env (Lit k) a = (a = TNat) -Synths tyEnv env Suc a = (a = TArrow TNat TNat) -Synths tyEnv env (App e ts) a = - ( fun ** - ( Synths tyEnv env e fun - , CheckSpine tyEnv env fun ts a - )) -Synths tyEnv env (Prj e x) a = - ( b ** - ( Synths tyEnv env e b - , ( as ** - ( IsProduct b as - , GetAt x as a - )) - )) -Synths tyEnv env (Expand e) a = - ( b ** - ( Synths tyEnv env e b - , ( xc ** - ( IsFixpoint b xc - , a = sub (Base Id :< (fst xc :- b)) (snd xc) - )) - )) -Synths tyEnv env (Annot t a) b = - ( Not (IllFormed a) - , Checks tyEnv env (expand tyEnv a) t - , expand tyEnv a = b - ) - -Checks tyEnv env a (LetTy x b t) = - ( Not (IllFormed b) - , Checks (tyEnv :< (x :- b)) env a t - ) -Checks tyEnv env a (Let x e t) = - ( b ** - ( Synths tyEnv env e b - , Checks tyEnv (env :< (x :- b)) a t - )) -Checks tyEnv env a (Abs bound t) = - ( as ** b ** - ( IsFunction bound a as b - , Checks tyEnv (env ++ as) b t - )) -Checks tyEnv env a (Inj x t) = - ( as ** - ( IsSum a as - , ( b ** - ( GetAt x as b - , Checks tyEnv env b t - )) - )) -Checks tyEnv env a (Tup ts) = - ( as ** - ( IsProduct a as - , AllCheck tyEnv env as ts - )) -Checks tyEnv env a (Case e ts) = - ( b ** - ( Synths tyEnv env e b - , ( as ** - ( IsSum b as - , AllCheckBinding tyEnv env as a ts - )) - )) -Checks tyEnv env a (Contract t) = - ( xb ** - ( IsFixpoint a xb - , Checks tyEnv env (sub (Base Id :< (fst xb :- a)) (snd xb)) t - )) -Checks tyEnv env a (Fold e x t) = - ( b ** - ( Synths tyEnv env e b - , ( yc ** - ( IsFixpoint b yc - , Checks tyEnv (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t - )) - )) -Checks tyEnv env a (Embed e) = - ( b ** - ( Synths tyEnv env e b - , a `Eq` b - )) - -CheckSpine tyEnv env fun [] res = fun = res -CheckSpine tyEnv env fun (t :: ts) res = - ( a ** b ** - ( IsArrow fun a b - , Checks tyEnv env a t - , CheckSpine tyEnv env b ts res - )) - -AllCheck tyEnv env as [<] = (as = [<]) -AllCheck tyEnv env as (ts :< (x :- t)) = - ( a ** bs ** - ( Remove x as a bs - , Checks tyEnv env a t - , AllCheck tyEnv env bs ts - )) - -AllCheckBinding tyEnv env as a [<] = (as = [<]) -AllCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) = - ( b ** bs ** - ( Remove x as b bs - , Checks tyEnv (env :< (y :- b)) a t - , AllCheckBinding tyEnv env bs a ts - )) - --- Reordering - -allCheckReorder : - as <~> bs -> (ts : Row (CheckTerm tyCtx tmCtx)) -> - AllCheck tyEnv env as ts -> AllCheck tyEnv 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)) - -allCheckBindingReorder : - as <~> bs -> (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> - AllCheckBinding tyEnv env as a ts -> AllCheckBinding tyEnv 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 tyEnv : DEnv Ty tyCtx) -> - (0 env : All (const $ Ty [<] ()) tmCtx) -> - (e : SynthTerm tyCtx tmCtx) -> - Synths tyEnv env e a -> Synths tyEnv env e b -> a = b -checkSpineUnique : - (0 tyEnv : DEnv Ty tyCtx) -> - (0 env : All (const $ Ty [<] ()) tmCtx) -> - (fun : Ty [<] ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> - CheckSpine tyEnv env fun ts a -> CheckSpine tyEnv env fun ts b -> a = b - -synthsUnique tyEnv env (Var i) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique tyEnv env (Lit k) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique tyEnv env Suc prf1 prf2 = trans prf1 (sym prf2) -synthsUnique tyEnv env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22)) - with (synthsUnique tyEnv env e prf11 prf21) - synthsUnique tyEnv env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl = - checkSpineUnique tyEnv env fun ts prf12 prf22 -synthsUnique tyEnv env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique tyEnv env e prf11 prf21) - synthsUnique tyEnv env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl - with (isProductUnique a prf11 prf21) - synthsUnique tyEnv env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl = - getAtUnique k as prf1 prf2 -synthsUnique tyEnv env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique tyEnv env e prf11 prf21) - synthsUnique tyEnv env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl - with (isFixpointUnique a prf11 prf21) - synthsUnique tyEnv env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl = - trans prf1 (sym prf2) -synthsUnique tyEnv env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2) - -checkSpineUnique tyEnv env fun [] prf1 prf2 = trans (sym prf1) prf2 -checkSpineUnique tyEnv env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22)) - with (isArrowUnique fun prf11 prf21) - checkSpineUnique tyEnv env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) = - checkSpineUnique tyEnv env b ts prf1 prf2 - --- Decision +public export +data Synths : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Term tyCtx tmCtx -> Ty [<] -> Type +public export +data Checks : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Ty [<] -> Term tyCtx tmCtx -> Type + +namespace Spine + public export + data CheckSpine : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Ty [<] -> List (Term tyCtx tmCtx) -> Ty [<] -> Type + where + Nil : CheckSpine tyEnv tmEnv a [] a + (::) : + Checks tyEnv tmEnv a t -> + CheckSpine tyEnv tmEnv b ts c -> + CheckSpine tyEnv tmEnv (TArrow a b) (t :: ts) c + + %name CheckSpine prfs + +namespace Synths + public export + data AllSynths : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + (ts : Context (Term tyCtx tmCtx)) -> All (const $ Ty [<]) ts.names -> Type + where + Lin : AllSynths tyEnv tmEnv [<] [<] + (:<) : + AllSynths tyEnv tmEnv ts as -> + Synths tyEnv tmEnv t a -> + AllSynths tyEnv tmEnv (ts :< (l :- t)) (as :< a) + + %name AllSynths prfs + +namespace Checks + public export + data AllChecks : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Context (Ty [<]) -> Context (Term tyCtx tmCtx) -> Type + where + Base : AllChecks tyEnv tmEnv [<] [<] + Step : + (i : Elem (l :- a) as) -> + Checks tyEnv tmEnv a t -> + AllChecks tyEnv tmEnv (dropElem as i) ts -> + AllChecks tyEnv tmEnv as (ts :< (l :- t)) + + %name AllChecks prfs + +namespace Branches + public export + data AllBranches : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Context (Ty [<]) -> Ty [<] -> Context (x ** Term tyCtx (tmCtx :< x)) -> Type + where + Base : AllBranches tyEnv tmEnv [<] a [<] + Step : + (i : Elem (l :- a) as) -> + Checks tyEnv (tmEnv :< (a `Over` Id)) b t -> + AllBranches tyEnv tmEnv (dropElem as i) b ts -> + AllBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) + + %name AllBranches prfs + +data Synths where + AnnotS : + Not (IllFormed a) -> + Checks tyEnv tmEnv (sub tyEnv a) t -> + Synths tyEnv tmEnv (Annot t a) (sub tyEnv a) + VarS : + Synths tyEnv tmEnv (Var i) (indexAll i.pos tmEnv).extract + LetS : + Synths tyEnv tmEnv e a -> + Synths tyEnv (tmEnv :< (a `Over` Id)) f b -> + Synths tyEnv tmEnv (Let e (x ** f)) b + LetTyS : + Not (IllFormed a) -> + Synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e b -> + Synths tyEnv tmEnv (LetTy a (x ** e)) b + AppS : + Synths tyEnv tmEnv f a -> + CheckSpine tyEnv tmEnv a ts b -> + Synths tyEnv tmEnv (App f ts) b + TupS : + AllSynths tyEnv tmEnv es.context as -> + Synths tyEnv tmEnv (Tup es) (TProd (fromAll es as)) + PrjS : + Synths tyEnv tmEnv e (TProd as) -> + Elem (l :- a) as.context -> + Synths tyEnv tmEnv (Prj e l) a + UnrollS : + Synths tyEnv tmEnv e (TFix x a) -> + Synths tyEnv tmEnv (Unroll e) (sub [ + Not (IllFormed b) -> + Not (IllFormed c) -> + Synths tyEnv tmEnv (Map (x ** a) b c) + (TArrow (TArrow (sub tyEnv b) (sub tyEnv c)) + (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a) + (sub (tyEnv :< (sub tyEnv c `Over` Id)) a))) + GetChildrenS : + Not (IllFormed (TFix x a)) -> + Not (IllFormed b) -> + Synths tyEnv tmEnv (GetChildren (x ** a) b) + (TArrow (sub (tyEnv :< (sub tyEnv b `Over` Id)) a) + (TProd + [<"Children" :- sub tyEnv b + , "Shape" :- sub (tyEnv :< (TNat `Over` Id)) a])) + +data Checks where + EmbedC : + SynthsOnly e -> + Synths tyEnv tmEnv e a -> + Alpha a b -> + Checks tyEnv tmEnv b e + LetC : + Synths tyEnv tmEnv e a -> + Checks tyEnv (tmEnv :< (a `Over` Id)) b t -> + Checks tyEnv tmEnv b (Let e (x ** t)) + LetTyC : + Not (IllFormed a) -> + Checks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t -> + Checks tyEnv tmEnv b (LetTy a (x ** t)) + AbsC : + IsFunction bound a dom cod -> + Checks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t -> + Checks tyEnv tmEnv a (Abs (bound ** t)) + TupC : + AllChecks tyEnv tmEnv as.context ts.context -> + Checks tyEnv tmEnv (TProd as) (Tup ts) + InjC : + Elem (l :- a) as.context -> + Checks tyEnv tmEnv a t -> + Checks tyEnv tmEnv (TSum as) (Inj l t) + CaseC : + Synths tyEnv tmEnv e (TSum as) -> + AllBranches tyEnv tmEnv as.context a ts.context -> + Checks tyEnv tmEnv a (Case e ts) + RollC : + Checks tyEnv tmEnv (sub [ + Checks tyEnv tmEnv (TFix x a) (Roll t) + FoldC : + Synths tyEnv tmEnv e (TFix x a) -> + Checks tyEnv (tmEnv :< (sub [ + Checks tyEnv tmEnv b (Fold e (y ** t)) + +%name Synths prf +%name Checks prf + +public export +data NotSynths : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Term tyCtx tmCtx -> Type +public export +data NotChecks : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Ty [<] -> Term tyCtx tmCtx -> Type + +namespace Spine + public export + data NotCheckSpine : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Ty [<] -> List (Term tyCtx tmCtx) -> Type + where + Step1 : + ((b, c : Ty [<]) -> Not (a = TArrow b c)) -> + NotCheckSpine tyEnv tmEnv a (t :: ts) + Step2 : + These (NotChecks tyEnv tmEnv a t) (NotCheckSpine tyEnv tmEnv b ts) -> + NotCheckSpine tyEnv tmEnv (TArrow a b) (t :: ts) + + %name NotCheckSpine contras + +namespace Synths + public export + data AnyNotSynths : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + (ts : Context (Term tyCtx tmCtx)) -> Type + where + Step : + These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) -> + AnyNotSynths tyEnv tmEnv (ts :< (l :- t)) + + %name AnyNotSynths contras + +namespace Checks + public export + data AnyNotChecks : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Context (Ty [<]) -> Context (Term tyCtx tmCtx) -> Type + where + Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<] + Step1 : + ((a : Ty [<]) -> Not (Elem (l :- a) as)) -> + AnyNotChecks tyEnv tmEnv as (ts :< (l :- t)) + Step2 : + (i : Elem (l :- a) as) -> + These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts) -> + AnyNotChecks tyEnv tmEnv as (ts :< (l :- t)) + + %name AnyNotChecks contras + +namespace Branches + public export + data AnyNotBranches : + All (const $ Thinned Ty [<]) tyCtx -> + All (const $ Thinned Ty [<]) tmCtx -> + Context (Ty [<]) -> Ty [<] -> Context (x ** Term tyCtx (tmCtx :< x)) -> Type + where + Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<] + Step1 : + ((a : Ty [<]) -> Not (Elem (l :- a) as)) -> + AnyNotBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) + Step2 : + (i : Elem (l :- a) as) -> + These + (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t) + (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts) -> + AnyNotBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) + + %name AnyNotBranches contras + +data NotSynths where + ChecksNS : + ChecksOnly t -> + NotSynths tyEnv tmEnv t + AnnotNS : + These (IllFormed a) (NotChecks tyEnv tmEnv (sub tyEnv a) t) -> + NotSynths tyEnv tmEnv (Annot t a) + LetNS1 : + NotSynths tyEnv tmEnv e -> + NotSynths tyEnv tmEnv (Let e (x ** f)) + LetNS2 : + Synths tyEnv tmEnv e a -> + NotSynths tyEnv (tmEnv :< (a `Over` Id)) f -> + NotSynths tyEnv tmEnv (Let e (x ** f)) + LetTyNS : + These (IllFormed a) (NotSynths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e) -> + NotSynths tyEnv tmEnv (LetTy a (x ** e)) + AppNS1 : + NotSynths tyEnv tmEnv f -> + NotSynths tyEnv tmEnv (App f ts) + AppNS2 : + Synths tyEnv tmEnv f a -> + NotCheckSpine tyEnv tmEnv a ts -> + NotSynths tyEnv tmEnv (App f ts) + TupNS : + AnyNotSynths tyEnv tmEnv es.context -> + NotSynths tyEnv tmEnv (Tup es) + PrjNS1 : + NotSynths tyEnv tmEnv e -> + NotSynths tyEnv tmEnv (Prj e l) + PrjNS2 : + Synths tyEnv tmEnv e a -> + ((as : Row (Ty [<])) -> Not (a = TProd as)) -> + NotSynths tyEnv tmEnv (Prj e l) + PrjNS3 : + Synths tyEnv tmEnv e (TProd as) -> + ((a : Ty [<]) -> Not (Elem (l :- a) as.context)) -> + NotSynths tyEnv tmEnv (Prj e l) + UnrollNS1 : + NotSynths tyEnv tmEnv e -> + NotSynths tyEnv tmEnv (Unroll e) + UnrollNS2 : + Synths tyEnv tmEnv e a -> + ((x : String) -> (b : Ty [ Not (a = TFix x b)) -> + NotSynths tyEnv tmEnv (Unroll e) + MapNS : + These (IllFormed (TFix x a)) (These (IllFormed b) (IllFormed c)) -> + NotSynths tyEnv tmEnv (Map (x ** a) b c) + GetChildrenNS : + These (IllFormed (TFix x a)) (IllFormed b) -> + NotSynths tyEnv tmEnv (GetChildren (x ** a) b) + +data NotChecks where + EmbedNC1 : + SynthsOnly e -> + NotSynths tyEnv tmEnv e -> + NotChecks tyEnv tmEnv b e + EmbedNC2 : + SynthsOnly e -> + Synths tyEnv tmEnv e a -> + NotAlpha a b -> + NotChecks tyEnv tmEnv b e + LetNC1 : + NotSynths tyEnv tmEnv e -> + NotChecks tyEnv tmEnv b (Let e (x ** t)) + LetNC2 : + Synths tyEnv tmEnv e a -> + NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t -> + NotChecks tyEnv tmEnv b (Let e (x ** t)) + LetTyNC : + These (IllFormed a) (NotChecks (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv b t) -> + NotChecks tyEnv tmEnv b (LetTy a (x ** t)) + AbsNC1 : + NotFunction bound a -> + NotChecks tyEnv tmEnv a (Abs (bound ** t)) + AbsNC2 : + IsFunction bound a dom cod -> + NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) dom) cod t -> + NotChecks tyEnv tmEnv a (Abs (bound ** t)) + TupNC1 : + ((as : Row (Ty [<])) -> Not (a = TProd as)) -> + NotChecks tyEnv tmEnv a (Tup ts) + TupNC2 : + AnyNotChecks tyEnv tmEnv as.context ts.context -> + NotChecks tyEnv tmEnv (TProd as) (Tup ts) + InjNC1 : + ((as : Row (Ty [<])) -> Not (a = TSum as)) -> + NotChecks tyEnv tmEnv a (Inj l t) + InjNC2 : + ((a : Ty [<]) -> Not (Elem (l :- a) as.context)) -> + NotChecks tyEnv tmEnv (TSum as) (Inj l t) + InjNC3 : + Elem (l :- a) as.context -> + NotChecks tyEnv tmEnv a t -> + NotChecks tyEnv tmEnv (TSum as) (Inj l t) + CaseNC1 : + NotSynths tyEnv tmEnv e -> + NotChecks tyEnv tmEnv a (Case e ts) + CaseNC2 : + Synths tyEnv tmEnv e b -> + ((as : Row (Ty [<])) -> Not (b = TSum as)) -> + NotChecks tyEnv tmEnv a (Case e ts) + CaseNC3 : + Synths tyEnv tmEnv e (TSum as) -> + AnyNotBranches tyEnv tmEnv as.context a ts.context -> + NotChecks tyEnv tmEnv a (Case e ts) + RollNC1 : + ((x : String) -> (b : Ty [ Not (a = TFix x b)) -> + NotChecks tyEnv tmEnv a (Roll t) + RollNC2 : + NotChecks tyEnv tmEnv (sub [ + NotChecks tyEnv tmEnv (TFix x a) (Roll t) + FoldNC1 : + NotSynths tyEnv tmEnv e -> + NotChecks tyEnv tmEnv b (Fold e (y ** t)) + FoldNC2 : + Synths tyEnv tmEnv e a -> + ((x : String) -> (c : Ty [ Not (a = TFix x c)) -> + NotChecks tyEnv tmEnv b (Fold e (y ** t)) + FoldNC3 : + Synths tyEnv tmEnv e (TFix x a) -> + NotChecks tyEnv (tmEnv :< (sub [ + NotChecks tyEnv tmEnv b (Fold e (y ** t)) + +%name NotSynths contra +%name NotChecks contra + +Uninhabited (NotSynths tyEnv tmEnv (Var i)) where + uninhabited (ChecksNS Abs) impossible + uninhabited (ChecksNS Inj) impossible + uninhabited (ChecksNS Case) impossible + uninhabited (ChecksNS Roll) impossible + uninhabited (ChecksNS Fold) impossible + +-- Synthesis gives unique types + +synthsUnique : Synths tyEnv tmEnv e a -> Synths tyEnv tmEnv e b -> a = b +checkSpineUnique : CheckSpine tyEnv tmEnv a ts b -> CheckSpine tyEnv tmEnv a ts c -> b = c +allSynthsUnique : AllSynths tyEnv tmEnv es as -> AllSynths tyEnv tmEnv es bs -> as = bs + +synthsUnique (AnnotS _ _) (AnnotS _ _) = Refl +synthsUnique VarS VarS = Refl +synthsUnique (LetS prf1 prf2) (LetS prf1' prf2') = + let prf2' = rewrite synthsUnique prf1 prf1' in prf2' in + synthsUnique prf2 prf2' +synthsUnique (LetTyS _ prf) (LetTyS _ prf') = synthsUnique prf prf' +synthsUnique (AppS prf prfs) (AppS prf' prfs') = + let prfs' = rewrite synthsUnique prf prf' in prfs' in + checkSpineUnique prfs prfs' +synthsUnique (TupS {es} prfs) (TupS prfs') = + cong (TProd . fromAll es) $ allSynthsUnique prfs prfs' +synthsUnique (PrjS {as} prf i) (PrjS {as = bs} prf' j) = + let j = rewrite inj TProd $ synthsUnique prf prf' in j in + cong fst $ lookupUnique as i j +synthsUnique (UnrollS {x, a} prf) (UnrollS {x = y, a = b} prf') = + cong (\(x ** a) => sub [ NotSynths tyEnv tmEnv e -> Void +checksSplit : Checks tyEnv tmEnv a t -> NotChecks tyEnv tmEnv a t -> Void +checkSpineSplit : CheckSpine tyEnv tmEnv a ts b -> NotCheckSpine tyEnv tmEnv a ts -> Void +allSynthsSplit : AllSynths tyEnv tmEnv es as -> AnyNotSynths tyEnv tmEnv es -> Void +allChecksSplit : + (0 fresh : AllFresh as.names) -> + AllChecks tyEnv tmEnv as ts -> AnyNotChecks tyEnv tmEnv as ts -> Void +allBranchesSplit : + (0 fresh : AllFresh as.names) -> + AllBranches tyEnv tmEnv as a ts -> AnyNotBranches tyEnv tmEnv as a ts -> Void + +synthsSplit (AnnotS wf prf) (AnnotNS contras) = + these wf (checksSplit prf) (const $ checksSplit prf) contras +synthsSplit VarS contra = absurd contra +synthsSplit (LetS prf1 prf2) (LetNS1 contra) = synthsSplit prf1 contra +synthsSplit (LetS prf1 prf2) (LetNS2 prf1' contra) = + let contra = rewrite synthsUnique prf1 prf1' in contra in + synthsSplit prf2 contra +synthsSplit (LetTyS wf prf) (LetTyNS contras) = + these wf (synthsSplit prf) (const $ synthsSplit prf) contras +synthsSplit (AppS prf prfs) (AppNS1 contra) = synthsSplit prf contra +synthsSplit (AppS prf prfs) (AppNS2 prf' contras) = + let contras = rewrite synthsUnique prf prf' in contras in + checkSpineSplit prfs contras +synthsSplit (TupS prfs) (TupNS contras) = allSynthsSplit prfs contras +synthsSplit (PrjS prf i) (PrjNS1 contra) = synthsSplit prf contra +synthsSplit (PrjS {as} prf i) (PrjNS2 prf' contra) = + void $ contra as $ synthsUnique prf' prf +synthsSplit (PrjS {as, a} prf i) (PrjNS3 {as = bs} prf' contra) = + let i = rewrite inj TProd $ synthsUnique prf' prf in i in + void $ contra a i +synthsSplit (UnrollS prf) (UnrollNS1 contra) = synthsSplit prf contra +synthsSplit (UnrollS {x, a} prf) (UnrollNS2 prf' contra) = + void $ contra x a $ synthsUnique prf' prf +synthsSplit (MapS wf1 wf2 wf3) (MapNS contras) = + these wf1 (these wf2 wf3 (const wf3)) (const $ these wf2 wf3 (const wf3)) contras +synthsSplit (GetChildrenS wf1 wf2) (GetChildrenNS contras) = + these wf1 wf2 (const wf2) contras + +checksSplit (EmbedC _ prf1 prf2) (EmbedNC1 _ contra) = synthsSplit prf1 contra +checksSplit (EmbedC _ prf1 prf2) (EmbedNC2 _ prf1' contra) = + let contra = rewrite synthsUnique prf1 prf1' in contra in + alphaSplit prf2 contra +checksSplit (LetC prf1 prf2) (LetNC1 contra) = synthsSplit prf1 contra +checksSplit (LetC prf1 prf2) (LetNC2 prf1' contra) = + let contra = rewrite synthsUnique prf1 prf1' in contra in + checksSplit prf2 contra +checksSplit (LetTyC wf prf) (LetTyNC contras) = + these wf (checksSplit prf) (const $ checksSplit prf) contras +checksSplit (AbsC prf1 prf2) (AbsNC1 contra) = isFunctionSplit prf1 contra +checksSplit (AbsC prf1 prf2) (AbsNC2 prf1' contra) = + let (eq1, eq2) = isFunctionUnique prf1 prf1' in + let contra = rewrite eq1 in rewrite eq2 in contra in + checksSplit prf2 contra +checksSplit (TupC {as} prfs) (TupNC1 contra) = void $ contra as Refl +checksSplit (TupC {as} prfs) (TupNC2 contras) = allChecksSplit as.fresh prfs contras +checksSplit (InjC {as} i prf) (InjNC1 contra) = void $ contra as Refl +checksSplit (InjC {a} i prf) (InjNC2 contra) = void $ contra a i +checksSplit (InjC {as} i prf) (InjNC3 j contra) = + let contra = rewrite cong fst $ lookupUnique as i j in contra in + checksSplit prf contra +checksSplit (CaseC prf prfs) (CaseNC1 contra) = synthsSplit prf contra +checksSplit (CaseC {as} prf prfs) (CaseNC2 prf' contra) = + void $ contra as $ synthsUnique prf' prf +checksSplit (CaseC {as} prf prfs) (CaseNC3 prf' contras) = + let contras = rewrite inj TSum $ synthsUnique prf prf' in contras in + allBranchesSplit as.fresh prfs contras +checksSplit (RollC {x, a} prf) (RollNC1 contra) = void $ contra x a Refl +checksSplit (RollC prf) (RollNC2 contra) = checksSplit prf contra +checksSplit (FoldC prf1 prf2) (FoldNC1 contra) = synthsSplit prf1 contra +checksSplit (FoldC {x, a} prf1 prf2) (FoldNC2 prf1' contra) = + void $ contra x a $ synthsUnique prf1' prf1 +checksSplit (FoldC {t, b} prf1 prf2) (FoldNC3 prf1' contra) = + let + contra = + replace + {p = \(x ** a) => NotChecks tyEnv (tmEnv :< (sub [ These (NotChecks tyEnv tmEnv a t) (AnyNotChecks tyEnv tmEnv (dropElem as i) ts)} + (lookupUnique (MkRow as fresh) j i) + contras + 0 fresh = dropElemFresh as fresh i + in + these (checksSplit prf) (allChecksSplit fresh prfs) (const $ allChecksSplit fresh prfs) contras + +allBranchesSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i +allBranchesSplit fresh (Step {as, b, x, t, ts} i prf prfs) (Step2 j contras) = + let + contras = + replace + {p = \(a ** i) => + These + (NotChecks tyEnv (tmEnv :< (a `Over` Id)) b t) + (AnyNotBranches tyEnv tmEnv (dropElem as i) b ts)} + (lookupUnique (MkRow as fresh) j i) + contras + 0 fresh = dropElemFresh as fresh i + in + these (checksSplit prf) (allBranchesSplit fresh prfs) (const $ allBranchesSplit fresh prfs) contras + +-- Synthesis and Checking are decidable + +fallbackCheck : + SynthsOnly e -> + Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) -> + (a : Ty [<]) -> + LazyEither (Checks tyEnv tmEnv a e) (NotChecks tyEnv tmEnv a e) +fallbackCheck prf p a = + map + (\xPrf => uncurry (EmbedC prf) $ snd xPrf) + (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $ + (b := p) >=> alpha b a synths : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - SynthTerm tyCtx tmCtx -> Maybe (Ty [<] ()) + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (e : Term tyCtx tmCtx) -> + Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e) export checks : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Ty [<] () -> CheckTerm tyCtx tmCtx -> Bool + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (a : Ty [<]) -> (t : Term tyCtx tmCtx) -> + LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t) checkSpine : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty [<] ()) -allCheck : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Bool -allCheckBinding : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - Row (Ty [<] ()) -> Ty [<] () -> - Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> - Bool - -synths tyEnv env (Var i) = do - pure (indexAll i env) -synths tyEnv env (Lit k) = do - pure TNat -synths tyEnv env Suc = do - pure (TArrow TNat TNat) -synths tyEnv env (App e ts) = do - a <- synths tyEnv env e - checkSpine tyEnv env a ts -synths tyEnv env (Prj e k) = do - a <- synths tyEnv env e - as <- isProduct a - getAt k as -synths tyEnv env (Expand e) = do - a <- synths tyEnv env e - (x ** b) <- isFixpoint a - Just (sub (Base Id :< (x :- a)) b) -synths tyEnv env (Annot t a) = do - guard (not $ illFormed a) - guard (checks tyEnv env (expand tyEnv a) t) - Just (expand tyEnv a) - -checks tyEnv env a (LetTy x b t) = - not (illFormed b) && - checks (tyEnv :< (x :- b)) env a t -checks tyEnv env a (Let x e t) = - case synths tyEnv env e of - Just b => checks tyEnv (env :< (x :- b)) a t - Nothing => False -checks tyEnv env a (Abs bound t) = - case isFunction bound a of - Just (dom, cod) => checks tyEnv (env ++ dom) cod t - Nothing => False -checks tyEnv env a (Inj k t) = - case isSum a of - Just as => - case getAt k as of - Just b => checks tyEnv env b t - Nothing => False - Nothing => False -checks tyEnv env a (Tup ts) = - case isProduct a of - Just as => allCheck tyEnv env as ts - Nothing => False -checks tyEnv env a (Case e ts) = - case synths tyEnv env e of - Just b => - case isSum b of - Just as => allCheckBinding tyEnv env as a ts - Nothing => False - Nothing => False -checks tyEnv env a (Contract t) = - case isFixpoint a of - Just (x ** b) => checks tyEnv env (sub (Base Id :< (x :- a)) b) t - Nothing => False -checks tyEnv env a (Fold e x t) = - case synths tyEnv env e of - Just b => - case isFixpoint b of - Just (y ** c) => checks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t - Nothing => False - Nothing => False -checks tyEnv env a (Embed e) = - case synths tyEnv env e of - Just b => a == b - Nothing => False - -checkSpine tyEnv env a [] = do - pure a -checkSpine tyEnv env a (t :: ts) = do - (dom, cod) <- isArrow a - guard (checks tyEnv env dom t) - checkSpine tyEnv env cod ts - -allCheck tyEnv env as [<] = null as -allCheck tyEnv env as (ts :< (x :- t)) = - case remove' x as of - Just (a, bs) => checks tyEnv env a t && allCheck tyEnv env bs ts - Nothing => False - -allCheckBinding tyEnv env as a [<] = null as -allCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) = - case remove' x as of - Just (b, bs) => checks tyEnv (env :< (y :- b)) a t && allCheckBinding tyEnv env bs a ts - Nothing => False - --- Proof - --- FIXME: these are total; the termination checker is unreasonably slow. - -partial -0 reflectSynths : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (e : SynthTerm tyCtx tmCtx) -> - Synths tyEnv env e `OnlyWhen` synths tyEnv env e -partial -0 reflectChecks : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (a : Ty [<] ()) -> (t : CheckTerm tyCtx tmCtx) -> - Checks tyEnv env a t `Reflects` checks tyEnv env a t -partial -0 reflectCheckSpine : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (fun : Ty [<] ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> - CheckSpine tyEnv env fun ts `OnlyWhen` checkSpine tyEnv env fun ts -partial -0 reflectAllCheck : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (as : Row (Ty [<] ())) -> (ts : Row (CheckTerm tyCtx tmCtx)) -> - AllCheck tyEnv env as ts `Reflects` allCheck tyEnv env as ts -partial -0 reflectAllCheckBinding : - (tyEnv : DEnv Ty tyCtx) -> - (env : All (const $ Ty [<] ()) tmCtx) -> - (as : Row (Ty [<] ())) -> (a : Ty [<] ()) -> - (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> - AllCheckBinding tyEnv env as a ts `Reflects` allCheckBinding tyEnv env as a ts - -reflectSynths tyEnv env (Var i) = RJust Refl -reflectSynths tyEnv env (Lit k) = RJust Refl -reflectSynths tyEnv env Suc = RJust Refl -reflectSynths tyEnv env (App e ts) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just a with (reflectCheckSpine tyEnv env a ts) | (checkSpine tyEnv env a ts) - _ | RJust tsSpine | Just b = RJust (a ** (eTy, tsSpine)) - _ | RNothing tsBad | _ = - RNothing - (\c, (b ** (eTy', tsSpine)) => - let tsSpine = rewrite synthsUnique tyEnv env e {a, b} eTy eTy' in tsSpine in - tsBad c tsSpine) - _ | RNothing eBad | _ = - RNothing (\c, (b ** (eTy, _)) => eBad b eTy) -reflectSynths tyEnv env (Prj e x) with (reflectSynths tyEnv env e) | (synths tyEnv 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 tyEnv 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 tyEnv env e {a, b = a'} eTy eTy' in prf in - nprf as' prf) - _ | RNothing eBad | _ = RNothing (\x, (a' ** (eTy, _)) => eBad a' eTy) -reflectSynths tyEnv env (Expand e) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just a with (reflectIsFixpoint a) | (isFixpoint a) - _ | 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 tyEnv env e {a, b = a'} eTy eTy' in prf in - nprf b prf) - _ | RNothing eBad | _ = RNothing (\x, (a ** (eTy, _)) => eBad a eTy) -reflectSynths tyEnv env (Annot t a) with (reflectIllFormed a) | (illFormed a) - _ | RFalse wf | _ with (reflectChecks tyEnv env (expand tyEnv a) t) | (checks tyEnv env (expand tyEnv a) t) - _ | RTrue tTy | _ = RJust (wf, tTy, Refl) - _ | RFalse tBad | _ = RNothing (\x, (_, tTy, Refl) => tBad tTy) - _ | RTrue notWf | _ = RNothing (\x, (wf, _) => wf notWf) - -reflectChecks tyEnv env a (LetTy x b t) with (reflectIllFormed b) | (illFormed b) - _ | RFalse wf | _ with (reflectChecks (tyEnv :< (x :- b)) env a t) | (checks (tyEnv :< (x :- b)) env a t) - _ | RTrue tTy | _ = RTrue (wf, tTy) - _ | RFalse tBad | _ = RFalse (tBad . snd) - _ | RTrue notWf | _ = RFalse (\(wf, _) => wf notWf) -reflectChecks tyEnv env a (Let x e t) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just b with (reflectChecks tyEnv (env :< (x :- b)) a t) | (checks tyEnv (env :< (x :- b)) a t) - _ | RTrue tTy | _ = RTrue (b ** (eTy, tTy)) - _ | RFalse tBad | _ = - RFalse (\(b' ** (eTy', tTy)) => - let tTy = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in tTy in - tBad tTy) - _ | RNothing eBad | Nothing = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks tyEnv env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a) - _ | RJust prf | Just (as, b) with (reflectChecks tyEnv (env ++ as) b t) | (checks tyEnv (env ++ as) b t) - _ | RTrue tTy | _ = RTrue (as ** b ** (prf, tTy)) - _ | RFalse tBad | _ = - RFalse (\(as' ** b' ** (prf', tTy)) => - let - (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 tyEnv 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 tyEnv env b t) | (checks tyEnv env b t) - _ | RTrue tTy | _ = RTrue (as ** (prf, (b ** (got, tTy)))) - _ | RFalse tBad | _ = - RFalse (\(as' ** (prf', (b' ** (got', 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 isSumUnique a {as, bs = as'} prf prf' in got in - not b got) - _ | RNothing nprf | _ = RFalse (\(as ** (prf, _)) => nprf as prf) -reflectChecks tyEnv env a (Tup ts) with (reflectIsProduct a) | (isProduct a) - _ | RJust prf | Just as with (reflectAllCheck tyEnv env as ts) | (allCheck tyEnv 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 tyEnv env a (Case e ts) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just b with (reflectIsSum b) | (isSum b) - _ | RJust prf | Just as with (reflectAllCheckBinding tyEnv env as a ts) | (allCheckBinding tyEnv env as a ts) - _ | RTrue tsTy | _ = RTrue (b ** (eTy, (as ** (prf, tsTy)))) - _ | RFalse tsBad | _ = - RFalse - (\(b' ** (eTy', (as' ** (prf', tsTy)))) => - let prf' = rewrite synthsUnique tyEnv 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 tyEnv env e {a = b, b = b'} eTy eTy' in prf in - nprf as prf) - _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks tyEnv env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a) - _ | RJust prf | Just (x ** b) with (reflectChecks tyEnv env (sub (Base Id :< (x :- a)) b) t) | (checks tyEnv env (sub (Base Id :< (x :- a)) b) t) - _ | RTrue tTy | _ = RTrue ((x ** b) ** (prf, tTy)) - _ | RFalse tBad | _ = - RFalse (\(b' ** (prf', tTy)) => - let - eq = isFixpointUnique a {xb = (x ** b), yc = b'} prf prf' - tTy = - replace {p = \xb => Checks tyEnv 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 tyEnv env a (Fold e x t) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just b with (reflectIsFixpoint b) | (isFixpoint b) - _ | RJust prf | Just (y ** c) with (reflectChecks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks tyEnv (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 tyEnv 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 tyEnv (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 tyEnv env e {a = b, b = b'} eTy eTy' in prf in - nprf c prf) - _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) -reflectChecks tyEnv env a (Embed e) with (reflectSynths tyEnv env e) | (synths tyEnv env e) - _ | RJust eTy | Just b with (reflectEq a b) | (a == b) - _ | RTrue eq | _ = RTrue (b ** (eTy, eq)) - _ | RFalse neq | _ = - RFalse (\(b' ** (eTy', eq)) => - let eq = rewrite synthsUnique tyEnv env e {a = b, b = b'} eTy eTy' in eq in - neq eq) - _ | RNothing eBad | _ = RFalse (\(b ** (eTy, _)) => eBad b eTy) - -reflectCheckSpine tyEnv env a [] = RJust Refl -reflectCheckSpine tyEnv env a (t :: ts) with (reflectIsArrow a) | (isArrow a) - _ | RJust prf | Just (b, c) with (reflectChecks tyEnv env b t) | (checks tyEnv env b t) - _ | RTrue tTy | _ with (reflectCheckSpine tyEnv env c ts) | (checkSpine tyEnv env c ts) - _ | RJust tsTy | Just d = RJust (b ** c ** (prf, tTy, tsTy)) - _ | RNothing tsBad | _ = - RNothing (\d, (_ ** c' ** (prf', _, tsTy)) => - 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 (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 tyEnv env [<] [<] = RTrue Refl -reflectAllCheck tyEnv env (_ :< _) [<] = RFalse (\case Refl impossible) -reflectAllCheck tyEnv env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as) - _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks tyEnv env a t) (reflectAllCheck tyEnv env bs ts)) | (checks tyEnv env a t && allCheck tyEnv 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 tyEnv env [<] a [<] = RTrue Refl -reflectAllCheckBinding tyEnv env (_ :< _) a [<] = RFalse (\case Refl impossible) -reflectAllCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as) - _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks tyEnv (env :< (y :- b)) a t) (reflectAllCheckBinding tyEnv env bs a ts)) | (checks tyEnv (env :< (y :- b)) a t && allCheckBinding tyEnv 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) + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (a : Ty [<]) -> (ts : List (Term tyCtx tmCtx)) -> + Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts) +allSynths : + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (es : Context (Term tyCtx tmCtx)) -> + Proof (All (const $ Ty [<]) es.names) (AllSynths tyEnv tmEnv es) (AnyNotSynths tyEnv tmEnv es) +allChecks : + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (as : Context (Ty [<])) -> (ts : Context (Term tyCtx tmCtx)) -> + LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts) +allBranches : + (tyEnv : All (const $ Thinned Ty [<]) tyCtx) -> + (tmEnv : All (const $ Thinned Ty [<]) tmCtx) -> + (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term tyCtx (tmCtx :< x))) -> + LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts) + +synths tyEnv tmEnv (Annot t a) = + pure (sub tyEnv a) $ + map (uncurry AnnotS) AnnotNS $ + all (not $ illFormed a) (checks tyEnv tmEnv (sub tyEnv a) t) +synths tyEnv tmEnv (Var i) = Just (indexAll i.pos tmEnv).extract `Because` VarS +synths tyEnv tmEnv (Let e (x ** f)) = + map snd + (\(_, _), (prf1, prf2) => LetS prf1 prf2) + (either LetNS1 (\xPrfs => uncurry LetNS2 (snd xPrfs))) $ + (a := synths tyEnv tmEnv e) >=> synths tyEnv (tmEnv :< (a `Over` Id)) f +synths tyEnv tmEnv (LetTy a (x ** e)) = + map id (\_, (wf, prf) => LetTyS wf prf) LetTyNS $ + all (not $ illFormed a) (synths (tyEnv :< (sub tyEnv a `Over` Id)) tmEnv e) +synths tyEnv tmEnv (Abs (bound ** t)) = Nothing `Because` ChecksNS Abs +synths tyEnv tmEnv (App e ts) = + map snd + (\(_, _), (prf1, prf2) => AppS prf1 prf2) + (either AppNS1 (\xPrfs => uncurry AppNS2 (snd xPrfs))) $ + (a := synths tyEnv tmEnv e) >=> checkSpine tyEnv tmEnv a ts +synths tyEnv tmEnv (Tup (MkRow es fresh)) = + map (TProd . fromAll (MkRow es fresh)) (\_ => TupS) TupNS $ + allSynths tyEnv tmEnv es +synths tyEnv tmEnv (Prj e l) = + map (snd . snd) true false $ + (a := synths tyEnv tmEnv e) >=> + (as := isProd a) >=> + decLookup l as.context + where + true : + (x : (Ty [<], Row (Ty [<]), Ty [<])) -> + (Synths tyEnv tmEnv e (fst x), uncurry (\x, yz => (x = TProd (fst yz), uncurry (\y,z => Elem (l :- z) y.context) yz)) x) -> + Synths tyEnv tmEnv (Prj e l) (snd $ snd x) + true (.(TProd as), as, a) (prf, Refl, i) = PrjS prf i + + false : + Either + (NotSynths tyEnv tmEnv e) + (a : Ty [<] ** (Synths tyEnv tmEnv e a, + Either + ((as : Row (Ty [<])) -> Not (a = TProd as)) + (as : Row (Ty [<]) ** (a = TProd as, (b : Ty [<]) -> Not (Elem (l :- b) as.context))))) -> + NotSynths tyEnv tmEnv (Prj e l) + false (Left contra) = PrjNS1 contra + false (Right (a ** (prf1, Left contra))) = PrjNS2 prf1 contra + false (Right (.(TProd as) ** (prf1, Right (as ** (Refl, contra))))) = PrjNS3 prf1 contra +synths tyEnv tmEnv (Inj l t) = Nothing `Because` ChecksNS Inj +synths tyEnv tmEnv (Case e (MkRow ts _)) = Nothing `Because` ChecksNS Case +synths tyEnv tmEnv (Roll t) = Nothing `Because` ChecksNS Roll +synths tyEnv tmEnv (Unroll e) = + map f true false $ + synths tyEnv tmEnv e `andThen` isFix + where + f : (Ty [<], (x ** Ty [ Ty [<] + f (a, (x ** b)) = sub [ + (Synths tyEnv tmEnv e (fst axb), uncurry (\a,xb => a = TFix xb.fst xb.snd) axb) -> + Synths tyEnv tmEnv (Unroll e) (f axb) + true (.(TFix x a), (x ** a)) (prf, Refl) = UnrollS prf + + false : + Either + (NotSynths tyEnv tmEnv e) + (a ** (Synths tyEnv tmEnv e a, (x : _) -> (b : _) -> Not (a = TFix x b))) -> + NotSynths tyEnv tmEnv (Unroll e) + false (Left contra) = UnrollNS1 contra + false (Right (a ** (prf, contra))) = UnrollNS2 prf contra +synths tyEnv tmEnv (Fold e (x ** t)) = Nothing `Because` ChecksNS Fold +synths tyEnv tmEnv (Map (x ** a) b c) = + pure _ $ + map (\(wf1, wf2, wf3) => MapS wf1 wf2 wf3) MapNS $ + all (not $ illFormed (TFix x a)) (all (not $ illFormed b) (not $ illFormed c)) +synths tyEnv tmEnv (GetChildren (x ** a) b) = + pure _ $ + map (uncurry GetChildrenS) GetChildrenNS $ + all (not $ illFormed (TFix x a)) (not $ illFormed b) + +checks tyEnv tmEnv a (Annot t b) = fallbackCheck Annot (synths tyEnv tmEnv $ Annot t b) a +checks tyEnv tmEnv a (Var i) = fallbackCheck Var (synths tyEnv tmEnv $ Var i) a +checks tyEnv tmEnv a (Let e (x ** t)) = + map + (\(_ ** (prf1, prf2)) => LetC prf1 prf2) + (either LetNC1 (\xPrfs => uncurry LetNC2 $ snd xPrfs)) $ + (b := synths tyEnv tmEnv e) >=> checks tyEnv (tmEnv :< (b `Over` Id)) a t +checks tyEnv tmEnv a (LetTy b (x ** t)) = + map (uncurry LetTyC) LetTyNC $ + all (not $ illFormed b) (checks (tyEnv :< (sub tyEnv b `Over` Id)) tmEnv a t) +checks tyEnv tmEnv a (Abs (bound ** t)) = + map + (\((_, _) ** (prf1, prf2)) => AbsC prf1 prf2) + (either AbsNC1 false) $ + (domCod := isFunction bound a) >=> + checks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst domCod)) (snd domCod) t + where + false : + (x ** (uncurry (IsFunction bound a) x, NotChecks tyEnv (tmEnv <>< mapProperty (`Over` Id) (fst x)) (snd x) t)) -> + NotChecks tyEnv tmEnv a (Abs (bound ** t)) + false ((_,_) ** prf) = uncurry AbsNC2 prf +checks tyEnv tmEnv a (App f ts) = fallbackCheck App (synths tyEnv tmEnv $ App f ts) a +checks tyEnv tmEnv a (Tup (MkRow ts fresh')) = + map true false $ + (as := isProd a) >=> allChecks tyEnv tmEnv as.context ts + where + true : + forall a. + (as : Row (Ty [<]) ** (a = TProd as, AllChecks tyEnv tmEnv as.context ts)) -> + Checks tyEnv tmEnv a (Tup (MkRow ts fresh')) + true (as ** (Refl, prf)) = TupC prf + + false : + forall a. + Either + ((as : Row (Ty [<])) -> Not (a = TProd as)) + (as : Row (Ty [<]) ** (a = TProd as, AnyNotChecks tyEnv tmEnv as.context ts)) -> + NotChecks tyEnv tmEnv a (Tup (MkRow ts fresh')) + false (Left contra) = TupNC1 contra + false (Right (as ** (Refl, contra))) = TupNC2 contra +checks tyEnv tmEnv a (Prj e l) = fallbackCheck Prj (synths tyEnv tmEnv $ Prj e l) a +checks tyEnv tmEnv a (Inj l t) = + map true false $ + (as := isSum a) >=> + (b := decLookup l as.context) >=> + checks tyEnv tmEnv b t + where + true : + forall a. + (as ** (a = TSum as, (b ** (Elem (l :- b) as.context, Checks tyEnv tmEnv b t)))) -> + Checks tyEnv tmEnv a (Inj l t) + true (as ** (Refl, (b ** (i, prf)))) = InjC i prf + + false : + forall a. + Either + ((as : _) -> Not (a = TSum as)) + (as ** (a = TSum as, + Either + ((b : _) -> Not (Elem (l :- b) as.context)) + (b ** (Elem (l :- b) as.context, NotChecks tyEnv tmEnv b t)))) -> + NotChecks tyEnv tmEnv a (Inj l t) + false (Left contra) = InjNC1 contra + false (Right (as ** (Refl, Left contra))) = InjNC2 contra + false (Right (as ** (Refl, Right (b ** (i, contra))))) = InjNC3 i contra +checks tyEnv tmEnv a (Case e (MkRow ts fresh)) = + map true false $ + (b := synths tyEnv tmEnv e) >=> + (as := isSum b) >=> + allBranches tyEnv tmEnv as.context a ts + where + true : + forall fresh. + (b ** (Synths tyEnv tmEnv e b, (as ** (b = TSum as, AllBranches tyEnv tmEnv as.context a ts)))) -> + Checks tyEnv tmEnv a (Case e (MkRow ts fresh)) + true (.(TSum as) ** (prf, (as ** (Refl, prfs)))) = CaseC prf prfs + + false : + forall fresh. + Either + (NotSynths tyEnv tmEnv e) + (b ** (Synths tyEnv tmEnv e b, + Either + ((as : _) -> Not (b = TSum as)) + (as ** (b = TSum as, AnyNotBranches tyEnv tmEnv as.context a ts)))) -> + NotChecks tyEnv tmEnv a (Case e (MkRow ts fresh)) + false (Left contra) = CaseNC1 contra + false (Right (b ** (prf, Left contra))) = CaseNC2 prf contra + false (Right (.(TSum as) ** (prf, Right (as ** (Refl, contras))))) = CaseNC3 prf contras +checks tyEnv tmEnv a (Roll t) = + map true false $ + (xb := isFix a) >=> checks tyEnv tmEnv (ty xb) t + where + ty : (x ** Ty [ Ty [<] + ty (x ** b) = sub [ + Checks tyEnv tmEnv a (Roll t) + true ((x ** b) ** (Refl, prf)) = RollC prf + + false : + forall a. + Either + ((x : _) -> (b : Ty [ Not (a = TFix x b)) + (xb : (x ** Ty [ + NotChecks tyEnv tmEnv a (Roll t) + false (Left contra) = RollNC1 contra + false (Right ((x ** b) ** (Refl, contra))) = RollNC2 contra +checks tyEnv tmEnv a (Unroll e) = fallbackCheck Unroll (synths tyEnv tmEnv $ Unroll e) a +checks tyEnv tmEnv a (Fold e (x ** t)) = + map true false $ + (b := synths tyEnv tmEnv e) >=> + (yc := isFix b) >=> + checks tyEnv (tmEnv' yc) a t + where + tmEnv' : (y ** Ty [ All (const $ Thinned Ty [<]) (tmCtx :< x) + tmEnv' (y ** c) = tmEnv :< (sub [ + Checks tyEnv tmEnv a (Fold e (x ** t)) + true (.(TFix y b) ** (prf1, ((y ** b) ** (Refl, prf2)))) = FoldC prf1 prf2 + + false : + Either + (NotSynths tyEnv tmEnv e) + (b ** (Synths tyEnv tmEnv e b, + Either + ((y : _) -> (c : Ty [ Not (b = TFix y c)) + (yc ** (b = TFix (fst yc) (snd yc), NotChecks tyEnv (tmEnv' yc) a t)))) -> + NotChecks tyEnv tmEnv a (Fold e (x ** t)) + false (Left contra) = FoldNC1 contra + false (Right (b ** (prf1, Left contra))) = FoldNC2 prf1 contra + false (Right (.(TFix y b) ** (prf1, Right ((y ** b) ** (Refl, contra))))) = FoldNC3 prf1 contra +checks tyEnv tmEnv a (Map (x ** b) c d) = + fallbackCheck Map (synths tyEnv tmEnv $ Map (x ** b) c d) a +checks tyEnv tmEnv a (GetChildren (x ** b) c) = + fallbackCheck GetChildren (synths tyEnv tmEnv $ GetChildren (x ** b) c) a + +checkSpine tyEnv tmEnv a [] = Just a `Because` [] +checkSpine tyEnv tmEnv a (t :: ts) = + map snd true false $ + (bc := isArrow a) >=> + all (checks tyEnv tmEnv (fst bc) t) (checkSpine tyEnv tmEnv (snd bc) ts) + where + true : + forall a. + (bcd : ((Ty [<], Ty [<]), Ty [<])) -> + ( a = TArrow (fst $ fst bcd) (snd $ fst bcd) + , uncurry (\bc,d => (Checks tyEnv tmEnv (fst bc) t, CheckSpine tyEnv tmEnv (snd bc) ts d)) bcd) -> + CheckSpine tyEnv tmEnv a (t :: ts) (snd bcd) + true ((b, c), d) (Refl, (prf1, prf2)) = prf1 :: prf2 + + false : + forall a. + Either + ((b, c : Ty [<]) -> Not (a = TArrow b c)) + (bc : (Ty [<], Ty [<]) ** (a = TArrow (fst bc) (snd bc), + These + (NotChecks tyEnv tmEnv (fst bc) t) + (NotCheckSpine tyEnv tmEnv (snd bc) ts))) -> + NotCheckSpine tyEnv tmEnv a (t :: ts) + false (Left contra) = Step1 contra + false (Right ((b, c) ** (Refl, contras))) = Step2 contras + +allSynths tyEnv tmEnv [<] = Just [<] `Because` [<] +allSynths tyEnv tmEnv (es :< (l :- e)) = + map (uncurry (flip (:<))) (\(a, as), (prf, prfs) => prfs :< prf) Step $ + all (synths tyEnv tmEnv e) (allSynths tyEnv tmEnv es) + +allChecks tyEnv tmEnv [<] [<] = True `Because` Base +allChecks tyEnv tmEnv (as :< la) [<] = False `Because` Base1 +allChecks tyEnv tmEnv as (ts :< (l :- t)) = + map + (\((a ** i) ** (prf, prfs)) => Step i prf prfs) + (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $ + (ai := (decLookup l as).forget) >=> + all (checks tyEnv tmEnv (fst ai) t) (allChecks tyEnv tmEnv (dropElem as $ snd ai) ts) + +allBranches tyEnv tmEnv [<] b [<] = True `Because` Base +allBranches tyEnv tmEnv (as :< la) b [<] = False `Because` Base1 +allBranches tyEnv tmEnv as b (ts :< (l :- (x ** t))) = + map + (\((a ** i) ** (prf, prfs)) => Step i prf prfs) + (either Step1 (\xPrf => Step2 (snd $ fst xPrf) (snd xPrf))) $ + (ai := (decLookup l as).forget) >=> + all + (checks tyEnv (tmEnv :< (fst ai `Over` Id)) b t) + (allBranches tyEnv tmEnv (dropElem as $ snd ai) b ts) + +-- Sugar ----------------------------------------------------------------------- + +public export +CheckLit : Nat -> Term tyCtx tmCtx +CheckLit 0 = Roll (Inj "Z" $ Tup [<]) +CheckLit (S n) = Roll (Inj "S" $ CheckLit n) + +public export +Lit : Nat -> Term tyCtx tmCtx +Lit n = Annot (CheckLit n) TNat + +public export +Suc : Term tyCtx tmCtx +Suc = Annot (Abs (["_x"] ** Roll (Inj "S" $ Var (%% "_x")))) (TArrow TNat TNat) + +export +isCheckLit : Term tyCtx tmCtx -> Maybe Nat +isCheckLit (Roll (Inj "Z" (Tup (MkRow [<] _)))) = Just 0 +isCheckLit (Roll (Inj "S" t)) = S <$> isCheckLit t +isCheckLit _ = Nothing + +export +isLit : Term tyCtx tmCtx -> Maybe Nat +isLit (Annot t a) = + if (alpha {ctx2 = [<]} a TNat).does + then isCheckLit t + else Nothing +isLit _ = Nothing + +export +isSuc : Term tyCtx tmCtx -> Bool +isSuc (Annot (Abs ([x] ** Roll (Inj "S" $ Var ((%%) x {pos = Here})))) a) = + does (alpha {ctx2 = [<]} a (TArrow TNat TNat)) +isSuc _ = False diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index 6913bf8..90b4e08 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -1,14 +1,23 @@ module Inky.Term.Parser -import public Data.Fun +import public Inky.Data.Fun +import Data.Either +import Data.Nat import Data.List1 import Data.String -import Inky.Context + +import Inky.Data.Context +import Inky.Data.Context.Var +import Inky.Data.Row +import Inky.Data.SnocList.Var +import Inky.Data.SnocList.Thinning +import Inky.Decidable +import Inky.Decidable.Maybe import Inky.Parser import Inky.Term -import Inky.Thinning import Inky.Type + import Text.Lexer -- Lexer ----------------------------------------------------------------------- @@ -18,7 +27,6 @@ data InkyKind = TermIdent | TypeIdent | Lit - | Suc | Let | In | Case @@ -27,6 +35,10 @@ data InkyKind | Fold | By | Nat + | List + | Suc + | Map + | GetChildren | ParenOpen | ParenClose | BracketOpen @@ -52,7 +64,6 @@ export TermIdent == TermIdent = True TypeIdent == TypeIdent = True Lit == Lit = True - Suc == Suc = True Let == Let = True In == In = True Case == Case = True @@ -61,6 +72,10 @@ export Fold == Fold = True By == By = True Nat == Nat = True + List == List = True + Suc == Suc = True + Map == Map = True + GetChildren == GetChildren = True ParenOpen == ParenOpen = True ParenClose == ParenClose = True BracketOpen == BracketOpen = True @@ -87,7 +102,6 @@ Interpolation InkyKind where interpolate TermIdent = "term name" interpolate TypeIdent = "type name" interpolate Lit = "number" - interpolate Suc = "'suc'" interpolate Let = "'let'" interpolate In = "'in'" interpolate Case = "'case'" @@ -96,6 +110,10 @@ Interpolation InkyKind where interpolate Fold = "'fold'" interpolate By = "'by'" interpolate Nat = "'Nat'" + interpolate List = "'List'" + interpolate Suc = "'suc'" + interpolate Map = "'map'" + interpolate GetChildren = "'getChildren'" interpolate ParenOpen = "'('" interpolate ParenClose = "')'" interpolate BracketOpen = "'['" @@ -125,7 +143,6 @@ TokenKind InkyKind where tokValue TermIdent = id tokValue TypeIdent = id tokValue Lit = stringToNatOrZ - tokValue Suc = const () tokValue Let = const () tokValue In = const () tokValue Case = const () @@ -134,6 +151,10 @@ TokenKind InkyKind where tokValue Fold = const () tokValue By = const () tokValue Nat = const () + tokValue List = const () + tokValue Suc = const () + tokValue Map = const () + tokValue GetChildren = const () tokValue ParenOpen = const () tokValue ParenClose = const () tokValue BracketOpen = const () @@ -156,8 +177,7 @@ TokenKind InkyKind where keywords : List (String, InkyKind) keywords = - [ ("suc", Suc) - , ("let", Let) + [ ("let", Let) , ("in", In) , ("case", Case) , ("of", Of) @@ -165,6 +185,10 @@ keywords = , ("fold", Fold) , ("by", By) , ("Nat", Nat) + , ("List", List) + , ("suc", Suc) + , ("map", Map) + , ("getChildren", GetChildren) ] export @@ -220,71 +244,62 @@ tokenMap = -- Parser ---------------------------------------------------------------------- -public export -DFun : (ts : Vect n Type) -> Fun ts Type -> Type -DFun [] r = r -DFun (t :: ts) r = (x : t) -> DFun ts (r x) - -public export -DIFun : (ts : Vect n Type) -> Fun ts Type -> Type -DIFun [] r = r -DIFun (t :: ts) r = {x : t} -> DIFun ts (r x) - public export InkyParser : Bool -> Context Type -> Context Type -> (a : Type) -> Type InkyParser nil locked free a = Parser InkyKind nil - (map (\a => (False, a)) locked) - (map (\a => (False, a)) free) + (map (map (False,)) locked) + (map (map (False,)) free) a public export -record ParseFun (0 tys: Vect n Type) (0 p : Fun (map Context tys) Type) where +record ParseFun (0 n : Nat) (0 p : Fun (replicate n $ SnocList String) Type) where constructor MkParseFun - try : DFun (map Context tys) (chain {ts = map Context tys} (Either String) p) + try : + DFun (replicate n $ SnocList String) + (chain (lengthOfReplicate n $ SnocList String) (Either String) p) -mkVar : ({ctx : Context ()} -> Var ctx () -> p ctx) -> WithBounds String -> ParseFun [()] p +mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun 1 p mkVar f x = MkParseFun - (\ctx => case lookup x.val ctx of - Just (() ** i) => pure (f i) + (\ctx => case Var.lookup x.val ctx of + Just i => pure (f i) Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"") mkVar2 : - ({tyCtx, tmCtx : Context ()} -> Var tmCtx () -> p tyCtx tmCtx) -> - WithBounds String -> ParseFun [(), ()] p + ({tyCtx, tmCtx : _} -> Var tmCtx -> p tyCtx tmCtx) -> + WithBounds String -> ParseFun 2 p mkVar2 f x = MkParseFun - (\tyCtx, tmCtx => case lookup x.val tmCtx of - Just (() ** i) => pure (f i) + (\tyCtx, tmCtx => case Var.lookup x.val tmCtx of + Just i => pure (f i) Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"") public export TypeFun : Type -TypeFun = ParseFun [()] (\ctx => Ty ctx ()) - -public export -SynthFun : Type -SynthFun = ParseFun [(), ()] SynthTerm +TypeFun = ParseFun 1 Ty public export -CheckFun : Type -CheckFun = ParseFun [(), ()] CheckTerm +TermFun : Type +TermFun = ParseFun 2 Term public export -TypeParser : Context () -> Context () -> Type +TypeParser : SnocList String -> SnocList String -> Type TypeParser locked free = - InkyParser False (map (const TypeFun) locked) (map (const TypeFun) free) TypeFun + InkyParser False (map (:- TypeFun) locked) (map (:- TypeFun) free) TypeFun -RowOf : (0 free : Context Type) -> InkyParser False [<] free a -> InkyParser True [<] free (List $ WithBounds $ Assoc a) +RowOf : + (0 free : Context Type) -> + InkyParser False [<] free a -> + InkyParser True [<] free (List $ WithBounds $ Assoc a) RowOf free p = sepBy (match Comma) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p]) where mkAssoc : HList [String, (), a] -> Assoc a mkAssoc [x, _, v] = x :- v tryRow : - List (WithBounds $ Assoc (ParseFun [()] p)) -> - (ctx : Context ()) -> Either String (Row $ p ctx) + List (WithBounds $ Assoc (ParseFun 1 p)) -> + (ctx : _) -> Either String (Row $ p ctx) tryRow xs ctx = foldlM (\row, xf => do @@ -296,8 +311,8 @@ tryRow xs ctx = xs tryRow2 : - List (WithBounds $ Assoc (ParseFun [(), ()] p)) -> - (tyCtx, tmCtx : Context ()) -> Either String (Row $ p tyCtx tmCtx) + List (WithBounds $ Assoc (ParseFun 2 p)) -> + (tyCtx, tmCtx : _) -> Either String (Row $ p tyCtx tmCtx) tryRow2 xs tyCtx tmCtx = foldlM (\row, xf => do @@ -308,29 +323,29 @@ tryRow2 xs tyCtx tmCtx = [<] xs -OpenOrFixpointType : TypeParser [<] [<"openType" :- ()] +OpenOrFixpointType : TypeParser [<] [<"openType"] OpenOrFixpointType = OneOf [ mkFix <$> - Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%% "openType")] - , Var (%% "openType") + Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%%% "openType")] + , Var (%%% "openType") ] where mkFix : HList [(), String, (), TypeFun] -> TypeFun - mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ())))) + mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< x))) -AtomType : TypeParser [<"openType" :- ()] [<] +AtomType : TypeParser [<"openType"] [<] AtomType = OneOf [ mkVar TVar <$> WithBounds (match TypeIdent) , MkParseFun (\_ => pure TNat) <$ match Nat - , mkProd <$> enclose (match AngleOpen) (match AngleClose) Row - , mkSum <$> enclose (match BracketOpen) (match BracketClose) Row + , mkProd <$> enclose (match AngleOpen) (match AngleClose) row + , mkSum <$> enclose (match BracketOpen) (match BracketClose) row , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType ] where - Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun) - Row = RowOf [<"openType" :- TypeFun] $ Var (%% "openType") + row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun) + row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType") mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx) @@ -338,13 +353,25 @@ AtomType = mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx) +AppType : TypeParser [<"openType"] [<] +AppType = + OneOf + [ AtomType + , match List **> mkList <$> weaken (S Z) AtomType + ] + where + mkList : TypeFun -> TypeFun + mkList x = MkParseFun (\ctx => TList <$> x.try ctx) + export OpenType : TypeParser [<] [<] OpenType = - Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AtomType + Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AppType where mkArrow : List1 TypeFun -> TypeFun - mkArrow = foldr1 (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |])) + mkArrow = + foldr1 {a = TypeFun} + (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |])) %hint export @@ -353,95 +380,122 @@ OpenTypeWf = Oh -- Terms ----------------------------------------------------------------------- -embed : SynthFun -> CheckFun -embed x = MkParseFun (\tyCtx, tmCtx => Embed <$> x.try tyCtx tmCtx) - -unembed : WithBounds CheckFun -> SynthFun -unembed x = - MkParseFun (\tyCtx, tmCtx => do - t <- x.val.try tyCtx tmCtx - case t of - Embed e => pure e - _ => Left "\{x.bounds}: cannot synthesise type") - -AtomCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -AtomCheck = +AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +AtomTerm = OneOf - [ embed <$> mkVar2 Var <$> WithBounds (match TermIdent) - , embed <$> mkLit <$> match Lit - , embed <$> MkParseFun (\_, _ => pure Suc) <$ match Suc + [ mkVar2 Var <$> WithBounds (match TermIdent) + , mkLit <$> match Lit + , mkSuc <$ match Suc , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $ - RowOf [<"openCheck" :- CheckFun] (Var (%% "openCheck"))) - , enclose (match ParenOpen) (match ParenClose) (Var (%% "openCheck")) + RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm"))) + , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm")) ] where - mkLit : Nat -> SynthFun - mkLit k = MkParseFun (\_, _ => pure (Lit k)) + mkLit : Nat -> TermFun + mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k)) - mkTup : List (WithBounds $ Assoc CheckFun) -> CheckFun + mkSuc : TermFun + mkSuc = MkParseFun (\_, _ => pure Suc) + + mkTup : List (WithBounds $ Assoc TermFun) -> TermFun mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup <$> tryRow2 xs tyCtx tmCtx) -PrefixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -PrefixCheck = - Fix "prefixCheck" $ OneOf - [ embed <$> mkExpand <$> unembed <$> (match Bang **> WithBounds (Var $ %% "prefixCheck")) - , mkContract <$> (match Tilde **> Var (%% "prefixCheck")) - , rename (Drop Id) Id AtomCheck +PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +PrefixTerm = + Fix "prefixTerm" $ OneOf + [ match Tilde **> (mkRoll <$> Var (%%% "prefixTerm")) + , match Bang **> mkUnroll <$> Var (%%% "prefixTerm") + , rename (Drop Id) Id AtomTerm ] where - mkExpand : SynthFun -> SynthFun - mkExpand x = MkParseFun (\tyCtx, tmCtx => [| Expand (x.try tyCtx tmCtx) |]) + mkRoll : TermFun -> TermFun + mkRoll x = MkParseFun (\tyCtx, tmCtx => [| Roll (x.try tyCtx tmCtx) |]) - mkContract : CheckFun -> CheckFun - mkContract x = MkParseFun (\tyCtx, tmCtx => [| Contract (x.try tyCtx tmCtx) |]) + mkUnroll : TermFun -> TermFun + mkUnroll x = MkParseFun (\tyCtx, tmCtx => [| Unroll (x.try tyCtx tmCtx) |]) -SuffixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -SuffixCheck = mkSuffix <$> Seq [ WithBounds PrefixCheck , star (match Dot **> match TypeIdent) ] +SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> match TypeIdent) ] where - mkSuffix : HList [WithBounds CheckFun, List String] -> CheckFun - mkSuffix [t, []] = t.val + mkSuffix : HList [TermFun, List String] -> TermFun + mkSuffix [t, []] = t mkSuffix [t, prjs] = - embed $ - MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !((unembed t).try tyCtx tmCtx) prjs) + MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !(t.try tyCtx tmCtx) prjs) -AppCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -AppCheck = +AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +AppTerm = OneOf [ mkInj <$> Seq [ match TypeIdent - , weaken (S Z) SuffixCheck + , weaken (S Z) SuffixTerm + ] + , mkApp <$> Seq + [ OneOf {nils = [False, False, False]} + [ SuffixTerm + , mkMap <$> Seq + [ match Map + , enclose (match ParenOpen) (match ParenClose) $ Seq + [ match Backslash + , match TypeIdent + , match DoubleArrow + , rename Id (Drop Id) OpenType + ] + , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType + , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType + ] + , mkGetChildren <$> Seq + [ match GetChildren + , enclose (match ParenOpen) (match ParenClose) $ Seq + [ match Backslash + , match TypeIdent + , match DoubleArrow + , rename Id (Drop Id) OpenType + ] + , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType + ] + ] + , star (weaken (S Z) SuffixTerm) ] - , mkApp <$> Seq [ WithBounds SuffixCheck , star (weaken (S Z) SuffixCheck) ] ] where - mkInj : HList [String, CheckFun] -> CheckFun + mkInj : HList [String, TermFun] -> TermFun mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx) - mkApp : HList [WithBounds CheckFun, List CheckFun] -> CheckFun - mkApp [t, []] = t.val + mkMap : HList [_, HList [_, String, _, TypeFun], TypeFun, TypeFun] -> TermFun + mkMap [_, [_, x, _, a], b, c] = + MkParseFun (\tyCtx, tmCtx => + pure $ Map (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx)) + + mkGetChildren : HList [_, HList [_, String, _, TypeFun], TypeFun] -> TermFun + mkGetChildren [_, [_, x, _, a], b] = + MkParseFun (\tyCtx, tmCtx => + pure $ GetChildren (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx)) + + mkApp : HList [TermFun, List TermFun] -> TermFun + mkApp [t, []] = t mkApp [fun, (arg :: args)] = MkParseFun (\tyCtx, tmCtx => - pure $ Embed $ + pure $ App - !((unembed fun).try tyCtx tmCtx) + !(fun.try tyCtx tmCtx) ( !(arg.try tyCtx tmCtx) :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> []))) -AnnotCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -AnnotCheck = +AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +AnnotTerm = mkAnnot <$> Seq - [ AppCheck + [ AppTerm , option (match Colon **> rename Id (Drop Id) OpenType) ] where - mkAnnot : HList [CheckFun, Maybe TypeFun] -> CheckFun + mkAnnot : HList [TermFun, Maybe TypeFun] -> TermFun mkAnnot [t, Nothing] = t - mkAnnot [t, Just a] = embed $ MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |]) + mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |]) -- Open Terms -LetCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -LetCheck = +LetTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +LetTerm = match Let **> OneOf [ mkLet <$> Seq @@ -453,71 +507,72 @@ LetCheck = , match Colon , rename Id (Drop Id) OpenType , match Equal - , Var (%% "openCheck")] - , match Equal **> unembed <$> WithBounds (Var (%% "openCheck")) + , Var (%%% "openTerm")] + , match Equal **> Var (%%% "openTerm") ] , match In - , Var (%% "openCheck") + , Var (%%% "openTerm") ] , mkLetType <$> Seq [ match TypeIdent , match Equal , rename Id (Drop Id) OpenType , match In - , Var (%% "openCheck") + , Var (%%% "openTerm") ] ] where - mkLet : HList [String, SynthFun, (), CheckFun] -> CheckFun - mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let x !(e.try tyCtx tmCtx) !(t.try tyCtx (tmCtx :< (x :- ())))) + mkLet : HList [String, TermFun, (), TermFun] -> TermFun + mkLet [x, e, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Let !(e.try tyCtx tmCtx) (x ** !(t.try tyCtx (tmCtx :< x)))) - mkLetType : HList [String, (), TypeFun, (), CheckFun] -> CheckFun + mkLetType : HList [String, (), TypeFun, (), TermFun] -> TermFun mkLetType [x, _, a, _, t] = - MkParseFun (\tyCtx, tmCtx => pure $ LetTy x !(a.try tyCtx) !(t.try (tyCtx :< (x :- ())) tmCtx)) + MkParseFun (\tyCtx, tmCtx => pure $ LetTy !(a.try tyCtx) (x ** !(t.try (tyCtx :< x) tmCtx))) mkArrow : List TypeFun -> TypeFun -> TypeFun mkArrow [] cod = cod mkArrow (arg :: args) cod = MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |]) - mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), CheckFun] -> SynthFun + mkBound : HList [List (HList [String, (), TypeFun]), (), TypeFun, (), TermFun] -> TermFun mkBound [[], _, cod, _, t] = MkParseFun (\tyCtx, tmCtx => pure $ Annot !(t.try tyCtx tmCtx) !(cod.try tyCtx)) mkBound [args, _, cod, _, t] = - let dom = foldl (\dom, [x, _, a] => dom :< (x :- ())) [<] args in + let bound = map (\[x, _, a] => x) args in + let tys = map (\[x, _, a] => a) args in MkParseFun (\tyCtx, tmCtx => pure $ - Annot (Abs dom !(t.try tyCtx (tmCtx ++ dom))) !((mkArrow (map (\[x, _, a] => a) args) cod).try tyCtx)) + Annot (Abs (bound ** !(t.try tyCtx (tmCtx <>< bound)))) !((mkArrow tys cod).try tyCtx)) -AbsCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -AbsCheck = +AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +AbsTerm = mkAbs <$> Seq [ match Backslash , sepBy1 (match Comma) (match TermIdent) , match DoubleArrow - , Var (%% "openCheck") + , Var (%%% "openTerm") ] where - mkAbs : HList [(), List1 String, (), CheckFun] -> CheckFun + mkAbs : HList [(), List1 String, (), TermFun] -> TermFun mkAbs [_, args, _, body] = - let args = foldl (\args, x => args :< (x :- ())) [<] args in - MkParseFun (\tyCtx, tmCtx => Abs args <$> body.try tyCtx (tmCtx ++ args)) + MkParseFun (\tyCtx, tmCtx => + pure $ Abs (forget args ** !(body.try tyCtx (tmCtx <>< forget args)))) -CaseCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -CaseCheck = +CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +CaseTerm = (\[f, x] => f x) <$> Seq [ OneOf [ mkCase <$> Seq [ match Case - , unembed <$> WithBounds (Var $ %% "openCheck") + , Var (%%% "openTerm") , match Of ] , mkFoldCase <$> Seq [ match FoldCase - , unembed <$> WithBounds (Var $ %% "openCheck") + , Var (%%% "openTerm") , match By ] ] @@ -528,66 +583,66 @@ CaseCheck = [ match TypeIdent , match TermIdent , match DoubleArrow - , Var (%% "openCheck") + , Var (%%% "openTerm") ]) ] where Cases : Type - Cases = List (WithBounds $ HList [String, String, (), CheckFun]) + Cases = List (WithBounds $ HList [String, String, (), TermFun]) mkBranch : - HList [String, String, (), CheckFun] -> - Assoc (ParseFun [(), ()] $ \tyCtx, tmCtx => (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) + HList [String, String, (), TermFun] -> + Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term tyCtx (tmCtx :< x))) mkBranch [tag, bound, _, branch] = - tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< (bound :- ()))))) + tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound)))) - mkCase : HList [_, SynthFun, _] -> Cases -> CheckFun + mkCase : HList [_, TermFun, _] -> Cases -> TermFun mkCase [_, target, _] branches = let branches = map (map mkBranch) branches in MkParseFun (\tyCtx, tmCtx => [| Case (target.try tyCtx tmCtx) (tryRow2 branches tyCtx tmCtx) |]) - mkFoldCase : HList [_, SynthFun, _] -> Cases -> CheckFun + mkFoldCase : HList [_, TermFun, _] -> Cases -> TermFun mkFoldCase [_, target, _] branches = let branches = map (map mkBranch) branches in MkParseFun (\tyCtx, tmCtx => pure $ Fold !(target.try tyCtx tmCtx) - "__tmp" - (Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< ("__tmp" :- ()))))) + ("__tmp" ** Case (Var $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp")))) -FoldCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun -FoldCheck = +FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +FoldTerm = mkFold <$> Seq [ match Fold - , unembed <$> WithBounds (Var (%% "openCheck")) + , Var (%%% "openTerm") , match By , enclose (match ParenOpen) (match ParenClose) $ Seq [ match Backslash , match TermIdent , match DoubleArrow - , Var (%% "openCheck") + , Var (%%% "openTerm") ] ] where - mkFold : HList [(), SynthFun, (), HList [(), String, (), CheckFun]] -> CheckFun + mkFold : HList [(), TermFun, (), HList [(), String, (), TermFun]] -> TermFun mkFold [_, target, _, [_, arg, _, body]] = - MkParseFun (\tyCtx, tmCtx => pure $ Fold !(target.try tyCtx tmCtx) arg !(body.try tyCtx (tmCtx :< (arg :- ())))) + MkParseFun (\tyCtx, tmCtx => + pure $ Fold !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg)))) export -OpenCheck : InkyParser False [<] [<] CheckFun -OpenCheck = - Fix "openCheck" $ OneOf - [ LetCheck - , AbsCheck - , CaseCheck - , FoldCheck - , AnnotCheck +OpenTerm : InkyParser False [<] [<] TermFun +OpenTerm = + Fix "openTerm" $ OneOf + [ LetTerm + , AbsTerm + , CaseTerm + , FoldTerm + , AnnotTerm ] %hint export -OpenCheckWf : So (wellTyped EqI [<] [<] [<] [<] OpenCheck) -OpenCheckWf = ?d -- Oh +OpenTermWf : So (wellTyped EqI [<] [<] [<] [<] OpenTerm) +OpenTermWf = Oh diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index 3bed88b..a9055d4 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -1,116 +1,130 @@ module Inky.Term.Pretty -import Inky.Context +import Data.Singleton + +import Inky.Decidable.Maybe import Inky.Term import Inky.Type.Pretty import Text.PrettyPrint.Prettyprinter -appPrec, prjPrec, expandPrec, annotPrec, - letPrec, absPrec, injPrec, tupPrec, casePrec, contractPrec, foldPrec : Prec +appPrec, prjPrec, unrollPrec, annotPrec, + letPrec, absPrec, injPrec, tupPrec, casePrec, rollPrec, foldPrec : Prec appPrec = App prjPrec = User 9 -expandPrec = PrefixMinus +unrollPrec = PrefixMinus annotPrec = Equal letPrec = Open absPrec = Open injPrec = App tupPrec = Open casePrec = Open -contractPrec = PrefixMinus +rollPrec = PrefixMinus foldPrec = Open export -prettySynth : - {tyCtx, tmCtx : Context ()} -> - SynthTerm tyCtx tmCtx -> Prec -> Doc ann -export -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 ()} -> - Row (CheckTerm tyCtx tmCtx) -> Prec -> List (Doc ann) -prettyCheckCtxBinding : - {tyCtx, tmCtx : Context ()} -> - Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Prec -> List (Doc ann) +prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann +prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> Prec -> List (Doc ann) +prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> Prec -> SnocList (Doc ann) +prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann) +lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> Prec -> Doc ann -prettySynth (Var i) d = pretty (unVal $ nameOf i) -prettySynth (Lit k) d = pretty k -prettySynth Suc d = pretty "suc" -prettySynth (App e ts) d = - parenthesise (d >= appPrec) $ group $ align $ hang 2 $ - 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 x -prettySynth (Expand e) d = - "!" <+> - (parenthesise (d > expandPrec) $ group $ align $ hang 2 $ - prettySynth e expandPrec) -prettySynth (Annot t a) d = - parenthesise (d > annotPrec) $ group $ align $ hang 2 $ - prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec +prettyTerm t d = + case isLit t <|> isCheckLit t of + Just k => pretty k + Nothing => + if isSuc t + then pretty "suc" + else lessPrettyTerm t d + +prettyAllTerm [] d = [] +prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d -prettyCheck (LetTy x a t) d = +prettyTermCtx [<] d = [<] +prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d) + +prettyCases [<] = [<] +prettyCases (ts :< (l :- (x ** t))) = + prettyCases ts :< (pretty l <++> pretty x <++> "=>" <++> prettyTerm t Open) + + +lessPrettyTerm (Annot t a) d = + parenthesise (d > annotPrec) $ group $ align $ hang 2 $ + prettyTerm t annotPrec <++> ":" <+> line <+> prettyType a annotPrec +lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i) +lessPrettyTerm (Let e (x ** t)) d = parenthesise (d > letPrec) $ group $ align $ - "let" <++> (group $ align $ hang 2 $ - pretty x <++> "=" <+> line <+> prettyType a letPrec + pretty x <++> "=" <+> line <+> prettyTerm e letPrec ) <+> line <+> "in" <+> line <+> - prettyCheck t letPrec -prettyCheck (Let x e t) d = + prettyTerm t letPrec +lessPrettyTerm (LetTy a (x ** t)) d = parenthesise (d > letPrec) $ group $ align $ - "let" <++> (group $ align $ hang 2 $ - pretty x <++> "=" <+> line <+> prettySynth e letPrec + pretty x <++> "=" <+> line <+> prettyType a letPrec ) <+> line <+> "in" <+> line <+> - prettyCheck t letPrec -prettyCheck (Abs bound t) d = - parenthesise (d > absPrec) $ group $ align $ hang 2 $ - "\\" <+> concatWith (surround $ "," <+> line) (bindings bound <>> []) <++> "=>" <+> line <+> - prettyCheck t absPrec - where - 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 $ - pretty k <+> line <+> prettyCheck t injPrec -prettyCheck (Tup ts) d = + prettyTerm t letPrec +lessPrettyTerm (Abs (bound ** t)) d = + parenthesise (d > absPrec) $ group $ hang 2 $ + "\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+> + prettyTerm t absPrec +lessPrettyTerm (App (Map (x ** a) b c) ts) d = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + concatWith (surround line) + ( pretty "map" + :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open) + :: prettyType b appPrec + :: prettyType c appPrec + :: prettyAllTerm ts appPrec) +lessPrettyTerm (App (GetChildren (x ** a) b) ts) d = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + concatWith (surround line) + ( pretty "getChildren" + :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open) + :: prettyType b appPrec + :: prettyAllTerm ts appPrec) +lessPrettyTerm (App f ts) d = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + concatWith (surround line) (prettyTerm f appPrec :: prettyAllTerm ts appPrec) +lessPrettyTerm (Tup (MkRow ts _)) d = enclose "<" ">" $ group $ align $ hang 2 $ - concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec) -prettyCheck (Case e ts) d = + concatWith (surround $ "<" <+> line) (prettyTermCtx ts tupPrec <>> []) +lessPrettyTerm (Prj e l) d = + parenthesise (d > prjPrec) $ group $ align $ hang 2 $ + prettyTerm e prjPrec <+> line' <+> "." <+> pretty l +lessPrettyTerm (Inj l t) d = + parenthesise (d >= injPrec) $ group $ align $ hang 2 $ + pretty l <+> line <+> prettyTerm t absPrec +lessPrettyTerm (Case e (MkRow ts _)) d = parenthesise (d > casePrec) $ group $ align $ hang 2 $ - "case" <++> prettySynth e casePrec <++> "of" <+> line <+> + "case" <++> prettyTerm e casePrec <++> "of" <+> hardline <+> (braces $ group $ align $ hang 2 $ - concatWith (surround $ ";" <+> line) $ - prettyCheckCtxBinding ts casePrec) -prettyCheck (Contract t) d = - "~" <+> - (parenthesise (d > contractPrec) $ group $ align $ hang 2 $ - prettyCheck t contractPrec) -prettyCheck (Fold e x t) d = + concatWith (surround $ ";" <+> hardline) $ + prettyCases ts <>> []) +lessPrettyTerm (Roll t) d = + pretty "~" <+> + (parenthesise (d > rollPrec) $ group $ align $ hang 2 $ prettyTerm t rollPrec) +lessPrettyTerm (Unroll e) d = + pretty "!" <+> + (parenthesise (d > unrollPrec) $ group $ align $ hang 2 $ prettyTerm e unrollPrec) +lessPrettyTerm (Fold e (x ** t)) d = parenthesise (d > foldPrec) $ group $ align $ hang 2 $ - "fold" <++> prettySynth e foldPrec <++> "by" <+> line <+> + "fold" <++> prettyTerm e foldPrec <++> "by" <+> hardline <+> (parens $ group $ align $ hang 2 $ - "\\" <+> 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 - -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 + "\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open) +lessPrettyTerm (Map (x ** a) b c) d = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + concatWith (surround line) + [ pretty "map" + , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open) + , prettyType b appPrec + , prettyType c appPrec + ] +lessPrettyTerm (GetChildren (x ** a) b) d = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + concatWith (surround line) + [ pretty "getChildren" + , parens (group $ align $ hang 2 $ "\\" <+> pretty x <+> "=>" <+> line <+> prettyType a Open) + , prettyType b appPrec + ] diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr deleted file mode 100644 index 1627307..0000000 --- a/src/Inky/Thinning.idr +++ /dev/null @@ -1,310 +0,0 @@ -module Inky.Thinning - -import public Inky.Context - -import Control.Function -import Control.WellFounded -import Data.DPair -import Data.Nat - --------------------------------------------------------------------------------- --- Thinnings ------------------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -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 - -public export -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) - -public export -index : ctx1 `Thins` ctx2 -> Var ctx1 v -> Var ctx2 v -index f i = indexPos f i.pos - -export -(.) : ctx2 `Thins` ctx3 -> ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx3 -Id . g = g -Drop f . g = Drop (f . g) -Keep f . Id = Keep f -Keep f . Drop g = Drop (f . g) -Keep f . Keep g = Keep (f . g) - --- Basic properties - -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 -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) - -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 : 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 ------------------------------------------------------------------ - -export -infix 6 ~~~ - -public export -data (~~~) : ctx1 `Thins` ctx2 -> ctx1 `Thins` ctx2 -> Type where - IdId : Id ~~~ Id - IdKeep : Id ~~~ f -> Id ~~~ Keep f - KeepId : f ~~~ Id -> Keep f ~~~ Id - DropDrop : f ~~~ g -> Drop f ~~~ Drop g - KeepKeep : f ~~~ g -> Keep f ~~~ Keep g - -%name Thinning.(~~~) prf - -(.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 -(.index) : f ~~~ g -> (i : Var ctx1 v) -> index f i = index g i -prf.index i = prf.indexPos i.pos - --- Useful for Parsers ---------------------------------------------------------- - -public export -dropAll : Length ctx2 -> ctx1 `Thins` ctx1 ++ ctx2 -dropAll Z = Id -dropAll (S len) = Drop (dropAll len) - -public export -keepAll : Length ctx -> ctx1 `Thins` ctx2 -> ctx1 ++ ctx `Thins` ctx2 ++ ctx -keepAll Z f = f -keepAll (S {x = x :- _} len) f = Keep (keepAll len f) - -public export -append : - ctx1 `Thins` ctx3 -> ctx2 `Thins` ctx4 -> - {auto len : Length ctx4} -> - ctx1 ++ ctx2 `Thins` ctx3 ++ ctx4 -append f Id = keepAll len f -append f (Drop g) {len = S len} = Drop (append f g) -append f (Keep g) {len = S len} = Keep (append f g) - -public export -assoc : Length ctx3 -> ctx1 ++ (ctx2 ++ ctx3) `Thins` (ctx1 ++ ctx2) ++ ctx3 -assoc Z = Id -assoc (S {x = x :- _} len) = Keep (assoc len) - -public export -growLength : ctx1 `Thins` ctx2 -> Length ctx1 -> Length ctx2 -growLength Id len = len -growLength (Drop f) len = S (growLength f len) -growLength (Keep f) (S len) = S (growLength f len) - -public export -thinLength : ctx1 `Thins` ctx2 -> Length ctx2 -> Length ctx1 -thinLength Id len = len -thinLength (Drop f) (S len) = thinLength f len -thinLength (Keep f) (S len) = S (thinLength f len) - -public export -thinAll : ctx1 `Thins` ctx2 -> All p ctx2 -> All p ctx1 -thinAll Id env = env -thinAll (Drop f) (env :< (x :- px)) = thinAll f env -thinAll (Keep {x, y} f) (env :< (_ :- px)) = thinAll f env :< (x :- px) - -public export -splitL : - {0 ctx1, ctx2, ctx3 : Context a} -> - Length ctx3 -> - ctx1 `Thins` ctx2 ++ ctx3 -> - Exists (\ctxA => Exists (\ctxB => (ctx1 = ctxA ++ ctxB, ctxA `Thins` ctx2, ctxB `Thins` ctx3))) -splitL Z f = Evidence ctx1 (Evidence [<] (Refl, f, Id)) -splitL (S len) Id = Evidence ctx2 (Evidence ctx3 (Refl, Id, Id)) -splitL (S len) (Drop f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitL len f in - Evidence ctxA (Evidence ctxB (Refl, g, Drop h)) -splitL (S len) (Keep f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitL len f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Keep h)) - -public export -splitR : - {0 ctx1, ctx2, ctx3 : Context a} -> - Length ctx2 -> - ctx1 ++ ctx2 `Thins` ctx3 -> - Exists (\ctxA => Exists (\ctxB => (ctx3 = ctxA ++ ctxB, ctx1 `Thins` ctxA, ctx2 `Thins` ctxB))) -splitR Z f = Evidence ctx3 (Evidence [<] (Refl, f, Id)) -splitR (S len) Id = Evidence ctx1 (Evidence ctx2 (Refl, Id, Id)) -splitR (S len) (Drop f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitR (S len) f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Drop h)) -splitR (S len) (Keep f) = - let Evidence ctxA (Evidence ctxB (Refl, g, h)) = splitR len f in - Evidence ctxA (Evidence (ctxB :< _) (Refl, g, Keep h)) - --------------------------------------------------------------------------------- --- Environments ---------------------------------------------------------------- --------------------------------------------------------------------------------- - -public export -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 ctx1 ctx2 p -> Var ctx1 v -> Either (Var ctx2 v) (p v) -lookup env i = lookupPos env i.pos - --- Properties - -export -lookupHere : - (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> - lookup (env :< (x :- pv)) (toVar Here) = Right pv -lookupHere env x pv = Refl - -export -lookupFS : - (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 : 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 :< (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 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 - --- Well Founded ---------------------------------------------------------------- - -export -Sized (Context a) where - size [<] = 0 - size (ctx :< x) = S (size ctx) - --- Environments ------------------------------------------------------ - -namespace DEnv - public export - data DEnv : (0 p : Context a -> a -> Type) -> Context a -> Type where - Lin : DEnv p [<] - (:<) : - DEnv p ctx -> (px : Assoc0 (p ctx x.value)) -> - {auto 0 prf : px.name = x.name} -> - DEnv p (ctx :< x) - - %name DEnv.DEnv env - - export - length : DEnv p ctx -> Length ctx - length [<] = Z - length (env :< px) = S (length env) - - public export - record Entry (p : Context a -> a -> Type) (ctx : Context a) (v : a) where - constructor MkEntry - {0 support : Context a} - 0 prf : support `Smaller` ctx - thins : support `Thins` ctx - value : p support v - - export - indexDEnvPos : VarPos ctx x v -> DEnv p ctx -> Entry p ctx v - indexDEnvPos Here (env :< px) = MkEntry reflexive (Drop Id) px.value - indexDEnvPos (There pos) (env :< px) = - let MkEntry prf thins value = indexDEnvPos pos env in - MkEntry (lteSuccRight prf) (Drop thins) value - - export - indexDEnv' : Var ctx v -> DEnv p ctx -> Entry p ctx v - indexDEnv' i env = indexDEnvPos i.pos env - - export - indexDEnv : Rename a p => Var ctx v -> DEnv p ctx -> p ctx v - indexDEnv i env = - let MkEntry _ f x = indexDEnv' i env in - rename f x - - export - mapProperty : ({0 ctx : Context a} -> {0 v : a} -> p ctx v -> q ctx v) -> DEnv p ctx -> DEnv q ctx - mapProperty f [<] = [<] - mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px) diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index 26f3c0f..45645bc 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -1,421 +1,734 @@ module Inky.Type -import Data.Bool.Decidable +import public Inky.Data.Context.Var +import public Inky.Data.Row +import public Inky.Data.SnocList.Var + +import Control.Function import Data.DPair -import Data.Maybe.Decidable import Data.These -import Data.These.Decidable -import Inky.Context -import Inky.Thinning + +import Inky.Data.SnocList.Thinning +import Inky.Data.Thinned +import Inky.Decidable +import Inky.Decidable.Maybe + +%hide Prelude.Ops.infixl.(>=>) -- Definition ------------------------------------------------------------------ public export -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 () +data Ty : SnocList String -> Type where + TVar : Var ctx -> Ty ctx + TArrow : Ty ctx -> Ty ctx -> Ty ctx + TProd : (as : Row (Ty ctx)) -> Ty ctx + TSum : (as : Row (Ty ctx)) -> Ty ctx + TFix : (x : String) -> Ty (ctx :< x) -> Ty ctx %name Ty a, b, c --------------------------------------------------------------------------------- +export +Injective TProd where + injective Refl = Refl + +export +Injective TSum where + injective Refl = Refl + +export +fixInjective : TFix x t = TFix y u -> the (x ** Ty (ctx :< x)) (x ** t) = (y ** u) +fixInjective Refl = Refl + +-- Decisions ------------------------------------------------------------------- + +export +Uninhabited (TVar i = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TSum as) where + uninhabited Refl impossible + +export +Uninhabited (TVar i = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TSum as) where + uninhabited Refl impossible + +export +Uninhabited (TArrow a b = TFix x c) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TSum bs) where + uninhabited Refl impossible + +export +Uninhabited (TProd as = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TArrow a b) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TProd bs) where + uninhabited Refl impossible + +export +Uninhabited (TSum as = TFix x a) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TArrow b c) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TProd as) where + uninhabited Refl impossible + +export +Uninhabited (TFix x a = TSum as) where + uninhabited Refl impossible + +public export +isArrow : + (a : Ty ctx) -> + Proof (Ty ctx, Ty ctx) (\bc => a = TArrow (fst bc) (snd bc)) + ((b, c : Ty ctx) -> Not (a = TArrow b c)) +isArrow (TVar i) = Nothing `Because` (\_, _ => absurd) +isArrow (TArrow a b) = Just (a, b) `Because` Refl +isArrow (TProd as) = Nothing `Because` (\_, _ => absurd) +isArrow (TSum as) = Nothing `Because` (\_, _ => absurd) +isArrow (TFix x a) = Nothing `Because` (\_, _ => absurd) + +public export +isProd : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TProd as) +isProd (TVar i) = Nothing `Because` (\_ => absurd) +isProd (TArrow a b) = Nothing `Because` (\_ => absurd) +isProd (TProd as) = Just as `Because` Refl +isProd (TSum as) = Nothing `Because` (\_ => absurd) +isProd (TFix x a) = Nothing `Because` (\_ => absurd) + +public export +isSum : (a : Ty ctx) -> DecWhen (Row (Ty ctx)) (\as => a = TSum as) +isSum (TVar i) = Nothing `Because` (\_ => absurd) +isSum (TArrow a b) = Nothing `Because` (\_ => absurd) +isSum (TProd as) = Nothing `Because` (\_ => absurd) +isSum (TSum as) = Just as `Because` Refl +isSum (TFix x a) = Nothing `Because` (\_ => absurd) + +public export +isFix : + (a : Ty ctx) -> + Proof (x ** Ty (ctx :< x)) (\xb => a = TFix (fst xb) (snd xb)) + ((x : _) -> (b : _) -> Not (a = TFix x b)) +isFix (TVar i) = Nothing `Because` (\_, _ => absurd) +isFix (TArrow a b) = Nothing `Because` (\_, _ => absurd) +isFix (TProd as) = Nothing `Because` (\_, _ => absurd) +isFix (TSum as) = Nothing `Because` (\_, _ => absurd) +isFix (TFix x a) = Just (x ** a) `Because` Refl + -- Thinning -------------------------------------------------------------------- --------------------------------------------------------------------------------- -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) +thin : ctx1 `Thins` ctx2 -> Ty ctx1 -> Ty ctx2 +thinAll : ctx1 `Thins` ctx2 -> Context (Ty ctx1) -> Context (Ty ctx2) +thinAllNames : + (f : ctx1 `Thins` ctx2) -> + (ctx : Context (Ty ctx1)) -> + (thinAll f ctx).names = ctx.names 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 (TProd (MkRow as fresh)) = TProd (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh)) +thin f (TSum (MkRow as fresh)) = TSum (MkRow (thinAll f as) (rewrite thinAllNames f as in fresh)) thin f (TFix x a) = TFix x (thin (Keep f) a) thinAll f [<] = [<] -thinAll f ((:<) as (x :- a) {fresh}) = - (:<) (thinAll f as) (x :- thin f a) {fresh = thinAllFresh f x as fresh} +thinAll f (as :< (n :- a)) = thinAll f as :< (n :- thin f a) -thinAllFresh f x [<] = id -thinAllFresh f x (as :< (y :- a)) = andSo . mapSnd (thinAllFresh f x as) . soAnd +thinAllNames f [<] = Refl +thinAllNames f (as :< (n :- a)) = cong (:< n) $ thinAllNames f as -- 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 : f ~~~ g -> (a : Ty ctx1) -> thin f a = thin g a +thinCongAll : f ~~~ g -> (as : Context (Ty ctx1)) -> 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 (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinCongAll prf as) +thinCong prf (TSum (MkRow as fresh)) = cong TSum (rowCong $ 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) +thinCongAll prf (as :< (n :- a)) = + cong2 (:<) (thinCongAll prf as) (cong (n :-) $ thinCong prf a) -thinId : (a : Ty ctx v) -> thin Id a = a -thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as +thinId : (a : Ty ctx) -> thin Id a = a +thinIdAll : (as : Context (Ty ctx)) -> thinAll Id as = as thinId (TVar (%% x)) = Refl -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 (TProd (MkRow as fresh)) = cong TProd (rowCong $ thinIdAll as) +thinId (TSum (MkRow as fresh)) = cong TSum (rowCong $ 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) +thinIdAll (as :< (n :- a)) = cong2 (:<) (thinIdAll as) (cong (n :-) $ thinId a) export -Rename () Ty where - var = TVar +Rename String Ty where rename = thin renameCong = thinCong renameId = thinId --- Equality -------------------------------------------------------------------- - -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 - -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) +-- Alpha Equivalence ------------------------------------------------------------ -public export -Eq (Ty ctx v) where - a == b = preeq a b Id +namespace Shape + public export + data SameShape : Ty ctx1 -> Ty ctx2 -> Type where + TVar : SameShape (TVar i) (TVar j) + TArrow : SameShape (TArrow a c) (TArrow b d) + TProd : SameShape (TProd as) (TProd bs) + TSum : SameShape (TSum as) (TSum bs) + TFix : SameShape (TFix x a) (TFix y b) export -Eq : {ctx : Context ()} -> {v : ()} -> Ty ctx v -> Ty ctx v -> Type -Eq a b = Preeq a b Id +Uninhabited (SameShape (TVar i) (TArrow b d)) + where uninhabited TVar impossible export -0 reflectEq : (a, b : Ty ctx v) -> (a `Eq` b) `Reflects` (a == b) -reflectEq a b = reflectPreeq a b Id +Uninhabited (SameShape (TVar i) (TProd bs)) + where uninhabited TVar impossible --- Occurs ---------------------------------------------------------------------- +export +Uninhabited (SameShape (TVar i) (TSum bs)) + where uninhabited TVar impossible -OccursIn : Var ctx v -> Ty ctx w -> Type -OccursInAny : Var ctx v -> Row (Ty ctx w) -> Type +export +Uninhabited (SameShape (TVar i) (TFix y b)) + where uninhabited TVar impossible -i `OccursIn` TVar j = i = j -i `OccursIn` TNat = Void -i `OccursIn` TArrow a b = These (i `OccursIn` a) (i `OccursIn` b) -i `OccursIn` TProd as = i `OccursInAny` as -i `OccursIn` TSum as = i `OccursInAny` as -i `OccursIn` TFix x a = ThereVar i `OccursIn` a +export +Uninhabited (SameShape (TArrow a b) (TVar j)) + where uninhabited TVar impossible -i `OccursInAny` [<] = Void -i `OccursInAny` (as :< (x :- a)) = These (i `OccursIn` a) (i `OccursInAny` as) +export +Uninhabited (SameShape (TArrow a c) (TProd bs)) + where uninhabited TVar impossible --- Decidable +export +Uninhabited (SameShape (TArrow a c) (TSum bs)) + where uninhabited TVar impossible -occursIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool -occursInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool +export +Uninhabited (SameShape (TArrow a c) (TFix y b)) + where uninhabited TVar impossible -i `occursIn` (TVar j) = i `eq` j -i `occursIn` TNat = False -i `occursIn` (TArrow a b) = (i `occursIn` a) || (i `occursIn` b) -i `occursIn` (TProd as) = i `occursInAny` as -i `occursIn` (TSum as) = i `occursInAny` as -i `occursIn` (TFix x a) = ThereVar i `occursIn` a +export +Uninhabited (SameShape (TProd as) (TVar j)) + where uninhabited TVar impossible -i `occursInAny` [<] = False -i `occursInAny` (as :< (x :- a)) = (i `occursIn` a) || (i `occursInAny` as) +export +Uninhabited (SameShape (TProd as) (TArrow b d)) + where uninhabited TVar impossible -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) +export +Uninhabited (SameShape (TProd as) (TSum bs)) + where uninhabited TVar impossible -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 (TProd as) = reflectOccursInAny i as -reflectOccursIn i (TSum as) = reflectOccursInAny i as -reflectOccursIn i (TFix x a) = reflectOccursIn (ThereVar i) a +export +Uninhabited (SameShape (TProd as) (TFix y b)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TVar j)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TArrow b d)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TProd bs)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TSum as) (TFix y b)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TVar j)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TArrow b d)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TProd bs)) + where uninhabited TVar impossible + +export +Uninhabited (SameShape (TFix x a) (TSum bs)) + where uninhabited TVar impossible + +namespace Equivalence + public export + data Alpha : Ty ctx1 -> Ty ctx2 -> Type + public export + data AllAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type + + data Alpha where + TVar : elemToNat i.pos = elemToNat j.pos -> Alpha (TVar i) (TVar j) + TArrow : Alpha a b -> Alpha c d -> Alpha (TArrow a c) (TArrow b d) + TProd : AllAlpha as.context bs.context -> Alpha (TProd as) (TProd bs) + TSum : AllAlpha as.context bs.context -> Alpha (TSum as) (TSum bs) + TFix : Alpha a b -> Alpha (TFix x a) (TFix y b) + + data AllAlpha where + Base : AllAlpha [<] [<] + Step : + (i : Elem (n :- b) bs) -> + Alpha a b -> + AllAlpha as (dropElem bs i) -> + AllAlpha (as :< (n :- a)) bs + +namespace Inequivalence + public export + data NotAlpha : Ty ctx1 -> Ty ctx2 -> Type + public export + data AnyNotAlpha : Context (Ty ctx1) -> Context (Ty ctx2) -> Type + + data NotAlpha where + Shape : + Not (SameShape a b) -> + NotAlpha a b + TVar : + Not (elemToNat i.pos = elemToNat j.pos) -> + NotAlpha (TVar i) (TVar j) + TArrow : + These (NotAlpha a b) (NotAlpha c d) -> + NotAlpha (TArrow a c) (TArrow b d) + TProd : + AnyNotAlpha as.context bs.context -> + NotAlpha (TProd as) (TProd bs) + TSum : + AnyNotAlpha as.context bs.context -> + NotAlpha (TSum as) (TSum bs) + TFix : + NotAlpha a b -> + NotAlpha (TFix x a) (TFix y b) + + data AnyNotAlpha where + Base : AnyNotAlpha [<] (bs :< b) + Step1 : + ((b : Ty ctx2) -> Not (Elem (n :- b) bs)) -> + AnyNotAlpha (as :< (n :- a)) bs + Step2 : + (i : Elem (n :- b) bs) -> + These (NotAlpha a b) (AnyNotAlpha as (dropElem bs i)) -> + AnyNotAlpha (as :< (n :- a)) bs + +%name Alpha prf +%name AllAlpha prfs +%name NotAlpha contra +%name AnyNotAlpha contras + +export +alphaShape : Alpha a b -> SameShape a b +alphaShape (TVar prf) = TVar +alphaShape (TArrow prf1 prf2) = TArrow +alphaShape (TProd prfs) = TProd +alphaShape (TSum prfs) = TSum +alphaShape (TFix prf) = TFix + +export +alphaRefl : (a : Ty ctx1) -> (0 b : Ty ctx2) -> a ~=~ b -> Alpha a b +allAlphaRefl : (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) -> as ~=~ bs -> AllAlpha as bs + +alphaRefl (TVar i) .(TVar i) Refl = TVar Refl +alphaRefl (TArrow a b) .(TArrow a b) Refl = TArrow (alphaRefl a a Refl) (alphaRefl b b Refl) +alphaRefl (TProd (MkRow as fresh)) .(TProd (MkRow as fresh)) Refl = TProd (allAlphaRefl as as Refl) +alphaRefl (TSum (MkRow as fresh)) .(TSum (MkRow as fresh)) Refl = TSum (allAlphaRefl as as Refl) +alphaRefl (TFix x a) .(TFix x a) Refl = TFix (alphaRefl a a Refl) + +allAlphaRefl [<] .([<]) Refl = Base +allAlphaRefl (as :< (l :- a)) .(as :< (l :- a)) Refl = + Step Here (alphaRefl a a Refl) (allAlphaRefl as as Refl) + +export +alphaSplit : + {0 a : Ty ctx1} -> {0 b : Ty ctx2} -> + Alpha a b -> NotAlpha a b -> Void +export +allAlphaSplit : + {0 as : Context (Ty ctx1)} -> {0 bs : Context (Ty ctx2)} -> + (0 fresh : AllFresh bs.names) -> + AllAlpha as bs -> AnyNotAlpha as bs -> Void + +alphaSplit prf (Shape contra) = contra (alphaShape prf) +alphaSplit (TVar prf) (TVar contra) = contra prf +alphaSplit (TArrow prf1 prf2) (TArrow contras) = + these (alphaSplit prf1) (alphaSplit prf2) (const $ alphaSplit prf2) contras +alphaSplit (TProd {bs} prfs) (TProd contras) = allAlphaSplit bs.fresh prfs contras +alphaSplit (TSum {bs} prfs) (TSum contras) = allAlphaSplit bs.fresh prfs contras +alphaSplit (TFix prf) (TFix contra) = alphaSplit prf contra + +allAlphaSplit fresh (Step i prf prfs) (Step1 contra) = void $ contra _ i +allAlphaSplit fresh (Step {as, n} i prf prfs) (Step2 j contras) = + let 0 eq = lookupUnique (MkRow bs fresh) i j in + these + (\contra => alphaSplit prf $ rewrite cong fst eq in contra) + (\contras => + allAlphaSplit (dropElemFresh bs fresh i) prfs $ + replace {p = \bi => AnyNotAlpha as (dropElem bs {x = n :- fst bi} $ snd bi)} + (sym eq) + contras) + (\contra, _ => alphaSplit prf $ rewrite cong fst eq in contra) + contras + +export +alpha : (a : Ty ctx1) -> (b : Ty ctx2) -> LazyEither (Alpha a b) (NotAlpha a b) +export +allAlpha : + (as : Context (Ty ctx1)) -> (bs : Context (Ty ctx2)) -> + LazyEither (AllAlpha as bs) (AnyNotAlpha as bs) + +alpha (TVar i) (TVar j) = map TVar TVar $ decEq (elemToNat i.pos) (elemToNat j.pos) +alpha (TVar i) (TArrow a b) = False `Because` Shape absurd +alpha (TVar i) (TProd as) = False `Because` Shape absurd +alpha (TVar i) (TSum as) = False `Because` Shape absurd +alpha (TVar i) (TFix x a) = False `Because` Shape absurd +alpha (TArrow a c) (TVar i) = False `Because` Shape absurd +alpha (TArrow a c) (TArrow b d) = map (uncurry TArrow) TArrow $ all (alpha a b) (alpha c d) +alpha (TArrow a c) (TProd as) = False `Because` Shape absurd +alpha (TArrow a c) (TSum as) = False `Because` Shape absurd +alpha (TArrow a c) (TFix x b) = False `Because` Shape absurd +alpha (TProd as) (TVar i) = False `Because` Shape absurd +alpha (TProd as) (TArrow a b) = False `Because` Shape absurd +alpha (TProd (MkRow as _)) (TProd bs) = map TProd TProd $ allAlpha as bs.context +alpha (TProd as) (TSum bs) = False `Because` Shape absurd +alpha (TProd as) (TFix x a) = False `Because` Shape absurd +alpha (TSum as) (TVar i) = False `Because` Shape absurd +alpha (TSum as) (TArrow a b) = False `Because` Shape absurd +alpha (TSum as) (TProd bs) = False `Because` Shape absurd +alpha (TSum (MkRow as _)) (TSum bs) = map TSum TSum $ allAlpha as bs.context +alpha (TSum as) (TFix x a) = False `Because` Shape absurd +alpha (TFix x a) (TVar i) = False `Because` Shape absurd +alpha (TFix x a) (TArrow b c) = False `Because` Shape absurd +alpha (TFix x a) (TProd as) = False `Because` Shape absurd +alpha (TFix x a) (TSum as) = False `Because` Shape absurd +alpha (TFix x a) (TFix y b) = map TFix TFix $ alpha a b + +allAlpha [<] [<] = True `Because` Base +allAlpha [<] (bs :< nb) = False `Because` Base +allAlpha (as :< (n :- a)) bs = + map + (\((b ** i) ** (prf1, prf2)) => Step i prf1 prf2) + (either Step1 false) $ + (bi := (decLookup n bs).forget) >=> + all (alpha a $ fst bi) (allAlpha as (dropElem bs $ snd bi)) + where + p : (b ** Elem (n :- b) bs) -> Type + p bi = (Alpha a (fst bi), AllAlpha as (dropElem bs $ snd bi)) + + q : (b ** Elem (n :- b) bs) -> Type + q bi = These (NotAlpha a (fst bi)) (AnyNotAlpha as (dropElem bs $ snd bi)) + + false : (bi ** q bi) -> AnyNotAlpha (as :< (n :- a)) bs + false ((b ** i) ** contras) = Step2 i contras + +-- Occurs ---------------------------------------------------------------------- -reflectOccursInAny i [<] = RFalse id -reflectOccursInAny i (as :< (x :- a)) = - reflectThese (reflectOccursIn i a) (reflectOccursInAny i as) +namespace Strengthen + public export + data Strengthen : (i : Var ctx) -> Ty ctx -> Ty (dropElem ctx i.pos) -> Type + public export + data StrengthenAll : + (i : Var ctx) -> (as : Context (Ty ctx)) -> + All (const $ Ty $ dropElem ctx i.pos) as.names -> Type + + data Strengthen where + TVar : (j = index (dropPos i.pos) k) -> Strengthen i (TVar j) (TVar k) + TArrow : Strengthen i a c -> Strengthen i b d -> Strengthen i (TArrow a b) (TArrow c d) + TProd : StrengthenAll i as.context bs -> Strengthen i (TProd as) (TProd $ fromAll as bs) + TSum : StrengthenAll i as.context bs -> Strengthen i (TSum as) (TSum $ fromAll as bs) + TFix : Strengthen (ThereVar i) a b -> Strengthen i (TFix x a) (TFix x b) + + data StrengthenAll where + Lin : StrengthenAll i [<] [<] + (:<) : StrengthenAll i as bs -> Strengthen i a b -> StrengthenAll i (as :< (l :- a)) (bs :< b) + + %name Strengthen prf + %name StrengthenAll prfs + +strengthenEq : Strengthen i a b -> a = thin (dropPos i.pos) b +strengthenAllEq : StrengthenAll i as bs -> as = thinAll (dropPos i.pos) (fromAll as bs) + +strengthenEq (TVar prf) = cong TVar prf +strengthenEq (TArrow prf1 prf2) = cong2 TArrow (strengthenEq prf1) (strengthenEq prf2) +strengthenEq (TProd {as = MkRow _ _} prfs) = cong TProd $ rowCong $ strengthenAllEq prfs +strengthenEq (TSum {as = MkRow _ _} prfs) = cong TSum $ rowCong $ strengthenAllEq prfs +strengthenEq (TFix prf) = cong (TFix _) $ strengthenEq prf + +strengthenAllEq [<] = Refl +strengthenAllEq ((:<) {l} prfs prf) = + cong2 (:<) (strengthenAllEq prfs) (cong (l :-) $ strengthenEq prf) + +namespace Occurs + public export + data OccursIn : Var ctx -> Ty ctx -> Type + public export + data OccursInAny : Var ctx -> Context (Ty ctx) -> Type + + data OccursIn where + TVar : i = j -> i `OccursIn` TVar j + TArrow : These (i `OccursIn` a) (i `OccursIn` b) -> i `OccursIn` TArrow a b + TProd : i `OccursInAny` as.context -> i `OccursIn` TProd as + TSum : i `OccursInAny` as.context -> i `OccursIn` TSum as + TFix : ThereVar i `OccursIn` a -> i `OccursIn` TFix x a + + data OccursInAny where + And : These (i `OccursInAny` as) (i `OccursIn` a) -> i `OccursInAny` (as :< (n :- a)) + + %name OccursIn contra + %name OccursInAny contras + +export +Uninhabited (i `OccursInAny` [<]) where + uninhabited (And prf) impossible + +export +strengthenSplit : Strengthen i a b -> i `OccursIn` a -> Void +strengthenAllSplit : StrengthenAll i as bs -> i `OccursInAny` as -> Void + +strengthenSplit (TVar Refl) (TVar {i = %% n} contra) = void $ lemma _ _ contra + where + lemma : + (i : Elem x sx) -> (j : Elem y (dropElem sx i)) -> + Not (toVar i = toVar (indexPos (dropPos i) j)) + lemma Here j prf = absurd (toVarInjective prf) + lemma (There i) Here prf = absurd (toVarInjective prf) + lemma (There i) (There j) prf = lemma i j $ toVarCong $ thereInjective $ toVarInjective prf +strengthenSplit (TArrow prf1 prf2) (TArrow contras) = + these (strengthenSplit prf1) (strengthenSplit prf2) (const $ strengthenSplit prf2) contras +strengthenSplit (TProd prfs) (TProd contras) = strengthenAllSplit prfs contras +strengthenSplit (TSum prfs) (TSum contras) = strengthenAllSplit prfs contras +strengthenSplit (TFix prf) (TFix contra) = strengthenSplit prf contra + +strengthenAllSplit (prfs :< prf) (And contras) = + these (strengthenAllSplit prfs) (strengthenSplit prf) (const $ strengthenSplit prf) contras + +export +strengthen : + (i : Var ctx) -> (a : Ty ctx) -> + Proof (Ty (dropElem ctx i.pos)) (Strengthen i a) (i `OccursIn` a) +export +strengthenAll : + (i : Var ctx) -> (as : Context (Ty ctx)) -> + Proof (All (const $ Ty $ dropElem ctx i.pos) as.names) (StrengthenAll i as) (i `OccursInAny` as) + +strengthen ((%%) x {pos = i}) (TVar ((%%) y {pos = j})) = + map (TVar . toVar) + (\_, prf => TVar $ toVarCong prf) + (TVar . toVarCong . skipsDropPos i) $ + strengthen (dropPos i) j +strengthen i (TArrow a b) = + map (uncurry TArrow) (\(c, d) => uncurry TArrow) TArrow $ + all (strengthen i a) (strengthen i b) +strengthen i (TProd (MkRow as fresh)) = + map (TProd . fromAll (MkRow as fresh)) (\_ => TProd) TProd $ + strengthenAll i as +strengthen i (TSum (MkRow as fresh)) = + map (TSum . fromAll (MkRow as fresh)) (\_ => TSum) TSum $ + strengthenAll i as +strengthen i (TFix x a) = + map (TFix x) (\_ => TFix) TFix $ + strengthen (ThereVar i) a + +strengthenAll i [<] = Just [<] `Because` [<] +strengthenAll i (as :< (l :- a)) = + map (uncurry (:<) . swap) (\(_, _) => uncurry (:<) . swap) (And . swap) $ + all (strengthen i a) (strengthenAll i as) -- Not Strictly Positive ----------------------------------------------------------- -- We use negation so we get a cause on failure. -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 = - -- 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 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` as :< (x :- a) = These (i `NotPositiveIn` a) (i `NotPositiveInAny` as) - --- Not Positive implies Occurs - -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) = id -notPositiveToOccurs (TProd as) = notPositiveAnyToOccursAny as -notPositiveToOccurs (TSum as) = notPositiveAnyToOccursAny as -notPositiveToOccurs (TFix x a) = id - -notPositiveAnyToOccursAny [<] = id -notPositiveAnyToOccursAny (as :< (x :- a)) = bimap (notPositiveToOccurs a) (notPositiveAnyToOccursAny as) - --- -- Decidable - -notPositiveIn : (i : Var ctx v) -> (a : Ty ctx w) -> Bool -notPositiveInAny : (i : Var ctx v) -> (as : Row (Ty ctx w)) -> Bool - -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 `notPositiveInAny` [<] = False -i `notPositiveInAny` (as :< (x :- a)) = (i `notPositiveIn` a) || (i `notPositiveInAny` as) - -reflectNotPositiveIn : - (i : Var ctx v) -> (a : Ty ctx w) -> - (i `NotPositiveIn` a) `Reflects` (i `notPositiveIn` a) -reflectNotPositiveInAny : - (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) = reflectOccursIn i (TArrow a b) -reflectNotPositiveIn i (TProd as) = reflectNotPositiveInAny i as -reflectNotPositiveIn i (TSum as) = reflectNotPositiveInAny i as -reflectNotPositiveIn i (TFix x a) = reflectOccursIn (ThereVar i) a - -reflectNotPositiveInAny i [<] = RFalse id -reflectNotPositiveInAny i (as :< (x :- a)) = - reflectThese (reflectNotPositiveIn i a) (reflectNotPositiveInAny i as) +namespace NotPositive + public export + data NotPositiveIn : Var ctx -> Ty ctx -> Type + public export + data NotPositiveInAny : Var ctx -> Context (Ty ctx) -> Type --- Well Formed ----------------------------------------------------------------- + data NotPositiveIn where + TArrow : i `OccursIn` TArrow a b -> i `NotPositiveIn` TArrow a b + TProd : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TProd as + TSum : i `NotPositiveInAny` as.context -> i `NotPositiveIn` TSum as + TFix : ThereVar i `NotPositiveIn` a -> i `NotPositiveIn` TFix x a --- Negating decidable properties is fun. + data NotPositiveInAny where + And : + These (i `NotPositiveInAny` as) (i `NotPositiveIn` a) -> + i `NotPositiveInAny` (as :< (n :- a)) + + %name NotPositiveIn prf + %name NotPositiveInAny prf + +export +Uninhabited (i `NotPositiveIn` TVar j) where + uninhabited (TArrow prf) impossible export -IllFormed : Ty ctx v -> Type -AnyIllFormed : Row (Ty ctx v) -> Type +Uninhabited (i `NotPositiveInAny` [<]) where + uninhabited (And prf) impossible -IllFormed (TVar v) = Void -IllFormed TNat = Void -IllFormed (TArrow a b) = These (IllFormed a) (IllFormed b) -IllFormed (TProd as) = AnyIllFormed as -IllFormed (TSum as) = AnyIllFormed as -IllFormed (TFix x a) = These (%% x `NotPositiveIn` a) (IllFormed a) +export +getOccurs : i `NotPositiveIn` a -> i `OccursIn` a +export +getOccursAny : i `NotPositiveInAny` as -> i `OccursInAny` as -AnyIllFormed [<] = Void -AnyIllFormed (as :< (x :- a)) = These (IllFormed a) (AnyIllFormed as) +getOccurs (TArrow prf) = prf +getOccurs (TProd prf) = TProd (getOccursAny prf) +getOccurs (TSum prf) = TSum (getOccursAny prf) +getOccurs (TFix prf) = TFix (getOccurs prf) --- Decidable +getOccursAny (And (This prf)) = And (This (getOccursAny prf)) +getOccursAny (And (That prf)) = And (That (getOccurs prf)) +getOccursAny (And (Both prf1 prf2)) = And (Both (getOccursAny prf1) (getOccurs prf2)) export -illFormed : (a : Ty ctx v) -> Bool -anyIllFormed : (as : Row (Ty ctx v)) -> Bool +notPositiveIn : (i : Var ctx) -> (a : Ty ctx) -> Dec' (i `NotPositiveIn` a) +notPositiveInAny : (i : Var ctx) -> (as : Context (Ty ctx)) -> Dec' (i `NotPositiveInAny` as) + +i `notPositiveIn` TVar j = False `Because` absurd +i `notPositiveIn` TArrow a b = + map TArrow (\(_ ** prf) => \case (TArrow contra) => strengthenSplit prf contra) $ + not $ + (strengthen i $ TArrow a b).forget +i `notPositiveIn` TProd (MkRow as _) = mapDec TProd (\case TProd prf => prf) (i `notPositiveInAny` as) +i `notPositiveIn` TSum (MkRow as _) = mapDec TSum (\case TSum prf => prf) (i `notPositiveInAny` as) +i `notPositiveIn` TFix x a = mapDec TFix (\case TFix prf => prf) $ ThereVar i `notPositiveIn` a + +i `notPositiveInAny` [<] = False `Because` absurd +i `notPositiveInAny` (as :< (n :- a)) = + mapDec (And . swap) (\case And prf => swap prf) $ + orDec (i `notPositiveIn` a) (i `notPositiveInAny` as) -illFormed (TVar j) = False -illFormed TNat = False -illFormed (TArrow a b) = illFormed a || illFormed b -illFormed (TProd as) = anyIllFormed as -illFormed (TSum as) = anyIllFormed as -illFormed (TFix x a) = (%% x `notPositiveIn` a) || illFormed a +-- Well Formed ----------------------------------------------------------------- -anyIllFormed [<] = False -anyIllFormed (as :< (x :- a)) = illFormed a || anyIllFormed as +-- Negating decidable properties is fun. +namespace WellFormed + public export + data IllFormed : Ty ctx -> Type + public export + data AnyIllFormed : Context (Ty ctx) -> Type + + data IllFormed where + TArrow : These (IllFormed a) (IllFormed b) -> IllFormed (TArrow a b) + TProd : AnyIllFormed as.context -> IllFormed (TProd as) + TSum : AnyIllFormed as.context -> IllFormed (TSum as) + TFix : These (toVar Here `NotPositiveIn` a) (IllFormed a) -> IllFormed (TFix x a) + + data AnyIllFormed where + And : These (AnyIllFormed as) (IllFormed a) -> AnyIllFormed (as :< (n :- a)) + +export +Uninhabited (IllFormed (TVar i)) where + uninhabited (TArrow prf) impossible + +export +Uninhabited (AnyIllFormed [<]) where + uninhabited (And prf) impossible + +export +illFormed : (a : Ty ctx) -> Dec' (IllFormed a) export -reflectIllFormed : (a : Ty ctx v) -> IllFormed a `Reflects` illFormed a -reflectAnyIllFormed : (as : Row (Ty ctx v)) -> AnyIllFormed as `Reflects` anyIllFormed as +anyIllFormed : (as : Context (Ty ctx)) -> Dec' (AnyIllFormed as) -reflectIllFormed (TVar j) = RFalse id -reflectIllFormed TNat = RFalse id -reflectIllFormed (TArrow a b) = reflectThese (reflectIllFormed a) (reflectIllFormed b) -reflectIllFormed (TProd as) = reflectAnyIllFormed as -reflectIllFormed (TSum as) = reflectAnyIllFormed as -reflectIllFormed (TFix x a) = reflectThese (reflectNotPositiveIn (%% x) a) (reflectIllFormed a) +illFormed (TVar j) = False `Because` absurd +illFormed (TArrow a b) = mapDec TArrow (\case TArrow prf => prf) $ orDec (illFormed a) (illFormed b) +illFormed (TProd (MkRow as _)) = mapDec TProd (\case TProd prf => prf) (anyIllFormed as) +illFormed (TSum (MkRow as _)) = mapDec TSum (\case TSum prf => prf) (anyIllFormed as) +illFormed (TFix x a) = mapDec TFix (\case TFix prf => prf) $ orDec (%% x `notPositiveIn` a) (illFormed a) -reflectAnyIllFormed [<] = RFalse id -reflectAnyIllFormed (as :< (x :- a)) = - reflectThese (reflectIllFormed a) (reflectAnyIllFormed as) +anyIllFormed [<] = False `Because` absurd +anyIllFormed (as :< (n :- a)) = + mapDec (And . swap) (\case And prf => swap prf) $ + orDec (illFormed a) (anyIllFormed as) -------------------------------------------------------------------------------- -- Substitution ---------------------------------------------------------------- -------------------------------------------------------------------------------- -public export -fromVar : Either (Var ctx v) (Ty ctx v) -> Ty ctx v -fromVar = either TVar id - export -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 : All (const $ Thinned Ty ctx2) ctx1 -> Ty ctx1 -> Ty ctx2 +subAll : All (const $ Thinned Ty ctx2) ctx1 -> Context (Ty ctx1) -> Context (Ty ctx2) +subAllNames : + (f : All (const $ Thinned Ty ctx2) ctx1) -> + (ctx : Context (Ty ctx1)) -> + (subAll f ctx).names = ctx.names + +sub env (TVar i) = (indexAll i.pos env).extract sub env (TArrow a b) = TArrow (sub env a) (sub env b) -sub env (TProd as) = TProd (subAll env as) -sub env (TSum as) = TSum (subAll env as) -sub env (TFix x a) = TFix x (sub (lift (Drop Id) env :< (x :- TVar (%% x))) a) +sub env (TProd (MkRow as fresh)) = TProd (MkRow (subAll env as) (rewrite subAllNames env as in fresh)) +sub env (TSum (MkRow as fresh)) = TSum (MkRow (subAll env as) (rewrite subAllNames env as in fresh)) +sub env (TFix x a) = TFix x (sub (mapProperty (rename (Drop Id)) env :< (TVar (%% x) `Over` Id)) a) subAll env [<] = [<] -subAll env ((:<) as (x :- a) {fresh}) = - (:<) (subAll env as) (x :- sub env a) {fresh = subAllFresh env x as fresh} +subAll env (as :< (n :- a)) = subAll env as :< (n :- sub env a) -subAllFresh env x [<] = id -subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd +subAllNames env [<] = Refl +subAllNames env (as :< (n :- a)) = cong (:< n) (subAllNames env as) --- Expansion ------------------------------------------------------------------- +-- Special Types --------------------------------------------------------------- -export -expandEnv : DEnv Ty ctx -> Env ctx [<] (Ty [<]) -expandEnv [<] = Base Id -expandEnv {ctx = ctx :< (x :- v)} (env :< (y :- a)) = - let env' = expandEnv env in - expandEnv env :< (x :- sub env' a) +public export +TNat : Ty ctx +TNat = TFix "Nat" (TSum [<"Z" :- TProd [<], "S" :- TVar (%% "Nat")]) -export -expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v -expand = sub . expandEnv +public export +TList : Ty ctx -> Ty ctx +TList a = + TFix "List" (TSum + [<"N" :- TProd [<] + , "C" :- TProd [<"H" :- thin (Drop Id) a, "T" :- TVar (%% "List")]]) + +-- Testing if we have a list + +-- TODO: prove correct +isList : (a : Ty ctx) -> Maybe (Ty ctx) +isList (TFix x (TSum (MkRow + [<"N" :- TProd (MkRow [<] _) + , "C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"N" :- TProd (MkRow [<] _) + , "C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"C" :- TProd (MkRow [<"H" :- a, "T" :- TVar ((%%) x {pos = Here})] _) + , "N" :- TProd (MkRow [<] _)] _))) = + does (strengthen (%% x) a) +isList (TFix x (TSum (MkRow + [<"C" :- TProd (MkRow [<"T" :- TVar ((%%) x {pos = Here}), "H" :- a] _) + , "N" :- TProd (MkRow [<] _)] _))) = + does (strengthen (%% x) a) +isList _ = Nothing diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr index 83253b4..aaef606 100644 --- a/src/Inky/Type/Pretty.idr +++ b/src/Inky/Type/Pretty.idr @@ -1,43 +1,55 @@ module Inky.Type.Pretty -import Inky.Context +import Data.Singleton +import Inky.Decidable import Inky.Type import Text.PrettyPrint.Prettyprinter -arrowPrec, prodPrec, sumPrec, fixPrec : Prec +arrowPrec, prodPrec, sumPrec, fixPrec, listPrec : Prec arrowPrec = Open prodPrec = Open sumPrec = Open fixPrec = Open +listPrec = App export -prettyType : {ctx : Context ()} -> Ty ctx () -> Prec -> Doc ann -prettyTypeRow : {ctx : Context ()} -> Row (Ty ctx ()) -> Prec -> List (Doc ann) +prettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann +lessPrettyType : {ctx : SnocList String} -> Ty ctx -> Prec -> Doc ann +lessPrettyTypeRow : {ctx : SnocList String} -> Context (Ty ctx) -> Prec -> List (Doc ann) -prettyType (TVar i) d = pretty (unVal $ nameOf i) -prettyType TNat d = pretty "Nat" -prettyType (TArrow a b) d = +prettyType a d = + if does (alpha {ctx2 = [<]} a TNat) + then pretty "Nat" + else case isList a of + Just b => + parenthesise (d >= listPrec) $ group $ align $ hang 2 $ + pretty "List" <+> line <+> + prettyType (assert_smaller a b) d + Nothing => lessPrettyType a d + +lessPrettyType (TVar i) d = pretty (unVal $ nameOf i) +lessPrettyType (TArrow a b) d = parenthesise (d > arrowPrec) $ group $ align $ hang 2 $ let parts = stripArrow b in concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts) where - stripArrow : Ty ctx () -> List (Doc ann) + stripArrow : Ty ctx -> List (Doc ann) stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b stripArrow a = [prettyType a arrowPrec] -prettyType (TProd as) d = +lessPrettyType (TProd (MkRow as _)) d = enclose "<" ">" $ group $ align $ hang 2 $ - let parts = prettyTypeRow as prodPrec in + let parts = lessPrettyTypeRow as prodPrec in concatWith (surround $ "," <+> line) parts -prettyType (TSum as) d = +lessPrettyType (TSum (MkRow as _)) d = enclose "[" "]" $ group $ align $ hang 2 $ - let parts = prettyTypeRow as prodPrec in + let parts = lessPrettyTypeRow as prodPrec in concatWith (surround $ "," <+> line) parts -prettyType (TFix x a) d = +lessPrettyType (TFix x a) d = parens $ group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a fixPrec -prettyTypeRow [<] d = [] -prettyTypeRow (as :< (x :- a)) d = +lessPrettyTypeRow [<] d = [] +lessPrettyTypeRow (as :< (x :- a)) d = (group $ align $ hang 2 $ pretty x <+> ":" <+> line <+> prettyType a d) - :: prettyTypeRow as d + :: lessPrettyTypeRow as d -- cgit v1.2.3