]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/cicSubstitution.ml
...
[helm.git] / helm / software / components / 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 (* $Id$ *)
27
28 exception CannotSubstInMeta;;
29 exception RelToHiddenHypothesis;;
30 exception ReferenceToVariable;;
31 exception ReferenceToConstant;;
32 exception ReferenceToCurrentProof;;
33 exception ReferenceToInductiveDefinition;;
34
35 let debug = false
36 let debug_print =
37  if debug then
38   fun m  -> prerr_endline (Lazy.force m)
39  else
40   fun _  -> ()
41 ;;
42
43 let lift_map k map =
44  let rec liftaux k =
45   let module C = Cic in
46    function
47       C.Rel m ->
48        if m < k then
49         C.Rel m
50        else
51         C.Rel (map k m)
52     | C.Var (uri,exp_named_subst) ->
53        let exp_named_subst' = 
54         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
55        in
56         C.Var (uri,exp_named_subst')
57     | C.Meta (i,l) ->
58        let l' =
59         List.map
60          (function
61              None -> None
62            | Some t -> Some (liftaux k t)
63          ) l
64        in
65         C.Meta(i,l')
66     | C.Sort _ as t -> t
67     | C.Implicit _ as t -> t
68     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
69     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
70     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
71     | C.LetIn (n,s,ty,t) ->
72        C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
73     | C.Appl l -> C.Appl (List.map (liftaux k) l)
74     | C.Const (uri,exp_named_subst) ->
75        let exp_named_subst' = 
76         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
77        in
78         C.Const (uri,exp_named_subst')
79     | C.MutInd (uri,tyno,exp_named_subst) ->
80        let exp_named_subst' = 
81         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
82        in
83         C.MutInd (uri,tyno,exp_named_subst')
84     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
85        let exp_named_subst' = 
86         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
87        in
88         C.MutConstruct (uri,tyno,consno,exp_named_subst')
89     | C.MutCase (sp,i,outty,t,pl) ->
90        C.MutCase (sp, i, liftaux k outty, liftaux k t,
91         List.map (liftaux k) pl)
92     | C.Fix (i, fl) ->
93        let len = List.length fl in
94        let liftedfl =
95         List.map
96          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
97           fl
98        in
99         C.Fix (i, liftedfl)
100     | C.CoFix (i, fl) ->
101        let len = List.length fl in
102        let liftedfl =
103         List.map
104          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
105           fl
106        in
107         C.CoFix (i, liftedfl)
108  in
109  liftaux k
110
111 let lift_from k n =
112    lift_map k (fun _ m -> m + n)
113
114 let lift n t =
115   if n = 0 then
116    t
117   else
118    lift_from 1 n t
119 ;;
120
121 (* subst t1 t2                                                         *)
122 (* substitutes [t1] for [Rel 1] in [t2]                                *)
123 (* if avoid_beta_redexes is true (default: false) no new beta redexes  *)
124 (* are generated. WARNING: the substitution can diverge when t2 is not *)
125 (* well typed and avoid_beta_redexes is true.                          *)
126 let rec subst ?(avoid_beta_redexes=false) arg =
127  let rec substaux k =
128   let module C = Cic in
129    function
130       C.Rel n as t ->
131        (match n with
132            n when n = k -> lift (k - 1) arg
133          | n when n < k -> t
134          | _            -> C.Rel (n - 1)
135        )
136     | C.Var (uri,exp_named_subst) ->
137        let exp_named_subst' =
138         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
139        in
140         C.Var (uri,exp_named_subst')
141     | C.Meta (i, l) -> 
142        let l' =
143         List.map
144          (function
145              None -> None
146            | Some t -> Some (substaux k t)
147          ) l
148        in
149         C.Meta(i,l')
150     | C.Sort _ as t -> t
151     | C.Implicit _ as t -> t
152     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
153     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
154     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
155     | C.LetIn (n,s,ty,t) ->
156        C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
157     | C.Appl (he::tl) ->
158        (* Invariant: no Appl applied to another Appl *)
159        let tl' = List.map (substaux k) tl in
160         begin
161          match substaux k he with
162             C.Appl l -> C.Appl (l@tl')
163             (* Experimental *)
164           | C.Lambda (_,_,bo) when avoid_beta_redexes ->
165              (match tl' with
166                  [] -> assert false
167                | [he] -> subst ~avoid_beta_redexes he bo
168                | he::tl -> C.Appl (subst he bo::tl))
169           | _ as he' -> C.Appl (he'::tl')
170         end
171     | C.Appl _ -> assert false
172     | C.Const (uri,exp_named_subst)  ->
173        let exp_named_subst' =
174         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
175        in
176         C.Const (uri,exp_named_subst')
177     | C.MutInd (uri,typeno,exp_named_subst) ->
178        let exp_named_subst' =
179         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
180        in
181         C.MutInd (uri,typeno,exp_named_subst')
182     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
183        let exp_named_subst' =
184         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
185        in
186         C.MutConstruct (uri,typeno,consno,exp_named_subst')
187     | C.MutCase (sp,i,outt,t,pl) ->
188        C.MutCase (sp,i,substaux k outt, substaux k t,
189         List.map (substaux k) pl)
190     | C.Fix (i,fl) ->
191        let len = List.length fl in
192        let substitutedfl =
193         List.map
194          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
195           fl
196        in
197         C.Fix (i, substitutedfl)
198     | C.CoFix (i,fl) ->
199        let len = List.length fl in
200        let substitutedfl =
201         List.map
202          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
203           fl
204        in
205         C.CoFix (i, substitutedfl)
206  in
207   substaux 1
208 ;;
209
210 (*CSC: i controlli di tipo debbono essere svolti da destra a             *)
211 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b         *)
212 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma     *)
213 (*CSC: dovrebbe diventare da sinistra verso destra:                      *)
214 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H                       *)
215 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
216 let subst_vars exp_named_subst t =
217 (*
218 debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
219 *)
220  let rec substaux k =
221   let module C = Cic in
222    function
223       C.Rel _ as t -> t
224     | C.Var (uri,exp_named_subst') ->
225        (try
226          let (_,arg) =
227           List.find
228            (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
229          in
230           lift (k -1) arg
231         with
232          Not_found ->
233           let params =
234            let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
235            (match obj with
236                C.Constant _ -> raise ReferenceToConstant
237              | C.Variable (_,_,_,params,_) -> params
238              | C.CurrentProof _ -> raise ReferenceToCurrentProof
239              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
240            )
241           in
242            let exp_named_subst'' =
243             substaux_in_exp_named_subst uri k exp_named_subst' params
244            in
245             C.Var (uri,exp_named_subst'')
246        )
247     | C.Meta (i, l) -> 
248        let l' =
249         List.map
250          (function
251              None -> None
252            | Some t -> Some (substaux k t)
253          ) l
254        in
255         C.Meta(i,l')
256     | C.Sort _ as t -> t
257     | C.Implicit _ as t -> t
258     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
259     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
260     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
261     | C.LetIn (n,s,ty,t) ->
262        C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
263     | C.Appl (he::tl) ->
264        (* Invariant: no Appl applied to another Appl *)
265        let tl' = List.map (substaux k) tl in
266         begin
267          match substaux k he with
268             C.Appl l -> C.Appl (l@tl')
269           | _ as he' -> C.Appl (he'::tl')
270         end
271     | C.Appl _ -> assert false
272     | C.Const (uri,exp_named_subst')  ->
273        let params =
274         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
275         (match obj with
276             C.Constant (_,_,_,params,_) -> params
277           | C.Variable _ -> raise ReferenceToVariable
278           | C.CurrentProof (_,_,_,_,params,_) -> params
279           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
280         )
281        in
282         let exp_named_subst'' =
283          substaux_in_exp_named_subst uri k exp_named_subst' params
284         in
285          C.Const (uri,exp_named_subst'')
286     | C.MutInd (uri,typeno,exp_named_subst') ->
287        let params =
288         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
289         (match obj with
290             C.Constant _ -> raise ReferenceToConstant
291           | C.Variable _ -> raise ReferenceToVariable
292           | C.CurrentProof _ -> raise ReferenceToCurrentProof
293           | C.InductiveDefinition (_,params,_,_) -> params
294         )
295        in
296         let exp_named_subst'' =
297          substaux_in_exp_named_subst uri k exp_named_subst' params
298         in
299          C.MutInd (uri,typeno,exp_named_subst'')
300     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
301        let params =
302         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
303         (match obj with
304             C.Constant _ -> raise ReferenceToConstant
305           | C.Variable _ -> raise ReferenceToVariable
306           | C.CurrentProof _ -> raise ReferenceToCurrentProof
307           | C.InductiveDefinition (_,params,_,_) -> params
308         )
309        in
310         let exp_named_subst'' =
311          substaux_in_exp_named_subst uri k exp_named_subst' params
312         in
313 if (List.map fst exp_named_subst'' <> List.map fst (List.filter (fun (uri,_) -> List.mem uri params) exp_named_subst) @ List.map fst exp_named_subst') then (
314 debug_print (lazy "\n\n---- BEGIN ") ;
315 debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
316 debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
317 debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
318 debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
319 debug_print (lazy "---- END\n\n ") ;
320 );
321          C.MutConstruct (uri,typeno,consno,exp_named_subst'')
322     | C.MutCase (sp,i,outt,t,pl) ->
323        C.MutCase (sp,i,substaux k outt, substaux k t,
324         List.map (substaux k) pl)
325     | C.Fix (i,fl) ->
326        let len = List.length fl in
327        let substitutedfl =
328         List.map
329          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
330           fl
331        in
332         C.Fix (i, substitutedfl)
333     | C.CoFix (i,fl) ->
334        let len = List.length fl in
335        let substitutedfl =
336         List.map
337          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
338           fl
339        in
340         C.CoFix (i, substitutedfl)
341  and substaux_in_exp_named_subst uri k exp_named_subst' params =
342   let rec filter_and_lift =
343    function
344       [] -> []
345     | (uri,t)::tl when
346         List.for_all
347          (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
348         &&
349          List.mem uri params
350        ->
351         (uri,lift (k-1) t)::(filter_and_lift tl)
352     | _::tl -> filter_and_lift tl
353   in
354    let res =
355     List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
356      (filter_and_lift exp_named_subst)
357    in
358     let rec reorder =
359      function
360         [] -> []
361       | uri::tl ->
362          let he =
363           try
364            [uri,List.assoc uri res]
365           with
366            Not_found -> []
367          in
368           he@reorder tl
369     in
370      reorder params
371  in
372   if exp_named_subst = [] then t
373   else substaux 1 t
374 ;;
375
376 (* subst_meta [t_1 ; ... ; t_n] t                                *)
377 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
378 (* [t_i] is lifted as usual when it crosses an abstraction      *)
379 let subst_meta l t = 
380  let module C = Cic in
381   if l = [] then t else 
382    let rec aux k = function
383       C.Rel n as t -> 
384         if n <= k then t else 
385          (try
386            match List.nth l (n-k-1) with
387               None -> raise RelToHiddenHypothesis
388             | Some t -> lift k t
389           with
390            (Failure _) -> assert false
391          )
392     | C.Var (uri,exp_named_subst) ->
393        let exp_named_subst' =
394         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
395        in
396         C.Var (uri,exp_named_subst')
397     | C.Meta (i,l) ->
398        let l' =
399         List.map
400          (function
401              None -> None
402            | Some t ->
403               try
404                Some (aux k t)
405               with
406                RelToHiddenHypothesis -> None
407          ) l
408        in
409         C.Meta(i,l')
410     | C.Sort _ as t -> t
411     | C.Implicit _ as t -> t
412     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
413     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
414     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
415     | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
416     | C.Appl l -> C.Appl (List.map (aux k) l)
417     | C.Const (uri,exp_named_subst) ->
418        let exp_named_subst' =
419         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
420        in
421         C.Const (uri,exp_named_subst')
422     | C.MutInd (uri,typeno,exp_named_subst) ->
423        let exp_named_subst' =
424         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
425        in
426         C.MutInd (uri,typeno,exp_named_subst')
427     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
428        let exp_named_subst' =
429         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
430        in
431         C.MutConstruct (uri,typeno,consno,exp_named_subst')
432     | C.MutCase (sp,i,outt,t,pl) ->
433        C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
434     | C.Fix (i,fl) ->
435        let len = List.length fl in
436        let substitutedfl =
437         List.map
438          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
439           fl
440        in
441         C.Fix (i, substitutedfl)
442     | C.CoFix (i,fl) ->
443        let len = List.length fl in
444        let substitutedfl =
445         List.map
446          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
447           fl
448        in
449         C.CoFix (i, substitutedfl)
450  in
451   aux 0 t          
452 ;;
453
454 Deannotate.lift := lift;;