| [ 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:
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
+
| 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
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
+ | FwdSimpl (_, ident) -> sprintf "fwd %s" ident
let pp_flavour = function
| `Definition -> "Definition"
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
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 \
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
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 \
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
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 $< >> $@
--- /dev/null
+(* 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
--- /dev/null
+(* 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
(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
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
+
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
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
projects / helm.git / commitdiff