From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 13:51:02 +0000 (+0000) Subject: New tactic unfold. X-Git-Tag: V_0_7_2~17 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git New tactic unfold. --- diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index 61b9670b7..b078b1ded 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -120,6 +120,7 @@ split to transitivity + unfold whd diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 1d23ac063..da3a730fb 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -97,6 +97,7 @@ let tactic_of_ast = function | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] | `Reduce -> ProofEngineReduction.reduce | `Simpl -> ProofEngineReduction.simpl + | `Unfold what -> ProofEngineReduction.unfold ?what | `Whd -> CicReduction.whd ~delta:false ~subst:[] in Tactics.fold ~reduction ~term ~pattern @@ -125,6 +126,7 @@ let tactic_of_ast = function | `Normalize -> Tactics.normalize ~pattern | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern + | `Unfold what -> Tactics.unfold ~pattern ?what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity | GrafiteAst.Replace (_, pattern, with_what) -> @@ -171,6 +173,16 @@ let disambiguate_pattern status (wanted, hyp_paths, goal_path) = status, Some wanted in status, (wanted, hyp_paths ,goal_path) + +let disambiguate_reduction_kind status = function + | `Unfold (Some t) -> + let status, t = disambiguate_term status t in + status, `Unfold (Some t) + | `Normalize + | `Reduce + | `Simpl + | `Unfold None + | `Whd as kind -> status, kind let disambiguate_tactic status = function | GrafiteAst.Apply (loc, term) -> @@ -233,10 +245,11 @@ let disambiguate_tactic status = function status, GrafiteAst.ElimType (loc, what, None, depth, idents) | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,reduction_kind, term, pattern) -> + | GrafiteAst.Fold (loc,red_kind, term, pattern) -> let status, pattern = disambiguate_pattern status pattern in let status, term = disambiguate_term status term in - status, GrafiteAst.Fold (loc,reduction_kind, term, pattern) + let status, red_kind = disambiguate_reduction_kind status red_kind in + status, GrafiteAst.Fold (loc,red_kind, term, pattern) | GrafiteAst.FwdSimpl (loc, hyp, names) -> status, GrafiteAst.FwdSimpl (loc, hyp, names) | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc @@ -262,9 +275,10 @@ let disambiguate_tactic status = function | GrafiteAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in status, GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, reduction_kind, pattern) -> + | GrafiteAst.Reduce (loc, red_kind, pattern) -> let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Reduce(loc, reduction_kind, pattern) + let status, red_kind = disambiguate_reduction_kind status red_kind in + status, GrafiteAst.Reduce(loc, red_kind, pattern) | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc | GrafiteAst.Replace (loc, pattern, with_what) -> let status, pattern = disambiguate_pattern status pattern in diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index c2e44a5df..fb654529b 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -24,7 +24,8 @@ *) type direction = [ `LeftToRight | `RightToLeft ] -type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] +type 'term reduction_kind = + [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ] type loc = CicNotationPt.location @@ -54,7 +55,7 @@ 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 * 'term reduction_kind * 'term * ('term, 'ident) pattern | Fourier of loc | FwdSimpl of loc * string * 'ident list | Generalize of loc * ('term, 'ident) pattern * 'ident option @@ -65,7 +66,7 @@ type ('term, 'ident) tactic = | LApply of loc * int option * 'term list * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident - | Reduce of loc * reduction_kind * ('term, 'ident) pattern + | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern | Reflexivity of loc | Replace of loc * ('term, 'ident) pattern * 'term | Rewrite of loc * direction * 'term * ('term, 'ident) pattern diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index c15b6fe71..7d1f8c22e 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -39,10 +39,12 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms) let pp_reduction_kind = function + | `Normalize -> "normalize" | `Reduce -> "reduce" | `Simpl -> "simplify" + | `Unfold (Some t) -> "unfold " ^ pp_term_ast t + | `Unfold None -> "unfold" | `Whd -> "whd" - | `Normalize -> "normalize" let pp_pattern (t, hyp, goal) = diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index fae3df93d..c138fce27 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -52,10 +52,11 @@ EXTEND [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ IDENT "reduce" -> `Reduce + [ IDENT "normalize" -> `Normalize + | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl - | IDENT "whd" -> `Whd - | IDENT "normalize" -> `Normalize ] + | IDENT "unfold"; t = OPT term -> `Unfold t + | IDENT "whd" -> `Whd ] ]; sequent_pattern_spec: [ [ hyp_paths = diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 0817b75c1..d28ff337d 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -18,8 +18,8 @@ statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi -proofEngineReduction.cmo: proofEngineReduction.cmi -proofEngineReduction.cmx: proofEngineReduction.cmi +proofEngineReduction.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineHelpers.cmx proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi tacticals.cmo: proofEngineTypes.cmi tacticals.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 32f74fec2..0f902c47e 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -8,7 +8,7 @@ REQUIRES = \ INTERFACE_FILES = \ proofEngineTypes.mli \ - proofEngineReduction.mli proofEngineHelpers.mli \ + proofEngineHelpers.mli proofEngineReduction.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ variousTactics.mli autoTactic.mli \ diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index c24ccc773..c9dc6c2c6 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -554,15 +554,23 @@ exception Fail of string in subst,metasenv,ugraph,context_terms, ty_terms -(** locate_in_term what where -* [what] must be a physical pointer to a subterm of [where] -* It returns the context of [what] in [where] *) -let locate_in_term what ~where context = +exception TermNotFound +exception TermFoundMultipleTimes + +(** locate_in_term equality what where context +* [what] must match a subterm of [where] according to [equality] +* It returns the matched term together with its context in [where] +* [equality] defaults to physical equality +* [context] must be the context of [where] +* It may raise TermNotFound or TermFoundMultipleTimes +*) +let locate_in_term ?(equality=(==))what ~where context = + let (@@) (l1,l2) (l1',l2') = l1 @ l1', l2 @ l2' in + let list_concat l = List.fold_right (@@) l ([],[]) in let add_ctx context name entry = - (Some (name, entry)) :: context - in + (Some (name, entry)) :: context in let rec aux context where = - if what == where then context + if equality what where then context,[where] else match where with | Cic.Implicit _ @@ -572,64 +580,75 @@ let locate_in_term what ~where context = | Cic.Var _ | Cic.Const _ | Cic.MutInd _ - | Cic.MutConstruct _ -> [] - | Cic.Cast (te, ty) -> aux context te @ aux context ty + | Cic.MutConstruct _ -> [],[] + | Cic.Cast (te, ty) -> aux context te @@ aux context ty | Cic.Prod (name, s, t) | Cic.Lambda (name, s, t) -> - aux context s @ aux (add_ctx context name (Cic.Decl s)) t + aux context s @@ aux (add_ctx context name (Cic.Decl s)) t | Cic.LetIn (name, s, t) -> - aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t + aux context s @@ aux (add_ctx context name (Cic.Def (s,None))) t | Cic.Appl tl -> auxs context tl | Cic.MutCase (_, _, out, t, pat) -> - aux context out @ aux context t @ auxs context pat + aux context out @@ aux context t @@ auxs context pat | Cic.Fix (_, funs) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in - List.concat + list_concat (List.map (fun (_, _, ty, bo) -> - aux context ty @ aux (tys @ context) bo) + aux context ty @@ aux (tys @ context) bo) funs) | Cic.CoFix (_, funs) -> let tys = List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs in - List.concat + list_concat (List.map (fun (_, ty, bo) -> - aux context ty @ aux (tys @ context) bo) + aux context ty @@ aux (tys @ context) bo) funs) and auxs context tl = (* as aux for list of terms *) - List.concat (List.map (fun t -> aux context t) tl) + list_concat (List.map (fun t -> aux context t) tl) in - aux context where + match aux context where with + context,[] -> raise TermNotFound + | context,[t] -> context,t + | context,_ -> raise TermFoundMultipleTimes -(** locate_in_conjecture what where -* [what] must be a physical pointer to a subterm of [where] -* It returns the context of [what] in [where] *) -let locate_in_conjecture what (_,context,ty) = +(** locate_in_term equality what where +* [what] must be a subterm of [where] according to [equality] +* It returns the context of [what] in [where] +* [equality] defaults to physical equality +* It may raise TermNotFound or TermFoundMultipleTimes +*) +let locate_in_conjecture ?(equality=(==)) what (_,context,ty) = + let (@@) (l1,l2) (l1',t) = l1 @ l1', l2 @ [t] in let context,res = List.fold_right (fun entry (context,res) -> match entry with None -> entry::context, res | Some (_, Cic.Decl ty) -> - let res = res @ locate_in_term what ~where:ty context in + let res = res @@ locate_in_term ~equality what ~where:ty context in let context' = entry::context in context',res | Some (_, Cic.Def (bo,ty)) -> - let res = res @ locate_in_term what ~where:bo context in + let res = res @@ locate_in_term ~equality what ~where:bo context in let res = match ty with None -> res - | Some ty -> res @ locate_in_term what ~where:ty context in + | Some ty -> + res @@ locate_in_term ~equality what ~where:ty context in let context' = entry::context in context',res - ) context ([],[]) + ) context ([],([],[])) in - res @ locate_in_term what ~where:ty context - + let res = res @@ locate_in_term ~equality what ~where:ty context in + match res with + context,[] -> raise TermNotFound + | context,[_] -> context + | context,_ -> raise TermFoundMultipleTimes (* saturate_term newmeta metasenv context ty *) (* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index f71574aef..574a94413 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -80,10 +80,29 @@ val select: ] option list * (Cic.context * Cic.term) list -(** locate_in_conjecture what where -* [what] must be a physical pointer to a subterm of [where] -* It returns the context of [what] in [where] *) -val locate_in_conjecture: Cic.term -> Cic.conjecture -> Cic.context +exception TermNotFound +exception TermFoundMultipleTimes + +(** locate_in_term equality what where context +* [what] must match a subterm of [where] according to [equality] +* It returns the matched term together with its context in [where] +* [equality] defaults to physical equality +* [context] must be the context of [where] +* It may raise TermNotFound or TermFoundMultipleTimes +*) +val locate_in_term: + ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> where:Cic.term -> + Cic.context -> Cic.context * Cic.term + +(** locate_in_conjecture equality what where +* [what] must match a subterm of [where] according to [equality] +* It returns the context of [what] in [where] +* [equality] defaults to physical equality +* It may raise TermNotFound or TermFoundMultipleTimes +*) +val locate_in_conjecture: + ?equality:(Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture -> + Cic.context (* saturate_term newmeta metasenv context ty *) (* Given a type [ty] (a backbone), it returns its head and a new metasenv in *) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 8a6ef81a2..a9b8b5500 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -874,3 +874,78 @@ let simpl context = in reduceaux context [] ;; + +let unfold ?what context where = + let first_is_the_expandable_head_of_second t1 t2 = + match t1,t2 with + Cic.Const (uri,_), Cic.Const (uri',_) + | Cic.Var (uri,_), Cic.Var (uri',_) + | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_) + | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri' + | Cic.Const _, _ + | Cic.Var _, _ -> false + | _,_ -> + raise + (ProofEngineTypes.Fail + "The term to unfold is neither a constant nor a variable") + in + let appl he tl = + if tl = [] then he else Cic.Appl (he::tl) in + let cannot_delta_expand t = + raise + (ProofEngineTypes.Fail + ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in + let rec hd_delta_beta context tl = + function + Cic.Rel n as t -> + (try + match List.nth context (n-1) with + Some (_,Cic.Decl _) -> cannot_delta_expand t + | Some (_,Cic.Def (bo,_)) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.lift n bo) tl) + | None -> raise RelToHiddenHypothesis + with + Failure _ -> assert false) + | Cic.Const (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | Cic.Var (uri,exp_named_subst) as t -> + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with + Cic.Constant _ -> raise ReferenceToConstant + | Cic.CurrentProof _ -> raise ReferenceToCurrentProof + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | Cic.Variable (_,Some body,_,_,_) -> + CicReduction.head_beta_reduce + (appl (CicSubstitution.subst_vars exp_named_subst body) tl) + | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t + ) + | Cic.Appl [] -> assert false + | Cic.Appl (he::tl) -> hd_delta_beta context tl he + | t -> cannot_delta_expand t + in + let context, where = + match what with + None -> context, where + | Some what -> + try + ProofEngineHelpers.locate_in_term + ~equality:first_is_the_expandable_head_of_second + what ~where context + with + ProofEngineHelpers.TermNotFound -> + raise + (ProofEngineTypes.Fail + ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)) + in + hd_delta_beta context [] where +;; diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli index 02e56ba6a..ebb61a7c8 100644 --- a/helm/ocaml/tactics/proofEngineReduction.mli +++ b/helm/ocaml/tactics/proofEngineReduction.mli @@ -46,3 +46,4 @@ val replace_lifting_csc : what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term +val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 1885e956c..492b265cb 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -73,16 +73,20 @@ let reduction_tac ~reduction ~pattern (proof,goal) = (curi,metasenv',pbo,pty), [metano] ;; -let simpl_tac ~pattern = +let simpl_tac ~pattern = mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; -let reduce_tac ~pattern = +let reduce_tac ~pattern = mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; + +let unfold_tac ?what ~pattern = + mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what) + ~pattern);; -let whd_tac ~pattern = +let whd_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; -let normalize_tac ~pattern = +let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);; exception NotConvertible diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 2b01561a5..6ef80512b 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -28,6 +28,8 @@ val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic +val unfold_tac: + ?what:Cic.term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val change_tac: pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index f6c166268..e75677caf 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -66,4 +66,5 @@ let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac +let unfold = ReductionTactics.unfold_tac let whd = ReductionTactics.whd_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 76f1e89d2..4780a82fb 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -78,4 +78,7 @@ val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic +val unfold : + ?what:Cic.term -> + pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic