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;;
33 let debug_print = fun _ -> ()
44 | C.Var (uri,exp_named_subst) ->
45 let exp_named_subst' =
46 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
48 C.Var (uri,exp_named_subst')
54 | Some t -> Some (liftaux k t)
59 | C.Implicit _ as t -> t
60 | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
61 | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
62 | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
63 | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
64 | C.Appl l -> C.Appl (List.map (liftaux k) l)
65 | C.Const (uri,exp_named_subst) ->
66 let exp_named_subst' =
67 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
69 C.Const (uri,exp_named_subst')
70 | C.MutInd (uri,tyno,exp_named_subst) ->
71 let exp_named_subst' =
72 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
74 C.MutInd (uri,tyno,exp_named_subst')
75 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
76 let exp_named_subst' =
77 List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
79 C.MutConstruct (uri,tyno,consno,exp_named_subst')
80 | C.MutCase (sp,i,outty,t,pl) ->
81 C.MutCase (sp, i, liftaux k outty, liftaux k t,
82 List.map (liftaux k) pl)
84 let len = List.length fl in
87 (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
92 let len = List.length fl in
95 (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
111 let module C = Cic in
115 n when n = k -> lift (k - 1) arg
119 | C.Var (uri,exp_named_subst) ->
120 let exp_named_subst' =
121 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
123 C.Var (uri,exp_named_subst')
129 | Some t -> Some (substaux k t)
134 | C.Implicit _ as t -> t
135 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
136 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
137 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
138 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
140 (* Invariant: no Appl applied to another Appl *)
141 let tl' = List.map (substaux k) tl in
143 match substaux k he with
144 C.Appl l -> C.Appl (l@tl')
145 | _ as he' -> C.Appl (he'::tl')
147 | C.Appl _ -> assert false
148 | C.Const (uri,exp_named_subst) ->
149 let exp_named_subst' =
150 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
152 C.Const (uri,exp_named_subst')
153 | C.MutInd (uri,typeno,exp_named_subst) ->
154 let exp_named_subst' =
155 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
157 C.MutInd (uri,typeno,exp_named_subst')
158 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
159 let exp_named_subst' =
160 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
162 C.MutConstruct (uri,typeno,consno,exp_named_subst')
163 | C.MutCase (sp,i,outt,t,pl) ->
164 C.MutCase (sp,i,substaux k outt, substaux k t,
165 List.map (substaux k) pl)
167 let len = List.length fl in
170 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
173 C.Fix (i, substitutedfl)
175 let len = List.length fl in
178 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
181 C.CoFix (i, substitutedfl)
186 (*CSC: i controlli di tipo debbono essere svolti da destra a *)
187 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b *)
188 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma *)
189 (*CSC: dovrebbe diventare da sinistra verso destra: *)
190 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *)
191 (*CSC: per la roba che proviene da Coq questo non serve! *)
192 let subst_vars exp_named_subst =
194 debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
197 let module C = Cic in
200 | C.Var (uri,exp_named_subst') ->
204 (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
210 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
212 C.Constant _ -> raise ReferenceToConstant
213 | C.Variable (_,_,_,params,_) -> params
214 | C.CurrentProof _ -> raise ReferenceToCurrentProof
215 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
219 debug_print (lazy "\n\n---- BEGIN ") ;
220 debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
221 debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
222 debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
224 let exp_named_subst'' =
225 substaux_in_exp_named_subst uri k exp_named_subst' params
228 debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
229 debug_print (lazy "---- END\n\n ") ;
231 C.Var (uri,exp_named_subst'')
238 | Some t -> Some (substaux k t)
243 | C.Implicit _ as t -> t
244 | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
245 | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
246 | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
247 | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
249 (* Invariant: no Appl applied to another Appl *)
250 let tl' = List.map (substaux k) tl in
252 match substaux k he with
253 C.Appl l -> C.Appl (l@tl')
254 | _ as he' -> C.Appl (he'::tl')
256 | C.Appl _ -> assert false
257 | C.Const (uri,exp_named_subst') ->
259 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
261 C.Constant (_,_,_,params,_) -> params
262 | C.Variable _ -> raise ReferenceToVariable
263 | C.CurrentProof (_,_,_,_,params,_) -> params
264 | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
267 let exp_named_subst'' =
268 substaux_in_exp_named_subst uri k exp_named_subst' params
270 C.Const (uri,exp_named_subst'')
271 | C.MutInd (uri,typeno,exp_named_subst') ->
273 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
275 C.Constant _ -> raise ReferenceToConstant
276 | C.Variable _ -> raise ReferenceToVariable
277 | C.CurrentProof _ -> raise ReferenceToCurrentProof
278 | C.InductiveDefinition (_,params,_,_) -> params
281 let exp_named_subst'' =
282 substaux_in_exp_named_subst uri k exp_named_subst' params
284 C.MutInd (uri,typeno,exp_named_subst'')
285 | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
287 let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
289 C.Constant _ -> raise ReferenceToConstant
290 | C.Variable _ -> raise ReferenceToVariable
291 | C.CurrentProof _ -> raise ReferenceToCurrentProof
292 | C.InductiveDefinition (_,params,_,_) -> params
295 let exp_named_subst'' =
296 substaux_in_exp_named_subst uri k exp_named_subst' params
298 C.MutConstruct (uri,typeno,consno,exp_named_subst'')
299 | C.MutCase (sp,i,outt,t,pl) ->
300 C.MutCase (sp,i,substaux k outt, substaux k t,
301 List.map (substaux k) pl)
303 let len = List.length fl in
306 (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
309 C.Fix (i, substitutedfl)
311 let len = List.length fl in
314 (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
317 C.CoFix (i, substitutedfl)
318 and substaux_in_exp_named_subst uri k exp_named_subst' params =
319 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
320 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *)
321 let rec filter_and_lift =
326 (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
330 (uri,lift (k-1) t)::(filter_and_lift tl)
331 | _::tl -> filter_and_lift tl
334 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
335 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
336 exp_named_subst' then debug_print (lazy "---- OK1") ;
337 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
338 if List.mem uri params then debug_print (lazy "---- OK2") ;
342 List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
343 (filter_and_lift exp_named_subst)
348 (* subst_meta [t_1 ; ... ; t_n] t *)
349 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
350 (* [t_i] is lifted as usual when it crosses an abstraction *)
352 let module C = Cic in
353 if l = [] then t else
354 let rec aux k = function
356 if n <= k then t else
358 match List.nth l (n-k-1) with
359 None -> raise RelToHiddenHypothesis
362 (Failure _) -> assert false
364 | C.Var (uri,exp_named_subst) ->
365 let exp_named_subst' =
366 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
368 C.Var (uri,exp_named_subst')
378 RelToHiddenHypothesis -> None
383 | C.Implicit _ as t -> t
384 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
385 | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
386 | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
387 | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
388 | C.Appl l -> C.Appl (List.map (aux k) l)
389 | C.Const (uri,exp_named_subst) ->
390 let exp_named_subst' =
391 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
393 C.Const (uri,exp_named_subst')
394 | C.MutInd (uri,typeno,exp_named_subst) ->
395 let exp_named_subst' =
396 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
398 C.MutInd (uri,typeno,exp_named_subst')
399 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
400 let exp_named_subst' =
401 List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
403 C.MutConstruct (uri,typeno,consno,exp_named_subst')
404 | C.MutCase (sp,i,outt,t,pl) ->
405 C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
407 let len = List.length fl in
410 (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
413 C.Fix (i, substitutedfl)
415 let len = List.length fl in
418 (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
421 C.CoFix (i, substitutedfl)