From: Ferruccio Guidi Date: Wed, 15 Jun 2005 12:38:41 +0000 (+0000) Subject: beginning of the tactics lapply and fwd X-Git-Tag: PRE_STORAGE~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0aa359c7943ea10c70ae1ec053062c658b28b8ce;p=helm.git beginning of the tactics lapply and fwd used to support forward reasoning --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index feb161d7f..3b958c2c2 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -413,6 +413,10 @@ EXTEND | [ IDENT "transitivity" ]; t = tactic_term -> TacticAst.Transitivity (loc, t) + | [ IDENT "fwd" ]; name = IDENT -> + TacticAst.FwdSimpl (loc, name) + | [ IDENT "lapply" ]; t = term -> + TacticAst.LApply (loc, t, []) ] ]; tactical: diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 5cbda28d6..a845a332d 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -39,5 +39,10 @@ val type_of_aux': Cic.term -> CicUniv.universe_graph -> Cic.term * CicUniv.universe_graph +(* does_not_occur context lower upper term *) +(* searches for a Cic.Rel i in term with lower < i <= upper *) +val does_not_occur : Cic.context -> int -> int -> Cic.term -> bool + (* typechecks the obj and puts it in the environment *) val typecheck_obj : UriManager.uri -> Cic.obj -> unit + diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index fab264d07..76ce8994f 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -75,6 +75,8 @@ type ('term, 'ident) tactic = | Split of loc | Symmetry of loc | Transitivity of loc * 'term + | FwdSimpl of loc * 'ident + | LApply of loc * 'term * ('ident * 'term) list type thm_flavour = [ `Definition diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index b9babaa65..e86f77bd6 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -101,6 +101,7 @@ let rec pp_tactic = function | Split _ -> "split" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term + | FwdSimpl (_, ident) -> sprintf "fwd %s" ident let pp_flavour = function | `Definition -> "Definition" diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index e31ec55a9..d3d898457 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -10,9 +10,9 @@ cicUnification.cmx: freshNamesGenerator.cmx cicMetaSubst.cmx \ cicUnification.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi -coercGraph.cmo: freshNamesGenerator.cmi coercGraph.cmi -coercGraph.cmx: freshNamesGenerator.cmx coercGraph.cmi -cicRefine.cmo: freshNamesGenerator.cmi cicUnification.cmi cicMkImplicit.cmi \ - cicMetaSubst.cmi cicRefine.cmi -cicRefine.cmx: freshNamesGenerator.cmx cicUnification.cmx cicMkImplicit.cmx \ - cicMetaSubst.cmx cicRefine.cmi +coercGraph.cmo: freshNamesGenerator.cmi coercDb.cmi coercGraph.cmi +coercGraph.cmx: freshNamesGenerator.cmx coercDb.cmx coercGraph.cmi +cicRefine.cmo: freshNamesGenerator.cmi coercGraph.cmi cicUnification.cmi \ + cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi +cicRefine.cmx: freshNamesGenerator.cmx coercGraph.cmx cicUnification.cmx \ + cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index ecf65ea6d..d620a3c9a 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -19,9 +19,9 @@ http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \ http_getter_md5.cmo: http_getter_env.cmi http_getter_md5.cmi http_getter_md5.cmx: http_getter_env.cmx http_getter_md5.cmi http_getter_common.cmo: http_getter_types.cmo http_getter_misc.cmi \ - http_getter_env.cmi http_getter_common.cmi + http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \ - http_getter_env.cmx http_getter_common.cmi + http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi http_getter_map.cmo: http_getter_types.cmo http_getter_misc.cmi \ http_getter_map.cmi http_getter_map.cmx: http_getter_types.cmx http_getter_misc.cmx \ diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 2c6ce4b0f..02467679c 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -13,6 +13,7 @@ equalityTactics.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi +fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi @@ -89,6 +90,8 @@ fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ fourier.cmx equalityTactics.cmx fourierR.cmi +fwdSimplTactic.cmo: proofEngineTypes.cmi metadataQuery.cmi fwdSimplTactic.cmi +fwdSimplTactic.cmx: proofEngineTypes.cmx metadataQuery.cmx fwdSimplTactic.cmi history.cmo: history.cmi history.cmx: history.cmi statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ @@ -97,9 +100,11 @@ statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi tactics.cmo: variousTactics.cmi ring.cmi reductionTactics.cmi \ primitiveTactics.cmi negationTactics.cmi introductionTactics.cmi \ - fourierR.cmi equalityTactics.cmi eliminationTactics.cmi \ - discriminationTactics.cmi autoTactic.cmi tactics.cmi + fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \ + eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi \ + tactics.cmi tactics.cmx: variousTactics.cmx ring.cmx reductionTactics.cmx \ primitiveTactics.cmx negationTactics.cmx introductionTactics.cmx \ - fourierR.cmx equalityTactics.cmx eliminationTactics.cmx \ - discriminationTactics.cmx autoTactic.cmx tactics.cmi + fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \ + eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx \ + tactics.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 744527b1e..32f74fec2 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -14,12 +14,12 @@ INTERFACE_FILES = \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ - fourierR.mli history.mli statefulProofEngine.mli tactics.mli + fourierR.mli fwdSimplTactic.mli history.mli statefulProofEngine.mli tactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: -tactics.mli: tactics.ml *Tactics.mli autoTactic.mli fourierR.mli ring.mli +tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli echo "(* GENERATED FILE, DO NOT EDIT *)" > $@ $(OCAMLC) -i $< >> $@ diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml new file mode 100644 index 000000000..c1a5347f4 --- /dev/null +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -0,0 +1,87 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module MI = CicMkImplicit +module TC = CicTypeChecker +module PET = ProofEngineTypes +module U = CicUniv +module S = CicSubstitution +module PT = PrimitiveTactics + +(* +let module R = CicReduction +*) + +let fail_msg0 = "not a declaration of the current context" +let fail_msg1 = "no applicable simplification" + +let error msg = raise (PET.Fail msg) + +let rec declaration name = function + | [] -> error fail_msg0 + | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty + | _ :: tail -> declaration name tail + +(* lapply *******************************************************************) + +let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ?(substs = []) what = + let rec strip_dependent_prods metasenv context ss = function + | Cic.Prod (name, t1, t2) as t -> + if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else + let metasenv, index = MI.mk_implicit metasenv [] context in + let rs = MI.identity_relocation_list_for_metavariable context in + let e, s = Some (name, Cic.Decl t1), Some (Cic.Meta (index, rs)) in + strip_dependent_prods metasenv (e :: context) (s :: ss) t2 + | t -> metasenv, ss, t + in + let update_metasenv metasenv ((xuri, _, u,t), goal) = + ((xuri, metasenv, u,t), goal) + in + let lapply_tac status = + let (proof, goal) = status in + let _,metasenv,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in + let metasenv, substs, stripped_lemma = strip_dependent_prods metasenv context [] lemma in + let status = update_metasenv metasenv status in + let holed_lemma = S.subst_meta substs stripped_lemma in + PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status + in + PET.mk_tactic lapply_tac + +(* fwd **********************************************************************) + +let fwd_simpl_tac ~hyp ~dbd = + let fwd_simpl_tac status = + let (proof, goal) = status in + let _,metasenv,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let major = declaration hyp context in + match MetadataQuery.fwd_simpl ~dbd major with + | [] -> error fail_msg1 + | uri :: _ -> prerr_endline uri; (proof, []) + in + PET.mk_tactic fwd_simpl_tac diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli new file mode 100644 index 000000000..0b065f920 --- /dev/null +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val lapply_tac: + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?substs:(Cic.name * Cic.term) list -> Cic.term -> + ProofEngineTypes.tactic + +val fwd_simpl_tac: + hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 962aad8e7..1e7bbe690 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -444,4 +444,69 @@ let instance ~dbd t = (n,from,where) constraints_for_dummy_type in Constr.exec ~dbd (m,from,where) +(* fwd_simpl ****************************************************************) +let rec map_filter f n = function + | [] -> [] + | hd :: tl -> + match f n hd with + | None -> map_filter f (succ n) tl + | Some hd -> hd :: map_filter f (succ n) tl + +let get_uri t = + let aux = function + | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl) + | hd -> Some (CicUtil.uri_of_term hd, []) + in + try aux t with + | Invalid_argument "uri_of_term" -> None + +let get_metadata t = + let f n t = + match get_uri t with + | None -> None + | Some (uri, _) -> Some (n, uri) + in + match get_uri t with + | None -> None + | Some (uri, args) -> Some (uri, map_filter f 1 args) + +let debug_metadata = function + | None -> () + | Some (outer, inners) -> + let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n uri in + Printf.eprintf "\n%s: %s\n" "fwd" outer; + List.iter f inners; prerr_newline () + +let fwd_simpl ~dbd t = + let map inners row = + match row.(0), row.(1), row.(2) with + | Some source, Some inner, Some index -> + source, List.mem (int_of_string index, inner) inners + | _ -> "", false + in + let rec rank ranks (source, ok) = + match ranks, ok with + | [], false -> [source, 0] + | [], true -> [source, 1] + | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl + | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl + | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl + | hd :: tl, _ -> hd :: rank tl (source, ok) + in + let compare (_, x) (_, y) = compare x y in + let filter n (uri, rank) = + if rank > 0 then Some uri else None + in + match get_metadata t with + | None -> [] + | Some (outer, inners) -> + let select = "source, h_inner, h_index" in + let from = "genLemma" in + let where = Printf.sprintf "h_outer = \"%s\"" (Mysql.escape outer) in + let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in + let result = Mysql.exec dbd query in + let lemmas = Mysql.map result ~f:(map inners) in + let ranked = List.fold_left rank [] lemmas in + let ordered = List.rev (List.fast_sort compare ranked) in + map_filter filter 0 ordered diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 475b841f1..035f3ae73 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -54,3 +54,6 @@ val match_term: dbd:Mysql.dbd -> Cic.term -> string list val elim: dbd:Mysql.dbd -> string -> string list val instance: dbd:Mysql.dbd -> Cic.term -> string list + +val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> string list + diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml index 3ac33d2f5..5bbb01645 100644 --- a/helm/ocaml/tactics/tactics.ml +++ b/helm/ocaml/tactics/tactics.ml @@ -64,3 +64,5 @@ let symmetry = EqualityTactics.symmetry_tac let transitivity = EqualityTactics.transitivity_tac let whd = ReductionTactics.whd_tac let normalize = ReductionTactics.normalize_tac +let fwd_simpl = FwdSimplTactic.fwd_simpl_tac +let lapply = FwdSimplTactic.lapply_tac diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 780961d6b..ae9746da1 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -66,3 +66,7 @@ val whd : val normalize : also_in_hypotheses:bool -> terms:Cic.term list option -> ProofEngineTypes.tactic +val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic +val lapply : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic