max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/ir/type_check): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-08 14:50:28 -07:00
parent 4ed7b57903
commit 9373133800
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/lean/ir/type_check.lean
View file

@ -78,6 +78,9 @@ match op with
@[reducible] def type_checker_m := except_t format (reader_t (environment × list result) (state_t context id))
def type_checker_m.run {α} (a : type_checker_m α) (env : environment) (r : list result) : except format α :=
((a.run.run (env, r)).run mk_context).1
def match_type (x : var) (t expected : type) : type_checker_m unit :=
unless (t = expected) $
throw ("type mismatch, variable `" ++ to_fmt x ++ "` has type `" ++ to_fmt t ++ "`" ++
@ -177,8 +180,7 @@ def decl.infer_types : decl → type_checker_m context
/-- Return context with the type of variables used in the given declaration.
It does not check whether instructions are being used correctly. -/
def infer_types (d : decl) (env : environment) : except format context :=
let (r, _) := (d.infer_types.run.run (env, d.header.return)).run mk_context
in r
d.infer_types.run env d.header.return
def check_arg_types : list var → list arg → type_checker_m unit
| [] [] := return ()
@ -243,9 +245,7 @@ def decl.check : decl → type_checker_m unit
| _ := return ()
def type_check (d : decl) (env : environment := λ _, none) : except format context :=
let act := do ctx ← d.infer_types, d.check, return ctx in
let (r, _) := (act.run.run (env, d.header.return)).run mk_context in
r
(d.infer_types >> d.check >> get).run env d.header.return
end ir
end lean