4b21484 · Idris-dev · git.iko.soy

39

40{- Update an entry in a context with a new state -}

41public export

42−updateRes : (res : Resources) ->

42+updateRes : (res : Resources) ->

43 InState lbl st res -> Type -> Resources

44updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)

45updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty

46

47{- Remove an entry from a context -}

48public export

49−drop : (res : Resources) -> (prf : InState lbl st res) ->

49+drop : (res : Resources) -> (prf : InState lbl st res) ->

50 Resources

51drop (MkRes lbl st :: rs) Here = rs

52drop (r :: rs) (There p) = r :: drop rs p

128updateWith new [] SubNil = new

129updateWith new [] (InRes el z) = absurd el

130-- 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)

132 = updateWith [] (dropEl _ el) p

133-- 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)

135 = n :: updateWith ns (dropEl _ el) p

136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p

137

154

155public export

156combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources

157−combineVarsIn {comp} res (InResVar el x)

157+combineVarsIn {comp} res (InResVar el x)

158 = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x))

159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x

160

172lookupEnv Here (x :: xs) = x

173lookupEnv (There p) (x :: xs) = lookupEnv p xs

174

175−updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->

175+updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->

176 Env (updateRes res prf ty')

177updateEnv Here (x :: xs) val = val :: xs

178updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val

205

206mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf)

207mkComposite [] VarsNil = CompNil

208−mkComposite env (InResVar el z)

208+mkComposite env (InResVar el z)

209 = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)

210mkComposite (x :: env) (SkipVar z) = mkComposite env z

211

212−rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->

212+rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->

213 Env (combineVarsIn res prf)

214−rebuildVarsIn env (InResVar el p)

214+rebuildVarsIn env (InResVar el p)

215 = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p)

216rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p

217

218{- Some things to make STrans interfaces look prettier -}

219

220infix 6 :->

221−

221+

222public export

223data Action : Type -> Type where

224 Stable : Var -> Type -> Action ty

254public export %error_reduce

255add : Type -> Action Var

256add ty = Add (\var => [var ::: ty])

257−

257+

258public export %error_reduce

259remove : Var -> Type -> Action ty

260remove = Remove

285 (ty : Type) ->

286 Resources -> (ty -> Resources) ->

287 Type where

288− Pure : (result : ty) ->

288+ Pure : (result : ty) ->

289 STrans m ty (out_fn result) out_fn

290 Bind : STrans m a st1 st2_fn ->

291− ((result : a) ->

291+ ((result : a) ->

292 STrans m b (st2_fn result) st3_fn) ->

293 STrans m b st1 st3_fn

294 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) ->

296 STrans m (m t) in_res (const out_res)

297

298− New : (val : state) ->

298+ New : (val : state) ->

299 STrans m Var res (\lbl => (lbl ::: state) :: res)

300 Delete : (lbl : Var) ->

301 (prf : InState lbl st res) ->

305

306 Split : (lbl : Var) ->

307 (prf : InState lbl (Composite vars) res) ->

308− STrans m (VarList vars) res

308+ STrans m (VarList vars) res

309− (\ vs => mkRes vs ++

309+ (\ vs => mkRes vs ++

310 updateRes res prf (State ()))

311 Combine : (comp : Var) -> (vs : List Var) ->

312 (prf : VarsIn (comp :: vs) res) ->

340dropEnv : Env ys -> SubRes xs ys -> Env xs

341dropEnv [] SubNil = []

342dropEnv [] (InRes idx rest) = absurd idx

343−dropEnv (z :: zs) (InRes idx rest)

343+dropEnv (z :: zs) (InRes idx rest)

344 = let [e] = envElem idx (z :: zs) in

345 e :: dropEnv (dropDups (z :: zs) idx) rest

346dropEnv (z :: zs) (Skip p) = dropEnv zs p

355 Env (updateWith new old prf)

356rebuildEnv new [] SubNil = new

357rebuildEnv new [] (InRes el p) = absurd el

358−rebuildEnv [] (x :: xs) (InRes el p)

358+rebuildEnv [] (x :: xs) (InRes el p)

359 = rebuildEnv [] (dropDups (x :: xs) el) p

360−rebuildEnv (e :: es) (x :: xs) (InRes el p)

360+rebuildEnv (e :: es) (x :: xs) (InRes el p)

361 = e :: rebuildEnv es (dropDups (x :: xs) el) p

362rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p

363

364runST : Env invars -> STrans m a invars outfn ->

365 ((x : a) -> Env (outfn x) -> m b) -> m b

366runST env (Pure result) k = k result env

367−runST env (Bind prog next) k

367+runST env (Bind prog next) k

368 = runST env prog (\prog', env' => runST env' (next prog') k)

