4 exception AssertFailure of string
5 exception MetaSubstFailure of string
6 exception RelToHiddenHypothesis
8 let debug_print = prerr_endline
10 type substitution = (int * Cic.term) list
15 (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
20 (* the delift function takes in input an ordered list of optional terms *)
21 (* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *)
22 (* rel(k). Typically, the list of optional terms is the explicit substitution *)
23 (* that is applied to a metavariable occurrence and the result of the delift *)
24 (* function is a term the implicit variable can be substituted with to make *)
25 (* the term [t] unifiable with the metavariable occurrence. *)
26 (* In general, the problem is undecidable if we consider equivalence in place *)
27 (* of alpha convertibility. Our implementation, though, is even weaker than *)
28 (* alpha convertibility, since it replace the term [tk] if and only if [tk] *)
29 (* is a Rel (missing all the other cases). Does this matter in practice? *)
31 exception NotInTheList;;
36 [] -> raise NotInTheList
37 | (Some (Cic.Rel m))::_ when m=n -> k
38 | _::tl -> aux (k+1) tl in
42 (*CSC: this restriction function is utterly wrong, since it does not check *)
43 (*CSC: that the variable that is going to be restricted does not occur free *)
44 (*CSC: in a part of the sequent that is not going to be restricted. *)
45 (*CSC: In particular, the whole approach is wrong; if restriction can fail *)
46 (*CSC: (as indeed it is the case), we can not collect all the restrictions *)
47 (*CSC: and restrict everything at the end ;-( *)
48 let restrict to_be_restricted =
52 | _::tl when List.mem (n,i) to_be_restricted ->
53 None::(erase (i+1) n tl)
54 | he::tl -> he::(erase (i+1) n tl) in
58 | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
62 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
63 let delift context metasenv l t =
64 let module S = CicSubstitution in
65 let to_be_restricted = ref [] in
71 C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
72 (*CSC: deliftato la regola per il LetIn *)
73 (*CSC: FALSO! La regola per il LetIn non lo fa *)
75 (match List.nth context (m-k-1) with
76 Some (_,C.Def (t,_)) ->
77 (*CSC: Hmmm. This bit of reduction is not in the spirit of *)
78 (*CSC: first order unification. Does it help or does it harm? *)
79 deliftaux k (S.lift m t)
80 | Some (_,C.Decl t) ->
81 (*CSC: The following check seems to be wrong! *)
82 (*CSC: B:Set |- ?2 : Set *)
83 (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x *)
84 (*CSC: Why should I restrict ?2 over B? The instantiation *)
85 (*CSC: ?1 := A is perfectly reasonable and well-typed. *)
86 (*CSC: Thus I comment out the following two lines that *)
87 (*CSC: are the incriminated ones. *)
88 (*(* It may augment to_be_restricted *)
89 ignore (deliftaux k (S.lift m t)) ;*)
90 (*CSC: end of bug commented out *)
91 C.Rel ((position (m-k) l) + k)
92 | None -> raise RelToHiddenHypothesis)
93 | C.Var (uri,exp_named_subst) ->
94 let exp_named_subst' =
95 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
97 C.Var (uri,exp_named_subst')
98 | C.Meta (i, l1) as t ->
102 | None::tl -> None::(deliftl (j+1) tl)
104 let l1' = (deliftl (j+1) tl) in
106 Some (deliftaux k t)::l1'
108 RelToHiddenHypothesis
110 to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
112 let l' = deliftl 1 l1 in
115 | C.Implicit as t -> t
116 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
117 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
118 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
119 | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
120 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
121 | C.Const (uri,exp_named_subst) ->
122 let exp_named_subst' =
123 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
125 C.Const (uri,exp_named_subst')
126 | C.MutInd (uri,typeno,exp_named_subst) ->
127 let exp_named_subst' =
128 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
130 C.MutInd (uri,typeno,exp_named_subst')
131 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
132 let exp_named_subst' =
133 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
135 C.MutConstruct (uri,typeno,consno,exp_named_subst')
136 | C.MutCase (sp,i,outty,t,pl) ->
137 C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
138 List.map (deliftaux k) pl)
140 let len = List.length fl in
143 (fun (name, i, ty, bo) ->
144 (name, i, deliftaux k ty, deliftaux (k+len) bo))
149 let len = List.length fl in
152 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
155 C.CoFix (i, liftedfl)
162 (* This is the case where we fail even first order unification. *)
163 (* The reason is that our delift function is weaker than first *)
164 (* order (in the sense of alpha-conversion). See comment above *)
165 (* related to the delift function. *)
166 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 !!!!!!!!!!!!!!!!" ;
167 raise (MetaSubstFailure (sprintf
168 "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
172 (function Some t -> CicPp.ppterm t | None -> "_")
175 res, restrict !to_be_restricted metasenv
178 (**** END OF DELIFT ****)
180 let rec unwind metasenv subst unwinded t =
181 let unwinded = ref unwinded in
182 let frozen = ref [] in
183 let rec um_aux metasenv =
184 let module C = Cic in
185 let module S = CicSubstitution in
187 C.Rel _ as t -> t,metasenv
188 | C.Var _ as t -> t,metasenv
191 S.lift_meta l (List.assoc i !unwinded), metasenv
193 if List.mem i !frozen then
194 raise (MetaSubstFailure
195 "Failed to unify due to cyclic constraints (occur check)")
197 let saved_frozen = !frozen in
198 frozen := i::!frozen ;
201 let t = List.assoc i subst in
202 let t',metasenv' = um_aux metasenv t in
204 let (_,canonical_context,_) =
205 List.find (function (m,_,_) -> m=i) metasenv
207 delift canonical_context metasenv' l t'
209 unwinded := (i,t')::!unwinded ;
210 S.lift_meta l t', metasenv'
213 (* not constrained variable, i.e. free in subst*)
216 (fun t (tl,metasenv) ->
218 None -> None::tl,metasenv
220 let t',metasenv' = um_aux metasenv t in
221 (Some t')::tl, metasenv'
224 C.Meta (i,l'), metasenv'
226 frozen := saved_frozen ;
230 | C.Implicit as t -> t,metasenv
232 let te',metasenv' = um_aux metasenv te in
233 let ty',metasenv'' = um_aux metasenv' ty in
234 C.Cast (te',ty'),metasenv''
236 let s',metasenv' = um_aux metasenv s in
237 let t',metasenv'' = um_aux metasenv' t in
238 C.Prod (n, s', t'), metasenv''
239 | C.Lambda (n,s,t) ->
240 let s',metasenv' = um_aux metasenv s in
241 let t',metasenv'' = um_aux metasenv' t in
242 C.Lambda (n, s', t'), metasenv''
244 let s',metasenv' = um_aux metasenv s in
245 let t',metasenv'' = um_aux metasenv' t in
246 C.LetIn (n, s', t'), metasenv''
250 (fun t (tl,metasenv) ->
251 let t',metasenv' = um_aux metasenv t in
256 match um_aux metasenv' he with
257 (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
258 | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
260 | C.Appl _ -> assert false
261 | C.Const (uri,exp_named_subst) ->
262 let exp_named_subst', metasenv' =
264 (fun (uri,t) (tl,metasenv) ->
265 let t',metasenv' = um_aux metasenv t in
266 (uri,t')::tl, metasenv'
267 ) exp_named_subst ([],metasenv)
269 C.Const (uri,exp_named_subst'),metasenv'
270 | C.MutInd (uri,typeno,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.MutInd (uri,typeno,exp_named_subst'),metasenv'
279 | C.MutConstruct (uri,typeno,consno,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.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
288 | C.MutCase (sp,i,outty,t,pl) ->
289 let outty',metasenv' = um_aux metasenv outty in
290 let t',metasenv'' = um_aux metasenv' t in
291 let pl',metasenv''' =
293 (fun p (pl,metasenv) ->
294 let p',metasenv' = um_aux metasenv p in
298 C.MutCase (sp, i, outty', t', pl'),metasenv'''
300 let len = List.length fl in
301 let liftedfl,metasenv' =
303 (fun (name, i, ty, bo) (fl,metasenv) ->
304 let ty',metasenv' = um_aux metasenv ty in
305 let bo',metasenv'' = um_aux metasenv' bo in
306 (name, i, ty', bo')::fl,metasenv''
309 C.Fix (i, liftedfl),metasenv'
311 let len = List.length fl in
312 let liftedfl,metasenv' =
314 (fun (name, ty, bo) (fl,metasenv) ->
315 let ty',metasenv' = um_aux metasenv ty in
316 let bo',metasenv'' = um_aux metasenv' bo in
317 (name, ty', bo')::fl,metasenv''
320 C.CoFix (i, liftedfl),metasenv'
322 let t',metasenv' = um_aux metasenv t in
323 t',metasenv',!unwinded
325 let apply_subst subst t =
326 (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
328 let (t',_,_) = unwind metasenv [] subst t in
331 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
332 (* performs as (apply_subst subst t) until it finds an application of *)
333 (* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
334 (* a new beta-redex; in this case up to [reductions_no] consecutive *)
335 (* beta-reductions are performed. *)
336 (* Hint: this function is usually called when [reductions_no] *)
337 (* eta-expansions have been performed and the head of the new *)
338 (* application has been unified with (META [meta_to_reduce]): *)
339 (* during the unwinding the eta-expansions are undone. *)
341 let rec apply_subst_context subst =
343 | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
344 | Some (n, Cic.Def (t, ty)) ->
348 | Some ty -> Some (apply_subst subst ty)
350 Some (n, Cic.Def (apply_subst subst t, ty'))
353 let rec apply_subst_reducing subst meta_to_reduce t =
355 let module C = Cic in
356 let module S = CicSubstitution in
360 | C.Meta (i,l) as t ->
362 S.lift_meta l (List.assoc i subst)
366 | C.Implicit as t -> t
367 | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
368 | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
369 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
370 | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
372 let tl' = List.map um_aux tl in
375 C.Appl l -> C.Appl (l@tl')
376 | _ as he' -> C.Appl (he'::tl')
379 match meta_to_reduce,he with
380 Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
381 let rec beta_reduce =
383 (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
384 let he'' = CicSubstitution.subst he' t in
388 beta_reduce (n-1,C.Appl(he''::tl'))
391 beta_reduce (reductions_no,t')
394 | C.Appl _ -> assert false
395 | C.Const (uri,exp_named_subst) ->
396 let exp_named_subst' =
397 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
399 C.Const (uri,exp_named_subst')
400 | C.MutInd (uri,typeno,exp_named_subst) ->
401 let exp_named_subst' =
402 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
404 C.MutInd (uri,typeno,exp_named_subst')
405 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
406 let exp_named_subst' =
407 List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
409 C.MutConstruct (uri,typeno,consno,exp_named_subst')
410 | C.MutCase (sp,i,outty,t,pl) ->
411 C.MutCase (sp, i, um_aux outty, um_aux t,
414 let len = List.length fl in
417 (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
422 let len = List.length fl in
425 (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
428 C.CoFix (i, liftedfl)
432 let ppcontext ?(sep = "\n") subst context =
434 (List.rev_map (function
435 | Some (n, Cic.Decl t) ->
437 (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t))
438 | Some (n, Cic.Def (t, ty)) ->
439 sprintf "%s : %s := %s"
443 | Some ty -> CicPp.ppterm (apply_subst subst ty))
444 (CicPp.ppterm (apply_subst subst t))
448 let ppmetasenv ?(sep = "\n") subst metasenv =
452 sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
453 (CicPp.ppterm (apply_subst subst t)))
455 (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
458 (* UNWIND THE MGU INSIDE THE MGU *)
459 let unwind_subst metasenv subst =
461 (fun (unwinded,metasenv) (i,_) ->
462 let (_,canonical_context,_) =
463 List.find (function (m,_,_) -> m=i) metasenv
465 let identity_relocation_list =
466 CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
468 let (_,metasenv',subst') =
469 unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
472 ) ([],metasenv) subst
474 (* From now on we recreate a kernel abstraction where substitutions are part of
477 let whd subst context term =
478 let term = apply_subst subst term in
479 let context = apply_subst_context subst context in
481 CicReduction.whd context term
483 raise (MetaSubstFailure ("Weak head reduction failure: " ^
484 Printexc.to_string e))
486 let are_convertible subst context t1 t2 =
487 let context = apply_subst_context subst context in
488 let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
489 CicReduction.are_convertible context t1 t2
491 let type_of_aux' metasenv subst context term =
492 let term = apply_subst subst term in
493 let context = apply_subst_context subst context in
496 (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
498 (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
502 CicTypeChecker.type_of_aux' metasenv context term
503 with CicTypeChecker.TypeCheckerFailure msg ->
504 raise (MetaSubstFailure ("Type checker failure: " ^ msg))