X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=d51ce368582efc41e1084bb84e780ad4bd7d041c;hb=HEAD;hp=03f4affdf64dd672ff82996b8dd26e944317f21c;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml index 03f4affdf..d51ce3685 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.ml +++ b/matita/components/ng_refiner/nCicMetaSubst.ml @@ -47,22 +47,25 @@ let outside exc_opt = 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 @@ -218,7 +221,7 @@ and restrict status metasenv subst i (restrictions as orig) = 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 @@ -247,7 +250,7 @@ and restrict status metasenv subst i (restrictions as orig) = 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 @@ -260,18 +263,20 @@ and restrict status metasenv subst i (restrictions as orig) = ;; 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 @@ -303,6 +308,7 @@ let int_of_out_scope_tag tag = 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 @@ -359,7 +365,7 @@ let delift status ~unify metasenv subst context n l t = 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 *) @@ -384,7 +390,7 @@ let delift status ~unify metasenv subst context n l t = 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 _ -> @@ -443,7 +449,7 @@ let delift status ~unify metasenv subst context n l t = 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: " ^ @@ -467,25 +473,75 @@ let delift status ~unify metasenv subst context n l 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") (status#ppterm ~metasenv ~subst + ("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 - status 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 @@ -516,7 +572,7 @@ let extend_meta metasenv n = | 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