mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 15:07:37 +03:00
Add missing files (I knew there'd be a couple...)
This commit is contained in:
Edwin Brady
parent
a941116b2f
commit
17b17be963
147
idris2.ipkg
Normal file
147
idris2.ipkg
Normal file
@ -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
|
||||
202
src/Core/Name.idr
Normal file
202
src/Core/Name.idr
Normal file
@ -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
|
||||
|
||||
106
src/Data/ANameMap.idr
Normal file
106
src/Data/ANameMap.idr
Normal file
@ -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)
|
||||
|
||||
|
||||
46
src/Data/Bool/Extra.idr
Normal file
46
src/Data/Bool/Extra.idr
Normal file
@ -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
|
||||
616
src/Parser/Support.idr
Normal file
616
src/Parser/Support.idr
Normal file
@ -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)
|
||||
Loading…
Reference in New Issue
Block a user