]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_paramodulation/nCicProof.ml
short names
[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 let reference_of_oxuri = ref (fun _ -> assert false);;
15 let set_reference_of_oxuri f = reference_of_oxuri := f;;
16
17
18   let eqP () = 
19     let r = 
20       !reference_of_oxuri 
21        (UriManager.uri_of_string 
22          "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
23     in
24     NCic.Const r
25   ;;
26
27   let eq_ind () = 
28     let r = 
29       !reference_of_oxuri 
30        (UriManager.uri_of_string 
31          "cic:/matita/logic/equality/eq_ind.con")
32     in
33     NCic.Const r
34   ;;
35
36   let eq_ind_r () = 
37     let r = 
38       !reference_of_oxuri 
39        (UriManager.uri_of_string 
40          "cic:/matita/logic/equality/eq_elim_r.con")
41     in
42     NCic.Const r
43   ;;
44
45   let eq_refl () = 
46     let r = 
47       !reference_of_oxuri 
48        (UriManager.uri_of_string 
49          "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
50     in
51     NCic.Const r
52   ;;
53
54   let extract lift vl t =
55     let rec pos i = function 
56       | [] -> raise Not_found 
57       | j :: tl when j <> i -> 1+ pos i tl
58       | _ -> 1
59     in
60     let vl_len = List.length vl in
61     let rec extract = function
62       | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
63       | Terms.Var j -> 
64            (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term) 
65       | Terms.Node l -> NCic.Appl (List.map extract l)
66     in
67       extract t
68   ;;
69
70    let mk_predicate hole_type amount ft p1 vl =
71     let rec aux t p = 
72       match p with
73       | [] -> NCic.Rel 1
74       | n::tl ->
75           match t with
76           | Terms.Leaf _ 
77           | Terms.Var _ -> 
78               let module Pp = 
79                 Pp.Pp(NCicBlob.NCicBlob(
80                         struct
81                           let metasenv = [] let subst = [] let context = []
82                         end))
83               in  
84                prerr_endline ("term: " ^ Pp.pp_foterm ft);
85                prerr_endline ("path: " ^ String.concat "," 
86                  (List.map string_of_int p1));
87                prerr_endline ("leading to: " ^ Pp.pp_foterm t);
88                assert false
89           | Terms.Node l -> 
90               let l = 
91                 HExtlib.list_mapi
92                   (fun t i -> 
93                     if i = n then aux t tl 
94                     else extract amount (0::vl) t)
95                   l
96               in            
97               NCic.Appl l
98     in
99       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
100     ;;
101
102   let mk_proof (bag : NCic.term Terms.bag) mp steps =
103     let module Subst = FoSubst in
104     let position i l = 
105       let rec aux = function
106        | [] -> assert false
107        | (j,_) :: tl when i = j -> 1
108        | _ :: tl -> 1 + aux tl
109       in
110         aux l
111     in
112     let vars_of i l = fst (List.assoc i l) in
113     let ty_of i l = snd (List.assoc i l) in
114     let close_with_lambdas vl t = 
115       List.fold_left 
116        (fun t i -> 
117           NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
118        t vl  
119     in
120     let close_with_forall vl t = 
121       List.fold_left 
122        (fun t i -> 
123           NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
124        t vl  
125     in
126     let get_literal id =
127       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
128       let lit =match lit with 
129           | Terms.Predicate t -> assert false 
130           | Terms.Equation (l,r,ty,_) -> 
131               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
132       in
133         lit, vl, proof
134     in
135     let rec aux ongoal seen = function
136       | [] -> NCic.Rel 1
137       | id :: tl ->
138           let amount = List.length seen in
139           let lit,vl,proof = get_literal id in
140           if not ongoal && id = mp then
141             ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
142              NCic.LetIn ("clause_" ^ string_of_int id, 
143                 extract amount [] lit, 
144                 (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
145                 aux true ((id,([],lit))::seen) (id::tl)))
146           else
147           match proof with
148           | Terms.Exact _ when tl=[] ->
149               (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
150               aux ongoal seen tl
151           | Terms.Step _ when tl=[] -> assert false
152           | Terms.Exact ft ->
153               (* prerr_endline ("Exact for " ^ (string_of_int id));*)
154                NCic.LetIn ("clause_" ^ string_of_int id, 
155                  close_with_forall vl (extract amount vl lit),
156                  close_with_lambdas vl (extract amount vl ft),
157                  aux ongoal 
158                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
159           | Terms.Step (_, id1, id2, dir, pos, subst) ->
160               let id, id1,(lit,vl,proof) =
161                 if ongoal then id1,id,get_literal id1
162                 else id,id1,(lit,vl,proof)
163               in
164               let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
165               let proof_of_id id = 
166                 let vars = List.rev (vars_of id seen) in
167                 let args = List.map (Subst.apply_subst subst) vars in
168                 let args = List.map (extract amount vl) args in
169                 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
170                   if args = [] then rel_for_id              
171                   else NCic.Appl (rel_for_id::args)
172               in
173               let p_id1 = proof_of_id id1 in
174               let p_id2 = proof_of_id id2 in
175               let pred, hole_type, l, r = 
176                 let id1_ty = ty_of id1 seen in
177                 let id2_ty,l,r = 
178                   match ty_of id2 seen with
179                   | Terms.Node [ _; t; l; r ] -> 
180                       extract amount vl (Subst.apply_subst subst t),
181                       extract amount vl (Subst.apply_subst subst l),
182                       extract amount vl (Subst.apply_subst subst r)
183                   | _ -> assert false
184                 in
185                   (*prerr_endline "mk_predicate :";
186                   if ongoal then prerr_endline "ongoal=true"
187                   else prerr_endline "ongoal=false";
188                   prerr_endline ("id=" ^ string_of_int id);
189                   prerr_endline ("id1=" ^ string_of_int id1);
190                   prerr_endline ("id2=" ^ string_of_int id2);
191                   prerr_endline ("Positions :" ^
192                                    (String.concat ", "
193                                       (List.map string_of_int pos)));*)
194                 mk_predicate 
195                   id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
196                 id2_ty,
197                 l,r
198               in
199               let l, r, eq_ind = 
200                 if (ongoal=true) = (dir=Terms.Left2Right) then
201                   r,l,eq_ind_r ()
202                 else
203                   l,r,eq_ind ()
204               in
205                NCic.LetIn ("clause_" ^ string_of_int id, 
206                  close_with_forall vl (extract amount vl lit),
207                            (* NCic.Implicit `Type, *)
208                  close_with_lambdas vl 
209                    (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
210                  aux ongoal 
211                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
212     in 
213       aux false [] steps
214   ;;
215