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;;
30 type substitution = (int * Cic.term) list
32 (*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
33 (*CSC: lift? O creare una proofEngineSubstitution? *)
34 (* the function delift n m un-lifts a lambda term m of n level of abstractions.
35 It returns an exception Free if M contains a free variable in the range 1--n *)
41 if m < k then C.Rel m else
42 if m < k+n then raise Free
47 | C.Implicit as t -> t
48 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
49 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
50 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
51 | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
52 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
55 | C.MutInd _ as t -> t
56 | C.MutConstruct _ as t -> t
57 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
58 C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
59 List.map (deliftaux k) pl)
61 let len = List.length fl in
64 (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo))
69 let len = List.length fl in
72 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
83 (* NUOVA UNIFICAZIONE *)
84 (* A substitution is a (int * Cic.term) list that associates a
85 metavariable i with its body.
86 A metaenv is a (int * Cic.term) list that associate a metavariable
88 fo_unif_new takes a metasenv, a context,
89 two terms t1 and t2 and gives back a new
90 substitution which is _NOT_ unwinded. It must be unwinded before
93 let fo_unif_new metasenv context t1 t2 =
95 let module R = CicReduction in
96 let module S = CicSubstitution in
97 let rec fo_unif_aux subst k t1 t2 =
99 (C.Meta n, C.Meta m) -> if n == m then subst
101 let tn = try List.assoc n subst
102 with Not_found -> C.Meta n in
103 let tm = try List.assoc m subst
104 with Not_found -> C.Meta m in
106 (C.Meta n, C.Meta m) -> if n==m then subst
108 then (m, C.Meta n)::subst
109 else (n, C.Meta m)::subst
110 | (C.Meta n, tm) -> (n, tm)::subst
111 | (tn, C.Meta m) -> (m, tn)::subst
112 | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
113 (* unify types first *)
114 let tyn = List.assoc n metasenv in
115 let tym = List.assoc m metasenv in
116 fo_unif_aux subst' 0 tyn tym
118 | (t, C.Meta n) -> (* unify types first *)
119 let t' = delift k t in
121 (try fo_unif_aux subst 0 (List.assoc n subst) t'
122 with Not_found -> (n, t')::subst) in
123 let tyn = List.assoc n metasenv in
124 let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
125 fo_unif_aux subst' 0 tyn tyt
133 | (_, C.Implicit) -> if R.are_convertible context t1 t2 then subst
134 else raise UnificationFailed
135 | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
136 | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
137 | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) ->
138 let subst' = fo_unif_aux subst k s1 s2 in
139 fo_unif_aux subst' (k+1) t1 t2
140 | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) ->
141 let subst' = fo_unif_aux subst k s1 s2 in
142 fo_unif_aux subst' (k+1) t1 t2
143 | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
144 | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
145 | (C.Appl l1, C.Appl l2) ->
146 let lr1 = List.rev l1 in
147 let lr2 = List.rev l2 in
148 let rec fo_unif_l subst = function
150 | _,[] -> assert false
151 | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
153 | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
154 | ((h1::l1),(h2::l2)) ->
155 let subst' = fo_unif_aux subst k h1 h2 in
156 fo_unif_l subst' (l1,l2)
158 fo_unif_l subst (lr1, lr2)
165 | (C.MutConstruct _, _)
166 | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst
167 else raise UnificationFailed
168 | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
169 let subst' = fo_unif_aux subst k outt1 outt2 in
170 let subst'' = fo_unif_aux subst' k t1 t2 in
171 List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2
175 | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst
176 else raise UnificationFailed
177 | (_,_) -> raise UnificationFailed
178 in fo_unif_aux [] 0 t1 t2;;
180 (* unwind mgu mark m applies mgu to the term m; mark is an array of integers
181 mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding,
182 and is 1 if it has been succesfully unwinded. Meeting the value 2 during
183 the computation is an error: occur-check *)
185 let unwind subst unwinded t =
186 let unwinded = ref unwinded in
187 let frozen = ref [] in
189 let module C = Cic in
190 let module S = CicSubstitution in
194 | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
196 if List.mem i !frozen then
199 let saved_frozen = !frozen in
200 frozen := i::!frozen ;
203 let t = List.assoc i subst in
204 let t' = um_aux 0 t in
205 unwinded := (i,t')::!unwinded ;
209 (* not constrained variable, i.e. free in subst*)
212 frozen := saved_frozen ;
216 | C.Implicit as t -> t
217 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
218 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
219 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
220 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
222 let tl' = List.map (um_aux k) tl in
224 match um_aux k he with
225 C.Appl l -> C.Appl (l@tl')
226 | _ as he' -> C.Appl (he'::tl')
228 | C.Appl _ -> assert false
229 | C.Const _ as t -> t
231 | C.MutInd _ as t -> t
232 | C.MutConstruct _ as t -> t
233 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
234 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
235 List.map (um_aux k) pl)
237 let len = List.length fl in
240 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
245 let len = List.length fl in
248 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
251 C.CoFix (i, liftedfl)
256 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
257 (* performs as (apply_subst subst t) until it finds an application of *)
258 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
259 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
260 (* beta-reductions are performed. *)
261 (* Hint: this function is usually called when [reductions_no] *)
262 (* eta-expansions have been performed and the head of the new *)
263 (* application has been unified with (META [meta_to_reduce]): *)
264 (* during the unwinding the eta-expansions are undone. *)
266 let apply_subst_reducing subst meta_to_reduce t =
267 let unwinded = ref subst in
269 let module C = Cic in
270 let module S = CicSubstitution in
276 S.lift k (List.assoc i !unwinded)
280 | C.Implicit as t -> t
281 | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
282 | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
283 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
284 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
286 let tl' = List.map (um_aux k) tl in
288 match um_aux k he with
289 C.Appl l -> C.Appl (l@tl')
290 | _ as he' -> C.Appl (he'::tl')
293 match meta_to_reduce with
294 Some (mtr,reductions_no) when he = C.Meta mtr ->
295 let rec beta_reduce =
297 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
298 let he'' = CicSubstitution.subst he' t in
302 beta_reduce (n-1,C.Appl(he''::tl'))
305 beta_reduce (reductions_no,t')
308 | C.Appl _ -> assert false
309 | C.Const _ as t -> t
311 | C.MutInd _ as t -> t
312 | C.MutConstruct _ as t -> t
313 | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
314 C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
315 List.map (um_aux k) pl)
317 let len = List.length fl in
320 (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo))
325 let len = List.length fl in
328 (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo))
331 C.CoFix (i, liftedfl)
336 (* UNWIND THE MGU INSIDE THE MGU *)
337 let unwind_subst subst =
339 (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
342 let apply_subst subst t =
343 fst (unwind [] subst t)
346 (* A substitution is a (int * Cic.term) list that associates a
347 metavariable i with its body.
348 A metaenv is a (int * Cic.term) list that associate a metavariable
350 fo_unif takes a metasenv, a context,
351 two terms t1 and t2 and gives back a new
352 substitution which is already unwinded and ready to be applied. *)
353 let fo_unif metasenv context t1 t2 =
354 let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
355 unwind_subst subst_to_unwind