exception MetaSubstFailure of string Lazy.t
exception Uncertain of string Lazy.t
-let newmeta,maxmeta =
+let newmeta,maxmeta,pushmaxmeta,popmaxmeta =
let maxmeta = ref 0 in
+ let pushedmetas = ref [] in
(fun () -> incr maxmeta; !maxmeta),
- (fun () -> !maxmeta)
+ (fun () -> !maxmeta),
+ (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0),
+ (fun () -> match !pushedmetas with [] -> assert false | _hd::tl -> pushedmetas := tl)
;;
-exception NotInTheList;;
+exception NotFound of [`NotInTheList | `NotWellTyped];;
let position to_skip n (shift, lc) =
match lc with
- | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *)
- | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
+ | NCic.Irl len when n <= shift + to_skip || n > shift + len ->
+ raise (NotFound `NotInTheList)
| NCic.Irl _ -> n - shift
| NCic.Ctx tl ->
let rec aux to_skip k = function
- | [] -> raise NotInTheList
+ | [] -> raise (NotFound `NotInTheList)
| _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl
| (NCic.Rel m)::_ when m + shift = n -> k
| _::tl -> aux to_skip (k+1) tl
end
;;
-let rec force_does_not_occur metasenv subst restrictions t =
+let rec force_does_not_occur status metasenv subst restrictions t =
let rec aux k ms = function
| NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
| NCic.Rel r as orig ->
| NCic.Meta (n, (shift,lc as l)) as orig ->
(try
let _,_,bo,_ = NCicUtils.lookup_subst n subst in
- aux k ms (NCicSubstitution.subst_meta l bo)
+ aux k ms (NCicSubstitution.subst_meta status l bo)
with
NCicUtils.Subst_not_found _ ->
(* we ignore the subst since restrict will take care of already
* instantiated/restricted metavariabels *)
let l = NCicUtils.expand_local_context lc in
- let sl = List.map (NCicSubstitution.lift shift) l in
+ let sl = List.map (NCicSubstitution.lift status shift) l in
let (metasenv,subst as ms), _, restrictions_for_n, l' =
List.fold_right
(fun t (ms, i, restrictions_for_n, l) ->
try
(*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
- string_of_int shift ^ " t=" ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
+ string_of_int shift ^ " t=" ^ status#ppterm ~metasenv ~subst ~context:[] t));*)
let ms, t = aux k ms t in
- (*pp (lazy ("LA FOSSA: " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
+ (*pp (lazy ("LA FOSSA: " ^ status#ppterm ~metasenv ~subst ~context:[] t));*)
ms, i-1, restrictions_for_n, t::l
with Occur ->
ms, i-1, i::restrictions_for_n, l)
in
if restrictions_for_n = [] then
ms, if sl = l' then orig else (
- (*pp (lazy ("FINITO: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[]
+ (*pp (lazy ("FINITO: " ^ status#ppterm ~metasenv:[] ~subst:[]
~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
)
let l' = pack_lc (0, NCic.Ctx l') in
let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
let metasenv, subst, newmeta, more_restricted =
- restrict metasenv subst n restrictions_for_n in
+ restrict status metasenv subst n restrictions_for_n in
let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst), NCic.Meta (newmeta, l'))
- | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
+ | t -> NCicUntrusted.map_term_fold_a status (fun _ k -> k+1) k aux ms t
in
aux 0 (metasenv,subst) t
-and force_does_not_occur_in_context metasenv subst restrictions = function
+and force_does_not_occur_in_context status metasenv subst restrictions = function
| name, NCic.Decl t as orig ->
- (* pp (lazy ("CCC: hd is" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^
+ (* pp (lazy ("CCC: hd is" ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t ^
"\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
let (metasenv, subst), t' =
- force_does_not_occur metasenv subst restrictions t in
+ force_does_not_occur status metasenv subst restrictions t in
metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
| name, NCic.Def (bo, ty) as orig ->
let (metasenv, subst), bo' =
- force_does_not_occur metasenv subst restrictions bo in
+ force_does_not_occur status metasenv subst restrictions bo in
let (metasenv, subst), ty' =
- force_does_not_occur metasenv subst restrictions ty in
+ force_does_not_occur status metasenv subst restrictions ty in
metasenv, subst,
(if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))
-and erase_in_context metasenv subst pos restrictions = function
+and erase_in_context status metasenv subst pos restrictions = function
| [] -> metasenv, subst, restrictions, []
| hd::tl as orig ->
let metasenv, subst, restricted, tl' =
- erase_in_context metasenv subst (pos+1) restrictions tl in
+ erase_in_context status metasenv subst (pos+1) restrictions tl in
if List.mem pos restricted then
metasenv, subst, restricted, tl'
else
let delifted_restricted =
List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
force_does_not_occur_in_context
- metasenv subst delifted_restricted hd
+ status metasenv subst delifted_restricted hd
in
metasenv, subst, restricted,
(if hd' == hd && tl' == tl then orig else (hd' :: tl'))
with Occur ->
metasenv, subst, (pos :: restricted), tl'
-and restrict metasenv subst i (restrictions as orig) =
+and restrict status metasenv subst i (restrictions as orig) =
assert (restrictions <> []);
try
let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
try
let metasenv, subst, restrictions, newctx =
- erase_in_context metasenv subst 1 restrictions ctx in
+ erase_in_context status metasenv subst 1 restrictions ctx in
let (metasenv, subst), newty =
- force_does_not_occur metasenv subst restrictions ty in
+ force_does_not_occur status metasenv subst restrictions ty in
let (metasenv, subst), newbo =
- force_does_not_occur metasenv subst restrictions bo in
+ force_does_not_occur status metasenv subst restrictions bo in
let j = newmeta () in
let subst_entry_j = j, (name, newctx, newbo, newty) in
let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in
"with %s and at least one of the hypotheses occurs in "^^
"the substituted term") i (String.concat ", "
(List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
- (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))
+ (status#ppterm ~metasenv ~subst ~context:ctx bo))))
with NCicUtils.Subst_not_found _ ->
try
let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
try
let metasenv, subst, restrictions, newctx =
- erase_in_context metasenv subst 1 restrictions ctx in
+ erase_in_context status metasenv subst 1 restrictions ctx in
let (metasenv, subst), newty =
- force_does_not_occur metasenv subst restrictions ty in
+ force_does_not_occur status metasenv subst restrictions ty in
let j = newmeta () in
let metasenv_entry = j, (name, newctx, newty) in
let reloc_irl =
| NCicUtils.Meta_not_found _ -> assert false
;;
-let rec flexible_arg context subst = function
- | NCic.Meta (i,_) ->
+let rec is_flexible status context ~subst = function
+ | NCic.Meta (i,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta status lc t in
+ is_flexible status context ~subst t
+ with NCicUtils.Subst_not_found _ -> true)
+ | NCic.Appl (NCic.Meta (i,lc) :: args)->
(try
- let _,_,t,_ = List.assoc i subst in
- flexible_arg context subst t
- with Not_found -> true)
- | NCic.Appl (NCic.Meta (i,_) :: args)->
- (try
- let _,_,t,_ = List.assoc i subst in
- flexible_arg context subst
- (NCicReduction.head_beta_reduce ~delta:max_int
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta status lc t in
+ is_flexible status context ~subst
+ (NCicReduction.head_beta_reduce status ~delta:max_int
(NCic.Appl (t :: args)))
- with Not_found -> true)
+ with NCicUtils.Subst_not_found _ -> true)
(* this is a cheap whd, it only performs zeta-reduction.
*
* it works when the **omissis** disambiguation algorithm
match List.nth context (i-1)
with
| _,NCic.Def (bo,_) ->
- flexible_arg context subst
- (NCicSubstitution.lift i bo)
+ is_flexible status context ~subst
+ (NCicSubstitution.lift status i bo)
| _ -> false
with
| Failure _ ->
prerr_endline (Printf.sprintf "Rel %d inside context:\n%s" i
- (NCicPp.ppcontext ~subst ~metasenv:[] context));
+ (status#ppcontext ~subst ~metasenv:[] context));
assert false
| Invalid_argument _ -> assert false)
| _ -> false
exception Found;;
+exception TypeNotGood;;
(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
otherwise the occur check does not make sense in case of unification
of ?n with ?n *)
-let delift ~unify metasenv subst context n l t =
+let delift status ~unify metasenv subst context n l t =
(*D*) inside 'D'; try let rc =
let is_in_scope_meta subst = function
| NCic.Meta (i,_) ->
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
- if flexible_arg context subst t || contains_in_scope subst t then None else
+ if is_flexible status context ~subst t || contains_in_scope subst t then None else
let lb =
List.map (fun t ->
- let t = NCicSubstitution.lift (k+shift) t in
- t, flexible_arg context subst t)
+ let t = NCicSubstitution.lift status (k+shift) t in
+ t, is_flexible status context ~subst t)
l
in
HExtlib.list_findopt
lb
in
let rec aux (context,k,in_scope) (metasenv, subst as ms) t =
- (* XXX if t is closed, we should just terminate. Speeds up hints! *)
- if NCicUntrusted.looks_closed t then ms, t
- else
match unify_list in_scope metasenv subst context k t with
| Some x -> x
| None ->
match List.nth context (n-1) with
| _,NCic.Def (bo,_) ->
(try ms, NCic.Rel ((position in_scope (n-k) l) + k)
- with NotInTheList ->
+ with (NotFound `NotInTheList) ->
(* CSC: This bit of reduction hurts performances since it is
* possible to have an exponential explosion of the size of the
* proof. required for nat/nth_prime.ma *)
- aux (context,k,in_scope) ms (NCicSubstitution.lift n bo))
+ aux (context,k,in_scope) ms (NCicSubstitution.lift status n bo))
| _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k)
with Failure _ -> assert false) (*Unbound variable found in delift*)
| NCic.Meta (i,_) when i=n ->
"Cannot unify the metavariable ?%d with a term that has "^^
"as subterm %s in which the same metavariable "^^
"occurs (occur check)") i
- (NCicPp.ppterm ~context ~metasenv ~subst t))))
+ (status#ppterm ~context ~metasenv ~subst t))))
| NCic.Meta (i,l1) as orig ->
(try
let tag,c,t,ty = NCicUtils.lookup_subst i subst in
metasenv,
(i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
in
- aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
+ aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
with NCicUtils.Subst_not_found _ ->
if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
else
when shift1 + len1 < shift || shift1 > shift + len ->
let restrictions = HExtlib.list_seq 1 (len1 + 1) in
let metasenv, subst, newmeta, more_restricted =
- restrict metasenv subst i restrictions in
+ restrict status metasenv subst i restrictions in
let l' = (0,NCic.Irl (max 0 (k-shift1))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst),NCic.Meta (newmeta,l')
else ms, NCic.Meta (i, (new_shift, lc1))
else
let metasenv, subst, newmeta, more_restricted =
- restrict metasenv subst i restrictions in
+ restrict status metasenv subst i restrictions in
let newlc_len = len1 - List.length restrictions in
let l' = new_shift, NCic.Irl newlc_len in
let l' = purge_restricted restrictions more_restricted l' in
| _ ->
let lc1 = NCicUtils.expand_local_context lc1 in
- let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in
+ let lc1 = List.map (NCicSubstitution.lift status shift1) lc1 in
let rec deliftl tbr j ms = function
| [] -> ms, tbr, []
| t::tl ->
let ms, t = aux (context,k,in_scope) ms t in
ms, tbr, t::tl
with
- | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
+ | (NotFound `NotInTheList) | MetaSubstFailure _ -> ms, j::tbr, tl
in
let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
pp (lazy ("TO BE RESTRICTED: " ^
(String.concat "," (List.map string_of_int to_be_r))));
let l1 = pack_lc (0, NCic.Ctx lc1') in
- pp (lazy ("newmeta:" ^ NCicPp.ppterm
+ pp (lazy ("newmeta:" ^ status#ppterm
~metasenv ~subst ~context (NCic.Meta (999,l1))));
- pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
+ pp (lazy (status#ppmetasenv ~subst metasenv));
if to_be_r = [] then
(metasenv, subst),
(if lc1' = lc1 then orig else NCic.Meta (i,l1))
else
let metasenv, subst, newmeta, more_restricted =
- restrict metasenv subst i to_be_r in
+ restrict status metasenv subst i to_be_r in
let l1 = purge_restricted to_be_r more_restricted l1 in
(metasenv, subst), NCic.Meta(newmeta,l1))
| t ->
- NCicUntrusted.map_term_fold_a
+ NCicUntrusted.map_term_fold_a status
(fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
in
(*
prerr_endline (
- "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
- String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) (
+ "DELIFTO " ^ status#ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
+ status#ppterm ~metasenv ~subst ~context (NCic.Meta(n,l)) ^ " i.e. " ^
+ String.concat ", " (List.map (status#ppterm ~metasenv ~subst ~context) (
let shift, lc = l in
- (List.map (NCicSubstitution.lift shift)
+ (List.map (NCicSubstitution.lift status shift)
(NCicUtils.expand_local_context lc))
)));
*)
- try aux (context,0,0) (metasenv,subst) t
- with NotInTheList ->
+ try
+(*assert (try n = -1 or (ignore(NCicUtils.lookup_meta n metasenv); true) with NCicUtils.Meta_not_found _ -> false);*)
+ let ((metasenv,subst),t) as res = aux (context,0,0) (metasenv,subst) t in
+ if (try n <> -1 && (ignore(NCicUtils.lookup_meta n metasenv); false)
+ with NCicUtils.Meta_not_found _ -> true)
+ then
+ let _,context,bo,_ = NCicUtils.lookup_subst n subst in
+ match unify metasenv subst context bo t with
+ None -> raise (NotFound `NotWellTyped)
+ | Some (metasenv,subst) -> (metasenv,subst),t
+ else
+ (try
+ let _,context,ty = NCicUtils.lookup_meta n metasenv in
+ let ty' =
+ match t with
+ NCic.Sort _ -> (* could be algebraic *) NCic.Implicit `Closed
+ | _ -> NCicTypeChecker.typeof status ~subst ~metasenv context t in
+ (match ty,ty' with
+ NCic.Implicit _,_ ->
+ (match ty' with
+ NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+ | _ -> raise TypeNotGood)
+ | _,NCic.Implicit _ ->
+ (match ty with
+ NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+ | _ -> raise TypeNotGood)
+ | _ ->
+ if
+ NCicReduction.are_convertible status ~metasenv ~subst context ty' ty
+ then
+ res
+ else
+ raise TypeNotGood)
+ with
+ NCicUtils.Meta_not_found _ ->
+ (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
+ assert (n = -1); res
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ HLog.error "----------- Problem with Dependent Types ----------";
+ HLog.error (Lazy.force msg) ;
+ HLog.error "---------------------------------------------------";
+ raise (NotFound `NotWellTyped)
+ | TypeNotGood
+ | NCicTypeChecker.AssertFailure _
+ | NCicReduction.AssertFailure _ ->
+ raise (NotFound `NotWellTyped))
+ with NotFound reason ->
(* This is the case where we fail even first order unification. *)
(* The reason is that our delift function is weaker than first *)
(* order (in the sense of alpha-conversion). See comment above *)
(* related to the delift function. *)
+ let reason =
+ match reason with
+ `NotInTheList -> "some variable cannot be delifted"
+ | `NotWellTyped -> "the unifier found is not well typed" in
let msg = (lazy (Printf.sprintf
- ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
- "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst
- ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv
+ ("Error trying to abstract %s over [%s]: %s")
+ (status#ppterm ~metasenv ~subst
+ ~context t) (String.concat "; " (List.map (status#ppterm ~metasenv
~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
- shift) (NCicUtils.expand_local_context lc))))))
+ status shift) (NCicUtils.expand_local_context lc)))) reason))
in
let shift, lc = l in
let lc = NCicUtils.expand_local_context lc in
- let l = List.map (NCicSubstitution.lift shift) lc in
+ let l = List.map (NCicSubstitution.lift status shift) lc in
if
- List.exists (fun t-> NCicUntrusted.metas_of_term subst context t <> [])l
+ List.exists (fun t-> NCicUntrusted.metas_of_term status subst context t <> [])l
then
raise (Uncertain msg)
else
with NCicUtils.Meta_not_found _ -> assert false
;;
-let saturate ?(delta=0) metasenv subst context ty goal_arity =
+let saturate status ?(delta=0) metasenv subst context ty goal_arity =
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
let metasenv1, _, arg,_ =
mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
let t, metasenv1, args, pno =
- aux metasenv1 (NCicSubstitution.subst arg t)
+ aux metasenv1 (NCicSubstitution.subst status arg t)
in
if pno + 1 = goal_arity then
ty, metasenv, [], goal_arity+1
else
t, metasenv1, arg::args, pno+1
| ty ->
- match NCicReduction.whd ~subst context ty ~delta with
+ match NCicReduction.whd status ~subst context ty ~delta with
| NCic.Prod _ as ty -> aux metasenv ty
| ty -> ty, metasenv, [], 0
in
projects / helm.git / blobdiff