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/.
28 exception CannotSubstInMeta;;
29 exception RelToHiddenHypothesis;;
30 exception ReferenceToVariable;;
31 exception ReferenceToConstant;;
32 exception ReferenceToCurrentProof;;
33 exception ReferenceToInductiveDefinition;;
35 let debug_print = fun _ -> ()
46 | C.Var (uri,exp_named_subst) ->
47 let exp_named_subst' =
48 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
50 C.Var (uri,exp_named_subst')
56 | Some t -> Some (liftaux k t)
61 | C.Implicit _ as t -> t
62 | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
63 | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
64 | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
65 | C.LetIn (n,s,ty,t) ->
66 C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
67 | C.Appl l -> C.Appl (List.map (liftaux k) l)
68 | C.Const (uri,exp_named_subst) ->
69 let exp_named_subst' =
70 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
72 C.Const (uri,exp_named_subst')
73 | C.MutInd (uri,tyno,exp_named_subst) ->
74 let exp_named_subst' =
75 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
77 C.MutInd (uri,tyno,exp_named_subst')
78 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
79 let exp_named_subst' =
80 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
82 C.MutConstruct (uri,tyno,consno,exp_named_subst')
83 | C.MutCase (sp,i,outty,t,pl) ->
84 C.MutCase (sp, i, liftaux k outty, liftaux k t,
85 List.map (liftaux k) pl)
87 let len = List.length fl in
90 (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
95 let len = List.length fl in
98 (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
101 C.CoFix (i, liftedfl)
113 (* substitutes [t1] for [Rel 1] in [t2] *)
114 (* if avoid_beta_redexes is true (default: false) no new beta redexes *)
115 (* are generated. WARNING: the substitution can diverge when t2 is not *)
116 (* well typed and avoid_beta_redexes is true. *)
117 let rec subst ?(avoid_beta_redexes=false) arg =
119 let module C = Cic in
123 n when n = k -> lift (k - 1) arg
127 | C.Var (uri,exp_named_subst) ->
128 let exp_named_subst' =
129 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
131 C.Var (uri,exp_named_subst')
137 | Some t -> Some (substaux k t)
142 | C.Implicit _ as t -> t
143 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
144 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
145 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
146 | C.LetIn (n,s,ty,t) ->
147 C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
149 (* Invariant: no Appl applied to another Appl *)
150 let tl' = List.map (substaux k) tl in
152 match substaux k he with
153 C.Appl l -> C.Appl (l@tl')
155 | C.Lambda (_,_,bo) when avoid_beta_redexes ->
158 | [he] -> subst ~avoid_beta_redexes he bo
159 | he::tl -> C.Appl (subst he bo::tl))
160 | _ as he' -> C.Appl (he'::tl')
162 | C.Appl _ -> assert false
163 | C.Const (uri,exp_named_subst) ->
164 let exp_named_subst' =
165 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
167 C.Const (uri,exp_named_subst')
168 | C.MutInd (uri,typeno,exp_named_subst) ->
169 let exp_named_subst' =
170 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
172 C.MutInd (uri,typeno,exp_named_subst')
173 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
174 let exp_named_subst' =
175 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
177 C.MutConstruct (uri,typeno,consno,exp_named_subst')
178 | C.MutCase (sp,i,outt,t,pl) ->
179 C.MutCase (sp,i,substaux k outt, substaux k t,
180 List.map (substaux k) pl)
182 let len = List.length fl in
185 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
188 C.Fix (i, substitutedfl)
190 let len = List.length fl in
193 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
196 C.CoFix (i, substitutedfl)
201 (*CSC: i controlli di tipo debbono essere svolti da destra a *)
202 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b *)
203 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma *)
204 (*CSC: dovrebbe diventare da sinistra verso destra: *)
205 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *)
206 (*CSC: per la roba che proviene da Coq questo non serve! *)
207 let subst_vars exp_named_subst t =
209 debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
212 let module C = Cic in
215 | C.Var (uri,exp_named_subst') ->
219 (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
225 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
227 C.Constant _ -> raise ReferenceToConstant
228 | C.Variable (_,_,_,params,_) -> params
229 | C.CurrentProof _ -> raise ReferenceToCurrentProof
230 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
234 debug_print (lazy "\n\n---- BEGIN ") ;
235 debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
236 debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
237 debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
239 let exp_named_subst'' =
240 substaux_in_exp_named_subst uri k exp_named_subst' params
243 debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
244 debug_print (lazy "---- END\n\n ") ;
246 C.Var (uri,exp_named_subst'')
253 | Some t -> Some (substaux k t)
258 | C.Implicit _ as t -> t
259 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
260 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
261 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
262 | C.LetIn (n,s,ty,t) ->
263 C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
265 (* Invariant: no Appl applied to another Appl *)
266 let tl' = List.map (substaux k) tl in
268 match substaux k he with
269 C.Appl l -> C.Appl (l@tl')
270 | _ as he' -> C.Appl (he'::tl')
272 | C.Appl _ -> assert false
273 | C.Const (uri,exp_named_subst') ->
275 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
277 C.Constant (_,_,_,params,_) -> params
278 | C.Variable _ -> raise ReferenceToVariable
279 | C.CurrentProof (_,_,_,_,params,_) -> params
280 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
283 let exp_named_subst'' =
284 substaux_in_exp_named_subst uri k exp_named_subst' params
286 C.Const (uri,exp_named_subst'')
287 | C.MutInd (uri,typeno,exp_named_subst') ->
289 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
291 C.Constant _ -> raise ReferenceToConstant
292 | C.Variable _ -> raise ReferenceToVariable
293 | C.CurrentProof _ -> raise ReferenceToCurrentProof
294 | C.InductiveDefinition (_,params,_,_) -> params
297 let exp_named_subst'' =
298 substaux_in_exp_named_subst uri k exp_named_subst' params
300 C.MutInd (uri,typeno,exp_named_subst'')
301 | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
303 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
305 C.Constant _ -> raise ReferenceToConstant
306 | C.Variable _ -> raise ReferenceToVariable
307 | C.CurrentProof _ -> raise ReferenceToCurrentProof
308 | C.InductiveDefinition (_,params,_,_) -> params
311 let exp_named_subst'' =
312 substaux_in_exp_named_subst uri k exp_named_subst' params
314 C.MutConstruct (uri,typeno,consno,exp_named_subst'')
315 | C.MutCase (sp,i,outt,t,pl) ->
316 C.MutCase (sp,i,substaux k outt, substaux k t,
317 List.map (substaux k) pl)
319 let len = List.length fl in
322 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
325 C.Fix (i, substitutedfl)
327 let len = List.length fl in
330 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
333 C.CoFix (i, substitutedfl)
334 and substaux_in_exp_named_subst uri k exp_named_subst' params =
335 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
336 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
337 let rec filter_and_lift =
342 (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
346 (uri,lift (k-1) t)::(filter_and_lift tl)
347 | _::tl -> filter_and_lift tl
350 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
351 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
352 exp_named_subst' then debug_print (lazy "---- OK1") ;
353 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
354 if List.mem uri params then debug_print (lazy "---- OK2") ;
358 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
359 (filter_and_lift exp_named_subst)
361 if exp_named_subst = [] then t
365 (* subst_meta [t_1 ; ... ; t_n] t *)
366 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
367 (* [t_i] is lifted as usual when it crosses an abstraction *)
369 let module C = Cic in
370 if l = [] then t else
371 let rec aux k = function
373 if n <= k then t else
375 match List.nth l (n-k-1) with
376 None -> raise RelToHiddenHypothesis
379 (Failure _) -> assert false
381 | C.Var (uri,exp_named_subst) ->
382 let exp_named_subst' =
383 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
385 C.Var (uri,exp_named_subst')
395 RelToHiddenHypothesis -> None
400 | C.Implicit _ as t -> t
401 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
402 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
403 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
404 | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
405 | C.Appl l -> C.Appl (List.map (aux k) l)
406 | C.Const (uri,exp_named_subst) ->
407 let exp_named_subst' =
408 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
410 C.Const (uri,exp_named_subst')
411 | C.MutInd (uri,typeno,exp_named_subst) ->
412 let exp_named_subst' =
413 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
415 C.MutInd (uri,typeno,exp_named_subst')
416 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
417 let exp_named_subst' =
418 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
420 C.MutConstruct (uri,typeno,consno,exp_named_subst')
421 | C.MutCase (sp,i,outt,t,pl) ->
422 C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
424 let len = List.length fl in
427 (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
430 C.Fix (i, substitutedfl)
432 let len = List.length fl in
435 (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
438 C.CoFix (i, substitutedfl)
443 Deannotate.lift := lift;;