X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=0207c9231e058b15d5ab820d21b0bf1719ca2cca;hb=47a745462a714af9d65cea7b61af56524bd98fa1;hp=b18364509db79f282b7d18372bee0d2cd189f87c;hpb=2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd;p=helm.git diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml index b18364509..0207c9231 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 @@ -117,7 +120,7 @@ let purge_restricted restrictions more_restrictions l = 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 -> @@ -128,21 +131,21 @@ let rec force_does_not_occur metasenv subst restrictions t = | 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) @@ -150,7 +153,7 @@ let rec force_does_not_occur metasenv subst restrictions t = 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')) ) @@ -158,34 +161,34 @@ let rec force_does_not_occur metasenv subst restrictions t = 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 @@ -194,24 +197,24 @@ and erase_in_context metasenv subst pos restrictions = function 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 @@ -228,15 +231,15 @@ and restrict metasenv subst i (restrictions as orig) = "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 = @@ -259,19 +262,21 @@ and restrict metasenv subst i (restrictions as orig) = | NCicUtils.Meta_not_found _ -> assert false ;; -let rec is_flexible 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 - is_flexible context ~subst t - with Not_found -> true) - | NCic.Appl (NCic.Meta (i,_) :: args)-> - (try - let _,_,t,_ = List.assoc i subst in - is_flexible 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 @@ -283,13 +288,13 @@ let rec is_flexible context ~subst = function match List.nth context (i-1) with | _,NCic.Def (bo,_) -> - is_flexible 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 @@ -303,11 +308,12 @@ 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 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,_) -> @@ -332,11 +338,11 @@ let delift ~unify metasenv subst context n l t = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> - if is_flexible 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, is_flexible context ~subst t) + let t = NCicSubstitution.lift status (k+shift) t in + t, is_flexible status context ~subst t) l in HExtlib.list_findopt @@ -359,11 +365,11 @@ let delift ~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 *) - 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 -> @@ -371,7 +377,7 @@ let delift ~unify metasenv subst context n l t = "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 @@ -386,7 +392,7 @@ let delift ~unify metasenv subst context n l t = 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 @@ -398,7 +404,7 @@ let delift ~unify metasenv subst context n l t = 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') @@ -426,7 +432,7 @@ let delift ~unify metasenv subst context n l t = 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 @@ -434,7 +440,7 @@ let delift ~unify metasenv subst context n l t = | _ -> 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 -> @@ -443,55 +449,106 @@ let delift ~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: " ^ (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 _ + | NCicTypeChecker.TypeCheckerFailure _ -> + 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 @@ -526,21 +583,21 @@ let extend_meta metasenv n = 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