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