369−runST env (Lift action) k

369+runST env (Lift action) k

370 = do res <- action

371 k res env

372runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')

373runST env (New val) k = k MkVar (val :: env)

374runST env (Delete lbl prf) k = k () (dropVal prf env)

375runST 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

377 env' = updateEnv prf env (Value ()) in

378 k (mkVars val) (addToEnv val env')

379 where

386 addToEnv (CompCons x xs) env = x :: addToEnv xs env

387runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])

388runST 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

390 = let env' = dropEnv env res_prf in

391 runST env' prog

392 (\prog', envk => k prog' (rebuildEnv envk env res_prf))

404 (k : (x : a) -> Env (outfn x) -> m b) ->

405 (onDry : m b) -> m b

406runSTLoop Empty _ _ _ onDry = onDry

407−runSTLoop (More x) env (Bind prog next) k onDry

407+runSTLoop (More x) env (Bind prog next) k onDry

408 = runST env prog (\prog', env' => runSTLoop x env' (next prog') k onDry)

409runSTLoop (More x) env (Pure result) k onDry = k result env

410

411−export

411+export

412pure : (result : ty) -> STrans m ty (out_fn result) out_fn

413pure = Pure

414

415−export

415+export

416(>>=) : STrans m a st1 st2_fn ->

417 ((result : a) -> STrans m b (st2_fn result) st3_fn) ->

418 STrans m b st1 st3_fn

423 STrans m ty res out_fn

424returning res prog = do prog

425 pure res

426−

426+

427

428export

429lift : Monad m => m t -> STrans m t res (const res)

430lift = Lift

431

432export

433−runAs : Applicative m => STrans m t in_res (const out_res) ->

433+runAs : Applicative m => STrans m t in_res (const out_res) ->

434 STrans m (m t) in_res (const out_res)

435runAs = RunAs

436

437export

438−new : (val : state) ->

438+new : (val : state) ->

439 STrans m Var res (\lbl => (lbl ::: State state) :: res)

440new val = New (Value val)

441

455export

456split : (lbl : Var) ->

457 {auto prf : InState lbl (Composite vars) res} ->

458− STrans m (VarList vars) res

458+ STrans m (VarList vars) res

