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;;
27 (*CSC: Vecchia unificazione: exception Impossible;;*)
29 exception OccurCheck;;
31 type substitution = (int * Cic.term) list
33 (*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
34 (*CSC: lift? O creare una proofEngineSubstitution? *)
35 (* the function delift n m un-lifts a lambda term m of n level of abstractions.
36 It returns an exception Free if M contains a free variable in the range 1--n *)
42 if m < k then C.Rel m else
43 if m < k+n then raise Free
48 | C.Implicit as t -> t
49 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
50 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
51 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
52 | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
53 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
56 | C.MutInd _ as t -> t
57 | C.MutConstruct _ as t -> t
58 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
59 C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
60 List.map (deliftaux k) pl)
62 let len = List.length fl in
65 (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo))
70 let len = List.length fl in
73 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
84 (* Questa funzione non serve piu'... per il momento la lascio *)
86 let closed_up_to_n n m =
87 let rec closed_aux k =
90 C.Rel m -> if m > k then () else raise Free
92 | C.Meta _ (* we assume Meta are closed up to k; note that during
93 meta-unfolding we shall need to properly lift the
94 "body" of Metavariables *)
97 | C.Cast (te,ty) -> closed_aux k te; closed_aux k ty
98 | C.Prod (n,s,t) -> closed_aux k s; closed_aux (k+1) t
99 | C.Lambda (n,s,t) -> closed_aux k s; closed_aux (k+1) t
100 | C.LetIn (n,s,t) -> closed_aux k s; closed_aux (k+1) t
101 | C.Appl l -> List.iter (closed_aux k) l
105 | C.MutConstruct _ -> ()
106 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
107 closed_aux k outty; closed_aux k t;
108 List.iter (closed_aux k) pl
110 let len = List.length fl in
112 (fun (name, i, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
115 let len = List.length fl in
117 (fun (name, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo)
122 try closed_aux n m; true
126 (* NUOVA UNIFICAZIONE *)
127 (* A substitution is a (int * Cic.term) list that associates a
128 metavariable i with its body.
129 A metaenv is a (int * Cic.term) list that associate a metavariable
131 fo_unif_new takes a metasenv, a context,
132 two terms t1 and t2 and gives back a new
133 substitution which is _NOT_ unwinded. It must be unwinded before
136 let fo_unif_new metasenv context t1 t2 =
137 let module C = Cic in
138 let module R = CicReduction in
139 let module S = CicSubstitution in
140 let rec fo_unif_aux subst k t1 t2 =
142 (C.Meta n, C.Meta m) -> if n == m then subst
144 let tn = try List.assoc n subst
145 with Not_found -> C.Meta n in
146 let tm = try List.assoc m subst
147 with Not_found -> C.Meta m in
149 (C.Meta n, C.Meta m) -> if n==m then subst
151 then (m, C.Meta n)::subst
152 else (n, C.Meta m)::subst
153 | (C.Meta n, tm) -> (n, tm)::subst
154 | (tn, C.Meta m) -> (m, tn)::subst
155 | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
156 (* unify types first *)
157 let tyn = List.assoc n metasenv in
158 let tym = List.assoc m metasenv in
159 fo_unif_aux subst' 0 tyn tym
161 | (t, C.Meta n) -> (* unify types first *)
162 let t' = delift k t in
164 (try fo_unif_aux subst 0 (List.assoc n subst) t'
165 with Not_found -> (n, t')::subst) in
166 let tyn = List.assoc n metasenv in
167 let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
168 fo_unif_aux subst' 0 tyn tyt
176 | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
177 else raise UnificationFailed
178 | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
179 | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
180 | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) ->
181 let subst' = fo_unif_aux subst k s1 s2 in
182 fo_unif_aux subst' (k+1) t1 t2
183 | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) ->
184 let subst' = fo_unif_aux subst k s1 s2 in
185 fo_unif_aux subst' (k+1) t1 t2
186 | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
187 | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
188 | (C.Appl l1, C.Appl l2) ->
189 let lr1 = List.rev l1 in
190 let lr2 = List.rev l2 in
191 let rec fo_unif_l subst = function
193 | _,[] -> assert false
194 | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
196 | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
197 | ((h1::l1),(h2::l2)) ->
198 let subst' = fo_unif_aux subst k h1 h2 in
199 fo_unif_l subst' (l1,l2)
201 fo_unif_l subst (lr1, lr2)
208 | (C.MutConstruct _, _)
209 | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
210 else raise UnificationFailed
211 | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
212 let subst' = fo_unif_aux subst k outt1 outt2 in
213 let subst'' = fo_unif_aux subst' k t1 t2 in
214 List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2
218 | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
219 else raise UnificationFailed
220 | (_,_) -> raise UnificationFailed
221 in fo_unif_aux [] 0 t1 t2;;
223 (* VECCHIA UNIFICAZIONE -- molto piu' bella, alas *)
225 let fo_unif_mgu k t1 t2 mgu =
226 let module C = Cic in
227 let module R = CicReduction in
228 let module S = CicSubstitution in
229 let rec deref n = match mgu.(n) with
230 C.Meta m as t -> if n = m then t else (deref m)
233 let rec fo_unif k t1 t2 = match (t1, t2) with
234 (* aggiungere l'unificazione sui tipi in caso di istanziazione *)
235 (C.Meta n, C.Meta m) -> if n == m then () else
238 (* deref of metavariables ARE already delifted *)
239 (match (t1',t2') with
240 (C.Meta n, C.Meta m) -> if n = m then () else
241 if n < m then mgu.(m) <- t1' else
242 if n > m then mgu.(n) <- t2'
243 | (C.Meta n, _) -> mgu.(n) <- t2'
244 | (_, C.Meta m) -> mgu.(m) <- t1'
245 | (_,_) -> fo_unif k t1' t2')
246 | (C.Meta n, _) -> let t1' = deref n in
247 let t2' = try delift k t2
248 with Free -> raise UnificationFailed in
250 C.Meta n -> mgu.(n) <- t2'
251 | _ -> fo_unif k t1' t2')
252 | (_, C.Meta m) -> let t2' = deref m in
253 let t1' = try delift k t1
254 with Free -> raise UnificationFailed in
256 C.Meta m -> mgu.(m) <- t1'
257 | _ -> fo_unif k t1' t2')
265 | (_, C.Implicit) -> if R.are_convertible t1 t2 then ()
266 else raise UnificationFailed
267 | (C.Cast (te,ty), _) -> fo_unif k te t2
268 | (_, C.Cast (te,ty)) -> fo_unif k t1 te
269 | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> fo_unif k s1 s2;
271 | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> fo_unif k s1 s2;
273 | (C.LetIn (_,s1,t1), _) -> fo_unif k (S.subst s1 t1) t2
274 | (_, C.LetIn (_,s2,t2)) -> fo_unif k t1 (S.subst s2 t2)
275 | (C.Appl (h1::l1), C.Appl (h2::l2)) ->
276 let lr1 = List.rev l1 in
277 let lr2 = List.rev l2 in
278 let rec fo_unif_aux = function
281 | ((h1::l1),(h2::l2)) -> fo_unif k h1 h2;
284 (match fo_unif_aux (lr1, lr2) with
285 ([],[]) -> fo_unif k h1 h2
286 | ([],l2) -> fo_unif k h1 (C.Appl (h2::List.rev l2))
287 | (l1,[]) -> fo_unif k (C.Appl (h1::List.rev l1)) h2
288 | (_,_) -> raise Impossible)
295 | (C.MutConstruct _, _)
296 | (_, C.MutConstruct _) -> print_endline "siamo qui"; flush stdout;
297 if R.are_convertible t1 t2 then ()
298 else raise UnificationFailed
299 | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
300 fo_unif k outt1 outt2;
302 List.iter2 (fo_unif k) pl1 pl2
306 | (_, C.CoFix _) -> if R.are_convertible t1 t2 then ()
307 else raise UnificationFailed
308 | (_,_) -> raise UnificationFailed
309 in fo_unif k t1 t2;mgu ;;
312 (* unwind mgu mark m applies mgu to the term m; mark is an array of integers
313 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
314 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
315 the computation is an error: occur-check *)
317 let unwind subst unwinded t =
318 let unwinded = ref unwinded in
319 let frozen = ref [] in
321 let module C = Cic in
322 let module S = CicSubstitution in
326 | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
328 if List.mem i !frozen then
331 let saved_frozen = !frozen in
332 frozen := i::!frozen ;
335 let t = List.assoc i subst in
336 let t' = um_aux 0 t in
337 unwinded := (i,t)::!unwinded ;
341 (* not constrained variable, i.e. free in subst *)
344 frozen := saved_frozen ;
348 | C.Implicit as t -> t
349 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
350 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
351 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
352 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
354 let tl' = List.map (um_aux k) tl in
356 match um_aux k he with
357 C.Appl l -> C.Appl (l@tl')
358 | _ as he' -> C.Appl (he'::tl')
360 | C.Appl _ -> assert false
361 | C.Const _ as t -> t
363 | C.MutInd _ as t -> t
364 | C.MutConstruct _ as t -> t
365 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
366 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
367 List.map (um_aux k) pl)
369 let len = List.length fl in
372 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
377 let len = List.length fl in
380 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
383 C.CoFix (i, liftedfl)
389 let unwind_meta mgu mark =
391 let module C = Cic in
392 let module S = CicSubstitution in
396 | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
397 if mark.(i)=1 then S.lift k mgu.(i)
398 else (match mgu.(i) with
399 C.Meta k as t1 -> if k = i then t
401 mgu.(i) <- (um_aux 0 t1);
404 | _ -> (mark.(i) <- 2;
405 mgu.(i) <- (um_aux 0 mgu.(i));
409 | C.Implicit as t -> t
410 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
411 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
412 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
413 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
415 let tl' = List.map (um_aux k) tl in
417 match um_aux k he with
418 C.Appl l -> C.Appl (l@tl')
419 | _ as he' -> C.Appl (he'::tl')
421 | C.Appl _ -> assert false
422 | C.Const _ as t -> t
424 | C.MutInd _ as t -> t
425 | C.MutConstruct _ as t -> t
426 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
427 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
428 List.map (um_aux k) pl)
430 let len = List.length fl in
433 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
438 let len = List.length fl in
441 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
444 C.CoFix (i, liftedfl)
450 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
451 (* performs as (apply_subst subst t) until it finds an application of *)
452 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
453 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
454 (* beta-reductions are performed. *)
455 (* Hint: this function is usually called when [reductions_no] *)
456 (* eta-expansions have been performed and the head of the new *)
457 (* application has been unified with (META [meta_to_reduce]): *)
458 (* during the unwinding the eta-expansions are undone. *)
460 let apply_subst_reducing subst meta_to_reduce t =
461 let unwinded = ref subst in
463 let module C = Cic in
464 let module S = CicSubstitution in
470 S.lift k (List.assoc i !unwinded)
474 | C.Implicit as t -> t
475 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
476 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
477 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
478 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
480 let tl' = List.map (um_aux k) tl in
482 match um_aux k he with
483 C.Appl l -> C.Appl (l@tl')
484 | _ as he' -> C.Appl (he'::tl')
487 match meta_to_reduce with
488 Some (mtr,reductions_no) when he = C.Meta mtr ->
489 let rec beta_reduce =
491 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
492 let he'' = CicSubstitution.subst he' t in
496 beta_reduce (n-1,C.Appl(he''::tl'))
499 beta_reduce (reductions_no,t')
502 | C.Appl _ -> assert false
503 | C.Const _ as t -> t
505 | C.MutInd _ as t -> t
506 | C.MutConstruct _ as t -> t
507 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
508 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
509 List.map (um_aux k) pl)
511 let len = List.length fl in
514 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
519 let len = List.length fl in
522 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
525 C.CoFix (i, liftedfl)
530 (* unwind mgu mark mm m applies mgu to the term m; mark is an array of integers
531 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
532 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
533 the computation is an error: occur-check. When the META mm is to be unfolded
534 and it is applied to something, one-step beta reduction is performed just
535 after the unfolding. *)
538 let unwind_meta_reducing mgu mark meta_to_reduce =
540 let module C = Cic in
541 let module S = CicSubstitution in
545 | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else
546 if mark.(i)=1 then S.lift k mgu.(i)
547 else (match mgu.(i) with
548 C.Meta k as t1 -> if k = i then t
550 mgu.(i) <- (um_aux 0 t1);
553 | _ -> (mark.(i) <- 2;
554 mgu.(i) <- (um_aux 0 mgu.(i));
558 | C.Implicit as t -> t
559 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
560 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
561 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
562 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
564 let tl' = List.map (um_aux k) tl in
566 match um_aux k he with
567 C.Appl l -> C.Appl (l@tl')
568 | _ as he' -> C.Appl (he'::tl')
571 match t', meta_to_reduce with
572 (C.Appl (C.Lambda (n,s,t)::he'::tl')),Some mtr
573 when he = C.Meta mtr ->
574 (*CSC: Sbagliato!!! Effettua beta riduzione solo del primo argomento
575 *CSC: mentre dovrebbe farla dei primi n, dove n sono quelli eta-astratti
577 C.Appl((CicSubstitution.subst he' t)::tl')
580 | C.Appl _ -> assert false
581 | C.Const _ as t -> t
583 | C.MutInd _ as t -> t
584 | C.MutConstruct _ as t -> t
585 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
586 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
587 List.map (um_aux k) pl)
589 let len = List.length fl in
592 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
597 let len = List.length fl in
600 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
603 C.CoFix (i, liftedfl)
608 (* UNWIND THE MGU INSIDE THE MGU *)
610 let mark = Array.make (Array.length mgu) 0 in
611 Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *)
613 let unwind_subst subst =
615 (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
618 let apply_subst subst t =
619 fst (unwind [] subst t)
622 (* A substitution is a (int * Cic.term) list that associates a
623 metavariable i with its body.
624 A metaenv is a (int * Cic.term) list that associate a metavariable
626 fo_unif takes a metasenv, a context,
627 two terms t1 and t2 and gives back a new
628 substitution which is already unwinded and ready to be applied. *)
629 let fo_unif metasenv context t1 t2 =
630 let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
631 unwind_subst subst_to_unwind