1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 exception CannotSubstInMeta;;
27 exception RelToHiddenHypothesis;;
28 exception ReferenceToVariable;;
29 exception ReferenceToConstant;;
30 exception ReferenceToCurrentProof;;
31 exception ReferenceToInductiveDefinition;;
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
46 C.Var (uri,exp_named_subst')
52 | Some t -> Some (liftaux k 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
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
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
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)
82 let len = List.length fl in
85 (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
90 let len = List.length fl in
93 (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
107 (* delifts a term t of n levels strating from k, that is changes (Rel m)
108 * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
110 let delift_from k n =
112 let module C = Cic in
117 else if m < k + n then
118 (failwith "delifting this term whould capture free variables")
121 | C.Var (uri,exp_named_subst) ->
122 let exp_named_subst' =
123 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
125 C.Var (uri,exp_named_subst')
131 | Some t -> Some (liftaux k t)
136 | C.Implicit _ as t -> t
137 | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
138 | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
139 | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
140 | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
141 | C.Appl l -> C.Appl (List.map (liftaux k) l)
142 | C.Const (uri,exp_named_subst) ->
143 let exp_named_subst' =
144 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
146 C.Const (uri,exp_named_subst')
147 | C.MutInd (uri,tyno,exp_named_subst) ->
148 let exp_named_subst' =
149 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
151 C.MutInd (uri,tyno,exp_named_subst')
152 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
153 let exp_named_subst' =
154 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
156 C.MutConstruct (uri,tyno,consno,exp_named_subst')
157 | C.MutCase (sp,i,outty,t,pl) ->
158 C.MutCase (sp, i, liftaux k outty, liftaux k t,
159 List.map (liftaux k) pl)
161 let len = List.length fl in
164 (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
169 let len = List.length fl in
172 (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
175 C.CoFix (i, liftedfl)
184 let module C = Cic in
188 n when n = k -> lift (k - 1) arg
192 | C.Var (uri,exp_named_subst) ->
193 let exp_named_subst' =
194 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
196 C.Var (uri,exp_named_subst')
197 | C.Meta (i, l) as t ->
202 | Some t -> Some (substaux k t)
207 | C.Implicit _ as t -> t
208 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
209 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
210 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
211 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
213 (* Invariant: no Appl applied to another Appl *)
214 let tl' = List.map (substaux k) tl in
216 match substaux k he with
217 C.Appl l -> C.Appl (l@tl')
218 | _ as he' -> C.Appl (he'::tl')
220 | C.Appl _ -> assert false
221 | C.Const (uri,exp_named_subst) ->
222 let exp_named_subst' =
223 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
225 C.Const (uri,exp_named_subst')
226 | C.MutInd (uri,typeno,exp_named_subst) ->
227 let exp_named_subst' =
228 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
230 C.MutInd (uri,typeno,exp_named_subst')
231 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
232 let exp_named_subst' =
233 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
235 C.MutConstruct (uri,typeno,consno,exp_named_subst')
236 | C.MutCase (sp,i,outt,t,pl) ->
237 C.MutCase (sp,i,substaux k outt, substaux k t,
238 List.map (substaux k) pl)
240 let len = List.length fl in
243 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
246 C.Fix (i, substitutedfl)
248 let len = List.length fl in
251 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
254 C.CoFix (i, substitutedfl)
259 (*CSC: i controlli di tipo debbono essere svolti da destra a *)
260 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b *)
261 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma *)
262 (*CSC: dovrebbe diventare da sinistra verso destra: *)
263 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *)
264 (*CSC: per la roba che proviene da Coq questo non serve! *)
265 let subst_vars exp_named_subst =
267 prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
270 let module C = Cic in
273 | C.Var (uri,exp_named_subst') ->
277 (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
283 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
285 C.Constant _ -> raise ReferenceToConstant
286 | C.Variable (_,_,_,params,_) -> params
287 | C.CurrentProof _ -> raise ReferenceToCurrentProof
288 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
292 prerr_endline "\n\n---- BEGIN " ;
293 prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
294 prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ;
295 prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ;
297 let exp_named_subst'' =
298 substaux_in_exp_named_subst uri k exp_named_subst' params
301 prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ;
302 prerr_endline "---- END\n\n " ;
304 C.Var (uri,exp_named_subst'')
306 | C.Meta (i, l) as t ->
311 | Some t -> Some (substaux k t)
316 | C.Implicit _ as t -> t
317 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
318 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
319 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
320 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
322 (* Invariant: no Appl applied to another Appl *)
323 let tl' = List.map (substaux k) tl in
325 match substaux k he with
326 C.Appl l -> C.Appl (l@tl')
327 | _ as he' -> C.Appl (he'::tl')
329 | C.Appl _ -> assert false
330 | C.Const (uri,exp_named_subst') ->
332 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
334 C.Constant (_,_,_,params,_) -> params
335 | C.Variable _ -> raise ReferenceToVariable
336 | C.CurrentProof (_,_,_,_,params,_) -> params
337 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
340 let exp_named_subst'' =
341 substaux_in_exp_named_subst uri k exp_named_subst' params
343 C.Const (uri,exp_named_subst'')
344 | C.MutInd (uri,typeno,exp_named_subst') ->
346 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
348 C.Constant _ -> raise ReferenceToConstant
349 | C.Variable _ -> raise ReferenceToVariable
350 | C.CurrentProof _ -> raise ReferenceToCurrentProof
351 | C.InductiveDefinition (_,params,_,_) -> params
354 let exp_named_subst'' =
355 substaux_in_exp_named_subst uri k exp_named_subst' params
357 C.MutInd (uri,typeno,exp_named_subst'')
358 | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
360 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
362 C.Constant _ -> raise ReferenceToConstant
363 | C.Variable _ -> raise ReferenceToVariable
364 | C.CurrentProof _ -> raise ReferenceToCurrentProof
365 | C.InductiveDefinition (_,params,_,_) -> params
368 let exp_named_subst'' =
369 substaux_in_exp_named_subst uri k exp_named_subst' params
371 C.MutConstruct (uri,typeno,consno,exp_named_subst'')
372 | C.MutCase (sp,i,outt,t,pl) ->
373 C.MutCase (sp,i,substaux k outt, substaux k t,
374 List.map (substaux k) pl)
376 let len = List.length fl in
379 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
382 C.Fix (i, substitutedfl)
384 let len = List.length fl in
387 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
390 C.CoFix (i, substitutedfl)
391 and substaux_in_exp_named_subst uri k exp_named_subst' params =
392 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
393 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
394 let rec filter_and_lift =
399 (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
403 (uri,lift (k-1) t)::(filter_and_lift tl)
404 | _::tl -> filter_and_lift tl
407 prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
408 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
409 prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
410 if List.mem uri params then prerr_endline "---- OK2" ;
414 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
415 (filter_and_lift exp_named_subst)
420 (* lift_meta [t_1 ; ... ; t_n] t *)
421 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
422 (* [t_i] is lifted as usual when it crosses an abstraction *)
424 let module C = Cic in
425 if l = [] then t else
426 let rec aux k = function
428 if n <= k then t else
430 match List.nth l (n-k-1) with
431 None -> raise RelToHiddenHypothesis
434 (Failure _) -> assert false
436 | C.Var (uri,exp_named_subst) ->
437 let exp_named_subst' =
438 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
440 C.Var (uri,exp_named_subst')
450 RelToHiddenHypothesis -> None
455 | C.Implicit _ as t -> t
456 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
457 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
458 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
459 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
460 | C.Appl l -> C.Appl (List.map (aux k) l)
461 | C.Const (uri,exp_named_subst) ->
462 let exp_named_subst' =
463 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
465 C.Const (uri,exp_named_subst')
466 | C.MutInd (uri,typeno,exp_named_subst) ->
467 let exp_named_subst' =
468 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
470 C.MutInd (uri,typeno,exp_named_subst')
471 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
472 let exp_named_subst' =
473 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
475 C.MutConstruct (uri,typeno,consno,exp_named_subst')
476 | C.MutCase (sp,i,outt,t,pl) ->
477 C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
479 let len = List.length fl in
482 (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
485 C.Fix (i, substitutedfl)
487 let len = List.length fl in
490 (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
493 C.CoFix (i, substitutedfl)