sigrid/idris2

src/Control/Delayed.idr+26−0

@@ -0,0 +1,26 @@
	1	\|\|\| Utilities functions for contitionally delaying values.
	2	module Control.Delayed
	3
	4	%default total
	5
	6	\|\|\| Type-level function for a conditionally delayed type (`Lazy` or `Inf`).
	7	public export
	8	delayed : DelayReason -> Bool -> Type -> Type
	9	delayed r False a = a
	10	delayed r True a = Delayed r a
	11
	12	\|\|\| Type-level function for a conditionally infinite type.
	13	public export
	14	inf : Bool -> Type -> Type
	15	inf = delayed Infinite
	16
	17	\|\|\| Type-level function for a conditionally lazy type.
	18	public export
	19	lazy : Bool -> Type -> Type
	20	lazy = delayed LazyValue
	21
	22	\|\|\| Conditionally delay a value.
	23	export
	24	delay : (d : Bool) -> a -> delayed r d a
	25	delay False x = x
	26	delay True x = Delay x

src/Core/Core.idr+433−0

@@ -0,0 +1,433 @@
	1	module Core.Core
	2
	3	import Core.Env
	4	import Core.TT
	5	import Parser.Support
	6
	7	import public Control.Catchable
	8	import public Data.IORef
	9
	10	%default covering
	11
	12	public export
	13	data TTCErrorMsg
	14	= FormatOlder
	15	\| FormatNewer
	16	\| EndOfBuffer String
	17	\| Corrupt String
	18
	19	public export
	20	data CaseError = DifferingArgNumbers
	21	\| DifferingTypes
	22	\| MatchErased (vars ** (Env Term vars, Term vars))
	23	\| UnknownType
	24
	25	-- All possible errors, carrying a location
	26	public export
	27	data Error
	28	= Fatal Error -- flag as unrecoverable (so don't postpone awaiting further info)
	29	\| CantConvert FC (Env Term vars) (Term vars) (Term vars)
	30	\| CantSolveEq FC (Env Term vars) (Term vars) (Term vars)
	31	\| Cycle FC (Env Term vars) (Term vars) (Term vars)
	32	\| WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error
	33	\| ValidCase FC (Env Term vars) (Either (Term vars) Error)
	34	\| UndefinedName FC Name
	35	\| InvisibleName FC Name
	36	\| BadTypeConType FC Name
	37	\| BadDataConType FC Name Name
	38	-- \| NotCovering FC Name Covering
	39	-- \| NotTotal FC Name PartialReason
	40	\| LinearUsed FC Nat Name
	41	\| LinearMisuse FC Name RigCount RigCount
	42	\| BorrowPartial FC (Env Term vars) (Term vars) (Term vars)
	43	\| BorrowPartialType FC (Env Term vars) (Term vars)
	44	\| AmbiguousName FC (List Name)
	45	\| AmbiguousElab FC (Env Term vars) (List (Term vars))
	46	\| AmbiguousSearch FC (Env Term vars) (List (Term vars))
	47	\| AllFailed (List (Maybe Name, Error))
	48	\| RecordTypeNeeded FC (Env Term vars)
	49	\| NotRecordField FC String (Maybe Name)
	50	\| NotRecordType FC Name
	51	\| IncompatibleFieldUpdate FC (List String)
	52	\| InvalidImplicit FC (Env Term vars) Name (Term vars)
	53	\| TryWithImplicits FC (Env Term vars) (List (Name, Term vars))
	54	\| CantSolveGoal FC (Term [])
	55	\| DeterminingArg FC Name (Env Term vars) (Term vars)
	56	\| UnsolvedHoles (List (FC, Name))
	57	\| CantInferArgType FC (Env Term vars) Name Name (Term vars)
	58	\| SolvedNamedHole FC (Env Term vars) Name (Term vars)
	59	\| VisibilityError FC Visibility Name Visibility Name
	60	\| NonLinearPattern FC Name
	61	\| BadPattern FC Name
	62	\| NoDeclaration FC Name
	63	\| AlreadyDefined FC Name
	64	\| NotFunctionType FC (Env Term vars) (Term vars)
	65	\| RewriteNoChange FC (Env Term vars) (Term vars) (Term vars)
	66	\| NotRewriteRule FC (Env Term vars) (Term vars)
	67	\| CaseCompile FC Name CaseError
	68	\| BadDotPattern FC (Env Term vars) String (Term vars) (Term vars)
	69	\| BadImplicit FC String
	70	\| BadRunElab FC (Env Term vars) (Term vars)
	71	\| GenericMsg FC String
	72	\| TTCError TTCErrorMsg
	73	\| FileErr String FileError
	74	\| ParseFail FC ParseError
	75	\| ModuleNotFound FC (List String)
	76	\| CyclicImports (List (List String))
	77	\| ForceNeeded
	78	\| InternalError String
	79
	80	\| InType FC Name Error
	81	\| InCon FC Name Error
	82	\| InLHS FC Name Error
	83	\| InRHS FC Name Error
	84
	85	export
	86	Show TTCErrorMsg where
	87	show FormatOlder = "TTC data is in an older format"
	88	show FormatNewer = "TTC data is in a newer format"
	89	show (EndOfBuffer when) = "End of buffer when reading " ++ when
	90	show (Corrupt ty) = "Corrupt TTC data for " ++ ty
	91
	92	-- Simplest possible display - higher level languages should unelaborate names
	93	-- and display annotations appropriately
	94	export
	95	Show Error where
	96	show (Fatal err) = show err
	97	show (CantConvert fc env x y)
	98	= show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y
	99	show (CantSolveEq fc env x y)
	100	= show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
	101	show (Cycle fc env x y)
	102	= show fc ++ ":Occurs check failed: " ++ show x ++ " and " ++ show y
	103	show (WhenUnifying fc _ x y err)
	104	= show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
	105	show (ValidCase fc _ prob)
	106	= show fc ++ ":" ++
	107	case prob of
	108	Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"
	109	Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)
	110	show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x
	111	show (InvisibleName fc (NS ns x))
	112	= show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
	113	showSep "." (reverse ns) ++ " is not explicitly imported"
	114	show (InvisibleName fc x) = show fc ++ ":Name " ++ show x ++ " is inaccessible"
	115	show (BadTypeConType fc n)
	116	= show fc ++ ":Return type of " ++ show n ++ " must be Type"
	117	show (BadDataConType fc n fam)
	118	= show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam
	119	-- show (NotCovering fc n cov)
	120	-- = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
	121	-- case cov of
	122	-- IsCovering => "Oh yes it is (Internal error!)"
	123	-- MissingCases cs => "Missing cases:\n\t" ++
	124	-- showSep "\n\t" (map show cs)
	125	-- NonCoveringCall ns => "Calls non covering function"
	126	-- ++ (case ns of
	127	-- [fn] => " " ++ show fn
	128	-- _ => "s: " ++ showSep ", " (map show ns))
	129	--
	130	-- show (NotTotal fc n r)
	131	-- = show fc ++ ":" ++ show n ++ " is not total"
	132	show (LinearUsed fc count n)
	133	= show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n
	134	show (LinearMisuse fc n exp ctx)
	135	= show fc ++ ":Trying to use " ++ showRig exp ++ " name " ++ show n ++
	136	" in " ++ showRel ctx ++ " context"
	137	where
	138	showRig : RigCount -> String
	139	showRig Rig0 = "irrelevant"
	140	showRig Rig1 = "linear"
	141	showRig RigW = "unrestricted"
	142
	143	showRel : RigCount -> String
	144	showRel Rig0 = "irrelevant"
	145	showRel Rig1 = "relevant"
	146	showRel RigW = "non-linear"
	147	show (BorrowPartial fc env t arg)
	148	= show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++
	149	" so must be fully applied"
	150	show (BorrowPartialType fc env t)
	151	= show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type"
	152
	153	show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns
	154	show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts
	155	show (AmbiguousSearch fc env ts) = show fc ++ ":Ambiguous search " ++ show ts
	156	show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
	157	show (RecordTypeNeeded fc env)
	158	= show fc ++ ":Can't infer type of record to update"
	159	show (NotRecordField fc fld Nothing)
	160	= show fc ++ ":" ++ fld ++ " is not part of a record type"
	161	show (NotRecordField fc fld (Just ty))
	162	= show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld
	163	show (NotRecordType fc ty)
	164	= show fc ++ ":" ++ show ty ++ " is not a record type"
	165	show (IncompatibleFieldUpdate fc flds)
	166	= show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
	167	show (InvalidImplicit fc env n tm) = show fc ++ ":" ++ show n ++ " is not a valid implicit argument in " ++ show tm
	168	show (TryWithImplicits fc env imps)
	169	= show fc ++ ":Need to bind implicits "
	170	++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
	171	++ "\n(The front end should probably have done this for you. Please report!)"
	172	show (CantSolveGoal fc g) = show fc ++ ":Can't solve goal " ++ assert_total (show g)
	173	show (DeterminingArg fc n env g)
	174	= show fc ++ ":Can't solve goal " ++ assert_total (show g) ++
	175	" since argument " ++ show n ++ " can't be inferred"
	176	show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs
	177	show (CantInferArgType fc env n h ty)
	178	= show fc ++ ":Can't infer type for " ++ show n ++
	179	" (got " ++ show ty ++ " with hole " ++ show h ++ ")"
	180	show (SolvedNamedHole fc _ h _) = show fc ++ ":Named hole " ++ show h ++ " is solved by unification"
	181	show (VisibilityError fc vx x vy y)
	182	= show fc ++ ":" ++ show vx ++ " " ++ show x ++ " cannot refer to "
	183	++ show vy ++ " " ++ show y
	184	show (NonLinearPattern fc n) = show fc ++ ":Non linear pattern variable " ++ show n
	185	show (BadPattern fc n) = show fc ++ ":Pattern not allowed here: " ++ show n
	186	show (NoDeclaration fc x) = show fc ++ ":No type declaration for " ++ show x
	187	show (AlreadyDefined fc x) = show fc ++ ":" ++ show x ++ " is already defined"
	188	show (NotFunctionType fc env tm) = show fc ++ ":Not a function type: " ++ show tm
	189	show (RewriteNoChange fc env rule ty)
	190	= show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty
	191	show (NotRewriteRule fc env rule)
	192	= show fc ++ ":" ++ show rule ++ " is not a rewrite rule type"
	193	show (CaseCompile fc n DifferingArgNumbers)
	194	= show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments"
	195	show (CaseCompile fc n DifferingTypes)
	196	= show fc ++ ":Patterns for " ++ show n ++ " require matching on different types"
	197	show (CaseCompile fc n UnknownType)
	198	= show fc ++ ":Can't infer type to match in " ++ show n
	199	show (CaseCompile fc n (MatchErased (_ ** (env, tm))))
	200	= show fc ++ ":Attempt to match on erased argument " ++ show tm ++
	201	" in " ++ show n
	202	show (BadDotPattern fc env reason x y)
	203	= show fc ++ ":Can't match on " ++ show x ++
	204	(if reason /= "" then " (" ++ reason ++ ")" else "") ++
	205	" - it elaborates to " ++ show y
	206	show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
	207	show (BadRunElab fc env script) = show fc ++ ":Bad elaborator script " ++ show script
	208	show (GenericMsg fc str) = show fc ++ ":" ++ str
	209	show (TTCError msg) = "Error in TTC file: " ++ show msg
	210	show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
	211	show (ParseFail fc err) = "Parse error (" ++ show err ++ ")"
	212	show (ModuleNotFound fc ns)
	213	= show fc ++ ":" ++ showSep "." (reverse ns) ++ " not found"
	214	show (CyclicImports ns)
	215	= "Module imports form a cycle: " ++ showSep " -> " (map showMod ns)
	216	where
	217	showMod : List String -> String
	218	showMod ns = showSep "." (reverse ns)
	219	show ForceNeeded = "Internal error when resolving implicit laziness"
	220	show (InternalError str) = "INTERNAL ERROR: " ++ str
	221
	222	show (InType fc n err)
	223	= show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
	224	show err
	225	show (InCon fc n err)
	226	= show fc ++ ":When elaborating type of constructor " ++ show n ++ ":\n" ++
	227	show err
	228	show (InLHS fc n err)
	229	= show fc ++ ":When elaborating left hand side of " ++ show n ++ ":\n" ++
	230	show err
	231	show (InRHS fc n err)
	232	= show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++
	233	show err
	234
	235	export
	236	getErrorLoc : Error -> Maybe FC
	237	getErrorLoc (Fatal err) = getErrorLoc err
	238	getErrorLoc (CantConvert loc env tm y) = Just loc
	239	getErrorLoc (CantSolveEq loc env tm y) = Just loc
	240	getErrorLoc (Cycle loc env tm y) = Just loc
	241	getErrorLoc (WhenUnifying loc env tm y z) = Just loc
	242	getErrorLoc (ValidCase loc env y) = Just loc
	243	getErrorLoc (UndefinedName loc y) = Just loc
	244	getErrorLoc (InvisibleName loc y) = Just loc
	245	getErrorLoc (BadTypeConType loc y) = Just loc
	246	getErrorLoc (BadDataConType loc y z) = Just loc
	247	-- getErrorLoc (NotCovering loc _ _) = Just loc
	248	-- getErrorLoc (NotTotal loc _ _) = Just loc
	249	getErrorLoc (LinearUsed loc k y) = Just loc
	250	getErrorLoc (LinearMisuse loc y z w) = Just loc
	251	getErrorLoc (BorrowPartial loc _ _ _) = Just loc
	252	getErrorLoc (BorrowPartialType loc _ _) = Just loc
	253	getErrorLoc (AmbiguousName loc xs) = Just loc
	254	getErrorLoc (AmbiguousElab loc _ xs) = Just loc
	255	getErrorLoc (AmbiguousSearch loc _ xs) = Just loc
	256	getErrorLoc (AllFailed ((_, x) :: xs)) = getErrorLoc x
	257	getErrorLoc (AllFailed []) = Nothing
	258	getErrorLoc (RecordTypeNeeded loc _) = Just loc
	259	getErrorLoc (NotRecordField loc _ _) = Just loc
	260	getErrorLoc (NotRecordType loc _) = Just loc
	261	getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
	262	getErrorLoc (InvalidImplicit loc _ y tm) = Just loc
	263	getErrorLoc (TryWithImplicits loc _ _) = Just loc
	264	getErrorLoc (CantSolveGoal loc tm) = Just loc
	265	getErrorLoc (DeterminingArg loc y env tm) = Just loc
	266	getErrorLoc (UnsolvedHoles ((loc, _) :: xs)) = Just loc
	267	getErrorLoc (UnsolvedHoles []) = Nothing
	268	getErrorLoc (CantInferArgType loc _ y z tm) = Just loc
	269	getErrorLoc (SolvedNamedHole loc _ _ y) = Just loc
	270	getErrorLoc (VisibilityError loc y z w s) = Just loc
	271	getErrorLoc (NonLinearPattern loc y) = Just loc
	272	getErrorLoc (BadPattern loc y) = Just loc
	273	getErrorLoc (NoDeclaration loc y) = Just loc
	274	getErrorLoc (AlreadyDefined loc y) = Just loc
	275	getErrorLoc (NotFunctionType loc _ tm) = Just loc
	276	getErrorLoc (RewriteNoChange loc _ tm ty) = Just loc
	277	getErrorLoc (NotRewriteRule loc _ ty) = Just loc
	278	getErrorLoc (CaseCompile loc y z) = Just loc
	279	getErrorLoc (BadDotPattern loc _ y tm z) = Just loc
	280	getErrorLoc (BadImplicit loc y) = Just loc
	281	getErrorLoc (BadRunElab loc _ tm) = Just loc
	282	getErrorLoc (GenericMsg loc y) = Just loc
	283	getErrorLoc (TTCError x) = Nothing
	284	getErrorLoc (FileErr x y) = Nothing
	285	getErrorLoc (ParseFail loc x) = Just loc
	286	getErrorLoc (ModuleNotFound loc xs) = Just loc
	287	getErrorLoc (CyclicImports xs) = Nothing
	288	getErrorLoc ForceNeeded = Nothing
	289	getErrorLoc (InternalError x) = Nothing
	290	getErrorLoc (InType x y err) = getErrorLoc err
	291	getErrorLoc (InCon x y err) = getErrorLoc err
	292	getErrorLoc (InLHS x y err) = getErrorLoc err
	293	getErrorLoc (InRHS x y err) = getErrorLoc err
	294
	295	public export
	296	record GlobalOpts where
	297	constructor MkGlobalOpts
	298	logLevel : Nat
	299
	300	export
	301	defaultOpts : GlobalOpts
	302	defaultOpts = MkGlobalOpts 0
	303
	304	-- Core is a wrapper around IO that is specialised for efficiency.
	305	export
	306	record Core t where
	307	constructor MkCore
	308	runCore : IORef GlobalOpts -> IO (Either Error t)
	309
	310	export
	311	coreRun : GlobalOpts ->
	312	Core a ->
	313	(Error -> IO b) -> (a -> IO b) -> IO b
	314	coreRun opts (MkCore act) err ok
	315	= do oref <- newIORef opts
	316	either err ok !(act oref)
	317
	318	export
	319	coreFail : Error -> Core a
	320	coreFail e = MkCore (\oref => pure (Left e))
	321
	322	export
	323	wrapError : (Error -> Error) -> Core a -> Core a
	324	wrapError fe (MkCore prog)
	325	= MkCore (\oref =>
	326	prog oref >>=
	327	(\x => case x of
	328	Left err => pure (Left (fe err))
	329	Right val => pure (Right val)))
	330
	331	-- This would be better if we restrict it to a limited set of IO operations
	332	export
	333	%inline
	334	coreLift : IO a -> Core a
	335	coreLift op = MkCore (\oref => map Right op)
	336
	337	{- Monad, Applicative, Traversable are specialised by hand for Core.
	338	In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't
	339	specialise interfaces under 'case' expressions, and this has a significant
	340	impact on both compile time and run time.
	341
	342	Of course it would be a good idea to fix this in Idris, but it's not an urgent
	343	thing on the road to self hosting, and we can make sure this isn't a problem
	344	in the next version (i.e., in this project...)! -}
	345
	346	-- Monad (specialised)
	347	export %inline
	348	(>>=) : Core a -> (a -> Core b) -> Core b
	349	(>>=) (MkCore act) f
	350	= MkCore (\oref =>
	351	act oref >>=
	352	(\x => case x of
	353	Left err => pure (Left err)
	354	Right val => runCore (f val) oref))
	355
	356	-- Applicative (specialised)
	357	export %inline
	358	pure : a -> Core a
	359	pure x = MkCore (\oref => pure (pure x))
	360
	361	export
	362	(<*>) : Core (a -> b) -> Core a -> Core b
	363	(<>) (MkCore f) (MkCore a) = MkCore (\oref => [\| f oref <> a oref \|])
	364
	365	export %inline
	366	when : Bool -> Lazy (Core ()) -> Core ()
	367	when True f = f
	368	when False f = pure ()
	369
	370	export
	371	Catchable Core Error where
	372	catch (MkCore prog) h
	373	= MkCore (\oref =>
	374	do p' <- prog oref
	375	case p' of
	376	Left e => let MkCore he = h e in he oref
	377	Right val => pure (Right val))
	378	throw = coreFail
	379
	380	-- Traversable (specialised)
	381	traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
	382	traverse' f [] acc = pure (reverse acc)
	383	traverse' f (x :: xs) acc
	384	= traverse' f xs (!(f x) :: acc)
	385
	386	export
	387	traverse : (a -> Core b) -> List a -> Core (List b)
	388	traverse f xs = traverse' f xs []
	389
	390	export
	391	data Ref : label -> Type -> Type where
	392	MkRef : IORef a -> Ref x a
	393
	394	export
	395	newRef : (x : label) -> t -> Core (Ref x t)
	396	newRef x val
	397	= do ref <- coreLift (newIORef val)
	398	pure (MkRef ref)
	399
	400	export %inline
	401	get : (x : label) -> {auto ref : Ref x a} -> Core a
	402	get x {ref = MkRef io} = coreLift (readIORef io)
	403
	404	export %inline
	405	put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
	406	put x {ref = MkRef io} val = coreLift (writeIORef io val)
	407
	408	export %inline
	409	getOpts : Core GlobalOpts
	410	getOpts = MkCore (\oref => pure (Right !(readIORef oref)))
	411
	412	export %inline
	413	putOpts : GlobalOpts -> Core ()
	414	putOpts opts = MkCore (\oref => pure (Right !(writeIORef oref opts)))
	415
	416	export
	417	cond : List (Lazy Bool, Lazy a) -> a -> a
	418	cond [] def = def
	419	cond ((x, y) :: xs) def = if x then y else cond xs def
	420
	421	export
	422	log : Nat -> String -> Core ()
	423	log lvl msg
	424	= do opts <- getOpts
	425	if logLevel opts >= lvl
	426	then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
	427	else pure ()
	428	export
	429	setLogLevel : Nat -> Core ()
	430	setLogLevel n
	431	= do opts <- getOpts
	432	putOpts (record { logLevel = n } opts)
	433

