]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/nCicProof.ml
some corrections ...
[helm.git] / helm / software / components / ng_paramodulation / nCicProof.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
13
14 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
15               
16 let eqsig = ref (fun _ -> assert false);;
17 let set_sig f = eqsig:= f;;
18 let get_sig = fun x -> !eqsig x;;
19
20 let default_sig = function
21   | Eq -> 
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
24         NCic.Const ref
25   | EqInd_l -> 
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
28         NCic.Const ref
29   | EqInd_r -> 
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
32         NCic.Const ref
33   | Refl ->
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
36         NCic.Const ref
37
38 let set_default_sig () =
39   (*prerr_endline "setting default sig";*)
40   eqsig := default_sig
41
42 let set_reference_of_oxuri reference_of_oxuri = 
43   prerr_endline "setting oxuri in nCicProof";
44   let nsig = function
45     | Eq -> 
46         NCic.Const
47           (reference_of_oxuri 
48              (UriManager.uri_of_string 
49                 "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))  
50     | EqInd_l -> 
51         NCic.Const
52           (reference_of_oxuri 
53              (UriManager.uri_of_string 
54                 "cic:/matita/logic/equality/eq_ind.con"))
55     | EqInd_r -> 
56         NCic.Const
57           (reference_of_oxuri 
58              (UriManager.uri_of_string 
59                 "cic:/matita/logic/equality/eq_elim_r.con"))
60     | Refl ->
61         NCic.Const
62           (reference_of_oxuri 
63              (UriManager.uri_of_string 
64                 "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
65   in eqsig:= nsig
66   ;;
67
68 (* let debug c r = prerr_endline r; c *)
69 let debug c _ = c;;
70
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";;
75
76
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
81       | _ -> 1
82     in
83     let vl_len = List.length vl in
84     let rec extract = function
85       | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
86       | Terms.Var j -> 
87            (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term) 
88       | Terms.Node l -> NCic.Appl (List.map extract l)
89     in
90       extract t
91   ;;
92
93
94    let mk_predicate hole_type amount ft p1 vl =
95     let rec aux t p = 
96       match p with
97       | [] -> NCic.Rel 1
98       | n::tl ->
99           match t with
100           | Terms.Leaf _ 
101           | Terms.Var _ -> 
102               let module NCicBlob = NCicBlob.NCicBlob(
103                         struct
104                           let metasenv = [] let subst = [] let context = []
105                         end)
106                           in
107               let module Pp = Pp.Pp(NCicBlob) in  
108                prerr_endline ("term: " ^ Pp.pp_foterm ft);
109                prerr_endline ("path: " ^ String.concat "," 
110                  (List.map string_of_int p1));
111                prerr_endline ("leading to: " ^ Pp.pp_foterm t);
112                assert false
113           | Terms.Node l -> 
114               let l = 
115                 HExtlib.list_mapi
116                   (fun t i -> 
117                     if i = n then aux t tl 
118                     else extract amount (0::vl) t)
119                   l
120               in            
121               NCic.Appl l
122     in
123       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
124     ;;
125
126   let dag = 
127    let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in
128    let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in
129      NCic.Const ref
130   ;;
131
132   (*
133   let eq_setoid = 
134    let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
135    let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in
136      NCic.Const ref
137   ;;
138   *)
139
140   let sym eq = 
141    let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.con" in
142    let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
143      NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
144      NCic.Implicit `Term; NCic.Implicit `Term; eq]; 
145   ;;
146
147   let eq_morphism1 eq = 
148    let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in
149    let u = NReference.reference_of_spec u (NReference.Def 4) in
150      NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
151      NCic.Implicit `Term; NCic.Implicit `Term; eq]; 
152   ;;
153
154   let eq_morphism2 eq = 
155    let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in
156    let u = NReference.reference_of_spec u (NReference.Def 4) in
157      NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
158      NCic.Implicit `Term; eq; NCic.Implicit `Term]; 
159   ;;
160
161   let trans eq p = 
162    let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in
163    let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
164      NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
165      NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq]
166   ;;
167
168   let iff1 eq p = 
169    let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in
170    let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in
171      NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type; 
172                eq; p]; 
173   ;;
174
175 (*
176   let mk_refl = function
177       | NCic.Appl [_; _; x; _] -> 
178    let uri= NUri.uri_of_string "cic:/matita/ng/properties/relations/refl.con" in
179    let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,3)) in
180     NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Term;
181     NCic.Implicit `Term(*x*)]
182       | _ -> assert false
183 *)   
184
185   let mk_refl = function
186     | NCic.Appl [_; ty; l; _]
187       -> NCic.Appl [eq_refl();ty;l]
188     | _ -> assert false
189
190
191    let mk_morphism eq amount ft pl vl =
192     let rec aux t p = 
193       match p with
194       | [] -> eq
195       | n::tl ->
196           prerr_endline (string_of_int n);
197           match t with
198           | Terms.Leaf _ 
199           | Terms.Var _ -> assert false
200           | Terms.Node [] -> assert false
201           | Terms.Node [ Terms.Leaf eqt ; _; l; r ]
202              when (eqP ()) = eqt ->
203                if n=2 then eq_morphism1 (aux l tl)
204                else eq_morphism2 (aux r tl)
205           | Terms.Node (f::l) ->
206              snd (
207               List.fold_left
208                (fun (i,acc) t ->
209                  i+1,
210                        let f = extract amount vl f in
211                   if i = n then
212                    let imp = NCic.Implicit `Term in
213                     NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
214                                [aux t tl])
215                   else
216                     NCicUntrusted.mk_appl acc [extract amount vl t]
217                ) (1,extract amount vl f) l)
218     in aux ft (List.rev pl)
219     ;;
220
221   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
222     let module NCicBlob = 
223        NCicBlob.NCicBlob(
224          struct
225            let metasenv = [] let subst = [] let context = []
226          end)
227      in
228      let  module Pp = Pp.Pp(NCicBlob) 
229      in
230     let module Subst = FoSubst in
231     let position i l = 
232       let rec aux = function
233        | [] -> assert false
234        | (j,_) :: tl when i = j -> 1
235        | _ :: tl -> 1 + aux tl
236       in
237         aux l
238     in
239     let vars_of i l = fst (List.assoc i l) in
240     let ty_of i l = snd (List.assoc i l) in
241     let close_with_lambdas vl t = 
242       List.fold_left 
243        (fun t i -> 
244           NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
245        t vl  
246     in
247     let close_with_forall vl t = 
248       List.fold_left 
249        (fun t i -> 
250           NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
251        t vl  
252     in
253     let get_literal id =
254       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
255       let lit =match lit with 
256           | Terms.Predicate t -> t (* assert false *) 
257           | Terms.Equation (l,r,ty,_) -> 
258               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
259       in
260         lit, vl, proof
261     in
262     let proof_type =
263       let lit,_,_ = get_literal mp in
264       let lit = Subst.apply_subst subst lit in
265         extract 0 [] lit in
266     (* composition of all subst acting on goal *)
267     let res_subst =
268       let rec rsaux ongoal acc = 
269         function
270           | [] -> acc (* is the final subst for refl *)
271           | id::tl when ongoal ->
272             let lit,vl,proof = get_literal id in
273               (match proof with
274                 | Terms.Exact _ -> rsaux ongoal acc tl
275                 | Terms.Step (_, _, _, _, _, s) ->
276                     rsaux ongoal (s@acc) tl)
277           | id::tl -> 
278             (* subst is the the substitution for refl *)
279             rsaux (id=mp) subst tl
280       in 
281       let r = rsaux false [] steps in
282         (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
283            prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
284       r
285     in
286     let rec aux ongoal seen = function
287       | [] -> NCic.Rel 1
288       | id :: tl ->
289           let amount = List.length seen in
290           let lit,vl,proof = get_literal id in
291           if not ongoal && id = mp then
292             let lit = Subst.apply_subst subst lit in 
293             let eq_ty = extract amount [] lit in
294             let refl = 
295               if demod then NCic.Implicit `Term 
296               else mk_refl eq_ty in
297              (* prerr_endline ("Reached m point, id=" ^ (string_of_int id));
298                 (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
299                 aux true ((id,([],lit))::seen) (id::tl))) *)
300               NCicSubstitution.subst 
301                 ~avoid_beta_redexes:true ~no_implicit:false refl
302                 (aux true ((id,([],lit))::seen) (id::tl))
303           else
304           match proof with
305           | Terms.Exact _ when tl=[] ->
306               (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
307               aux ongoal seen tl
308           | Terms.Step _ when tl=[] -> assert false
309           | Terms.Exact ft ->
310               (*
311                prerr_endline ("Exact for " ^ (string_of_int id));
312                NCic.LetIn ("clause_" ^ string_of_int id, 
313                  close_with_forall vl (extract amount vl lit),
314                  close_with_lambdas vl (extract amount vl ft),
315                  aux ongoal 
316                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
317               *)
318                NCicSubstitution.subst 
319                  ~avoid_beta_redexes:true ~no_implicit:false
320                  (close_with_lambdas vl (extract amount vl ft))
321                  (aux ongoal 
322                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
323           | Terms.Step (_, id1, id2, dir, pos, subst) ->
324               let id, id1,(lit,vl,proof) =
325                 if ongoal then
326                   let lit,vl,proof = get_literal id1 in
327                   id1,id,(Subst.apply_subst res_subst lit, 
328                           Subst.filter res_subst vl, proof)
329                 else id,id1,(lit,vl,proof) in
330               (* free variables remaining in the goal should not
331                  be abstracted: we do not want to prove a generalization *)
332               let vl = if ongoal then [] else vl in 
333               let proof_of_id id = 
334                 let vars = List.rev (vars_of id seen) in
335                 let args = List.map (Subst.apply_subst subst) vars in
336                 let args = List.map (extract amount vl) args in
337                 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
338                   if args = [] then rel_for_id                    
339                   else NCic.Appl (rel_for_id::args)
340               in
341               let p_id1 = proof_of_id id1 in
342               let p_id2 = proof_of_id id2 in
343 (*
344               let morphism, l, r =
345                 let p =                 
346                   if (ongoal=true) = (dir=Terms.Left2Right) then
347                     p_id2 
348                   else sym p_id2 in
349                 let id1_ty = ty_of id1 seen in
350                 let id2_ty,l,r = 
351                   match ty_of id2 seen with
352                   | Terms.Node [ _; t; l; r ] -> 
353                       extract amount vl (Subst.apply_subst subst t),
354                       extract amount vl (Subst.apply_subst subst l),
355                       extract amount vl (Subst.apply_subst subst r)
356                   | _ -> assert false
357                 in
358                   (*prerr_endline "mk_predicate :";
359                   if ongoal then prerr_endline "ongoal=true"
360                   else prerr_endline "ongoal=false";
361                   prerr_endline ("id=" ^ string_of_int id);
362                   prerr_endline ("id1=" ^ string_of_int id1);
363                   prerr_endline ("id2=" ^ string_of_int id2);
364                   prerr_endline ("Positions :" ^
365                                    (String.concat ", "
366                                       (List.map string_of_int pos)));*)
367                 mk_morphism
368                   p amount (Subst.apply_subst subst id1_ty) pos vl,
369                 l,r
370               in
371               let rewrite_step = iff1 morphism p_id1
372               in
373 *)
374               let pred, hole_type, l, r = 
375                 let id1_ty = ty_of id1 seen in
376                 let id2_ty,l,r = 
377                   match ty_of id2 seen with
378                   | Terms.Node [ _; t; l; r ] -> 
379                       extract amount vl (Subst.apply_subst subst t),
380                       extract amount vl (Subst.apply_subst subst l),
381                       extract amount vl (Subst.apply_subst subst r)
382                   | _ -> assert false
383                 in
384                   (*
385                   prerr_endline "mk_predicate :";
386                   if ongoal then prerr_endline "ongoal=true"
387                   else prerr_endline "ongoal=false";
388                   prerr_endline ("id=" ^ string_of_int id);
389                   prerr_endline ("id1=" ^ string_of_int id1 
390                                  ^": " ^ Pp.pp_foterm id1_ty);
391                   prerr_endline ("id2=" ^ string_of_int id2
392                                  ^ ": " ^ NCicPp.ppterm [][][] id2_ty);
393                   prerr_endline ("Positions :" ^
394                                    (String.concat ", "
395                                       (List.map string_of_int pos)));*)
396                 mk_predicate 
397                   id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
398                 id2_ty,
399                 l,r
400               in
401               let rewrite_step =
402                 if (ongoal=true) = (dir=Terms.Left2Right) then
403                   NCic.Appl 
404                     [eq_ind_r(); hole_type; r; pred; p_id1; l; p_id2]
405                 else
406                   NCic.Appl 
407                     [ eq_ind(); hole_type; l; pred; p_id1; r; p_id2]
408               in
409               let body = aux ongoal 
410                 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl 
411               in 
412               let occ= NCicUntrusted.count_occurrences [] 1 body in
413                 if occ <= 1 then
414                   NCicSubstitution.subst 
415                     ~avoid_beta_redexes:true ~no_implicit:false
416                     (close_with_lambdas vl rewrite_step) body
417                 else
418                   NCic.LetIn ("clause_" ^ string_of_int id, 
419                     close_with_forall vl (extract amount vl lit),
420                            (* NCic.Implicit `Type, *)
421                     close_with_lambdas vl rewrite_step, body)
422     in 
423       aux false [] steps, proof_type
424   ;;
425