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:= f;;
18 let get_sig = fun x -> !eqsig x;;
20 let default_sig = function
22 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
23 let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
26 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
27 let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
30 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
31 let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
34 let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
35 let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
38 let set_default_sig () =
39 prerr_endline "setting default sig";
42 let set_reference_of_oxuri reference_of_oxuri =
43 prerr_endline "setting oxuri in nCicProof";
48 (UriManager.uri_of_string
49 "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
53 (UriManager.uri_of_string
54 "cic:/matita/logic/equality/eq_ind.con"))
58 (UriManager.uri_of_string
59 "cic:/matita/logic/equality/eq_elim_r.con"))
63 (UriManager.uri_of_string
64 "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
68 (* let debug c r = prerr_endline r; c *)
71 let eqP() = debug (!eqsig Eq) "eq" ;;
72 let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
73 let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";;
74 let eq_refl() = 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 subst 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 mk_refl = function
159 | NCic.Appl [_; ty; l; _]
160 -> NCic.Appl [eq_refl();ty;l]
164 let lit,_,_ = get_literal mp in
165 let lit = Subst.apply_subst subst lit in
167 let rec aux ongoal seen = function
170 let amount = List.length seen in
171 let lit,vl,proof = get_literal id in
172 if not ongoal && id = mp then
173 let lit = Subst.apply_subst subst lit in
174 let eq_ty = extract amount [] lit in
175 let refl = mk_refl eq_ty in
176 ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
177 NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
178 aux true ((id,([],lit))::seen) (id::tl)))
181 | Terms.Exact _ when tl=[] ->
182 (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
184 | Terms.Step _ when tl=[] -> assert false
186 (* prerr_endline ("Exact for " ^ (string_of_int id));*)
187 NCic.LetIn ("clause_" ^ string_of_int id,
188 close_with_forall vl (extract amount vl lit),
189 close_with_lambdas vl (extract amount vl ft),
191 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
192 | Terms.Step (_, id1, id2, dir, pos, subst) ->
193 let id, id1,(lit,vl,proof) =
194 if ongoal then id1,id,get_literal id1
195 else id,id1,(lit,vl,proof)
197 let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
199 let vars = List.rev (vars_of id seen) in
200 let args = List.map (Subst.apply_subst subst) vars in
201 let args = List.map (extract amount vl) args in
202 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
203 if args = [] then rel_for_id
204 else NCic.Appl (rel_for_id::args)
206 let p_id1 = proof_of_id id1 in
207 let p_id2 = proof_of_id id2 in
208 let pred, hole_type, l, r =
209 let id1_ty = ty_of id1 seen in
211 match ty_of id2 seen with
212 | Terms.Node [ _; t; l; r ] ->
213 extract amount vl (Subst.apply_subst subst t),
214 extract amount vl (Subst.apply_subst subst l),
215 extract amount vl (Subst.apply_subst subst r)
218 (*prerr_endline "mk_predicate :";
219 if ongoal then prerr_endline "ongoal=true"
220 else prerr_endline "ongoal=false";
221 prerr_endline ("id=" ^ string_of_int id);
222 prerr_endline ("id1=" ^ string_of_int id1);
223 prerr_endline ("id2=" ^ string_of_int id2);
224 prerr_endline ("Positions :" ^
226 (List.map string_of_int pos)));*)
228 id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
233 if (ongoal=true) = (dir=Terms.Left2Right) then
238 NCic.LetIn ("clause_" ^ string_of_int id,
239 close_with_forall vl (extract amount vl lit),
240 (* NCic.Implicit `Type, *)
241 close_with_lambdas vl
242 (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
244 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
246 aux false [] steps, proof_type