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 UnificationFailed;;
28 exception OccurCheck;;
29 exception RelToHiddenHypothesis;;
34 (* the delift function takes in input an ordered list of integers [n1,...,nk]
35 and a term t, and relocates rel(nk) to k. Typically, the list of integers
36 is a parameter of a metavariable occurrence. *)
38 exception NotInTheList;;
43 [] -> raise NotInTheList
44 | (Some (Cic.Rel m))::_ when m=n -> k
45 | _::tl -> aux (k+1) tl in
49 let restrict to_be_restricted =
53 | _::tl when List.mem (n,i) to_be_restricted ->
54 None::(erase (i+1) n tl)
55 | he::tl -> he::(erase (i+1) n tl) in
59 | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
64 let delift context metasenv l t =
65 let module S = CicSubstitution in
66 let to_be_restricted = ref [] in
72 C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
73 (*CSC: deliftato la regola per il LetIn *)
75 (match List.nth context (m-k-1) with
76 Some (_,C.Def t) -> deliftaux k (S.lift m t)
77 | Some (_,C.Decl t) ->
78 (* It may augment to_be_restricted *)
79 ignore (deliftaux k (S.lift m t)) ;
80 C.Rel ((position (m-k) l) + k)
81 | None -> raise RelToHiddenHypothesis)
83 | C.Meta (i, l1) as t ->
87 | None::tl -> None::(deliftl (j+1) tl)
89 let l1' = (deliftl (j+1) tl) in
91 Some (deliftaux k t)::l1'
95 to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
97 let l' = deliftl 1 l1 in
100 | C.Implicit as t -> t
101 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
102 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
103 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
104 | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
105 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
106 | C.Const _ as t -> t
107 | C.MutInd _ as t -> t
108 | C.MutConstruct _ as t -> t
109 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
110 C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
111 List.map (deliftaux k) pl)
113 let len = List.length fl in
116 (fun (name, i, ty, bo) ->
117 (name, i, deliftaux k ty, deliftaux (k+len) bo))
122 let len = List.length fl in
125 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
128 C.CoFix (i, liftedfl)
130 let res = deliftaux 0 t in
131 res, restrict !to_be_restricted metasenv
134 (**** END OF DELIFT ****)
136 type substitution = (int * Cic.term) list
138 (* NUOVA UNIFICAZIONE *)
139 (* A substitution is a (int * Cic.term) list that associates a
140 metavariable i with its body.
141 A metaenv is a (int * Cic.term) list that associate a metavariable
143 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
144 a new substitution which is _NOT_ unwinded. It must be unwinded before
147 let fo_unif_new metasenv context t1 t2 =
148 let module C = Cic in
149 let module R = CicReduction in
150 let module S = CicSubstitution in
151 let rec fo_unif_aux subst context metasenv t1 t2 =
153 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
161 | Some t1', Some t2' ->
162 (* First possibility: restriction *)
163 (* Second possibility: unification *)
164 (* Third possibility: convertibility *)
165 R.are_convertible context t1' t2'
168 if ok then subst,metasenv else
169 raise UnificationFailed
170 | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
171 fo_unif_aux subst context metasenv t2 t1
173 | (t, C.Meta (n,l)) ->
174 let subst',metasenv' =
176 let oldt = (List.assoc n subst) in
177 let lifted_oldt = S.lift_meta l oldt in
178 fo_unif_aux subst context metasenv lifted_oldt t
180 prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ;
181 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
182 prerr_endline "<DELIFT2" ; flush stderr ;
183 let t',metasenv' = delift context metasenv l t in
184 (n, t')::subst, metasenv'
186 let (_,_,meta_type) =
187 List.find (function (m,_,_) -> m=n) metasenv' in
188 let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
189 fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt
198 if R.are_convertible context t1 t2 then subst, metasenv
199 else raise UnificationFailed
200 | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2
201 | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te
202 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
203 let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
204 fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
205 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
206 let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
207 fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
208 | (C.LetIn (_,s1,t1), t2)
209 | (t2, C.LetIn (_,s1,t1)) ->
210 fo_unif_aux subst context metasenv t2 (S.subst s1 t1)
211 | (C.Appl l1, C.Appl l2) ->
212 let lr1 = List.rev l1 in
213 let lr2 = List.rev l2 in
214 let rec fo_unif_l subst metasenv = function
216 | _,[] -> assert false
218 fo_unif_aux subst context metasenv h1 h2
221 fo_unif_aux subst context metasenv h (C.Appl (List.rev l))
222 | ((h1::l1),(h2::l2)) ->
223 let subst', metasenv' =
224 fo_unif_aux subst context metasenv h1 h2
226 fo_unif_l subst' metasenv' (l1,l2)
228 fo_unif_l subst metasenv (lr1, lr2)
233 | (C.MutConstruct _, _)
234 | (_, C.MutConstruct _) ->
235 if R.are_convertible context t1 t2 then subst, metasenv
236 else raise UnificationFailed
237 | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
238 let subst', metasenv' =
239 fo_unif_aux subst context metasenv outt1 outt2 in
240 let subst'',metasenv'' =
241 fo_unif_aux subst' context metasenv' t1 t2 in
243 (function (subst,metasenv) ->
244 fo_unif_aux subst context metasenv
245 ) (subst'',metasenv'') pl1 pl2
250 if R.are_convertible context t1 t2 then subst, metasenv
251 else raise UnificationFailed
252 | (_,_) -> raise UnificationFailed
253 in fo_unif_aux [] context metasenv t1 t2;;
255 (*CSC: ???????????????
256 (* m is the index of a metavariable to restrict, k is nesting depth
257 of the occurrence m, and l is its relocation list. canonical_context
258 is the context of the metavariable we are instantiating - containing
259 m - Only rel in the domain of canonical_context are accessible.
260 This function takes in input a metasenv and gives back a metasenv.
261 A rel(j) in the canonical context of m, is rel(List.nth l j) for the
262 instance of m under consideration, that is rel (List.nth l j) - k
263 in canonical_context. *)
265 let restrict canonical_context m k l =
269 | None::tl -> None::(erase (i+1) tl)
271 let i' = (List.nth l (i-1)) in
273 then he::(erase (i+1) tl) (* local variable *)
276 (try List.nth canonical_context (i'-k-1)
277 with Failure _ -> None) in
279 then None::(erase (i+1) tl)
280 else he::(erase (i+1) tl) in
284 | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
285 | hd::tl -> hd::(aux tl)
291 let check_accessibility metasenv i =
292 let module C = Cic in
293 let module S = CicSubstitution in
294 let (_,canonical_context,_) =
295 List.find (function (m,_,_) -> m=i) metasenv in
299 delift canonical_context metasenv ? t
305 let rec aux metasenv k =
312 match List.nth canonical_context (i-k-1) with
314 | Some (_,C.Def t) -> aux metasenv k (S.lift i t)
315 | None -> raise RelToHiddenHypothesis
317 Failure _ -> raise OpenTerm
319 | C.Var _ -> metasenv
320 | C.Meta (i,l) -> restrict canonical_context i k l metasenv
321 | C.Sort _ -> metasenv
322 | C.Implicit -> metasenv
324 let metasenv' = aux metasenv k te in
329 let metasenv' = aux metasenv k s in
330 aux metasenv' (k+1) t
333 (function metasenv -> aux metasenv k) metasenv l
336 | C.MutConstruct _ -> metasenv
337 | C.MutCase (_,_,_,outty,t,pl) ->
338 let metasenv' = aux metasenv k outty in
339 let metasenv'' = aux metasenv' k t in
341 (function metasenv -> aux metasenv k) metasenv'' pl
343 let len = List.length fl in
346 let (_,_,ty,bo) = f in
347 let metasenv' = aux metasenv k ty in
348 aux metasenv' (k+len) bo
351 let len = List.length fl in
355 let metasenv' = aux metasenv k ty in
356 aux metasenv' (k+len) bo
363 let unwind metasenv subst unwinded t =
364 let unwinded = ref unwinded in
365 let frozen = ref [] in
366 let rec um_aux metasenv =
367 let module C = Cic in
368 let module S = CicSubstitution in
370 C.Rel _ as t -> t,metasenv
371 | C.Var _ as t -> t,metasenv
374 S.lift_meta l (List.assoc i !unwinded), metasenv
376 if List.mem i !frozen then raise OccurCheck
378 let saved_frozen = !frozen in
379 frozen := i::!frozen ;
382 let t = List.assoc i subst in
383 let t',metasenv' = um_aux metasenv t in
385 let (_,canonical_context,_) =
386 List.find (function (m,_,_) -> m=i) metasenv
388 prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
389 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
390 prerr_endline "<DELIFT" ; flush stderr ;
391 delift canonical_context metasenv' l t'
393 unwinded := (i,t')::!unwinded ;
394 S.lift_meta l t', metasenv'
397 (* not constrained variable, i.e. free in subst*)
400 (fun t (tl,metasenv) ->
402 None -> None::tl,metasenv
404 let t',metasenv' = um_aux metasenv t in
405 (Some t')::tl, metasenv'
408 C.Meta (i,l'), metasenv'
410 frozen := saved_frozen ;
414 | C.Implicit as t -> t,metasenv
416 let te',metasenv' = um_aux metasenv te in
417 let ty',metasenv'' = um_aux metasenv' ty in
418 C.Cast (te',ty'),metasenv''
420 let s',metasenv' = um_aux metasenv s in
421 let t',metasenv'' = um_aux metasenv' t in
422 C.Prod (n, s', t'), metasenv''
423 | C.Lambda (n,s,t) ->
424 let s',metasenv' = um_aux metasenv s in
425 let t',metasenv'' = um_aux metasenv' t in
426 C.Lambda (n, s', t'), metasenv''
428 let s',metasenv' = um_aux metasenv s in
429 let t',metasenv'' = um_aux metasenv' t in
430 C.LetIn (n, s', t'), metasenv''
434 (fun t (tl,metasenv) ->
435 let t',metasenv' = um_aux metasenv t in
440 match um_aux metasenv' he with
441 (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
442 | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
444 | C.Appl _ -> assert false
447 | C.MutConstruct _ as t -> t,metasenv
448 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
449 let outty',metasenv' = um_aux metasenv outty in
450 let t',metasenv'' = um_aux metasenv' t in
451 let pl',metasenv''' =
453 (fun p (pl,metasenv) ->
454 let p',metasenv' = um_aux metasenv p in
458 C.MutCase (sp, cookingsno, i, outty', t', pl'),metasenv'''
460 let len = List.length fl in
461 let liftedfl,metasenv' =
463 (fun (name, i, ty, bo) (fl,metasenv) ->
464 let ty',metasenv' = um_aux metasenv ty in
465 let bo',metasenv'' = um_aux metasenv' bo in
466 (name, i, ty', bo')::fl,metasenv''
469 C.Fix (i, liftedfl),metasenv'
471 let len = List.length fl in
472 let liftedfl,metasenv' =
474 (fun (name, ty, bo) (fl,metasenv) ->
475 let ty',metasenv' = um_aux metasenv ty in
476 let bo',metasenv'' = um_aux metasenv' bo in
477 (name, ty', bo')::fl,metasenv''
480 C.CoFix (i, liftedfl),metasenv'
482 let t',metasenv' = um_aux metasenv t in
483 t',metasenv',!unwinded
486 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
487 (* performs as (apply_subst subst t) until it finds an application of *)
488 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
489 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
490 (* beta-reductions are performed. *)
491 (* Hint: this function is usually called when [reductions_no] *)
492 (* eta-expansions have been performed and the head of the new *)
493 (* application has been unified with (META [meta_to_reduce]): *)
494 (* during the unwinding the eta-expansions are undone. *)
496 let apply_subst_reducing subst meta_to_reduce t =
497 let unwinded = ref subst in
499 let module C = Cic in
500 let module S = CicSubstitution in
504 | C.Meta (i,l) as t ->
506 S.lift_meta l (List.assoc i !unwinded)
510 | C.Implicit as t -> t
511 | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
512 | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
513 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
514 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
516 let tl' = List.map um_aux tl in
519 C.Appl l -> C.Appl (l@tl')
520 | _ as he' -> C.Appl (he'::tl')
523 match meta_to_reduce,he with
524 Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
525 let rec beta_reduce =
527 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
528 let he'' = CicSubstitution.subst he' t in
532 beta_reduce (n-1,C.Appl(he''::tl'))
535 beta_reduce (reductions_no,t')
538 | C.Appl _ -> assert false
539 | C.Const _ as t -> t
540 | C.MutInd _ as t -> t
541 | C.MutConstruct _ as t -> t
542 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
543 C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t,
546 let len = List.length fl in
549 (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
554 let len = List.length fl in
557 (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
560 C.CoFix (i, liftedfl)
565 (* UNWIND THE MGU INSIDE THE MGU *)
566 let unwind_subst metasenv subst =
567 let identity_relocation_list_for_metavariable i =
568 let (_,canonical_context,_) =
569 List.find (function (m,_,_) -> m=i) metasenv
571 let canonical_context_length = List.length canonical_context in
574 n when n > canonical_context_length -> []
575 | n -> (Some (Cic.Rel n))::(aux (n+1))
580 (fun (unwinded,metasenv) (i,_) ->
581 let identity_relocation_list =
582 identity_relocation_list_for_metavariable i
584 let (_,metasenv',subst') =
585 unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
588 ) ([],metasenv) subst
591 let apply_subst subst t =
592 (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
594 let (t',_,_) = unwind metasenv [] subst t in
598 (* A substitution is a (int * Cic.term) list that associates a *)
599 (* metavariable i with its body. *)
600 (* metasenv is of type Cic.metasenv *)
601 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
602 (* a new substitution which is already unwinded and ready to be applied and *)
603 (* a new metasenv in which some hypothesis in the contexts of the *)
604 (* metavariables may have been restricted. *)
605 let fo_unif metasenv context t1 t2 =
606 prerr_endline "INIZIO FASE 1" ; flush stderr ;
607 let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in
608 prerr_endline "FINE FASE 1" ; flush stderr ;
610 unwind_subst metasenv' subst_to_unwind
612 prerr_endline "FINE FASE 2" ; flush stderr ; res