From df0606d3bcbc41272fcde2d013bbe0b1aadf98af Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 16:57:10 +0000 Subject: [PATCH] A few other tactics made available to matita. A few tactics (change, fold, replace) generalized to patterns. The argument of clear and clearbody is now an identifier. WARNING: the implementation of change, fold and replace has been commented out to generalize them to patterns. To be committed soon. --- .../cic_disambiguation/cicTextualParser2.ml | 19 +- helm/ocaml/cic_transformations/tacticAst.ml | 10 +- .../cic_transformations/tacticAst2Box.ml | 25 -- helm/ocaml/cic_transformations/tacticAstPp.ml | 20 +- helm/ocaml/tactics/eliminationTactics.ml | 8 +- helm/ocaml/tactics/equalityTactics.ml | 6 +- helm/ocaml/tactics/equalityTactics.mli | 3 +- helm/ocaml/tactics/fourierR.ml | 2 +- helm/ocaml/tactics/primitiveTactics.mli | 3 - .../tactics/proofEngineStructuralRules.ml | 246 +++++++++--------- .../tactics/proofEngineStructuralRules.mli | 7 +- helm/ocaml/tactics/reductionTactics.ml | 13 +- helm/ocaml/tactics/reductionTactics.mli | 2 +- helm/ocaml/tactics/ring.ml | 12 +- helm/ocaml/tactics/tacticals.ml | 54 +--- helm/ocaml/tactics/tacticals.mli | 6 +- helm/ocaml/tactics/tactics.ml | 6 +- helm/ocaml/tactics/tactics.mli | 11 +- helm/ocaml/tactics/variousTactics.ml | 10 - helm/ocaml/tactics/variousTactics.mli | 3 - 20 files changed, 202 insertions(+), 264 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 3fdda212d..0ef9ec617 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -352,6 +352,10 @@ EXTEND depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; width = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,depth,width) + | IDENT "clear"; id = IDENT -> + TacticAst.Clear (loc,id) + | IDENT "clearbody"; id = IDENT -> + TacticAst.ClearBody (loc,id) | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; "in"; where = pattern_spec -> TacticAst.Change (loc, t1, t2, where) @@ -378,8 +382,11 @@ EXTEND TacticAst.Exact (loc, t) | IDENT "exists" -> TacticAst.Exists loc - | IDENT "fold"; kind = reduction_kind; t = tactic_term -> - TacticAst.Fold (loc, kind, t) + | IDENT "fail" -> TacticAst.Fail loc + | IDENT "fold"; kind = reduction_kind; t = tactic_term; + p = OPT [ pattern_spec ] -> + let p = match p with None -> [], None | Some p -> p in + TacticAst.Fold (loc, kind, t, p) | IDENT "fourier" -> TacticAst.Fourier loc | IDENT "fwd"; t = term -> @@ -391,6 +398,7 @@ EXTEND TacticAst.Generalize (loc,t,id,p) | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) + | IDENT "id" -> TacticAst.IdTac loc | IDENT "injection"; t = term -> TacticAst.Injection (loc, t) | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> @@ -410,8 +418,9 @@ EXTEND TacticAst.Reduce (loc, kind, p) | IDENT "reflexivity" -> TacticAst.Reflexivity loc - | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term -> - TacticAst.Replace (loc, t1, t2) + | IDENT "replace"; p = OPT [ pattern_spec ]; "with"; t = tactic_term -> + let p = match p with None -> [], None | Some p -> p in + TacticAst.Replace (loc, p, t) | IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] -> let p = match p with None -> [], None | Some p -> p in TacticAst.Rewrite (loc, d, t, p) @@ -449,8 +458,6 @@ EXTEND TacticAst.Tries (loc, tacs) | IDENT "try"; tac = NEXT -> TacticAst.Try (loc, tac) - | IDENT "fail" -> TacticAst.Fail loc - | IDENT "id" -> TacticAst.IdTac loc | PAREN "("; tac = tactical; PAREN ")" -> tac | tac = tactic -> TacticAst.Tactic (loc, tac) ] diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 47f275a68..7622ce963 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -37,6 +37,8 @@ type ('term, 'ident) tactic = | Assumption of loc | Auto of loc * int option * int option (* depth, width *) | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *) + | Clear of loc * 'ident + | ClearBody of loc * 'ident | Compare of loc * 'term | Constructor of loc * int | Contradiction of loc @@ -48,11 +50,13 @@ type ('term, 'ident) tactic = | ElimType of loc * 'term | Exact of loc * 'term | Exists of loc - | Fold of loc * reduction_kind * 'term + | Fail of loc + | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern | Fourier of loc | FwdSimpl of loc * 'term | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern | Goal of loc * int (* change current goal, argument is goal number 1-based *) + | IdTac of loc | Injection of loc * 'term | Intros of loc * int option * 'ident list | LApply of loc * 'term option * 'term @@ -60,7 +64,7 @@ type ('term, 'ident) tactic = | LetIn of loc * 'term * 'ident | Reduce of loc * reduction_kind * ('term, 'ident) pattern | Reflexivity of loc - | Replace of loc * 'term * 'term (* what, with what *) + | Replace of loc * ('term, 'ident) pattern * 'term | Rewrite of loc * direction * 'term * ('term, 'ident) pattern | Right of loc | Ring of loc @@ -135,9 +139,7 @@ type ('term,'obj) command = type ('term, 'ident) tactical = | Tactic of loc * ('term, 'ident) tactic - | Fail of loc | Do of loc * int * ('term, 'ident) tactical - | IdTac of loc | Repeat of loc * ('term, 'ident) tactical | Seq of loc * ('term, 'ident) tactical list (* sequential composition *) | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index f0626c772..ba14fd0d6 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -65,8 +65,6 @@ let rec count_tactic current_size tac = | ElimType (_, term) -> countterm (current_size + 10) term | Exact (_, term) -> countterm (current_size + 6) term | Exists _ -> current_size + 6 - | Fold (_, kind, term) -> - countterm (current_size + 5) term | Fourier _ -> current_size + 7 | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) | Injection (_, term) -> @@ -79,9 +77,6 @@ let rec count_tactic current_size tac = | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term | Reflexivity _ -> current_size + 11 - | Replace (_, t1, t2) -> - let size1 = countterm (current_size + 14) t1 in (* replace, with *) - countterm size1 t2 | Right _ -> current_size + 5 | Ring _ -> current_size + 4 | Split _ -> current_size + 5 @@ -162,11 +157,6 @@ and big_tactic2box = function Box.V([],[Box.Text([],"exact"); Box.indent(ast2astBox term)]) | Exists _ -> Box.Text([],"exists") - | Fold (_, kind, term) -> - Box.V([],[Box.H([],[Box.Text([],"fold"); - Box.smallskip; - Box.Text([],string_of_kind kind)]); - Box.indent(ast2astBox term)]) | Fourier _ -> Box.Text([],"fourier") | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) | Intros (_, num, idents) -> @@ -188,14 +178,6 @@ and big_tactic2box = function Box.Text([],"=")]); Box.indent (ast2astBox term)]) | Reflexivity _ -> Box.Text([],"reflexivity") - | Replace (_, t1, t2) -> - Box.V([], - (pretty_append - [Box.Text([],"replace")] - t1)@ - (pretty_append - [Box.Text([],"with")] - t2)) | Right _ -> Box.Text([],"right") | Ring _ -> Box.Text([],"ring") | Split _ -> Box.Text([],"split") @@ -209,16 +191,9 @@ open TacticAst let rec tactical2box = function | Tactic (_, tac) -> tactic2box tac -(* - | Command cmd -> (* TODO dummy implementation *) - Box.Text([], TacticAstPp.pp_tactical (Command cmd)) -*) - - | Fail _ -> Box.Text([],"fail") | Do (_, count, tac) -> Box.V([],[Box.Text([],"do " ^ string_of_int count); Box.indent (tactical2box tac)]) - | IdTac _ -> Box.Text([],"id") | Repeat (_, tac) -> Box.V([],[Box.Text([],"repeat"); Box.indent (tactical2box tac)]) diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 019ba6172..452976e59 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -55,7 +55,7 @@ let pp_pattern (hyp, goal) = | Some p -> pp_term_ast p in let separator = - if hyp <> [] then " \vdash " else " " + if hyp <> [] then " \\vdash " else " " in "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal @@ -65,8 +65,10 @@ let rec pp_tactic = function | Auto _ -> "auto" | Assumption _ -> "assumption" | Change (_, t1, t2, where) -> - sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2) + sprintf "change %s with %s %s" (pp_term_ast t1) (pp_term_ast t2) (pp_pattern where) + | Clear (_,id) -> sprintf "clear %s" id + | ClearBody (_,id) -> sprintf "clearbody %s" id | Compare (_,term) -> "compare " ^ pp_term_ast term | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" @@ -83,14 +85,17 @@ let rec pp_tactic = function | ElimType (_, term) -> "elim type " ^ pp_term_ast term | Exact (_, term) -> "exact " ^ pp_term_ast term | Exists _ -> "exists" - | Fold (_, kind, term) -> - sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term_ast term) + | Fold (_, kind, term, pattern) -> + sprintf "fold %s %s %s" (pp_reduction_kind kind) (pp_term_ast term) + (pp_pattern pattern) | Generalize (_, term, ident, pattern) -> sprintf "generalize %s%s %s" (pp_term_ast term) (match ident with None -> "" | Some id -> " as " ^ id) (pp_pattern pattern) | Goal (_, n) -> "goal " ^ string_of_int n + | Fail _ -> "fail" | Fourier _ -> "fourier" + | IdTac _ -> "id" | Injection (_, term) -> "injection " ^ pp_term_ast term | Intros (_, None, []) -> "intro" | Intros (_, num, idents) -> @@ -102,8 +107,8 @@ let rec pp_tactic = function | Reduce (_, kind, pat) -> sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat) | Reflexivity _ -> "reflexivity" - | Replace (_, t1, t2) -> - sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2) + | Replace (_, pattern, t) -> + sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t) | Rewrite (_, pos, t, pattern) -> sprintf "rewrite %s %s %s" (if pos = `Left then "left" else "right") (pp_term_ast t) @@ -221,10 +226,7 @@ let pp_command = function let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac - - | Fail _ -> "fail" | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) - | IdTac _ -> "id" | Repeat (_, tac) -> "repeat " ^ pp_tactical tac | Seq (_, tacs) -> pp_tacticals tacs | Then (_, tac, tacs) -> diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index d018dc52c..4f840764a 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -158,12 +158,18 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = let new_context_len = List.length context in warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in + let hyp_name = + match List.nth context new_nr_of_hyp_still_to_elim with + None + | Some (Cic.Anonymous,_) -> assert false + | Some (Cic.Name name,_) -> name + in ProofEngineTypes.apply_tactic (T.then_ ~start:( if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) then begin debug_print ("%%%%%%% no clear"); T.id_tac end - else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) + else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:hyp_name) end) ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim))) status ))) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 8cbfed96b..b9db6f705 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -143,8 +143,9 @@ let rewrite_back_simpl_tac ?where ~term () = ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term) ;; -let replace_tac ~what ~with_what = - let replace_tac ~what ~with_what status = +let replace_tac ~pattern ~with_what = +(* + let replace_tac ~pattern ~with_what status = let (proof, goal) = status in let module C = Cic in let module U = UriManager in @@ -179,6 +180,7 @@ let replace_tac ~what ~with_what = raise (ProofEngineTypes.Fail "Replace: empty context") in ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what) +*) assert false ;; diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index 698b34e9c..d156ae440 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -37,7 +37,8 @@ val rewrite_back_simpl_tac: term:Cic.term -> unit -> ProofEngineTypes.tactic val replace_tac: - what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> + with_what:Cic.term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 2ee088edb..724d2c647 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -693,7 +693,7 @@ let tac_zero_infeq_false gl (n,d) = (Tacticals.then_ ~start: (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~also_in_hypotheses:false + ~pattern:([],None) ~term: (Cic.Appl [_Rle ; _R0 ; diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index 81385510c..4d4eef849 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -56,8 +56,5 @@ val elim_intros_simpl_tac: val elim_intros_tac: term: Cic.term -> ProofEngineTypes.tactic -val elim_intros_tac: - term: Cic.term -> ProofEngineTypes.tactic - val change_tac: what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 3b8b6f92c..17378ffe7 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -28,135 +28,131 @@ open ProofEngineTypes let clearbody ~hyp = let clearbody ~hyp (proof, goal) = let module C = Cic in - match hyp with - None -> assert false - | Some (_, C.Def (_, Some _)) -> assert false - | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") - | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> - let curi,metasenv,pbo,pty = proof in - let metano,_,_ = CicUtil.lookup_meta goal metasenv in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear_body -> - let cleared_entry = - let ty,_ = - CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph (* TASSI: FIXME *) - in - Some (n_to_clear_body, Cic.Decl ty) - in - cleared_entry::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _,_ = - try - CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph (* TASSI: FIXME *) - with - _ -> - raise - (Fail - ("The correctness of hypothesis " ^ - string_of_name n ^ - " relies on the body of " ^ - string_of_name n_to_clear_body) - ) - in - entry::context - | Some (_,Cic.Def (_,Some _)) -> assert false - ) canonical_context [] - in - let _,_ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph (* TASSI: FIXME *) - with - _ -> - raise - (Fail - ("The correctness of the goal relies on the body of " ^ - string_of_name n_to_clear_body)) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] + let curi,metasenv,pbo,pty = proof in + let metano,_,_ = CicUtil.lookup_meta goal metasenv in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' -> + let cleared_entry = + let ty = + match ty with + Some ty -> ty + | None -> + fst + (CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph) (* TASSI: FIXME *) + in + Some (C.Name hyp, Cic.Decl ty) + in + cleared_entry::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def (t,None)) -> + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.empty_ugraph (* TASSI: FIXME *) + with + _ -> + raise + (Fail + ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ hyp) + ) + in + entry::context + | Some (_,Cic.Def (_,Some _)) -> assert false + ) canonical_context [] + in + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + CicUniv.empty_ugraph (* TASSI: FIXME *) + with + _ -> + raise + (Fail + ("The correctness of the goal relies on the body of " ^ + hyp)) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] in mk_tactic (clearbody ~hyp) let clear ~hyp = - let clear ~hyp:hyp_to_clear (proof, goal) = + let clear ~hyp (proof, goal) = let module C = Cic in - match hyp_to_clear with - None -> assert false - | Some (n_to_clear, _) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - CicUtil.lookup_meta goal metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear -> None::context - | None -> None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _,_ = - try - CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph (* TASSI: FIXME *) - with - _ -> - raise - (Fail - ("Hypothesis " ^ - string_of_name n ^ - " uses hypothesis " ^ - string_of_name n_to_clear) - ) - in - entry::context - ) canonical_context [] - in - let _,_ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph (* TASSI: FIXME *) - with - _ -> - raise - (Fail - ("Hypothesis " ^ string_of_name n_to_clear ^ - " occurs in the goal")) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = + CicUtil.lookup_meta goal metasenv + in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + Some (Cic.Name hyp',_) when hyp' = hyp -> None::context + | None -> None::context + | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,C.Decl t) + | Some (n,C.Def (t,None)) -> + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.empty_ugraph (* TASSI: FIXME *) + with _ -> + raise + (Fail + ("Hypothesis " ^ string_of_name n ^ + " uses hypothesis " ^ hyp)) + in + entry::context + ) canonical_context [] + in + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + CicUniv.empty_ugraph (* TASSI: FIXME *) + with _ -> + raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal")) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] in mk_tactic (clear ~hyp) + +let set_goal n = + ProofEngineTypes.mk_tactic + (fun (proof, goal) -> + let (_, metasenv, _, _) = proof in + if CicUtil.exists_meta n metasenv then + (proof, [n]) + else + raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n))) diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.mli b/helm/ocaml/tactics/proofEngineStructuralRules.mli index 32ba812ac..142b82b68 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.mli +++ b/helm/ocaml/tactics/proofEngineStructuralRules.mli @@ -23,5 +23,8 @@ * http://cs.unibo.it/helm/. *) -val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic -val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic +val clearbody: hyp:string -> ProofEngineTypes.tactic +val clear: hyp:string -> ProofEngineTypes.tactic + + (* change the current goal to those referred by the given meta number *) +val set_goal: int -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 430414b78..bfbfdb2a3 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -125,15 +125,13 @@ let whd_tac ~pattern = let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; -let fold_tac ~reduction ~also_in_hypotheses ~term = - let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = +let fold_tac ~reduction ~pattern ~term = +(* + let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal) + = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let term' = reduction context term in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) - (*CSC: che si guadagni nulla in fatto di efficienza. *) let replace = ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] in @@ -160,5 +158,6 @@ let fold_tac ~reduction ~also_in_hypotheses ~term = in (curi,metasenv',pbo,pty), [metano] in - mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term) + mk_tactic (fold_tac ~reduction ~pattern ~term) +*) assert false ;; diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index bb4ca3c70..dbee7c5cd 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -31,4 +31,4 @@ val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fold_tac: reduction:(Cic.context -> Cic.term -> Cic.term) -> - also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index cebb4cf91..ab7bde56f 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -437,9 +437,15 @@ let purge_hyps_tac ~count = match (n, context) with | (0, _) -> status | (n, hd::tl) -> - aux (n-1) tl - (status_of_single_goal_tactic_result - (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status)) + let name_of_hyp = + match hd with + None + | Some (Cic.Anonymous,_) -> assert false + | Some (Cic.Name name,_) -> name + in + aux (n-1) tl + (status_of_single_goal_tactic_result + (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status)) | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in let (_, metasenv, _, _) = proof in diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 62f1ce322..3c89150ad 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -194,7 +194,7 @@ let try_tactic ~tactic = mk_tactic (try_tactic ~tactic) ;; -let fail = mk_tactic (fun _ -> raise (Fail "fail tactical")) +let fail_tac = mk_tactic (fun _ -> raise (Fail "fail tactical")) (* This tries tactics until one of them doesn't _solve_ the goal *) (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) @@ -226,55 +226,3 @@ let solve_tactics ~tactics = in mk_tactic (solve_tactics ~tactics) ;; - - - - - - - - - - - (** tattica di prova per debuggare i tatticali *) -(* -let thens' ~start ~continuations status = - let (proof,new_goals) = start status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic (proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - -let prova_tac = - let apply_T_tac status = - let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - let rel = - let rec find n = - function - [] -> assert false - | (Some (Cic.Name name,_))::_ when name = "T" -> n - | _::tl -> find (n+1) tl - in - debug_print ("eseguo find"); - find 1 context - in - debug_print ("eseguo apply"); - apply_tac ~term:(Cic.Rel rel) status - in -(* do_tactic ~n:2 *) - repeat_tactic - ~tactic: - (then_ - ~start:(intros_tac ~name:"pippo") - ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)])) -(* id_tac *) -;; -*) - - diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli index d7cc27545..ab2f71823 100644 --- a/helm/ocaml/tactics/tacticals.mli +++ b/helm/ocaml/tactics/tacticals.mli @@ -54,8 +54,4 @@ val try_tactic: val solve_tactics: tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic -val fail: ProofEngineTypes.tactic - -(* -val prova_tac : ProofEngineTypes.tactic -*) +val fail_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index e67fa5fde..fc2c1c75d 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -28,6 +28,8 @@ let apply = PrimitiveTactics.apply_tac let assumption = VariousTactics.assumption_tac let auto = AutoTactic.auto_tac let change = PrimitiveTactics.change_tac +let clear = ProofEngineStructuralRules.clear +let clearbody = ProofEngineStructuralRules.clearbody let compare = DiscriminationTactics.compare_tac let constructor = IntroductionTactics.constructor_tac let contradiction = NegationTactics.contradiction_tac @@ -40,10 +42,12 @@ let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac let elim_type = EliminationTactics.elim_type_tac let exact = PrimitiveTactics.exact_tac let exists = IntroductionTactics.exists_tac +let fail = Tacticals.fail_tac let fold = ReductionTactics.fold_tac let fourier = FourierR.fourier_tac let fwd_simpl = FwdSimplTactic.fwd_simpl_tac let generalize = VariousTactics.generalize_tac +let id = Tacticals.id_tac let injection = DiscriminationTactics.injection_tac let intros = PrimitiveTactics.intros_tac let lapply = FwdSimplTactic.lapply_tac @@ -59,7 +63,7 @@ let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac -let set_goal = VariousTactics.set_goal +let set_goal = ProofEngineStructuralRules.set_goal let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac let symmetry = EqualityTactics.symmetry_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index d5016dabc..c4c1a32e4 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -6,6 +6,8 @@ val auto : ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic +val clear : hyp:string -> ProofEngineTypes.tactic +val clearbody : hyp:string -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic val constructor : n:int -> ProofEngineTypes.tactic val contradiction : ProofEngineTypes.tactic @@ -27,14 +29,17 @@ val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic val elim_type : term:Cic.term -> ProofEngineTypes.tactic val exact : term:Cic.term -> ProofEngineTypes.tactic val exists : ProofEngineTypes.tactic +val fail : ProofEngineTypes.tactic val fold : reduction:(Cic.context -> Cic.term -> Cic.term) -> - also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> + term:Cic.term -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val id : ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : ?howmany:int -> @@ -50,7 +55,9 @@ val letin : val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic -val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic +val replace : + pattern:ProofEngineTypes.pattern -> + with_what:Cic.term -> ProofEngineTypes.tactic val rewrite : ?where:ProofEngineTypes.pattern -> term:Cic.term -> unit -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 9fcbb966f..226a8c87c 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -131,13 +131,3 @@ let generalize_tac in PET.mk_tactic (generalize_tac mk_fresh_name_callback ~term pattern) ;; - -let set_goal n = - ProofEngineTypes.mk_tactic - (fun (proof, goal) -> - let (_, metasenv, _, _) = proof in - if CicUtil.exists_meta n metasenv then - (proof, [n]) - else - raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n))) - diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index 2c891b036..264168ed7 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -32,6 +32,3 @@ val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic - - (* change the current goal to those referred by the given meta number *) -val set_goal: int -> ProofEngineTypes.tactic -- 2.39.2