diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Inky.idr | 67 | ||||
| -rw-r--r-- | src/Inky/Context.idr | 52 | ||||
| -rw-r--r-- | src/Inky/Parser.idr | 698 | ||||
| -rw-r--r-- | src/Inky/Term/Parser.idr | 286 | ||||
| -rw-r--r-- | src/Inky/Thinning.idr | 97 | ||||
| -rw-r--r-- | src/Inky/Type.idr | 2 |
6 files changed, 960 insertions, 242 deletions
diff --git a/src/Inky.idr b/src/Inky.idr new file mode 100644 index 0000000..5c7a821 --- /dev/null +++ b/src/Inky.idr @@ -0,0 +1,67 @@ +module Inky + +import Control.App +import Control.App.Console +import Control.App.FileIO +import Inky.Context +import Inky.Parser +import Inky.Term.Parser +import Inky.Type +import Inky.Type.Pretty +import System.File.ReadWrite +import System.File.Virtual +import Text.Lexer +import Text.PrettyPrint.Prettyprinter +import Text.PrettyPrint.Prettyprinter.Render.Terminal + +%default partial + +lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken)) +lexInkyString file = do + let (tokens, _, _, "") = lex tokenMap file + | (_, 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 toks = do + let Ok res [] _ = parse @{EqI} OpenType toks + | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input" + | Err msg => throw msg + let Right a = res.try [<] + | Left msg => throw msg + pure a + +checkType : HasErr String es => Ty [<] () -> App es () +checkType a = do + let False = illFormed a + | True => throw "type ill-formed" + 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 + +main : IO () +main = + run $ + handle {err = IOError} + (handle {err = String} ppType + (const $ pure ()) + printErrLn) + (const $ pure ()) + (printErrLn . show) + where + printErrLn : PrimIO es => String -> App es () + printErrLn msg = do + primIO $ () <$ fPutStrLn stderr msg + pure () diff --git a/src/Inky/Context.idr b/src/Inky/Context.idr index b0393f3..2e9af8f 100644 --- a/src/Inky/Context.idr +++ b/src/Inky/Context.idr @@ -7,15 +7,13 @@ import Data.Bool.Decidable import Data.Maybe.Decidable import Data.DPair import Data.Nat +import Decidable.Equality -- Contexts -------------------------------------------------------------------- export infix 2 :- -export -prefix 2 %% - public export record Assoc (a : Type) where constructor (:-) @@ -72,7 +70,7 @@ public export ctx ++ [<] = ctx ctx ++ ctx' :< x = (ctx ++ ctx') :< x -export +public export lengthAppend : Length ctx1 -> Length ctx2 -> Length (ctx1 ++ ctx2) lengthAppend len1 Z = len1 lengthAppend len1 (S len2) = S (lengthAppend len1 len2) @@ -83,9 +81,11 @@ length (ctx :< x) = S (length ctx) -- Variables ------------------------------------------------------------------- +export prefix 2 %% + public export -data VarPos : Context a -> (0 x : String) -> a -> Type where - [search x] +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 @@ -171,28 +171,31 @@ reflectEq ((%%) x {pos = pos1}) ((%%) y {pos = pos2}) -- 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 -export +public export wknL : {auto len : Length ctx2} -> Var ctx1 v -> Var (ctx1 ++ ctx2) v wknL i = toVar $ wknLPos i.pos len -export +public export wknR : Var ctx2 v -> Var (ctx1 ++ ctx2) v wknR i = toVar $ wknRPos i.pos -export +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 @@ -213,6 +216,19 @@ 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 @@ -226,11 +242,12 @@ namespace Quantifier %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 - export + public export indexAll : Var ctx v -> All p ctx -> p v indexAll i env = indexAllPos i.pos env @@ -239,11 +256,16 @@ namespace Quantifier mapProperty f [<] = [<] mapProperty f (env :< (x :- px)) = mapProperty f env :< (x :- f px) - export + 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 @@ -274,7 +296,6 @@ namespace Row mapFresh f [<] = id mapFresh f (row :< (y :- _)) = andSo . mapSnd (mapFresh f row) . soAnd - public export Functor Row where map = Row.map @@ -295,6 +316,13 @@ namespace Row 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 diff --git a/src/Inky/Parser.idr b/src/Inky/Parser.idr index 1ad48d8..c44e7bd 100644 --- a/src/Inky/Parser.idr +++ b/src/Inky/Parser.idr @@ -1,21 +1,27 @@ 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.List.Elem import Data.List1 -import Data.Nat import Data.So +import Data.String.Extra import Inky.Context +import Inky.Thinning import Text.Lexer +export +Interpolation Bounds where + interpolate bounds = "\{show (1 + bounds.startLine)}:\{show bounds.startCol}--\{show (1 + bounds.endLine)}:\{show bounds.endCol}" -- Parser Expressions ---------------------------------------------------------- -export -infixl 3 <**>, **>, <** -infixr 2 <||> +export infixl 3 <**>, **>, <** +export infixr 2 <||> public export linUnless : Bool -> Context a -> Context a @@ -23,124 +29,272 @@ linUnless False ctx = [<] linUnless True ctx = ctx public export -data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type where - Var : (f : a -> b) -> Var free (nil, a) -> Parser i nil locked free b - Fail : (msg : String) -> Parser i False locked free a - Empty : (x : a) -> Parser i True locked free a - Lit : (text : i) -> (x : String -> a) -> Parser i False locked free a - (<**>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free (a -> b) -> - Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) a -> - Parser i (nil1 && nil2) locked free b - (<|>) : - {nil1, nil2 : Bool} -> - Parser i nil1 locked free a -> Parser i nil2 locked free a -> - So (not (nil1 && nil2)) => - Parser i (nil1 || nil2) locked free a +linUnlessLin : (0 a : Type) -> (b : Bool) -> linUnless {a} b [<] = [<] +linUnlessLin a False = Refl +linUnlessLin a True = Refl + +public export +data Parser : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> Type -> Type + +public export +data ParserChain : (i : Type) -> (nil : Bool) -> (locked, free : Context (Bool, Type)) -> List Type -> Type + +data Parser where + Var : Var free (nil, a) -> Parser i nil locked free a + Lit : (text : i) -> Parser i False locked free String + Seq : + ParserChain i nil locked free as -> + Parser i nil locked free (HList as) + OneOf : + {nils : List Bool} -> + All (\nil => Parser i nil locked free a) nils -> + {auto 0 prf : length (filter Basics.id nils) `LTE` 1} -> + Parser i (any Basics.id nils) locked free a Fix : (0 x : String) -> - (f : a -> b) -> Parser i nil (locked :< (x :- (nil, a))) free a -> - Parser i nil locked free b + Parser i nil locked free a + Map : (a -> b) -> Parser i nil locked free a -> Parser i nil locked free b + WithBounds : Parser i nil locked free a -> Parser i nil locked free (WithBounds a) + +data ParserChain where + Nil : ParserChain i True locked free [] + (::) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) as -> + ParserChain i (nil1 && nil2) locked free (a :: as) %name Parser p, q +%name ParserChain ps, qs + +-- Weakening ------------------------------------------------------------------- public export -Functor (Parser i nil locked free) where - map f (Var g x) = Var (f . g) x - map f (Fail msg) = Fail msg - map f (Empty x) = Empty (f x) - map f (Lit text g) = Lit text (f . g) - map f ((<**>) {nil1 = True} p q) = map (f .) p <**> q - map f ((<**>) {nil1 = False} p q) = map (f .) p <**> q - map f (p <|> q) = map f p <|> map f q - map f (Fix x g p) = Fix x (f . g) p +rename : + locked1 `Thins` locked2 -> + free1 `Thins` free2 -> + {auto len : Length 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} -> + 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 + +rename f g (Var i) = Var (index g i) +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) +rename f g (Fix x p) = Fix x (rename (Keep f) g p) +rename f g (Map h p) = Map h (rename f g p) +rename f g (WithBounds p) = WithBounds (rename f g p) + +renameChain f g [] = [] +renameChain f g ((::) {nil1 = False} p ps) = rename f g p :: renameChain Id (append g f) ps +renameChain f g ((::) {nil1 = True} p ps) = rename f g p :: renameChain f g ps + +renameAll f g [] = [] +renameAll f g (p :: ps) = rename f g p :: renameAll f g ps public export -Applicative (Parser i True locked free) where - pure = Empty - (<*>) = (<**>) +weaken : + (len1 : Length free2) -> + {auto len2 : Length 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} -> + 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 + +weaken len1 (Var x) = Var (wknL x) +weaken len1 (Lit text) = Lit text +weaken len1 (Seq ps) = Seq (weakenChain len1 ps) +weaken len1 (OneOf ps) = OneOf (weakenAll len1 ps) +weaken len1 (Fix x p) = Fix x (weaken len1 p) +weaken len1 (Map f p) = Map f (weaken len1 p) +weaken len1 (WithBounds p) = WithBounds (weaken len1 p) + +weakenChain len1 [] = [] +weakenChain len1 ((::) {nil1 = False} p ps) = weaken len1 p :: renameChain Id (assoc len2) ps +weakenChain len1 ((::) {nil1 = True} p ps) = weaken len1 p :: weakenChain len1 ps + +weakenAll len1 [] = [] +weakenAll len1 (p :: ps) = weaken len1 p :: weakenAll len1 ps -- Typing ---------------------------------------------------------------------- -export +-- Lists are sufficient, as we assume each symbol appears once. +-- TODO: switch to some efficient tree? + +public export peek : (env : All (const (List i)) free) -> Parser i nil locked free a -> List i -peek env (Var f x) = indexAll x env -peek env (Fail msg) = [] -peek env (Empty x) = [] -peek env (Lit text x) = [text] -peek env ((<**>) {nil1 = False} p q) = peek env p -peek env ((<**>) {nil1 = True} p q) = peek env p ++ peek env q -peek env (p <|> q) = peek env p ++ peek env q -peek env (Fix x f p) = peek env p +public export +peekChain : + (env : All (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 -export +peek env (Var x) = indexAll x env +peek env (Lit text) = [text] +peek env (Seq ps) = peekChain env ps +peek env (OneOf ps) = concat (forget $ peekAll env ps) +peek env (Fix x p) = peek env p +peek env (Map f p) = peek env p +peek env (WithBounds p) = peek env p + +peekChain env [] = [] +peekChain env ((::) {nil1 = False} p ps) = peek env p +peekChain env ((::) {nil1 = True} p ps) = peek env p ++ peekChain env ps + +peekAll env [] = [] +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) -> Parser i nil locked free a -> List i -follow penv1 penv2 fenv1 fenv2 (Var f x) = indexAll x fenv2 -follow penv1 penv2 fenv1 fenv2 (Fail msg) = empty -follow penv1 penv2 fenv1 fenv2 (Empty x) = empty -follow penv1 penv2 fenv1 fenv2 (Lit text x) = empty -follow penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = False} p q) = - follow [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) q -follow penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = True} p q) = - peek penv2 q ++ - follow penv1 penv2 fenv1 fenv2 p ++ - follow penv1 penv2 fenv1 fenv2 q -follow penv1 penv2 fenv1 fenv2 (p <|> q) = - follow penv1 penv2 fenv1 fenv2 p ++ - follow penv1 penv2 fenv1 fenv2 q -follow penv1 penv2 fenv1 fenv2 (Fix x f p) = +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) -> + 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 +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 +follow penv1 penv2 fenv1 fenv2 (Fix x p) = -- Conjecture: The fix point converges after one step -- Proof: -- - we always add information -- - no step depends on existing information follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- empty)) fenv2 p +follow penv1 penv2 fenv1 fenv2 (Map f p) = follow penv1 penv2 fenv1 fenv2 p +follow penv1 penv2 fenv1 fenv2 (WithBounds p) = follow penv1 penv2 fenv1 fenv2 p + +followChain penv1 penv2 fenv1 fenv2 [] = [] +followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = False, nil2} p ps) = + (if nil2 + then peekChain (penv2 ++ penv1) ps ++ follow penv1 penv2 fenv1 fenv2 p + else []) ++ + followChain [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps +followChain penv1 penv2 fenv1 fenv2 ((::) {nil1 = True, nil2} p ps) = + (if nil2 + then peekChain penv2 ps ++ follow penv1 penv2 fenv1 fenv2 p + else []) ++ + followChain penv1 penv2 fenv1 fenv2 ps + +followAll penv1 penv2 fenv1 fenv2 [] = [] +followAll penv1 penv2 fenv1 fenv2 (p :: ps) = + follow penv1 penv2 fenv1 fenv2 p ++ + followAll penv1 penv2 fenv1 fenv2 ps -export -WellTyped : - 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) -> - Parser i nil locked free a -> Type -WellTyped penv1 penv2 fenv1 fenv2 (Var f x) = () -WellTyped penv1 penv2 fenv1 fenv2 (Fail msg) = () -WellTyped penv1 penv2 fenv1 fenv2 (Empty x) = () -WellTyped penv1 penv2 fenv1 fenv2 (Lit text x) = () -WellTyped penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = False} p q) = - let set1 = follow penv1 penv2 fenv1 fenv2 p in - let set2 = peek (penv2 ++ penv1) q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 ((<**>) {nil1 = True} p q) = - let set1 = follow penv1 penv2 fenv1 fenv2 p in - let set2 = peek penv2 q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped penv1 penv2 fenv1 fenv2 q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 (p <|> q) = - let set1 = peek penv2 p in - let set2 = peek penv2 q in - ( WellTyped penv1 penv2 fenv1 fenv2 p - , WellTyped penv1 penv2 fenv1 fenv2 q - , So (not $ any (`elem` set2) set1) - ) -WellTyped penv1 penv2 fenv1 fenv2 (Fix x f p) = - let fst = peek penv2 p in - let flw = follow (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- empty)) fenv2 p in - WellTyped (penv1 :< (x :- fst)) penv2 (fenv1 :< (x :- flw)) fenv2 p +public export +all' : (a -> Bool) -> List a -> Bool +all' f [] = True +all' f (x :: xs) = f x && all' f xs + +allTrue : (xs : List a) -> all' (const True) xs = True +allTrue [] = Refl +allTrue (x :: xs) = allTrue xs + +public export +disjoint : Eq a => List (List a) -> Bool +disjoint [] = True +disjoint (xs :: xss) = all' (\ys => all' (\x => not (x `elem` ys)) xs) xss && disjoint xss + +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) -> + 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) -> + 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 -> + Bool + + wellTyped e penv1 penv2 fenv1 fenv2 (Var i) = True + wellTyped e penv1 penv2 fenv1 fenv2 (Lit txt) = True + wellTyped e penv1 penv2 fenv1 fenv2 (Seq ps) = wellTypedChain e penv1 penv2 fenv1 fenv2 ps + wellTyped e penv1 penv2 fenv1 fenv2 (OneOf {nils, prf} ps) = + disjoint (forget $ peekAll penv2 ps) && allWellTyped e penv1 penv2 fenv1 fenv2 ps + wellTyped e penv1 penv2 fenv1 fenv2 (Fix x p) = + wellTyped e + (penv1 :< (x :- peek penv2 p)) + penv2 + (fenv1 :< (x :- follow (penv1 :< (x :- peek penv2 p)) penv2 (fenv1 :< (x :- [])) fenv2 p)) + fenv2 + p + wellTyped e penv1 penv2 fenv1 fenv2 (Map f p) = wellTyped e penv1 penv2 fenv1 fenv2 p + wellTyped e penv1 penv2 fenv1 fenv2 (WithBounds p) = wellTyped e penv1 penv2 fenv1 fenv2 p + + wellTypedChain e penv1 penv2 fenv1 fenv2 [] = True + wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = False} p ps) = + disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain (penv2 ++ penv1) ps] && + wellTyped e penv1 penv2 fenv1 fenv2 p && + wellTypedChain e [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ps + wellTypedChain e penv1 penv2 fenv1 fenv2 ((::) {nil1 = True} p ps) = + disjoint [follow penv1 penv2 fenv1 fenv2 p, peekChain penv2 ps] && + wellTyped e penv1 penv2 fenv1 fenv2 p && + wellTypedChain e penv1 penv2 fenv1 fenv2 ps + + allWellTyped e penv1 penv2 fenv1 fenv2 [] = True + allWellTyped e penv1 penv2 fenv1 fenv2 (p :: ps) = + wellTyped e penv1 penv2 fenv1 fenv2 p && + allWellTyped e penv1 penv2 fenv1 fenv2 ps -- Parsing Function ------------------------------------------------------------ @@ -168,8 +322,10 @@ wknSmallerL (Strict prf) _ = ofSmaller prf wknSmallerL (Lax prf) _ = Lax prf wknSmallerR : (b1 : Bool) -> SmallerX b2 xs ys -> SmallerX (b1 || b2) xs ys -wknSmallerR b1 (Strict prf) = rewrite orFalseNeutral b1 in ofSmaller prf -wknSmallerR b1 (Lax prf) = rewrite orTrueTrue b1 in Lax prf +wknSmallerR b1 (Strict prf) = + if b1 then ofSmaller prf else ofSmaller prf +wknSmallerR b1 (Lax prf) = + if b1 then Lax prf else Lax prf forget : SmallerX b xs ys -> SmallerX True xs ys forget = wknSmallerR True @@ -180,6 +336,16 @@ toSmaller {xs = []} {ys = (y :: ys)} (Strict prf) = LTESucc LTEZero toSmaller {xs = (x :: xs)} {ys = []} (Strict prf) impossible toSmaller {xs = (x :: xs)} {ys = (y :: ys)} (Strict (LTESucc prf)) = LTESucc (toSmaller (Strict prf)) +anyCons : (b : Bool) -> (bs : List Bool) -> any Basics.id (b :: bs) = b || any Basics.id bs +anyCons b [] = sym (orFalseNeutral b) +anyCons b (b' :: bs) = + trans (anyCons (b || b') bs) $ + trans (sym $ orAssociative b b' (any id bs)) + (cong (b ||) (sym $ anyCons b' bs)) + +anyTrue : (bs : List Bool) -> any Basics.id (True :: bs) = True +anyTrue = anyCons True + -- Return Type namespace M @@ -203,39 +369,146 @@ namespace M wknR b1 (Err msg) = Err msg wknR b1 (Ok res ys prf) = Ok res ys (wknSmallerR b1 prf) + export + anyL : + (b : Bool) -> {0 bs : List Bool} -> + M xs (any Basics.id bs) a -> M xs (any Basics.id (b :: bs)) a + anyL b m = rewrite anyCons b bs in wknR b m + + export + anyR : (bs : List Bool) -> M xs b a -> M xs (any Basics.id (b :: bs)) a + anyR bs m = rewrite anyCons b bs in wknL m (any id bs) + -- 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) + parser : - Eq i => Interpolation i => + (e : Eq i) => Interpolation i => (p : Parser i nil locked free a) -> (penv1 : _) -> (penv2 : _) -> (fenv1 : _) -> (fenv2 : _) -> - {auto 0 wf : WellTyped penv1 penv2 fenv1 fenv2 p} -> + {auto 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 -> M xs nil a -parser (Var f x) penv1 penv2 fenv1 fenv2 xs env1 env2 = - f <$> indexAll x env2 xs (Lax reflexive) -parser (Fail msg) penv1 penv2 fenv1 fenv2 xs env1 env2 = - Err msg -parser (Empty x) penv1 penv2 fenv1 fenv2 xs env1 env2 = - Ok x xs (Lax reflexive) -parser (Lit text f) penv1 penv2 fenv1 fenv2 xs env1 env2 = +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)} -> + (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 : + (e : Eq i) => Interpolation i => + (at : FirstNil 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 : 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 = + 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 (f y.val.text) ys (Strict reflexive) - else Err "\{show y.bounds}: expected \{text}, got \{y.val.kind}" -parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = + 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} = + let 0 wfs = soAnd {a = disjoint (forget $ peekAll penv2 ps)} wf in + case findNil nils 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} = + 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 = + 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 f ys lt => + Ok x ys lt => case - parser q [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) + parserChain ps [<] (penv2 ++ penv1) [<] (fenv2 ++ fenv1) ys [<] ( mapProperty (\f, zs, 0 prf => f zs $ forget $ transX prf lt) env2 @@ -243,122 +516,102 @@ parser ((<**>) {nil1 = False, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = ) of Err msg => Err msg - Ok x zs prf => Ok (f x) zs (rewrite sym $ andFalseFalse nil2 in transX prf lt) -parser ((<**>) {nil1 = True, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = + 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 f ys lte => + Ok x ys lte => case - parser q penv1 penv2 fenv1 fenv2 + 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 x zs prf => Ok (f x) zs (rewrite sym $ andTrueNeutral nil2 in transX prf lte) -parser ((<|>) {nil1, nil2} p q) penv1 penv2 fenv1 fenv2 xs env1 env2 = - case xs of - [] => - if nil1 - then parser p penv1 penv2 fenv1 fenv2 [] env1 env2 - else if nil2 - then parser q penv1 penv2 fenv1 fenv2 [] env1 env2 - else Err "unexpected end of input" - x :: xs => - if elem x.val.kind (peek penv2 p) - then wknL (parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) nil2 - else if elem x.val.kind (peek penv2 q) - then wknR nil1 (parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2) - else if nil1 - then parser p penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - else if nil2 - then parser q penv1 penv2 fenv1 fenv2 (x :: xs) env1 env2 - else Err "\{show x.bounds}: unexpected \{x.val.kind}" -parser (Fix {a, b, nil} x f p) penv1 penv2 fenv1 fenv2 xs env1 env2 = - let g = parser p _ _ _ _ {wf} in - let - res : M xs nil a - res = - sizeInd {P = \ys => (0 prf : SmallerX True ys xs) -> M ys nil a} - (\ys, rec, lte => - g 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 - f <$> res + 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 = + 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 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 = + 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) export parse : - Eq i => Interpolation i => + (e : Eq i) => Interpolation i => (p : Parser i nil [<] [<] a) -> - {auto 0 wf : WellTyped [<] [<] [<] [<] p} -> + {auto 0 wf : So (wellTyped e [<] [<] [<] [<] p)} -> (xs : List (WithBounds (Token i))) -> M xs nil a parse p xs = parser p [<] [<] [<] [<] xs [<] [<] --- Weakening ------------------------------------------------------------------- +-- Functor --------------------------------------------------------------------- public export -rename : - (len1 : Length locked1) -> - (len2 : Length locked2) -> - (forall x. Var locked1 x -> Var locked2 x) -> - (forall x. Var free1 x -> Var free2 x) -> - Parser i nil locked1 free1 a -> Parser i nil locked2 free2 a -rename len1 len2 ren1 ren2 (Var f x) = Var f (ren2 x) -rename len1 len2 ren1 ren2 (Fail msg) = Fail msg -rename len1 len2 ren1 ren2 (Empty x) = Empty x -rename len1 len2 ren1 ren2 (Lit text x) = Lit text x -rename len1 len2 ren1 ren2 ((<**>) {nil1 = False} p q) = - rename len1 len2 ren1 ren2 p <**> - rename Z Z id (either (wknL {len = len2} . ren2) (wknR . ren1) . split) q -rename len1 len2 ren1 ren2 ((<**>) {nil1 = True} p q) = - rename len1 len2 ren1 ren2 p <**> rename len1 len2 ren1 ren2 q -rename len1 len2 ren1 ren2 (p <|> q) = - rename len1 len2 ren1 ren2 p <|> rename len1 len2 ren1 ren2 q -rename len1 len2 ren1 ren2 (Fix x f p) = - Fix x f (rename (S len1) (S len2) (lift {len = S Z} ren1) ren2 p) +(++) : + {nil2 : Bool} -> + ParserChain i nil1 locked free as -> + ParserChain i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) bs -> + ParserChain i (nil1 && nil2) locked free (as ++ bs) +[] ++ qs = qs +((::) {nil1 = False, nil2} p ps) ++ qs = + p :: + ( ps + ++ rewrite linUnlessLin (Bool, Type) nil2 in + rewrite linUnlessLin (Bool, Type) (not nil2) in + qs) +((::) {nil1 = True, nil2} p ps) ++ qs = p :: (ps ++ qs) public export -weaken : - (len1 : Length free2) -> - {auto len2 : Length locked} -> - Parser i nil (free2 ++ locked) free1 a -> Parser i nil locked (free1 ++ free2) a -weaken len1 (Var f x) = Var f (wknL x) -weaken len1 (Fail msg) = Fail msg -weaken len1 (Empty x) = Empty x -weaken len1 (Lit text x) = Lit text x -weaken len1 ((<**>) {nil1 = False} p q) = - weaken len1 p <**> - rename Z Z - id - ( either (wknL . wknL) (either (wknL . wknR) wknR . split) - . split {len = lengthAppend len1 len2} - ) - q -weaken len1 ((<**>) {nil1 = True} p q) = weaken len1 p <**> weaken len1 q -weaken len1 (p <|> q) = weaken len1 p <|> weaken len1 q -weaken len1 (Fix x f p) = Fix x f (weaken len1 p) - -public export -shift : - {auto len1 : Length locked1} -> - (len2 : Length locked2) -> - (len3 : Length free2) -> - Parser i nil locked1 free1 a -> Parser i nil (locked1 ++ locked2) (free1 ++ free2) a -shift len2 len3 = rename len1 (lengthAppend len1 len2) wknL wknL +(<**>) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> + Parser i (nil1 && nil2) locked free (a, b) +p <**> Seq ps = Map (\(x :: xs) => (x, xs)) $ Seq (p :: ps) +-- HACK: andTrueNeutral isn't public, so do a full case split. +(<**>) {nil1 = True, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = True, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = False, nil2 = True} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] +(<**>) {nil1 = False, nil2 = False} p q = Map (\[x, y] => (x, y)) $ Seq [p, q] + +public export +Functor (Parser i nil locked free) where + map f (Map g p) = Map (f . g) p + map f p = Map f p + +public export +Applicative (Parser i True locked free) where + pure x = map (const x) (Seq []) + p <*> q = map (\(f, x) => f x) (p <**> q) -- Combinator ------------------------------------------------------------------ public export +(<|>) : + {nil1, nil2 : Bool} -> + Parser i nil1 locked free a -> + Parser i nil2 locked free a -> + {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> + Parser i (nil1 || nil2) locked free a +p <|> q = OneOf [p, q] + +public export (<||>) : {nil1, nil2 : Bool} -> Parser i nil1 locked free a -> Parser i nil2 locked free b -> - So (not (nil1 && nil2)) => + {auto 0 prf : length (filter Basics.id [nil1, nil2]) `LTE` 1} -> Parser i (nil1 || nil2) locked free (Either a b) p <||> q = Left <$> p <|> Right <$> q @@ -368,7 +621,7 @@ public export Parser i nil1 locked free a -> Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> Parser i (nil1 && nil2) locked free b -p **> q = (\_ => id) <$> p <**> q +p **> q = snd <$> (p <**> q) public export (<**) : @@ -376,11 +629,24 @@ public export Parser i nil1 locked free a -> Parser i nil2 (linUnless nil1 locked) (free ++ linUnless (not nil1) locked) b -> Parser i (nil1 && nil2) locked free a -p <** q = const <$> p <**> q +p <** q = fst <$> (p <**> q) public export match : TokenKind i => (kind : i) -> Parser i False locked free (TokType kind) -match kind = Lit kind (tokValue kind) +match kind = Map (tokValue kind) $ Lit kind + +public export +enclose : + {b1, b2, b3 : Bool} -> + (left : Parser i b1 locked free ()) -> + (right : + Parser i b3 + (linUnless b2 (linUnless b1 locked)) + ((free ++ linUnless (not b1) locked) ++ linUnless (not b2) (linUnless b1 locked)) + ()) -> + Parser i b2 (linUnless b1 locked) (free ++ linUnless (not b1) locked) a -> + Parser i (b1 && b2 && b3 && True) locked free a +enclose left right p = (\[_, x, _] => x) <$> Seq {as = [(), a, ()]} [left, p, right] public export option : Parser i False locked free a -> Parser i True locked free (Maybe a) @@ -392,15 +658,29 @@ plus : Parser i False locked free a -> Parser i False locked free (List1 a) plus p = - Fix "plus" id - ( (:::) <$> shift (S Z) Z p - <**> maybe [] forget <$> option (Var id (%% "plus"))) + Fix "plus" + ( uncurry (:::) + <$> (rename (Drop Id) Id p <**> maybe [] forget <$> option (Var $ %% "plus"))) public export star : {auto len : Length locked} -> Parser i False locked free a -> Parser i True locked free (List a) -star p = - Fix "star" id - (maybe [] id <$> option ((::) <$> shift (S Z) Z p <**> Var id (%% "star"))) +star p = maybe [] forget <$> option (plus p) + +public export +sepBy1 : + {auto len : Length locked} -> + (sep : Parser i False locked free ()) -> + Parser i False locked free a -> + Parser i False locked free (List1 a) +sepBy1 sep p = uncurry (:::) <$> (p <**> star (weaken len sep **> weaken len p)) + +public export +sepBy : + {auto len : Length locked} -> + (sep : Parser i False locked free ()) -> + Parser i False locked free a -> + Parser i True locked free (List a) +sepBy sep p = maybe [] forget <$> option (sepBy1 sep p) diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr new file mode 100644 index 0000000..7a67441 --- /dev/null +++ b/src/Inky/Term/Parser.idr @@ -0,0 +1,286 @@ +module Inky.Term.Parser + +import Data.List1 +import Data.String +import Inky.Context +import Inky.Parser +import Inky.Term +import Inky.Thinning +import Inky.Type +import Text.Lexer + +-- Lexer ----------------------------------------------------------------------- + +export +data InkyKind + = TermIdent + | TypeIdent + | Lit + | Suc + | Let + | In + | Case + | Of + | Fold + | By + | Nat + | ParenOpen + | ParenClose + | BracketOpen + | BracketClose + | AngleOpen + | AngleClose + | BraceOpen + | BraceClose + | Arrow + | DoubleArrow + | Bang + | Tilde + | Backslash + | Colon + | Equal + | Comma + | Ignore + +export +[EqI] Eq InkyKind where + TermIdent == TermIdent = True + TypeIdent == TypeIdent = True + Lit == Lit = True + Suc == Suc = True + Let == Let = True + In == In = True + Case == Case = True + Of == Of = True + Fold == Fold = True + By == By = True + Nat == Nat = True + ParenOpen == ParenOpen = True + ParenClose == ParenClose = True + BracketOpen == BracketOpen = True + BracketClose == BracketClose = True + AngleOpen == AngleOpen = True + AngleClose == AngleClose = True + BraceOpen == BraceOpen = True + BraceClose == BraceClose = True + Arrow == Arrow = True + DoubleArrow == DoubleArrow = True + Bang == Bang = True + Tilde == Tilde = True + Backslash == Backslash = True + Colon == Colon = True + Equal == Equal = True + Comma == Comma = True + Ignore == Ignore = True + _ == _ = False + +export +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'" + interpolate Of = "'of'" + interpolate Fold = "'fold'" + interpolate By = "'by'" + interpolate Nat = "'Nat'" + interpolate ParenOpen = "'('" + interpolate ParenClose = "')'" + interpolate BracketOpen = "'['" + interpolate BracketClose = "']'" + interpolate AngleOpen = "'<'" + interpolate AngleClose = "'>'" + interpolate BraceOpen = "'{'" + interpolate BraceClose = "'}'" + interpolate Arrow = "'->'" + interpolate DoubleArrow = "'=>'" + interpolate Bang = "'!'" + interpolate Tilde = "'~'" + interpolate Backslash = "'\\'" + interpolate Colon = "':'" + interpolate Equal = "'='" + interpolate Comma = "','" + interpolate Ignore = "" + +TokenKind InkyKind where + TokType TermIdent = String + TokType TypeIdent = String + TokType Lit = Nat + TokType _ = () + + tokValue TermIdent = id + tokValue TypeIdent = id + tokValue Lit = stringToNatOrZ + tokValue Suc = const () + tokValue Let = const () + tokValue In = const () + tokValue Case = const () + tokValue Of = const () + tokValue Fold = const () + tokValue By = const () + tokValue Nat = const () + tokValue ParenOpen = const () + tokValue ParenClose = const () + tokValue BracketOpen = const () + tokValue BracketClose = const () + tokValue AngleOpen = const () + tokValue AngleClose = const () + tokValue BraceOpen = const () + tokValue BraceClose = const () + tokValue Arrow = const () + tokValue DoubleArrow = const () + tokValue Bang = const () + tokValue Tilde = const () + tokValue Backslash = const () + tokValue Colon = const () + tokValue Equal = const () + tokValue Comma = const () + tokValue Ignore = const () + +keywords : List (String, InkyKind) +keywords = + [ ("suc", Suc) + , ("let", Let) + , ("in", In) + , ("case", Case) + , ("of", Of) + , ("fold", Fold) + , ("by", By) + , ("Nat", Nat) + ] + +export +relevant : InkyKind -> Bool +relevant = (/=) @{EqI} Ignore + +public export +InkyToken : Type +InkyToken = Token InkyKind + +termIdentifier : Lexer +termIdentifier = lower <+> many (alphaNum <|> exact "_") + +typeIdentifier : Lexer +typeIdentifier = upper <+> many (alphaNum <|> exact "_") + +export +tokenMap : TokenMap InkyToken +tokenMap = + toTokenMap [(spaces, Ignore)] ++ + [(termIdentifier, \s => + case lookup s keywords of + Just k => Tok k s + Nothing => Tok TermIdent s) + ,(typeIdentifier, \s => + case lookup s keywords of + Just k => Tok k s + Nothing => Tok TypeIdent s)] ++ + toTokenMap + [ (digits, Lit) + , (exact "(", ParenOpen) + , (exact ")", ParenClose) + , (exact "[", BracketOpen) + , (exact "]", BracketClose) + , (exact "<", AngleOpen) + , (exact ">", AngleClose) + , (exact "{", BraceOpen) + , (exact "}", BraceClose) + , (exact "->", Arrow) + , (exact "=>", DoubleArrow) + , (exact "!", Bang) + , (exact "~", Tilde) + , (exact "\\", Backslash) + , (exact ":", Colon) + , (exact "=", Equal) + , (exact ",", Comma) + ] + +-- Parser ---------------------------------------------------------------------- + +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) + a + +public export +record TypeFun where + constructor MkTypeFun + try : (ctx : Context ()) -> Either String (Ty ctx ()) + +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")]) + where + mkAssoc : HList [String, (), TypeFun] -> Assoc TypeFun + mkAssoc [x, _, v] = x :- v + +tryRow : WithBounds (List $ Assoc TypeFun) -> (ctx : Context ()) -> Either String (Row (Ty 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}\"" + pure row') + [<] + xs.val + +OpenOrFixpointType : TypeParser [<] [<"openType" :- ()] +OpenOrFixpointType = + OneOf + [ mkFix <$> + Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%% "openType")] + , Var (%% "openType") + ] + where + mkFix : HList [(), String, (), TypeFun] -> TypeFun + mkFix [_, x, _, a] = MkTypeFun (\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) + , 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}\"") + + mkProd : WithBounds (List $ Assoc TypeFun) -> TypeFun + mkProd xs = MkTypeFun (\ctx => TProd <$> tryRow xs ctx) + + mkSum : WithBounds (List $ Assoc TypeFun) -> TypeFun + mkSum xs = MkTypeFun (\ctx => TSum <$> tryRow xs ctx) + +export +OpenType : TypeParser [<] [<] +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) |])) + +%hint +export +OpenTypeWf : So (wellTyped EqI [<] [<] [<] [<] OpenType) +OpenTypeWf = Oh diff --git a/src/Inky/Thinning.idr b/src/Inky/Thinning.idr index 3d593ae..87640e2 100644 --- a/src/Inky/Thinning.idr +++ b/src/Inky/Thinning.idr @@ -20,13 +20,14 @@ data Thins : Context a -> Context a -> Type where -- 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) -export +public export index : ctx1 `Thins` ctx2 -> Var ctx1 v -> Var ctx2 v index f i = indexPos f i.pos @@ -53,24 +54,6 @@ 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) -export -indexId : (0 i : Var ctx v) -> index Id i = i -indexId (%% x) = Refl - -export -indexDrop : (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) -> index (Drop f) i = ThereVar (index f i) -indexDrop f (%% x) = Refl - -export -indexKeepHere : (0 f : ctx1 `Thins` ctx2) -> index (Keep {x, y} f) (%% x) = (%% y) -indexKeepHere f = Refl - -export -indexKeepThere : - (0 f : ctx1 `Thins` ctx2) -> (0 i : Var ctx1 v) -> - index (Keep f) (ThereVar i) = ThereVar (index f i) -indexKeepThere f (%% x) = Refl - indexPosComp : (f : ctx2 `Thins` ctx3) -> (g : ctx1 `Thins` ctx2) -> (pos : VarPos ctx1 x v) -> indexPos (f . g) pos = index f (indexPos g pos) @@ -117,6 +100,80 @@ 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 ---------------------------------------------------------------- -------------------------------------------------------------------------------- @@ -145,7 +202,7 @@ lookup env i = lookupPos env i.pos export lookupHere : (0 env : Env ctx1 ctx2 p) -> (0 x : String) -> (0 pv : p v) -> - lookup (env :< (x :- pv)) (%% x) = Right pv + lookup (env :< (x :- pv)) (toVar Here) = Right pv lookupHere env x pv = Refl export diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr index e3eee12..9cfc1f7 100644 --- a/src/Inky/Type.idr +++ b/src/Inky/Type.idr @@ -65,7 +65,7 @@ thinCongAll prf (as :< (x :- a)) = thinId : (a : Ty ctx v) -> thin Id a = a thinIdAll : (as : Row (Ty ctx v)) -> thinAll Id as = as -thinId (TVar i) = cong TVar (indexId i) +thinId (TVar (%% x)) = Refl thinId TNat = Refl thinId (TArrow a b) = cong2 TArrow (thinId a) (thinId b) thinId (TProd as) = cong TProd (thinIdAll as) |