From: Claudio Sacerdoti Coen Date: Thu, 29 Jun 2006 11:27:35 +0000 (+0000) Subject: Demodulate used to be a reduction_kind and it used to take a ~pattern. X-Git-Tag: 0.4.95@7852~1255 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa576f13a6fd64586b389880dec3e47f703cd300;p=helm.git Demodulate used to be a reduction_kind and it used to take a ~pattern. Since demodulation is not a reduction kind, I changed it to a normal tactic. Moreover, since the ~pattern was unused, I have temporarily removed it. Doc changed accordingly. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 32625f39f..5896e116f 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -37,8 +37,7 @@ type ('term, 'ident) type_spec = | Type of UriManager.uri * int type 'lazy_term reduction = - [ `Demodulate - | `Normalize + [ `Normalize | `Reduce | `Simpl | `Unfold of 'lazy_term option @@ -57,6 +56,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Contradiction of loc | Cut of loc * 'ident option * 'term | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list + | Demodulate of loc | Discriminate of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list | ElimType of loc * 'term * 'term option * int option * 'ident list diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 18f14c5ce..941f75d9d 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -36,7 +36,6 @@ let command_terminator = tactical_terminator let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" let pp_reduction_kind ~term_pp = function - | `Demodulate -> "demodulate" | `Normalize -> "normalize" | `Reduce -> "reduce" | `Simpl -> "simplify" @@ -99,6 +98,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = in let types = List.rev_map to_ident types in sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) + | Demodulate _ -> "demodulate" | Discriminate (_, term) -> "discriminate " ^ term_pp term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ term_pp term ^ diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index d7343c98c..b066b8ae0 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -83,6 +83,7 @@ let tactic_of_ast ast = let dbd = LibraryDb.instance () in let mk_fresh_name_callback = namer_of names in Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what + | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term | GrafiteAst.Elim (_, what, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) @@ -96,8 +97,6 @@ let tactic_of_ast ast = | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> let reduction = match reduction_kind with - | `Demodulate -> - GrafiteTypes.command_error "demodulation can't be folded" | `Normalize -> PET.const_lazy_reduction (CicReduction.normalize ~delta:false ~subst:[]) @@ -139,7 +138,6 @@ let tactic_of_ast ast = Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with - | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern | `Normalize -> Tactics.normalize ~pattern | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 5babe3604..6b7dd076b 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -98,7 +98,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function | `Unfold (Some t) -> let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in `Unfold (Some t) - | `Demodulate | `Normalize | `Reduce | `Simpl @@ -164,6 +163,8 @@ let disambiguate_tactic List.fold_left disambiguate (metasenv,[]) types in metasenv,GrafiteAst.Decompose (loc, types, what, names) + | GrafiteAst.Demodulate loc -> + metasenv,GrafiteAst.Demodulate loc | GrafiteAst.Discriminate (loc,term) -> let metasenv,term = disambiguate_term context metasenv term in metasenv,GrafiteAst.Discriminate(loc,term) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index ccff1fab1..f99573b30 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -68,8 +68,7 @@ EXTEND [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ IDENT "demodulate" -> `Demodulate - | IDENT "normalize" -> `Normalize + [ IDENT "normalize" -> `Normalize | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl | IDENT "unfold"; t = OPT tactic_term -> `Unfold t @@ -154,6 +153,7 @@ EXTEND let idents = match idents with None -> [] | Some idents -> idents in let to_spec id = GrafiteAst.Ident id in GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) + | IDENT "demodulate" -> GrafiteAst.Demodulate loc | IDENT "discriminate"; t = tactic_term -> GrafiteAst.Discriminate (loc, t) | IDENT "elim"; what = tactic_term; using = using; diff --git a/components/tactics/.depend b/components/tactics/.depend index 743811ceb..500838027 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -16,11 +16,11 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi -autoTactic.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi +autoTactic.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi @@ -102,12 +102,6 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ variousTactics.cmi -autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \ - paramodulation/equality.cmi autoTactic.cmi -autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \ - paramodulation/equality.cmx autoTactic.cmi introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ @@ -130,6 +124,14 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi +autoTactic.cmo: tacticals.cmi paramodulation/saturation.cmi \ + proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ + metadataQuery.cmi equalityTactics.cmi paramodulation/equality.cmi \ + autoTactic.cmi +autoTactic.cmx: tacticals.cmx paramodulation/saturation.cmx \ + proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ + metadataQuery.cmx equalityTactics.cmx paramodulation/equality.cmx \ + autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi @@ -150,6 +152,8 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi +setoids.cmo: proofEngineTypes.cmi setoids.cmi +setoids.cmx: proofEngineTypes.cmx setoids.cmi fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index cbf15f0df..6cd2bcf4a 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1873,7 +1873,7 @@ let main_demod_equalities dbd term metasenv ugraph = *) ;; -let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = +let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_uri = eq_of_goal ty in @@ -1917,13 +1917,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = else (* if newty = ty then *) raise (ProofEngineTypes.Fail (lazy "no progress")) (*else ProofEngineTypes.apply_tactic - (ReductionTactics.simpl_tac ~pattern) - initialstatus*) + (ReductionTactics.simpl_tac + ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~pattern = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) -;; +let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);; let rec find_in_ctx i name = function | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 8a03cd547..d48dfc349 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -48,9 +48,7 @@ val main_demod_equalities: HMysql.dbd -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit val main: HMysql.dbd -> bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit -val demodulate_tac: - dbd:HMysql.dbd -> - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic val superposition_tac: target:string -> table:string -> subterms_only:bool -> diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 73d864e1d..d8a3959bf 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -19,9 +19,7 @@ val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:(UriManager.uri * int) list -> ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic -val demodulate : - dbd:HMysql.dbd -> - pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 130c08e56..56037dde5 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -450,16 +450,16 @@ - - demodulation - demodulation - demodulation patt + + demodulate + demodulate + demodulate Synopsis: - demodulation &pattern; + demodulate diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index d521ac870..945a43837 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -643,11 +643,6 @@ &reduction-kind; ::= - demodulate - - - - | normalize Computes the βδιζ-normal form diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index dd14d8a26..58fd32afd 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -51,7 +51,11 @@ - demodulation pattern + + + demodulate + + discriminate sterm