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;;
32 type substitution = (int * Cic.term) list
34 (* NUOVA UNIFICAZIONE *)
35 (* A substitution is a (int * Cic.term) list that associates a
36 metavariable i with its body.
37 A metaenv is a (int * Cic.term) list that associate a metavariable
39 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
40 a new substitution which is _NOT_ unwinded. It must be unwinded before
43 let fo_unif_new metasenv context t1 t2 =
45 let module R = CicReduction in
46 let module S = CicSubstitution in
47 let rec fo_unif_aux subst context metasenv t1 t2 =
49 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
57 | Some t1', Some t2' ->
58 (* First possibility: restriction *)
59 (* Second possibility: unification *)
60 (* Third possibility: convertibility *)
61 R.are_convertible context t1' t2'
64 if ok then subst,metasenv else
65 raise UnificationFailed
66 | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
67 fo_unif_aux subst context metasenv t2 t1
69 | (t, C.Meta (n,l)) ->
70 let subst',metasenv' =
72 let oldt = (List.assoc n subst) in
73 let lifted_oldt = S.lift_meta l oldt in
74 fo_unif_aux subst context metasenv lifted_oldt t
76 prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ;
77 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
78 prerr_endline "<DELIFT2" ; flush stderr ;
79 let t',metasenv' = S.delift context metasenv l t in
80 (n, t')::subst, metasenv'
83 List.find (function (m,_,_) -> m=n) metasenv' in
84 let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
85 fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt
94 if R.are_convertible context t1 t2 then subst, metasenv
95 else raise UnificationFailed
96 | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2
97 | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te
98 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
99 let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
100 fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
101 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
102 let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in
103 fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
104 | (C.LetIn (_,s1,t1), t2)
105 | (t2, C.LetIn (_,s1,t1)) ->
106 fo_unif_aux subst context metasenv t2 (S.subst s1 t1)
107 | (C.Appl l1, C.Appl l2) ->
108 let lr1 = List.rev l1 in
109 let lr2 = List.rev l2 in
110 let rec fo_unif_l subst metasenv = function
112 | _,[] -> assert false
114 fo_unif_aux subst context metasenv h1 h2
117 fo_unif_aux subst context metasenv h (C.Appl (List.rev l))
118 | ((h1::l1),(h2::l2)) ->
119 let subst', metasenv' =
120 fo_unif_aux subst context metasenv h1 h2
122 fo_unif_l subst' metasenv' (l1,l2)
124 fo_unif_l subst metasenv (lr1, lr2)
131 | (C.MutConstruct _, _)
132 | (_, C.MutConstruct _) ->
133 if R.are_convertible context t1 t2 then subst, metasenv
134 else raise UnificationFailed
135 | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
136 let subst', metasenv' =
137 fo_unif_aux subst context metasenv outt1 outt2 in
138 let subst'',metasenv'' =
139 fo_unif_aux subst' context metasenv' t1 t2 in
141 (function (subst,metasenv) ->
142 fo_unif_aux subst context metasenv
143 ) (subst'',metasenv'') pl1 pl2
148 if R.are_convertible context t1 t2 then subst, metasenv
149 else raise UnificationFailed
150 | (_,_) -> raise UnificationFailed
151 in fo_unif_aux [] context metasenv t1 t2;;
153 (*CSC: ???????????????
154 (* m is the index of a metavariable to restrict, k is nesting depth
155 of the occurrence m, and l is its relocation list. canonical_context
156 is the context of the metavariable we are instantiating - containing
157 m - Only rel in the domain of canonical_context are accessible.
158 This function takes in input a metasenv and gives back a metasenv.
159 A rel(j) in the canonical context of m, is rel(List.nth l j) for the
160 instance of m under consideration, that is rel (List.nth l j) - k
161 in canonical_context. *)
163 let restrict canonical_context m k l =
167 | None::tl -> None::(erase (i+1) tl)
169 let i' = (List.nth l (i-1)) in
171 then he::(erase (i+1) tl) (* local variable *)
174 (try List.nth canonical_context (i'-k-1)
175 with Failure _ -> None) in
177 then None::(erase (i+1) tl)
178 else he::(erase (i+1) tl) in
182 | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
183 | hd::tl -> hd::(aux tl)
189 let check_accessibility metasenv i =
190 let module C = Cic in
191 let module S = CicSubstitution in
192 let (_,canonical_context,_) =
193 List.find (function (m,_,_) -> m=i) metasenv in
197 S.delift canonical_context metasenv ? t
203 let rec aux metasenv k =
210 match List.nth canonical_context (i-k-1) with
212 | Some (_,C.Def t) -> aux metasenv k (S.lift i t)
213 | None -> raise RelToHiddenHypothesis
215 Failure _ -> raise OpenTerm
217 | C.Var _ -> metasenv
218 | C.Meta (i,l) -> restrict canonical_context i k l metasenv
219 | C.Sort _ -> metasenv
220 | C.Implicit -> metasenv
222 let metasenv' = aux metasenv k te in
227 let metasenv' = aux metasenv k s in
228 aux metasenv' (k+1) t
231 (function metasenv -> aux metasenv k) metasenv l
235 | C.MutConstruct _ -> metasenv
236 | C.MutCase (_,_,_,outty,t,pl) ->
237 let metasenv' = aux metasenv k outty in
238 let metasenv'' = aux metasenv' k t in
240 (function metasenv -> aux metasenv k) metasenv'' pl
242 let len = List.length fl in
245 let (_,_,ty,bo) = f in
246 let metasenv' = aux metasenv k ty in
247 aux metasenv' (k+len) bo
250 let len = List.length fl in
254 let metasenv' = aux metasenv k ty in
255 aux metasenv' (k+len) bo
262 let unwind metasenv subst unwinded t =
263 let unwinded = ref unwinded in
264 let frozen = ref [] in
265 let rec um_aux metasenv =
266 let module C = Cic in
267 let module S = CicSubstitution in
269 C.Rel _ as t -> t,metasenv
270 | C.Var _ as t -> t,metasenv
273 S.lift_meta l (List.assoc i !unwinded), metasenv
275 if List.mem i !frozen then raise OccurCheck
277 let saved_frozen = !frozen in
278 frozen := i::!frozen ;
281 let t = List.assoc i subst in
282 let t',metasenv' = um_aux metasenv t in
284 let (_,canonical_context,_) =
285 List.find (function (m,_,_) -> m=i) metasenv
287 prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
288 List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
289 prerr_endline "<DELIFT" ; flush stderr ;
290 S.delift canonical_context metasenv' l t'
292 unwinded := (i,t')::!unwinded ;
293 S.lift_meta l t', metasenv'
296 (* not constrained variable, i.e. free in subst*)
299 (fun t (tl,metasenv) ->
301 None -> None::tl,metasenv
303 let t',metasenv' = um_aux metasenv t in
304 (Some t')::tl, metasenv'
307 C.Meta (i,l'), metasenv'
309 frozen := saved_frozen ;
313 | C.Implicit as t -> t,metasenv
315 let te',metasenv' = um_aux metasenv te in
316 let ty',metasenv'' = um_aux metasenv' ty in
317 C.Cast (te',ty'),metasenv''
319 let s',metasenv' = um_aux metasenv s in
320 let t',metasenv'' = um_aux metasenv' t in
321 C.Prod (n, s', t'), metasenv''
322 | C.Lambda (n,s,t) ->
323 let s',metasenv' = um_aux metasenv s in
324 let t',metasenv'' = um_aux metasenv' t in
325 C.Lambda (n, s', t'), metasenv''
327 let s',metasenv' = um_aux metasenv s in
328 let t',metasenv'' = um_aux metasenv' t in
329 C.LetIn (n, s', t'), metasenv''
333 (fun t (tl,metasenv) ->
334 let t',metasenv' = um_aux metasenv t in
339 match um_aux metasenv' he with
340 (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
341 | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
343 | C.Appl _ -> assert false
347 | C.MutConstruct _ as t -> t,metasenv
348 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
349 let outty',metasenv' = um_aux metasenv outty in
350 let t',metasenv'' = um_aux metasenv' t in
351 let pl',metasenv''' =
353 (fun p (pl,metasenv) ->
354 let p',metasenv' = um_aux metasenv p in
358 C.MutCase (sp, cookingsno, i, outty', t', pl'),metasenv'''
360 let len = List.length fl in
361 let liftedfl,metasenv' =
363 (fun (name, i, ty, bo) (fl,metasenv) ->
364 let ty',metasenv' = um_aux metasenv ty in
365 let bo',metasenv'' = um_aux metasenv' bo in
366 (name, i, ty', bo')::fl,metasenv''
369 C.Fix (i, liftedfl),metasenv'
371 let len = List.length fl in
372 let liftedfl,metasenv' =
374 (fun (name, ty, bo) (fl,metasenv) ->
375 let ty',metasenv' = um_aux metasenv ty in
376 let bo',metasenv'' = um_aux metasenv' bo in
377 (name, ty', bo')::fl,metasenv''
380 C.CoFix (i, liftedfl),metasenv'
382 let t',metasenv' = um_aux metasenv t in
383 t',metasenv',!unwinded
386 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
387 (* performs as (apply_subst subst t) until it finds an application of *)
388 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
389 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
390 (* beta-reductions are performed. *)
391 (* Hint: this function is usually called when [reductions_no] *)
392 (* eta-expansions have been performed and the head of the new *)
393 (* application has been unified with (META [meta_to_reduce]): *)
394 (* during the unwinding the eta-expansions are undone. *)
396 let apply_subst_reducing subst meta_to_reduce t =
397 let unwinded = ref subst in
399 let module C = Cic in
400 let module S = CicSubstitution in
404 | C.Meta (i,l) as t ->
406 S.lift_meta l (List.assoc i !unwinded)
410 | C.Implicit as t -> t
411 | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
412 | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
413 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
414 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
416 let tl' = List.map um_aux tl in
419 C.Appl l -> C.Appl (l@tl')
420 | _ as he' -> C.Appl (he'::tl')
423 match meta_to_reduce,he with
424 Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
425 let rec beta_reduce =
427 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
428 let he'' = CicSubstitution.subst he' t in
432 beta_reduce (n-1,C.Appl(he''::tl'))
435 beta_reduce (reductions_no,t')
438 | C.Appl _ -> assert false
439 | C.Const _ as t -> t
441 | C.MutInd _ as t -> t
442 | C.MutConstruct _ as t -> t
443 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
444 C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t,
447 let len = List.length fl in
450 (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
455 let len = List.length fl in
458 (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
461 C.CoFix (i, liftedfl)
466 (* UNWIND THE MGU INSIDE THE MGU *)
467 let unwind_subst metasenv subst =
468 let identity_relocation_list_for_metavariable i =
469 let (_,canonical_context,_) =
470 List.find (function (m,_,_) -> m=i) metasenv
472 let canonical_context_length = List.length canonical_context in
475 n when n > canonical_context_length -> []
476 | n -> (Some (Cic.Rel n))::(aux (n+1))
481 (fun (unwinded,metasenv) (i,_) ->
482 let identity_relocation_list =
483 identity_relocation_list_for_metavariable i
485 let (_,metasenv',subst') =
486 unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
489 ) ([],metasenv) subst
492 let apply_subst subst t =
493 (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
495 let (t',_,_) = unwind metasenv [] subst t in
499 (* A substitution is a (int * Cic.term) list that associates a *)
500 (* metavariable i with its body. *)
501 (* metasenv is of type Cic.metasenv *)
502 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
503 (* a new substitution which is already unwinded and ready to be applied and *)
504 (* a new metasenv in which some hypothesis in the contexts of the *)
505 (* metavariables may have been restricted. *)
506 let fo_unif metasenv context t1 t2 =
507 prerr_endline "INIZIO FASE 1" ; flush stderr ;
508 let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in
509 prerr_endline "FINE FASE 1" ; flush stderr ;
511 unwind_subst metasenv' subst_to_unwind
513 prerr_endline "FINE FASE 2" ; flush stderr ; res