459− (\ vs => mkRes vs ++

459+ (\ vs => mkRes vs ++

460 updateRes res prf (State ()))

461split lbl {prf} = Split lbl prf

462

467 STrans m () res

468 (const (combineVarsIn res var_prf))

469combine comp vs {var_prf} = Combine comp vs var_prf

470−

470+

471export

472toEnd : (lbl : Var) ->

473 {auto prf : InState lbl state res} ->

479 {auto res_prf : SubRes sub old} ->

480 STrans m t old (\res => updateWith (new_f res) old res_prf)

481call prog {res_prf} = Call prog res_prf

482−

482+

483export

484read : (lbl : Var) ->

485 {auto prf : InState lbl (State ty) res} ->

493 (val : ty') ->

494 STrans m () res (const (updateRes res prf (State ty')))

495write lbl {prf} val = Write lbl prf (Value val)

496−

496+

497export

498update : (lbl : Var) ->

499 {auto prf : InState lbl (State ty) res} ->

512 export

513 pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn

514 pure = Pure

515−

515+

516public export %error_reduce

517out_res : ty -> (as : List (Action ty)) -> Resources

518out_res x [] = []

519out_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)

521 = (lbl ::: outr x) :: out_res x xs

522out_res x ((Remove lbl inr) :: xs) = out_res x xs

523out_res x (Add outf :: xs) = outf x ++ out_res x xs

533public export

534%error_reduce -- always evaluate this before showing errors

535ST : (m : Type -> Type) ->

536− (ty : Type) ->

536+ (ty : Type) ->

537 List (Action ty) -> Type

538ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)

539

540public export

541%error_reduce -- always evaluate this before showing errors

542STLoop : (m : Type -> Type) ->

543− (ty : Type) ->

543+ (ty : Type) ->

544 List (Action ty) -> Type

545STLoop m ty xs = STransLoop m ty (in_res xs) (\result : ty => out_res result xs)

546

550 putStr : String -> STrans m () xs (const xs)

551 getStr : STrans m String xs (const xs)

552

553+ putChar : Char -> STrans m () xs (const xs)

554+ getChar : STrans m Char xs (const xs)

555+

556+

553export

557export

554putStrLn : ConsoleIO m => String -> STrans m () xs (const xs)

558putStrLn : ConsoleIO m => String -> STrans m () xs (const xs)

555putStrLn str = putStr (str ++ "\n")

559putStrLn str = putStr (str ++ "\n")

556

560

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+

557export

569export

558ConsoleIO IO where

570ConsoleIO IO where

559 putStr str = lift (Interactive.putStr str)

571 putStr str = lift (Interactive.putStr str)

560 getStr = lift Interactive.getLine

572 getStr = lift Interactive.getLine

561

573

574+ putChar c = lift $ Interactive.putChar c

575+ getChar = lift Interactive.getChar

562

576

563export

577export

564run : Applicative m => ST m a [] -> m a

578run : Applicative m => ST m a [] -> m a

565run prog = runST [] prog (\res, env' => pure res)

579run prog = runST [] prog (\res, env' => pure res)

566

580

567export

581export

568−runLoop : Applicative m => Fuel -> STLoop m a [] ->

582+runLoop : Applicative m => Fuel -> STLoop m a [] ->

569 (onEmpty : m a) ->

583 (onEmpty : m a) ->

570 m a

584 m a

571runLoop fuel prog onEmpty

585runLoop fuel prog onEmpty

580||| to ensure that it isn't duplicated.

594||| to ensure that it isn't duplicated.

581export

595export

582runWith : {resf : _} ->

596runWith : {resf : _} ->

583− Env res -> STrans IO a res (\result => resf result) ->

597+ Env res -> STrans IO a res (\result => resf result) ->

584 IO (result ** Env (resf result))

598 IO (result ** Env (resf result))

585runWith env prog = runST env prog (\res, env' => pure (res ** env'))

599runWith env prog = runST env prog (\res, env' => pure (res ** env'))

586

600

587export

601export

588runWithLoop : {resf : _} ->

602runWithLoop : {resf : _} ->

589− Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->

603+ Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->

590 IO (Maybe (result ** Env (resf result)))

604 IO (Maybe (result ** Env (resf result)))

591−runWithLoop env fuel prog

605+runWithLoop env fuel prog

592− = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))

606+ = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))

593 (pure Nothing)

607 (pure Nothing)

594

608

595export

609export

602export

616export

603st_precondition : Err -> Maybe (List ErrorReportPart)

617st_precondition : Err -> Maybe (List ErrorReportPart)

604st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)

618st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)

605− = pure

619+ = pure

606 [TextPart "'call' is not valid here. ",

620 [TextPart "'call' is not valid here. ",

607 TextPart "The operation has preconditions ",

621 TextPart "The operation has preconditions ",

608 TermPart sub,

622 TermPart sub,

629 getPostconditions _ = Nothing

643 getPostconditions _ = Nothing

630

644

631 renderPre : TT -> TT -> List (ErrorReportPart)

645 renderPre : TT -> TT -> List (ErrorReportPart)

632− renderPre got req

646+ renderPre got req

633 = [SubReport [TextPart "Operation has preconditions: ",

647 = [SubReport [TextPart "Operation has preconditions: ",

634 TermPart req],

648 TermPart req],

635 SubReport [TextPart "States here are: ",

649 SubReport [TextPart "States here are: ",

636 TermPart got]]

650 TermPart got]]

637 renderPost : TT -> TT -> List (ErrorReportPart)

651 renderPost : TT -> TT -> List (ErrorReportPart)

638− renderPost got req

652+ renderPost got req

639 = [SubReport [TextPart "Operation has postconditions: ",

653 = [SubReport [TextPart "Operation has postconditions: ",

640 TermPart req],

654 TermPart req],

641 SubReport [TextPart "Required result states here are: ",

655 SubReport [TextPart "Required result states here are: ",