From 80fc89019bcb7fb7e0e1fb8bb111b708be49d19f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jun 2005 16:18:05 +0000 Subject: [PATCH] 1. new syntax for patterns: [t] [in p] where t is the term to be matched and p is the pattern on the hypotheses and on the conclusion (whose syntax is not changed). All the tactics now use the new syntax. 2. several tactics have been changed to use the new kind of patterns (that also have the optional term in them) 3. the signature of the select function has changed to require the context (and return a context and not a "context patch"); moreover it performs now both the search for roots and the search for subterms of the roots that are alpha-convertible with the optional given term (if any) WARNING!!! The following tactics have been commented out for a while: replace rewrite change fold --- .../cic_disambiguation/cicTextualParser2.ml | 68 +++++---- helm/ocaml/cic_transformations/.depend | 4 +- helm/ocaml/cic_transformations/cicAstPp.ml | 4 +- helm/ocaml/cic_transformations/tacticAst.ml | 9 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 33 ++--- helm/ocaml/tactics/.depend | 10 +- helm/ocaml/tactics/discriminationTactics.ml | 58 ++++---- helm/ocaml/tactics/equalityTactics.ml | 8 +- helm/ocaml/tactics/fourierR.ml | 28 ++-- helm/ocaml/tactics/primitiveTactics.ml | 5 +- helm/ocaml/tactics/primitiveTactics.mli | 3 +- helm/ocaml/tactics/proofEngineHelpers.ml | 113 ++++++++++----- helm/ocaml/tactics/proofEngineHelpers.mli | 21 ++- helm/ocaml/tactics/proofEngineTypes.ml | 5 +- helm/ocaml/tactics/proofEngineTypes.mli | 10 +- helm/ocaml/tactics/reductionTactics.ml | 130 ++++++++++-------- helm/ocaml/tactics/reductionTactics.mli | 2 +- helm/ocaml/tactics/tactics.mli | 9 +- helm/ocaml/tactics/variousTactics.ml | 86 +++++++----- helm/ocaml/tactics/variousTactics.mli | 2 +- 20 files changed, 335 insertions(+), 273 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 352c925fb..fc46cc725 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -325,15 +325,30 @@ EXTEND | [ IDENT "normalize" ] -> `Normalize ] ]; pattern_spec: [ - [ "in"; - hyp_paths = - LIST0 - [ id = IDENT ; - path = OPT [SYMBOL ":" ; path = term -> path ] -> - (id,match path with Some p -> p | None -> CicAst.UserInput) ] - SEP SYMBOL ";"; - goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> - (hyp_paths, goal_path) ] + [ wanted = OPT term; + hyp_paths_and_goal_path = + OPT [ + "in"; + hyp_paths = + LIST0 + [ id = IDENT ; + path = OPT [SYMBOL ":" ; path = term -> path ] -> + (id,match path with Some p -> p | None -> CicAst.UserInput) ] + SEP SYMBOL ";"; + goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> + let goal_path = + match goal_path with + None -> CicAst.UserInput + | Some goal_path -> goal_path + in + hyp_paths,goal_path + ] -> + let hyp_paths,goal_path = + match hyp_paths_and_goal_path with + None -> [], CicAst.UserInput + | Some (hyp_paths,goal_path) -> hyp_paths,goal_path + in + wanted, hyp_paths, goal_path ] ]; direction: [ [ IDENT "left" -> `Left @@ -356,9 +371,8 @@ EXTEND 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) + | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> + TacticAst.Change (loc, what, t) | IDENT "compare"; t = tactic_term -> TacticAst.Compare (loc,t) | IDENT "constructor"; n = NUM -> @@ -383,19 +397,14 @@ EXTEND | IDENT "exists" -> TacticAst.Exists loc | 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 "fold"; kind = reduction_kind; p = pattern_spec -> + TacticAst.Fold (loc, kind, p) | IDENT "fourier" -> TacticAst.Fourier loc | IDENT "fwd"; t = term -> TacticAst.FwdSimpl (loc, t) - | IDENT "generalize"; t = tactic_term; - id = OPT [ "as" ; id = IDENT -> id ]; - p = OPT [ pattern_spec ] -> - let p = match p with None -> [], None | Some p -> p in - TacticAst.Generalize (loc,t,id,p) + | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> + TacticAst.Generalize (loc,p,id) | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) | IDENT "id" -> TacticAst.IdTac loc @@ -414,17 +423,20 @@ EXTEND | IDENT "left" -> TacticAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) - | kind = reduction_kind; p = OPT [ pattern_spec ] -> - let p = match p with None -> [], None | Some p -> p in + | kind = reduction_kind; p = pattern_spec -> TacticAst.Reduce (loc, kind, p) | IDENT "reflexivity" -> TacticAst.Reflexivity loc - | IDENT "replace"; p = OPT [ pattern_spec ]; "with"; t = tactic_term -> - let p = match p with None -> [], None | Some p -> p in + | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> 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) + | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (Parse_error + (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")) + else + TacticAst.Rewrite (loc, d, t, p) | IDENT "right" -> TacticAst.Right loc | IDENT "ring" -> diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 4203ff228..f4c554908 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -42,9 +42,9 @@ xml2Gdome.cmx: xml2Gdome.cmi sequentPp.cmo: cic2Xml.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx sequentPp.cmi applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \ - content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi + domMisc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \ - content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi + domMisc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index bb365d73c..8076e0062 100644 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -35,7 +35,6 @@ let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s let rec pp_term = function | CicAst.AttributedTerm (_, term) -> pp_term term - | CicAst.Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body) @@ -79,8 +78,7 @@ let rec pp_term = function | CicAst.Sort `Type -> "Type" | CicAst.Sort `CProp -> "CProp" | CicAst.Symbol (name, _) -> name - - | CicAst.UserInput -> "" + | CicAst.UserInput -> "%" and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 191323599..15961702d 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -28,15 +28,14 @@ type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] type loc = CicAst.location -type ('term, 'ident) pattern = - ('ident * 'term) list * 'term option +type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term | Assumption of loc | Auto of loc * int option * int option (* depth, width *) - | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *) + | Change of loc * ('term,'ident) pattern * 'term | Clear of loc * 'ident | ClearBody of loc * 'ident | Compare of loc * 'term @@ -51,10 +50,10 @@ type ('term, 'ident) tactic = | Exact of loc * 'term | Exists of loc | Fail of loc - | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern + | Fold of loc * reduction_kind * ('term, 'ident) pattern | Fourier of loc | FwdSimpl of loc * 'term - | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern + | Generalize of loc * ('term, 'ident) pattern * 'ident option | Goal of loc * int (* change current goal, argument is goal number 1-based *) | IdTac of loc | Injection of loc * 'term diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 2e8124d7e..33b5e8ade 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -44,29 +44,24 @@ let pp_reduction_kind = function | `Normalize -> "normalize" -let pp_pattern (hyp, goal) = +let pp_pattern (t, hyp, goal) = let pp_hyp_pattern l = String.concat "; " - (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) + (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in + let pp_t t = + match t with + None -> "" + | Some t -> pp_term_ast t in - let pp_goal_pattern p = - match p with - | None -> "" - | Some p -> pp_term_ast p - in - let separator = - if hyp <> [] then " \\vdash " else " " - in - "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal + pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal let rec pp_tactic = function | Absurd (_, term) -> "absurd" ^ pp_term_ast term | Apply (_, term) -> "apply " ^ pp_term_ast term | Auto _ -> "auto" | Assumption _ -> "assumption" - | Change (_, t1, t2, where) -> - sprintf "change %s with %s %s" (pp_term_ast t1) (pp_term_ast t2) - (pp_pattern where) + | Change (_, where, with_what) -> + sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what) | Clear (_,id) -> sprintf "clear %s" id | ClearBody (_,id) -> sprintf "clearbody %s" id | Compare (_,term) -> "compare " ^ pp_term_ast term @@ -85,13 +80,11 @@ 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, 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) + | Fold (_, kind, pattern) -> + sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern) + | Generalize (_, pattern, ident) -> + sprintf "generalize %s%s" (pp_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) - (pp_pattern pattern) | Goal (_, n) -> "goal " ^ string_of_int n | Fail _ -> "fail" | Fourier _ -> "fourier" diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 481447099..91e755580 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -20,8 +20,8 @@ proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi -proofEngineHelpers.cmo: proofEngineHelpers.cmi -proofEngineHelpers.cmx: proofEngineHelpers.cmi +proofEngineHelpers.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineReduction.cmx proofEngineHelpers.cmi tacticals.cmo: proofEngineTypes.cmi tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ @@ -67,11 +67,9 @@ negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \ negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \ primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ - introductionTactics.cmi equalityTactics.cmi + primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ - introductionTactics.cmx equalityTactics.cmi + primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmi discriminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \ eliminationTactics.cmi discriminationTactics.cmi diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 24ab511f0..05344e0ab 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -164,23 +164,21 @@ and injection1_tac ~term ~i = in ProofEngineTypes.apply_tactic (P.change_tac - ~what:new_t1' - ~pattern:([],None) - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ( - (C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1] - )) + ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) + (C.Appl [ + C.Lambda ( + C.Name "x", tty, + C.MutCase ( + turi, typeno, + (C.Lambda ( + (C.Name "x"), + (S.lift 1 tty), + (S.lift 2 tty'))), + (C.Rel 1), pattern + ) + ); + t1] + )) status )) ~continuation: @@ -300,20 +298,18 @@ let discriminate'_tac ~term = (T.then_ ~start: (P.change_tac - ~what:gty' - ~pattern:([],None) - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); - t2] - ) + ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty')) + (C.Appl [ + C.Lambda ( + C.Name "x", tty, + C.MutCase ( + turi, typeno, + (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), + (C.Rel 1), pattern + ) + ); + t2] + ) ) ~continuation: ( diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index b9db6f705..94f62a955 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -25,6 +25,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = +(* let module C = Cic in let module U = UriManager in let module PET = ProofEngineTypes in @@ -105,6 +106,7 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) = in assert (List.length goals = 0) ; (proof',[fresh_meta]) +*) assert false let rewrite_tac ?where ~term () = @@ -119,7 +121,8 @@ let rewrite_simpl_tac ?where ~term () = (Tacticals.then_ ~start:(rewrite_tac ?where ~term ()) ~continuation: - (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern)) + (ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None))) status in ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term) @@ -137,7 +140,8 @@ let rewrite_back_simpl_tac ?where ~term () = (Tacticals.then_ ~start:(rewrite_back_tac ?where ~term ()) ~continuation: - (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern)) + (ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None))) status in ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term) diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index c51d3bf0c..e6fa4edcd 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -693,14 +693,15 @@ let tac_zero_infeq_false gl (n,d) = (Tacticals.then_ ~start: (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~pattern:([],None) - ~term: - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) + ~pattern: + (ProofEngineTypes.conclusion_pattern + (Some + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ))) ) ~continuation: (Tacticals.then_ @@ -1133,8 +1134,9 @@ let rec fourier (s_proof,s_goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in apply_tactic - (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None) - ~with_what:(Cic.Appl [ _not; ineq])) + (PrimitiveTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) + (Cic.Appl [ _not; ineq])) status)) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: @@ -1178,8 +1180,10 @@ let rec fourier (s_proof,s_goal)= |_ -> assert false) in let r = apply_tactic - (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None) - ~with_what:w1) status in + (PrimitiveTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) + w1) status + in debug("fine MY_CHNGE\n"); r)) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c5815471a..07cdd5bfe 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -586,7 +586,8 @@ let elim_intros_simpl_tac ~term = (Tacticals.thens ~start:(intros_tac ()) ~continuations: - [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern]) + [ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None)]) ;; exception NotConvertible @@ -595,7 +596,7 @@ exception NotConvertible (*CSC: while [what] can have a richer context (because of binders) *) (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) (*CSC: Is that evident? Is that right? Or should it be changed? *) -let change_tac ~what ~with_what ~pattern = +let change_tac ~pattern with_what = (* let change_tac ~what ~with_what ~pattern (proof, goal) = let curi,metasenv,pbo,pty = proof in diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index 68570d5ca..70b18da56 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -57,5 +57,4 @@ val elim_intros_tac: term: Cic.term -> ProofEngineTypes.tactic val change_tac: - what: Cic.term -> with_what: Cic.term -> pattern:ProofEngineTypes.pattern -> - ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 20e8341a6..4adcb8416 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -111,10 +111,10 @@ let compare_metasenvs ~oldmetasenv ~newmetasenv = ;; (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *) -let find_subterms ~eq ~wanted t = - let rec find w t = - if eq w t then - [t] +let find_subterms ~wanted ~context t = + let rec find context w t = + if ProofEngineReduction.alpha_equivalence w t then + [context,t] else match t with | Cic.Sort _ @@ -124,96 +124,133 @@ let find_subterms ~eq ~wanted t = fun acc e -> match e with | None -> acc - | Some t -> find w t @ acc + | Some t -> find context w t @ acc ) [] ctx - | Cic.Lambda (_, t1, t2) - | Cic.Prod (_, t1, t2) - | Cic.LetIn (_, t1, t2) -> - find w t1 @ find (CicSubstitution.lift 1 w) t2 + | Cic.Lambda (name, t1, t2) + | Cic.Prod (name, t1, t2) -> + find context w t1 @ + find (Some (name, Cic.Decl t1)::context) + (CicSubstitution.lift 1 w) t2 + | Cic.LetIn (name, t1, t2) -> + find context w t1 @ + find (Some (name, Cic.Def (t1,None))::context) + (CicSubstitution.lift 1 w) t2 | Cic.Appl l -> - List.fold_left (fun acc t -> find w t @ acc) [] l - | Cic.Cast (t, ty) -> find w t @ find w ty + List.fold_left (fun acc t -> find context w t @ acc) [] l + | Cic.Cast (t, ty) -> find context w t @ find context w ty | Cic.Implicit _ -> assert false | Cic.Const (_, esubst) | Cic.Var (_, esubst) | Cic.MutInd (_, _, esubst) | Cic.MutConstruct (_, _, _, esubst) -> - List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst + List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst | Cic.MutCase (_, _, outty, indterm, patterns) -> - find w outty @ find w indterm @ - List.fold_left (fun acc p -> find w p @ acc) [] patterns + find context w outty @ find context w indterm @ + List.fold_left (fun acc p -> find context w p @ acc) [] patterns | Cic.Fix (_, funl) -> + let tys = + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl + in List.fold_left ( - fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc + fun acc (_, _, ty, bo) -> + find context w ty @ find (tys @ context) w bo @ acc ) [] funl | Cic.CoFix (_, funl) -> + let tys = + List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl + in List.fold_left ( - fun acc (_, ty, bo) -> find w ty @ find w bo @ acc + fun acc (_, ty, bo) -> + find context w ty @ find (tys @ context) w bo @ acc ) [] funl in - find wanted t + find context wanted t -let select ~term ~pattern = - let add_ctx i name entry = - (Some (name, entry)) :: i +let select ~context ~term ~pattern:(wanted,where) = + let add_ctx context name entry = + (Some (name, entry)) :: context in - (* i is the number of binder traversed *) - let rec aux i pattern term = - match (pattern, term) with - | Cic.Implicit (Some `Hole), t -> [i,t] + let rec aux context where term = + match (where, term) with + | Cic.Implicit (Some `Hole), t -> [context,t] | Cic.Implicit (Some `Type), t -> [] | Cic.Implicit None,_ -> [] | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> List.concat (List.map2 (fun t1 t2 -> - (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> [])) + (match (t1, t2) with + Some t1, Some t2 -> aux context t1 t2 + | _ -> [])) ctxt1 ctxt2) - | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2 + | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> + aux context te1 te2 @ aux context ty1 ty2 | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2) | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) -> - aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2 + aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2 | Cic.Prod (Cic.Name n1, s1, t1), Cic.Prod ((Cic.Name n2) as name , s2, t2) | Cic.Lambda (Cic.Name n1, s1, t1), Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2-> - aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2 + aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2 | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2) | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> [] | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> - aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2 + aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 | Cic.LetIn (Cic.Name n1, s1, t1), Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> - aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2 + aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> [] - | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2 + | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2 | Cic.Var (_, subst1), Cic.Var (_, subst2) | Cic.Const (_, subst1), Cic.Const (_, subst2) | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2) | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) -> - auxs i (List.map snd subst1) (List.map snd subst2) + auxs context (List.map snd subst1) (List.map snd subst2) | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> - aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2 + aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2 | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> + let tys = + List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 + in List.concat (List.map2 (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> - aux i ty1 ty2 @ aux i bo1 bo2) + aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) funs1 funs2) | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> + let tys = + List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 + in List.concat (List.map2 - (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2) + (fun (_, ty1, bo1) (_, ty2, bo2) -> + aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) funs1 funs2) | x,y -> raise (Bad_pattern (Printf.sprintf "Pattern %s versus term %s" (CicPp.ppterm x) (CicPp.ppterm y))) - and auxs i terms1 terms2 = (* as aux for list of terms *) - List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2) + and auxs context terms1 terms2 = (* as aux for list of terms *) + List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2) in - aux [] pattern term + let roots = aux context where term in + match wanted with + None -> roots + | Some wanted -> + let rec find_in_roots = + function + [] -> [] + | (context,where)::tl -> + let tl' = find_in_roots tl in + let found = + let wanted = CicSubstitution.lift (List.length context) wanted in + find_subterms ~wanted ~context where + in + found @ tl' + in + find_in_roots roots let pattern_of ?(equality=(==)) ~term terms = let (===) x y = equality x y in diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index c2f8c640a..c11ad6eca 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -55,16 +55,11 @@ val pattern_of: ?equality:(Cic.term -> Cic.term -> bool) -> term:Cic.term -> Cic.term list -> Cic.term -(** select all subterms of a given term matching a given pattern (i.e. subtrees -* rooted at pattern's holes. The first component is the context the term lives -* in). raise Bad_pattern (pattern_entry, term_entry) *) -val select: term:Cic.term -> pattern:Cic.term -> (Cic.context * Cic.term) list - - -(** Finds the _pointers_ to subterms that are alpha-equivalent to wanted in t. - * wanted is properly lifted when binders are crossed *) -val find_subterms : - eq:(Cic.term -> Cic.term -> bool) -> - wanted:Cic.term -> Cic.term -> - Cic.term list - +(** select context term (what,where) +* select all subterms of [term] matching [what] in positions rooted at the holes +* of the pattern [where]. [context] is the context of [term]. It returns +* the list of the matched terms (that can be compared using physical equality) +* together with their contexts. *) +val select: + context:Cic.context -> term:Cic.term -> pattern:(Cic.term option * Cic.term) -> + (Cic.context * Cic.term) list diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 7d1a53d73..9e92a076c 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -56,8 +56,9 @@ type tactic = status -> proof * goal list (** creates an opaque tactic from a status->proof*goal list function *) let mk_tactic t = t -type pattern = (string * Cic.term) list * Cic.term option -let goal_pattern = [],None + (** what, hypothesis patterns, conclusion pattern *) +type pattern = Cic.term option * (string * Cic.term) list * Cic.term +let conclusion_pattern t = t,[],Cic.Implicit (Some `Hole) (** tactic failure *) exception Fail of string diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index 6d2bae11e..4d418b5bc 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -44,13 +44,11 @@ val initial_status: Cic.term -> Cic.metasenv -> status type tactic val mk_tactic: (status -> proof * goal list) -> tactic -(** the type of a tactic application domain - * [ hypothesis_name * path ] * goal_path - *) -type pattern = (string * Cic.term) list * Cic.term option + (** what, hypothesis patterns, conclusion pattern *) +type pattern = Cic.term option * (string * Cic.term) list * Cic.term -(** the pattern for the whole goal *) -val goal_pattern : pattern + (** conclusion_pattern [t] returns the pattern (t,[],%) *) +val conclusion_pattern : Cic.term option -> pattern (** tactic failure *) exception Fail of string diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index bfbfdb2a3..65dc19912 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -25,81 +25,95 @@ open ProofEngineTypes -(* -let reduction_tac ~reduction (proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let new_ty = reduction context ty in - let new_metasenv = - List.map - (function - (n,_,_) when n = metano -> (metano,context,new_ty) - | _ as t -> t - ) metasenv - in - (curi,new_metasenv,pbo,pty), [metano] -;; -*) - (* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = +let reduction_tac ~reduction ~pattern:(what,hyp_patterns,goal_pattern) + (proof,goal) += let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv 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: Il vero problema e' che non sapendo dove sia il term non *) - (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) - (*CSC: e' meglio prima cercare il termine e scoprirne il *) - (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where terms = - (*CSC: Per il momento se la riduzione fallisce significa solamente che *) - (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) - (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let terms, terms' = - List.split - (List.map - (fun i, t -> t, reduction (i @ context) t) - terms) - in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where - (* FIXME this is a catch ALL... bad thing *) - with exc -> (*prerr_endline (Printexc.to_string exc);*) where - in + let replace where terms = + let terms, terms' = + List.split (List.map (fun (context, t) -> t, reduction context t) terms) + in + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where in let find_pattern_for name = try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) - with Not_found -> None - in + with Not_found -> None in let ty' = - match goal_pattern with - | None -> replace context ty [[],ty] - | Some pat -> - let terms = ProofEngineHelpers.select ~term:ty ~pattern:pat in - replace context ty terms - in + let terms = + ProofEngineHelpers.select ~context ~term:ty ~pattern:(what,goal_pattern) + in + replace ty terms in + let context_len = List.length context in let context' = if hyp_patterns <> [] then List.fold_right (fun entry context -> match entry with + None -> None::context | Some (name,Cic.Decl term) -> (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = ProofEngineHelpers.select ~term ~pattern:pat in - let where = replace context term terms in - let entry = Some (name,Cic.Decl where) in - entry::context) - | Some (name,Cic.Def (term, None)) -> + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms = + ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in + let term' = replace term terms in + Some (name,Cic.Decl term') :: context + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (ProofEngineTypes.Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) + | Some (name,Cic.Def (term, ty)) -> (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = ProofEngineHelpers.select ~term ~pattern:pat in - let where = replace context term terms in - let entry = Some (name,Cic.Def (where,None)) in - entry::context) - | _ -> entry::context + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms = + ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in + let term' = replace term terms in + let ty' = + match ty with + None -> None + | Some ty -> + let terms = + ProofEngineHelpers.select + ~context ~term:ty ~pattern:(what,pat) + in + Some (replace ty terms) + in + Some (name,Cic.Def (term',ty')) :: context + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (ProofEngineTypes.Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) ) context [] else context @@ -125,7 +139,7 @@ let whd_tac ~pattern = let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; -let fold_tac ~reduction ~pattern ~term = +let fold_tac ~reduction ~pattern = (* let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal) = diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index dbee7c5cd..20e45827d 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) -> - pattern:ProofEngineTypes.pattern -> term:Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 30d670f3e..a8730287e 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -6,9 +6,7 @@ val auto : ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic val change : - what:Cic.term -> - with_what:Cic.term -> - pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic val clear : hyp:string -> ProofEngineTypes.tactic val clearbody : hyp:string -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic @@ -35,13 +33,12 @@ val exists : ProofEngineTypes.tactic val fail : ProofEngineTypes.tactic val fold : reduction:(Cic.context -> Cic.term -> Cic.term) -> - pattern:ProofEngineTypes.pattern -> - term:Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> 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 + ProofEngineTypes.pattern -> ProofEngineTypes.tactic val id : ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 226a8c87c..2e6810387 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -63,6 +63,8 @@ let assumption_tac = (* ANCORA DA DEBUGGARE *) +exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;; +exception TheSelectedTermsMustLiveInTheGoalContext exception AllSelectedTermsMustBeConvertible;; exception CannotGeneralizeInHypotheses;; @@ -72,10 +74,12 @@ contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) let generalize_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - ~term pattern + pattern = let module PET = ProofEngineTypes in - let generalize_tac mk_fresh_name_callback ~term (hyps_pat,concl_pat) status = + let generalize_tac mk_fresh_name_callback + ~pattern:(term,hyps_pat,concl_pat) status + = if hyps_pat <> [] then raise CannotGeneralizeInHypotheses ; let (proof, goal) = status in let module C = Cic in @@ -83,36 +87,48 @@ let generalize_tac let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in - let terms = - let path = - match concl_pat with - None -> Cic.Implicit (Some `Hole) - | Some path -> path in - let roots = ProofEngineHelpers.select ~term:ty ~pattern:path in - List.fold_left - (fun acc (i, r) -> - ProofEngineHelpers.find_subterms - ~eq:ProofEngineReduction.alpha_equivalence ~wanted:term r @ acc - ) [] roots - in - let typ = - let typ,u = - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in - (* We need to check that all the convertibility of all the terms *) - ignore ( - (* TASSI: FIXME *) - List.fold_left - (fun u t -> - let b,u1 = CicReduction.are_convertible context term t u in - if not b then - raise AllSelectedTermsMustBeConvertible - else - u1 - ) u terms) ; - typ - in - PET.apply_tactic - (T.thens + let terms_with_context = + ProofEngineHelpers.select ~context ~term:ty ~pattern:(term,concl_pat) in + let typ,term = + match terms_with_context, term with + [], None -> + raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly + | _, Some term + | (_,term)::_, None -> + fst + (CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph), + term in + (* We need to check: + 1. whether they live in the context of the goal; + if they do they are also well-typed since they are closed subterms + of a well-typed term in the well-typed context of the well-typed + term + 2. whether they are convertible + *) + ignore ( + (* TASSI: FIXME *) + List.fold_left + (fun u (context_of_t,t) -> + (* 1 *) + begin + try + ignore + (CicMetaSubst.delift_rels [] metasenv + (List.length context_of_t - List.length context) t) + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise TheSelectedTermsMustLiveInTheGoalContext + end; + (* 2 *) + let b,u1 = CicReduction.are_convertible context term t u in + if not b then + raise AllSelectedTermsMustBeConvertible + else + u1 + ) CicUniv.empty_ugraph terms_with_context) ; + PET.apply_tactic + (T.thens ~start: (P.cut_tac (C.Prod( @@ -120,8 +136,8 @@ let generalize_tac typ, (ProofEngineReduction.replace_lifting_csc 1 ~equality:(==) - ~what:terms - ~with_what:(List.map (function _ -> C.Rel 1) terms) + ~what:(List.map snd terms_with_context) + ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context) ~where:ty) ))) ~continuations: @@ -129,5 +145,5 @@ let generalize_tac T.id_tac]) status in - PET.mk_tactic (generalize_tac mk_fresh_name_callback ~term pattern) + PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) ;; diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index 264168ed7..a71332879 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -30,5 +30,5 @@ val assumption_tac: ProofEngineTypes.tactic val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - term:Cic.term -> ProofEngineTypes.pattern -> + ProofEngineTypes.pattern -> ProofEngineTypes.tactic -- 2.39.2