Commit 8668805e authored by Timmy Weerwag's avatar Timmy Weerwag

improved tactics and added tactic for statement function calls

parent 2ed837d2
......@@ -52,6 +52,30 @@ Ltac solve_binop :=
Ltac solve_most_typing :=
repeat first [constructor | solve_fvar | solve_binop].
Ltac solve_stmt_funcall argtys retty s :=
let v := fresh "v" in
let H := fresh "H" in
match goal with
| [|- stmt_type ?g (SFunCall ?x _) _] =>
lazymatch eval compute in (find_env g x) with
| Some ?tyscm => apply (TSFunCall _ _ _ tyscm argtys retty)
| _ => fail "not found in environment" x
end;
[ reflexivity
| exists s; split;
[ intros v H;
simpl in H;
repeat match goal with
[ H : _ \/ _ |- _ ] => inversion_clear H
end;
solve [ subst v; reflexivity | contradiction ]
| reflexivity ]
| ]
end; solve_most_typing.
Ltac solve_simple_stmt_funcall argtys retty :=
solve_stmt_funcall argtys retty SubstId.
Ltac solve_funcall argtys s :=
let v := fresh "v" in
let H := fresh "H" in
......@@ -77,6 +101,9 @@ Ltac solve_funcall argtys s :=
Ltac solve_simple_funcall argtys :=
solve_funcall argtys SubstId.
Ltac solve_stmt_val ty :=
apply (TSVal _ _ _ _ ty); solve_most_typing.
Ltac solve_fun fty :=
lazymatch eval hnf in fty with
| TFun ?argtys ?retty => apply (TPFun _ _ _ argtys _ retty)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment