4 exception AssertFailure of string
5 exception MetaSubstFailure of string
7 exception RelToHiddenHypothesis (* TODO remove this exception *)
9 let debug_print = prerr_endline
11 type substitution = (int * Cic.term) list
16 (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
20 (* the delift function takes in input a metavariable index, an ordered list of
21 * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
22 * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit
23 * substitution that is applied to a metavariable occurrence and the result of
24 * the delift function is a term the implicit variable can be substituted with
25 * to make the term [t] unifiable with the metavariable occurrence. In general,
26 * the problem is undecidable if we consider equivalence in place of alpha
27 * convertibility. Our implementation, though, is even weaker than alpha
28 * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
29 * (missing all the other cases). Does this matter in practice?
30 * The metavariable index is the index of the metavariable that must not occur
31 * in the term (for occur check).
34 exception NotInTheList;;
39 [] -> raise NotInTheList
40 | (Some (Cic.Rel m))::_ when m=n -> k
41 | _::tl -> aux (k+1) tl in
45 (*CSC: this restriction function is utterly wrong, since it does not check *)
46 (*CSC: that the variable that is going to be restricted does not occur free *)
47 (*CSC: in a part of the sequent that is not going to be restricted. *)
48 (*CSC: In particular, the whole approach is wrong; if restriction can fail *)
49 (*CSC: (as indeed it is the case), we can not collect all the restrictions *)
50 (*CSC: and restrict everything at the end ;-( *)
51 let restrict to_be_restricted =
55 | _::tl when List.mem (n,i) to_be_restricted ->
56 None::(erase (i+1) n tl)
57 | he::tl -> he::(erase (i+1) n tl) in
61 | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
65 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
66 let delift n subst context metasenv l t =
67 let module S = CicSubstitution in
68 let to_be_restricted = ref [] in
74 C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
75 (*CSC: deliftato la regola per il LetIn *)
76 (*CSC: FALSO! La regola per il LetIn non lo fa *)
78 (match List.nth context (m-k-1) with
79 Some (_,C.Def (t,_)) ->
80 (*CSC: Hmmm. This bit of reduction is not in the spirit of *)
81 (*CSC: first order unification. Does it help or does it harm? *)
82 deliftaux k (S.lift m t)
83 | Some (_,C.Decl t) ->
84 (*CSC: The following check seems to be wrong! *)
85 (*CSC: B:Set |- ?2 : Set *)
86 (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x *)
87 (*CSC: Why should I restrict ?2 over B? The instantiation *)
88 (*CSC: ?1 := A is perfectly reasonable and well-typed. *)
89 (*CSC: Thus I comment out the following two lines that *)
90 (*CSC: are the incriminated ones. *)
91 (*(* It may augment to_be_restricted *)
92 ignore (deliftaux k (S.lift m t)) ;*)
93 (*CSC: end of bug commented out *)
94 C.Rel ((position (m-k) l) + k)
95 | None -> raise RelToHiddenHypothesis)
96 | C.Var (uri,exp_named_subst) ->
97 let exp_named_subst' =
98 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
100 C.Var (uri,exp_named_subst')
101 | C.Meta (i, l1) as t ->
103 raise (MetaSubstFailure (sprintf
104 "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
108 deliftaux k (S.lift_meta l (List.assoc i subst))
113 | None::tl -> None::(deliftl (j+1) tl)
115 let l1' = (deliftl (j+1) tl) in
117 Some (deliftaux k t)::l1'
119 RelToHiddenHypothesis
121 | MetaSubstFailure _ ->
122 to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
124 let l' = deliftl 1 l1 in
127 | C.Implicit as t -> t
128 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
129 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
130 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
131 | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
132 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
133 | C.Const (uri,exp_named_subst) ->
134 let exp_named_subst' =
135 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
137 C.Const (uri,exp_named_subst')
138 | C.MutInd (uri,typeno,exp_named_subst) ->
139 let exp_named_subst' =
140 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
142 C.MutInd (uri,typeno,exp_named_subst')
143 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
144 let exp_named_subst' =
145 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
147 C.MutConstruct (uri,typeno,consno,exp_named_subst')
148 | C.MutCase (sp,i,outty,t,pl) ->
149 C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
150 List.map (deliftaux k) pl)
152 let len = List.length fl in
155 (fun (name, i, ty, bo) ->
156 (name, i, deliftaux k ty, deliftaux (k+len) bo))
161 let len = List.length fl in
164 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
167 C.CoFix (i, liftedfl)
174 (* This is the case where we fail even first order unification. *)
175 (* The reason is that our delift function is weaker than first *)
176 (* order (in the sense of alpha-conversion). See comment above *)
177 (* related to the delift function. *)
178 debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
179 raise (MetaSubstFailure (sprintf
180 "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
184 (function Some t -> CicPp.ppterm t | None -> "_")
187 res, restrict !to_be_restricted metasenv
190 (**** END OF DELIFT ****)
192 let rec unwind metasenv subst unwinded t =
193 let unwinded = ref unwinded in
194 let frozen = ref [] in
195 let rec um_aux metasenv =
196 let module C = Cic in
197 let module S = CicSubstitution in
199 C.Rel _ as t -> t,metasenv
200 | C.Var _ as t -> t,metasenv
203 S.lift_meta l (List.assoc i !unwinded), metasenv
205 if List.mem i !frozen then
206 raise (MetaSubstFailure
207 "Failed to unify due to cyclic constraints (occur check)")
209 let saved_frozen = !frozen in
210 frozen := i::!frozen ;
213 let t = List.assoc i subst in
214 let t',metasenv' = um_aux metasenv t in
216 let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
217 delift i subst canonical_context metasenv' l t'
219 unwinded := (i,t')::!unwinded ;
220 S.lift_meta l t', metasenv'
222 (* not constrained variable, i.e. free in subst*)
225 (fun t (tl,metasenv) ->
227 None -> None::tl,metasenv
229 let t',metasenv' = um_aux metasenv t in
230 (Some t')::tl, metasenv'
233 C.Meta (i,l'), metasenv'
235 frozen := saved_frozen ;
239 | C.Implicit as t -> t,metasenv
241 let te',metasenv' = um_aux metasenv te in
242 let ty',metasenv'' = um_aux metasenv' ty in
243 C.Cast (te',ty'),metasenv''
245 let s',metasenv' = um_aux metasenv s in
246 let t',metasenv'' = um_aux metasenv' t in
247 C.Prod (n, s', t'), metasenv''
248 | C.Lambda (n,s,t) ->
249 let s',metasenv' = um_aux metasenv s in
250 let t',metasenv'' = um_aux metasenv' t in
251 C.Lambda (n, s', t'), metasenv''
253 let s',metasenv' = um_aux metasenv s in
254 let t',metasenv'' = um_aux metasenv' t in
255 C.LetIn (n, s', t'), metasenv''
259 (fun t (tl,metasenv) ->
260 let t',metasenv' = um_aux metasenv t in
265 match um_aux metasenv' he with
266 (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
267 | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
269 | C.Appl _ -> assert false
270 | C.Const (uri,exp_named_subst) ->
271 let exp_named_subst', metasenv' =
273 (fun (uri,t) (tl,metasenv) ->
274 let t',metasenv' = um_aux metasenv t in
275 (uri,t')::tl, metasenv'
276 ) exp_named_subst ([],metasenv)
278 C.Const (uri,exp_named_subst'),metasenv'
279 | C.MutInd (uri,typeno,exp_named_subst) ->
280 let exp_named_subst', metasenv' =
282 (fun (uri,t) (tl,metasenv) ->
283 let t',metasenv' = um_aux metasenv t in
284 (uri,t')::tl, metasenv'
285 ) exp_named_subst ([],metasenv)
287 C.MutInd (uri,typeno,exp_named_subst'),metasenv'
288 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
289 let exp_named_subst', metasenv' =
291 (fun (uri,t) (tl,metasenv) ->
292 let t',metasenv' = um_aux metasenv t in
293 (uri,t')::tl, metasenv'
294 ) exp_named_subst ([],metasenv)
296 C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
297 | C.MutCase (sp,i,outty,t,pl) ->
298 let outty',metasenv' = um_aux metasenv outty in
299 let t',metasenv'' = um_aux metasenv' t in
300 let pl',metasenv''' =
302 (fun p (pl,metasenv) ->
303 let p',metasenv' = um_aux metasenv p in
307 C.MutCase (sp, i, outty', t', pl'),metasenv'''
309 let len = List.length fl in
310 let liftedfl,metasenv' =
312 (fun (name, i, ty, bo) (fl,metasenv) ->
313 let ty',metasenv' = um_aux metasenv ty in
314 let bo',metasenv'' = um_aux metasenv' bo in
315 (name, i, ty', bo')::fl,metasenv''
318 C.Fix (i, liftedfl),metasenv'
320 let len = List.length fl in
321 let liftedfl,metasenv' =
323 (fun (name, ty, bo) (fl,metasenv) ->
324 let ty',metasenv' = um_aux metasenv ty in
325 let bo',metasenv'' = um_aux metasenv' bo in
326 (name, ty', bo')::fl,metasenv''
329 C.CoFix (i, liftedfl),metasenv'
331 let t',metasenv' = um_aux metasenv t in
332 t',metasenv',!unwinded
334 let apply_subst subst t =
335 (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
337 let (t',_,_) = unwind metasenv [] subst t in
340 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
341 (* performs as (apply_subst subst t) until it finds an application of *)
342 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
343 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
344 (* beta-reductions are performed. *)
345 (* Hint: this function is usually called when [reductions_no] *)
346 (* eta-expansions have been performed and the head of the new *)
347 (* application has been unified with (META [meta_to_reduce]): *)
348 (* during the unwinding the eta-expansions are undone. *)
350 let rec apply_subst_context subst =
352 | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
353 | Some (n, Cic.Def (t, ty)) ->
357 | Some ty -> Some (apply_subst subst ty)
359 Some (n, Cic.Def (apply_subst subst t, ty'))
362 let rec apply_subst_reducing subst meta_to_reduce t =
364 let module C = Cic in
365 let module S = CicSubstitution in
369 | C.Meta (i,l) as t ->
371 S.lift_meta l (List.assoc i subst)
375 | C.Implicit as t -> t
376 | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
377 | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
378 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
379 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
381 let tl' = List.map um_aux tl in
384 C.Appl l -> C.Appl (l@tl')
385 | _ as he' -> C.Appl (he'::tl')
388 match meta_to_reduce,he with
389 Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
390 let rec beta_reduce =
392 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
393 let he'' = CicSubstitution.subst he' t in
397 beta_reduce (n-1,C.Appl(he''::tl'))
400 beta_reduce (reductions_no,t')
403 | C.Appl _ -> assert false
404 | C.Const (uri,exp_named_subst) ->
405 let exp_named_subst' =
406 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
408 C.Const (uri,exp_named_subst')
409 | C.MutInd (uri,typeno,exp_named_subst) ->
410 let exp_named_subst' =
411 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
413 C.MutInd (uri,typeno,exp_named_subst')
414 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
415 let exp_named_subst' =
416 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
418 C.MutConstruct (uri,typeno,consno,exp_named_subst')
419 | C.MutCase (sp,i,outty,t,pl) ->
420 C.MutCase (sp, i, um_aux outty, um_aux t,
423 let len = List.length fl in
426 (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
431 let len = List.length fl in
434 (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
437 C.CoFix (i, liftedfl)
441 let ppcontext ?(sep = "\n") subst context =
443 (List.rev_map (function
444 | Some (n, Cic.Decl t) ->
446 (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t))
447 | Some (n, Cic.Def (t, ty)) ->
448 sprintf "%s : %s := %s"
452 | Some ty -> CicPp.ppterm (apply_subst subst ty))
453 (CicPp.ppterm (apply_subst subst t))
457 let ppmetasenv ?(sep = "\n") subst metasenv =
461 sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
462 (CicPp.ppterm (apply_subst subst t)))
464 (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
467 (* UNWIND THE MGU INSIDE THE MGU *)
468 let unwind_subst metasenv subst =
470 (fun (unwinded,metasenv) (i,_) ->
471 let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
472 let identity_relocation_list =
473 CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
475 let (_,metasenv',subst') =
476 unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
479 ) ([],metasenv) subst
481 (* From now on we recreate a kernel abstraction where substitutions are part of
484 let lift metasenv subst n term =
485 (* TODO unwind's result is thrown away :-( *)
486 let (subst, _) = unwind_subst metasenv subst in
487 let term = apply_subst subst term in
489 CicSubstitution.lift n term
491 raise (MetaSubstFailure ("Lift failure: " ^
492 Printexc.to_string e))
494 let whd metasenv subst context term =
495 (* TODO unwind's result is thrown away :-( *)
496 let (subst, _) = unwind_subst metasenv subst in
497 let term = apply_subst subst term in
498 let context = apply_subst_context subst context in
500 CicReduction.whd context term
502 raise (MetaSubstFailure ("Weak head reduction failure: " ^
503 Printexc.to_string e))
505 let are_convertible metasenv subst context t1 t2 =
506 (* TODO unwind's result is thrown away :-( *)
507 let (subst, _) = unwind_subst metasenv subst in
508 let context = apply_subst_context subst context in
509 let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
510 CicReduction.are_convertible context t1 t2
512 let type_of_aux' metasenv subst context term =
513 (* TODO unwind's result is thrown away :-( *)
514 let (subst, _) = unwind_subst metasenv subst in
515 let term = apply_subst subst term in
516 let context = apply_subst_context subst context in
519 (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
521 (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
525 CicTypeChecker.type_of_aux' metasenv context term
526 with CicTypeChecker.TypeCheckerFailure msg ->
527 raise (MetaSubstFailure ("Type checker failure: " ^ msg))