2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
19 open Continuationals.Stack
21 module Ast = CicNotationPt
23 (* =================================== paramod =========================== *)
24 let auto_paramod ~params:(l,_) status goal =
25 let gty = get_goalty status goal in
26 let n,h,metasenv,subst,o = status#obj in
27 let status,t = term_of_cic_term status gty (ctx_of gty) in
31 let status, t = disambiguate status t None (ctx_of gty) in
32 let status, ty = typeof status (ctx_of t) t in
33 let status, t = term_of_cic_term status t (ctx_of gty) in
34 let status, ty = term_of_cic_term status ty (ctx_of ty) in
35 (status, (t,ty) :: l))
39 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
41 | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
42 | (pt, metasenv, subst)::_ ->
43 let status = status#set_obj (n,h,metasenv,subst,o) in
44 instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
47 let auto_paramod_tac ~params status =
48 NTactics.distribute_tac (auto_paramod ~params) status
51 (* =================================== auto =========================== *)
52 let auto_tac ~params status =
53 prerr_endline "I teoremi noti sono";
54 NDiscriminationTree.DiscriminationTree.iter status#auto_cache
58 (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
59 (NDiscriminationTree.TermSet.elements t));
63 (* ========================= dispatching of auto/auto_paramod ============ *)
64 let auto_tac ~params:(_,flags as params) =
65 if List.mem_assoc "paramodulation" flags then
66 auto_paramod_tac ~params