From 8c3f8406ec805c07c39ab2a8e801e81185aaa9cc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 29 Oct 2007 19:11:26 +0000 Subject: [PATCH] - destruct: core of subst tactic implemented, must be linked to destruct in order to work - "if" tactical implemented (used by core subst tactic) - to be tested - added freqently used constant hole = Cic.Implicit (Some 'Hole) --- components/tactics/discriminationTactics.ml | 49 ++++++++++++++++----- components/tactics/proofEngineTypes.ml | 4 +- components/tactics/proofEngineTypes.mli | 1 + components/tactics/tacticals.ml | 22 +++++++++ components/tactics/tacticals.mli | 1 + 5 files changed, 65 insertions(+), 12 deletions(-) diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index f31b52a2e..83f676ed3 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -37,6 +37,7 @@ module CU = CicUniv module S = CicSubstitution module RT = ReductionTactics module PEH = ProofEngineHelpers +module ET = EqualityTactics let debug = false let debug_print = @@ -242,7 +243,7 @@ let discriminate_tac ~term = ~continuation: (T.then_ ~start: - (EqualityTactics.rewrite_simpl_tac + (ET.rewrite_simpl_tac ~direction:`RightToLeft ~pattern:(PET.conclusion_pattern None) term []) @@ -418,8 +419,8 @@ let rec injection_tac ~map ~term ~i ~continuation = with | CTC.TypeCheckerFailure _ -> false in - if not go_on then - PET.apply_tactic T.id_tac status (* FG: ??????? *) + if not go_on then + PET.apply_tactic (continuation ~map) status else let tac term = let tac status = @@ -441,11 +442,11 @@ let rec injection_tac ~map ~term ~i ~continuation = RT.change_tac ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1'])) (fun _ m u -> changed,m,u); - EqualityTactics.rewrite_simpl_tac + ET.rewrite_simpl_tac ~direction:`LeftToRight ~pattern:(PET.conclusion_pattern None) term []; - EqualityTactics.reflexivity_tac + ET.reflexivity_tac ] in PET.apply_tactic tac status in @@ -455,7 +456,7 @@ let rec injection_tac ~map ~term ~i ~continuation = PET.apply_tactic (T.thens ~start: (P.cut_tac cutted) ~continuations:[ - (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id + (destruct ~first_time:false ~term:(C.Rel 1) ~map:id ~continuation:(after2 continuation succ map) ); tac term] @@ -467,11 +468,37 @@ let rec injection_tac ~map ~term ~i ~continuation = (* ~term vive nel contesto della tattica una volta ~mappato * ~continuation riceve la mappa assoluta *) -and qnify_tac ~first_time ~map ~term ~continuation = +and subst_tac ~map ~term ~direction ~where ~continuation = + let fail_tactic = continuation ~map in + let subst_tac status = + let term = relocate_term map term in + let tactic = match where with + | None -> + let pattern = PET.conclusion_pattern None in + let tactic = ET.rewrite_tac ~direction ~pattern term [] in + T.then_ ~start:(T.try_tactic ~tactic) + ~continuation:fail_tactic + | Some name -> + let pattern = None, [name, PET.hole], None in + let start = ET.rewrite_tac ~direction ~pattern term [] in + let continuation = + destruct ~first_time:false ~term:(C.Rel 1) ~map:id + ~continuation:(after2 continuation succ map) + in + T.if_ ~start ~continuation ~fail:fail_tactic + in + PET.apply_tactic tactic status + in + PET.mk_tactic subst_tac + +(* ~term vive nel contesto della tattica una volta ~mappato + * ~continuation riceve la mappa assoluta + *) +and destruct ~first_time ~map ~term ~continuation = let are_convertible hd1 hd2 metasenv context = fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph) in - let qnify_tac status = + let destruct status = let (proof, goal) = status in let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in @@ -527,7 +554,7 @@ and qnify_tac ~first_time ~map ~term ~continuation = | _ when not first_time -> continuation ~map | _ (* when first_time *) -> T.then_ ~start:(simpl_in_term context term) - ~continuation:(qnify_tac ~first_time:false ~term ~map ~continuation) + ~continuation:(destruct ~first_time:false ~term ~map ~continuation) end | _ when not first_time -> continuation ~map | _ (* when first_time *) -> raise exn_nonproj @@ -536,10 +563,10 @@ and qnify_tac ~first_time ~map ~term ~continuation = in PET.apply_tactic tac status in - PET.mk_tactic qnify_tac + PET.mk_tactic destruct (* destruct performs either injection or discriminate *) (* equivalent to Coq's "analyze equality" *) let destruct_tac = - qnify_tac + destruct ~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac) diff --git a/components/tactics/proofEngineTypes.ml b/components/tactics/proofEngineTypes.ml index abe460775..93436e799 100644 --- a/components/tactics/proofEngineTypes.ml +++ b/components/tactics/proofEngineTypes.ml @@ -76,13 +76,15 @@ type ('term, 'lazy_term) pattern = type lazy_pattern = (Cic.term, Cic.lazy_term) pattern +let hole = Cic.Implicit (Some `Hole) + let conclusion_pattern t = let t' = match t with | None -> None | Some t -> Some (const_lazy_term t) in - t',[],Some (Cic.Implicit (Some `Hole)) + t',[], Some hole (** tactic failure *) exception Fail of string Lazy.t diff --git a/components/tactics/proofEngineTypes.mli b/components/tactics/proofEngineTypes.mli index 6edcfeccc..7c7b8330e 100644 --- a/components/tactics/proofEngineTypes.mli +++ b/components/tactics/proofEngineTypes.mli @@ -75,3 +75,4 @@ type mk_fresh_name_type = val goals_of_proof: proof -> goal list +val hole: Cic.term diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml index 06f96a573..cf5f22206 100644 --- a/components/tactics/tacticals.ml +++ b/components/tactics/tacticals.ml @@ -180,6 +180,28 @@ let seq ~tactics = (HExtlib.list_concat ~sep:[ C.Semicolon ] (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics))) +let if_ ~start ~continuation ~fail = + S.mk_tactic + (fun istatus -> + let xostatus = + try + let res = C.eval (C.Tactical (C.Tactic start)) istatus in + info (lazy ("Tacticals.if_: succedeed!!!")); + Some res + with PET.Fail _ -> None + in + match xostatus with + | Some ostatus -> + let opened,closed = S.goals ostatus in + begin match opened with + | [] -> ostatus + | _ -> + fold_eval (S.focus ~-1 ostatus) + [ C.Semicolon; C.Tactical (C.Tactic continuation) ] + end + | None -> C.eval (C.Tactical (C.Tactic fail)) istatus + ) + (* Tacticals that cannot be implemented on top of tynycals *) let first ~tactics = diff --git a/components/tactics/tacticals.mli b/components/tactics/tacticals.mli index cdc3bac77..800991bb5 100644 --- a/components/tactics/tacticals.mli +++ b/components/tactics/tacticals.mli @@ -31,6 +31,7 @@ val fail_tac: tactic val first: tactics: tactic list -> tactic val thens: start: tactic -> continuations: tactic list -> tactic val then_: start: tactic -> continuation: tactic -> tactic +val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic val seq: tactics: tactic list -> tactic (** "folding" of then_ *) val repeat_tactic: tactic: tactic -> tactic val do_tactic: n: int -> tactic: tactic -> tactic -- 2.39.2