]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_proof_checking/cicSubstitution.ml
snapshot
[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 exception CannotSubstInMeta;;
27 exception RelToHiddenHypothesis;;
28 exception ReferenceToVariable;;
29 exception ReferenceToConstant;;
30 exception ReferenceToCurrentProof;;
31 exception ReferenceToInductiveDefinition;;
32
33 let lift n =
34  let rec liftaux k =
35   let module C = Cic in
36    function
37       C.Rel m ->
38        if m < k then
39         C.Rel m
40        else
41         C.Rel (m + n)
42     | C.Var (uri,exp_named_subst) ->
43        let exp_named_subst' = 
44         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
45        in
46         C.Var (uri,exp_named_subst')
47     | C.Meta (i,l) ->
48        let l' =
49         List.map
50          (function
51              None -> None
52            | Some t -> Some (liftaux k t)
53          ) l
54        in
55         C.Meta(i,l')
56     | C.Sort _ as t -> t
57     | C.Implicit _ as t -> t
58     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
59     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
60     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
61     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
62     | C.Appl l -> C.Appl (List.map (liftaux k) l)
63     | C.Const (uri,exp_named_subst) ->
64        let exp_named_subst' = 
65         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
66        in
67         C.Const (uri,exp_named_subst')
68     | C.MutInd (uri,tyno,exp_named_subst) ->
69        let exp_named_subst' = 
70         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
71        in
72         C.MutInd (uri,tyno,exp_named_subst')
73     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
74        let exp_named_subst' = 
75         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
76        in
77         C.MutConstruct (uri,tyno,consno,exp_named_subst')
78     | C.MutCase (sp,i,outty,t,pl) ->
79        C.MutCase (sp, i, liftaux k outty, liftaux k t,
80         List.map (liftaux k) pl)
81     | C.Fix (i, fl) ->
82        let len = List.length fl in
83        let liftedfl =
84         List.map
85          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
86           fl
87        in
88         C.Fix (i, liftedfl)
89     | C.CoFix (i, fl) ->
90        let len = List.length fl in
91        let liftedfl =
92         List.map
93          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
94           fl
95        in
96         C.CoFix (i, liftedfl)
97  in
98   if n = 0 then
99    (function t -> t)
100   else
101    liftaux 1
102 ;;
103
104 let subst arg =
105  let rec substaux k =
106   let module C = Cic in
107    function
108       C.Rel n as t ->
109        (match n with
110            n when n = k -> lift (k - 1) arg
111          | n when n < k -> t
112          | _            -> C.Rel (n - 1)
113        )
114     | C.Var (uri,exp_named_subst) ->
115        let exp_named_subst' =
116         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
117        in
118         C.Var (uri,exp_named_subst')
119     | C.Meta (i, l) as t -> 
120        let l' =
121         List.map
122          (function
123              None -> None
124            | Some t -> Some (substaux k t)
125          ) l
126        in
127         C.Meta(i,l')
128     | C.Sort _ as t -> t
129     | C.Implicit _ as t -> t
130     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
131     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
132     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
133     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
134     | C.Appl (he::tl) ->
135        (* Invariant: no Appl applied to another Appl *)
136        let tl' = List.map (substaux k) tl in
137         begin
138          match substaux k he with
139             C.Appl l -> C.Appl (l@tl')
140           | _ as he' -> C.Appl (he'::tl')
141         end
142     | C.Appl _ -> assert false
143     | C.Const (uri,exp_named_subst)  ->
144        let exp_named_subst' =
145         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
146        in
147         C.Const (uri,exp_named_subst')
148     | C.MutInd (uri,typeno,exp_named_subst) ->
149        let exp_named_subst' =
150         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
151        in
152         C.MutInd (uri,typeno,exp_named_subst')
153     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
154        let exp_named_subst' =
155         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
156        in
157         C.MutConstruct (uri,typeno,consno,exp_named_subst')
158     | C.MutCase (sp,i,outt,t,pl) ->
159        C.MutCase (sp,i,substaux k outt, substaux k t,
160         List.map (substaux k) pl)
161     | C.Fix (i,fl) ->
162        let len = List.length fl in
163        let substitutedfl =
164         List.map
165          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
166           fl
167        in
168         C.Fix (i, substitutedfl)
169     | C.CoFix (i,fl) ->
170        let len = List.length fl in
171        let substitutedfl =
172         List.map
173          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
174           fl
175        in
176         C.CoFix (i, substitutedfl)
177  in
178   substaux 1
179 ;;
180
181 (*CSC: i controlli di tipo debbono essere svolti da destra a             *)
182 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b         *)
183 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma     *)
184 (*CSC: dovrebbe diventare da sinistra verso destra:                      *)
185 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H                       *)
186 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
187 let subst_vars exp_named_subst =
188 (*
189 prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
190 *)
191  let rec substaux k =
192   let module C = Cic in
193    function
194       C.Rel _ as t -> t
195     | C.Var (uri,exp_named_subst') ->
196        (try
197          let (_,arg) =
198           List.find
199            (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
200          in
201           lift (k -1) arg
202         with
203          Not_found ->
204           let params =
205            (match CicEnvironment.get_cooked_obj ~trust:true uri with
206                C.Constant _ -> raise ReferenceToConstant
207              | C.Variable (_,_,_,params) -> params
208              | C.CurrentProof _ -> raise ReferenceToCurrentProof
209              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
210            )
211           in
212 (*
213 prerr_endline "\n\n---- BEGIN " ;
214 prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
215 prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
216 prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
217 *)
218            let exp_named_subst'' =
219             substaux_in_exp_named_subst uri k exp_named_subst' params
220            in
221 (*
222 prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
223 prerr_endline "---- END\n\n " ;
224 *)
225             C.Var (uri,exp_named_subst'')
226        )
227     | C.Meta (i, l) as t -> 
228        let l' =
229         List.map
230          (function
231              None -> None
232            | Some t -> Some (substaux k t)
233          ) l
234        in
235         C.Meta(i,l')
236     | C.Sort _ as t -> t
237     | C.Implicit _ as t -> t
238     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
239     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
240     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
241     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
242     | C.Appl (he::tl) ->
243        (* Invariant: no Appl applied to another Appl *)
244        let tl' = List.map (substaux k) tl in
245         begin
246          match substaux k he with
247             C.Appl l -> C.Appl (l@tl')
248           | _ as he' -> C.Appl (he'::tl')
249         end
250     | C.Appl _ -> assert false
251     | C.Const (uri,exp_named_subst')  ->
252        let params =
253         (match CicEnvironment.get_cooked_obj ~trust:true uri with
254             C.Constant (_,_,_,params) -> params
255           | C.Variable _ -> raise ReferenceToVariable
256           | C.CurrentProof (_,_,_,_,params) -> params
257           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
258         )
259        in
260         let exp_named_subst'' =
261          substaux_in_exp_named_subst uri k exp_named_subst' params
262         in
263          C.Const (uri,exp_named_subst'')
264     | C.MutInd (uri,typeno,exp_named_subst') ->
265        let params =
266         (match CicEnvironment.get_cooked_obj ~trust:true uri with
267             C.Constant _ -> raise ReferenceToConstant
268           | C.Variable _ -> raise ReferenceToVariable
269           | C.CurrentProof _ -> raise ReferenceToCurrentProof
270           | C.InductiveDefinition (_,params,_) -> params
271         )
272        in
273         let exp_named_subst'' =
274          substaux_in_exp_named_subst uri k exp_named_subst' params
275         in
276          C.MutInd (uri,typeno,exp_named_subst'')
277     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
278        let params =
279         (match CicEnvironment.get_cooked_obj ~trust:true uri with
280             C.Constant _ -> raise ReferenceToConstant
281           | C.Variable _ -> raise ReferenceToVariable
282           | C.CurrentProof _ -> raise ReferenceToCurrentProof
283           | C.InductiveDefinition (_,params,_) -> params
284         )
285        in
286         let exp_named_subst'' =
287          substaux_in_exp_named_subst uri k exp_named_subst' params
288         in
289          C.MutConstruct (uri,typeno,consno,exp_named_subst'')
290     | C.MutCase (sp,i,outt,t,pl) ->
291        C.MutCase (sp,i,substaux k outt, substaux k t,
292         List.map (substaux k) pl)
293     | C.Fix (i,fl) ->
294        let len = List.length fl in
295        let substitutedfl =
296         List.map
297          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
298           fl
299        in
300         C.Fix (i, substitutedfl)
301     | C.CoFix (i,fl) ->
302        let len = List.length fl in
303        let substitutedfl =
304         List.map
305          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
306           fl
307        in
308         C.CoFix (i, substitutedfl)
309  and substaux_in_exp_named_subst uri k exp_named_subst' params =
310 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
311 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
312   let rec filter_and_lift =
313    function
314       [] -> []
315     | (uri,t)::tl when
316         List.for_all
317          (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
318         &&
319          List.mem uri params
320        ->
321         (uri,lift (k-1) t)::(filter_and_lift tl)
322     | _::tl -> filter_and_lift tl
323 (*
324     | (uri,_)::tl ->
325 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
326 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
327 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
328 if List.mem uri params then prerr_endline "---- OK2" ;
329         filter_and_lift tl
330 *)
331   in
332    List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
333     (filter_and_lift exp_named_subst)
334  in
335   substaux 1
336 ;;
337
338 (* lift_meta [t_1 ; ... ; t_n] t                                *)
339 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
340 (* [t_i] is lifted as usual when it crosses an abstraction      *)
341 let lift_meta l t = 
342  let module C = Cic in
343   if l = [] then t else 
344    let rec aux k = function
345       C.Rel n as t -> 
346         if n <= k then t else 
347          (try
348            match List.nth l (n-k-1) with
349               None -> raise RelToHiddenHypothesis
350             | Some t -> lift k t
351           with
352            (Failure _) -> assert false
353          )
354     | C.Var (uri,exp_named_subst) ->
355        let exp_named_subst' =
356         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
357        in
358         C.Var (uri,exp_named_subst')
359     | C.Meta (i,l) ->
360        let l' =
361         List.map
362          (function
363              None -> None
364            | Some t ->
365               try
366                Some (aux k t)
367               with
368                RelToHiddenHypothesis -> None
369          ) l
370        in
371         C.Meta(i,l')
372     | C.Sort _ as t -> t
373     | C.Implicit _ as t -> t
374     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
375     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
376     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
377     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
378     | C.Appl l -> C.Appl (List.map (aux k) l)
379     | C.Const (uri,exp_named_subst) ->
380        let exp_named_subst' =
381         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
382        in
383         C.Const (uri,exp_named_subst')
384     | C.MutInd (uri,typeno,exp_named_subst) ->
385        let exp_named_subst' =
386         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
387        in
388         C.MutInd (uri,typeno,exp_named_subst')
389     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
390        let exp_named_subst' =
391         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
392        in
393         C.MutConstruct (uri,typeno,consno,exp_named_subst')
394     | C.MutCase (sp,i,outt,t,pl) ->
395        C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
396     | C.Fix (i,fl) ->
397        let len = List.length fl in
398        let substitutedfl =
399         List.map
400          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
401           fl
402        in
403         C.Fix (i, substitutedfl)
404     | C.CoFix (i,fl) ->
405        let len = List.length fl in
406        let substitutedfl =
407         List.map
408          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
409           fl
410        in
411         C.CoFix (i, substitutedfl)
412  in
413   aux 0 t          
414 ;;