src/Core/Env.idr+25−0

@@ -0,0 +1,25 @@
	1	module Core.Env
	2
	3	import Core.TT
	4
	5	-- Environment containing types and values of local variables
	6	namespace Env
	7	public export
	8	data Env : (tm : List Name -> Type) -> List Name -> Type where
	9	Nil : Env tm []
	10	(::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
	11
	12	export
	13	extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)
	14	extend x = (::) {x}
	15
	16	export
	17	length : Env tm xs -> Nat
	18	length [] = 0
	19	length (x :: xs) = S (length xs)
	20
	21	export
	22	bindEnv : FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
	23	bindEnv loc [] tm = tm
	24	bindEnv loc (b :: env) tm
	25	= bindEnv loc env (Bind loc _ b tm)

src/Core/FC.idr+37−0

@@ -0,0 +1,37 @@
	1	module Core.FC
	2
	3	public export
	4	FilePos : Type
	5	FilePos = (Int, Int)
	6
	7	showPos : FilePos -> String
	8	showPos (l, c) = show (l + 1) ++ ":" ++ show (c + 1)
	9
	10	public export
	11	FileName : Type
	12	FileName = String
	13
	14	public export
	15	record FC where
	16	constructor MkFC
	17	file : FileName
	18	startPos : FilePos
	19	endPos : FilePos
	20
	21	export
	22	emptyFC : FC
	23	emptyFC = MkFC "(no file)" (0, 0) (0, 0)
	24
	25	export
	26	toplevelFC : FC
	27	toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
	28
	29	%name FC fc
	30
	31	export
	32	Show FC where
	33	show loc = file loc ++ ":" ++
	34	showPos (startPos loc) ++ "--" ++
	35	showPos (endPos loc)
	36
	37

src/Core/Name.idr+23−0

@@ -0,0 +1,23 @@
	1	module Core.Name
	2
	3	%default total
	4
	5	public export
	6	data Name : Type where
	7	NS : List String -> Name -> Name -- in a namespace
	8	UN : String -> Name -- user defined name
	9	MN : String -> Int -> Name -- machine generated name
	10	PV : Name -> Name -> Name -- pattern variable name
	11	MV : Int -> Name -- metavariable reference
	12	Nested : Name -> Name -> Name -- nested function name
	13	Resolved : Int -> Name -- resolved, index into context
	14
	15	export Show Name where
	16	show n = "[not done yet]"
	17
	18	export
	19	showSep : String -> List String -> String
	20	showSep sep [] = ""
	21	showSep sep [x] = x
	22	showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
	23

src/Core/TT.idr+381−0

