diff --git a/TinyIdris-v1/src/Core/CaseBuilder.idr b/TinyIdris-v1/src/Core/CaseBuilder.idr index 41e2229..7df08ec 100644 --- a/TinyIdris-v1/src/Core/CaseBuilder.idr +++ b/TinyIdris-v1/src/Core/CaseBuilder.idr @@ -10,7 +10,7 @@ import Core.Value import Data.LengthMatch import Data.List -import Data.Strings +import Data.String import Decidable.Equality @@ -22,6 +22,7 @@ data ArgType : List Name -> Type where Unknown : ArgType vars -- arg's type is not yet known due to a previously stuck argument +covering {ns : _} -> Show (ArgType ns) where show (Known t) = "Known " ++ show t show (Stuck t) = "Stuck " ++ show t @@ -72,7 +73,7 @@ updatePats {todo = pvar :: ns} env (NBind _ (Pi _ farg) fsc) (p :: ps) Unknown => do defs <- get Ctxt empty <- clearDefs defs - pure (record { argType = Known !(quote empty env farg) } p + pure ({ argType := Known !(quote empty env farg) } p :: !(updatePats env !(fsc defs (toClosure env (Ref Bound pvar))) ps)) _ => pure (p :: ps) updatePats env nf (p :: ps) @@ -80,7 +81,7 @@ updatePats env nf (p :: ps) Unknown => do defs <- get Ctxt empty <- clearDefs defs - pure (record { argType = Stuck !(quote empty env nf) } p :: ps) + pure ({ argType := Stuck !(quote empty env nf) } p :: ps) _ => pure (p :: ps) substInPatInfo : {pvar, vars, todo : _} -> @@ -90,14 +91,14 @@ substInPatInfo : {pvar, vars, todo : _} -> Core (PatInfo pvar vars, NamedPats vars todo) substInPatInfo {pvar} {vars} n tm p ps = case argType p of - Known ty => pure (record { argType = Known (substName n tm ty) } p, ps) + Known ty => pure ({ argType := Known (substName n tm ty) } p, ps) Stuck fty => do defs <- get Ctxt empty <- clearDefs defs let env = mkEnv vars case !(nf defs env (substName n tm fty)) of NBind _ (Pi _ farg) fsc => - pure (record { argType = Known !(quote empty env farg) } p, + pure ({ argType := Known !(quote empty env farg) } p, !(updatePats env !(fsc defs (toClosure env (Ref Bound pvar))) ps)) @@ -259,7 +260,6 @@ checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pa (Just Refl, Yes Refl) => ConMatch prf _ => NoMatch checkGroupMatch (CName x tag) ps _ = NoMatch -checkGroupMatch _ _ _ = NoMatch data PName : Type where @@ -305,7 +305,7 @@ newPats : (pargs : List Pat) -> LengthMatch pargs ns -> NamedPats vars ns newPats [] NilMatch rest = [] newPats (newpat :: xs) (ConsMatch w) (pi :: rest) - = record { pat = newpat} pi :: newPats xs w rest + = { pat := newpat} pi :: newPats xs w rest updateNames : List (Name, Pat) -> List (Name, Name) updateNames = mapMaybe update @@ -317,7 +317,7 @@ updateNames = mapMaybe update updatePatNames : List (Name, Name) -> NamedPats vars todo -> NamedPats vars todo updatePatNames _ [] = [] updatePatNames ns (pi :: ps) - = record { pat $= update } pi :: updatePatNames ns ps + = { pat $= update } pi :: updatePatNames ns ps where update : Pat -> Pat update (PCon n i a ps) = PCon n i a (map update ps) @@ -641,7 +641,7 @@ mutual pure (Just !(varRule fn vs fallthrough)) mixture fn {a} {todo} NoClauses err = pure err --- +-- mkPatClause : {auto c : Ref Ctxt Defs} -> Name -> diff --git a/TinyIdris-v1/src/Core/CaseTree.idr b/TinyIdris-v1/src/Core/CaseTree.idr index 0d0dd66..8452b2f 100644 --- a/TinyIdris-v1/src/Core/CaseTree.idr +++ b/TinyIdris-v1/src/Core/CaseTree.idr @@ -71,7 +71,7 @@ data Pat : Type where PLoc : Name -> Pat PUnmatchable : Term [] -> Pat -export +export covering Show Pat where show (PCon n t a args) = show n ++ show (t, a) ++ show args show (PLoc n) = "{" ++ show n ++ "}" @@ -104,7 +104,7 @@ mkTerm vars (PUnmatchable tm) = embed tm -- Show instances mutual - export + export covering {vars : _} -> Show (CaseTree vars) where show (Case {name} idx prf ty alts) = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++ @@ -113,7 +113,7 @@ mutual show (Unmatched msg) = "Error: " ++ show msg show Impossible = "Impossible" - export + export covering {vars : _} -> Show (CaseAlt vars) where show (ConCase n tag args sc) = show n ++ " " ++ showSep " " (map show args) ++ " => " ++ diff --git a/TinyIdris-v1/src/Core/Core.idr b/TinyIdris-v1/src/Core/Core.idr index dfce5a7..dadefb3 100644 --- a/TinyIdris-v1/src/Core/Core.idr +++ b/TinyIdris-v1/src/Core/Core.idr @@ -36,7 +36,7 @@ data Error : Type where GenericMsg : String -> Error FileErr : String -> FileError -> Error -export +export covering Show Error where show (CantConvert env x y) = "Type mismatch: " ++ show x ++ " and " ++ show y @@ -116,6 +116,10 @@ export %inline pure : a -> Core a pure x = MkCore (pure (pure x)) +export %inline +(>>) : Core a -> (Core b) -> Core b +(>>) a b = do _ <- a ; b + export (<*>) : Core (a -> b) -> Core a -> Core b (<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |] @@ -153,7 +157,7 @@ traverse f xs = traverse' f xs [] export traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b) -traverseList1 f (x :: xs) = [| f x :: traverse f xs |] +traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |] export traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b) @@ -174,7 +178,7 @@ traverse_ f (x :: xs) export traverseList1_ : (a -> Core b) -> List1 a -> Core () -traverseList1_ f (x :: xs) = do +traverseList1_ f (x ::: xs) = do f x traverse_ f xs diff --git a/TinyIdris-v1/src/Core/Env.idr b/TinyIdris-v1/src/Core/Env.idr index 83683c8..d1819f0 100644 --- a/TinyIdris-v1/src/Core/Env.idr +++ b/TinyIdris-v1/src/Core/Env.idr @@ -8,7 +8,7 @@ data Env : (tm : List Name -> Type) -> List Name -> Type where Nil : Env tm [] (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars) -revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xs +revOnto : (xs, vs : _) -> List.reverseOnto xs vs = reverse vs ++ xs revOnto xs [] = Refl revOnto xs (v :: vs) = rewrite revOnto (v :: xs) vs in @@ -28,7 +28,7 @@ revNs (v :: vs) ns -- in big environments -- Also reversing the names at the end saves significant time over concatenating -- when environments get fairly big. -getBinderUnder : Weaken tm => +getBinderUnder : {tm : _} -> Weaken tm => {vars : _} -> {idx : Nat} -> (ns : List Name) -> (0 p : IsVar x idx vars) -> Env tm vars -> @@ -39,7 +39,7 @@ getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env) = getBinderUnder (v :: ns) lp env export -getBinder : Weaken tm => +getBinder : {tm : _} -> Weaken tm => {vars : _} -> {idx : Nat} -> (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm vars) getBinder el env = getBinderUnder [] el env diff --git a/TinyIdris-v1/src/Core/Normalise.idr b/TinyIdris-v1/src/Core/Normalise.idr index 7fee171..9cb90ae 100644 --- a/TinyIdris-v1/src/Core/Normalise.idr +++ b/TinyIdris-v1/src/Core/Normalise.idr @@ -14,7 +14,7 @@ import Data.Vect -- part will only be constructed when needed, because it's in Core. public export data Glued : List Name -> Type where - MkGlue : Core (Term vars) -> + MkGlue : Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars export @@ -39,7 +39,7 @@ data CaseResult a = Result a | NoMatch -- case alternative didn't match anything | GotStuck -- alternative matched, but got stuck later - + -- So that we can call 'eval' with new defs evalTop : {free, vars : _} -> Defs -> Env Term free -> LocalEnv free vars -> diff --git a/TinyIdris-v1/src/Core/TT.idr b/TinyIdris-v1/src/Core/TT.idr index 44e30a9..daa2202 100644 --- a/TinyIdris-v1/src/Core/TT.idr +++ b/TinyIdris-v1/src/Core/TT.idr @@ -125,7 +125,7 @@ data Term : List Name -> Type where Erased : Term vars public export -interface Weaken (tm : List Name -> Type) where +interface Weaken (0 tm : List Name -> Type) where weaken : {n, vars : _} -> tm vars -> tm (n :: vars) weakenNs : {vars : _} -> (ns : List Name) -> tm vars -> tm (ns ++ vars) @@ -384,7 +384,7 @@ nameAt : {vars : _} -> nameAt {vars = n :: ns} Z First = n nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p -export +export covering {vars : _} -> Show (Term vars) where show tm = let (fn, args) = getFnArgs tm in showApp fn args where diff --git a/TinyIdris-v1/src/Parser/Lexer/Package.idr b/TinyIdris-v1/src/Parser/Lexer/Package.idr index 1a063c7..512f041 100644 --- a/TinyIdris-v1/src/Parser/Lexer/Package.idr +++ b/TinyIdris-v1/src/Parser/Lexer/Package.idr @@ -6,7 +6,7 @@ import public Text.Parser import Data.List import Data.List1 -import Data.Strings +import Data.String import Data.String.Extra import Utils.String @@ -27,7 +27,7 @@ Show Token where show (Comment str) = "Comment: " ++ str show EndOfInput = "EndOfInput" show Equals = "Equals" - show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid) + show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (toList dsid) show Separator = "Separator" show Space = "Space" show (StringLit s) = "StringLit: " ++ s @@ -50,7 +50,7 @@ rawTokens = ] where splitNamespace : String -> List1 String - splitNamespace = Data.Strings.split (== '.') + splitNamespace = split (== '.') export lex : String -> Either (Int, Int, String) (List (TokenData Token)) diff --git a/TinyIdris-v1/src/Parser/Lexer/Source.idr b/TinyIdris-v1/src/Parser/Lexer/Source.idr index f2910cc..a285680 100644 --- a/TinyIdris-v1/src/Parser/Lexer/Source.idr +++ b/TinyIdris-v1/src/Parser/Lexer/Source.idr @@ -4,7 +4,7 @@ import public Parser.Lexer.Common import Data.List1 import Data.List -import Data.Strings +import Data.String import Data.String.Extra import Utils.Hex @@ -46,7 +46,7 @@ Show Token where -- Identifiers show (HoleIdent x) = "hole identifier " ++ x show (Ident x) = "identifier " ++ x - show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs) + show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (toList $ reverse xs) show (DotIdent x) = "dot+identifier " ++ x show (Symbol x) = "symbol " ++ x -- Comments @@ -222,7 +222,7 @@ rawTokens = else Ident x parseNamespace : String -> Token parseNamespace ns = case List1.reverse . split (== '.') $ ns of - [ident] => parseIdent ident + (ident ::: []) => parseIdent ident ns => DotSepIdent ns export diff --git a/TinyIdris-v1/src/Parser/Rule/Package.idr b/TinyIdris-v1/src/Parser/Rule/Package.idr index 643d4b5..2fbbaee 100644 --- a/TinyIdris-v1/src/Parser/Rule/Package.idr +++ b/TinyIdris-v1/src/Parser/Rule/Package.idr @@ -34,7 +34,7 @@ export exactProperty : String -> Rule String exactProperty p = terminal ("Expected property " ++ p) (\x => case tok x of - DotSepIdent [p'] => + DotSepIdent (p' ::: []) => if p == p' then Just p else Nothing _ => Nothing) @@ -64,7 +64,7 @@ export packageName : Rule String packageName = terminal "Expected package name" (\x => case tok x of - DotSepIdent [str] => + DotSepIdent (str ::: []) => if isIdent AllowDashes str then Just str else Nothing _ => Nothing) diff --git a/TinyIdris-v1/src/Parser/Rule/Source.idr b/TinyIdris-v1/src/Parser/Rule/Source.idr index 63b721e..b6a3dc8 100644 --- a/TinyIdris-v1/src/Parser/Rule/Source.idr +++ b/TinyIdris-v1/src/Parser/Rule/Source.idr @@ -6,7 +6,7 @@ import public Parser.Support import Core.TT import Data.List1 -import Data.Strings +import Data.String %default total @@ -124,7 +124,7 @@ namespacedIdent = terminal "Expected namespaced name" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just [i] + Ident i => Just (singleton i) _ => Nothing) export @@ -133,7 +133,7 @@ moduleIdent = terminal "Expected module identifier" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just [i] + Ident i => Just (singleton i) _ => Nothing) export @@ -168,8 +168,8 @@ init = 0 continueF : SourceEmptyRule () -> (indent : IndentInfo) -> SourceEmptyRule () continueF err indent - = do eoi; err - <|> do keyword "where"; err + = eoi *> err + <|> keyword "where" *> err <|> do col <- Common.column if col <= indent then err @@ -259,9 +259,9 @@ atEndIndent indent -- must start, given where the current block entry started terminator : ValidIndent -> Int -> SourceEmptyRule ValidIndent terminator valid laststart - = do eoi - pure EndOfBlock - <|> do symbol ";" + = (eoi *> + pure EndOfBlock) + <|> symbol ";" *> pure (afterSemi valid) <|> do col <- column afterDedent valid col @@ -307,7 +307,7 @@ blockEntry valid rule blockEntries : ValidIndent -> (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty) blockEntries valid rule - = do eoi; pure [] + = eoi *> pure [] <|> do res <- blockEntry valid rule ts <- blockEntries (snd res) rule pure (fst res :: ts) diff --git a/TinyIdris-v1/src/Parser/Unlit.idr b/TinyIdris-v1/src/Parser/Unlit.idr index e0ca498..fcd80f0 100644 --- a/TinyIdris-v1/src/Parser/Unlit.idr +++ b/TinyIdris-v1/src/Parser/Unlit.idr @@ -1,7 +1,7 @@ module Parser.Unlit import public Text.Literate -import Data.Strings +import Data.String %default total diff --git a/TinyIdris-v1/src/TTImp/Parser.idr b/TinyIdris-v1/src/TTImp/Parser.idr index a9a9921..e50c280 100644 --- a/TinyIdris-v1/src/TTImp/Parser.idr +++ b/TinyIdris-v1/src/TTImp/Parser.idr @@ -10,7 +10,7 @@ import public Text.Parser import Data.List import Data.List.Views import Data.List1 -import Data.Strings +import Data.String import Debug.Trace @@ -41,8 +41,8 @@ collectDefs : List ImpDecl -> List ImpDecl atom : FileName -> Rule RawImp atom fname - = do exactIdent "Type" - pure IType + = exactIdent "Type" + *> pure IType -- <|> do start <- location -- symbol "_" -- end <- location @@ -56,8 +56,8 @@ getRight (Right v) = Just v bindSymbol : Rule PiInfo bindSymbol - = do symbol "->" - pure Explicit + = symbol "->" + *> pure Explicit mutual appExpr : FileName -> IndentInfo -> Rule RawImp @@ -68,8 +68,8 @@ mutual argExpr : FileName -> IndentInfo -> Rule RawImp argExpr fname indents - = do continue indents - simpleExpr fname indents + = continue indents + *> simpleExpr fname indents simpleExpr : FileName -> IndentInfo -> Rule RawImp simpleExpr fname indents @@ -112,8 +112,8 @@ mutual (do n <- unqualifiedName ty <- option Implicit - (do symbol ":" - appExpr fname indents) + (symbol ":" + *> appExpr fname indents) pure (UN n, ty)) @@ -143,7 +143,7 @@ mutual commit ns <- sepBy1 (symbol ",") unqualifiedName let binders = map (\n => (Just (UN n), Implicit)) ns - symbol "." + _ <- symbol "." scope <- typeExpr fname indents pure (pibindAll Implicit binders scope) diff --git a/TinyIdris-v1/src/TTImp/ProcessDef.idr b/TinyIdris-v1/src/TTImp/ProcessDef.idr index 6736791..10ac8f5 100644 --- a/TinyIdris-v1/src/TTImp/ProcessDef.idr +++ b/TinyIdris-v1/src/TTImp/ProcessDef.idr @@ -28,7 +28,7 @@ processClause : {auto c : Ref Ctxt Defs} -> processClause (PatClause lhs rhs) = do -- Check the LHS (lhstm, lhsty) <- checkTerm [] lhs Nothing - -- Get the pattern variables from the LHS, and the expected type, + -- Get the pattern variables from the LHS, and the expected type, -- and check the RHS in that context (vars ** (env, lhsenv, rhsexp)) <- @@ -50,5 +50,5 @@ processDef n clauses (args ** tree) <- getPMDef n (type gdef) chkcs -- Update the definition with the compiled tree - updateDef n (record { definition = PMDef args tree }) + updateDef n ({ definition := PMDef args tree }) coreLift $ putStrLn $ "Processed " ++ show n diff --git a/TinyIdris-v1/src/Text/Lexer/Core.idr b/TinyIdris-v1/src/Text/Lexer/Core.idr index ff145fb..437c4ed 100644 --- a/TinyIdris-v1/src/Text/Lexer/Core.idr +++ b/TinyIdris-v1/src/Text/Lexer/Core.idr @@ -5,7 +5,7 @@ import Data.Bool.Extra import Data.List import Data.Maybe import Data.Nat -import Data.Strings +import Data.String %default total diff --git a/TinyIdris-v1/src/Text/Literate.idr b/TinyIdris-v1/src/Text/Literate.idr index 557fb12..51e2856 100644 --- a/TinyIdris-v1/src/Text/Literate.idr +++ b/TinyIdris-v1/src/Text/Literate.idr @@ -27,7 +27,7 @@ import Text.Lexer import Data.List import Data.List.Views -import Data.Strings +import Data.String %default total @@ -63,12 +63,12 @@ rawTokens delims ls = ||| Merge the tokens into a single source file. reduce : List (TokenData Token) -> List String -> String -reduce [] acc = fastAppend (reverse acc) +reduce [] acc = concat (reverse acc) reduce (MkToken _ _ _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc) where -- Preserve the original document's line count. blank_content : String - blank_content = fastAppend (replicate (length (lines x)) "\n") + blank_content = concat (replicate (length (lines x)) "\n") reduce (MkToken _ _ _ _ (CodeLine m src) :: rest) acc = if m == trim src diff --git a/TinyIdris-v1/src/Text/Parser.idr b/TinyIdris-v1/src/Text/Parser.idr index 04852c6..85a4024 100644 --- a/TinyIdris-v1/src/Text/Parser.idr +++ b/TinyIdris-v1/src/Text/Parser.idr @@ -17,7 +17,7 @@ match : (Eq k, TokenKind k) => Grammar (Token k) True (TokType kind) match kind = terminal "Unrecognised input" $ \(Tok kind' text) => if kind' == kind - then Just $ tokValue kind text + then Just $ TokValue kind text else Nothing ||| Optionally parse a thing, with a default value if the grammar doesn't @@ -41,7 +41,7 @@ optional p = option Nothing (map Just p) ||| which option succeeded. If both would succeed, the left option ||| takes priority. export -choose : {c1, c2 : Bool} -> +choose : {c1, c2 : Bool} -> (l : Grammar tok c1 a) -> (r : Grammar tok c2 b) -> Grammar tok (c1 && c2) (Either a b) @@ -64,7 +64,7 @@ choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in ||| Try each grammar in a container until the first one succeeds. ||| Fails if the container is empty. export -choice : Foldable t => +choice : Foldable t => {c : Bool} -> t (Grammar tok c a) -> Grammar tok c a @@ -154,7 +154,7 @@ mutual (skip : Grammar tok True s) -> (p : Grammar tok c a) -> Grammar tok True a - afterSome skip p = do skip + afterSome skip p = do _ <- skip afterMany skip p ||| Parse zero or more instance of `skip` until `p` is encountered, diff --git a/TinyIdris-v1/src/Text/Parser/Core.idr b/TinyIdris-v1/src/Text/Parser/Core.idr index fdbf80c..4a6e8a8 100644 --- a/TinyIdris-v1/src/Text/Parser/Core.idr +++ b/TinyIdris-v1/src/Text/Parser/Core.idr @@ -67,7 +67,7 @@ join {c1 = True} p = SeqEat p id ||| Give two alternative grammars. If both consume, the combination is ||| guaranteed to consume. export %inline -(<|>) : {c1,c2 : Bool} -> +(<|>) : {c1,c2 : Bool} -> Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) -> Grammar tok (c1 && c2) ty @@ -119,6 +119,13 @@ export %inline Grammar tok (c1 || c2) b (*>) x y = map (const id) x <*> y +export %inline +(>>) : {c1,c2 : Bool} -> + Grammar tok c1 a -> + Grammar tok c2 b -> + Grammar tok (c1 || c2) b +(>>) x y = map (const id) x <*> y + ||| Produce a grammar that can parse a different type of token by providing a ||| function converting the new token type into the original one. export @@ -187,9 +194,9 @@ data ParseResult : Type -> Type -> Type where (val : ty) -> (more : List tok) -> ParseResult tok ty mutual - doParse : (commit : Bool) -> + doParse : (commit : Bool) -> (act : Grammar tok c ty) -> - (xs : List tok) -> + (xs : List tok) -> ParseResult tok ty doParse com (Empty val) xs = Res com val xs doParse com (Fail fatal str) [] = Failure com fatal str [] diff --git a/TinyIdris-v1/src/Text/Token.idr b/TinyIdris-v1/src/Text/Token.idr index 1327e8a..ede2ebd 100644 --- a/TinyIdris-v1/src/Text/Token.idr +++ b/TinyIdris-v1/src/Text/Token.idr @@ -18,23 +18,23 @@ module Text.Token ||| tokValue SKComma x = () ||| ``` public export -interface TokenKind (k : Type) where +interface TokenKind (0 k : Type) where ||| The type that a token of this kind converts to. TokType : k -> Type ||| Convert a recognised string into a value. The type is determined ||| by the kind of token. - tokValue : (kind : k) -> String -> TokType kind + TokValue : (kind : k) -> String -> TokType kind ||| A token of a particular kind and the text that was recognised. public export record Token k where constructor Tok - kind : k - text : String + Kind : k + Text : String ||| Get the value of a `Token k`. The resulting type depends upon ||| the kind of token. public export -value : TokenKind k => (t : Token k) -> TokType (kind t) -value (Tok k x) = tokValue k x +value : TokenKind kn => (t : Token kn) -> TokType (Kind t) +value (Tok k x) = TokValue k x diff --git a/TinyIdris-v2/src/Core/CaseBuilder.idr b/TinyIdris-v2/src/Core/CaseBuilder.idr index 41e2229..3a40f82 100644 --- a/TinyIdris-v2/src/Core/CaseBuilder.idr +++ b/TinyIdris-v2/src/Core/CaseBuilder.idr @@ -10,7 +10,7 @@ import Core.Value import Data.LengthMatch import Data.List -import Data.Strings +import Data.String import Decidable.Equality @@ -27,7 +27,7 @@ data ArgType : List Name -> Type where show (Stuck t) = "Stuck " ++ show t show Unknown = "Unknown" -record PatInfo (pvar : Name) (vars : List Name) where +record PatInfo (0 pvar : Name) (vars : List Name) where constructor MkInfo {idx : Nat} {name : Name} @@ -72,7 +72,7 @@ updatePats {todo = pvar :: ns} env (NBind _ (Pi _ farg) fsc) (p :: ps) Unknown => do defs <- get Ctxt empty <- clearDefs defs - pure (record { argType = Known !(quote empty env farg) } p + pure ({ argType := Known !(quote empty env farg) } p :: !(updatePats env !(fsc defs (toClosure env (Ref Bound pvar))) ps)) _ => pure (p :: ps) updatePats env nf (p :: ps) @@ -80,7 +80,7 @@ updatePats env nf (p :: ps) Unknown => do defs <- get Ctxt empty <- clearDefs defs - pure (record { argType = Stuck !(quote empty env nf) } p :: ps) + pure ({ argType := Stuck !(quote empty env nf) } p :: ps) _ => pure (p :: ps) substInPatInfo : {pvar, vars, todo : _} -> @@ -90,14 +90,14 @@ substInPatInfo : {pvar, vars, todo : _} -> Core (PatInfo pvar vars, NamedPats vars todo) substInPatInfo {pvar} {vars} n tm p ps = case argType p of - Known ty => pure (record { argType = Known (substName n tm ty) } p, ps) + Known ty => pure ({ argType := Known (substName n tm ty) } p, ps) Stuck fty => do defs <- get Ctxt empty <- clearDefs defs let env = mkEnv vars case !(nf defs env (substName n tm fty)) of NBind _ (Pi _ farg) fsc => - pure (record { argType = Known !(quote empty env farg) } p, + pure ({ argType := Known !(quote empty env farg) } p, !(updatePats env !(fsc defs (toClosure env (Ref Bound pvar))) ps)) @@ -115,12 +115,12 @@ substInPats n tm (p :: ps) = do (p', ps') <- substInPatInfo n tm p ps pure (p' :: !(substInPats n tm ps')) -getPat : {idx : Nat} -> +getPat : forall name. {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps -> PatInfo name ns getPat First (x :: xs) = x getPat (Later p) (x :: xs) = getPat p xs -dropPat : {idx : Nat} -> +dropPat : forall name. {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps -> NamedPats ns (dropVar ps el) dropPat First (x :: xs) = xs @@ -259,7 +259,6 @@ checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pa (Just Refl, Yes Refl) => ConMatch prf _ => NoMatch checkGroupMatch (CName x tag) ps _ = NoMatch -checkGroupMatch _ _ _ = NoMatch data PName : Type where @@ -305,7 +304,7 @@ newPats : (pargs : List Pat) -> LengthMatch pargs ns -> NamedPats vars ns newPats [] NilMatch rest = [] newPats (newpat :: xs) (ConsMatch w) (pi :: rest) - = record { pat = newpat} pi :: newPats xs w rest + = { pat := newpat} pi :: newPats xs w rest updateNames : List (Name, Pat) -> List (Name, Name) updateNames = mapMaybe update @@ -317,7 +316,7 @@ updateNames = mapMaybe update updatePatNames : List (Name, Name) -> NamedPats vars todo -> NamedPats vars todo updatePatNames _ [] = [] updatePatNames ns (pi :: ps) - = record { pat $= update } pi :: updatePatNames ns ps + = { pat $= update } pi :: updatePatNames ns ps where update : Pat -> Pat update (PCon n i a ps) = PCon n i a (map update ps) @@ -385,7 +384,7 @@ groupCons fn pvars cs = do gs' <- addConG n tag pargs pats rhs gs pure (g :: gs') - addGroup : {vars, todo, idx : _} -> + addGroup : forall name. {vars, todo, idx : _} -> Pat -> (0 p : IsVar name idx vars) -> NamedPats vars todo -> Term vars -> List (Group vars todo) -> @@ -522,11 +521,11 @@ pickNext {ps = q :: qs} fn npss _ => do (_ ** MkNVar var) <- pickNext fn (map tail npss) pure (_ ** MkNVar (Later var)) -moveFirst : {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps -> +moveFirst : forall name. {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps -> NamedPats ns (name :: dropVar ps el) moveFirst el nps = getPat el nps :: dropPat el nps -shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo -> +shuffleVars : forall name. {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo -> PatClause vars (name :: dropVar todo el) shuffleVars el (MkPatClause pvars lhs rhs) = MkPatClause pvars (moveFirst el lhs) rhs @@ -641,7 +640,7 @@ mutual pure (Just !(varRule fn vs fallthrough)) mixture fn {a} {todo} NoClauses err = pure err --- +-- mkPatClause : {auto c : Ref Ctxt Defs} -> Name -> diff --git a/TinyIdris-v2/src/Core/CaseTree.idr b/TinyIdris-v2/src/Core/CaseTree.idr index 0d0dd66..876b4a7 100644 --- a/TinyIdris-v2/src/Core/CaseTree.idr +++ b/TinyIdris-v2/src/Core/CaseTree.idr @@ -73,7 +73,7 @@ data Pat : Type where export Show Pat where - show (PCon n t a args) = show n ++ show (t, a) ++ show args + show (PCon n t a args) = assert_total $ show n ++ show (t, a) ++ show args show (PLoc n) = "{" ++ show n ++ "}" show _ = "_" diff --git a/TinyIdris-v2/src/Core/Core.idr b/TinyIdris-v2/src/Core/Core.idr index dfce5a7..6f53c81 100644 --- a/TinyIdris-v2/src/Core/Core.idr +++ b/TinyIdris-v2/src/Core/Core.idr @@ -111,6 +111,10 @@ export %inline Left err => pure (Left err) Right val => runCore (f val))) +export %inline +(>>) : Core a -> Core b -> Core b +(>>) f b = f >>= (\_ => b) + -- Applicative (specialised) export %inline pure : a -> Core a @@ -153,7 +157,7 @@ traverse f xs = traverse' f xs [] export traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b) -traverseList1 f (x :: xs) = [| f x :: traverse f xs |] +traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |] export traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b) @@ -174,7 +178,7 @@ traverse_ f (x :: xs) export traverseList1_ : (a -> Core b) -> List1 a -> Core () -traverseList1_ f (x :: xs) = do +traverseList1_ f (x ::: xs) = do f x traverse_ f xs diff --git a/TinyIdris-v2/src/Core/Env.idr b/TinyIdris-v2/src/Core/Env.idr index 83683c8..d1819f0 100644 --- a/TinyIdris-v2/src/Core/Env.idr +++ b/TinyIdris-v2/src/Core/Env.idr @@ -8,7 +8,7 @@ data Env : (tm : List Name -> Type) -> List Name -> Type where Nil : Env tm [] (::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars) -revOnto : (xs, vs : _) -> reverseOnto xs vs = reverse vs ++ xs +revOnto : (xs, vs : _) -> List.reverseOnto xs vs = reverse vs ++ xs revOnto xs [] = Refl revOnto xs (v :: vs) = rewrite revOnto (v :: xs) vs in @@ -28,7 +28,7 @@ revNs (v :: vs) ns -- in big environments -- Also reversing the names at the end saves significant time over concatenating -- when environments get fairly big. -getBinderUnder : Weaken tm => +getBinderUnder : {tm : _} -> Weaken tm => {vars : _} -> {idx : Nat} -> (ns : List Name) -> (0 p : IsVar x idx vars) -> Env tm vars -> @@ -39,7 +39,7 @@ getBinderUnder {idx = S k} {vars = v :: vs} ns (Later lp) (b :: env) = getBinderUnder (v :: ns) lp env export -getBinder : Weaken tm => +getBinder : {tm : _} -> Weaken tm => {vars : _} -> {idx : Nat} -> (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm vars) getBinder el env = getBinderUnder [] el env diff --git a/TinyIdris-v2/src/Core/Normalise.idr b/TinyIdris-v2/src/Core/Normalise.idr index 7fee171..38a8b7f 100644 --- a/TinyIdris-v2/src/Core/Normalise.idr +++ b/TinyIdris-v2/src/Core/Normalise.idr @@ -14,7 +14,7 @@ import Data.Vect -- part will only be constructed when needed, because it's in Core. public export data Glued : List Name -> Type where - MkGlue : Core (Term vars) -> + MkGlue : Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars export @@ -39,7 +39,7 @@ data CaseResult a = Result a | NoMatch -- case alternative didn't match anything | GotStuck -- alternative matched, but got stuck later - + -- So that we can call 'eval' with new defs evalTop : {free, vars : _} -> Defs -> Env Term free -> LocalEnv free vars -> @@ -75,7 +75,7 @@ parameters (defs : Defs) evalLocClosure env stk (MkClosure locs' env' tm') = eval env' locs' tm' stk - evalLocal : {free, vars : _} -> + evalLocal : forall name. {free, vars : _} -> Env Term free -> (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) -> Stack free -> diff --git a/TinyIdris-v2/src/Core/TT.idr b/TinyIdris-v2/src/Core/TT.idr index e8f4163..1a004b9 100644 --- a/TinyIdris-v2/src/Core/TT.idr +++ b/TinyIdris-v2/src/Core/TT.idr @@ -3,6 +3,15 @@ module Core.TT import Data.List import Decidable.Equality +import Deriving.Show + +%language ElabReflection + +%hide Reflection.TT.Name +%hide Reflection.TT.NameType +%hide Language.Reflection.TT.showSep +%hide Language.Reflection.TT.IsVar + -- In Idris2, this is defined in Core.Name public export data Name : Type where @@ -93,6 +102,10 @@ data PiInfo : Type where Implicit : PiInfo Explicit : PiInfo +%hint public export +impPiInfo : Show PiInfo +impPiInfo = %runElab derive + public export data Binder : Type -> Type where Lam : PiInfo -> ty -> Binder ty @@ -290,7 +303,7 @@ resolveNames vars tm = tm namespace SubstEnv public export data SubstEnv : List Name -> List Name -> Type where - Nil : SubstEnv [] vars + Nil : SubstEnv [] vars (::) : Term vars -> SubstEnv ds vars -> SubstEnv (d :: ds) vars @@ -311,7 +324,8 @@ namespace SubstEnv find {outer = x :: xs} (Later p) env = weaken (find p env) substEnv : {drop, vars, outer : _} -> - SubstEnv drop vars -> Term (outer ++ (drop ++ vars)) -> + SubstEnv drop vars -> + Term (outer ++ (drop ++ vars)) -> Term (outer ++ vars) substEnv env (Local _ prf) = find prf env @@ -458,9 +472,9 @@ nameAt : {vars : _} -> nameAt {vars = n :: ns} Z First = n nameAt {vars = n :: ns} (S k) (Later p) = nameAt k p -export +export {vars : _} -> Show (Term vars) where - show tm = let (fn, args) = getFnArgs tm in showApp fn args + show tm = let (fn, args) = getFnArgs tm in assert_total $ showApp fn args where showApp : {vars : _} -> Term vars -> List (Term vars) -> String showApp (Local {name} idx p) [] diff --git a/TinyIdris-v2/src/Core/Unify.idr b/TinyIdris-v2/src/Core/Unify.idr index 1399966..cfcad16 100644 --- a/TinyIdris-v2/src/Core/Unify.idr +++ b/TinyIdris-v2/src/Core/Unify.idr @@ -50,7 +50,7 @@ solvedHole = MkUnifyResult [] True ufail : String -> Core a ufail msg = throw (GenericMsg msg) -unifyArgs : (Unify tm, Quote tm) => +unifyArgs : {tm : _} -> (Unify tm, Quote tm) => {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -178,7 +178,7 @@ data IVars : List Name -> List Name -> Type where ICons : Maybe (Var newvars) -> IVars vs newvars -> IVars (v :: vs) newvars -Weaken (IVars vs) where +{vs : _} -> Weaken (IVars vs) where weaken INil = INil weaken (ICons Nothing ts) = ICons Nothing (weaken ts) weaken (ICons (Just t) ts) = ICons (Just (weaken t)) (weaken ts) @@ -208,11 +208,11 @@ instantiate {newvars} env mname mdef locs tm defs <- get Ctxt rhs <- mkDef locs INil tm ty - let newdef = record { definition = PMDef [] (STerm rhs) } mdef + let newdef = { definition := PMDef [] (STerm rhs) } mdef addDef mname newdef removeHole mname where - updateIVar : {v : Nat} -> + updateIVar : forall name. {v : Nat} -> forall vs, newvars . IVars vs newvars -> (0 p : IsVar name v newvars) -> Maybe (Var vs) updateIVar {v} (ICons Nothing rest) prf @@ -304,7 +304,7 @@ mutual empty <- clearDefs defs tm <- quote empty env tmnf case shrinkTerm tm submv of - Nothing => + Nothing => -- Not well scoped, but it might be if we -- normalise (TODO: Exercise) postpone env (NApp (NMeta n margs) fargs) tmnf @@ -326,7 +326,7 @@ mutual export Unify NF where -- If we have two pi binders, check the arguments and scope - unify env (NBind x b sc) (NBind x' b' sc') = ?unifyBinders + unify env (NBind x b sc) (NBind x' b' sc') = ?hhahaha -- Matching constructors, reduces the problem to unifying the arguments unify env nx@(NDCon n t a args) ny@(NDCon n' t' a' args') = if t == t' @@ -396,22 +396,22 @@ retryGuess n = do defs <- get Ctxt case !(lookupDef n defs) of Nothing => pure False - Just gdef => + Just gdef => case definition gdef of Guess tm cs => do cs' <- traverse retry cs let csAll = unionAll cs' case constraints csAll of [] => -- fine now, complete the definition - do let gdef = record { - definition = PMDef [] (STerm tm) + do let gdef = { + definition := PMDef [] (STerm tm) } gdef updateDef n (const gdef) pure True cs => -- still constraints, but might be new -- ones, so update the definition - do let gdef = record { - definition = Guess tm cs + do let gdef = { + definition := Guess tm cs } gdef updateDef n (const gdef) pure False diff --git a/TinyIdris-v2/src/Core/UnifyState.idr b/TinyIdris-v2/src/Core/UnifyState.idr index 81995a1..62ff8dc 100644 --- a/TinyIdris-v2/src/Core/UnifyState.idr +++ b/TinyIdris-v2/src/Core/UnifyState.idr @@ -49,7 +49,7 @@ resetNextVar : {auto u : Ref UST UState} -> Core () resetNextVar = do ust <- get UST - put UST (record { nextName = 0 } ust) + put UST ({ nextName := 0 } ust) -- Generate a global name based on the given root, in the current namespace export @@ -57,27 +57,27 @@ genName : {auto u : Ref UST UState} -> String -> Core Name genName str = do ust <- get UST - put UST (record { nextName $= (+1) } ust) + put UST ({ nextName $= (+1) } ust) pure (MN str (nextName ust)) addHoleName : {auto u : Ref UST UState} -> Name -> Core () addHoleName n = do ust <- get UST - put UST (record { holes $= insert n } ust) + put UST ({ holes $= insert n } ust) addGuessName : {auto u : Ref UST UState} -> Name -> Core () addGuessName n = do ust <- get UST - put UST (record { guesses $= insert n } ust) + put UST ({ guesses $= insert n } ust) export removeHole : {auto u : Ref UST UState} -> Name -> Core () removeHole n = do ust <- get UST - put UST (record { holes $= delete n } ust) + put UST ({ holes $= delete n } ust) export addConstraint : {auto u : Ref UST UState} -> @@ -85,8 +85,8 @@ addConstraint : {auto u : Ref UST UState} -> addConstraint constr = do ust <- get UST let cid = nextConstraint ust - put UST (record { constraints $= insert cid constr, - nextConstraint = cid+1 } ust) + put UST ({ constraints $= insert cid constr, + nextConstraint := cid+1 } ust) pure cid export @@ -94,7 +94,7 @@ deleteConstraint : {auto u : Ref UST UState} -> Int -> Core () deleteConstraint cid = do ust <- get UST - put UST (record { constraints $= delete cid } ust) + put UST ({ constraints $= delete cid } ust) -- Make a type which abstracts over an environment -- Don't include 'let' bindings, since they have a concrete value and @@ -118,7 +118,7 @@ mkConstantAppArgs {done} {vars = x :: xs} (b :: env) wkns Local (length wkns) (mkVar wkns) :: rewrite (appendAssociative wkns [x] (xs ++ done)) in rec where - mkVar : (wkns : List Name) -> + mkVar : forall name. (wkns : List Name) -> IsVar name (length wkns) (wkns ++ name :: vars ++ done) mkVar [] = First mkVar (w :: ws) = Later (mkVar ws) diff --git a/TinyIdris-v2/src/Core/Value.idr b/TinyIdris-v2/src/Core/Value.idr index b997615..70ddf90 100644 --- a/TinyIdris-v2/src/Core/Value.idr +++ b/TinyIdris-v2/src/Core/Value.idr @@ -20,7 +20,7 @@ mutual -- The head of a value: things you can apply arguments to public export data NHead : List Name -> Type where - NLocal : (idx : Nat) -> (0 p : IsVar name idx vars) -> + NLocal : forall name. (idx : Nat) -> (0 p : IsVar name idx vars) -> NHead vars NRef : NameType -> Name -> NHead vars NMeta : Name -> List (Closure vars) -> NHead vars diff --git a/TinyIdris-v2/src/Parser/Lexer/Package.idr b/TinyIdris-v2/src/Parser/Lexer/Package.idr index 1a063c7..31a32b5 100644 --- a/TinyIdris-v2/src/Parser/Lexer/Package.idr +++ b/TinyIdris-v2/src/Parser/Lexer/Package.idr @@ -6,7 +6,7 @@ import public Text.Parser import Data.List import Data.List1 -import Data.Strings +import Data.String import Data.String.Extra import Utils.String @@ -27,7 +27,7 @@ Show Token where show (Comment str) = "Comment: " ++ str show EndOfInput = "EndOfInput" show Equals = "Equals" - show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.toList dsid) + show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep (List1.forget dsid) show Separator = "Separator" show Space = "Space" show (StringLit s) = "StringLit: " ++ s @@ -50,7 +50,7 @@ rawTokens = ] where splitNamespace : String -> List1 String - splitNamespace = Data.Strings.split (== '.') + splitNamespace = Data.String.split (== '.') export lex : String -> Either (Int, Int, String) (List (TokenData Token)) diff --git a/TinyIdris-v2/src/Parser/Lexer/Source.idr b/TinyIdris-v2/src/Parser/Lexer/Source.idr index f2910cc..a8b8857 100644 --- a/TinyIdris-v2/src/Parser/Lexer/Source.idr +++ b/TinyIdris-v2/src/Parser/Lexer/Source.idr @@ -4,7 +4,7 @@ import public Parser.Lexer.Common import Data.List1 import Data.List -import Data.Strings +import Data.String import Data.String.Extra import Utils.Hex @@ -46,7 +46,7 @@ Show Token where -- Identifiers show (HoleIdent x) = "hole identifier " ++ x show (Ident x) = "identifier " ++ x - show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.toList $ reverse xs) + show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (List1.forget $ reverse xs) show (DotIdent x) = "dot+identifier " ++ x show (Symbol x) = "symbol " ++ x -- Comments @@ -222,7 +222,7 @@ rawTokens = else Ident x parseNamespace : String -> Token parseNamespace ns = case List1.reverse . split (== '.') $ ns of - [ident] => parseIdent ident + ident ::: [] => parseIdent ident ns => DotSepIdent ns export diff --git a/TinyIdris-v2/src/Parser/Rule/Package.idr b/TinyIdris-v2/src/Parser/Rule/Package.idr index 643d4b5..2fbbaee 100644 --- a/TinyIdris-v2/src/Parser/Rule/Package.idr +++ b/TinyIdris-v2/src/Parser/Rule/Package.idr @@ -34,7 +34,7 @@ export exactProperty : String -> Rule String exactProperty p = terminal ("Expected property " ++ p) (\x => case tok x of - DotSepIdent [p'] => + DotSepIdent (p' ::: []) => if p == p' then Just p else Nothing _ => Nothing) @@ -64,7 +64,7 @@ export packageName : Rule String packageName = terminal "Expected package name" (\x => case tok x of - DotSepIdent [str] => + DotSepIdent (str ::: []) => if isIdent AllowDashes str then Just str else Nothing _ => Nothing) diff --git a/TinyIdris-v2/src/Parser/Rule/Source.idr b/TinyIdris-v2/src/Parser/Rule/Source.idr index 63b721e..491adc0 100644 --- a/TinyIdris-v2/src/Parser/Rule/Source.idr +++ b/TinyIdris-v2/src/Parser/Rule/Source.idr @@ -6,7 +6,7 @@ import public Parser.Support import Core.TT import Data.List1 -import Data.Strings +import Data.String %default total @@ -20,9 +20,7 @@ SourceEmptyRule = EmptyRule Token export eoi : SourceEmptyRule () -eoi - = do nextIs "Expected end of input" (isEOI . tok) - pure () +eoi = ignore $ nextIs "Expected end of input" (isEOI . tok) where isEOI : Token -> Bool isEOI EndInput = True @@ -124,7 +122,7 @@ namespacedIdent = terminal "Expected namespaced name" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just [i] + Ident i => Just (i ::: []) _ => Nothing) export @@ -133,7 +131,7 @@ moduleIdent = terminal "Expected module identifier" (\x => case tok x of DotSepIdent ns => Just ns - Ident i => Just [i] + Ident i => Just (i ::: []) _ => Nothing) export diff --git a/TinyIdris-v2/src/Parser/Support.idr b/TinyIdris-v2/src/Parser/Support.idr index 72d74a4..4edb21d 100644 --- a/TinyIdris-v2/src/Parser/Support.idr +++ b/TinyIdris-v2/src/Parser/Support.idr @@ -12,14 +12,14 @@ import System.File %default total public export -data ParseError tok - = ParseFail String (Maybe (Int, Int)) (List tok) +data ParseError tkn + = ParseFail String (Maybe (Int, Int)) (List tkn) | LexFail (Int, Int, String) | FileFail FileError | LitFail LiterateError export -Show tok => Show (ParseError tok) where +Show tkn => Show (ParseError tkn) where show (ParseFail err loc toks) = "Parse error: " ++ err ++ " (next tokens: " ++ show (take 10 toks) ++ ")" diff --git a/TinyIdris-v2/src/Parser/Unlit.idr b/TinyIdris-v2/src/Parser/Unlit.idr index e0ca498..fcd80f0 100644 --- a/TinyIdris-v2/src/Parser/Unlit.idr +++ b/TinyIdris-v2/src/Parser/Unlit.idr @@ -1,7 +1,7 @@ module Parser.Unlit import public Text.Literate -import Data.Strings +import Data.String %default total diff --git a/TinyIdris-v2/src/TTImp/Parser.idr b/TinyIdris-v2/src/TTImp/Parser.idr index 9748001..cf45d60 100644 --- a/TinyIdris-v2/src/TTImp/Parser.idr +++ b/TinyIdris-v2/src/TTImp/Parser.idr @@ -10,7 +10,7 @@ import public Text.Parser import Data.List import Data.List.Views import Data.List1 -import Data.Strings +import Data.String import Debug.Trace @@ -137,13 +137,13 @@ mutual forall_ : FileName -> IndentInfo -> Rule RawImp forall_ fname indents - = do keyword "forall" - commit - ns <- sepBy1 (symbol ",") unqualifiedName - let binders = map (\n => (Just (UN n), Implicit)) ns - symbol "." - scope <- typeExpr fname indents - pure (pibindAll Implicit binders scope) + = Core.do keyword "forall" + commit + ns <- sepBy1 (symbol ",") unqualifiedName + let binders = map (\n => (Just (UN n), Implicit)) ns + symbol "." + scope <- typeExpr fname indents + pure (pibindAll Implicit binders scope) implicitPi : FileName -> IndentInfo -> Rule RawImp implicitPi fname indents diff --git a/TinyIdris-v2/src/TTImp/ProcessDef.idr b/TinyIdris-v2/src/TTImp/ProcessDef.idr index 9d33c68..fec7d2c 100644 --- a/TinyIdris-v2/src/TTImp/ProcessDef.idr +++ b/TinyIdris-v2/src/TTImp/ProcessDef.idr @@ -30,7 +30,7 @@ processClause : {auto c : Ref Ctxt Defs} -> processClause (PatClause lhs rhs) = do -- Check the LHS (lhstm, lhsty) <- checkTerm [] lhs Nothing - -- Get the pattern variables from the LHS, and the expected type, + -- Get the pattern variables from the LHS, and the expected type, -- and check the RHS in that context (vars ** (env, lhsenv, rhsexp)) <- @@ -53,5 +53,5 @@ processDef n clauses (args ** tree) <- getPMDef n (type gdef) chkcs -- Update the definition with the compiled tree - updateDef n (record { definition = PMDef args tree }) + updateDef n ({ definition := PMDef args tree }) coreLift $ putStrLn $ "Processed " ++ show n diff --git a/TinyIdris-v2/src/TTImp/TTImp.idr b/TinyIdris-v2/src/TTImp/TTImp.idr index 0a073fb..a77caba 100644 --- a/TinyIdris-v2/src/TTImp/TTImp.idr +++ b/TinyIdris-v2/src/TTImp/TTImp.idr @@ -2,6 +2,12 @@ module TTImp.TTImp import Core.TT +import Deriving.Show + +%hide Reflection.TT.Name + +%language ElabReflection + public export data RawImp : Type where IVar : Name -> RawImp @@ -17,20 +23,34 @@ data RawImp : Type where Implicit : RawImp IType : RawImp +%hint export +impRawImp : Show RawImp +impRawImp = %runElab derive + public export data ImpTy : Type where MkImpTy : (n : Name) -> (ty : RawImp) -> ImpTy +%hint export +impTy : Show ImpTy +impTy = %runElab derive + public export data ImpClause : Type where PatClause : (lhs : RawImp) -> (rhs : RawImp) -> ImpClause +%hint export +impClause : Show ImpClause +impClause = %runElab derive public export data ImpData : Type where - MkImpData : (n : Name) -> + MkImpData : (n : Name) -> (tycon : RawImp) -> -- type constructor type (datacons : List ImpTy) -> -- constructor type declarations ImpData +%hint export +impData : Show ImpData +impData = %runElab derive public export data ImpDecl : Type where @@ -38,6 +58,10 @@ data ImpDecl : Type where IData : ImpData -> ImpDecl IDef : Name -> List ImpClause -> ImpDecl +%hint export +impShow : Show ImpDecl +impShow = %runElab derive + export apply : RawImp -> List RawImp -> RawImp apply f [] = f diff --git a/TinyIdris-v2/src/Text/Lexer/Core.idr b/TinyIdris-v2/src/Text/Lexer/Core.idr index ff145fb..437c4ed 100644 --- a/TinyIdris-v2/src/Text/Lexer/Core.idr +++ b/TinyIdris-v2/src/Text/Lexer/Core.idr @@ -5,7 +5,7 @@ import Data.Bool.Extra import Data.List import Data.Maybe import Data.Nat -import Data.Strings +import Data.String %default total diff --git a/TinyIdris-v2/src/Text/Literate.idr b/TinyIdris-v2/src/Text/Literate.idr index 557fb12..6dc781c 100644 --- a/TinyIdris-v2/src/Text/Literate.idr +++ b/TinyIdris-v2/src/Text/Literate.idr @@ -27,7 +27,7 @@ import Text.Lexer import Data.List import Data.List.Views -import Data.Strings +import Data.String %default total @@ -63,12 +63,12 @@ rawTokens delims ls = ||| Merge the tokens into a single source file. reduce : List (TokenData Token) -> List String -> String -reduce [] acc = fastAppend (reverse acc) +reduce [] acc = fastConcat (reverse acc) reduce (MkToken _ _ _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc) where -- Preserve the original document's line count. blank_content : String - blank_content = fastAppend (replicate (length (lines x)) "\n") + blank_content = fastConcat (replicate (length (lines x)) "\n") reduce (MkToken _ _ _ _ (CodeLine m src) :: rest) acc = if m == trim src diff --git a/TinyIdris-v2/src/Text/Parser.idr b/TinyIdris-v2/src/Text/Parser.idr index 04852c6..3df6381 100644 --- a/TinyIdris-v2/src/Text/Parser.idr +++ b/TinyIdris-v2/src/Text/Parser.idr @@ -12,7 +12,7 @@ import public Text.Token ||| Parse a terminal based on a kind of token. export -match : (Eq k, TokenKind k) => +match : {k : _} -> (Eq k, TokenKind k) => (kind : k) -> Grammar (Token k) True (TokType kind) match kind = terminal "Unrecognised input" $ @@ -41,7 +41,7 @@ optional p = option Nothing (map Just p) ||| which option succeeded. If both would succeed, the left option ||| takes priority. export -choose : {c1, c2 : Bool} -> +choose : {c1, c2 : Bool} -> (l : Grammar tok c1 a) -> (r : Grammar tok c2 b) -> Grammar tok (c1 && c2) (Either a b) @@ -64,7 +64,7 @@ choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in ||| Try each grammar in a container until the first one succeeds. ||| Fails if the container is empty. export -choice : Foldable t => +choice : Foldable t => {c : Bool} -> t (Grammar tok c a) -> Grammar tok c a @@ -154,7 +154,7 @@ mutual (skip : Grammar tok True s) -> (p : Grammar tok c a) -> Grammar tok True a - afterSome skip p = do skip + afterSome skip p = do _ <- skip afterMany skip p ||| Parse zero or more instance of `skip` until `p` is encountered, diff --git a/TinyIdris-v2/src/Text/Parser/Core.idr b/TinyIdris-v2/src/Text/Parser/Core.idr index fdbf80c..de0edee 100644 --- a/TinyIdris-v2/src/Text/Parser/Core.idr +++ b/TinyIdris-v2/src/Text/Parser/Core.idr @@ -67,7 +67,7 @@ join {c1 = True} p = SeqEat p id ||| Give two alternative grammars. If both consume, the combination is ||| guaranteed to consume. export %inline -(<|>) : {c1,c2 : Bool} -> +(<|>) : {c1,c2 : Bool} -> Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) -> Grammar tok (c1 && c2) ty @@ -119,6 +119,14 @@ export %inline Grammar tok (c1 || c2) b (*>) x y = map (const id) x <*> y +export %inline +(>>) : {c1, c2 : Bool} -> + Grammar tok c1 a -> + Grammar tok c2 b -> + Grammar tok (c1 || c2) b +(>>) f g {c1 = True} = f >>= (\_ => g) +(>>) f g {c1 = False} = f >>= (\_ => g) + ||| Produce a grammar that can parse a different type of token by providing a ||| function converting the new token type into the original one. export @@ -134,6 +142,10 @@ mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x)) mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y) +export %inline +ignore : {c : _} -> Grammar b c ty -> Grammar b c () +ignore g = map (const ()) g + ||| Always succeed with the given value. export %inline pure : (val : ty) -> Grammar tok False ty @@ -187,9 +199,9 @@ data ParseResult : Type -> Type -> Type where (val : ty) -> (more : List tok) -> ParseResult tok ty mutual - doParse : (commit : Bool) -> + doParse : (commit : Bool) -> (act : Grammar tok c ty) -> - (xs : List tok) -> + (xs : List tok) -> ParseResult tok ty doParse com (Empty val) xs = Res com val xs doParse com (Fail fatal str) [] = Failure com fatal str [] diff --git a/TinyIdris-v2/src/Text/Token.idr b/TinyIdris-v2/src/Text/Token.idr index 1327e8a..492f62c 100644 --- a/TinyIdris-v2/src/Text/Token.idr +++ b/TinyIdris-v2/src/Text/Token.idr @@ -36,5 +36,5 @@ record Token k where ||| Get the value of a `Token k`. The resulting type depends upon ||| the kind of token. public export -value : TokenKind k => (t : Token k) -> TokType (kind t) +value : {k : _} -> TokenKind k => (t : Token k) -> TokType (kind t) value (Tok k x) = tokValue k x