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 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
16 let eqsig = ref (fun _ -> assert false);;
17 let set_sig f = eqsig:=
21 let default_sig = function
23 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
24 let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
27 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
28 let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
31 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
32 let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
35 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
36 let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
39 let set_default_sig () =
40 prerr_endline "setting default sig";
43 let set_reference_of_oxuri reference_of_oxuri =
44 prerr_endline "setting oxuri in nCicProof";
49 (UriManager.uri_of_string
50 "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
54 (UriManager.uri_of_string
55 "cic:/matita/logic/equality/eq_ind.con"))
59 (UriManager.uri_of_string
60 "cic:/matita/logic/equality/eq_elim_r.con"))
64 (UriManager.uri_of_string
65 "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
69 let debug c r = prerr_endline r; c
71 let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp" ;;
72 let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;;
73 let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";;
74 let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";;
77 let extract lift vl t =
78 let rec pos i = function
79 | [] -> raise Not_found
80 | j :: tl when j <> i -> 1+ pos i tl
83 let vl_len = List.length vl in
84 let rec extract = function
85 | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
87 (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
88 | Terms.Node l -> NCic.Appl (List.map extract l)
93 let mk_predicate hole_type amount ft p1 vl =
102 Pp.Pp(NCicBlob.NCicBlob(
104 let metasenv = [] let subst = [] let context = []
107 prerr_endline ("term: " ^ Pp.pp_foterm ft);
108 prerr_endline ("path: " ^ String.concat ","
109 (List.map string_of_int p1));
110 prerr_endline ("leading to: " ^ Pp.pp_foterm t);
116 if i = n then aux t tl
117 else extract amount (0::vl) t)
122 NCic.Lambda("x", hole_type, aux ft (List.rev p1))
125 let mk_proof (bag : NCic.term Terms.bag) mp steps =
126 let module Subst = FoSubst in
128 let rec aux = function
130 | (j,_) :: tl when i = j -> 1
131 | _ :: tl -> 1 + aux tl
135 let vars_of i l = fst (List.assoc i l) in
136 let ty_of i l = snd (List.assoc i l) in
137 let close_with_lambdas vl t =
140 NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
143 let close_with_forall vl t =
146 NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
150 let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
151 let lit =match lit with
152 | Terms.Predicate t -> assert false
153 | Terms.Equation (l,r,ty,_) ->
154 Terms.Node [ Terms.Leaf eqP(); ty; l; r]
158 let rec aux ongoal seen = function
161 let amount = List.length seen in
162 let lit,vl,proof = get_literal id in
163 if not ongoal && id = mp then
164 ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
165 NCic.LetIn ("clause_" ^ string_of_int id,
166 extract amount [] lit,
167 (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
168 aux true ((id,([],lit))::seen) (id::tl)))
171 | Terms.Exact _ when tl=[] ->
172 (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
174 | Terms.Step _ when tl=[] -> assert false
176 (* prerr_endline ("Exact for " ^ (string_of_int id));*)
177 NCic.LetIn ("clause_" ^ string_of_int id,
178 close_with_forall vl (extract amount vl lit),
179 close_with_lambdas vl (extract amount vl ft),
181 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
182 | Terms.Step (_, id1, id2, dir, pos, subst) ->
183 let id, id1,(lit,vl,proof) =
184 if ongoal then id1,id,get_literal id1
185 else id,id1,(lit,vl,proof)
187 let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
189 let vars = List.rev (vars_of id seen) in
190 let args = List.map (Subst.apply_subst subst) vars in
191 let args = List.map (extract amount vl) args in
192 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
193 if args = [] then rel_for_id
194 else NCic.Appl (rel_for_id::args)
196 let p_id1 = proof_of_id id1 in
197 let p_id2 = proof_of_id id2 in
198 let pred, hole_type, l, r =
199 let id1_ty = ty_of id1 seen in
201 match ty_of id2 seen with
202 | Terms.Node [ _; t; l; r ] ->
203 extract amount vl (Subst.apply_subst subst t),
204 extract amount vl (Subst.apply_subst subst l),
205 extract amount vl (Subst.apply_subst subst r)
208 (*prerr_endline "mk_predicate :";
209 if ongoal then prerr_endline "ongoal=true"
210 else prerr_endline "ongoal=false";
211 prerr_endline ("id=" ^ string_of_int id);
212 prerr_endline ("id1=" ^ string_of_int id1);
213 prerr_endline ("id2=" ^ string_of_int id2);
214 prerr_endline ("Positions :" ^
216 (List.map string_of_int pos)));*)
218 id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
223 if (ongoal=true) = (dir=Terms.Left2Right) then
228 NCic.LetIn ("clause_" ^ string_of_int id,
229 close_with_forall vl (extract amount vl lit),
230 (* NCic.Implicit `Type, *)
231 close_with_lambdas vl
232 (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
234 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)