@@ -0,0 +1,381 @@
	1	module Core.TT
	2
	3	import public Core.FC
	4	import public Core.Name
	5
	6	%default covering
	7
	8	%hide Raw -- from Reflection in the Prelude
	9	%hide Binder
	10	%hide NameType
	11	%hide Case
	12
	13	public export
	14	data NameType : Type where
	15	Bound : NameType
	16	Func : NameType
	17	DataCon : (tag : Int) -> (arity : Nat) -> NameType
	18	TyCon : (tag : Int) -> (arity : Nat) -> NameType
	19
	20	public export
	21	data Constant
	22	= I Int
	23	\| BI Integer
	24	\| Str String
	25	\| Ch Char
	26	\| Db Double
	27	\| WorldVal
	28
	29	\| IntType
	30	\| IntegerType
	31	\| StringType
	32	\| CharType
	33	\| DoubleType
	34	\| WorldType
	35
	36	export
	37	constantEq : (x, y : Constant) -> Maybe (x = y)
	38	constantEq (I x) (I y) = case decEq x y of
	39	Yes Refl => Just Refl
	40	No contra => Nothing
	41	constantEq (BI x) (BI y) = case decEq x y of
	42	Yes Refl => Just Refl
	43	No contra => Nothing
	44	constantEq (Str x) (Str y) = case decEq x y of
	45	Yes Refl => Just Refl
	46	No contra => Nothing
	47	constantEq (Ch x) (Ch y) = case decEq x y of
	48	Yes Refl => Just Refl
	49	No contra => Nothing
	50	constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!
	51	constantEq WorldVal WorldVal = Just Refl
	52	constantEq IntType IntType = Just Refl
	53	constantEq IntegerType IntegerType = Just Refl
	54	constantEq StringType StringType = Just Refl
	55	constantEq CharType CharType = Just Refl
	56	constantEq DoubleType DoubleType = Just Refl
	57	constantEq WorldType WorldType = Just Refl
	58	constantEq _ _ = Nothing
	59
	60	export
	61	Show Constant where
	62	show (I x) = show x
	63	show (BI x) = show x
	64	show (Str x) = show x
	65	show (Ch x) = show x
	66	show (Db x) = show x
	67	show WorldVal = "%MkWorld"
	68	show IntType = "Int"
	69	show IntegerType = "Integer"
	70	show StringType = "String"
	71	show CharType = "Char"
	72	show DoubleType = "Double"
	73	show WorldType = "%World"
	74
	75	export
	76	Eq Constant where
	77	(I x) == (I y) = x == y
	78	(BI x) == (BI y) = x == y
	79	(Str x) == (Str y) = x == y
	80	(Ch x) == (Ch y) = x == y
	81	(Db x) == (Db y) = x == y
	82	WorldVal == WorldVal = True
	83	IntType == IntType = True
	84	IntegerType == IntegerType = True
	85	StringType == StringType = True
	86	CharType == CharType = True
	87	DoubleType == DoubleType = True
	88	WorldType == WorldType = True
	89	_ == _ = False
	90
	91	public export
	92	data PiInfo = Implicit \| Explicit \| AutoImplicit
	93
	94	public export
	95	data RigCount = Rig0 \| Rig1 \| RigW
	96
	97	export
	98	isLinear : RigCount -> Bool
	99	isLinear Rig1 = True
	100	isLinear _ = False
	101
	102	export
	103	Eq RigCount where
	104	(==) Rig0 Rig0 = True
	105	(==) Rig1 Rig1 = True
	106	(==) RigW RigW = True
	107	(==) _ _ = False
	108
	109	export
	110	Ord RigCount where
	111	compare Rig0 Rig0 = EQ
	112	compare Rig0 Rig1 = LT
	113	compare Rig0 RigW = LT
	114
	115	compare Rig1 Rig0 = GT
	116	compare Rig1 Rig1 = EQ
	117	compare Rig1 RigW = LT
	118
	119	compare RigW Rig0 = GT
	120	compare RigW Rig1 = GT
	121	compare RigW RigW = EQ
	122
	123	export
	124	Show RigCount where
	125	show Rig0 = "Rig0"
	126	show Rig1 = "Rig1"
	127	show RigW = "RigW"
	128
	129	export
	130	rigPlus : RigCount -> RigCount -> RigCount
	131	rigPlus Rig0 Rig0 = Rig0
	132	rigPlus Rig0 Rig1 = Rig1
	133	rigPlus Rig0 RigW = RigW
	134	rigPlus Rig1 Rig0 = Rig1
	135	rigPlus Rig1 Rig1 = RigW
	136	rigPlus Rig1 RigW = RigW
	137	rigPlus RigW Rig0 = RigW
	138	rigPlus RigW Rig1 = RigW
	139	rigPlus RigW RigW = RigW
	140
	141	export
	142	rigMult : RigCount -> RigCount -> RigCount
	143	rigMult Rig0 Rig0 = Rig0
	144	rigMult Rig0 Rig1 = Rig0
	145	rigMult Rig0 RigW = Rig0
	146	rigMult Rig1 Rig0 = Rig0
	147	rigMult Rig1 Rig1 = Rig1
	148	rigMult Rig1 RigW = RigW
	149	rigMult RigW Rig0 = Rig0
	150	rigMult RigW Rig1 = RigW
	151	rigMult RigW RigW = RigW
	152
	153	public export
	154	data Binder : Type -> Type where
	155	-- Lambda bound variables with their implicitness
	156	Lam : RigCount -> PiInfo -> (ty : type) -> Binder type
	157	-- Let bound variables with their value
	158	Let : RigCount -> (val : type) -> (ty : type) -> Binder type
	159	-- Forall/pi bound variables with their implicitness
	160	Pi : RigCount -> PiInfo -> (ty : type) -> Binder type
	161	-- pattern bound variables
	162	PVar : RigCount -> (ty : type) -> Binder type
	163	-- the type of pattern bound variables
	164	PVTy : RigCount -> (ty : type) -> Binder type
	165
	166	export
	167	binderType : Binder tm -> tm
	168	binderType (Lam _ x ty) = ty
	169	binderType (Let _ val ty) = ty
	170	binderType (Pi _ x ty) = ty
	171	binderType (PVar _ ty) = ty
	172	binderType (PVTy _ ty) = ty
	173
	174	export
	175	multiplicity : Binder tm -> RigCount
	176	multiplicity (Lam c x ty) = c
	177	multiplicity (Let c val ty) = c
	178	multiplicity (Pi c x ty) = c
	179	multiplicity (PVar c ty) = c
	180	multiplicity (PVTy c ty) = c
	181
	182	export
	183	setMultiplicity : Binder tm -> RigCount -> Binder tm
	184	setMultiplicity (Lam c x ty) c' = Lam c' x ty
	185	setMultiplicity (Let c val ty) c' = Let c' val ty
	186	setMultiplicity (Pi c x ty) c' = Pi c' x ty
	187	setMultiplicity (PVar c ty) c' = PVar c' ty
	188	setMultiplicity (PVTy c ty) c' = PVTy c' ty
	189
	190	showCount : RigCount -> String
	191	showCount Rig0 = "0 "
	192	showCount Rig1 = "1 "
	193	showCount RigW = ""
	194
	195	Show ty => Show (Binder ty) where
	196	show (Lam c _ t) = "\\" ++ showCount c ++ show t
	197	show (Pi c _ t) = "Pi " ++ showCount c ++ show t
	198	show (Let c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
	199	show (PVar c t) = "pat " ++ showCount c ++ show t
	200	show (PVTy c t) = "pty " ++ showCount c ++ show t
	201
	202	export
	203	setType : Binder tm -> tm -> Binder tm
	204	setType (Lam c x _) ty = Lam c x ty
	205	setType (Let c val _) ty = Let c val ty
	206	setType (Pi c x _) ty = Pi c x ty
	207	setType (PVar c _) ty = PVar c ty
	208	setType (PVTy c _) ty = PVTy c ty
	209
	210	export
	211	Functor Binder where
	212	map func (Lam c x ty) = Lam c x (func ty)
	213	map func (Let c val ty) = Let c (func val) (func ty)
	214	map func (Pi c x ty) = Pi c x (func ty)
	215	map func (PVar c ty) = PVar c (func ty)
	216	map func (PVTy c ty) = PVTy c (func ty)
	217
	218	public export
	219	data IsVar : Name -> Nat -> List Name -> Type where
	220	First : IsVar n Z (n :: ns)
	221	Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
	222
	223	public export
	224	data Var : List Name -> Type where
	225	MkVar : {i : Nat} -> IsVar n i vars -> Var vars
	226
	227	export
	228	sameVar : {i, j : _} -> IsVar n i xs -> IsVar m j xs -> Bool
	229	sameVar {i} {j} _ _ = i == j
	230
	231	public export
	232	record AppInfo where
	233	constructor MkAppInfo
	234	plicit : PiInfo
	235
	236	export
	237	appInf : PiInfo -> AppInfo
	238	appInf p = MkAppInfo p
	239
	240	export
	241	implApp : AppInfo
	242	implApp = appInf Implicit
	243
	244	export
	245	explApp : AppInfo
	246	explApp = appInf Explicit
	247
	248	namespace CList
	249	-- A list correspoding to another list
	250	public export
	251	data CList : List a -> Type -> Type where
	252	Nil : CList [] ty
	253	(::) : (x : ty) -> CList cs ty -> CList (c :: cs) ty
	254
	255	-- Typechecked terms
	256	-- These are guaranteed to be well-scoped wrt local variables, because they are
	257	-- indexed by the names of local variables in scope
	258	mutual
	259	public export
	260	data Term : List Name -> Type where
	261	Local : FC -> Maybe RigCount ->
	262	(idx : Nat) -> IsVar name idx vars -> Term vars
	263	Ref : FC -> NameType -> (name : Name) -> Term vars
	264	-- Metavariable solution binding
	265	ULet : Int -> Term vars -> Term vars -> Term vars
	266	Bind : FC -> (x : Name) ->
	267	(b : Binder (Term vars)) ->
	268	(scope : Term (x :: vars)) -> Term vars
	269	App : FC -> (fn : Term vars) -> (p : AppInfo) -> (arg : Term vars) -> Term vars
	270	Case : FC -> (cs : List (Var vars)) ->
	271	(ty : Term vars) ->
	272	Maybe (CaseTree vars) ->
	273	(alts : List (PatAlt cs vars)) ->
	274	Term vars
	275	PrimVal : FC -> (c : Constant) -> Term vars
	276	Erased : FC -> Term vars
	277	TType : FC -> Term vars
	278
	279	public export
	280	data Pat : List Name -> Type where
	281	PAs : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
	282	PCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
	283	List (Pat vars) -> Pat vars
	284	PLoc : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars
	285	PUnmatchable : FC -> Term vars -> Pat vars
	286
	287	public export
	288	data PatAlt : List (Var vs) -> List Name -> Type where
	289	CBind : RigCount -> (x : Name) -> (ty : Term vars) ->
	290	PatAlt cs (x :: vars) -> PatAlt cs vars
	291	CPats : CList cs (Pat vars) -> Term vars -> PatAlt cs vars
	292
	293	public export
	294	data CaseTree : List Name -> Type where
	295	Switch : (idx : Nat) -> IsVar name idx vars ->
	296	(scTy : Term vars) -> List (CaseAlt vars) ->
	297	CaseTree vars
	298	STerm : Term vars -> CaseTree vars
	299	Unmatched : (msg : String) -> CaseTree vars
	300	Impossible : CaseTree vars
	301
	302	public export
	303	data CaseAlt : List Name -> Type where
	304	ConCase : Name -> (tag : Int) -> (args : List Name) ->
	305	CaseTree (args ++ vars) -> CaseAlt vars
	306	ConstCase : Constant -> CaseTree vars -> CaseAlt vars
	307	DefaultCase : CaseTree vars -> CaseAlt vars
	308
	309	export Show (Term vars) where
	310	show tm = "[not done yet]"
	311
	312	public export
	313	ClosedTerm : Type
	314	ClosedTerm = Term []
	315
	316	export
	317	apply : FC -> AppInfo -> Term vars -> List (Term vars) -> Term vars
	318	apply loc p fn [] = fn
	319	apply loc p fn (a :: args) = apply loc p (App loc fn p a) args
	320
	321	public export
	322	data Visibility = Private \| Export \| Public
	323
	324	export
	325	Show Visibility where
	326	show Private = "private"
	327	show Export = "export"
	328	show Public = "public export"
	329
	330	export
	331	Eq Visibility where
	332	Private == Private = True
	333	Export == Export = True
	334	Public == Public = True
	335	_ == _ = False
	336
	337	export
	338	Ord Visibility where
	339	compare Private Export = LT
	340	compare Private Public = LT
	341	compare Export Public = LT
	342
	343	compare Private Private = EQ
	344	compare Export Export = EQ
	345	compare Public Public = EQ
	346
	347	compare Export Private = GT
	348	compare Public Private = GT
	349	compare Public Export = GT
	350
	351	--- Some test stuff
	352	loc : (n : Name) -> {auto prf : IsVar n idx vars} -> Term vars
	353	loc n {prf} = Local emptyFC Nothing _ prf
	354
	355	cvar : (n : Name) -> {auto prf : IsVar n idx vars} -> Var vars
	356	cvar n {prf} = MkVar prf
	357
	358	ploc : (n : Name) -> {auto prf : IsVar n idx vars} -> Pat vars
	359	ploc n {prf} = PLoc emptyFC _ prf
	360
	361	lam : (n : Name) -> Term vars -> Term (n :: vars) -> Term vars
	362	lam n ty sc = Bind emptyFC n (Lam RigW Explicit ty) sc
	363
	364	NatTy : Term vs
	365	NatTy = Ref emptyFC (TyCon 0 2) (UN "Nat")
	366
	367	testPlus : Term []
	368	testPlus
	369	= lam (UN "x") NatTy $
	370	lam (UN "y") NatTy $
	371	Case emptyFC [cvar (UN "x")] NatTy Nothing
	372	[CPats [PCon emptyFC (UN "Z") 0 0 []] (loc (UN "y")),
	373	CBind RigW (UN "k") NatTy
	374	(CPats [PCon emptyFC (UN "S") 1 1 [ploc (UN "k")]]
	375	(apply emptyFC explApp (Ref emptyFC (DataCon 1 1) (UN "S"))
	376	[apply emptyFC explApp (Ref emptyFC Func (UN "plus"))
	377	[loc (UN "k"), loc (UN "y")]]))]
	378
	379
	380
	381

src/Core/Value.idr+49−0

@@ -0,0 +1,49 @@
	1	module Core.Value
	2
	3	import Core.TT
	4	import Core.Env
	5
	6	public export
	7	record EvalOpts where
	8	constructor MkEvalOpts
	9	holesOnly : Bool -- only evaluate hole solutions
	10	evalAll : Bool -- evaluate everything, including private names
	11	tcInline : Bool -- inline for totality checking
	12	fuel : Maybe Nat -- Limit for recursion depth
	13
	14	mutual
	15	public export
	16	data LocalEnv : List Name -> List Name -> Type where
	17	Nil : LocalEnv free []
	18	(::) : Closure free -> LocalEnv free vars -> LocalEnv free (x :: vars)
	19
	20	public export
	21	data Closure : List Name -> Type where
	22	MkClosure : (opts : EvalOpts) ->
	23	LocalEnv free vars ->
	24	Env Term free ->
	25	Term (vars ++ free) -> Closure free
	26	MkNFClosure : NF free -> Closure free
	27
	28	-- The head of a value: things you can apply arguments to
	29	public export
	30	data NHead : List Name -> Type where
	31	NLocal : Maybe RigCount -> (idx : Nat) -> IsVar name idx vars ->
	32	NHead vars
	33	NRef : NameType -> Name -> NHead vars
	34	NBlocked : Closure vars -> NHead vars -- complex blocked term, e.g. Case
	35
	36	-- Values themselves
	37	public export
	38	data NF : List Name -> Type where
	39	NBind : FC -> (x : Name) -> Binder (NF vars) ->
	40	(Closure vars -> NF vars) -> NF vars
	41	NApp : FC -> NHead vars -> List (Closure vars) -> NF vars
	42	NDCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
	43	List (Closure vars) -> NF vars
	44	NTCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
	45	List (Closure vars) -> NF vars
	46	NPrimVal : FC -> Constant -> NF vars
	47	NErased : FC -> NF vars
	48	NType : FC -> NF vars
	49

src/Data/Bool/Extra.idr+32−0

@@ -0,0 +1,32 @@
	1	module Data.Bool.Extra
	2
	3	%access public export
	4	%default total
	5
	6	andSameNeutral : (x : Bool) -> x && x = x
	7	andSameNeutral False = Refl
	8	andSameNeutral True = Refl
	9
	10	andFalseFalse : (x : Bool) -> x && False = False
	11	andFalseFalse False = Refl
	12	andFalseFalse True = Refl
	13
	14	andTrueNeutral : (x : Bool) -> x && True = x
	15	andTrueNeutral False = Refl
	16	andTrueNeutral True = Refl
	17
	18	orSameNeutral : (x : Bool) -> x \|\| x = x
	19	orSameNeutral False = Refl
	20	orSameNeutral True = Refl
	21
	22	orFalseNeutral : (x : Bool) -> x \|\| False = x
	23	orFalseNeutral False = Refl
	24	orFalseNeutral True = Refl
	25
	26	orTrueTrue : (x : Bool) -> x \|\| True = True
	27	orTrueTrue False = Refl
	28	orTrueTrue True = Refl
	29
	30	orSameAndRightNeutral : (x, right : Bool) -> x \|\| (x && right) = x
	31	orSameAndRightNeutral False _ = Refl
	32	orSameAndRightNeutral True _ = Refl

src/Data/StringMap.idr+303−0

@@ -0,0 +1,303 @@
	1	module Data.StringMap
	2
	3	-- Hand specialised map, for efficiency...
	4
	5	%default covering
	6
	7	Key : Type
	8	Key = String
	9
	10	-- TODO: write split
	11
	12	private
	13	data Tree : Nat -> Type -> Type where
	14	Leaf : Key -> v -> Tree Z v
	15	Branch2 : Tree n v -> Key -> Tree n v -> Tree (S n) v
	16	Branch3 : Tree n v -> Key -> Tree n v -> Key -> Tree n v -> Tree (S n) v
	17
	18	branch4 :
	19	Tree n v -> Key ->
	20	Tree n v -> Key ->
	21	Tree n v -> Key ->
	22	Tree n v ->
	23	Tree (S (S n)) v
	24	branch4 a b c d e f g =
	25	Branch2 (Branch2 a b c) d (Branch2 e f g)
	26
	27	branch5 :
	28	Tree n v -> Key ->
	29	Tree n v -> Key ->
	30	Tree n v -> Key ->
	31	Tree n v -> Key ->
	32	Tree n v ->
	33	Tree (S (S n)) v
	34	branch5 a b c d e f g h i =
	35	Branch2 (Branch2 a b c) d (Branch3 e f g h i)
	36
	37	branch6 :
	38	Tree n v -> Key ->
	39	Tree n v -> Key ->
	40	Tree n v -> Key ->
	41	Tree n v -> Key ->
	42	Tree n v -> Key ->
	43	Tree n v ->
	44	Tree (S (S n)) v
	45	branch6 a b c d e f g h i j k =
	46	Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
	47
	48	branch7 :
	49	Tree n v -> Key ->
	50	Tree n v -> Key ->
	51	Tree n v -> Key ->
	52	Tree n v -> Key ->
	53	Tree n v -> Key ->
	54	Tree n v -> Key ->
	55	Tree n v ->
	56	Tree (S (S n)) v
	57	branch7 a b c d e f g h i j k l m =
	58	Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
	59
	60	merge1 : Tree n v -> Key -> Tree (S n) v -> Key -> Tree (S n) v -> Tree (S (S n)) v
	61	merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
	62	merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
	63	merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
	64	merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
	65
	66	merge2 : Tree (S n) v -> Key -> Tree n v -> Key -> Tree (S n) v -> Tree (S (S n)) v
	67	merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
	68	merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
	69	merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
	70	merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
	71
	72	merge3 : Tree (S n) v -> Key -> Tree (S n) v -> Key -> Tree n v -> Tree (S (S n)) v
	73	merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
	74	merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
	75	merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
	76	merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m
	77
	78	treeLookup : Key -> Tree n v -> Maybe v
	79	treeLookup k (Leaf k' v) =
	80	if k == k' then
	81	Just v
	82	else
	83	Nothing
	84	treeLookup k (Branch2 t1 k' t2) =
	85	if k <= k' then
	86	treeLookup k t1
	87	else
	88	treeLookup k t2
	89	treeLookup k (Branch3 t1 k1 t2 k2 t3) =
	90	if k <= k1 then
	91	treeLookup k t1
	92	else if k <= k2 then
	93	treeLookup k t2
	94	else
	95	treeLookup k t3
	96
	97	treeInsert' : Key -> v -> Tree n v -> Either (Tree n v) (Tree n v, Key, Tree n v)
	98	treeInsert' k v (Leaf k' v') =
	99	case compare k k' of
	100	LT => Right (Leaf k v, k, Leaf k' v')
	101	EQ => Left (Leaf k v)
	102	GT => Right (Leaf k' v', k', Leaf k v)
	103	treeInsert' k v (Branch2 t1 k' t2) =
	104	if k <= k' then
	105	case treeInsert' k v t1 of
	106	Left t1' => Left (Branch2 t1' k' t2)
	107	Right (a, b, c) => Left (Branch3 a b c k' t2)
	108	else
	109	case treeInsert' k v t2 of
	110	Left t2' => Left (Branch2 t1 k' t2')
	111	Right (a, b, c) => Left (Branch3 t1 k' a b c)
	112	treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
	113	if k <= k1 then
	114	case treeInsert' k v t1 of
	115	Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
	116	Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
	117	else
	118	if k <= k2 then
	119	case treeInsert' k v t2 of
	120	Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
	121	Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
	122	else
	123	case treeInsert' k v t3 of
	124	Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
	125	Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
	126
	127	treeInsert : Key -> v -> Tree n v -> Either (Tree n v) (Tree (S n) v)
	128	treeInsert k v t =
	129	case treeInsert' k v t of
	130	Left t' => Left t'
	131	Right (a, b, c) => Right (Branch2 a b c)
	132
	133	delType : Nat -> Type -> Type
	134	delType Z v = ()
	135	delType (S n) v = Tree n v
	136
	137	treeDelete : Key -> Tree n v -> Either (Tree n v) (delType n v)
	138	treeDelete k (Leaf k' v) =
	139	if k == k' then
	140	Right ()
	141	else
	142	Left (Leaf k' v)
	143	treeDelete {n=S Z} k (Branch2 t1 k' t2) =
	144	if k <= k' then
	145	case treeDelete k t1 of
	146	Left t1' => Left (Branch2 t1' k' t2)
	147	Right () => Right t2
	148	else
	149	case treeDelete k t2 of
	150	Left t2' => Left (Branch2 t1 k' t2')
	151	Right () => Right t1
	152	treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =
	153	if k <= k1 then
	154	case treeDelete k t1 of
	155	Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
	156	Right () => Left (Branch2 t2 k2 t3)
	157	else if k <= k2 then
	158	case treeDelete k t2 of
	159	Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
	160	Right () => Left (Branch2 t1 k1 t3)
	161	else
	162	case treeDelete k t3 of
	163	Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
	164	Right () => Left (Branch2 t1 k1 t2)
	165	treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =
	166	if k <= k' then
	167	case treeDelete k t1 of
	168	Left t1' => Left (Branch2 t1' k' t2)
	169	Right t1' =>
	170	case t2 of
	171	Branch2 a b c => Right (Branch3 t1' k' a b c)
	172	Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
	173	else
	174	case treeDelete k t2 of
	175	Left t2' => Left (Branch2 t1 k' t2')
	176	Right t2' =>
	177	case t1 of
	178	Branch2 a b c => Right (Branch3 a b c k' t2')
	179	Branch3 a b c d e => Left (branch4 a b c d e k' t2')
	180	treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
	181	if k <= k1 then
	182	case treeDelete k t1 of
	183	Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
	184	Right t1' => Left (merge1 t1' k1 t2 k2 t3)
	185	else if k <= k2 then
	186	case treeDelete k t2 of
	187	Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
	188	Right t2' => Left (merge2 t1 k1 t2' k2 t3)
	189	else
	190	case treeDelete k t3 of
	191	Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
	192	Right t3' => Left (merge3 t1 k1 t2 k2 t3')
	193
	194	treeToList : Tree n v -> List (Key, v)
	195	treeToList = treeToList' (:: [])
	196	where
	197	treeToList' : ((Key, v) -> List (Key, v)) -> Tree n v -> List (Key, v)
	198	treeToList' cont (Leaf k v) = cont (k, v)
	199	treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
	200	treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
	201
	202	export
	203	data StringMap : Type -> Type where
	204	Empty : StringMap v
	205	M : (n : Nat) -> Tree n v -> StringMap v
	206
	207	export
	208	empty : StringMap v
	209	empty = Empty
	210
	211	export
	212	lookup : String -> StringMap v -> Maybe v
	213	lookup _ Empty = Nothing
	214	lookup k (M _ t) = treeLookup k t
	215
	216	export
	217	insert : String -> v -> StringMap v -> StringMap v
	218	insert k v Empty = M Z (Leaf k v)
	219	insert k v (M _ t) =
	220	case treeInsert k v t of
	221	Left t' => (M _ t')
	222	Right t' => (M _ t')
	223
	224	export
	225	insertFrom : Foldable f => f (String, v) -> StringMap v -> StringMap v
	226	insertFrom = flip $ foldl $ flip $ uncurry insert
	227
	228	export
	229	delete : String -> StringMap v -> StringMap v
	230	delete _ Empty = Empty
	231	delete k (M Z t) =
	232	case treeDelete k t of
	233	Left t' => (M _ t')
	234	Right () => Empty
	235	delete k (M (S _) t) =
	236	case treeDelete k t of
	237	Left t' => (M _ t')
	238	Right t' => (M _ t')
	239
	240	export
	241	fromList : List (String, v) -> StringMap v
	242	fromList l = foldl (flip (uncurry insert)) empty l
	243
	244	export
	245	toList : StringMap v -> List (String, v)
	246	toList Empty = []
	247	toList (M _ t) = treeToList t
	248
	249	\|\|\| Gets the Keyeys of the map.
	250	export
	251	keys : StringMap v -> List String
	252	keys = map fst . toList
	253
	254	\|\|\| Gets the values of the map. Could contain duplicates.
	255	export
	256	values : StringMap v -> List v
	257	values = map snd . toList
	258
	259	treeMap : (a -> b) -> Tree n a -> Tree n b
	260	treeMap f (Leaf k v) = Leaf k (f v)
	261	treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
	262	treeMap f (Branch3 t1 k1 t2 k2 t3)
	263	= Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
	264
	265	export
	266	implementation Functor (StringMap) where
	267	map _ Empty = Empty
	268	map f (M n t) = M _ (treeMap f t)
	269
	270	\|\|\| Merge two maps. When encountering duplicate keys, using a function to combine the values.
	271	\|\|\| Uses the ordering of the first map given.
	272	export
	273	mergeWith : (v -> v -> v) -> StringMap v -> StringMap v -> StringMap v
	274	mergeWith f x y = insertFrom inserted x where
	275	inserted : List (Key, v)
	276	inserted = do
	277	(k, v) <- toList y
	278	let v' = (maybe id f $ lookup k x) v
	279	pure (k, v')
	280
	281	\|\|\| Merge two maps using the Semigroup (and by extension, Monoid) operation.
	282	\|\|\| Uses mergeWith internally, so the ordering of the left map is kept.
	283	export
	284	merge : Semigroup v => StringMap v -> StringMap v -> StringMap v
	285	merge = mergeWith (<+>)
	286
	287	\|\|\| Left-biased merge, also keeps the ordering specified by the left map.
	288	export
	289	mergeLeft : StringMap v -> StringMap v -> StringMap v
	290	mergeLeft = mergeWith const
	291
	292	-- TODO: is this the right variant of merge to use for this? I think it is, but
	293	-- I could also see the advantages of using `mergeLeft`. The current approach is
	294	-- strictly more powerful I believe, because `mergeLeft` can be emulated with
	295	-- the `First` monoid. However, this does require more code to do the same
	296	-- thing.
	297	export
	298	Semigroup v => Semigroup (StringMap v) where
	299	(<+>) = merge
	300
	301	export
	302	(Semigroup v) => Monoid (StringMap v) where
	303	neutral = empty

src/Parser/Lexer.idr+176−0

@@ -0,0 +1,176 @@
	1	module Parser.Lexer
	2
	3	import public Text.Lexer
	4
	5	%default total
	6
	7	public export
	8	data Token = Ident String
	9	\| HoleIdent String
	10	\| Literal Integer
	11	\| StrLit String
	12	\| CharLit String
	13	\| DoubleLit Double
	14	\| Symbol String
	15	\| Keyword String
	16	\| Unrecognised String
	17	\| Comment String
	18	\| DocComment String
	19	\| CGDirective String
	20	\| EndInput
	21
	22	export
	23	Show Token where
	24	show (Ident x) = "identifier " ++ x
	25	show (HoleIdent x) = "hole identifier " ++ x
	26	show (Literal x) = "literal " ++ show x
	27	show (StrLit x) = "string " ++ show x
	28	show (CharLit x) = "character " ++ show x
	29	show (DoubleLit x) = "double " ++ show x
	30	show (Symbol x) = "symbol " ++ x
	31	show (Keyword x) = x
	32	show (Unrecognised x) = "Unrecognised " ++ x
	33	show (Comment x) = "comment"
	34	show (DocComment x) = "doc comment"
	35	show (CGDirective x) = "CGDirective " ++ x
	36	show EndInput = "end of input"
	37
	38	export
	39	Show (TokenData Token) where
	40	show t = show (line t, col t, tok t)
	41
	42	comment : Lexer
	43	comment = is '-' <+> is '-' <+> many (isNot '\n')
	44
	45	toEndComment : (k : Nat) -> Recognise (k /= 0)
	46	toEndComment Z = empty
	47	toEndComment (S k)
	48	= some (pred (\c => c /= '-' && c /= '{'))
	49	<+> toEndComment (S k)
	50	<\|> is '{' <+> is '-' <+> toEndComment (S (S k))
	51	<\|> is '-' <+> is '}' <+> toEndComment k
	52	<\|> is '{' <+> toEndComment (S k)
	53	<\|> is '-' <+> toEndComment (S k)
	54
	55	blockComment : Lexer
	56	blockComment = is '{' <+> is '-' <+> toEndComment 1
	57
	58	docComment : Lexer
	59	docComment = is '\|' <+> is '\|' <+> is '\|' <+> many (isNot '\n')
	60
	61	ident : Lexer
	62	ident = pred startIdent <+> many (pred validIdent)
	63	where
	64	startIdent : Char -> Bool
	65	startIdent '_' = True
	66	startIdent x = isAlpha x
	67
	68	validIdent : Char -> Bool
	69	validIdent '_' = True
	70	validIdent '\'' = True
	71	validIdent x = isAlphaNum x
	72
	73	holeIdent : Lexer
	74	holeIdent = is '?' <+> ident
	75
	76	doubleLit : Lexer
	77	doubleLit
	78	= digits <+> is '.' <+> digits <+> opt
	79	(is 'e' <+> opt (is '-' <\|> is '+') <+> digits)
	80
	81	-- Do this as an entire token, because the contents will be processed by
	82	-- a specific back end
	83	cgDirective : Lexer
	84	cgDirective
	85	= exact "%cg" <+>
	86	((some space <+>
	87	some (pred isAlphaNum) <+> many space <+>
	88	is '{' <+> many (isNot '}') <+>
	89	is '}')
	90	<\|> many (isNot '\n'))
	91
	92	mkDirective : String -> Token
	93	mkDirective str = CGDirective (trim (substr 3 (length str) str))
	94
	95	-- Reserved words
	96	keywords : List String
	97	keywords = ["data", "module", "where", "let", "in", "do", "record",
	98	"auto", "implicit", "mutual", "namespace", "parameters",
	99	"with", "impossible", "case", "of",
	100	"if", "then", "else", "forall", "rewrite",
	101	"using", "interface", "implementation", "open", "import",
	102	"public", "export", "private",
	103	"infixl", "infixr", "infix", "prefix",
	104	"Type", "Int", "Integer", "String", "Char", "Double",
	105	"total", "partial", "covering"]
	106
	107	-- Reserved words for internal syntax
	108	special : List String
	109	special = ["%lam", "%pi", "%imppi", "%let"]
	110
	111	-- Special symbols - things which can't be a prefix of another symbol, and
	112	-- don't match 'validSymbol'
	113	export
	114	symbols : List String
	115	symbols
	116	= [".(", -- for things such as Foo.Bar.(+)
	117	"@{",
	118	"(", ")", "{", "}", "[", "]", ",", ";", "_",
	119	"`(", "`", "~"]
	120
	121	export
	122	opChars : String
	123	opChars = ":!#$%&*+./<=>?@\\^\|-~"
	124
	125	validSymbol : Lexer
	126	validSymbol = some (oneOf opChars)
	127
	128	-- Valid symbols which have a special meaning so can't be operators
	129	export
	130	reservedSymbols : List String
	131	reservedSymbols
	132	= symbols ++
	133	["%", "\\", ":", "=", "\|", "\|\|\|", "<-", "->", "=>", "?", "&", "**"]
	134
	135	symbolChar : Char -> Bool
	136	symbolChar c = c `elem` unpack opChars
	137
	138	rawTokens : TokenMap Token
	139	rawTokens =
	140	[(comment, Comment),
	141	(blockComment, Comment),
	142	(docComment, DocComment),
	143	(cgDirective, mkDirective),
	144	(holeIdent, \x => HoleIdent (assert_total (strTail x)))] ++
	145	map (\x => (exact x, Symbol)) symbols ++
	146	[(doubleLit, \x => DoubleLit (cast x)),
	147	(digits, \x => Literal (cast x)),
	148	(stringLit, \x => StrLit (stripQuotes x)),
	149	(charLit, \x => CharLit (stripQuotes x)),
	150	(ident, \x => if x `elem` keywords then Keyword x else Ident x),
	151	(space, Comment),
	152	(validSymbol, Symbol),
	153	(symbol, Unrecognised)]
	154	where
	155	stripQuotes : String -> String
	156	-- ASSUMPTION! Only total because we know we're getting quoted strings.
	157	stripQuotes = assert_total (strTail . reverse . strTail . reverse)
	158
	159	export
	160	lex : String -> Either (Int, Int, String) (List (TokenData Token))
	161	lex str
	162	= case lex rawTokens str of
	163	-- Add the EndInput token so that we'll have a line and column
	164	-- number to read when storing spans in the file
	165	(tok, (l, c, "")) => Right (filter notComment tok ++
	166	[MkToken l c EndInput])
	167	(_, fail) => Left fail
	168	where
	169	notComment : TokenData Token -> Bool
	170	notComment t = case tok t of
	171	Comment _ => False
	172	DocComment _ => False -- TODO!
	173	_ => True
	174
	175	testLex : String -> String
	176	testLex inp = show (Lexer.lex inp)

src/Parser/Support.idr+521−0

@@ -0,0 +1,521 @@
	1	module Parser.Support
	2
	3	import public Text.Lexer
	4	import public Parser.Lexer
	5	import public Text.Parser
	6
	7	import Core.TT
	8	import Data.List.Views
	9
	10	%default total
	11
	12	public export
	13	Rule : Type -> Type
	14	Rule ty = Grammar (TokenData Token) True ty
	15
	16	public export
	17	EmptyRule : Type -> Type
	18	EmptyRule ty = Grammar (TokenData Token) False ty
	19
	20	public export
	21	data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
	22	\| LexFail (Int, Int, String)
	23	\| FileFail FileError
	24
	25	export
	26	Show ParseError where
	27	show (ParseFail err loc toks)
	28	= "Parse error: " ++ err ++ " (next tokens: "
	29	++ show (take 10 toks) ++ ")"
	30	show (LexFail (c, l, str))
	31	= "Lex error at " ++ show (c, l) ++ " input: " ++ str
	32	show (FileFail err)
	33	= "File error: " ++ show err
	34
	35	export
	36	eoi : EmptyRule ()
	37	eoi
	38	= do nextIs "Expected end of input" (isEOI . tok)
	39	pure ()
	40	where
	41	isEOI : Token -> Bool
	42	isEOI EndInput = True
	43	isEOI _ = False
	44
	45	export
	46	runParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty
	47	runParser str p
	48	= case lex str of
	49	Left err => Left $ LexFail err
	50	Right toks =>
	51	case parse p toks of
	52	Left (Error err []) =>
	53	Left $ ParseFail err Nothing []
	54	Left (Error err (t :: ts)) =>
	55	Left $ ParseFail err (Just (line t, col t))
	56	(map tok (t :: ts))
	57	Right (val, _) => Right val
	58
	59	export
	60	parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
	61	parseFile fn p
	62	= do Right str <- readFile fn
	63	\| Left err => pure (Left (FileFail err))
	64	pure (runParser str p)
	65
	66
	67	-- Some basic parsers used by all the intermediate forms
	68
	69	export
	70	location : EmptyRule (Int, Int)
	71	location
	72	= do tok <- peek
	73	pure (line tok, col tok)
	74
	75	export
	76	column : EmptyRule Int
	77	column
	78	= do (line, col) <- location
	79	pure col
	80
	81	hex : Char -> Maybe Int
	82	hex '0' = Just 0
	83	hex '1' = Just 1
	84	hex '2' = Just 2
	85	hex '3' = Just 3
	86	hex '4' = Just 4
	87	hex '5' = Just 5
	88	hex '6' = Just 6
	89	hex '7' = Just 7
	90	hex '8' = Just 8
	91	hex '9' = Just 9
	92	hex 'a' = Just 10
	93	hex 'b' = Just 11
	94	hex 'c' = Just 12
	95	hex 'd' = Just 13
	96	hex 'e' = Just 14
	97	hex 'f' = Just 15
	98	hex _ = Nothing
	99
	100	dec : Char -> Maybe Int
	101	dec '0' = Just 0
	102	dec '1' = Just 1
	103	dec '2' = Just 2
	104	dec '3' = Just 3
	105	dec '4' = Just 4
	106	dec '5' = Just 5
	107	dec '6' = Just 6
	108	dec '7' = Just 7
	109	dec '8' = Just 8
	110	dec '9' = Just 9
	111	dec _ = Nothing
	112
	113	oct : Char -> Maybe Int
	114	oct '0' = Just 0
	115	oct '1' = Just 1
	116	oct '2' = Just 2
	117	oct '3' = Just 3
	118	oct '4' = Just 4
	119	oct '5' = Just 5
	120	oct '6' = Just 6
	121	oct '7' = Just 7
	122	oct _ = Nothing
	123
	124	getEsc : String -> Maybe Char
	125	getEsc "NUL" = Just '\NUL'
	126	getEsc "SOH" = Just '\SOH'
	127	getEsc "STX" = Just '\STX'
	128	getEsc "ETX" = Just '\ETX'
	129	getEsc "EOT" = Just '\EOT'
	130	getEsc "ENQ" = Just '\ENQ'
	131	getEsc "ACK" = Just '\ACK'
	132	getEsc "BEL" = Just '\BEL'
	133	getEsc "BS" = Just '\BS'
	134	getEsc "HT" = Just '\HT'
	135	getEsc "LF" = Just '\LF'
	136	getEsc "VT" = Just '\VT'
	137	getEsc "FF" = Just '\FF'
	138	getEsc "CR" = Just '\CR'
	139	getEsc "SO" = Just '\SO'
	140	getEsc "SI" = Just '\SI'
	141	getEsc "DLE" = Just '\DLE'
	142	getEsc "DC1" = Just '\DC1'
	143	getEsc "DC2" = Just '\DC2'
	144	getEsc "DC3" = Just '\DC3'
	145	getEsc "DC4" = Just '\DC4'
	146	getEsc "NAK" = Just '\NAK'
	147	getEsc "SYN" = Just '\SYN'
	148	getEsc "ETB" = Just '\ETB'
	149	getEsc "CAN" = Just '\CAN'
	150	getEsc "EM" = Just '\EM'
	151	getEsc "SUB" = Just '\SUB'
	152	getEsc "ESC" = Just '\ESC'
	153	getEsc "FS" = Just '\FS'
	154	getEsc "GS" = Just '\GS'
	155	getEsc "RS" = Just '\RS'
	156	getEsc "US" = Just '\US'
	157	getEsc "SP" = Just '\SP'
	158	getEsc "DEL" = Just '\DEL'
	159	getEsc str = Nothing
	160
	161	escape' : List Char -> Maybe (List Char)
	162	escape' [] = pure []
	163	escape' ('\\' :: '\\' :: xs) = pure $ '\\' :: !(escape' xs)
	164	escape' ('\\' :: '&' :: xs) = pure !(escape' xs)
	165	escape' ('\\' :: 'a' :: xs) = pure $ '\a' :: !(escape' xs)
	166	escape' ('\\' :: 'b' :: xs) = pure $ '\b' :: !(escape' xs)
	167	escape' ('\\' :: 'f' :: xs) = pure $ '\f' :: !(escape' xs)
	168	escape' ('\\' :: 'n' :: xs) = pure $ '\n' :: !(escape' xs)
	169	escape' ('\\' :: 'r' :: xs) = pure $ '\r' :: !(escape' xs)
	170	escape' ('\\' :: 't' :: xs) = pure $ '\t' :: !(escape' xs)
	171	escape' ('\\' :: 'v' :: xs) = pure $ '\v' :: !(escape' xs)
	172	escape' ('\\' :: '\'' :: xs) = pure $ '\'' :: !(escape' xs)
	173	escape' ('\\' :: '\"' :: xs) = pure $ '\"' :: !(escape' xs)
	174	escape' ('\\' :: 'x' :: xs)
	175	= case span isHexDigit xs of
	176	([], rest) => assert_total (escape' rest)
	177	(ds, rest) => pure $ cast !(toHex 1 (reverse ds)) ::
	178	!(assert_total (escape' rest))
	179	where
	180	toHex : Int -> List Char -> Maybe Int
	181	toHex _ [] = Just 0
	182	toHex m (d :: ds)
	183	= pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
	184	escape' ('\\' :: 'o' :: xs)
	185	= case span isOctDigit xs of
	186	([], rest) => assert_total (escape' rest)
	187	(ds, rest) => pure $ cast !(toOct 1 (reverse ds)) ::
	188	!(assert_total (escape' rest))
	189	where
	190	toOct : Int -> List Char -> Maybe Int
	191	toOct _ [] = Just 0
	192	toOct m (d :: ds)
	193	= pure $ !(oct (toLower d)) * m + !(toOct (m*8) ds)
	194	escape' ('\\' :: xs)
	195	= case span isDigit xs of
	196	([], (a :: b :: c :: rest)) =>
	197	case getEsc (pack (the (List _) [a, b, c])) of
	198	Just v => Just (v :: !(assert_total (escape' rest)))
	199	Nothing => case getEsc (pack (the (List _) [a, b])) of
	200	Just v => Just (v :: !(assert_total (escape' (c :: rest))))
	201	Nothing => escape' xs
	202	([], (a :: b :: [])) =>
	203	case getEsc (pack (the (List _) [a, b])) of
	204	Just v => Just (v :: [])
	205	Nothing => escape' xs
	206	([], rest) => assert_total (escape' rest)
	207	(ds, rest) => Just $ cast (cast {to=Int} (pack ds)) ::
	208	!(assert_total (escape' rest))
	209	escape' (x :: xs) = Just $ x :: !(escape' xs)
	210
	211	escape : String -> Maybe String
	212	escape x = pure $ pack !(escape' (unpack x))
	213
	214	getCharLit : String -> Maybe Char
	215	getCharLit str
	216	= do e <- escape str
	217	if length e == 1
	218	then Just (assert_total (strHead e))
	219	else if length e == 0 -- parsed the NULL character that terminated the string!
	220	then Just '\0000'
	221	else Nothing
	222
	223	export
	224	constant : Rule Constant
	225	constant
	226	= terminal "Expected constant"
	227	(\x => case tok x of
	228	Literal i => Just (BI i)
	229	StrLit s => case escape s of
	230	Nothing => Nothing
	231	Just s' => Just (Str s')
	232	CharLit c => case getCharLit c of
	233	Nothing => Nothing
	234	Just c' => Just (Ch c')
	235	DoubleLit d => Just (Db d)
	236	Keyword "Int" => Just IntType
	237	Keyword "Integer" => Just IntegerType
	238	Keyword "String" => Just StringType
	239	Keyword "Char" => Just CharType
	240	Keyword "Double" => Just DoubleType
	241	_ => Nothing)
	242
	243	export
	244	intLit : Rule Integer
	245	intLit
	246	= terminal "Expected integer literal"
	247	(\x => case tok x of
	248	Literal i => Just i
	249	_ => Nothing)
	250
	251	export
	252	strLit : Rule String
	253	strLit
	254	= terminal "Expected string literal"
	255	(\x => case tok x of
	256	StrLit s => Just s
	257	_ => Nothing)
	258
	259	export
	260	symbol : String -> Rule ()
	261	symbol req
	262	= terminal ("Expected '" ++ req ++ "'")
	263	(\x => case tok x of
	264	Symbol s => if s == req then Just ()
	265	else Nothing
	266	_ => Nothing)
	267
	268	export
	269	keyword : String -> Rule ()
	270	keyword req
	271	= terminal ("Expected '" ++ req ++ "'")
	272	(\x => case tok x of
	273	Keyword s => if s == req then Just ()
	274	else Nothing
	275	_ => Nothing)
	276
	277	export
	278	exactIdent : String -> Rule ()
	279	exactIdent req
	280	= terminal ("Expected " ++ req)
	281	(\x => case tok x of
	282	Ident s => if s == req then Just ()
	283	else Nothing
	284	_ => Nothing)
	285
	286	export
	287	operator : Rule String
	288	operator
	289	= terminal "Expected operator"
	290	(\x => case tok x of
	291	Symbol s =>
	292	if s `elem` reservedSymbols
	293	then Nothing
	294	else Just s
	295	_ => Nothing)
	296
	297	identPart : Rule String
	298	identPart
	299	= terminal "Expected name"
	300	(\x => case tok x of
	301	Ident str => Just str
	302	_ => Nothing)
	303
	304	export
	305	namespace_ : Rule (List String)
	306	namespace_
	307	= do ns <- sepBy1 (do col <- column
	308	symbol "."
	309	col' <- column
	310	if (col' - col == 1)
	311	then pure ()
	312	else fail "No whitepace allowed after namespace separator")
	313	identPart
	314	pure (reverse ns) -- innermost first, so reverse
	315
	316	export
	317	unqualifiedName : Rule String
	318	unqualifiedName = identPart
	319
	320	export
	321	holeName : Rule String
	322	holeName
	323	= terminal "Expected hole name"
	324	(\x => case tok x of
	325	HoleIdent str => Just str
	326	_ => Nothing)
	327
	328	export
	329	name : Rule Name
	330	name
	331	= do ns <- namespace_
	332	(do symbol ".("
	333	op <- operator
	334	symbol ")"
	335	pure (NS ns (UN op))) <\|>
	336	(pure (mkFullName ns))
	337	<\|> do symbol "("
	338	op <- operator
	339	symbol ")"
	340	pure (UN op)
	341	where
	342	mkFullName : List String -> Name
	343	mkFullName [] = UN "NONE" -- Can't happen :)
	344	mkFullName [n] = UN n
	345	mkFullName (n :: ns) = NS ns (UN n)
	346
	347	export
	348	IndentInfo : Type
	349	IndentInfo = Int
	350
	351	export
	352	init : IndentInfo
	353	init = 0
	354
	355	continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
	356	continueF err indent
	357	= do eoi; err
	358	<\|> do col <- column
	359	if (col <= indent)
	360	then err
	361	else pure ()
	362
	363	-- Fail if this is the end of a block entry or end of file
	364	export
	365	continue : (indent : IndentInfo) -> EmptyRule ()
	366	continue = continueF (fail "Unexpected end of expression")
	367
	368	-- As 'continue' but failing is fatal (i.e. entire parse fails)
	369	export
	370	mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
	371	mustContinue indent Nothing
	372	= continueF (fatalError "Unexpected end of expression") indent
	373	mustContinue indent (Just req)
	374	= continueF (fatalError ("Expected '" ++ req ++ "'")) indent
	375
	376	data ValidIndent
	377	= AnyIndent -- In {}, entries can begin in any column
	378	\| AtPos Int -- Entry must begin in a specific column
	379	\| AfterPos Int -- Entry can begin in this column or later
	380	\| EndOfBlock -- Block is finished
	381
	382	Show ValidIndent where
	383	show AnyIndent = "[any]"
	384	show (AtPos i) = "[col " ++ show i ++ "]"
	385	show (AfterPos i) = "[after " ++ show i ++ "]"
	386	show EndOfBlock = "[EOB]"
	387
	388	checkValid : ValidIndent -> Int -> EmptyRule ()
	389	checkValid AnyIndent c = pure ()
	390	checkValid (AtPos x) c = if c == x
	391	then pure ()
	392	else fail "Invalid indentation"
	393	checkValid (AfterPos x) c = if c >= x
	394	then pure ()
	395	else fail "Invalid indentation"
	396	checkValid EndOfBlock c = fail "End of block"
	397
	398	-- Any token which indicates the end of a statement/block
	399	isTerminator : Token -> Bool
	400	isTerminator (Symbol ",") = True
	401	isTerminator (Symbol "]") = True
	402	isTerminator (Symbol ";") = True
	403	isTerminator (Symbol "}") = True
	404	isTerminator (Symbol ")") = True
	405	isTerminator (Symbol "\|") = True
	406	isTerminator (Keyword "in") = True
	407	isTerminator EndInput = True
	408	isTerminator _ = False
	409
	410	-- Check we're at the end of a block entry, given the start column
	411	-- of the block.
	412	-- It's the end if we have a terminating token, or the next token starts
	413	-- in or before indent. Works by looking ahead but not consuming.
	414	export
	415	atEnd : (indent : IndentInfo) -> EmptyRule ()
	416	atEnd indent
	417	= eoi
	418	<\|> do nextIs "Expected end of block" (isTerminator . tok)
	419	pure ()
	420	<\|> do col <- column
	421	if (col <= indent)
	422	then pure ()
	423	else fail "Not the end of a block entry"
	424
	425	-- Parse a terminator, return where the next block entry
	426	-- must start, given where the current block entry started
	427	terminator : ValidIndent -> Int -> EmptyRule ValidIndent
	428	terminator valid laststart
	429	= do eoi
	430	pure EndOfBlock
	431	<\|> do symbol ";"
	432	pure (afterSemi valid)
	433	<\|> do col <- column
	434	afterDedent valid col
	435	<\|> pure EndOfBlock
	436	where
	437	-- Expected indentation for the next token can either be anything (if
	438	-- we're inside a brace delimited block) or anywhere after the initial
	439	-- column (if we're inside an indentation delimited block)
	440	afterSemi : ValidIndent -> ValidIndent
	441	afterSemi AnyIndent = AnyIndent -- in braces, anything goes
	442	afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
	443	afterSemi (AfterPos c) = AfterPos c
	444	afterSemi EndOfBlock = EndOfBlock
	445
	446	-- Expected indentation for the next token can either be anything (if
	447	-- we're inside a brace delimited block) or in exactly the initial column
	448	-- (if we're inside an indentation delimited block)
	449	afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
	450	afterDedent AnyIndent col
	451	= if col <= laststart
	452	then pure AnyIndent
	453	else fail "Not the end of a block entry"
	454	afterDedent (AfterPos c) col
	455	= if col <= laststart
	456	then pure (AtPos c)
	457	else fail "Not the end of a block entry"
	458	afterDedent (AtPos c) col
	459	= if col <= laststart
	460	then pure (AtPos c)
	461	else fail "Not the end of a block entry"
	462	afterDedent EndOfBlock col = pure EndOfBlock
	463
	464	-- Parse an entry in a block
	465	blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
	466	Rule (ty, ValidIndent)
	467	blockEntry valid rule
	468	= do col <- column
	469	checkValid valid col
	470	p <- rule col
	471	valid' <- terminator valid col
	472	pure (p, valid')
	473
	474	blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
	475	EmptyRule (List ty)
	476	blockEntries valid rule
	477	= do eoi; pure []
	478	<\|> do res <- blockEntry valid rule
	479	ts <- blockEntries (snd res) rule
	480	pure (fst res :: ts)
	481	<\|> pure []
	482
	483	export
	484	block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
	485	block item
	486	= do symbol "{"
	487	commit
	488	ps <- blockEntries AnyIndent item
	489	symbol "}"
	490	pure ps
	491	<\|> do col <- column
	492	blockEntries (AtPos col) item
	493
	494	export
	495	blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
	496	blockAfter mincol item
	497	= do symbol "{"
	498	commit
	499	ps <- blockEntries AnyIndent item
	500	symbol "}"
	501	pure ps
	502	<\|> do col <- column
	503	if col <= mincol
	504	then pure []
	505	else blockEntries (AtPos col) item
	506
	507	export
	508	nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
	509	nonEmptyBlock item
	510	= do symbol "{"
	511	commit
	512	res <- blockEntry AnyIndent item
	513	ps <- blockEntries (snd res) item
	514	symbol "}"
	515	pure (fst res :: ps)
	516	<\|> do col <- column
	517	res <- blockEntry (AtPos col) item
	518	ps <- blockEntries (snd res) item
	519	pure (fst res :: ps)
	520
	521

src/Text/Lexer.idr+324−0

@@ -0,0 +1,324 @@
	1	module Text.Lexer
	2
	3	import Data.Bool.Extra
	4
	5	import public Text.Lexer.Core
	6	import public Text.Quantity
	7	import public Text.Token
	8
	9	%access export
	10	%default total
	11
	12	toTokenMap : List (Lexer, k) -> TokenMap (Token k)
	13	toTokenMap = map $ \(l, kind) => (l, Tok kind)
	14
	15	\|\|\| Recognise any character.
	16	\|\|\| /./
	17	any : Lexer
	18	any = pred (const True)
	19
	20	\|\|\| Recognise a lexer or recognise no input. This is not guaranteed
	21	\|\|\| to consume input.
	22	\|\|\| /`l`?/
	23	opt : (l : Lexer) -> Recognise False
	24	opt l = l <\|> empty
	25
	26	\|\|\| Recognise any character if the sub-lexer `l` fails.
	27	\|\|\| /(?!`l`)./
	28	non : (l : Lexer) -> Lexer
	29	non l = reject l <+> any
	30
	31	\|\|\| Produce recognisers by applying a function to elements of a container, and
	32	\|\|\| recognise the first match. Consumes input if the function produces consuming
	33	\|\|\| recognisers. Fails if the container is empty.
	34	choiceMap : {c : Bool} ->
	35	Foldable t => (a -> Recognise c) -> t a -> Recognise c
	36	choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
	37	f x <\|> acc)
	38	fail xs
	39
	40	\|\|\| Recognise the first matching recogniser in a container. Consumes input if
	41	\|\|\| recognisers in the list consume. Fails if the container is empty.
	42	choice : Foldable t => t (Recognise c) -> Recognise c
	43	choice = choiceMap id
	44
	45	\|\|\| Sequence a list of recognisers. Guaranteed to consume input if the list is
	46	\|\|\| non-empty and the recognisers consume.
	47	concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)
	48	concat = concatMap id
	49
	50	\|\|\| Recognise a specific character.
	51	\|\|\| /[`x`]/
	52	is : (x : Char) -> Lexer
	53	is x = pred (==x)
	54
	55	\|\|\| Recognise anything but the given character.
	56	\|\|\| /[\^`x`]/
	57	isNot : (x : Char) -> Lexer
	58	isNot x = pred (/=x)
	59
	60	\|\|\| Recognise a specific character (case-insensitive).
	61	\|\|\| /[`x`]/i
	62	like : (x : Char) -> Lexer
	63	like x = pred (\y => toUpper x == toUpper y)
	64
	65	\|\|\| Recognise anything but the given character (case-insensitive).
	66	\|\|\| /[\^`x`]/i
	67	notLike : (x : Char) -> Lexer
	68	notLike x = pred (\y => toUpper x /= toUpper y)
	69
	70	\|\|\| Recognise a specific string.
	71	\|\|\| Fails if the string is empty.
	72	\|\|\| /`str`/
	73	exact : (str : String) -> Lexer
	74	exact str = case unpack str of
	75	[] => fail
	76	(x :: xs) => concatMap is (x :: xs)
	77
	78	\|\|\| Recognise a specific string (case-insensitive).
	79	\|\|\| Fails if the string is empty.
	80	\|\|\| /`str`/i
	81	approx : (str : String) -> Lexer
	82	approx str = case unpack str of
	83	[] => fail
	84	(x :: xs) => concatMap like (x :: xs)
	85
	86	\|\|\| Recognise any of the characters in the given string.
	87	\|\|\| /[`chars`]/
	88	oneOf : (chars : String) -> Lexer
	89	oneOf chars = pred (\x => x `elem` unpack chars)
	90
	91	\|\|\| Recognise a character range. Also works in reverse!
	92	\|\|\| /[`start`-`end`]/
	93	range : (start : Char) -> (end : Char) -> Lexer
	94	range start end = pred (\x => (x >= min start end)
	95	&& (x <= max start end))
	96
	97	mutual
	98	\|\|\| Recognise a sequence of at least one sub-lexers
	99	\|\|\| /`l`+/
	100	some : Lexer -> Lexer
	101	some l = l <+> many l
	102
	103	\|\|\| Recognise a sequence of at zero or more sub-lexers. This is not
	104	\|\|\| guaranteed to consume input
	105	\|\|\| /`l`\*/
	106	many : Lexer -> Recognise False
	107	many l = opt (some l)
	108
	109	\|\|\| Repeat the sub-lexer `l` zero or more times until the lexer
	110	\|\|\| `stopBefore` is encountered. `stopBefore` will not be consumed.
	111	\|\|\| Not guaranteed to consume input.
	112	\|\|\| /((?!`stopBefore`)`l`)\*/
	113	manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
	114	manyUntil stopBefore l = many (reject stopBefore <+> l)
	115
	116	\|\|\| Repeat the sub-lexer `l` zero or more times until the lexer
	117	\|\|\| `stopAfter` is encountered, and consume it. Guaranteed to
	118	\|\|\| consume if `stopAfter` consumes.
	119	\|\|\| /`l`\*?`stopAfter`/
	120	manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
	121	manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
	122
	123	\|\|\| Recognise many instances of `l` until an instance of `end` is
	124	\|\|\| encountered.
	125	\|\|\|
	126	\|\|\| Useful for defining comments.
	127	manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
	128	manyTill l end = end <\|> opt (l <+> manyTill l end)
	129	%deprecate manyTill
	130	"Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
	131
	132	\|\|\| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
	133	\|\|\| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
	134	\|\|\| /`l`{`q`}/
	135	count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
	136	count (Qty Z Nothing) l = many l
	137	count (Qty Z (Just Z)) _ = empty
	138	count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l
	139	count (Qty (S min) Nothing) l = l <+> count (atLeast min) l
	140	count (Qty (S min) (Just Z)) _ = fail
	141	count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
	142
	143	\|\|\| Recognise a single digit 0-9
	144	\|\|\| /[0-9]/
	145	digit : Lexer
	146	digit = pred isDigit
	147
	148	\|\|\| Recognise one or more digits
	149	\|\|\| /[0-9]+/
	150	digits : Lexer
	151	digits = some digit
	152
	153	\|\|\| Recognise a single hexidecimal digit
	154	\|\|\| /[0-9A-Fa-f]/
	155	hexDigit : Lexer
	156	hexDigit = pred isHexDigit
	157
	158	\|\|\| Recognise one or more hexidecimal digits
	159	\|\|\| /[0-9A-Fa-f]+/
	160	hexDigits : Lexer
	161	hexDigits = some hexDigit
	162
	163	\|\|\| Recognise a single octal digit
	164	\|\|\| /[0-8]/
	165	octDigit : Lexer
	166	octDigit = pred isHexDigit
	167
	168	\|\|\| Recognise one or more octal digits
	169	\|\|\| /[0-8]+/
	170	octDigits : Lexer
	171	octDigits = some hexDigit
	172
	173	\|\|\| Recognise a single alpha character
	174	\|\|\| /[A-Za-z]/
	175	alpha : Lexer
	176	alpha = pred isAlpha
	177
	178	\|\|\| Recognise one or more alpha characters
	179	\|\|\| /[A-Za-z]+/
	180	alphas : Lexer
	181	alphas = some alpha
	182
	183	\|\|\| Recognise a lowercase alpha character
	184	\|\|\| /[a-z]/
	185	lower : Lexer
	186	lower = pred isLower
	187
	188	\|\|\| Recognise one or more lowercase alpha characters
	189	\|\|\| /[a-z]+/
	190	lowers : Lexer
	191	lowers = some lower
	192
	193	\|\|\| Recognise an uppercase alpha character
	194	\|\|\| /[A-Z]/
	195	upper : Lexer
	196	upper = pred isUpper
	197
	198	\|\|\| Recognise one or more uppercase alpha characters
	199	\|\|\| /[A-Z]+/
	200	uppers : Lexer
	201	uppers = some upper
	202
	203	\|\|\| Recognise an alphanumeric character
	204	\|\|\| /[A-Za-z0-9]/
	205	alphaNum : Lexer
	206	alphaNum = pred isAlphaNum
	207
	208	\|\|\| Recognise one or more alphanumeric characters
	209	\|\|\| /[A-Za-z0-9]+/
	210	alphaNums : Lexer
	211	alphaNums = some alphaNum
	212
	213	\|\|\| Recognise a single whitespace character
	214	\|\|\| /\\s/
	215	space : Lexer
	216	space = pred isSpace
	217
	218	\|\|\| Recognise one or more whitespace characters
	219	\|\|\| /\\s+/
	220	spaces : Lexer
	221	spaces = some space
	222
	223	\|\|\| Recognise a single newline sequence. Understands CRLF, CR, and LF
	224	\|\|\| /\\r\\n\|[\\r\\n]/
	225	newline : Lexer
	226	newline = let crlf = "\r\n" in
	227	exact crlf <\|> oneOf crlf
	228
	229	\|\|\| Recognise one or more newline sequences. Understands CRLF, CR, and LF
	230	\|\|\| /(\\r\\n\|[\\r\\n])+)/
	231	newlines : Lexer
	232	newlines = some newline
	233
	234	\|\|\| Recognise a single non-whitespace, non-alphanumeric character
	235	\|\|\| /[\^\\sA-Za-z0-9]/
	236	symbol : Lexer
	237	symbol = pred (\x => not (isSpace x \|\| isAlphaNum x))
	238
	239	\|\|\| Recognise one or more non-whitespace, non-alphanumeric characters
	240	\|\|\| /[\^\\sA-Za-z0-9]+/
	241	symbols : Lexer
	242	symbols = some symbol
	243
	244	\|\|\| Recognise a single control character
	245	\|\|\| /[\\x00-\\x1f\\x7f-\\x9f]/
	246	control : Lexer
	247	control = pred isControl
	248
	249	\|\|\| Recognise one or more control characters
	250	\|\|\| /[\\x00-\\x1f\\x7f-\\x9f]+/
	251	controls : Lexer
	252	controls = some control
	253
	254	\|\|\| Recognise zero or more occurrences of a sub-lexer between
	255	\|\|\| delimiting lexers
	256	\|\|\| /`start`(`l`)\*?`end`/
	257	surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
	258	surround start end l = start <+> manyThen end l
	259
	260	\|\|\| Recognise zero or more occurrences of a sub-lexer surrounded
	261	\|\|\| by the same quote lexer on both sides (useful for strings)
	262	\|\|\| /`q`(`l`)\*?`q`/
	263	quote : (q : Lexer) -> (l : Lexer) -> Lexer
	264	quote q l = surround q q l
	265
	266	\|\|\| Recognise an escape character (often '\\') followed by a sub-lexer
	267	\|\|\| /[`esc`]`l`/
	268	escape : (esc : Char) -> Lexer -> Lexer
	269	escape esc l = is esc <+> l
	270
	271	\|\|\| Recognise a string literal, including escaped characters.
	272	\|\|\| (Note: doesn't yet handle escape sequences such as \123)
	273	\|\|\| /"(\\\\.\|.)\*?"/
	274	stringLit : Lexer
	275	stringLit = quote (is '"') (escape '\\' any <\|> any)
	276
	277	\|\|\| Recognise a character literal, including escaped characters.
	278	\|\|\| (Note: doesn't yet handle escape sequences such as \123)
	279	\|\|\| /'(\\\\.\|[\^'])'/
	280	charLit : Lexer
	281	charLit = let q = '\'' in
	282	is q <+> (escape '\\' (control <\|> any) <\|> isNot q) <+> is q
	283	where
	284	lexStr : List String -> Lexer
	285	lexStr [] = fail
	286	lexStr (t :: ts) = exact t <\|> lexStr ts
	287
	288	control : Lexer
	289	control = lexStr ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
	290	"BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",
	291	"DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
	292	"CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US",
	293	"SP", "DEL"]
	294	<\|> (is 'x' <+> hexDigits)
	295	<\|> (is 'o' <+> octDigits)
	296	<\|> digits
	297
	298	\|\|\| Recognise an integer literal (possibly with a '-' prefix)
	299	\|\|\| /-?[0-9]+/
	300	intLit : Lexer
	301	intLit = opt (is '-') <+> digits
	302
	303	\|\|\| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
	304	\|\|\| /0[Xx][0-9A-Fa-f]+/
	305	hexLit : Lexer
	306	hexLit = approx "0x" <+> hexDigits
	307
	308	\|\|\| Recognise `start`, then recognise all input until a newline is encountered,
	309	\|\|\| and consume the newline. Will succeed if end-of-input is encountered before
	310	\|\|\| a newline.
	311	\|\|\| /`start`[\^\\r\\n]+(\\r\\n\|[\\r\\n])?/
	312	lineComment : (start : Lexer) -> Lexer
	313	lineComment start = start <+> manyUntil newline any <+> opt newline
	314
	315	\|\|\| Recognise all input between `start` and `end` lexers.
	316	\|\|\| Supports balanced nesting.
	317	\|\|\|
	318	\|\|\| For block comments that don't support nesting (such as C-style comments),
	319	\|\|\| use `surround`
	320	blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
	321	blockComment start end = start <+> middle <+> end
	322	where
	323	middle : Recognise False
	324	middle = manyUntil end (blockComment start end <\|> any)

src/Text/Lexer/Core.idr+192−0

@@ -0,0 +1,192 @@
	1	module Text.Lexer.Core
	2
	3	import Data.Bool.Extra
	4
	5	import public Control.Delayed
	6
	7	%default total
	8
	9	\|\|\| A language of token recognisers.
	10	\|\|\| @ consumes If `True`, this recogniser is guaranteed to consume at
	11	\|\|\| least one character of input when it succeeds.
	12	export
	13	data Recognise : (consumes : Bool) -> Type where
	14	Empty : Recognise False
	15	Fail : Recognise c
	16	Lookahead : (positive : Bool) -> Recognise c -> Recognise False
	17	Pred : (Char -> Bool) -> Recognise True
	18	SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
	19	SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 \|\| e2)
	20	Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
	21
	22	\|\|\| A token recogniser. Guaranteed to consume at least one character.
	23	public export
	24	Lexer : Type
	25	Lexer = Recognise True
	26
	27	\|\|\| Sequence two recognisers. If either consumes a character, the sequence
	28	\|\|\| is guaranteed to consume a character.
	29	export %inline
	30	(<+>) : {c1 : Bool} ->
	31	Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 \|\| c2)
	32	(<+>) {c1 = False} = SeqEmpty
	33	(<+>) {c1 = True} = SeqEat
	34
	35	\|\|\| Alternative recognisers. If both consume, the combination is guaranteed
	36	\|\|\| to consumer a character.
	37	export
	38	(<\|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
	39	(<\|>) = Alt
	40
	41	\|\|\| A recogniser that always fails.
	42	export
	43	fail : Recognise c
	44	fail = Fail
	45
	46	\|\|\| Recognise no input (doesn't consume any input)
	47	export
	48	empty : Recognise False
	49	empty = Empty
	50
	51	\|\|\| Recognise a character that matches a predicate
	52	export
	53	pred : (Char -> Bool) -> Lexer
	54	pred = Pred
	55
	56	\|\|\| Positive lookahead. Never consumes input.
	57	export
	58	expect : Recognise c -> Recognise False
	59	expect = Lookahead True
	60
	61	\|\|\| Negative lookahead. Never consumes input.
	62	export
	63	reject : Recognise c -> Recognise False
	64	reject = Lookahead False
	65
	66	\|\|\| Sequence the recognisers resulting from applying a function to each element
	67	\|\|\| of a list. The resulting recogniser will consume input if the produced
	68	\|\|\| recognisers consume and the list is non-empty.
	69	export
	70	concatMap : {c : Bool} ->
	71	(a -> Recognise c) -> (xs : List a) -> Recognise (c && isCons xs)
	72	concatMap {c} _ [] = rewrite andFalseFalse c in Empty
	73	concatMap {c} f (x :: xs) = rewrite andTrueNeutral c in
	74	rewrite sym (orSameAndRightNeutral c (isCons xs)) in
	75	SeqEmpty (f x) (concatMap f xs)
	76
	77	data StrLen : Type where
	78	MkStrLen : String -> Nat -> StrLen
	79
	80	getString : StrLen -> String
	81	getString (MkStrLen str n) = str
	82
	83	strIndex : StrLen -> Nat -> Maybe Char
	84	strIndex (MkStrLen str len) i
	85	= if cast {to = Integer} i >= cast len then Nothing
	86	else Just (assert_total (prim__strIndex str (cast i)))
	87
	88	mkStr : String -> StrLen
	89	mkStr str = MkStrLen str (length str)
	90
	91	strTail : Nat -> StrLen -> StrLen
	92	strTail start (MkStrLen str len)
	93	= MkStrLen (substr start len str) (minus len start)
	94
	95	-- If the string is recognised, returns the index at which the token
	96	-- ends
	97	scan : Recognise c -> Nat -> StrLen -> Maybe Nat
	98	scan Empty idx str = pure idx
	99	scan Fail idx str = Nothing
	100	scan (Lookahead positive r) idx str
	101	= if isJust (scan r idx str) == positive
	102	then Just idx
	103	else Nothing
	104	scan (Pred f) idx (MkStrLen str len)
	105	= if cast {to = Integer} idx >= cast len
	106	then Nothing
	107	else if f (assert_total (prim__strIndex str (cast idx)))
	108	then Just (idx + 1)
	109	else Nothing
	110	scan (SeqEat r1 r2) idx str
	111	= do idx' <- scan r1 idx str
	112	-- TODO: Can we prove totality instead by showing idx has increased?
	113	assert_total (scan r2 idx' str)
	114	scan (SeqEmpty r1 r2) idx str
	115	= do idx' <- scan r1 idx str
	116	scan r2 idx' str
	117	scan (Alt r1 r2) idx str
	118	= maybe (scan r2 idx str) Just (scan r1 idx str)
	119
	120	takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
	121	takeToken lex str
	122	= do i <- scan lex 0 str -- i must be > 0 if successful
	123	pure (substr 0 i (getString str), strTail i str)
	124
	125	\|\|\| A mapping from lexers to the tokens they produce.
	126	\|\|\| This is a list of pairs `(Lexer, String -> tokenType)`
	127	\|\|\| For each Lexer in the list, if a substring in the input matches, run
	128	\|\|\| the associated function to produce a token of type `tokenType`
	129	public export
	130	TokenMap : (tokenType : Type) -> Type
	131	TokenMap tokenType = List (Lexer, String -> tokenType)
	132
	133	\|\|\| A token, and the line and column where it was in the input
	134	public export
	135	record TokenData a where
	136	constructor MkToken
	137	line : Int
	138	col : Int
	139	tok : a
	140
	141	fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
	142	fspanEnd k p "" = (k, "")
	143	fspanEnd k p xxs
	144	= assert_total $
	145	let x = prim__strHead xxs
	146	xs = prim__strTail xxs in
	147	if p x then fspanEnd (S k) p xs
	148	else (k, xxs)
	149
	150	-- Faster version of 'span' from the prelude (avoids unpacking)
	151	export
	152	fspan : (Char -> Bool) -> String -> (String, String)
	153	fspan p xs
	154	= let (end, rest) = fspanEnd 0 p xs in
	155	(substr 0 end xs, rest)
	156
	157	tokenise : (line : Int) -> (col : Int) ->
	158	List (TokenData a) -> TokenMap a ->
	159	StrLen -> (List (TokenData a), (Int, Int, StrLen))
	160	tokenise line col acc tmap str
	161	= case getFirstToken tmap str of
	162	Just (tok, line', col', rest) =>
	163	-- assert total because getFirstToken must consume something
	164	assert_total (tokenise line' col' (tok :: acc) tmap rest)
	165	Nothing => (reverse acc, (line, col, str))
	166	where
	167	countNLs : List Char -> Nat
	168	countNLs str = List.length (filter (== '\n') str)
	169
	170	getCols : String -> Int -> Int
	171	getCols x c
	172	= case fspan (/= '\n') (reverse x) of
	173	(incol, "") => c + cast (length incol)
	174	(incol, _) => cast (length incol)
	175
	176	getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
	177	getFirstToken [] str = Nothing
	178	getFirstToken ((lex, fn) :: ts) str
	179	= case takeToken lex str of
	180	Just (tok, rest) => Just (MkToken line col (fn tok),
	181	line + cast (countNLs (unpack tok)),
	182	getCols tok col, rest)
	183	Nothing => getFirstToken ts str
	184
	185	\|\|\| Given a mapping from lexers to token generating functions (the
	186	\|\|\| TokenMap a) and an input string, return a list of recognised tokens,
	187	\|\|\| and the line, column, and remainder of the input at the first point in the
	188	\|\|\| string where there are no recognised tokens.
	189	export
	190	lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
	191	lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
	192	(ts, (l, c, getString str'))

src/Text/Parser.idr+226−0

@@ -0,0 +1,226 @@
	1	module Text.Parser
	2
	3	import Data.Bool.Extra
	4
	5	import public Text.Parser.Core
	6	import public Text.Quantity
	7	import public Text.Token
	8
	9	%access export
	10	%default total
	11
	12	\|\|\| Parse a terminal based on a kind of token.
	13	match : (Eq k, TokenKind k) =>
	14	(kind : k) ->
	15	Grammar (Token k) True (TokType kind)
	16	match kind = terminal "Unrecognised input" $
	17	\(Tok kind' text) => if kind' == kind
	18	then Just $ tokValue kind text
	19	else Nothing
	20
	21	\|\|\| Optionally parse a thing, with a default value if the grammar doesn't
	22	\|\|\| match. May match the empty input.
	23	option : {c : Bool} ->
	24	(def : a) -> (p : Grammar tok c a) ->
	25	Grammar tok False a
	26	option {c = False} def p = p <\|> pure def
	27	option {c = True} def p = p <\|> pure def
	28
	29	\|\|\| Optionally parse a thing.
	30	\|\|\| To provide a default value, use `option` instead.
	31	optional : (p : Grammar tok c a) ->
	32	Grammar tok False (Maybe a)
	33	optional p = option Nothing (map Just p)
	34
	35	\|\|\| Try to parse one thing or the other, producing a value that indicates
	36	\|\|\| which option succeeded. If both would succeed, the left option
	37	\|\|\| takes priority.
	38	choose : (l : Grammar tok c1 a) ->
	39	(r : Grammar tok c2 b) ->
	40	Grammar tok (c1 && c2) (Either a b)
	41	choose l r = map Left l <\|> map Right r
	42
	43	\|\|\| Produce a grammar by applying a function to each element of a container,
	44	\|\|\| then try each resulting grammar until the first one succeeds. Fails if the
	45	\|\|\| container is empty.
	46	choiceMap : {c : Bool} ->
	47	(a -> Grammar tok c b) ->
	48	Foldable t => t a ->
	49	Grammar tok c b
	50	choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
	51	f x <\|> acc)
	52	(fail "No more options") xs
	53
	54	\|\|\| Try each grammar in a container until the first one succeeds.
	55	\|\|\| Fails if the container is empty.
	56	choice : Foldable t => t (Grammar tok c a) ->
	57	Grammar tok c a
	58	choice = choiceMap id
	59
	60	mutual
	61	\|\|\| Parse one or more things
	62	some : Grammar tok True a ->
	63	Grammar tok True (List a)
	64	some p = pure (!p :: !(many p))
	65
	66	\|\|\| Parse zero or more things (may match the empty input)
	67	many : Grammar tok True a ->
	68	Grammar tok False (List a)
	69	many p = option [] (some p)
	70
	71	\|\|\| Parse one or more instances of `p`, returning the parsed items and proof
	72	\|\|\| that the resulting list is non-empty.
	73	some' : (p : Grammar tok True a) ->
	74	Grammar tok True (xs : List a ** NonEmpty xs)
	75	some' p = pure (!p :: !(many p) ** IsNonEmpty)
	76
	77	mutual
	78	private
	79	count1 : (q : Quantity) ->
	80	(p : Grammar tok True a) ->
	81	Grammar tok True (List a)
	82	count1 q p = do x <- p
	83	seq (count q p)
	84	(\xs => pure (x :: xs))
	85
	86	\|\|\| Parse `p`, repeated as specified by `q`, returning the list of values.
	87	count : (q : Quantity) ->
	88	(p : Grammar tok True a) ->
	89	Grammar tok (isSucc (min q)) (List a)
	90	count (Qty Z Nothing) p = many p
	91	count (Qty Z (Just Z)) _ = pure []
	92	count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
	93	count (Qty (S min) Nothing) p = count1 (atLeast min) p
	94	count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
	95	count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p
	96
	97	mutual
	98	\|\|\| Parse one or more instances of `p` until `end` succeeds, returning the
	99	\|\|\| list of values from `p`. Guaranteed to consume input.
	100	someTill : {c : Bool} ->
	101	(end : Grammar tok c e) ->
	102	(p : Grammar tok True a) ->
	103	Grammar tok True (List a)
	104	someTill {c} end p = do x <- p
	105	seq (manyTill end p)
	106	(\xs => pure (x :: xs))
	107
	108	\|\|\| Parse zero or more instances of `p` until `end` succeeds, returning the
	109	\|\|\| list of values from `p`. Guaranteed to consume input if `end` consumes.
	110	manyTill : {c : Bool} ->
	111	(end : Grammar tok c e) ->
	112	(p : Grammar tok True a) ->
	113	Grammar tok c (List a)
	114	manyTill {c} end p = rewrite sym (andTrueNeutral c) in
	115	map (const []) end <\|> someTill end p
	116
	117	\|\|\| Parse one or more instances of `p` until `end` succeeds, returning the
	118	\|\|\| list of values from `p`, along with a proof that the resulting list is
	119	\|\|\| non-empty.
	120	someTill' : {c : Bool} ->
	121	(end : Grammar tok c e) ->
	122	(p : Grammar tok True a) ->
	123	Grammar tok True (xs : List a ** NonEmpty xs)
	124	someTill' end p
	125	= do x <- p
	126	seq (manyTill end p)
	127	(\xs => pure (x :: xs ** IsNonEmpty))
	128
	129	mutual
	130	\|\|\| Parse one or more instance of `skip` until `p` is encountered,
	131	\|\|\| returning its value.
	132	afterSome : (skip : Grammar tok True s) ->
	133	(p : Grammar tok c a) ->
	134	Grammar tok True a
	135	afterSome skip p = do skip
	136	afterMany skip p
	137
	138	\|\|\| Parse zero or more instance of `skip` until `p` is encountered,
	139	\|\|\| returning its value.
	140	afterMany : {c : Bool} ->
	141	(skip : Grammar tok True s) ->
	142	(p : Grammar tok c a) ->
	143	Grammar tok c a
	144	afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
	145	p <\|> afterSome skip p
	146
	147	\|\|\| Parse one or more things, each separated by another thing.
	148	sepBy1 : {c : Bool} ->
	149	(sep : Grammar tok True s) ->
	150	(p : Grammar tok c a) ->
	151	Grammar tok c (List a)
	152	sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
	153	[\| p :: many (sep *> p) \|]
	154
	155	\|\|\| Parse zero or more things, each separated by another thing. May
	156	\|\|\| match the empty input.
	157	sepBy : (sep : Grammar tok True s) ->
	158	(p : Grammar tok c a) ->
	159	Grammar tok False (List a)
	160	sepBy sep p = option [] $ sepBy1 sep p
	161
	162	\|\|\| Parse one or more instances of `p` separated by `sep`, returning the
	163	\|\|\| parsed items and proof that the resulting list is non-empty.
	164	sepBy1' : {c : Bool} ->
	165	(sep : Grammar tok True s) ->
	166	(p : Grammar tok c a) ->
	167	Grammar tok c (xs : List a ** NonEmpty xs)
	168	sepBy1' {c} sep p
	169	= rewrite sym (orFalseNeutral c) in
	170	seq p (\x => do xs <- many (sep *> p)
	171	pure (x :: xs ** IsNonEmpty))
	172
	173	\|\|\| Parse one or more instances of `p` separated by and optionally terminated by
	174	\|\|\| `sep`.
	175	sepEndBy1 : {c : Bool} ->
	176	(sep : Grammar tok True s) ->
	177	(p : Grammar tok c a) ->
	178	Grammar tok c (List a)
	179	sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
	180	sepBy1 sep p <* optional sep
	181
	182	\|\|\| Parse zero or more instances of `p`, separated by and optionally terminated
	183	\|\|\| by `sep`. Will not match a separator by itself.
	184	sepEndBy : (sep : Grammar tok True s) ->
	185	(p : Grammar tok c a) ->
	186	Grammar tok False (List a)
	187	sepEndBy sep p = option [] $ sepEndBy1 sep p
	188
	189	\|\|\| Parse zero or more instances of `p`, separated by and optionally terminated
	190	\|\|\| by `sep`, returning the parsed items and a proof that the resulting list
	191	\|\|\| is non-empty.
	192	sepEndBy1' : {c : Bool} ->
	193	(sep : Grammar tok True s) ->
	194	(p : Grammar tok c a) ->
	195	Grammar tok c (xs : List a ** NonEmpty xs)
	196	sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in
	197	sepBy1' sep p <* optional sep
	198
	199	\|\|\| Parse one or more instances of `p`, separated and terminated by `sep`.
	200	endBy1 : {c : Bool} ->
	201	(sep : Grammar tok True s) ->
	202	(p : Grammar tok c a) ->
	203	Grammar tok True (List a)
	204	endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
	205	p <* sep
	206
	207	endBy : (sep : Grammar tok True s) ->
	208	(p : Grammar tok c a) ->
	209	Grammar tok False (List a)
	210	endBy sep p = option [] $ endBy1 sep p
	211
	212	\|\|\| Parse zero or more instances of `p`, separated and terminated by `sep`,
	213	\|\|\| returning the parsed items and a proof that the resulting list is non-empty.
	214	endBy1' : {c : Bool} ->
	215	(sep : Grammar tok True s) ->
	216	(p : Grammar tok c a) ->
	217	Grammar tok True (xs : List a ** NonEmpty xs)
	218	endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in
	219	p <* sep
	220
	221	\|\|\| Parse an instance of `p` that is between `left` and `right`.
	222	between : (left : Grammar tok True l) ->
	223	(right : Grammar tok True r) ->
	224	(p : Grammar tok c a) ->
	225	Grammar tok True a
	226	between left right contents = left > contents < right

src/Text/Parser/Core.idr+284−0

@@ -0,0 +1,284 @@
	1	module Text.Parser.Core
	2
	3	import public Control.Delayed
	4
	5	%default total
	6
	7	-- TODO: Add some primitives for helping with error messages.
	8	-- e.g. perhaps set a string to state what we're currently trying to
	9	-- parse, or to say what the next expected token is in words
	10
	11	\|\|\| Description of a language's grammar. The `tok` parameter is the type
	12	\|\|\| of tokens, and the `consumes` flag is True if the language is guaranteed
	13	\|\|\| to be non-empty - that is, successfully parsing the language is guaranteed
	14	\|\|\| to consume some input.
	15	export
	16	data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
	17	Empty : (val : ty) -> Grammar tok False ty
	18	Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
	19	NextIs : String -> (tok -> Bool) -> Grammar tok False tok
	20	EOF : Grammar tok False ()
	21
	22	Fail : Bool -> String -> Grammar tok c ty
	23	Commit : Grammar tok False ()
	24	MustWork : Grammar tok c a -> Grammar tok c a
	25
	26	SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
	27	Grammar tok True b
	28	SeqEmpty : {c1, c2 : Bool} ->
	29	Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
	30	Grammar tok (c1 \|\| c2) b
	31	Alt : {c1, c2 : Bool} ->
	32	Grammar tok c1 ty -> Grammar tok c2 ty ->
	33	Grammar tok (c1 && c2) ty
	34
	35	\|\|\| Sequence two grammars. If either consumes some input, the sequence is
	36	\|\|\| guaranteed to consume some input. If the first one consumes input, the
	37	\|\|\| second is allowed to be recursive (because it means some input has been
	38	\|\|\| consumed and therefore the input is smaller)
	39	export %inline
	40	(>>=) : {c1 : Bool} ->
	41	Grammar tok c1 a ->
	42	inf c1 (a -> Grammar tok c2 b) ->
	43	Grammar tok (c1 \|\| c2) b
	44	(>>=) {c1 = False} = SeqEmpty
	45	(>>=) {c1 = True} = SeqEat
	46
	47	\|\|\| Sequence two grammars. If either consumes some input, the sequence is
	48	\|\|\| guaranteed to consume input. This is an explicitly non-infinite version
	49	\|\|\| of `>>=`.
	50	export
	51	seq : Grammar tok c1 a ->
	52	(a -> Grammar tok c2 b) ->
	53	Grammar tok (c1 \|\| c2) b
	54	seq = SeqEmpty
	55
	56	\|\|\| Sequence a grammar followed by the grammar it returns.
	57	export
	58	join : {c1 : Bool} ->
	59	Grammar tok c1 (Grammar tok c2 a) ->
	60	Grammar tok (c1 \|\| c2) a
	61	join {c1 = False} p = SeqEmpty p id
	62	join {c1 = True} p = SeqEat p id
	63
	64	\|\|\| Give two alternative grammars. If both consume, the combination is
	65	\|\|\| guaranteed to consume.
	66	export
	67	(<\|>) : Grammar tok c1 ty ->
	68	Grammar tok c2 ty ->
	69	Grammar tok (c1 && c2) ty
	70	(<\|>) = Alt
	71
	72	\|\|\| Allows the result of a grammar to be mapped to a different value.
	73	export
	74	Functor (Grammar tok c) where
	75	map f (Empty val) = Empty (f val)
	76	map f (Fail fatal msg) = Fail fatal msg
	77	map f (MustWork g) = MustWork (map f g)
	78	map f (Terminal msg g) = Terminal msg (\t => map f (g t))
	79	map f (Alt x y) = Alt (map f x) (map f y)
	80	map f (SeqEat act next)
	81	= SeqEat act (\val => map f (next val))
	82	map f (SeqEmpty act next)
	83	= SeqEmpty act (\val => map f (next val))
	84	-- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
	85	-- so a sequence must be used.
	86	map {c = False} f p = SeqEmpty p (Empty . f)
	87
	88	\|\|\| Sequence a grammar with value type `a -> b` and a grammar
	89	\|\|\| with value type `a`. If both succeed, apply the function
	90	\|\|\| from the first grammar to the value from the second grammar.
	91	\|\|\| Guaranteed to consume if either grammar consumes.
	92	export
	93	(<*>) : Grammar tok c1 (a -> b) ->
	94	Grammar tok c2 a ->
	95	Grammar tok (c1 \|\| c2) b
	96	(<*>) x y = SeqEmpty x (\f => map f y)
	97
	98	\|\|\| Sequence two grammars. If both succeed, use the value of the first one.
	99	\|\|\| Guaranteed to consume if either grammar consumes.
	100	export
	101	(<*) : Grammar tok c1 a ->
	102	Grammar tok c2 b ->
	103	Grammar tok (c1 \|\| c2) a
	104	(<) x y = map const x <> y
	105
	106	\|\|\| Sequence two grammars. If both succeed, use the value of the second one.
	107	\|\|\| Guaranteed to consume if either grammar consumes.
	108	export
	109	(*>) : Grammar tok c1 a ->
	110	Grammar tok c2 b ->
	111	Grammar tok (c1 \|\| c2) b
	112	(>) x y = map (const id) x <> y
	113
	114	\|\|\| Produce a grammar that can parse a different type of token by providing a
	115	\|\|\| function converting the new token type into the original one.
	116	export
	117	mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
	118	mapToken f (Empty val) = Empty val
	119	mapToken f (Terminal msg g) = Terminal msg (g . f)
	120	mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
	121	mapToken f EOF = EOF
	122	mapToken f (Fail fatal msg) = Fail fatal msg
	123	mapToken f (MustWork g) = MustWork (mapToken f g)
	124	mapToken f Commit = Commit
	125	mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))
	126	mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
	127	mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
	128
	129	\|\|\| Always succeed with the given value.
	130	export
	131	pure : (val : ty) -> Grammar tok False ty
	132	pure = Empty
	133
	134	\|\|\| Check whether the next token satisfies a predicate
	135	export
	136	nextIs : String -> (tok -> Bool) -> Grammar tok False tok
	137	nextIs = NextIs
	138
	139	\|\|\| Look at the next token in the input
	140	export
	141	peek : Grammar tok False tok
	142	peek = nextIs "Unrecognised token" (const True)
	143
	144	\|\|\| Succeeds if running the predicate on the next token returns Just x,
	145	\|\|\| returning x. Otherwise fails.
	146	export
	147	terminal : String -> (tok -> Maybe a) -> Grammar tok True a
	148	terminal = Terminal
	149
	150	\|\|\| Always fail with a message
	151	export
	152	fail : String -> Grammar tok c ty
	153	fail = Fail False
	154
	155	export
	156	fatalError : String -> Grammar tok c ty
	157	fatalError = Fail True
	158
	159	\|\|\| Succeed if the input is empty
	160	export
	161	eof : Grammar tok False ()
	162	eof = EOF
	163
	164	\|\|\| Commit to an alternative; if the current branch of an alternative
	165	\|\|\| fails to parse, no more branches will be tried
	166	export
	167	commit : Grammar tok False ()
	168	commit = Commit
	169
	170	\|\|\| If the parser fails, treat it as a fatal error
	171	export
	172	mustWork : Grammar tok c ty -> Grammar tok c ty
	173	mustWork = MustWork
	174
	175	data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
	176	Failure : {xs : List tok} ->
	177	(committed : Bool) -> (fatal : Bool) ->
	178	(err : String) -> (rest : List tok) -> ParseResult xs c ty
	179	EmptyRes : (committed : Bool) ->
	180	(val : ty) -> (more : List tok) -> ParseResult more False ty
	181	NonEmptyRes : (committed : Bool) ->
	182	(val : ty) -> (more : List tok) ->
	183	ParseResult (x :: xs ++ more) c ty
	184
	185	-- Take the result of an alternative branch, reset the commit flag to
	186	-- the commit flag from the outer alternative, and weaken the 'consumes'
	187	-- flag to take both alternatives into account
	188	weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
	189	(com' : Bool) ->
	190	ParseResult xs c ty -> ParseResult xs (whatever && c) ty
	191	weakenRes com' (Failure com fatal msg ts) = Failure com' fatal msg ts
	192	weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
	193	weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
	194	weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
	195
	196	shorter : (more : List tok) -> .(ys : List tok) ->
	197	LTE (S (length more)) (S (length (ys ++ more)))
	198	shorter more [] = lteRefl
	199	shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
	200
	201	doParse : {c : Bool} ->
	202	(commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
	203	ParseResult xs c ty
	204	-- doParse com xs act with (sizeAccessible xs)
	205	doParse com xs (Empty val) = EmptyRes com val xs
	206	doParse com [] (Fail fatal str) = Failure com fatal str []
	207	doParse com (x :: xs) (Fail fatal str) = Failure com fatal str (x :: xs)
	208	doParse com xs Commit = EmptyRes True () xs
	209	doParse com xs (MustWork g) =
	210	let p' = doParse com xs g in
	211	case p' of
	212	Failure com' _ msg ts => Failure com' True msg ts
	213	res => res
	214	doParse com [] (Terminal err f) = Failure com False "End of input" []
	215	doParse com (x :: xs) (Terminal err f)
	216	= maybe
	217	(Failure com False err (x :: xs))
	218	(\a => NonEmptyRes com {xs=[]} a xs)
	219	(f x)
	220	doParse com [] EOF = EmptyRes com () []
	221	doParse com (x :: xs) EOF
	222	= Failure com False "Expected end of input" (x :: xs)
	223	doParse com [] (NextIs err f) = Failure com False "End of input" []
	224	doParse com (x :: xs) (NextIs err f)
	225	= if f x
	226	then EmptyRes com x (x :: xs)
	227	else Failure com False err (x :: xs)
	228	doParse com xs (Alt x y)
	229	= let p' = doParse False xs x in
	230	case p' of
	231	Failure com' fatal msg ts
	232	=> if com' \|\| fatal
	233	-- If the alternative had committed, don't try the
	234	-- other branch (and reset commit flag)
	235	then Failure com fatal msg ts
	236	else weakenRes com (doParse False xs y)
	237	-- Successfully parsed the first option, so use the outer commit flag
	238	EmptyRes _ val xs => EmptyRes com val xs
	239	NonEmptyRes _ val more => NonEmptyRes com val more
	240	doParse com xs (SeqEmpty act next)
	241	= let p' = assert_total (doParse com xs act) in
	242	case p' of
	243	Failure com fatal msg ts => Failure com fatal msg ts
	244	EmptyRes com val xs =>
	245	case assert_total (doParse com xs (next val)) of
	246	Failure com' fatal msg ts => Failure com' fatal msg ts
	247	EmptyRes com' val xs => EmptyRes com' val xs
	248	NonEmptyRes com' val more => NonEmptyRes com' val more
	249	NonEmptyRes {x} {xs=ys} com val more =>
	250	case (assert_total (doParse com more (next val))) of
	251	Failure com' fatal msg ts => Failure com' fatal msg ts
	252	EmptyRes com' val _ => NonEmptyRes com' val more
	253	NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
	254	rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
	255	NonEmptyRes com' val more'
	256	doParse com xs (SeqEat act next) with (doParse com xs act)
	257	doParse com xs (SeqEat act next) \| Failure com' fatal msg ts
	258	= Failure com' fatal msg ts
	259	doParse com (x :: (ys ++ more)) (SeqEat act next) \| (NonEmptyRes com' val more)
	260	= let p' = assert_total (doParse com' more (next val)) in
	261	case p' of
	262	Failure com' fatal msg ts => Failure com' fatal msg ts
	263	EmptyRes com' val _ => NonEmptyRes com' val more
	264	NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
	265	rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
	266	NonEmptyRes com' val more'
	267	-- This next line is not strictly necessary, but it stops the coverage
	268	-- checker taking a really long time and eating lots of memory...
	269	-- doParse _ _ _ \| sml = Failure True "Help the coverage checker!" []
	270
	271	public export
	272	data ParseError tok = Error String (List tok)
	273
	274	\|\|\| Parse a list of tokens according to the given grammar. If successful,
	275	\|\|\| returns a pair of the parse result and the unparsed tokens (the remaining
	276	\|\|\| input).
	277	export
	278	parse : (act : Grammar tok c ty) -> (xs : List tok) ->
	279	Either (ParseError tok) (ty, List tok)
	280	parse act xs
	281	= case doParse False xs act of
	282	Failure _ _ msg ts => Left (Error msg ts)
	283	EmptyRes _ val rest => pure (val, rest)
	284	NonEmptyRes _ val rest => pure (val, rest)

src/Text/Quantity.idr+38−0

@@ -0,0 +1,38 @@
	1	module Text.Quantity
	2
	3	%access public export
	4	%default total
	5
	6	record Quantity where
	7	constructor Qty
	8	min : Nat
	9	max : Maybe Nat
	10
	11	Show Quantity where
	12	show (Qty Z Nothing) = "*"
	13	show (Qty Z (Just (S Z))) = "?"
	14	show (Qty (S Z) Nothing) = "+"
	15	show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
	16	where
	17	showMax : String
	18	showMax = case max of
	19	Nothing => ","
	20	Just max' => if min == max'
	21	then ""
	22	else "," ++ show max'
	23
	24	between : Nat -> Nat -> Quantity
	25	between min max = Qty min (Just max)
	26
	27	atLeast : Nat -> Quantity
	28	atLeast min = Qty min Nothing
	29
	30	atMost : Nat -> Quantity
	31	atMost max = Qty 0 (Just max)
	32
	33	exactly : Nat -> Quantity
	34	exactly n = Qty n (Just n)
	35
	36	inOrder : Quantity -> Bool
	37	inOrder (Qty min Nothing) = True
	38	inOrder (Qty min (Just max)) = min <= max

src/Text/Token.idr+38−0

@@ -0,0 +1,38 @@
	1	module Text.Token
	2
	3	%access public export
	4	%default total
	5
	6	\|\|\| For a type `kind`, specify a way of converting the recognised
	7	\|\|\| string into a value.
	8	\|\|\|
	9	\|\|\| ```idris example
	10	\|\|\| data SimpleKind = SKString \| SKInt \| SKComma
	11	\|\|\|
	12	\|\|\| TokenKind SimpleKind where
	13	\|\|\| TokType SKString = String
	14	\|\|\| TokType SKInt = Int
	15	\|\|\| TokType SKComma = ()
	16	\|\|\|
	17	\|\|\| tokValue SKString x = x
	18	\|\|\| tokValue SKInt x = cast x
	19	\|\|\| tokValue SKComma x = ()
	20	\|\|\| ```
	21	interface TokenKind (k : Type) where
	22	\|\|\| The type that a token of this kind converts to.
	23	TokType : k -> Type
	24
	25	\|\|\| Convert a recognised string into a value. The type is determined
	26	\|\|\| by the kind of token.
	27	tokValue : (kind : k) -> String -> TokType kind
	28
	29	\|\|\| A token of a particular kind and the text that was recognised.
	30	record Token k where
	31	constructor Tok
	32	kind : k
	33	text : String
	34
	35	\|\|\| Get the value of a `Token k`. The resulting type depends upon
	36	\|\|\| the kind of token.
	37	value : TokenKind k => (t : Token k) -> TokType (kind t)
	38	value (Tok k x) = tokValue k x

yaffle.ipkg+31−0

@@ -0,0 +1,31 @@
	1	package yaffle
	2
	3	modules =
	4	Control.Delayed,
	5
	6	Core.Core,
	7	Core.Env,
	8	Core.FC,
	9	Core.Name,
	10	Core.TT,
	11	Core.Value,
	12
	13	Data.Bool.Extra,
	14	Data.StringMap,
	15
	16	Parser.Lexer,
	17	Parser.Support,
	18
	19	Text.Lexer,
	20	Text.Lexer.Core,
	21	Text.Parser,
	22	Text.Parser.Core,
	23	Text.Quantity,
	24	Text.Token
	25
	26	sourcedir = src
	27	-- executable = ttimp
	28	opts = "--partial-eval"
	29
	30	-- main = TTImp.Main
	31

Initial structure

Keyboard shortcuts

General

Issues and pull requests

Issues, pull requests and Inbox

Repository code