Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Dependent type checking fallback #5

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Dependent type checking fallback #5

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions coq/Frontend.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,36 @@ Notation _must_succeed_vm r :=
Notation _must_succeed_native r :=
(extract_success r (@eq_refl bool true <<: is_success r = true)).

Ltac solve_eqdec_t :=
repeat match goal with
| |- context [EqDec.eq_dec ?x ?x] =>
try rewrite eq_dec_refl || vm_compute (EqDec.eq_dec x x)
| |- context [EqDec.eq_dec ?x ?y] =>
vm_compute (EqDec.eq_dec x y)
end.

(* This tactic will first try to rewrite `eq_dec` occurrences
in order to handles cases like `forall s, ... EqDec.eq_dec s s ...`,
which could not be solved by vm_compute.

For that the goal needs to be simplified very carefully which is done
by leaving `eq_dec` opaque, such that it cannot be unfolded by `cbn` *)
Ltac tc_action_dependent_t :=
cbv zeta;
unfold TypeInference.tc_action;
repeat match goal with
| _ => progress with_strategy opaque [ EqDec.eq_dec ] cbn
| _ => progress solve_eqdec_t
| |- context [type_action] => unfold type_action
| |- context [cast_action] => unfold cast_action
| |- context [cast_action'] => unfold cast_action'
end;
reflexivity.

Ltac _extract_success_dependent r :=
let eq_pr := constr:(ltac:(tc_action_dependent_t) : is_success r = true) in
exact (extract_success r eq_pr).

Inductive TC_Strategy := TC_conv | TC_vm | TC_native.
Ltac _tc_strategy := exact TC_vm.

Expand All @@ -147,6 +177,10 @@ Ltac _tc_action_fast R Sigma sig tau uaction :=
let result := constr:(desugar_and_tc_action R Sigma sig tau uaction) in
_extract_success result.

Ltac _tc_action_dependent R Sigma sig tau uaction :=
let result := constr:(desugar_and_tc_action R Sigma sig tau uaction) in
_extract_success_dependent result.

Arguments place_error_beacon {var_t fn_name_t reg_t ext_fn_t} / rev_target current_path a : assert.

Ltac _report_typechecking_errors uaction tc_result :=
Expand Down Expand Up @@ -199,8 +233,13 @@ Ltac _tc_illtyped_action R Sigma sig tau uaction :=
let result := constr:(desugar_and_tc_action R Sigma sig tau annotated) in
_report_typechecking_errors uaction result.

(* type checking is done aggressively by [_tc_action_fast]
if that fails [_tc_action_dependent] tries to solve it
with specialized tactics which handle certain corner cases better,
but slower *)
Ltac _tc_action R Sigma sig tau uaction :=
(_tc_action_fast R Sigma sig tau uaction ||
_tc_action_dependent R Sigma sig tau uaction ||
_tc_illtyped_action R Sigma sig tau uaction).

(* FIXME: Find a way to propagate reg_t and ext_fn_t from R and Sigma to ua.
Expand Down
Loading