exception AssertFailure of string
exception MetaSubstFailure of string
-exception RelToHiddenHypothesis
+
+exception RelToHiddenHypothesis (* TODO remove this exception *)
let debug_print = prerr_endline
subst)
(**** DELIFT ****)
-
-(* the delift function takes in input an ordered list of optional terms *)
-(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *)
-(* rel(k). Typically, the list of optional terms is the explicit substitution *)
-(* that is applied to a metavariable occurrence and the result of the delift *)
-(* function is a term the implicit variable can be substituted with to make *)
-(* the term [t] unifiable with the metavariable occurrence. *)
-(* In general, the problem is undecidable if we consider equivalence in place *)
-(* of alpha convertibility. Our implementation, though, is even weaker than *)
-(* alpha convertibility, since it replace the term [tk] if and only if [tk] *)
-(* is a Rel (missing all the other cases). Does this matter in practice? *)
+(* the delift function takes in input a metavariable index, an ordered list of
+ * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
+ * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit
+ * substitution that is applied to a metavariable occurrence and the result of
+ * the delift function is a term the implicit variable can be substituted with
+ * to make the term [t] unifiable with the metavariable occurrence. In general,
+ * the problem is undecidable if we consider equivalence in place of alpha
+ * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
+ * (missing all the other cases). Does this matter in practice?
+ * The metavariable index is the index of the metavariable that must not occur
+ * in the term (for occur check).
+ *)
exception NotInTheList;;
;;
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
-let delift context metasenv l t =
+let delift n subst context metasenv l t =
let module S = CicSubstitution in
let to_be_restricted = ref [] in
let rec deliftaux k =
in
C.Var (uri,exp_named_subst')
| C.Meta (i, l1) as t ->
- let rec deliftl j =
- function
- [] -> []
- | None::tl -> None::(deliftl (j+1) tl)
- | (Some t)::tl ->
- let l1' = (deliftl (j+1) tl) in
- try
- Some (deliftaux k t)::l1'
- with
- RelToHiddenHypothesis
- | NotInTheList ->
- to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
- in
- let l' = deliftl 1 l1 in
- C.Meta(i,l')
+ if i = n then
+ raise (MetaSubstFailure (sprintf
+ "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
+ i (CicPp.ppterm t)))
+ else
+ (try
+ deliftaux k (S.lift_meta l (List.assoc i subst))
+ with Not_found ->
+ let rec deliftl j =
+ function
+ [] -> []
+ | None::tl -> None::(deliftl (j+1) tl)
+ | (Some t)::tl ->
+ let l1' = (deliftl (j+1) tl) in
+ try
+ Some (deliftaux k t)::l1'
+ with
+ RelToHiddenHypothesis
+ | NotInTheList
+ | MetaSubstFailure _ ->
+ to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+ in
+ let l' = deliftl 1 l1 in
+ C.Meta(i,l'))
| C.Sort _ as t -> t
| C.Implicit as t -> t
| C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
let t = List.assoc i subst in
let t',metasenv' = um_aux metasenv t in
let _,metasenv'' =
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> m=i) metasenv
- in
- delift canonical_context metasenv' l t'
+ let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
+ delift i subst canonical_context metasenv' l t'
in
unwinded := (i,t')::!unwinded ;
S.lift_meta l t', metasenv'
- with
- Not_found ->
+ with Not_found ->
(* not constrained variable, i.e. free in subst*)
let l',metasenv' =
List.fold_right
let unwind_subst metasenv subst =
List.fold_left
(fun (unwinded,metasenv) (i,_) ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> m=i) metasenv
- in
+ let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
let identity_relocation_list =
CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
in
(* From now on we recreate a kernel abstraction where substitutions are part of
* the calculus *)
-let whd subst context term =
+let whd metasenv subst context term =
+ (* TODO unwind's result is thrown away :-( *)
+ let (subst, _) = unwind_subst metasenv subst in
let term = apply_subst subst term in
let context = apply_subst_context subst context in
try
raise (MetaSubstFailure ("Weak head reduction failure: " ^
Printexc.to_string e))
-let are_convertible subst context t1 t2 =
+let are_convertible metasenv subst context t1 t2 =
+ (* TODO unwind's result is thrown away :-( *)
+ let (subst, _) = unwind_subst metasenv subst in
let context = apply_subst_context subst context in
let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
CicReduction.are_convertible context t1 t2
let type_of_aux' metasenv subst context term =
+ (* TODO unwind's result is thrown away :-( *)
+ let (subst, _) = unwind_subst metasenv subst in
let term = apply_subst subst term in
let context = apply_subst_context subst context in
let metasenv =
projects / helm.git / blobdiff