diff --git a/idris2.ipkg b/idris2.ipkg new file mode 100644 index 000000000..29185a67f --- /dev/null +++ b/idris2.ipkg @@ -0,0 +1,147 @@ +package idris2 + +modules = +-- Algebra, + Algebra.Preorder +-- Algebra.Semiring, +-- Algebra.ZeroOneOmega, + +-- Compiler.ANF, +-- Compiler.Common, +-- Compiler.CompileExpr, +-- Compiler.Inline, +-- Compiler.LambdaLift, +-- Compiler.Scheme.Chez, +-- Compiler.Scheme.Racket, +-- Compiler.Scheme.Gambit, +-- Compiler.Scheme.Common, +-- Compiler.VMCode, +-- +-- Control.Delayed, +-- +-- Core.AutoSearch, +-- Core.Binary, +-- Core.CaseBuilder, +-- Core.CaseTree, +-- Core.Context, +-- Core.CompileExpr, +-- Core.Core, +-- Core.Coverage, +-- Core.Directory, +-- Core.Env, +-- Core.FC, +-- Core.GetType, +-- Core.Hash, +-- Core.LinearCheck, +-- Core.Metadata, +-- Core.Name, +-- Core.Normalise, +-- Core.Options, +-- -- Core.Reflect, +-- Core.Termination, +-- Core.TT, +-- Core.TTC, +-- Core.Unify, +-- Core.UnifyState, +-- Core.Value, +-- +-- Data.ANameMap, +-- Data.Bool.Extra, +-- Data.IntMap, +-- Data.IOArray, +-- Data.NameMap, +-- Data.StringMap, +-- Data.These, +-- Data.StringTrie, +-- +-- Idris.CommandLine, +-- Idris.Desugar, +-- Idris.Elab.Implementation, +-- Idris.Elab.Interface, +-- Idris.Error, +-- Idris.IDEMode.CaseSplit, +-- Idris.IDEMode.Commands, +-- Idris.IDEMode.MakeClause, +-- Idris.IDEMode.Parser, +-- Idris.IDEMode.REPL, +-- Idris.IDEMode.TokenLine, +-- Idris.ModTree, +-- Idris.Package, +-- Idris.Parser, +-- Idris.ProcessIdr, +-- Idris.REPL, +-- Idris.REPLCommon, +-- Idris.REPLOpts, +-- Idris.Resugar, +-- Idris.SetOptions, +-- Idris.Socket, +-- Idris.Socket.Data, +-- Idris.Socket.Raw, +-- Idris.Syntax, +-- Idris.Version, +-- +-- Parser.Lexer, +-- Parser.Support, +-- Parser.Unlit, +-- +-- Text.Lexer, +-- Text.Lexer.Core, +-- Text.Literate, +-- Text.Parser, +-- Text.Parser.Core, +-- Text.Quantity, +-- Text.Token, +-- +-- TTImp.BindImplicits, +-- TTImp.Elab, +-- TTImp.Elab.Ambiguity, +-- TTImp.Elab.App, +-- TTImp.Elab.As, +-- TTImp.Elab.Binders, +-- TTImp.Elab.Case, +-- TTImp.Elab.Check, +-- TTImp.Elab.Dot, +-- TTImp.Elab.Hole, +-- TTImp.Elab.ImplicitBind, +-- TTImp.Elab.Lazy, +-- TTImp.Elab.Local, +-- TTImp.Elab.Prim, +-- -- TTImp.Elab.Quote, +-- TTImp.Elab.Record, +-- TTImp.Elab.Rewrite, +-- TTImp.Elab.Term, +-- TTImp.Elab.Utils, +-- TTImp.Impossible, +-- TTImp.Interactive.CaseSplit, +-- TTImp.Interactive.ExprSearch, +-- TTImp.Interactive.GenerateDef, +-- TTImp.Interactive.MakeLemma, +-- TTImp.Parser, +-- TTImp.PartialEval, +-- TTImp.ProcessData, +-- TTImp.ProcessDecls, +-- TTImp.ProcessDef, +-- TTImp.ProcessParams, +-- TTImp.ProcessRecord, +-- TTImp.ProcessTransform, +-- TTImp.ProcessType, +-- -- TTImp.Reflect, +-- TTImp.TTImp, +-- TTImp.Unelab, +-- TTImp.Utils, +-- TTImp.WithClause, +-- +-- Utils.Binary, +-- Utils.Hex, +-- Utils.Octal, +-- Utils.Shunting, +-- Utils.String, +-- +-- Yaffle.Main, +-- Yaffle.REPL + +depends = contrib + +sourcedir = "src" + +-- main = Idris.Main diff --git a/src/Core/Name.idr b/src/Core/Name.idr new file mode 100644 index 000000000..ad14e563f --- /dev/null +++ b/src/Core/Name.idr @@ -0,0 +1,202 @@ +module Core.Name + +import Data.List +import Decidable.Equality + +%default total + +public export +data Name : Type where + NS : List String -> Name -> Name -- in a namespace + UN : String -> Name -- user defined name + MN : String -> Int -> Name -- machine generated name + PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id + DN : String -> Name -> Name -- a name and how to display it + RF : String -> Name -- record field name + Nested : (Int, Int) -> Name -> Name -- nested function name + CaseBlock : Int -> Int -> Name -- case block nested in (resolved) name + WithBlock : Int -> Int -> Name -- with block nested in (resolved) name + Resolved : Int -> Name -- resolved, index into context + +export +userNameRoot : Name -> Maybe String +userNameRoot (NS _ n) = userNameRoot n +userNameRoot (UN n) = Just n +userNameRoot (DN _ n) = userNameRoot n +userNameRoot (RF n) = Just ("." ++ n) -- TMP HACK +userNameRoot _ = Nothing + +export +isUserName : Name -> Bool +isUserName (PV _ _) = False +isUserName (MN _ _) = False +isUserName (NS _ n) = isUserName n +isUserName (DN _ n) = isUserName n +isUserName _ = True + +export +nameRoot : Name -> String +nameRoot (NS _ n) = nameRoot n +nameRoot (UN n) = n +nameRoot (MN n _) = n +nameRoot (PV n _) = nameRoot n +nameRoot (DN _ n) = nameRoot n +nameRoot (RF n) = n +nameRoot (Nested _ inner) = nameRoot inner +nameRoot (CaseBlock n _) = "$" ++ show n +nameRoot (WithBlock n _) = "$" ++ show n +nameRoot (Resolved i) = "$" ++ show i + +--- Drop a namespace from a name +export +dropNS : Name -> Name +dropNS (NS _ n) = n +dropNS n = n + +export +showSep : String -> List String -> String +showSep sep [] = "" +showSep sep [x] = x +showSep sep (x :: xs) = x ++ sep ++ showSep sep xs + +export +Show Name where + show (NS ns n@(RF _)) = showSep "." (reverse ns) ++ ".(" ++ show n ++ ")" + show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n + show (UN x) = x + show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}" + show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}" + show (DN str n) = str + show (RF n) = "." ++ n + show (Nested (outer, idx) inner) + = show outer ++ ":" ++ show idx ++ ":" ++ show inner + show (CaseBlock outer i) = "case block in " ++ show outer ++ "(" ++ show i ++ ")" + show (WithBlock outer i) = "with block in " ++ show outer + show (Resolved x) = "$resolved" ++ show x + +export +Eq Name where + (==) (NS ns n) (NS ns' n') = n == n' && ns == ns' + (==) (UN x) (UN y) = x == y + (==) (MN x y) (MN x' y') = y == y' && x == x' + (==) (PV x y) (PV x' y') = x == x' && y == y' + (==) (DN _ n) (DN _ n') = n == n' + (==) (RF n) (RF n') = n == n' + (==) (Nested x y) (Nested x' y') = x == x' && y == y' + (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x' + (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x' + (==) (Resolved x) (Resolved x') = x == x' + (==) _ _ = False + +nameTag : Name -> Int +nameTag (NS _ _) = 0 +nameTag (UN _) = 1 +nameTag (MN _ _) = 2 +nameTag (PV _ _) = 3 +nameTag (DN _ _) = 4 +nameTag (RF _) = 5 +nameTag (Nested _ _) = 6 +nameTag (CaseBlock _ _) = 7 +nameTag (WithBlock _ _) = 8 +nameTag (Resolved _) = 9 + +export +Ord Name where + compare (NS x y) (NS x' y') + = case compare y y' of -- Compare base name first (more likely to differ) + EQ => compare x x' + -- Because of the terrible way Idris 1 compiles 'case', this + -- is actually faster than just having 't => t'... + GT => GT + LT => LT + compare (UN x) (UN y) = compare x y + compare (MN x y) (MN x' y') + = case compare y y' of + EQ => compare x x' + GT => GT + LT => LT + compare (PV x y) (PV x' y') + = case compare y y' of + EQ => compare x x' + GT => GT + LT => LT + compare (DN _ n) (DN _ n') = compare n n' + compare (RF n) (RF n') = compare n n' + compare (Nested x y) (Nested x' y') + = case compare y y' of + EQ => compare x x' + GT => GT + LT => LT + compare (CaseBlock x y) (CaseBlock x' y') + = case compare y y' of + EQ => compare x x' + GT => GT + LT => LT + compare (WithBlock x y) (WithBlock x' y') + = case compare y y' of + EQ => compare x x' + GT => GT + LT => LT + compare (Resolved x) (Resolved y) = compare x y + + compare x y = compare (nameTag x) (nameTag y) + +export +nameEq : (x : Name) -> (y : Name) -> Maybe (x = y) +nameEq (NS xs x) (NS ys y) with (decEq xs ys) + nameEq (NS ys x) (NS ys y) | (Yes Refl) with (nameEq x y) + nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing + nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl + nameEq (NS xs x) (NS ys y) | (No contra) = Nothing +nameEq (UN x) (UN y) with (decEq x y) + nameEq (UN y) (UN y) | (Yes Refl) = Just Refl + nameEq (UN x) (UN y) | (No contra) = Nothing +nameEq (MN x t) (MN x' t') with (decEq x x') + nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t') + nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl + nameEq (MN x t) (MN x t') | (Yes Refl) | (No contra) = Nothing + nameEq (MN x t) (MN x' t') | (No contra) = Nothing +nameEq (PV x t) (PV y t') with (nameEq x y) + nameEq (PV y t) (PV y t') | (Just Refl) with (decEq t t') + nameEq (PV y t) (PV y t) | (Just Refl) | (Yes Refl) = Just Refl + nameEq (PV y t) (PV y t') | (Just Refl) | (No p) = Nothing + nameEq (PV x t) (PV y t') | Nothing = Nothing +nameEq (DN x t) (DN y t') with (decEq x y) + nameEq (DN y t) (DN y t') | (Yes Refl) with (nameEq t t') + nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl + nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing + nameEq (DN x t) (DN y t') | (No p) = Nothing +nameEq (RF x) (RF y) with (decEq x y) + nameEq (RF y) (RF y) | (Yes Refl) = Just Refl + nameEq (RF x) (RF y) | (No contra) = Nothing +nameEq (Nested x y) (Nested x' y') with (decEq x x') + nameEq (Nested x y) (Nested x' y') | (No p) = Nothing + nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y') + nameEq (Nested x y) (Nested x y') | (Yes Refl) | Nothing = Nothing + nameEq (Nested x y) (Nested x y) | (Yes Refl) | (Just Refl) = Just Refl +nameEq (CaseBlock x y) (CaseBlock x' y') with (decEq x x') + nameEq (CaseBlock x y) (CaseBlock x' y') | (No p) = Nothing + nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) with (decEq y y') + nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) | (No p) = Nothing + nameEq (CaseBlock x y) (CaseBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl +nameEq (WithBlock x y) (WithBlock x' y') with (decEq x x') + nameEq (WithBlock x y) (WithBlock x' y') | (No p) = Nothing + nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) with (decEq y y') + nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) | (No p) = Nothing + nameEq (WithBlock x y) (WithBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl +nameEq (Resolved x) (Resolved y) with (decEq x y) + nameEq (Resolved y) (Resolved y) | (Yes Refl) = Just Refl + nameEq (Resolved x) (Resolved y) | (No contra) = Nothing +nameEq _ _ = Nothing + +export +namesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys) +namesEq [] [] = Just Refl +namesEq (x :: xs) (y :: ys) + = do p <- nameEq x y + ps <- namesEq xs ys + rewrite p + rewrite ps + Just Refl +namesEq _ _ = Nothing + diff --git a/src/Data/ANameMap.idr b/src/Data/ANameMap.idr new file mode 100644 index 000000000..193d5617b --- /dev/null +++ b/src/Data/ANameMap.idr @@ -0,0 +1,106 @@ +-- like name map, but able to return ambiguous names +module Data.ANameMap + +import Core.Name +import Data.NameMap +import Data.StringMap + +export +record ANameMap a where + constructor MkANameMap + -- for looking up by exact (completely qualified) names + exactNames : NameMap a + -- for looking up by name root or partially qualified (so possibly + -- ambiguous) names. This doesn't store machine generated names. + hierarchy : StringMap (List (Name, a)) + +export +empty : ANameMap a +empty = MkANameMap empty empty + +||| Given a Name, and an ANameMap, look up that name exactly +export +lookupExact : Name -> ANameMap a -> Maybe a +lookupExact n dict = lookup n (exactNames dict) + +export +lookupName : Name -> ANameMap a -> List (Name, a) +lookupName n dict + = case userNameRoot n of + Nothing => case lookupExact n dict of + Nothing => [] + Just res => [(n, res)] + Just r => case lookup r (hierarchy dict) of + Nothing => [] + Just ns => filter (matches n) ns + where + -- Name matches if a prefix of the namespace matches a prefix of the + -- namespace in the context + matches : Name -> (Name, a) -> Bool + matches (NS ns _) (NS cns _, _) = ns `isPrefixOf` cns + matches (NS _ _) _ = True -- no in library name, so root doesn't match + matches _ _ = True -- no prefix, so root must match, so good + +addToHier : Name -> a -> + StringMap (List (Name, a)) -> StringMap (List (Name, a)) +addToHier n val hier + -- Only add user defined names. Machine generated names can only be + -- found with the exactNames + = case userNameRoot n of + Nothing => hier + Just root => + case lookup root hier of + Nothing => insert root [(n, val)] hier + Just ns => insert root (update val ns) hier + where + update : a -> List (Name, a) -> List (Name, a) + update val [] = [(n, val)] + update val (old :: xs) + = if n == fst old + then (n, val) :: xs + else old :: update val xs + +export +addName : Name -> a -> ANameMap a -> ANameMap a +addName n val (MkANameMap dict hier) + = let dict' = insert n val dict + hier' = addToHier n val hier in + MkANameMap dict' hier' + +export +toList : ANameMap a -> List (Name, a) +toList dict = toList (exactNames dict) + +export +fromList : List (Name, a) -> ANameMap a +fromList = fromList' empty + where + fromList' : ANameMap a -> List (Name, a) -> ANameMap a + fromList' acc [] = acc + fromList' acc ((k, v) :: ns) = fromList' (addName k v acc) ns + +-- Merge two contexts, with entries in the second overriding entries in +-- the first +export +merge : ANameMap a -> ANameMap a -> ANameMap a +merge ctxt (MkANameMap exact hier) + = insertFrom (toList exact) ctxt + where + insertFrom : List (Name, a) -> ANameMap a -> ANameMap a + insertFrom [] ctxt = ctxt + insertFrom ((n, val) :: cs) ctxt + = insertFrom cs (addName n val ctxt) + +-- TODO: Update namespaces so 'as' works +export +mergeAs : List String -> List String -> + ANameMap a -> ANameMap a -> ANameMap a +mergeAs oldns newns ctxt (MkANameMap exact hier) + = insertFrom (toList exact) ctxt + where + insertFrom : List (Name, a) -> ANameMap a -> ANameMap a + insertFrom [] ctxt = ctxt + insertFrom ((n, val) :: cs) ctxt + = insertFrom cs (addName n val ctxt) + + diff --git a/src/Data/Bool/Extra.idr b/src/Data/Bool/Extra.idr new file mode 100644 index 000000000..95f31a97e --- /dev/null +++ b/src/Data/Bool/Extra.idr @@ -0,0 +1,46 @@ +module Data.Bool.Extra + +public export +andSameNeutral : (x : Bool) -> x && x = x +andSameNeutral False = Refl +andSameNeutral True = Refl + +public export +andFalseFalse : (x : Bool) -> x && False = False +andFalseFalse False = Refl +andFalseFalse True = Refl + +public export +andTrueNeutral : (x : Bool) -> x && True = x +andTrueNeutral False = Refl +andTrueNeutral True = Refl + +public export +orSameNeutral : (x : Bool) -> x || x = x +orSameNeutral False = Refl +orSameNeutral True = Refl + +public export +orFalseNeutral : (x : Bool) -> x || False = x +orFalseNeutral False = Refl +orFalseNeutral True = Refl + +public export +orTrueTrue : (x : Bool) -> x || True = True +orTrueTrue False = Refl +orTrueTrue True = Refl + +public export +orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x +orSameAndRightNeutral False _ = Refl +orSameAndRightNeutral True _ = Refl + +export +anyTrue : List Bool -> Bool +anyTrue [] = False +anyTrue (x :: xs) = x || anyTrue xs + +export +allTrue : List Bool -> Bool +allTrue [] = True +allTrue (x :: xs) = x && allTrue xs diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr new file mode 100644 index 000000000..2c7e2af16 --- /dev/null +++ b/src/Parser/Support.idr @@ -0,0 +1,616 @@ +module Parser.Support + +import public Text.Lexer +import public Parser.Lexer +import public Parser.Unlit +import public Text.Parser + +import Core.TT +import Data.List +import Data.List.Views +import System.File + +%default total + +public export +Rule : Type -> Type +Rule ty = Grammar (TokenData Token) True ty + +public export +EmptyRule : Type -> Type +EmptyRule ty = Grammar (TokenData Token) False ty + +public export +data ParseError = ParseFail String (Maybe (Int, Int)) (List Token) + | LexFail (Int, Int, String) + | FileFail FileError + | LitFail LiterateError + +export +Show ParseError where + show (ParseFail err loc toks) + = "Parse error: " ++ err ++ " (next tokens: " + ++ show (take 10 toks) ++ ")" + show (LexFail (c, l, str)) + = "Lex error at " ++ show (c, l) ++ " input: " ++ str + show (FileFail err) + = "File error: " ++ show err + show (LitFail (MkLitErr l c str)) + = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str + +export +eoi : EmptyRule () +eoi + = do nextIs "Expected end of input" (isEOI . tok) + pure () + where + isEOI : Token -> Bool + isEOI EndInput = True + isEOI _ = False + +export +runParserTo : {e : _} -> + Maybe LiterateStyle -> (TokenData Token -> Bool) -> + String -> Grammar (TokenData Token) e ty -> Either ParseError ty +runParserTo lit pred str p + = case unlit lit str of + Left l => Left $ LitFail l + Right str => + case lexTo pred str of + Left err => Left $ LexFail err + Right toks => + case parse p toks of + Left (Error err []) => + Left $ ParseFail err Nothing [] + Left (Error err (t :: ts)) => + Left $ ParseFail err (Just (line t, col t)) + (map tok (t :: ts)) + Right (val, _) => Right val + +export +runParser : {e : _} -> + Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty +runParser lit = runParserTo lit (const False) + +export +parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty) +parseFile fn p + = do Right str <- readFile fn + | Left err => pure (Left (FileFail err)) + pure (runParser (isLitFile fn) str p) + + +-- Some basic parsers used by all the intermediate forms + +export +location : EmptyRule (Int, Int) +location + = do tok <- peek + pure (line tok, col tok) + +export +column : EmptyRule Int +column + = do (line, col) <- location + pure col + +hex : Char -> Maybe Int +hex '0' = Just 0 +hex '1' = Just 1 +hex '2' = Just 2 +hex '3' = Just 3 +hex '4' = Just 4 +hex '5' = Just 5 +hex '6' = Just 6 +hex '7' = Just 7 +hex '8' = Just 8 +hex '9' = Just 9 +hex 'a' = Just 10 +hex 'b' = Just 11 +hex 'c' = Just 12 +hex 'd' = Just 13 +hex 'e' = Just 14 +hex 'f' = Just 15 +hex _ = Nothing + +dec : Char -> Maybe Int +dec '0' = Just 0 +dec '1' = Just 1 +dec '2' = Just 2 +dec '3' = Just 3 +dec '4' = Just 4 +dec '5' = Just 5 +dec '6' = Just 6 +dec '7' = Just 7 +dec '8' = Just 8 +dec '9' = Just 9 +dec _ = Nothing + +oct : Char -> Maybe Int +oct '0' = Just 0 +oct '1' = Just 1 +oct '2' = Just 2 +oct '3' = Just 3 +oct '4' = Just 4 +oct '5' = Just 5 +oct '6' = Just 6 +oct '7' = Just 7 +oct _ = Nothing + +getEsc : String -> Maybe Char +getEsc "NUL" = Just '\NUL' +getEsc "SOH" = Just '\SOH' +getEsc "STX" = Just '\STX' +getEsc "ETX" = Just '\ETX' +getEsc "EOT" = Just '\EOT' +getEsc "ENQ" = Just '\ENQ' +getEsc "ACK" = Just '\ACK' +getEsc "BEL" = Just '\BEL' +getEsc "BS" = Just '\BS' +getEsc "HT" = Just '\HT' +getEsc "LF" = Just '\LF' +getEsc "VT" = Just '\VT' +getEsc "FF" = Just '\FF' +getEsc "CR" = Just '\CR' +getEsc "SO" = Just '\SO' +getEsc "SI" = Just '\SI' +getEsc "DLE" = Just '\DLE' +getEsc "DC1" = Just '\DC1' +getEsc "DC2" = Just '\DC2' +getEsc "DC3" = Just '\DC3' +getEsc "DC4" = Just '\DC4' +getEsc "NAK" = Just '\NAK' +getEsc "SYN" = Just '\SYN' +getEsc "ETB" = Just '\ETB' +getEsc "CAN" = Just '\CAN' +getEsc "EM" = Just '\EM' +getEsc "SUB" = Just '\SUB' +getEsc "ESC" = Just '\ESC' +getEsc "FS" = Just '\FS' +getEsc "GS" = Just '\GS' +getEsc "RS" = Just '\RS' +getEsc "US" = Just '\US' +getEsc "SP" = Just '\SP' +getEsc "DEL" = Just '\DEL' +getEsc str = Nothing + +escape' : List Char -> Maybe (List Char) +escape' [] = pure [] +escape' ('\\' :: '\\' :: xs) = pure $ '\\' :: !(escape' xs) +escape' ('\\' :: '&' :: xs) = pure !(escape' xs) +escape' ('\\' :: 'a' :: xs) = pure $ '\a' :: !(escape' xs) +escape' ('\\' :: 'b' :: xs) = pure $ '\b' :: !(escape' xs) +escape' ('\\' :: 'f' :: xs) = pure $ '\f' :: !(escape' xs) +escape' ('\\' :: 'n' :: xs) = pure $ '\n' :: !(escape' xs) +escape' ('\\' :: 'r' :: xs) = pure $ '\r' :: !(escape' xs) +escape' ('\\' :: 't' :: xs) = pure $ '\t' :: !(escape' xs) +escape' ('\\' :: 'v' :: xs) = pure $ '\v' :: !(escape' xs) +escape' ('\\' :: '\'' :: xs) = pure $ '\'' :: !(escape' xs) +escape' ('\\' :: '\"' :: xs) = pure $ '\"' :: !(escape' xs) +escape' ('\\' :: 'x' :: xs) + = case span isHexDigit xs of + ([], rest) => assert_total (escape' rest) + (ds, rest) => pure $ cast !(toHex 1 (reverse ds)) :: + !(assert_total (escape' rest)) + where + toHex : Int -> List Char -> Maybe Int + toHex _ [] = Just 0 + toHex m (d :: ds) + = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds) +escape' ('\\' :: 'o' :: xs) + = case span isOctDigit xs of + ([], rest) => assert_total (escape' rest) + (ds, rest) => pure $ cast !(toOct 1 (reverse ds)) :: + !(assert_total (escape' rest)) + where + toOct : Int -> List Char -> Maybe Int + toOct _ [] = Just 0 + toOct m (d :: ds) + = pure $ !(oct (toLower d)) * m + !(toOct (m*8) ds) +escape' ('\\' :: xs) + = case span isDigit xs of + ([], (a :: b :: c :: rest)) => + case getEsc (pack (the (List _) [a, b, c])) of + Just v => Just (v :: !(assert_total (escape' rest))) + Nothing => case getEsc (pack (the (List _) [a, b])) of + Just v => Just (v :: !(assert_total (escape' (c :: rest)))) + Nothing => escape' xs + ([], (a :: b :: [])) => + case getEsc (pack (the (List _) [a, b])) of + Just v => Just (v :: []) + Nothing => escape' xs + ([], rest) => assert_total (escape' rest) + (ds, rest) => Just $ cast (cast {to=Int} (pack ds)) :: + !(assert_total (escape' rest)) +escape' (x :: xs) = Just $ x :: !(escape' xs) + +escape : String -> Maybe String +escape x = pure $ pack !(escape' (unpack x)) + +getCharLit : String -> Maybe Char +getCharLit str + = do e <- escape str + if length e == 1 + then Just (assert_total (prim__strHead e)) + else if length e == 0 -- parsed the NULL character that terminated the string! + then Just '\0000' + else Nothing + +export +constant : Rule Constant +constant + = terminal "Expected constant" + (\x => case tok x of + Literal i => Just (BI i) + StrLit s => case escape s of + Nothing => Nothing + Just s' => Just (Str s') + CharLit c => case getCharLit c of + Nothing => Nothing + Just c' => Just (Ch c') + DoubleLit d => Just (Db d) + NSIdent ["Int"] => Just IntType + NSIdent ["Integer"] => Just IntegerType + NSIdent ["String"] => Just StringType + NSIdent ["Char"] => Just CharType + NSIdent ["Double"] => Just DoubleType + _ => Nothing) + +export +intLit : Rule Integer +intLit + = terminal "Expected integer literal" + (\x => case tok x of + Literal i => Just i + _ => Nothing) + +export +strLit : Rule String +strLit + = terminal "Expected string literal" + (\x => case tok x of + StrLit s => Just s + _ => Nothing) + +export +recField : Rule Name +recField + = terminal "Expected record field" + (\x => case tok x of + RecordField s => Just (RF s) + _ => Nothing) + +export +symbol : String -> Rule () +symbol req + = terminal ("Expected '" ++ req ++ "'") + (\x => case tok x of + Symbol s => if s == req then Just () + else Nothing + _ => Nothing) + +export +keyword : String -> Rule () +keyword req + = terminal ("Expected '" ++ req ++ "'") + (\x => case tok x of + Keyword s => if s == req then Just () + else Nothing + _ => Nothing) + +export +exactIdent : String -> Rule () +exactIdent req + = terminal ("Expected " ++ req) + (\x => case tok x of + NSIdent [s] => if s == req then Just () + else Nothing + _ => Nothing) + +export +pragma : String -> Rule () +pragma n = + terminal ("Expected pragma " ++ n) + (\x => case tok x of + Pragma s => + if s == n + then Just () + else Nothing + _ => Nothing) + +export +operator : Rule Name +operator + = terminal "Expected operator" + (\x => case tok x of + Symbol s => + if s `elem` reservedSymbols + then Nothing + else Just (UN s) + _ => Nothing) + +identPart : Rule String +identPart + = terminal "Expected name" + (\x => case tok x of + NSIdent [str] => Just str + _ => Nothing) + +%hide Prelude.(>>=) + +export +nsIdent : Rule (List String) +nsIdent + = terminal "Expected namespaced name" + (\x => case tok x of + NSIdent ns => Just ns + _ => Nothing) + +export +unqualifiedName : Rule String +unqualifiedName = identPart + +export +holeName : Rule String +holeName + = terminal "Expected hole name" + (\x => case tok x of + HoleIdent str => Just str + _ => Nothing) + +reservedNames : List String +reservedNames + = ["Type", "Int", "Integer", "String", "Char", "Double", + "Lazy", "Inf", "Force", "Delay"] + +export +name : Rule Name +name = opNonNS <|> do + ns <- nsIdent + opNS ns <|> nameNS ns + where + reserved : String -> Bool + reserved n = n `elem` reservedNames + + nameNS : List String -> Grammar (TokenData Token) False Name + nameNS [] = pure $ UN "IMPOSSIBLE" + nameNS [x] = + if reserved x + then fail $ "can't use reserved name " ++ x + else pure $ UN x + nameNS (x :: xs) = + if reserved x + then fail $ "can't use reserved name " ++ x + else pure $ NS xs (UN x) + + opNonNS : Rule Name + opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")" + + opNS : List String -> Rule Name + opNS ns = do + symbol ".(" + n <- (operator <|> recField) + symbol ")" + pure (NS ns n) + +export +IndentInfo : Type +IndentInfo = Int + +export +init : IndentInfo +init = 0 + +%hide Prelude.pure + +continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule () +continueF err indent + = do eoi; err + <|> do keyword "where"; err + <|> do col <- Support.column + if col <= indent + then err + else pure () + +||| Fail if this is the end of a block entry or end of file +export +continue : (indent : IndentInfo) -> EmptyRule () +continue = continueF (fail "Unexpected end of expression") + +||| As 'continue' but failing is fatal (i.e. entire parse fails) +export +mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule () +mustContinue indent Nothing + = continueF (fatalError "Unexpected end of expression") indent +mustContinue indent (Just req) + = continueF (fatalError ("Expected '" ++ req ++ "'")) indent + +data ValidIndent = + ||| In {}, entries can begin in any column + AnyIndent | + ||| Entry must begin in a specific column + AtPos Int | + ||| Entry can begin in this column or later + AfterPos Int | + ||| Block is finished + EndOfBlock + +Show ValidIndent where + show AnyIndent = "[any]" + show (AtPos i) = "[col " ++ show i ++ "]" + show (AfterPos i) = "[after " ++ show i ++ "]" + show EndOfBlock = "[EOB]" + +checkValid : ValidIndent -> Int -> EmptyRule () +checkValid AnyIndent c = pure () +checkValid (AtPos x) c = if c == x + then pure () + else fail "Invalid indentation" +checkValid (AfterPos x) c = if c >= x + then pure () + else fail "Invalid indentation" +checkValid EndOfBlock c = fail "End of block" + +||| Any token which indicates the end of a statement/block +isTerminator : Token -> Bool +isTerminator (Symbol ",") = True +isTerminator (Symbol "]") = True +isTerminator (Symbol ";") = True +isTerminator (Symbol "}") = True +isTerminator (Symbol ")") = True +isTerminator (Symbol "|") = True +isTerminator (Keyword "in") = True +isTerminator (Keyword "then") = True +isTerminator (Keyword "else") = True +isTerminator (Keyword "where") = True +isTerminator EndInput = True +isTerminator _ = False + +||| Check we're at the end of a block entry, given the start column +||| of the block. +||| It's the end if we have a terminating token, or the next token starts +||| in or before indent. Works by looking ahead but not consuming. +export +atEnd : (indent : IndentInfo) -> EmptyRule () +atEnd indent + = eoi + <|> do nextIs "Expected end of block" (isTerminator . tok) + pure () + <|> do col <- Support.column + if (col <= indent) + then pure () + else fail "Not the end of a block entry" + +-- Check we're at the end, but only by looking at indentation +export +atEndIndent : (indent : IndentInfo) -> EmptyRule () +atEndIndent indent + = eoi + <|> do col <- Support.column + if col <= indent + then pure () + else fail "Not the end of a block entry" + + +-- Parse a terminator, return where the next block entry +-- must start, given where the current block entry started +terminator : ValidIndent -> Int -> EmptyRule ValidIndent +terminator valid laststart + = do eoi + pure EndOfBlock + <|> do symbol ";" + pure (afterSemi valid) + <|> do col <- column + afterDedent valid col + <|> pure EndOfBlock + where + -- Expected indentation for the next token can either be anything (if + -- we're inside a brace delimited block) or anywhere after the initial + -- column (if we're inside an indentation delimited block) + afterSemi : ValidIndent -> ValidIndent + afterSemi AnyIndent = AnyIndent -- in braces, anything goes + afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position + afterSemi (AfterPos c) = AfterPos c + afterSemi EndOfBlock = EndOfBlock + + -- Expected indentation for the next token can either be anything (if + -- we're inside a brace delimited block) or in exactly the initial column + -- (if we're inside an indentation delimited block) + afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent + afterDedent AnyIndent col + = if col <= laststart + then pure AnyIndent + else fail "Not the end of a block entry" + afterDedent (AfterPos c) col + = if col <= laststart + then pure (AtPos c) + else fail "Not the end of a block entry" + afterDedent (AtPos c) col + = if col <= laststart + then pure (AtPos c) + else fail "Not the end of a block entry" + afterDedent EndOfBlock col = pure EndOfBlock + +-- Parse an entry in a block +blockEntry : ValidIndent -> (IndentInfo -> Rule ty) -> + Rule (ty, ValidIndent) +blockEntry valid rule + = do col <- column + checkValid valid col + p <- rule col + valid' <- terminator valid col + pure (p, valid') + +blockEntries : ValidIndent -> (IndentInfo -> Rule ty) -> + EmptyRule (List ty) +blockEntries valid rule + = do eoi; pure [] + <|> do res <- blockEntry valid rule + ts <- blockEntries (snd res) rule + pure (fst res :: ts) + <|> pure [] + +export +block : (IndentInfo -> Rule ty) -> EmptyRule (List ty) +block item + = do symbol "{" + commit + ps <- blockEntries AnyIndent item + symbol "}" + pure ps + <|> do col <- column + blockEntries (AtPos col) item + + +||| `blockAfter col rule` parses a `rule`-block indented by at +||| least `col` spaces (unless the block is explicitly delimited +||| by curly braces). `rule` is a function of the actual indentation +||| level. +export +blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty) +blockAfter mincol item + = do symbol "{" + commit + ps <- blockEntries AnyIndent item + symbol "}" + pure ps + <|> do col <- Support.column + if col <= mincol + then pure [] + else blockEntries (AtPos col) item + +export +blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty) +blockWithOptHeaderAfter {ty} mincol header item + = do symbol "{" + commit + hidt <- optional $ blockEntry AnyIndent header + restOfBlock hidt + <|> do col <- Support.column + if col <= mincol + then pure (Nothing, []) + else do hidt <- optional $ blockEntry (AtPos col) header + ps <- blockEntries (AtPos col) item + pure (map fst hidt, ps) + where + restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty) + restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item + symbol "}" + pure (Just h, ps) + restOfBlock Nothing = do ps <- blockEntries AnyIndent item + symbol "}" + pure (Nothing, ps) + +export +nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty) +nonEmptyBlock item + = do symbol "{" + commit + res <- blockEntry AnyIndent item + ps <- blockEntries (snd res) item + symbol "}" + pure (fst res :: ps) + <|> do col <- column + res <- blockEntry (AtPos col) item + ps <- blockEntries (snd res) item + pure (fst res :: ps)