@@ -39,14 +39,14 @@ data InState : Var -> Type -> Resources -> Type where
3939
4040{- Update an entry in a context with a new state -}
4141public export
42−updateRes : (res : Resources) ->
42+updateRes : (res : Resources) ->
4343 InState lbl st res -> Type -> Resources
4444updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
4545updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty
4646
4747{- Remove an entry from a context -}
4848public export
49−drop : (res : Resources) -> (prf : InState lbl st res) ->
49+drop : (res : Resources) -> (prf : InState lbl st res) ->
5050 Resources
5151drop (MkRes lbl st :: rs) Here = rs
5252drop (r :: rs) (There p) = r :: drop rs p
@@ -128,10 +128,10 @@ updateWith : (new : Resources) -> (xs : Resources) ->
128128updateWith new [] SubNil = new
129129updateWith new [] (InRes el z) = absurd el
130130-- Don't add the ones which were consumed by the subctxt
131−updateWith [] (x :: xs) (InRes el p)
131+updateWith [] (x :: xs) (InRes el p)
132132 = updateWith [] (dropEl _ el) p
133133-- A new item corresponding to an existing thing
134−updateWith (n :: ns) (x :: xs) (InRes el p)
134+updateWith (n :: ns) (x :: xs) (InRes el p)
135135 = n :: updateWith ns (dropEl _ el) p
136136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137137
@@ -154,7 +154,7 @@ dropCombined {res = (y :: ys)} (SkipVar x) = y :: dropCombined x
154154
155155public export
156156combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources
157−combineVarsIn {comp} res (InResVar el x)
157+combineVarsIn {comp} res (InResVar el x)
158158 = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x))
159159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160160
@@ -172,7 +172,7 @@ lookupEnv : InState lbl ty res -> Env res -> ty
172172lookupEnv Here (x :: xs) = x
173173lookupEnv (There p) (x :: xs) = lookupEnv p xs
174174
175−updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->
175+updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->
176176 Env (updateRes res prf ty')
177177updateEnv Here (x :: xs) val = val :: xs
178178updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val
@@ -205,20 +205,20 @@ getVarEntry (x :: env) (VarThere p) = getVarEntry env p
205205
206206mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf)
207207mkComposite [] VarsNil = CompNil
208−mkComposite env (InResVar el z)
208+mkComposite env (InResVar el z)
209209 = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)
210210mkComposite (x :: env) (SkipVar z) = mkComposite env z
211211
212−rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->
212+rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->
213213 Env (combineVarsIn res prf)
214−rebuildVarsIn env (InResVar el p)
214+rebuildVarsIn env (InResVar el p)
215215 = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p)
216216rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p
217217
218218{- Some things to make STrans interfaces look prettier -}
219219
220220infix 6 :->
221−
221+
222222public export
223223data Action : Type -> Type where
224224 Stable : Var -> Type -> Action ty
@@ -254,7 +254,7 @@ or x y = either (const x) (const y)
254254public export %error_reduce
255255add : Type -> Action Var
256256add ty = Add (\var => [var ::: ty])
257−
257+
258258public export %error_reduce
259259remove : Var -> Type -> Action ty
260260remove = Remove
@@ -285,17 +285,17 @@ data STrans : (m : Type -> Type) ->
285285 (ty : Type) ->
286286 Resources -> (ty -> Resources) ->
287287 Type where
288− Pure : (result : ty) ->
288+ Pure : (result : ty) ->
289289 STrans m ty (out_fn result) out_fn
290290 Bind : STrans m a st1 st2_fn ->
291− ((result : a) ->
291+ ((result : a) ->
292292 STrans m b (st2_fn result) st3_fn) ->
293293 STrans m b st1 st3_fn
294294 Lift : Monad m => m t -> STrans m t res (const res)
295− RunAs : Applicative m => STrans m t in_res (const out_res) ->
295+ RunAs : Applicative m => STrans m t in_res (const out_res) ->
296296 STrans m (m t) in_res (const out_res)
297297
298− New : (val : state) ->
298+ New : (val : state) ->
299299 STrans m Var res (\lbl => (lbl ::: state) :: res)
300300 Delete : (lbl : Var) ->
301301 (prf : InState lbl st res) ->
@@ -305,8 +305,8 @@ data STrans : (m : Type -> Type) ->
305305
306306 Split : (lbl : Var) ->
307307 (prf : InState lbl (Composite vars) res) ->
308− STrans m (VarList vars) res
309− (\ vs => mkRes vs ++
308+ STrans m (VarList vars) res
309+ (\ vs => mkRes vs ++
310310 updateRes res prf (State ()))
311311 Combine : (comp : Var) -> (vs : List Var) ->
312312 (prf : VarsIn (comp :: vs) res) ->
@@ -340,7 +340,7 @@ export
340340dropEnv : Env ys -> SubRes xs ys -> Env xs
341341dropEnv [] SubNil = []
342342dropEnv [] (InRes idx rest) = absurd idx
343−dropEnv (z :: zs) (InRes idx rest)
343+dropEnv (z :: zs) (InRes idx rest)
344344 = let [e] = envElem idx (z :: zs) in
345345 e :: dropEnv (dropDups (z :: zs) idx) rest
346346dropEnv (z :: zs) (Skip p) = dropEnv zs p
@@ -355,25 +355,25 @@ rebuildEnv : Env new -> Env old -> (prf : SubRes sub old) ->
355355 Env (updateWith new old prf)
356356rebuildEnv new [] SubNil = new
357357rebuildEnv new [] (InRes el p) = absurd el
358−rebuildEnv [] (x :: xs) (InRes el p)
358+rebuildEnv [] (x :: xs) (InRes el p)
359359 = rebuildEnv [] (dropDups (x :: xs) el) p
360−rebuildEnv (e :: es) (x :: xs) (InRes el p)
360+rebuildEnv (e :: es) (x :: xs) (InRes el p)
361361 = e :: rebuildEnv es (dropDups (x :: xs) el) p
362362rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p
363363
364364runST : Env invars -> STrans m a invars outfn ->
365365 ((x : a) -> Env (outfn x) -> m b) -> m b
366366runST env (Pure result) k = k result env
367−runST env (Bind prog next) k
367+runST env (Bind prog next) k
368368 = runST env prog (\prog', env' => runST env' (next prog') k)
369−runST env (Lift action) k
369+runST env (Lift action) k
370370 = do res <- action
371371 k res env
372372runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
373373runST env (New val) k = k MkVar (val :: env)
374374runST env (Delete lbl prf) k = k () (dropVal prf env)
375375runST env (DropSubRes prf) k = k (dropEnv env prf) (keepEnv env prf)
376−runST env (Split lbl prf) k = let val = lookupEnv prf env
376+runST env (Split lbl prf) k = let val = lookupEnv prf env
377377 env' = updateEnv prf env (Value ()) in
378378 k (mkVars val) (addToEnv val env')
379379 where
@@ -386,7 +386,7 @@ runST env (Split lbl prf) k = let val = lookupEnv prf env
386386 addToEnv (CompCons x xs) env = x :: addToEnv xs env
387387runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
388388runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
389−runST env (Call prog res_prf) k
389+runST env (Call prog res_prf) k
390390 = let env' = dropEnv env res_prf in
391391 runST env' prog
392392 (\prog', envk => k prog' (rebuildEnv envk env res_prf))
@@ -404,15 +404,15 @@ runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
404404 (k : (x : a) -> Env (outfn x) -> m b) ->
405405 (onDry : m b) -> m b
406406runSTLoop Empty _ _ _ onDry = onDry
407−runSTLoop (More x) env (Bind prog next) k onDry
407+runSTLoop (More x) env (Bind prog next) k onDry
408408 = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry)
409409runSTLoop (More x) env (Pure result) k onDry = k result env
410410
411−export
411+export
412412pure : (result : ty) -> STrans m ty (out_fn result) out_fn
413413pure = Pure
414414
415−export
415+export
416416(>>=) : STrans m a st1 st2_fn ->
417417 ((result : a) -> STrans m b (st2_fn result) st3_fn) ->
418418 STrans m b st1 st3_fn
@@ -423,19 +423,19 @@ returning : (result : ty) -> STrans m () res (const (out_fn result)) ->
423423 STrans m ty res out_fn
424424returning res prog = do prog
425425 pure res
426−
426+
427427
428428export
429429lift : Monad m => m t -> STrans m t res (const res)
430430lift = Lift
431431
432432export
433−runAs : Applicative m => STrans m t in_res (const out_res) ->
433+runAs : Applicative m => STrans m t in_res (const out_res) ->
434434 STrans m (m t) in_res (const out_res)
435435runAs = RunAs
436436
437437export
438−new : (val : state) ->
438+new : (val : state) ->
439439 STrans m Var res (\lbl => (lbl ::: State state) :: res)
440440new val = New (Value val)
441441
@@ -455,8 +455,8 @@ dropSub {prf} = DropSubRes prf
455455export
456456split : (lbl : Var) ->
457457 {auto prf : InState lbl (Composite vars) res} ->
458− STrans m (VarList vars) res
459− (\ vs => mkRes vs ++
458+ STrans m (VarList vars) res
459+ (\ vs => mkRes vs ++
460460 updateRes res prf (State ()))
461461split lbl {prf} = Split lbl prf
462462
@@ -467,7 +467,7 @@ combine : (comp : Var) -> (vs : List Var) ->
467467 STrans m () res
468468 (const (combineVarsIn res var_prf))
469469combine comp vs {var_prf} = Combine comp vs var_prf
470−
470+
471471export
472472toEnd : (lbl : Var) ->
473473 {auto prf : InState lbl state res} ->
@@ -479,7 +479,7 @@ call : STrans m t sub new_f ->
479479 {auto res_prf : SubRes sub old} ->
480480 STrans m t old (\res => updateWith (new_f res) old res_prf)
481481call prog {res_prf} = Call prog res_prf
482−
482+
483483export
484484read : (lbl : Var) ->
485485 {auto prf : InState lbl (State ty) res} ->
@@ -493,7 +493,7 @@ write : (lbl : Var) ->
493493 (val : ty') ->
494494 STrans m () res (const (updateRes res prf (State ty')))
495495write lbl {prf} val = Write lbl prf (Value val)
496−
496+
497497export
498498update : (lbl : Var) ->
499499 {auto prf : InState lbl (State ty) res} ->
@@ -512,12 +512,12 @@ namespace Loop
512512 export
513513 pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
514514 pure = Pure
515−
515+
516516public export %error_reduce
517517out_res : ty -> (as : List (Action ty)) -> Resources
518518out_res x [] = []
519519out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs
520−out_res x ((Trans lbl inr outr) :: xs)
520+out_res x ((Trans lbl inr outr) :: xs)
521521 = (lbl ::: outr x) :: out_res x xs
522522out_res x ((Remove lbl inr) :: xs) = out_res x xs
523523out_res x (Add outf :: xs) = outf x ++ out_res x xs
@@ -533,14 +533,14 @@ in_res (Add outf :: xs) = in_res xs
533533public export
534534%error_reduce -- always evaluate this before showing errors
535535ST : (m : Type -> Type) ->
536− (ty : Type) ->
536+ (ty : Type) ->
537537 List (Action ty) -> Type
538538ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)
539539
540540public export
541541%error_reduce -- always evaluate this before showing errors
542542STLoop : (m : Type -> Type) ->
543− (ty : Type) ->
543+ (ty : Type) ->
544544 List (Action ty) -> Type
545545STLoop m ty xs = STransLoop m ty (in_res xs) (\result : ty => out_res result xs)
546546
@@ -550,22 +550,36 @@ interface ConsoleIO (m : Type -> Type) where
550550 putStr : String -> STrans m () xs (const xs)
551551 getStr : STrans m String xs (const xs)
552552
553+ putChar : Char -> STrans m () xs (const xs)
554+ getChar : STrans m Char xs (const xs)
555+
556+
553557export
554558putStrLn : ConsoleIO m => String -> STrans m () xs (const xs)
555559putStrLn str = putStr (str ++ "\n")
556560
561+export
562+print : (ConsoleIO m, Show a) => a -> STrans m () xs (const xs)
563+print a = putStr $ show a
564+
565+export
566+printLn : (ConsoleIO m, Show a) => a -> STrans m () xs (const xs)
567+printLn a = putStrLn $ show a
568+
557569export
558570ConsoleIO IO where
559571 putStr str = lift (Interactive.putStr str)
560572 getStr = lift Interactive.getLine
561573
574+ putChar c = lift $ Interactive.putChar c
575+ getChar = lift Interactive.getChar
562576
563577export
564578run : Applicative m => ST m a [] -> m a
565579run prog = runST [] prog (\res, env' => pure res)
566580
567581export
568−runLoop : Applicative m => Fuel -> STLoop m a [] ->
582+runLoop : Applicative m => Fuel -> STLoop m a [] ->
569583 (onEmpty : m a) ->
570584 m a
571585runLoop fuel prog onEmpty
@@ -580,16 +594,16 @@ runLoop fuel prog onEmpty
580594||| to ensure that it isn't duplicated.
581595export
582596runWith : {resf : _} ->
583− Env res -> STrans IO a res (\result => resf result) ->
597+ Env res -> STrans IO a res (\result => resf result) ->
584598 IO (result ** Env (resf result))
585599runWith env prog = runST env prog (\res, env' => pure (res ** env'))
586600
587601export
588602runWithLoop : {resf : _} ->
589− Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
603+ Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
590604 IO (Maybe (result ** Env (resf result)))
591−runWithLoop env fuel prog
592− = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
605+runWithLoop env fuel prog
606+ = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
593607 (pure Nothing)
594608
595609export
@@ -602,7 +616,7 @@ runPure prog = runST [] prog (\res, env' => res)
602616export
603617st_precondition : Err -> Maybe (List ErrorReportPart)
604618st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)
605− = pure
619+ = pure
606620 [TextPart "'call' is not valid here. ",
607621 TextPart "The operation has preconditions ",
608622 TermPart sub,
@@ -629,13 +643,13 @@ st_precondition (CantUnify _ tm1 tm2 _ _ _)
629643 getPostconditions _ = Nothing
630644
631645 renderPre : TT -> TT -> List (ErrorReportPart)
632− renderPre got req
646+ renderPre got req
633647 = [SubReport [TextPart "Operation has preconditions: ",
634648 TermPart req],
635649 SubReport [TextPart "States here are: ",
636650 TermPart got]]
637651 renderPost : TT -> TT -> List (ErrorReportPart)
638− renderPost got req
652+ renderPost got req
639653 = [SubReport [TextPart "Operation has postconditions: ",
640654 TermPart req],
641655 SubReport [TextPart "Required result states here are: ",