| C.Sort _ as t -> t
| C.Implicit -> assert false
| C.Meta (n, l) ->
- (try
- aux k (CicSubstitution.lift_meta l (List.assoc n subst))
- with Not_found ->
- let l' =
- let i = ref 0 in
- List.map
- (function
- | None -> None
- | Some t ->
- incr i;
- try
- Some (aux k t)
- with Occur ->
- more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
- None)
- l
- in
- C.Meta (n, l'))
+ (* we do not retrieve the term associated to ?n in subst since *)
+ (* in this way we can restrict if something goes wrong *)
+ let l' =
+ let i = ref 0 in
+ List.map
+ (function t ->
+ incr i ;
+ match t with
+ None -> None
+ | Some t ->
+ try
+ Some (aux k t)
+ with Occur ->
+prerr_endline (Printf.sprintf "RESTRINGO (%d,%d)" n !i) ;
+ more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
+ None)
+ l
+ in
+ C.Meta (n, l')
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
| C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
| C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
(CicPp.ppterm s)))
- with Not_found -> (more @ more_to_be_restricted, metasenv', subst))
+ with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
with Occur ->
raise (MetaSubstFailure (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
let delift n subst context metasenv l t =
- let l =
- let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
- List.map2 (fun ct lt ->
- match (ct, lt) with
- | None, _ -> None
- | Some _, _ -> lt)
- canonical_context l
- in
let module S = CicSubstitution in
let to_be_restricted = ref [] in
let rec deliftaux k =
"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
- NotInTheList
- | MetaSubstFailure _ ->
- to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
- in
- let l' = deliftl 1 l1 in
- C.Meta(i,l'))
+ (* I do not consider the term associated to ?i in subst since *)
+ (* in this way I can restrict if something goes wrong. *)
+ 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
+ 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)