From 8b326bb4a879be72cb6382519350cbb5231f7a6e Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 9 Oct 2024 16:26:23 +0100 Subject: Do a lot. - Add type aliases. - Make `suc` a symbol. - Fix incorrect specification for `IsFunction`. - Write parser for terms. - Use `collie` to improve command line experience. --- src/Inky.idr | 183 +++++++++++++++-- src/Inky/Context.idr | 15 +- src/Inky/Parser.idr | 264 ++++++++++++------------- src/Inky/Term.idr | 499 +++++++++++++++++++++++++---------------------- src/Inky/Term/Parser.idr | 369 ++++++++++++++++++++++++++++++++--- src/Inky/Term/Pretty.idr | 32 +-- src/Inky/Thinning.idr | 58 +++++- src/Inky/Type.idr | 13 ++ src/Inky/Type/Pretty.idr | 2 +- 9 files changed, 1004 insertions(+), 431 deletions(-) (limited to 'src') diff --git a/src/Inky.idr b/src/Inky.idr index 5c7a821..bd3975f 100644 --- a/src/Inky.idr +++ b/src/Inky.idr @@ -1,13 +1,18 @@ module Inky +import Collie import Control.App import Control.App.Console import Control.App.FileIO import Inky.Context 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 @@ -16,6 +21,10 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal %default partial +%hide Collie.Modifiers.infix.(::=) + +-- Actions --------------------------------------------------------------------- + lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken)) lexInkyString file = do let (tokens, _, _, "") = lex tokenMap file @@ -31,37 +40,171 @@ parseType toks = do | Left msg => throw msg pure a +parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (CheckTerm [<] [<]) +parseTerm toks = do + let Ok res [] _ = parse @{EqI} OpenCheck 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 a = do let False = illFormed a | True => throw "type ill-formed" pure () +checkTerm : HasErr String es => Ty [<] () -> CheckTerm [<] [<] -> App es () +checkTerm a t = do + let True = checks [<] [<] a t + | False => throw "term ill-typed" + pure () + printType : PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> Ty [<] () -> App es () printType a = do primIO $ renderIO $ layoutSmart opts $ prettyType a Open -ppType : FileIO es => PrimIO es => HasErr String es => App es () -ppType = do - file <- fGetStr stdin - toks <- lexInkyString file - a <- parseType toks - checkType a - printType a +printTerm : + PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> + CheckTerm [<] [<] -> App es () +printTerm a = do + primIO $ renderIO $ layoutSmart opts $ prettyCheck a Open -main : IO () -main = - run $ - handle {err = IOError} - (handle {err = String} ppType - (const $ pure ()) - printErrLn) - (const $ pure ()) - (printErrLn . show) +readFile : FileIO es => File -> App es String +readFile f = do + content <- read [<] f + pure (fastConcat $ content <>> []) where - printErrLn : PrimIO es => String -> App es () - printErrLn msg = do - primIO $ () <$ fPutStrLn stderr msg - pure () + read : SnocList String -> File -> App es (SnocList String) + read acc f = do + False <- fEOF f + | True => pure acc + str <- fGetStr f + read (acc :< str) f + +readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String +readFileOrStdin Nothing = readFile stdin +readFileOrStdin (Just path) = withFile path Read throw readFile + + +-- Arguments ------------------------------------------------------------------- + +Inky : Command "inky" +Inky = MkCommand + { description = """ + tool suite for Primrose programs + """ + , subcommands = + [ "--help" ::= basic "print this help text" none + , "format" ::= MkCommand + { description = """ + pretty print data + """ + , subcommands = + [ "type" ::= basic "print a type" filePath + , "term" ::= basic "print a term" filePath + ] + , modifiers = [] + , arguments = none + } + , "check" ::= MkCommand + { description = """ + check well-formedness + """ + , subcommands = + [ "type" ::= basic "check a type" filePath + , "term" ::= MkCommand + { description = "check a term" + , subcommands = [] + , modifiers = ["--type" ::= option "type to check against" filePath] + , arguments = filePath + } + ] + , modifiers = [] + , arguments = none + } + ] + , modifiers = [] + , arguments = none + } + +-- Driver ---------------------------------------------------------------------- + +parseArgs : + (cmd : Command nm) -> + App (String :: Init) (ParseTree cmd) +parseArgs cmd = do + Right args <- primIO cmd.parseArgs + | Left msg => throw msg + let Pure args = ParsedTree.finalising args + | Fail errs => throw (show $ the (Error ()) $ Fail errs) + pure args + +abortErr : PrimIO es => String -> App es a +abortErr msg = do + primIO $ () <$ fPutStrLn stderr msg + primIO exitFailure + +showHelp : Console es => App es () +showHelp = putStrLn "Usage: \{Inky .usage}" + +main : IO () +main = run {l = MayThrow} $ do + args <- handle {err = String} (parseArgs Inky) pure abortErr + Collie.handle {cmd = ("inky" ** Inky)} args + [ const showHelp + , "--help" ::= [ const showHelp ] + , "format" ::= + [ const showHelp + , "type" ::= + [ \cmd => do + let path = cmd.arguments + txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show) + toks <- handle {err = String} (lexInkyString txt) pure abortErr + a <- handle {err = String} (parseType toks) pure abortErr + printType a + pure () + ] + , "term" ::= + [ \cmd => do + let path = cmd.arguments + txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show) + toks <- handle {err = String} (lexInkyString txt) pure abortErr + t <- handle {err = String} (parseTerm toks) pure abortErr + printTerm t + pure () + ] + ] + , "check" ::= + [ const showHelp + , "type" ::= + [ \cmd => do + let path = cmd.arguments + txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show) + toks <- handle {err = String} (lexInkyString txt) pure abortErr + a <- handle {err = String} (parseType toks) pure abortErr + handle {err = String} (checkType a) pure abortErr + ] + , "term" ::= + [ \cmd => do + let path = cmd.arguments + txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show) + toks <- handle {err = String} (lexInkyString txt) pure abortErr + t <- handle {err = String} (parseTerm toks) pure abortErr + let [type] = cmd.modifiers.content + a <- + maybe (pure (TArrow TNat TNat)) + (\path => do + txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show) + toks <- handle {err = String} (lexInkyString txt) pure abortErr + a <- handle {err = String} (parseType toks) pure abortErr + handle {err = String} (checkType a) pure abortErr + pure a) + type + handle {err = String} (checkTerm a t) pure abortErr + ] + ] + ] diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr index 2e9af8f..586aae2 100644 --- a/src/Inky/Context.idr +++ b/src/Inky/Context.idr @@ -70,6 +70,11 @@ public export 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 @@ -111,6 +116,14 @@ 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 @@ -237,7 +250,7 @@ namespace Quantifier Lin : All p [<] (:<) : All p ctx -> (px : Assoc0 (p x.value)) -> - {auto 0 prf : px.name = x.name}-> + {auto 0 prf : px.name = x.name} -> All p (ctx :< x) %name Quantifier.All env diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr index c44e7bd..fc553ec 100644 --- a/src/Inky/Parser.idr +++ b/src/Inky/Parser.idr @@ -359,6 +359,42 @@ namespace M map f (Err msg) = Err msg map f (Ok res ys prf) = Ok (f res) ys prf + export + pure : {xs : List a} -> (x : b) -> M xs True b + pure x = Ok x xs (Lax reflexive) + + export + (>>=) : + M xs nil b -> + (b -> {ys : List a} -> {auto 0 prf : SmallerX nil ys xs} -> M ys nil' c) -> + M xs (nil && nil') c + Err str >>= f = Err str + Ok res ys prf >>= f = + case f {ys, prf} res of + Err str => Err str + Ok res' zs prf' => Ok res' zs (rewrite andCommutative nil nil' in transX prf' prf) + + export + take : + Eq a => + Interpolation a => + (toks : List a) -> + (xs : List (WithBounds (Token a))) -> + M xs False String + take [tok] [] = Err "expected \{tok}; got end of input" + take toks [] = Err "expected one of: \{join ", " $ map (\k => "\{k}") toks}; got end of input" + take toks (x :: xs) = + if x.val.kind `elem` toks + then Ok x.val.text xs (Strict reflexive) + else case toks of + [tok] => Err "\{x.bounds}: expected \{tok}; got \{x.val.kind}" + toks => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") toks}; got \{x.val.kind}" + + export + bounds : (xs : List (WithBounds a)) -> M xs True (Bool, Bounds) + bounds [] = Ok (True, MkBounds (-1) (-1) (-1) (-1)) [] (Lax reflexive) + bounds (x :: xs) = Ok (x.isIrrelevant, x.bounds) (x :: xs) (Lax reflexive) + export wknL : M xs b1 a -> (b2 : Bool) -> M xs (b1 || b2) a wknL (Err msg) b2 = Err msg @@ -381,30 +417,34 @@ namespace M -- The Big Function -data FirstNil : List Bool -> Type where - Here : FirstNil (True :: bs) - There : FirstNil bs -> FirstNil (False :: bs) - -findNil : (nils : List Bool) -> Maybe (FirstNil nils) -findNil [] = Nothing -findNil (False :: bs) = There <$> findNil bs -findNil (True :: bs) = Just Here - -memberOf : Eq a => (x : a) -> All.All (const $ List a) xs -> Maybe (Any (const ()) xs) -memberOf x [] = Nothing -memberOf x (xs :: xss) = - if x `elem` xs - then Just (Here ()) - else There <$> (x `memberOf` xss) +||| Searches `sets` for the first occurence of `x`. +||| On failure, returns the index for the nil element, if it exists. +||| +||| # Unsafe Invariants +||| * `nils` has at most one `True` element +||| * `sets` are disjoint +lookahead : + Eq a => + (x : Maybe a) -> + (nils : List Bool) -> + (sets : Lazy (All (const $ List a) nils)) -> + Maybe (Any (const ()) nils) +lookahead x [] [] = Nothing +lookahead x (nil :: nils) (set :: sets) = + (do + x <- x + if x `elem` set then Just (Here ()) else Nothing) + <|> There <$> lookahead x nils sets + <|> (if nil then Just (Here ()) else Nothing) parser : (e : Eq i) => Interpolation i => (p : Parser i nil locked free a) -> - (penv1 : _) -> - (penv2 : _) -> - (fenv1 : _) -> - (fenv2 : _) -> - {auto 0 wf : So (wellTyped e penv1 penv2 fenv1 fenv2 p)} -> + {penv1 : _} -> + {penv2 : _} -> + {0 fenv1 : _} -> + {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 -> @@ -412,140 +452,96 @@ parser : parserChain : (e : Eq i) => Interpolation i => (ps : ParserChain i nil locked free as) -> - (penv1 : _) -> - (penv2 : _) -> - (fenv1 : _) -> - (fenv2 : _) -> - {auto 0 wf : So (wellTypedChain e penv1 penv2 fenv1 fenv2 ps)} -> + {penv1 : _} -> + {penv2 : _} -> + {0 fenv1 : _} -> + {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 -> M xs nil (HList as) -parserNil : +parserOneOf : (e : Eq i) => Interpolation i => - (at : FirstNil nils) -> + {nils : List Bool} -> + (at : Any (const ()) nils) -> (ps : All (\nil => Parser i nil locked free a) nils) -> - (penv1 : _) -> - (penv2 : _) -> - (fenv1 : _) -> - (fenv2 : _) -> - {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} -> + {penv1 : _} -> + {penv2 : _} -> + {0 fenv1 : _} -> + {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 -> M xs (any Basics.id nils) a -parserOneOf : - (e : Eq i) => Interpolation i => - {nils : List Bool} -> - (at : Any (const ()) nils) -> - (ps : All (\nil => Parser i nil locked free a) nils) -> - (penv1 : _) -> - (penv2 : _) -> - (fenv1 : _) -> - (fenv2 : _) -> - {auto 0 wf : So (allWellTyped e penv1 penv2 fenv1 fenv2 ps)} -> - (xs : List1 (WithBounds (Token i))) -> - All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX False ys (forget xs)) -> uncurry (M ys) x) locked -> - All (\x => (ys : List (WithBounds (Token i))) -> (0 _ : SmallerX True ys (forget xs)) -> uncurry (M ys) x) free -> - M (forget xs) (any Basics.id nils) a - -parser (Var x) penv1 penv2 fenv1 fenv2 xs env1 env2 = + +parser (Var x) wf xs env1 env2 = indexAll x env2 xs (Lax reflexive) -parser (Lit text) penv1 penv2 fenv1 fenv2 xs env1 env2 = - case xs of - [] => Err "expected \{text}, got end of file" - y :: ys => - if y.val.kind == text - then Ok y.val.text ys (Strict reflexive) - else Err "\{y.bounds}: expected \{text}, got \{y.val.kind}" -parser (Seq ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = - parserChain ps penv1 penv2 fenv1 fenv2 xs env1 env2 -parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 [] env1 env2 {wf} = +parser (Lit text) wf xs env1 env2 = take [text] xs +parser (Seq ps) wf xs env1 env2 = + parserChain ps wf xs env1 env2 +parser (OneOf {nils} ps) wf [] env1 env2 = let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in - case findNil nils of + let sets = peekAll penv2 ps in + case lookahead Nothing nils sets of Nothing => Err "unexpected end of input" - Just at => parserNil at ps penv1 penv2 fenv1 fenv2 [] env1 env2 -parser (OneOf {nils} ps) penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 {wf = wf} = + Just at => parserOneOf at ps (snd wfs) [] env1 env2 +parser (OneOf {nils} ps) wf (x :: xs) env1 env2 = let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in let sets = peekAll penv2 ps in - case x.val.kind `memberOf` sets of - Just at => parserOneOf at ps penv1 penv2 fenv1 fenv2 (x ::: xs) env1 env2 - Nothing => case findNil nils of - Nothing => - Err - "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}" - Just at => parserNil at ps penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 -parser (Fix {a, nil} x p) penv1 penv2 fenv1 fenv2 xs env1 env2 = - let f = parser p _ _ _ _ {wf} in - let - res : M xs nil a - res = - 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 - :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) - ) - (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2)) - xs - (Lax reflexive) - in - res -parser (Map f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = - f <$> parser p penv1 penv2 fenv1 fenv2 xs env1 env2 -parser (WithBounds p) penv1 penv2 fenv1 fenv2 xs env1 env2 = - case xs of - [] => irrelevantBounds <$> parser p penv1 penv2 fenv1 fenv2 [] env1 env2 - (x :: xs) => - (\y => MkBounded y x.isIrrelevant x.bounds) <$> - parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - -parserChain [] penv1 penv2 fenv1 fenv2 xs env1 env2 = Ok [] xs (Lax reflexive) -parserChain ((::) {nil1 = False, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + case lookahead (Just x.val.kind) nils sets of + Nothing => Err "\{x.bounds}: expected one of: \{join ", " $ map (\k => "\{k}") $ concat $ forget sets}; got \{x.val.kind}" + Just at => parserOneOf at ps (snd wfs) (x :: xs) env1 env2 +parser (Fix {a, nil} x p) wf xs env1 env2 = + let f = parser p wf in + 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 + :< (x :- (\zs, prf => rec zs (toSmaller prf) (forget $ transX prf lte))) + ) + (mapProperty (\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 +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) + pure (MkBounded x irrel bounds) + +parserChain [] wf xs env1 env2 = Ok [] xs (Lax reflexive) +parserChain ((::) {nil1 = False, nil2} p ps) wf xs env1 env2 = let 0 wfs = soAnd wf in - let 0 wfs' = soAnd (snd wfs) in - case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of - Err msg => Err msg - Ok x ys lt => - case - parserChain ps [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) - ys + let 0 wfs' = soAnd (snd wfs) in do + x <- parser p (fst wfs') xs env1 env2 + y <- parserChain ps (snd wfs') + _ [<] - ( mapProperty (\f, zs, 0 prf => f zs $ forget $ transX prf lt) env2 - ++ mapProperty (\f, zs, 0 prf => f zs $ transX prf lt) env1 + ( 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 ) - of - Err msg => Err msg - Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt) -parserChain ((::) {nil1 = True, nil2} p ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = - let 0 wfs = soAnd wf in - let 0 wfs' = soAnd (snd wfs) in - case parser p penv1 penv2 fenv1 fenv2 xs env1 env2 of - Err msg => Err msg - Ok x ys lte => - case - parserChain ps penv1 penv2 fenv1 fenv2 - ys - (mapProperty (\f, zs, prf => f zs $ transX prf lte) env1) - (mapProperty (\f, zs, prf => f zs $ transX prf lte) env2) - of - Err msg => Err msg - Ok y zs prf => Ok (x :: y) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte) - -parserNil {nils = True :: nils} Here (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + pure (x :: y) +parserChain ((::) {nil1 = True, nil2} p ps) wf xs env1 env2 = let 0 wfs = soAnd wf in - rewrite anyTrue nils in - parser p penv1 penv2 fenv1 fenv2 xs env1 env2 -parserNil (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = - let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in - parserNil at ps penv1 penv2 fenv1 fenv2 xs env1 env2 - -parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + let 0 wfs' = soAnd (snd wfs) in do + x <- parser p (fst wfs') 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) + pure (x :: y) + +parserOneOf {nils = nil :: nils} (Here ()) (p :: ps) wf xs env1 env2 = let 0 wfs = soAnd wf in - anyR nils (parser p penv1 penv2 fenv1 fenv2 (forget xs) env1 env2) -parserOneOf {nils = nil :: nils} (There at) (p :: ps) penv1 penv2 fenv1 fenv2 xs env1 env2 = + anyR nils (parser p (fst wfs) xs env1 env2) +parserOneOf {nils = nil :: nils} (There at) (p :: ps) wf xs env1 env2 = let 0 wfs = soAnd {a = wellTyped e penv1 penv2 fenv1 fenv2 p} wf in - anyL nil (parserOneOf at ps penv1 penv2 fenv1 fenv2 xs env1 env2) + anyL nil (parserOneOf at ps (snd wfs) xs env1 env2) export parse : @@ -553,7 +549,7 @@ parse : (p : Parser i nil [<] [<] a) -> {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} -> (xs : List (WithBounds (Token i))) -> M xs nil a -parse p xs = parser p [<] [<] [<] [<] xs [<] [<] +parse p xs = parser p wf xs [<] [<] -- Functor --------------------------------------------------------------------- diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 807b3e3..54e51ae 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -20,17 +20,21 @@ data CheckTerm : (tyCtx, tmCtx : Context ()) -> Type data SynthTerm where Var : Var tmCtx v -> SynthTerm tyCtx tmCtx Lit : Nat -> SynthTerm tyCtx tmCtx - Suc : CheckTerm tyCtx tmCtx -> SynthTerm tyCtx tmCtx + Suc : SynthTerm tyCtx tmCtx App : SynthTerm tyCtx tmCtx -> (args : List (CheckTerm tyCtx tmCtx)) -> - {auto 0 _ : NonEmpty args} -> + {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 :- ())) -> @@ -178,32 +182,31 @@ IsFunction : Type IsFunction [<] fun dom cod = (dom = [<], cod = fun) IsFunction (bound :< (x :- ())) fun dom cod = - ( b ** c ** - ( IsArrow fun b c - , ( dom' ** - ( dom = dom' :< (x :- b) - , IsFunction bound c dom' cod + ( dom' ** cod' ** + ( IsFunction bound fun dom' cod' + , ( b ** + ( IsArrow cod' b cod + , dom = dom' :< (x :- b) )) )) - isFunctionUnique : (bound : Context ()) -> (a : Ty tyCtx ()) -> forall dom1, dom2, cod1, cod2. IsFunction bound a dom1 cod1 -> IsFunction bound a dom2 cod2 -> (dom1 = dom2, cod1 = cod2) isFunctionUnique [<] a (Refl, Refl) (Refl, Refl) = (Refl, Refl) isFunctionUnique (bound :< (x :- ())) a - (b1 ** c1 ** (isArrow1, (dom1' ** (Refl, isFunc1)))) - (b2 ** c2 ** (isArrow2, (dom2' ** (Refl, isFunc2)))) - with (isArrowUnique a isArrow1 isArrow2) + (dom1 ** cod1 ** (isFunc1, (b1 ** (isArrow1, eq1)))) + (dom2 ** cod2 ** (isFunc2, (b2 ** (isArrow2, eq2)))) + with (isFunctionUnique bound a isFunc1 isFunc2) isFunctionUnique (bound :< (x :- ())) a - (b ** c ** (_, (dom1' ** (Refl, isFunc1)))) - (b ** c ** (_, (dom2' ** (Refl, isFunc2)))) + (dom ** cod ** (_, (b1 ** (isArrow1, eq1)))) + (dom ** cod ** (_, (b2 ** (isArrow2, eq2)))) | (Refl, Refl) - with (isFunctionUnique bound c isFunc1 isFunc2) + with (isArrowUnique cod isArrow1 isArrow2) isFunctionUnique (bound :< (x :- ())) a - (b ** c ** (_, (dom' ** (Refl, _)))) - (b ** c ** (_, (dom' ** (Refl, _)))) + (dom ** cod ** (_, (b ** (isArrow1, Refl)))) + (dom ** cod ** (_, (b ** (isArrow2, Refl)))) | (Refl, Refl) | (Refl, Refl) = (Refl, Refl) isFunction : @@ -211,154 +214,168 @@ isFunction : Maybe (All (const $ Ty tyCtx ()) bound, Ty tyCtx ()) isFunction [<] a = Just ([<], a) isFunction (bound :< (x :- ())) a = do - (b, c) <- isArrow a - (dom, cod) <- isFunction bound c + (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 (reflectIsArrow a) | (isArrow a) - _ | RJust isArrow | Just (b, c) with (reflectIsFunction bound c) | (isFunction bound c) - _ | RJust isFunc | Just (dom, cod) = RJust (b ** c ** (isArrow , (dom ** (Refl, isFunc)))) - _ | RNothing notFunc | _ = - RNothing (\(dom :< (x :- b'), cod), (b' ** c' ** (isArrow', (dom ** (Refl, isFunc)))) => - let (eq1, eq2) = isArrowUnique a {b, c, d = b', e = c'} isArrow isArrow' in - let isFunc = rewrite eq2 in isFunc in - notFunc (dom, cod) isFunc) - _ | RNothing notArrow | _ = - RNothing (\(dom, cod), (b ** c ** (isArrow, _)) => notArrow (b, c) isArrow) +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 : - {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> - SynthTerm tyCtx tmCtx -> Ty tyCtx () -> Type + {tmCtx : Context ()} -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + SynthTerm tyCtx tmCtx -> Ty [<] () -> Type Checks : - {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> - Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Type + {tmCtx : Context ()} -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Ty [<] () -> CheckTerm tyCtx tmCtx -> Type CheckSpine : - {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> - (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty tyCtx ()) -> Type + {tmCtx : Context ()} -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> (res : Ty [<] ()) -> Type AllCheck : - {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> - Row (Ty tyCtx ()) -> Row (CheckTerm tyCtx tmCtx) -> Type + {tmCtx : Context ()} -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Type AllCheckBinding : - {tyCtx, tmCtx : Context ()} -> (env : All (const (Ty tyCtx ())) tmCtx) -> - Row (Ty tyCtx ()) -> Ty tyCtx () -> + {tmCtx : Context ()} -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Row (Ty [<] ()) -> Ty [<] () -> Row (x : String ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Type -Synths env (Var i) a = (a = indexAll i env) -Synths env (Lit k) a = (a = TNat) -Synths env (Suc t) a = (Checks env TNat t, a = TNat) -Synths env (App e ts) a = +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 env e fun - , CheckSpine env fun ts a + ( Synths tyEnv env e fun + , CheckSpine tyEnv env fun ts a )) -Synths env (Prj e x) a = +Synths tyEnv env (Prj e x) a = ( b ** - ( Synths env e b + ( Synths tyEnv env e b , ( as ** ( IsProduct b as , GetAt x as a )) )) -Synths env (Expand e) a = +Synths tyEnv env (Expand e) a = ( b ** - ( Synths env e b + ( Synths tyEnv env e b , ( xc ** ( IsFixpoint b xc , a = sub (Base Id :< (fst xc :- b)) (snd xc) )) )) -Synths env (Annot t a) b = +Synths tyEnv env (Annot t a) b = ( Not (IllFormed a) - , Checks env a t - , a = b + , Checks tyEnv env (expand tyEnv a) t + , expand tyEnv a = b ) -Checks env a (Let x e t) = +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 env e b - , Checks (env :< (x :- b)) a t + ( Synths tyEnv env e b + , Checks tyEnv (env :< (x :- b)) a t )) -Checks env a (Abs bound t) = +Checks tyEnv env a (Abs bound t) = ( as ** b ** ( IsFunction bound a as b - , Checks (env ++ as) b t + , Checks tyEnv (env ++ as) b t )) -Checks env a (Inj x t) = +Checks tyEnv env a (Inj x t) = ( as ** ( IsSum a as , ( b ** ( GetAt x as b - , Checks env b t + , Checks tyEnv env b t )) )) -Checks env a (Tup ts) = +Checks tyEnv env a (Tup ts) = ( as ** ( IsProduct a as - , AllCheck env as ts + , AllCheck tyEnv env as ts )) -Checks env a (Case e ts) = +Checks tyEnv env a (Case e ts) = ( b ** - ( Synths env e b + ( Synths tyEnv env e b , ( as ** ( IsSum b as - , AllCheckBinding env as a ts + , AllCheckBinding tyEnv env as a ts )) )) -Checks env a (Contract t) = +Checks tyEnv env a (Contract t) = ( xb ** ( IsFixpoint a xb - , Checks env (sub (Base Id :< (fst xb :- a)) (snd xb)) t + , Checks tyEnv env (sub (Base Id :< (fst xb :- a)) (snd xb)) t )) -Checks env a (Fold e x t) = +Checks tyEnv env a (Fold e x t) = ( b ** - ( Synths env e b + ( Synths tyEnv env e b , ( yc ** ( IsFixpoint b yc - , Checks (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t + , Checks tyEnv (env :< (x :- sub (Base Id :< (fst yc :- a)) (snd yc))) a t )) )) -Checks env a (Embed e) = +Checks tyEnv env a (Embed e) = ( b ** - ( Synths env e b + ( Synths tyEnv env e b , a `Eq` b )) -CheckSpine env fun [] res = fun = res -CheckSpine env fun (t :: ts) res = +CheckSpine tyEnv env fun [] res = fun = res +CheckSpine tyEnv env fun (t :: ts) res = ( a ** b ** ( IsArrow fun a b - , Checks env a t - , CheckSpine env b ts res + , Checks tyEnv env a t + , CheckSpine tyEnv env b ts res )) -AllCheck env as [<] = (as = [<]) -AllCheck env as (ts :< (x :- t)) = +AllCheck tyEnv env as [<] = (as = [<]) +AllCheck tyEnv env as (ts :< (x :- t)) = ( a ** bs ** ( Remove x as a bs - , Checks env a t - , AllCheck env bs ts + , Checks tyEnv env a t + , AllCheck tyEnv env bs ts )) -AllCheckBinding env as a [<] = (as = [<]) -AllCheckBinding env as a (ts :< (x :- (y ** t))) = +AllCheckBinding tyEnv env as a [<] = (as = [<]) +AllCheckBinding tyEnv env as a (ts :< (x :- (y ** t))) = ( b ** bs ** ( Remove x as b bs - , Checks (env :< (y :- b)) a t - , AllCheckBinding env bs a ts + , Checks tyEnv (env :< (y :- b)) a t + , AllCheckBinding tyEnv env bs a ts )) -- Reordering allCheckReorder : as <~> bs -> (ts : Row (CheckTerm tyCtx tmCtx)) -> - AllCheck env as ts -> AllCheck env bs ts + 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)) = @@ -366,7 +383,7 @@ allCheckReorder prf (ts :< (x :- t)) (a ** bs ** (prf1, prf2, prf3)) = allCheckBindingReorder : as <~> bs -> (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> - AllCheckBinding env as a ts -> AllCheckBinding env bs a ts + 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)) = @@ -375,139 +392,153 @@ allCheckBindingReorder prf (ts :< (x :- (y ** t))) (b ** bs ** (prf1, prf2, prf3 -- Uniqueness synthsUnique : - (0 env : All (const $ Ty tyCtx ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) -> - Synths env e a -> Synths env e b -> a = b + (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 env : All (const $ Ty tyCtx ()) tmCtx) -> - (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> - CheckSpine env fun ts a -> CheckSpine env fun ts b -> a = b - -synthsUnique env (Var i) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique env (Lit k) prf1 prf2 = trans prf1 (sym prf2) -synthsUnique env (Suc t) (_, prf1) (_, prf2) = trans prf1 (sym prf2) -synthsUnique env (App e ts) (fun1 ** (prf11, prf12)) (fun2 ** (prf21, prf22)) - with (synthsUnique env e prf11 prf21) - synthsUnique env (App e ts) (fun ** (prf11, prf12)) (fun ** (prf21, prf22)) | Refl = - checkSpineUnique env fun ts prf12 prf22 -synthsUnique env (Prj e k) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique env e prf11 prf21) - synthsUnique env (Prj e k) (a ** (_, (as ** (prf11, prf12)))) (a ** (_, (bs ** (prf21, prf22)))) | Refl + (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 env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl = + synthsUnique tyEnv env (Prj e k) (a ** (_, (as ** (_, prf1)))) (a ** (_, (as ** (_, prf2)))) | Refl | Refl = getAtUnique k as prf1 prf2 -synthsUnique env (Expand e) (a ** (prf11, prf12)) (b ** (prf21, prf22)) - with (synthsUnique env e prf11 prf21) - synthsUnique env (Expand e) (a ** (_, (b ** (prf11, prf12)))) (a ** (_, (c ** (prf21, prf22)))) | Refl +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 env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl = + synthsUnique tyEnv env (Expand e) (a ** (_, (b ** (_, prf1)))) (a ** (_, (b ** (_, prf2)))) | Refl | Refl = trans prf1 (sym prf2) -synthsUnique env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2) +synthsUnique tyEnv env (Annot t c) prf1 prf2 = trans (sym $ snd $ snd prf1) (snd $ snd prf2) -checkSpineUnique env fun [] prf1 prf2 = trans (sym prf1) prf2 -checkSpineUnique env fun (t :: ts) (a ** b ** (prf11, _ , prf12)) (c ** d ** (prf21, _ , prf22)) +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 env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) = - checkSpineUnique env b ts prf1 prf2 + checkSpineUnique tyEnv env fun (t :: ts) (a ** b ** (_, _ , prf1)) (a ** b ** (_, _ , prf2)) | (Refl, Refl) = + checkSpineUnique tyEnv env b ts prf1 prf2 -- Decision synths : - (env : All (const (Ty tyCtx ())) tmCtx) -> - SynthTerm tyCtx tmCtx -> Maybe (Ty tyCtx ()) + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + SynthTerm tyCtx tmCtx -> Maybe (Ty [<] ()) +export checks : - (env : All (const (Ty tyCtx ())) tmCtx) -> - Ty tyCtx () -> CheckTerm tyCtx tmCtx -> Bool + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Ty [<] () -> CheckTerm tyCtx tmCtx -> Bool checkSpine : - (env : All (const (Ty tyCtx ())) tmCtx) -> - (fun : Ty tyCtx ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty tyCtx ()) + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + (fun : Ty [<] ()) -> List (CheckTerm tyCtx tmCtx) -> Maybe (Ty [<] ()) allCheck : - (env : All (const (Ty tyCtx ())) tmCtx) -> - Row (Ty tyCtx ()) -> Row (CheckTerm tyCtx tmCtx) -> Bool + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Row (Ty [<] ()) -> Row (CheckTerm tyCtx tmCtx) -> Bool allCheckBinding : - (env : All (const (Ty tyCtx ())) tmCtx) -> - Row (Ty tyCtx ()) -> Ty tyCtx () -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + Row (Ty [<] ()) -> Ty [<] () -> Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ()))) -> Bool -synths env (Var i) = Just (indexAll i env) -synths env (Lit k) = Just TNat -synths env (Suc t) = do - guard (checks env TNat t) - Just TNat -synths env (App e ts) = do - a <- synths env e - checkSpine env a ts -synths env (Prj e k) = do - a <- synths env e +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 env (Expand e) = do - a <- synths env e +synths tyEnv env (Expand e) = do + a <- synths tyEnv env e (x ** b) <- isFixpoint a Just (sub (Base Id :< (x :- a)) b) -synths env (Annot t a) = do +synths tyEnv env (Annot t a) = do guard (not $ illFormed a) - guard (checks env a t) - Just a - -checks env a (Let x e t) = - case synths env e of - Just b => checks (env :< (x :- b)) a t + 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 env a (Abs bound t) = +checks tyEnv env a (Abs bound t) = case isFunction bound a of - Just (dom, cod) => checks (env ++ dom) cod t + Just (dom, cod) => checks tyEnv (env ++ dom) cod t Nothing => False -checks env a (Inj k t) = +checks tyEnv env a (Inj k t) = case isSum a of Just as => case getAt k as of - Just b => checks env b t + Just b => checks tyEnv env b t Nothing => False Nothing => False -checks env a (Tup ts) = +checks tyEnv env a (Tup ts) = case isProduct a of - Just as => allCheck env as ts + Just as => allCheck tyEnv env as ts Nothing => False -checks env a (Case e ts) = - case synths env e of +checks tyEnv env a (Case e ts) = + case synths tyEnv env e of Just b => case isSum b of - Just as => allCheckBinding env as a ts + Just as => allCheckBinding tyEnv env as a ts Nothing => False Nothing => False -checks env a (Contract t) = +checks tyEnv env a (Contract t) = case isFixpoint a of - Just (x ** b) => checks env (sub (Base Id :< (x :- a)) b) t + Just (x ** b) => checks tyEnv env (sub (Base Id :< (x :- a)) b) t Nothing => False -checks env a (Fold e x t) = - case synths env e of +checks tyEnv env a (Fold e x t) = + case synths tyEnv env e of Just b => case isFixpoint b of - Just (y ** c) => checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t + Just (y ** c) => checks tyEnv (env :< (x :- sub (Base Id :< (y :- a)) c)) a t Nothing => False Nothing => False -checks env a (Embed e) = - case synths env e of +checks tyEnv env a (Embed e) = + case synths tyEnv env e of Just b => a == b Nothing => False -checkSpine env a [] = Just a -checkSpine env a (t :: ts) = do +checkSpine tyEnv env a [] = do + pure a +checkSpine tyEnv env a (t :: ts) = do (dom, cod) <- isArrow a - guard (checks env dom t) - checkSpine env cod ts + guard (checks tyEnv env dom t) + checkSpine tyEnv env cod ts -allCheck env as [<] = null as -allCheck env as (ts :< (x :- t)) = +allCheck tyEnv env as [<] = null as +allCheck tyEnv env as (ts :< (x :- t)) = case remove' x as of - Just (a, bs) => checks env a t && allCheck env bs ts + Just (a, bs) => checks tyEnv env a t && allCheck tyEnv env bs ts Nothing => False -allCheckBinding env as a [<] = null as -allCheckBinding env as a (ts :< (x :- (y ** t))) = +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 (env :< (y :- b)) a t && allCheckBinding env bs a ts + Just (b, bs) => checks tyEnv (env :< (y :- b)) a t && allCheckBinding tyEnv env bs a ts Nothing => False -- Proof @@ -516,84 +547,92 @@ allCheckBinding env as a (ts :< (x :- (y ** t))) = partial 0 reflectSynths : - (env : All (const $ Ty tyCtx ()) tmCtx) -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> (e : SynthTerm tyCtx tmCtx) -> - Synths env e `OnlyWhen` synths env e + Synths tyEnv env e `OnlyWhen` synths tyEnv env e partial 0 reflectChecks : - (env : All (const $ Ty tyCtx ()) tmCtx) -> - (a : Ty tyCtx ()) -> (t : CheckTerm tyCtx tmCtx) -> - Checks env a t `Reflects` checks env a t + (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 : - (env : All (const $ Ty tyCtx ()) tmCtx) -> - (fun : Ty tyCtx ()) -> (ts : List (CheckTerm tyCtx tmCtx)) -> - CheckSpine env fun ts `OnlyWhen` checkSpine env fun ts + (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 : - (env : All (const $ Ty tyCtx ()) tmCtx) -> - (as : Row (Ty tyCtx ())) -> (ts : Row (CheckTerm tyCtx tmCtx)) -> - AllCheck env as ts `Reflects` allCheck env as ts + (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 : - (env : All (const $ Ty tyCtx ()) tmCtx) -> - (as : Row (Ty tyCtx ())) -> (a : Ty tyCtx ()) -> + (tyEnv : DEnv Ty tyCtx) -> + (env : All (const $ Ty [<] ()) tmCtx) -> + (as : Row (Ty [<] ())) -> (a : Ty [<] ()) -> (ts : Row (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) -> - AllCheckBinding env as a ts `Reflects` allCheckBinding env as a ts - -reflectSynths env (Var i) = RJust Refl -reflectSynths env (Lit k) = RJust Refl -reflectSynths env (Suc t) with (reflectChecks env TNat t) | (checks env TNat t) - _ | RTrue tNat | _ = RJust (tNat, Refl) - _ | RFalse tNotNat | _ = RNothing (\_, (tNat, _) => tNotNat tNat) -reflectSynths env (App e ts) with (reflectSynths env e) | (synths env e) - _ | RJust eTy | Just a with (reflectCheckSpine env a ts) | (checkSpine env a ts) + 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 env e {a, b} eTy eTy' in tsSpine in + 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 env (Prj e x) with (reflectSynths env e) | (synths env e) +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 env e {a, b = a'} eTy eTy' in prf' in + 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 env e {a, b = a'} eTy eTy' in prf in + 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 env (Expand e) with (reflectSynths env e) | (synths env e) +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 env e {a, b = a'} eTy eTy' in prf in + 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 env (Annot t a) with (reflectIllFormed a) | (illFormed a) - _ | RFalse wf | _ with (reflectChecks env a t) | (checks env a t) +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 env a (Let x e t) with (reflectSynths env e) | (synths env e) - _ | RJust eTy | Just b with (reflectChecks (env :< (x :- b)) a t) | (checks (env :< (x :- b)) a t) +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 env e {a = b, b = b'} eTy eTy' in tTy in + 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 env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction bound a) - _ | RJust prf | Just (as, b) with (reflectChecks (env ++ as) b t) | (checks (env ++ as) b t) +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)) => @@ -606,9 +645,9 @@ reflectChecks env a (Abs bound t) with (reflectIsFunction bound a) | (isFunction in tBad tTy) _ | RNothing nprf | _ = RFalse (\(as ** b ** (prf, _)) => nprf (as, b) prf) -reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a) +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 env b t) | (checks env b t) + _ | 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)))) => @@ -621,74 +660,74 @@ reflectChecks env a (Inj k t) with (reflectIsSum a) | (isSum a) 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 env a (Tup ts) with (reflectIsProduct a) | (isProduct a) - _ | RJust prf | Just as with (reflectAllCheck env as ts) | (allCheck env as ts) +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 env a (Case e ts) with (reflectSynths env e) | (synths env e) +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 env as a ts) | (allCheckBinding env as a ts) + _ | 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 env e {a = b, b = b'} eTy eTy' in prf' in + 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 env e {a = b, b = b'} eTy eTy' in prf in + 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 env a (Contract t) with (reflectIsFixpoint a) | (isFixpoint a) - _ | RJust prf | Just (x ** b) with (reflectChecks env (sub (Base Id :< (x :- a)) b) t) | (checks env (sub (Base Id :< (x :- a)) b) t) +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 env (sub (Base Id :< (xb.fst :- a)) xb.snd) t} + 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 env a (Fold e x t) with (reflectSynths env e) | (synths env e) +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 (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) | (checks (env :< (x :- sub (Base Id :< (y :- a)) c)) a t) + _ | 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 env e {a = b, b = b'} eTy eTy' in prf' + 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 (env :< (x :- sub (Base Id :< (yc.fst :- a)) yc.snd)) a t} + 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 env e {a = b, b = b'} eTy eTy' in prf in + 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 env a (Embed e) with (reflectSynths env e) | (synths env e) +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 env e {a = b, b = b'} eTy eTy' in eq in + 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 env a [] = RJust Refl -reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a) - _ | RJust prf | Just (b, c) with (reflectChecks env b t) | (checks env b t) - _ | RTrue tTy | _ with (reflectCheckSpine env c ts) | (checkSpine env c ts) +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)) => @@ -702,10 +741,10 @@ reflectCheckSpine env a (t :: ts) with (reflectIsArrow a) | (isArrow a) tBad tTy) _ | RNothing nprf | _ = RNothing (\d, (b ** c ** (prf, _)) => nprf (b, c) prf) -reflectAllCheck env [<] [<] = RTrue Refl -reflectAllCheck env (_ :< _) [<] = RFalse (\case Refl impossible) -reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x as) - _ | RJust prf | Just (a, bs) with (reflectAnd (reflectChecks env a t) (reflectAllCheck env bs ts)) | (checks env a t && allCheck env bs ts) +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)) => @@ -714,10 +753,10 @@ reflectAllCheck env as (ts :< (x :- t)) with (reflectRemove x as) | (remove' x a bimap (\x => rewrite eq in x) (allCheckReorder (sym reorder) ts) checks) _ | RNothing nprf | _ = RFalse (\(a ** bs ** (prf, _)) => nprf (a, bs) prf) -reflectAllCheckBinding env [<] a [<] = RTrue Refl -reflectAllCheckBinding env (_ :< _) a [<] = RFalse (\case Refl impossible) -reflectAllCheckBinding env as a (ts :< (x :- (y ** t))) with (reflectRemove x as) | (remove' x as) - _ | RJust prf | Just (b, bs) with (reflectAnd (reflectChecks (env :< (y :- b)) a t) (reflectAllCheckBinding env bs a ts)) | (checks (env :< (y :- b)) a t && allCheckBinding env bs a ts) +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)) => diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index 7a67441..6913bf8 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -1,5 +1,7 @@ module Inky.Term.Parser +import public Data.Fun + import Data.List1 import Data.String import Inky.Context @@ -21,6 +23,7 @@ data InkyKind | In | Case | Of + | FoldCase | Fold | By | Nat @@ -36,8 +39,10 @@ data InkyKind | DoubleArrow | Bang | Tilde + | Dot | Backslash | Colon + | Semicolon | Equal | Comma | Ignore @@ -52,6 +57,7 @@ export In == In = True Case == Case = True Of == Of = True + FoldCase == FoldCase = True Fold == Fold = True By == By = True Nat == Nat = True @@ -67,8 +73,10 @@ export DoubleArrow == DoubleArrow = True Bang == Bang = True Tilde == Tilde = True + Dot == Dot = True Backslash == Backslash = True Colon == Colon = True + Semicolon == Semicolon = True Equal == Equal = True Comma == Comma = True Ignore == Ignore = True @@ -84,6 +92,7 @@ Interpolation InkyKind where interpolate In = "'in'" interpolate Case = "'case'" interpolate Of = "'of'" + interpolate FoldCase = "'foldcase'" interpolate Fold = "'fold'" interpolate By = "'by'" interpolate Nat = "'Nat'" @@ -99,8 +108,10 @@ Interpolation InkyKind where interpolate DoubleArrow = "'=>'" interpolate Bang = "'!'" interpolate Tilde = "'~'" + interpolate Dot = "'.'" interpolate Backslash = "'\\'" interpolate Colon = "':'" + interpolate Semicolon = "';'" interpolate Equal = "'='" interpolate Comma = "','" interpolate Ignore = "" @@ -119,6 +130,7 @@ TokenKind InkyKind where tokValue In = const () tokValue Case = const () tokValue Of = const () + tokValue FoldCase = const () tokValue Fold = const () tokValue By = const () tokValue Nat = const () @@ -134,8 +146,10 @@ TokenKind InkyKind where tokValue DoubleArrow = const () tokValue Bang = const () tokValue Tilde = const () + tokValue Dot = const () tokValue Backslash = const () tokValue Colon = const () + tokValue Semicolon = const () tokValue Equal = const () tokValue Comma = const () tokValue Ignore = const () @@ -147,6 +161,7 @@ keywords = , ("in", In) , ("case", Case) , ("of", Of) + , ("foldcase", FoldCase) , ("fold", Fold) , ("by", By) , ("Nat", Nat) @@ -169,7 +184,10 @@ typeIdentifier = upper <+> many (alphaNum <|> exact "_") export tokenMap : TokenMap InkyToken tokenMap = - toTokenMap [(spaces, Ignore)] ++ + toTokenMap + [ (spaces, Ignore) + , (lineComment $ exact "--", Ignore) + ] ++ [(termIdentifier, \s => case lookup s keywords of Just k => Tok k s @@ -192,14 +210,26 @@ tokenMap = , (exact "=>", DoubleArrow) , (exact "!", Bang) , (exact "~", Tilde) + , (exact ".", Dot) , (exact "\\", Backslash) , (exact ":", Colon) + , (exact ";", Semicolon) , (exact "=", Equal) , (exact ",", Comma) ] -- 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 = @@ -209,33 +239,74 @@ InkyParser nil locked free a = a public export -record TypeFun where - constructor MkTypeFun - try : (ctx : Context ()) -> Either String (Ty ctx ()) +record ParseFun (0 tys: Vect n Type) (0 p : Fun (map Context tys) Type) where + constructor MkParseFun + try : DFun (map Context tys) (chain {ts = map Context tys} (Either String) p) + +mkVar : ({ctx : Context ()} -> Var ctx () -> p ctx) -> WithBounds String -> ParseFun [()] p +mkVar f x = + MkParseFun + (\ctx => case 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 +mkVar2 f x = + MkParseFun + (\tyCtx, tmCtx => case 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 + +public export +CheckFun : Type +CheckFun = ParseFun [(), ()] CheckTerm public export TypeParser : Context () -> Context () -> Type TypeParser locked free = InkyParser False (map (const TypeFun) locked) (map (const TypeFun) free) TypeFun -Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ Assoc TypeFun) -Row = - sepBy (match Comma) - (mkAssoc <$> Seq [match TypeIdent, match Colon, Var (%% "openType")]) +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, (), TypeFun] -> Assoc TypeFun + mkAssoc : HList [String, (), a] -> Assoc a mkAssoc [x, _, v] = x :- v -tryRow : WithBounds (List $ Assoc TypeFun) -> (ctx : Context ()) -> Either String (Row (Ty ctx ())) +tryRow : + List (WithBounds $ Assoc (ParseFun [()] p)) -> + (ctx : Context ()) -> Either String (Row $ p ctx) tryRow xs ctx = foldlM (\row, xf => do - a <- xf.value.try ctx - let Just row' = extend row (xf.name :- a) - | Nothing => Left "\{xs.bounds}: duplicate name \"\{xf.name}\"" + a <- xf.val.value.try ctx + let Just row' = extend row (xf.val.name :- a) + | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\"" + pure row') + [<] + xs + +tryRow2 : + List (WithBounds $ Assoc (ParseFun [(), ()] p)) -> + (tyCtx, tmCtx : Context ()) -> Either String (Row $ p tyCtx tmCtx) +tryRow2 xs tyCtx tmCtx = + foldlM + (\row, xf => do + a <- xf.val.value.try tyCtx tmCtx + let Just row' = extend row (xf.val.name :- a) + | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\"" pure row') [<] - xs.val + xs OpenOrFixpointType : TypeParser [<] [<"openType" :- ()] OpenOrFixpointType = @@ -246,31 +317,26 @@ OpenOrFixpointType = ] where mkFix : HList [(), String, (), TypeFun] -> TypeFun - mkFix [_, x, _, a] = MkTypeFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ())))) + mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< (x :- ())))) AtomType : TypeParser [<"openType" :- ()] [<] AtomType = OneOf - [ - mkVar <$> WithBounds (match TypeIdent) - , MkTypeFun (\_ => pure TNat) <$ match Nat - , mkProd <$> enclose (match AngleOpen) (match AngleClose) (WithBounds Row) - , mkSum <$> enclose (match BracketOpen) (match BracketClose) (WithBounds Row) + [ mkVar TVar <$> WithBounds (match TypeIdent) + , MkParseFun (\_ => pure TNat) <$ match Nat + , mkProd <$> enclose (match AngleOpen) (match AngleClose) Row + , mkSum <$> enclose (match BracketOpen) (match BracketClose) Row , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType ] where - mkVar : WithBounds String -> TypeFun - mkVar x = - MkTypeFun - (\ctx => case lookup x.val ctx of - Just (() ** i) => pure (TVar i) - Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"") + Row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun) + Row = RowOf [<"openType" :- TypeFun] $ Var (%% "openType") - mkProd : WithBounds (List $ Assoc TypeFun) -> TypeFun - mkProd xs = MkTypeFun (\ctx => TProd <$> tryRow xs ctx) + mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun + mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx) - mkSum : WithBounds (List $ Assoc TypeFun) -> TypeFun - mkSum xs = MkTypeFun (\ctx => TSum <$> tryRow xs ctx) + mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun + mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx) export OpenType : TypeParser [<] [<] @@ -278,9 +344,250 @@ OpenType = Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AtomType where mkArrow : List1 TypeFun -> TypeFun - mkArrow = foldr1 (\x, y => MkTypeFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |])) + mkArrow = foldr1 (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |])) %hint export OpenTypeWf : So (wellTyped EqI [<] [<] [<] [<] OpenType) 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 = + OneOf + [ embed <$> mkVar2 Var <$> WithBounds (match TermIdent) + , embed <$> mkLit <$> match Lit + , embed <$> MkParseFun (\_, _ => pure Suc) <$ match Suc + , mkTup <$> (enclose (match AngleOpen) (match AngleClose) $ + RowOf [<"openCheck" :- CheckFun] (Var (%% "openCheck"))) + , enclose (match ParenOpen) (match ParenClose) (Var (%% "openCheck")) + ] + where + mkLit : Nat -> SynthFun + mkLit k = MkParseFun (\_, _ => pure (Lit k)) + + mkTup : List (WithBounds $ Assoc CheckFun) -> CheckFun + 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 + ] + where + mkExpand : SynthFun -> SynthFun + mkExpand x = MkParseFun (\tyCtx, tmCtx => [| Expand (x.try tyCtx tmCtx) |]) + + mkContract : CheckFun -> CheckFun + mkContract x = MkParseFun (\tyCtx, tmCtx => [| Contract (x.try tyCtx tmCtx) |]) + +SuffixCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +SuffixCheck = mkSuffix <$> Seq [ WithBounds PrefixCheck , star (match Dot **> match TypeIdent) ] + where + mkSuffix : HList [WithBounds CheckFun, List String] -> CheckFun + mkSuffix [t, []] = t.val + mkSuffix [t, prjs] = + embed $ + MkParseFun (\tyCtx, tmCtx => pure $ foldl Prj !((unembed t).try tyCtx tmCtx) prjs) + +AppCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +AppCheck = + OneOf + [ mkInj <$> Seq + [ match TypeIdent + , weaken (S Z) SuffixCheck + ] + , mkApp <$> Seq [ WithBounds SuffixCheck , star (weaken (S Z) SuffixCheck) ] + ] + where + mkInj : HList [String, CheckFun] -> CheckFun + mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag <$> t.try tyCtx tmCtx) + + mkApp : HList [WithBounds CheckFun, List CheckFun] -> CheckFun + mkApp [t, []] = t.val + mkApp [fun, (arg :: args)] = + MkParseFun (\tyCtx, tmCtx => + pure $ Embed $ + App + !((unembed 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 = + mkAnnot <$> Seq + [ AppCheck + , option (match Colon **> rename Id (Drop Id) OpenType) + ] + where + mkAnnot : HList [CheckFun, Maybe TypeFun] -> CheckFun + mkAnnot [t, Nothing] = t + mkAnnot [t, Just a] = embed $ MkParseFun (\tyCtx, tmCtx => [| Annot (t.try tyCtx tmCtx) (a.try tyCtx) |]) + +-- Open Terms + +LetCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +LetCheck = + match Let **> + OneOf + [ mkLet <$> Seq + [ match TermIdent + , OneOf + [ mkBound <$> Seq + [ star (enclose (match ParenOpen) (match ParenClose) $ + Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ]) + , match Colon + , rename Id (Drop Id) OpenType + , match Equal + , Var (%% "openCheck")] + , match Equal **> unembed <$> WithBounds (Var (%% "openCheck")) + ] + , match In + , Var (%% "openCheck") + ] + , mkLetType <$> Seq + [ match TypeIdent + , match Equal + , rename Id (Drop Id) OpenType + , match In + , Var (%% "openCheck") + ] + ] + 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 :- ())))) + + mkLetType : HList [String, (), TypeFun, (), CheckFun] -> CheckFun + mkLetType [x, _, a, _, t] = + MkParseFun (\tyCtx, tmCtx => pure $ LetTy x !(a.try tyCtx) !(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 [[], _, 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 + MkParseFun (\tyCtx, tmCtx => + pure $ + Annot (Abs dom !(t.try tyCtx (tmCtx ++ dom))) !((mkArrow (map (\[x, _, a] => a) args) cod).try tyCtx)) + +AbsCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +AbsCheck = + mkAbs <$> Seq + [ match Backslash + , sepBy1 (match Comma) (match TermIdent) + , match DoubleArrow + , Var (%% "openCheck") + ] + where + mkAbs : HList [(), List1 String, (), CheckFun] -> CheckFun + mkAbs [_, args, _, body] = + let args = foldl (\args, x => args :< (x :- ())) [<] args in + MkParseFun (\tyCtx, tmCtx => Abs args <$> body.try tyCtx (tmCtx ++ args)) + +CaseCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +CaseCheck = + (\[f, x] => f x) <$> + Seq + [ OneOf + [ mkCase <$> Seq + [ match Case + , unembed <$> WithBounds (Var $ %% "openCheck") + , match Of + ] + , mkFoldCase <$> Seq + [ match FoldCase + , unembed <$> WithBounds (Var $ %% "openCheck") + , match By + ] + ] + , enclose (match BraceOpen) (match BraceClose) ( + sepBy (match Semicolon) $ + WithBounds $ + Seq + [ match TypeIdent + , match TermIdent + , match DoubleArrow + , Var (%% "openCheck") + ]) + ] + where + Cases : Type + Cases = List (WithBounds $ HList [String, String, (), CheckFun]) + + mkBranch : + HList [String, String, (), CheckFun] -> + Assoc (ParseFun [(), ()] $ \tyCtx, tmCtx => (x ** CheckTerm tyCtx (tmCtx :< (x :- ())))) + mkBranch [tag, bound, _, branch] = + tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< (bound :- ()))))) + + mkCase : HList [_, SynthFun, _] -> Cases -> CheckFun + 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 [_, 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" :- ()))))) + +FoldCheck : InkyParser False [<"openCheck" :- CheckFun] [<] CheckFun +FoldCheck = + mkFold <$> Seq + [ match Fold + , unembed <$> WithBounds (Var (%% "openCheck")) + , match By + , enclose (match ParenOpen) (match ParenClose) $ + Seq + [ match Backslash + , match TermIdent + , match DoubleArrow + , Var (%% "openCheck") + ] + ] + where + mkFold : HList [(), SynthFun, (), HList [(), String, (), CheckFun]] -> CheckFun + mkFold [_, target, _, [_, arg, _, body]] = + 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 + ] + +%hint +export +OpenCheckWf : So (wellTyped EqI [<] [<] [<] [<] OpenCheck) +OpenCheckWf = ?d -- Oh diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index 7c5ee4d..3bed88b 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -23,6 +23,7 @@ export prettySynth : {tyCtx, tmCtx : Context ()} -> SynthTerm tyCtx tmCtx -> Prec -> Doc ann +export prettyCheck : {tyCtx, tmCtx : Context ()} -> CheckTerm tyCtx tmCtx -> Prec -> Doc ann @@ -38,15 +39,13 @@ prettyCheckCtxBinding : prettySynth (Var i) d = pretty (unVal $ nameOf i) prettySynth (Lit k) d = pretty k -prettySynth (Suc t) d = - parenthesise (d >= appPrec) $ group $ align $ hang 2 $ - "suc" <+> line <+> prettyCheck t appPrec +prettySynth 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 <+> "." <+> pretty x + prettySynth e prjPrec <+> line' <+> "." <+> pretty x prettySynth (Expand e) d = "!" <+> (parenthesise (d > expandPrec) $ group $ align $ hang 2 $ @@ -55,17 +54,25 @@ prettySynth (Annot t a) d = parenthesise (d > annotPrec) $ group $ align $ hang 2 $ prettyCheck t annotPrec <++> ":" <+> line <+> prettyType a annotPrec +prettyCheck (LetTy x a t) d = + parenthesise (d > letPrec) $ group $ align $ + "let" <++> + (group $ align $ hang 2 $ + pretty x <++> "=" <+> line <+> prettyType a letPrec + ) <+> line <+> + "in" <+> line <+> + prettyCheck t letPrec prettyCheck (Let x e t) d = - parenthesise (d > letPrec) $ group $ align $ hang 2 $ + parenthesise (d > letPrec) $ group $ align $ "let" <++> (group $ align $ hang 2 $ pretty x <++> "=" <+> line <+> prettySynth e letPrec - ) <++> + ) <+> line <+> "in" <+> line <+> prettyCheck t letPrec prettyCheck (Abs bound t) d = parenthesise (d > absPrec) $ group $ align $ hang 2 $ - "\\" <+> concatWith (surround ",") (bindings bound <>> []) <++> "=>" <+> line <+> + "\\" <+> concatWith (surround $ "," <+> line) (bindings bound <>> []) <++> "=>" <+> line <+> prettyCheck t absPrec where bindings : Context () -> SnocList (Doc ann) @@ -73,16 +80,15 @@ prettyCheck (Abs bound t) d = bindings (bound :< (x :- ())) = bindings bound :< pretty x prettyCheck (Inj k t) d = parenthesise (d > injPrec) $ group $ align $ hang 2 $ - "<" <+> line' <+> pretty k <+> line' <+> ">" <+> prettyCheck t injPrec + pretty k <+> line <+> prettyCheck t injPrec prettyCheck (Tup ts) d = - parens $ group $ align $ hang 2 $ + enclose "<" ">" $ group $ align $ hang 2 $ concatWith (surround $ "," <+> line) (prettyCheckCtx ts tupPrec) prettyCheck (Case e ts) d = parenthesise (d > casePrec) $ group $ align $ hang 2 $ "case" <++> prettySynth e casePrec <++> "of" <+> line <+> - (braces $ align $ hang 2 $ - concatWith (surround hardline) $ - map parens $ + (braces $ group $ align $ hang 2 $ + concatWith (surround $ ";" <+> line) $ prettyCheckCtxBinding ts casePrec) prettyCheck (Contract t) d = "~" <+> @@ -106,5 +112,5 @@ prettyCheckCtx (ts :< (x :- t)) d = prettyCheckCtxBinding [<] d = [] prettyCheckCtxBinding (ts :< (x :- (y ** t))) d = (group $ align $ hang 2 $ - "\\" <+> pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) :: + pretty x <++> pretty y <++> "=>" <+> line <+> prettyCheck t d) :: prettyCheckCtxBinding ts d diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr index 87640e2..1627307 100644 --- a/src/Inky/Thinning.idr +++ b/src/Inky/Thinning.idr @@ -2,9 +2,10 @@ module Inky.Thinning import public Inky.Context +import Control.Function +import Control.WellFounded import Data.DPair import Data.Nat -import Control.Function -------------------------------------------------------------------------------- -- Thinnings ------------------------------------------------------------------- @@ -252,3 +253,58 @@ lookupLift : (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 9cfc1f7..26f3c0f 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -406,3 +406,16 @@ subAll env ((:<) as (x :- a) {fresh}) = subAllFresh env x [<] = id subAllFresh env x (as :< (y :- a)) = andSo . mapSnd (subAllFresh env x as) . soAnd + +-- Expansion ------------------------------------------------------------------- + +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) + +export +expand : DEnv Ty ctx -> Ty ctx v -> Ty [<] v +expand = sub . expandEnv diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr index 1f2d35b..83253b4 100644 --- a/src/Inky/Type/Pretty.idr +++ b/src/Inky/Type/Pretty.idr @@ -19,7 +19,7 @@ prettyType TNat d = pretty "Nat" prettyType (TArrow a b) d = parenthesise (d > arrowPrec) $ group $ align $ hang 2 $ let parts = stripArrow b in - concatWith (surround $ "->" <+> line) (prettyType a arrowPrec :: parts) + concatWith (surround $ neutral <++> "->" <+> line) (prettyType a arrowPrec :: parts) where stripArrow : Ty ctx () -> List (Doc ann) stripArrow (TArrow a b) = prettyType a arrowPrec :: stripArrow b -- cgit v1.2.3