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))
126 let mk_morphism eq amount ft p1 vl =
133 | Terms.Var _ -> assert false
135 let dag,arity = ____ in
137 HExtlib.list_rev_mapi_filter
139 if i < arity then None
140 else if i = n then Some (aux t tl)
141 else Some (NCic.Appl [refl ...]))
145 in aux ft (List.rev pl)
149 let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
150 let module Subst = FoSubst in
152 let rec aux = function
154 | (j,_) :: tl when i = j -> 1
155 | _ :: tl -> 1 + aux tl
159 let vars_of i l = fst (List.assoc i l) in
160 let ty_of i l = snd (List.assoc i l) in
161 let close_with_lambdas vl t =
164 NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
167 let close_with_forall vl t =
170 NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
174 let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
175 let lit =match lit with
176 | Terms.Predicate t -> assert false
177 | Terms.Equation (l,r,ty,_) ->
178 Terms.Node [ Terms.Leaf eqP(); ty; l; r]
182 let mk_refl = function
183 | NCic.Appl [_; ty; l; _]
184 -> NCic.Appl [eq_refl();ty;l]
188 let lit,_,_ = get_literal mp in
189 let lit = Subst.apply_subst subst lit in
191 let rec aux ongoal seen = function
194 let amount = List.length seen in
195 let lit,vl,proof = get_literal id in
196 if not ongoal && id = mp then
197 let lit = Subst.apply_subst subst lit in
198 let eq_ty = extract amount [] lit in
199 let refl = mk_refl eq_ty in
200 (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
201 (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
202 aux true ((id,([],lit))::seen) (id::tl))) *)
203 NCicSubstitution.subst
204 ~avoid_beta_redexes:true ~no_implicit:false refl
205 (aux true ((id,([],lit))::seen) (id::tl))
208 | Terms.Exact _ when tl=[] ->
209 (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
211 | Terms.Step _ when tl=[] -> assert false
213 (* prerr_endline ("Exact for " ^ (string_of_int id));*)
215 NCic.LetIn ("clause_" ^ string_of_int id,
216 close_with_forall vl (extract amount vl lit),
217 close_with_lambdas vl (extract amount vl ft),
219 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
221 NCicSubstitution.subst
222 ~avoid_beta_redexes:true ~no_implicit:false
223 (close_with_lambdas vl (extract amount vl ft))
225 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
226 | Terms.Step (_, id1, id2, dir, pos, subst) ->
227 let id, id1,(lit,vl,proof) =
228 if ongoal then id1,id,get_literal id1
229 else id,id1,(lit,vl,proof)
231 let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
233 let vars = List.rev (vars_of id seen) in
234 let args = List.map (Subst.apply_subst subst) vars in
235 let args = List.map (extract amount vl) args in
236 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
237 if args = [] then rel_for_id
238 else NCic.Appl (rel_for_id::args)
240 let p_id1 = proof_of_id id1 in
241 let p_id2 = proof_of_id id2 in
242 let pred, hole_type, l, r =
243 let id1_ty = ty_of id1 seen in
245 match ty_of id2 seen with
246 | Terms.Node [ _; t; l; r ] ->
247 extract amount vl (Subst.apply_subst subst t),
248 extract amount vl (Subst.apply_subst subst l),
249 extract amount vl (Subst.apply_subst subst r)
252 (*prerr_endline "mk_predicate :";
253 if ongoal then prerr_endline "ongoal=true"
254 else prerr_endline "ongoal=false";
255 prerr_endline ("id=" ^ string_of_int id);
256 prerr_endline ("id1=" ^ string_of_int id1);
257 prerr_endline ("id2=" ^ string_of_int id2);
258 prerr_endline ("Positions :" ^
260 (List.map string_of_int pos)));*)
262 id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
267 if (ongoal=true) = (dir=Terms.Left2Right) then
272 let body = aux ongoal
273 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
275 if NCicUntrusted.count_occurrences [] 0 body <= 1 then
276 NCicSubstitution.subst
277 ~avoid_beta_redexes:true ~no_implicit:false
278 (close_with_lambdas vl (NCic.Appl
279 [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
282 NCic.LetIn ("clause_" ^ string_of_int id,
283 close_with_forall vl (extract amount vl lit),
284 (* NCic.Implicit `Type, *)
285 close_with_lambdas vl (NCic.Appl
286 [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
289 aux false [] steps, proof_type