Last active
August 5, 2019 16:36
-
-
Save dselsam/bc46a2e3fb1d61929bc56b26f2f25568 to your computer and use it in GitHub Desktop.
match goes down wrong branch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
inductive Term : Type | |
| const : Nat -> Term | |
| app : List Term -> Term | |
namespace Term | |
instance : Inhabited Term := ⟨Term.const 0⟩ | |
partial def hasToString : Term -> String | (const n) := "CONST(" ++ toString n ++ ")" | (app ts) := "APP" | |
instance : HasToString Term := ⟨hasToString⟩ | |
end Term | |
open Term | |
structure MyState : Type := (ts : List Term) | |
def emit (t : Term) : State MyState Unit := modify (λ ms => ⟨t::ms.ts⟩) | |
partial def foo : MyState -> Term -> Term -> List Term | |
| ms₀ t u := | |
let stateT : State MyState Unit := do { | |
match t with | |
| const _ => pure () | |
| app _ => emit (const 1) *> pure () ; | |
match t, u with | |
| app _, app _ => emit (app []) *> pure () | |
| _, _ => pure () ; | |
match t, u with | |
| app _, app _ => emit (app []) *> pure () | |
| _, _ => emit (const 2) *> pure () | |
} ; | |
(stateT.run ⟨[]⟩).2.ts.reverse | |
def main : IO Unit := IO.println $ foo ⟨[]⟩ (app []) (app []) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment