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: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
14 NCicBlob.set_default_eqP()
16 NCicProof.set_default_sig()
20 let print s = prerr_endline (Lazy.force s);;
23 module B : Orderings.Blob
24 with type t = NCic.term and type input = NCic.term
25 = Orderings.LPO(NCicBlob.NCicBlob)
27 module NCicParamod = Paramod.Paramod(B)
29 let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
32 print_endline (Pp.pp_unit_clause ~margin:max_int
33 (fst(Terms.M.find x bag)))) l;
35 (* let stamp = Unix.gettimeofday () in *)
36 let proofterm,prooftype = NCicProof.mk_proof status ~demod bag i fo_subst l in
37 (* debug (lazy (Printf.sprintf "Got proof term in %fs"
38 (Unix.gettimeofday() -. stamp))); *)
40 let metasenv, proofterm =
41 let rec aux k metasenv = function
42 | NCic.Meta _ as t -> metasenv, t
44 let metasenv, i, _, _ =
45 NCicMetaSubst.mk_meta metasenv context `IsTerm
47 metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
48 | t -> NCicUntrusted.map_term_fold_a
49 (fun _ k -> k+1) k aux metasenv t
51 aux 0 metasenv proofterm
53 debug (lazy (status#ppterm ~metasenv ~subst ~context proofterm));
55 let stamp = Unix.gettimeofday () in
56 let metasenv, subst, proofterm, _prooftype =
58 (status#set_coerc_db NCicCoercion.empty_db)
59 metasenv subst context proofterm None
61 print (lazy (Printf.sprintf "Refined in %fs"
62 (Unix.gettimeofday() -. stamp)));
64 proofterm, prooftype, metasenv, subst
66 let nparamod status metasenv subst context t table =
67 let module P = NCicParamod in
68 let module Pp = Pp.Pp(B) in
69 let bag, maxvar = Terms.empty_bag, 0 in
71 NCicBlob.saturate status metasenv subst context t ty in
72 let (bag,maxvar), goals =
74 (fun x _ a -> P.mk_goal a (saturate x)) (bag,maxvar) [t]
76 let (bag,maxvar), passives =
78 (fun x _ a -> P.mk_passive a (saturate x)) (bag,maxvar) table
81 P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
82 ~g_passives:goals ~passives (bag,maxvar)
84 | P.Error _ | P.GaveUp | P.Timeout _ -> []
85 | P.Unsatisfiable solutions ->
86 List.map (readback status metasenv subst context) solutions
89 module CB = NCicBlob.NCicBlob
90 module P = NCicParamod
93 let empty_state = P.empty_state
95 let size_of_state = P.size_of_state
97 let forward_infer_step status metasenv subst context s t ty =
98 let bag = P.bag_of_state s in
100 NCicBlob.saturate status metasenv subst context t ty in
101 let bag,clause = P.mk_passive bag (saturate (t,ty)) in
102 if Terms.is_eq_clause clause then
103 ((*prerr_endline "is eq";*)
104 P.forward_infer_step (P.replace_bag s bag) clause 0)
105 else ((*print (lazy "not eq");*) s)
108 let index_obj status s uri =
109 let obj = NCicEnvironment.get_checked_obj status uri in
110 debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
111 debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri)))));
113 | (_,_,[],[],NCic.Constant(_,_,None,ty,_)) ->
114 let nref = NReference.reference_of_spec uri NReference.Decl in
115 forward_infer_step status [] [] [] s (NCic.Const nref) ty
116 | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
117 let nref = NReference.reference_of_spec uri (NReference.Def d) in
118 forward_infer_step status [] [] [] s (NCic.Const nref) ty
122 let demod status metasenv subst context s goal =
123 (* let stamp = Unix.gettimeofday () in *)
124 match P.demod s goal with
125 | P.Error _ | P.GaveUp | P.Timeout _ -> []
126 | P.Unsatisfiable solutions ->
127 (* print (lazy (Printf.sprintf "Got solutions in %fs"
128 (Unix.gettimeofday() -. stamp))); *)
129 List.map (readback ~demod:true status metasenv subst context) solutions
132 let paramod status metasenv subst context s goal =
133 (* let stamp = Unix.gettimeofday () in *)
134 match P.nparamod ~useage:true ~max_steps:max_int
135 ~timeout:(Unix.gettimeofday () +. 300.0) s goal with
136 | P.Error _ | P.GaveUp | P.Timeout _ -> []
137 | P.Unsatisfiable solutions ->
138 (* print (lazy (Printf.sprintf "Got solutions in %fs"
139 (Unix.gettimeofday() -. stamp))); *)
140 List.map (readback status metasenv subst context) solutions
143 let fast_eq_check status metasenv subst context s goal =
144 (* let stamp = Unix.gettimeofday () in *)
145 match P.fast_eq_check s goal with
146 | P.Error _ | P.GaveUp | P.Timeout _ -> []
147 | P.Unsatisfiable solutions ->
148 (* print (lazy (Printf.sprintf "Got solutions in %fs"
149 (Unix.gettimeofday() -. stamp))); *)
150 List.map (readback status metasenv subst context) solutions
153 let is_equation status metasenv subst context ty =
155 NCicMetaSubst.saturate status ~delta:0 metasenv subst context
158 | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true
163 let demodulate status metasenv subst context s goal =
164 (* let stamp = Unix.gettimeofday () in *)
165 match P.fast_eq_check s goal with
166 | P.Error _ | P.GaveUp | P.Timeout _ -> []
167 | P.Unsatisfiable solutions ->
168 (* print (lazy (Printf.sprintf "Got solutions in %fs"
169 (Unix.gettimeofday() -. stamp))); *)
170 List.map (readback status metasenv subst context) solutions