in
Tactics.fold ~reduction ~pattern
| TacticAst.Fourier _ -> Tactics.fourier
- | TacticAst.FwdSimpl (_, term) ->
- Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+ | TacticAst.FwdSimpl (_, hyp, names) ->
+ Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ())
| TacticAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
| TacticAst.Intros (_, Some num, names) ->
PrimitiveTactics.intros_tac ~howmany:num
~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.LApply (_, to_what, what, ident) ->
+ | TacticAst.LApply (_, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
| TacticAst.Left _ -> Tactics.left
| TacticAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| TacticAst.Fold (loc,reduction_kind, pattern) ->
let status, pattern = disambiguate_pattern status pattern in
status, TacticAst.Fold (loc,reduction_kind, pattern)
- | TacticAst.FwdSimpl (loc, term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.FwdSimpl (loc, term)
+ | TacticAst.FwdSimpl (loc, hyp, names) ->
+ status, TacticAst.FwdSimpl (loc, hyp, names)
| TacticAst.Fourier loc -> status, TacticAst.Fourier loc
| TacticAst.Generalize (loc,pattern,ident) ->
let status, pattern = disambiguate_pattern status pattern in
status, TacticAst.Injection (loc,term)
| TacticAst.Intros (loc, num, names) ->
status, TacticAst.Intros (loc, num, names)
- | TacticAst.LApply (loc, to_what, what, ident) ->
- let status, to_what =
- match to_what with
- None -> status,None
- | Some to_what ->
- let status, to_what = disambiguate_term status to_what in
- status, Some to_what
+ | TacticAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term (status, to_what) =
+ let status, term = disambiguate_term status term in
+ status, term :: to_what
in
+ let status, to_what = List.fold_right f to_what (status, []) in
let status, what = disambiguate_term status what in
- status, TacticAst.LApply (loc, to_what, what, ident)
+ status, TacticAst.LApply (loc, depth, to_what, what, ident)
| TacticAst.Left loc -> status, TacticAst.Left loc
| TacticAst.LetIn (loc, term, name) ->
let status, term = disambiguate_term status term in
alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
alias symbol "and" (instance 0) = "logical and".
alias symbol "eq" (instance 0) = "leibnitz's equality".
alias symbol "exists" (instance 0) = "exists".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
definition is_S: nat \to Prop \def
\lambda n. match n with
qed.
theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n).
-intros. cut (\exists p. (S n) = (S p) \land (le m p)).
-elim Hcut. elim H1. cut x = n.
-elim Hcut1. auto. symmetry. auto. auto.
+intros.
+lapply le_gen_S_x to H using H0. elim H0. elim H1.
+lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
qed.
theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
intros. auto.
qed.
-
-theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to
- \exists n. x = (S n) \land (le m n).
-intros.
-lapply le_gen_S_x to H using H0. elim H0. elim H1.
-exists. exact x1. auto.
-qed.
-
-(* proof of le_gen_S_S with lapply *)
-theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n).
-intros.
-lapply le_gen_S_x_2 to H using H0. elim H0. elim H1.
-lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
-qed.
+(*
+theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
+intros 1.
+elim x. auto.
+fwd H1 [].
+*)
ident_list0: [
[ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
];
+ tactic_term_list1: [
+ [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
+ ];
reduction_kind: [
[ [ IDENT "reduce" ] -> `Reduce
| [ IDENT "simplify" ] -> `Simpl
TacticAst.Assumption loc
| IDENT "auto";
depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
- width = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ] ->
+ width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] ->
TacticAst.Auto (loc,depth,width)
| IDENT "clear"; id = IDENT ->
TacticAst.Clear (loc,id)
TacticAst.Cut (loc, ident, t)
| IDENT "decide"; IDENT "equality" ->
TacticAst.DecideEquality loc
- | IDENT "decompose"; where = term ->
+ | IDENT "decompose"; where = tactic_term ->
TacticAst.Decompose (loc, where)
| IDENT "discriminate"; t = tactic_term ->
TacticAst.Discriminate (loc, t)
TacticAst.Fold (loc, kind, p)
| IDENT "fourier" ->
TacticAst.Fourier loc
- | IDENT "fwd"; t = term ->
- TacticAst.FwdSimpl (loc, t)
+ | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.FwdSimpl (loc, hyp, idents)
| 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
- | IDENT "injection"; t = term ->
+ | IDENT "injection"; t = tactic_term ->
TacticAst.Injection (loc, t)
- | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
- let idents = match idents with None -> [] | Some idents -> idents in
- TacticAst.Intros (loc, num, idents)
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
TacticAst.Intros (loc, Some 1, idents)
- | IDENT "lapply"; what = tactic_term;
- to_what = OPT [ "to" ; t = tactic_term -> t ];
- ident = OPT [ "using" ; id = IDENT -> id ] ->
- TacticAst.LApply (loc, to_what, what, ident)
+ | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.Intros (loc, num, idents)
+ | IDENT "lapply";
+ depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
+ what = tactic_term;
+ to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
+ ident = OPT [ "using" ; ident = IDENT -> ident ] ->
+ let to_what = match to_what with None -> [] | Some to_what -> to_what in
+ TacticAst.LApply (loc, depth, to_what, what, ident)
| IDENT "left" -> TacticAst.Left loc
| IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
TacticAst.LetIn (loc, t, where)
TacticAst.Reflexivity loc
| IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
TacticAst.Replace (loc, p, t)
- | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec ->
+ | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
let (pt,_,_) = p in
if pt <> None then
raise
]
| "then" NONA
[ tac = tactical;
- PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+ PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
(TacticAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
| Fail of loc
| Fold of loc * reduction_kind * ('term, 'ident) pattern
| Fourier of loc
- | FwdSimpl of loc * 'term
+ | FwdSimpl of loc * string * 'ident list
| 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
| Intros of loc * int option * 'ident list
- | LApply of loc * 'term option * 'term * 'ident option
+ | 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
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
| `Reduce -> "reduce"
| `Simpl -> "simplify"
| Exists _ -> "exists"
| Fold (_, kind, pattern) ->
sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern)
+ | FwdSimpl (_, hyp, idents) ->
+ sprintf "fwd %s%s" hyp
+ (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
| Generalize (_, pattern, ident) ->
sprintf "generalize %s%s" (pp_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
sprintf "intros%s%s"
(match num with None -> "" | Some num -> " " ^ string_of_int num)
(match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+ | LApply (_, level_opt, terms, term, ident_opt) ->
+ sprintf "lapply %s%s%s%s"
+ (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
+ (pp_term_ast term)
+ (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms)
+ (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
| Left _ -> "left"
| LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident
| Reduce (_, kind, pat) ->
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
- | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term)
- | LApply (_, term_opt, term, ident) ->
- sprintf "lapply %s%s%s" (pp_term_ast term)
- (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t)
- (match ident with None -> "" | Some id -> " using " ^ id)
let pp_flavour = function
| `Definition -> "Definition"
proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
proofEngineStructuralRules.cmi
primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
- proofEngineHelpers.cmi primitiveTactics.cmi
+ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi
primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
- proofEngineHelpers.cmx primitiveTactics.cmi
+ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi
hashtbl_equiv.cmo: hashtbl_equiv.cmi
hashtbl_equiv.cmx: hashtbl_equiv.cmi
metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \
proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
fourier.cmx equalityTactics.cmx fourierR.cmi
-fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
- primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi
-fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
- primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi
+fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
+ proofEngineStructuralRules.cmi primitiveTactics.cmi metadataQuery.cmi \
+ fwdSimplTactic.cmi
+fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
+ proofEngineStructuralRules.cmx primitiveTactics.cmx metadataQuery.cmx \
+ fwdSimplTactic.cmi
history.cmo: history.cmi
history.cmx: history.cmi
statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
* http://cs.unibo.it/helm/.
*)
-module MI = CicMkImplicit
-module TC = CicTypeChecker
-module PET = ProofEngineTypes
+(*
module PEH = ProofEngineHelpers
+*)
module U = CicUniv
+module TC = CicTypeChecker
+module PET = ProofEngineTypes
module S = CicSubstitution
module PT = PrimitiveTactics
module T = Tacticals
module FNG = FreshNamesGenerator
+module MI = CicMkImplicit
+module PESR = ProofEngineStructuralRules
-let fail_msg1 = "no applicable simplification"
+let fail_msg0 = "unexported clearbody: invalid argument"
+let fail_msg1 = "fwd: argument is not premise in the current goal"
+let fail_msg2 = "fwd: no applicable simplification"
let error msg = raise (PET.Fail msg)
+(* unexported tactics *******************************************************)
+
+let clearbody ~index =
+ let rec find_name index = function
+ | Some (Cic.Name name, _) :: _ when index = 1 -> name
+ | _ :: tail when index > 1 -> find_name (pred index) tail
+ | _ -> error fail_msg0
+ in
+ let clearbody status =
+ let (proof, goal) = status in
+ let _, metasenv, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
+ in
+ PET.mk_tactic clearbody
+
(* lapply *******************************************************************)
-let strip_dependent_prods metasenv context t =
+let strip_prods metasenv context ?how_many to_what term =
let irl = MI.identity_relocation_list_for_metavariable context in
- let mk_meta metasenv t =
+ let mk_meta metasenv its_type =
let index = MI.new_meta metasenv [] in
- let metasenv = [index, context, t] @ metasenv in
- metasenv, Cic.Meta (index, irl)
+ let metasenv = [index, context, its_type] @ metasenv in
+ metasenv, Cic.Meta (index, irl), index
in
- let rec aux metasenv metas = function
- | Cic.Prod (Cic.Name _ as name, t1, t2) ->
- let metasenv, meta = mk_meta metasenv t1 in
- aux metasenv (meta :: metas) (S.subst meta t2)
- | Cic.Prod (Cic.Anonymous, t1, _) ->
- let metasenv, meta = mk_meta metasenv t1 in
- metasenv, metas, Some meta
- | t -> metasenv, metas, None
+ let update_counters = function
+ | None, [] -> None, T.id_tac, []
+ | None, to_what :: tail -> None, PT.apply_tac ~term:to_what, tail
+ | Some hm, [] -> Some (pred hm), T.id_tac, []
+ | Some hm, to_what :: tail -> Some (pred hm), PT.apply_tac ~term:to_what, tail
+ in
+ let rec aux metasenv metas conts tw = function
+ | Some hm, _ when hm <= 0 -> metasenv, metas, conts
+ | xhm, Cic.Prod (Cic.Name _, t1, t2) ->
+ let metasenv, meta, index = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) ((T.id_tac, index) :: conts) tw (xhm, (S.subst meta t2))
+ | xhm, Cic.Prod (Cic.Anonymous, t1, t2) ->
+ let xhm, tac, tw = update_counters (xhm, tw) in
+ let metasenv, meta, index = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) ((tac, index) :: conts) tw (xhm, (S.subst meta t2))
+ | _, t -> metasenv, metas, conts
in
- aux metasenv [] t
+ aux metasenv [] [] to_what (how_many, term)
let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- (* ?(substs = []) *) ?to_what what =
+ (* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
let xuri, metasenv, u, t = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
- match strip_dependent_prods metasenv context lemma with
- | metasenv, metas, Some meta ->
- let pippo = Cic.Appl (what :: List.rev (meta :: metas)) in
- Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr;
- let outer_tac = letin_tac pippo in
- let status = (xuri, metasenv, u, t), goal in
- PET.apply_tactic outer_tac status
- | metasenv, metas, None ->
- failwith "lapply_tac: not implemented"
+ let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
+ let conclusion = Cic.Appl (what :: List.rev metas) in
+ let tac = T.thens ~start:(letin_tac conclusion)
+ ~continuations:[clearbody ~index:1]
+ in
+ let proof = (xuri, metasenv, u, t) in
+ let aux (proof, goals) (tac, goal) =
+ let proof, new_goals = PET.apply_tactic tac (proof, goal) in
+ proof, goals @ new_goals
+ in
+ List.fold_left aux (proof, []) ((tac, goal) :: conts)
in
PET.mk_tactic lapply_tac
-(*
-
-
-
-let skip_metas p =
- let rec aux conts p =
- if p <= 0 then conts else aux (T.id_tac :: conts) (pred p)
- in
- aux [] p
-
-let get_conclusion context t =
- let rec aux p context = function
- | Cic.Prod (name, t1, t2) ->
- aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
- | Cic.LetIn (name, u1, t2) ->
- aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
- | Cic.Cast (t2, t1) -> aux p context t2
- | t -> p, context, t
- in aux 0 context t
+(* fwd **********************************************************************)
-let get_conclusion_dependences context t =
- let p, context, conclusion = get_conclusion context t in
- let rec aux l q =
- if q <= 0 then l else
- let b = TC.does_not_occur context (pred q) q conclusion in
- aux (b :: l) (pred q)
+let fwd_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ ~hyp ~dbd =
+ let find_type metasenv context =
+ let rec aux p = function
+ | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
+ p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph)
+ | _ :: tail -> aux (succ p) tail
+ | [] -> error fail_msg1
+ in
+ aux 1 context
in
- aux [] p
-
-let solve_independents ?with_what deps =
- let rec aux p conts = function
- | [] -> p, conts
- | true :: tl ->
- let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
- aux (succ p) (cont :: conts) tl
- | false :: tl -> aux (succ p) conts tl
- in
- let p, conts = aux 0 [] deps in
- match with_what with
- | None -> conts
- | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
-
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- (* ?(substs = []) *) ?to_what what =
- let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
- let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
- let solve_conclusion_tac ?with_what p deps =
- T.then_ ~start:(intros_tac ())
- ~continuation:(
- T.thens ~start:(PT.apply_tac what)
- ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ]
-(* skip_metas p @ solve_independents ?with_what deps *)
- )
- )
+ let lapply_tac to_what lemma =
+ lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma
in
- let lapply_tac (proof, goal) =
- let xuri, metasenv, u, t = proof in
- let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
- let lemma = FNG.clean_dummy_dependent_types lemma in
- match strip_dependent_prods metasenv context lemma with
- | metasenv, p, Some premise, conclusion ->
- let deps = get_conclusion_dependences context conclusion in
- let inner_tac = match to_what with
- | None ->
- T.thens ~start:(cut_tac premise)
- ~continuations:[
- solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
- T.id_tac
- ]
- | Some with_what ->
- solve_conclusion_tac ~with_what p deps
- in
- let outer_tac =
- T.thens ~start:(cut_tac conclusion)
- ~continuations:[T.id_tac; T.id_tac (* inner_tac *)]
- in
-*)
-(* fwd **********************************************************************)
-
-let fwd_simpl_tac ~what ~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, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+ let index, major = find_type metasenv context in
match MetadataQuery.fwd_simpl ~dbd major with
- | [] -> error fail_msg1
- | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
+ | [] -> error fail_msg2
+ | uri :: _ ->
+ Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
+ let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in
+ let tac = T.thens ~start ~continuations:[PESR.clearbody hyp] in
+ PET.apply_tactic tac status
in
PET.mk_tactic fwd_simpl_tac
val lapply_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val fwd_simpl_tac:
- what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
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;
+ let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in
+ Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer);
List.iter f inners; prerr_newline ()
let fwd_simpl ~dbd t =
let compare (_, x) (_, y) = compare x y in
let filter n (uri, rank) =
if rank > 0 then Some (UriManager.uri_of_string uri) else None
- in
- match get_metadata t with
+ in
+ let metadata = get_metadata t in debug_metadata metadata;
+ match metadata with
| None -> []
| Some (outer, inners) ->
let select = "source, h_inner, h_index" 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
+ map_filter filter 0 ordered
reduction:(Cic.context -> Cic.term -> Cic.term) ->
pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val fourier : ProofEngineTypes.tactic
-val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val fwd_simpl :
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
ProofEngineTypes.pattern -> ProofEngineTypes.tactic
unit -> ProofEngineTypes.tactic
val lapply :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ ?how_many:int ->
+ ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val left : ProofEngineTypes.tactic
val letin :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
projects / helm.git / commitdiff