diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-12 14:16:04 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:59:21 +0200 |
commit | a1fd5fb489237a1300adb242e2c9b6c74c82981b (patch) | |
tree | d6cdbc54eaa310af02e9ffc25c1e1a3629c1db3c /plugins/firstorder/g_ground.ml4 | |
parent | 95b669a96f143d930b228a8b04041457040dd984 (diff) |
Porting the firstorder plugin to the new tactic API.
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 39 |
1 files changed, 23 insertions, 16 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3c0319319..8ef6a09d0 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -13,7 +13,9 @@ open Formula open Sequent open Ground open Goptions -open Tacticals +open Tacmach.New +open Tacticals.New +open Proofview.Notations open Tacinterp open Libnames open Stdarg @@ -81,21 +83,29 @@ END let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") -let gen_ground_tac flag taco ids bases gl= +let gen_ground_tac flag taco ids bases = let backup= !qflag in - try + Proofview.tclOR begin + Proofview.Goal.enter { enter = begin fun gl -> qflag:=flag; let solver= match taco with Some tac-> tac | None-> snd (default_solver ()) in - let startseq gl= + let startseq k = + Proofview.Goal.s_enter { s_enter = begin fun gl -> let seq=empty_seq !ground_depth in - let seq,gl = extend_with_ref_list ids seq gl in - extend_with_auto_hints bases seq gl in - let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in - qflag:=backup;result - with reraise -> qflag:=backup;raise reraise + let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in + let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in + Sigma.Unsafe.of_pair (k seq, sigma) + end } + in + let result=ground_tac solver startseq in + qflag := backup; + result + end } + end + (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e) (* special for compatibility with Intuition @@ -144,18 +154,15 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ] + [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ] + [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ] END - -open Proofview.Notations -open Cc_plugin |