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 NotFound of [`NotInTheList | `NotWellTyped];;
let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
let new_subst =
subst_entry_j :: List.map
- (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
+ (fun ((n,_) as orig) -> if i = n then subst_entry_i else orig) subst
in
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
metasenv, new_subst, j, diff
pp (lazy ("BBB: dopo metasenv\n" ^ NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
List.map
- (fun (n,_) as orig -> if i = n then metasenv_entry else orig)
+ (fun ((n,_) as orig) -> if i = n then metasenv_entry else orig)
metasenv,
subst_entry :: subst, j, diff
with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
;;
let rec is_flexible status context ~subst = function
- | NCic.Meta (i,_) ->
+ | 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
- is_flexible status context ~subst t
- with Not_found -> true)
- | NCic.Appl (NCic.Meta (i,_) :: args)->
- (try
- let _,_,t,_ = List.assoc i subst in
+ 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
if not clear then ms
else
metasenv,
- (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
+ (i,([],c,t,ty)) :: List.filter (fun (j,_) -> i <> j) subst
in
aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
with NCicUtils.Subst_not_found _ ->
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 _
- | NCicTypeChecker.TypeCheckerFailure _ ->
+ | NCicReduction.AssertFailure _ ->
raise (NotFound `NotWellTyped))
with NotFound reason ->
(* This is the case where we fail even first order unification. *)
| NCic.Implicit (`Typeof _) ->
let mk_meta context kind =
let metasenv, _, ty, _ = mk_meta metasenv context kind in
- (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
+ (n, (attrs, cc, ty)) :: List.filter (fun (x,_) -> x <> n) metasenv, ty
in
(match NCicUntrusted.kind_of_meta attrs with
| `IsSort