X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=6deaaf572b7914f9ad3edba29b1a937b4bc1a711;hb=106db6ec639e23ab8af56a1d889b3670fa292d6f;hp=2c23af050239065351c854f9c43cfc1651d64990;hpb=4a72a8de2b78b7ab0d200a4bf2f197d9ce2f2a13;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 2c23af050..6deaaf572 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -14,155 +14,27 @@ exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t -(* -(*** Functions to apply a substitution ***) - -let apply_subst_gen ~appl_fun subst term = - let rec um_aux = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Meta (i, l) -> - (try - let (_, t,_) = lookup_subst i subst in - um_aux (S.subst_meta l t) - with CicUtil.Subst_not_found _ -> - (* unconstrained variable, i.e. free in subst*) - let l' = - List.map (function None -> None | Some t -> Some (um_aux t)) l - in - C.Meta (i,l')) - | C.Sort _ - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) - | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t) - | C.Appl (hd :: tl) -> appl_fun um_aux hd tl - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - let pl' = List.map um_aux pl in - C.MutCase (sp, i, um_aux outty, um_aux t, pl') - | C.Fix (i, fl) -> - let fl' = - List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i, fl) -> - let fl' = - List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl - in - C.CoFix (i, fl') - in - um_aux term -;; - -let apply_subst = - let appl_fun um_aux he tl = - let tl' = List.map um_aux tl in - let t' = - match um_aux he with - Cic.Appl l -> Cic.Appl (l@tl') - | he' -> Cic.Appl (he'::tl') - in - begin - match he with - Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' - | _ -> t' - end - in - fun subst t -> -(* incr apply_subst_counter; *) -match subst with - [] -> t - | _ -> apply_subst_gen ~appl_fun subst t -;; - -let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" -let apply_subst s t = - profiler.HExtlib.profile (apply_subst s) t - - -let apply_subst_context subst context = - match subst with - [] -> context - | _ -> -(* - incr apply_subst_context_counter; - context_length := !context_length + List.length context; -*) - List.fold_right - (fun item context -> - match item with - | Some (n, Cic.Decl t) -> - let t' = apply_subst subst t in - Some (n, Cic.Decl t') :: context - | Some (n, Cic.Def (t, ty)) -> - let ty' = apply_subst subst ty in - let t' = apply_subst subst t in - Some (n, Cic.Def (t', ty')) :: context - | None -> None :: context) - context [] - -let apply_subst_metasenv subst metasenv = -(* - incr apply_subst_metasenv_counter; - metasenv_length := !metasenv_length + List.length metasenv; -*) -match subst with - [] -> metasenv - | _ -> - List.map - (fun (n, context, ty) -> - (n, apply_subst_context subst context, apply_subst subst ty)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv) - -let tempi_type_of_aux_subst = ref 0.0;; -let tempi_subst = ref 0.0;; -let tempi_type_of_aux = ref 0.0;; -*) - -let newmeta = +let newmeta,maxmeta = let maxmeta = ref 0 in - fun () -> incr maxmeta; !maxmeta + (fun () -> incr maxmeta; !maxmeta), + (fun () -> !maxmeta) ;; exception NotInTheList;; -let position n (shift, lc) = +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 _ -> n - shift | NCic.Ctx tl -> - let rec aux k = function + let rec aux to_skip k = function | [] -> raise NotInTheList + | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl | (NCic.Rel m)::_ when m + shift = n -> k - | _::tl -> aux (k+1) tl + | _::tl -> aux to_skip (k+1) tl in - aux 1 tl + aux to_skip 1 tl ;; let pack_lc orig = @@ -200,31 +72,41 @@ let rec force_does_not_occur metasenv subst restrictions t = in if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig | NCic.Meta (n, (shift,lc as l)) as orig -> - (* we ignore the subst since restrict will take care of already - * instantiated/restricted metavariabels *) - let (metasenv,subst as ms), restrictions_for_n, l' = - let l = NCicUtils.expand_local_context lc in - - let ms, _, restrictions_for_n, l = - List.fold_right - (fun t (ms, i, restrictions_for_n, l) -> - try - let ms, t = aux (k-shift) ms t in - ms, i-1, restrictions_for_n, t::l - with Occur -> - ms, i-1, i::restrictions_for_n, l) - l (ms, List.length l, [], []) - in - - ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) + let meta_chain = + try + Some (NCicUtils.lookup_subst n subst) + with + NCicUtils.Subst_not_found _ -> None in - if restrictions_for_n = [] then - ms, if l = l' then orig else NCic.Meta (n, l') - else - let metasenv, subst, newmeta = - restrict metasenv subst n restrictions_for_n - in - (metasenv, subst), NCic.Meta (newmeta, l') + (match meta_chain with + Some (_,_,bo,_) -> + aux k ms (NCicSubstitution.subst_meta l bo) + | None -> + (* we ignore the subst since restrict will take care of already + * instantiated/restricted metavariabels *) + let (metasenv,subst as ms), restrictions_for_n, l' = + let l = NCicUtils.expand_local_context lc in + + let ms, _, restrictions_for_n, l = + List.fold_right + (fun t (ms, i, restrictions_for_n, l) -> + try + let ms, t = aux (k-shift) ms t in + ms, i-1, restrictions_for_n, t::l + with Occur -> + ms, i-1, i::restrictions_for_n, l) + l (ms, List.length l, [], []) + in + + ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) + in + if restrictions_for_n = [] then + ms, if l = l' then orig else NCic.Meta (n, l') + else + let metasenv, subst, newmeta = + restrict metasenv subst n restrictions_for_n + in + (metasenv, subst), NCic.Meta (newmeta, l')) | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in aux 0 (metasenv,subst) t @@ -324,37 +206,135 @@ and restrict metasenv subst i restrictions = | NCicUtils.Meta_not_found _ -> assert false ;; +let rec flexible_arg context subst = function + | NCic.Meta (i,_) -> + (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 + (NCic.Appl (t :: args))) + with Not_found -> true) + (* this is a cheap whd, it only performs zeta-reduction. + * + * it works when the **omissis** disambiguation algorithm + * is run on `let x := K a b in t`, K is substituted for a + * ? and thus in t metavariables have a flexible Rel + *) + | NCic.Rel i -> + (try + match List.nth context (i-1) + with + | _,NCic.Def (bo,_) -> + flexible_arg context subst + (NCicSubstitution.lift i bo) + | _ -> false + with + | Failure _ -> + prerr_endline (Printf.sprintf "Rel %d inside context:\n%s" i + (NCicPp.ppcontext ~subst ~metasenv:[] context)); + assert false + | Invalid_argument _ -> assert false) + | _ -> false +;; + +let is_out_scope = function `OutScope _ -> true | _ -> false;; +let is_out_scope_tag = List.exists is_out_scope;; +let int_of_out_scope_tag tag = + match List.filter is_out_scope tag with [`OutScope n] -> n | _ -> assert false +;; + + +exception Found;; + (* 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 metasenv subst context n l t = - let rec aux k (metasenv, subst as ms) = function +let delift ~unify metasenv subst context n l t = + let is_in_scope_meta subst = function + | NCic.Meta (i,_) -> + (try + let tag, _, _, _ = NCicUtils.lookup_subst i subst in + List.mem `InScope tag + with NCicUtils.Subst_not_found _ -> false) + | _ -> false + in + let contains_in_scope subst t = + let rec aux _ () = function + | NCic.Meta _ as t -> + if is_in_scope_meta subst t then raise Found + else () + | t -> + if is_in_scope_meta subst t then raise Found + else NCicUtils.fold (fun _ () -> ()) () aux () t + in + try aux () () t; false with Found -> true + in + let unify_list in_scope = + 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 + let lb = + List.map (fun t -> + let t = NCicSubstitution.lift (k+shift) t in + t, flexible_arg context subst t) + l + in + HExtlib.list_findopt + (fun (li,flexible) i -> + if flexible || i < in_scope then None else + match unify metasenv subst context li t with + | Some (metasenv,subst) -> + Some ((metasenv, subst), NCic.Rel (i+1+k)) + | None -> None) + lb + in + let rec aux (context,k,in_scope) (metasenv, subst as ms) t = + match unify_list in_scope metasenv subst context k t with + | Some x -> x + | None -> + match t with | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> (try - match List.nth context (n-k-1) with + match List.nth context (n-1) with | _,NCic.Def (bo,_) -> - (try ms, NCic.Rel ((position (n-k) l) + k) + (try ms, NCic.Rel ((position in_scope (n-k) l) + k) with 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 k ms (NCicSubstitution.lift n bo)) - | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k) + aux (context,k,in_scope) ms (NCicSubstitution.lift 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 (_,(_,(NCic.Irl 0| NCic.Ctx []))) as orig -> ms, orig + | NCic.Meta (i,_) when i=n -> + raise (MetaSubstFailure (lazy (Printf.sprintf ( + "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)))) | NCic.Meta (i,l1) as orig -> (try - let _,_,t,_ = NCicUtils.lookup_subst i subst in - aux k ms (NCicSubstitution.subst_meta l1 t) + let tag,c,t,ty = NCicUtils.lookup_subst i subst in + let in_scope, clear = + if List.mem `InScope tag then 0, true + else if is_out_scope_tag tag then int_of_out_scope_tag tag,true + else in_scope, false + in + let ms = + if not clear then ms + else + metasenv, + (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst + in + aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> - (* see the top level invariant *) - if (i = n) then - raise (MetaSubstFailure (lazy (Printf.sprintf ( - "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)))) + if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig else let shift1,lc1 = l1 in let shift,lc = l in @@ -421,7 +401,7 @@ let delift metasenv subst context n l t = | t::tl -> let ms, tbr, tl = deliftl tbr (j+1) ms tl in try - let ms, t = aux k ms t in + let ms, t = aux (context,k,in_scope) ms t in ms, tbr, t::tl with | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl @@ -444,9 +424,20 @@ let delift metasenv subst context n l t = restrict metasenv subst i to_be_r in (metasenv, subst), NCic.Meta(newmeta,l1)) - | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t + | t -> + NCicUntrusted.map_term_fold_a + (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t in - try aux 0 (metasenv,subst) t +(* + prerr_endline ( + "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^ + String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) ( + let shift, lc = l in + (List.map (NCicSubstitution.lift shift) + (NCicUtils.expand_local_context lc)) + ))); +*) + try aux (context,0,0) (metasenv,subst) t with NotInTheList -> (* This is the case where we fail even first order unification. *) (* The reason is that our delift function is weaker than first *) @@ -463,46 +454,46 @@ let delift metasenv subst context n l t = let lc = NCicUtils.expand_local_context lc in let l = List.map (NCicSubstitution.lift shift) lc in if - List.exists - (fun t -> - NCicUntrusted.metas_of_term subst context t = []) - l + List.exists (fun t-> NCicUntrusted.metas_of_term subst context t <> [])l then raise (Uncertain msg) else raise (MetaSubstFailure msg) ;; -let mk_meta ?name metasenv context ty = - match ty with - | `Typeless -> - let n = newmeta () in - let ty = NCic.Implicit (`Typeof n) in - let menv_entry = (n, (name, context, ty)) in - menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty - | `Type - | `Term -> - let context_for_ty = if ty = `Type then [] else context in - let n = newmeta () in - let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in - let m = newmeta () in - let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in - let menv_entry = (m, (name, context, ty)) in - menv_entry :: ty_menv_entry :: metasenv, - NCic.Meta (m, (0,NCic.Irl (List.length context))), ty - | `WithType ty -> - let n = newmeta () in - let len = List.length context in - let menv_entry = (n, (name, context, ty)) in - menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty +let mk_meta ?(attrs=[]) metasenv context ?with_type kind = + assert(kind <> `IsSort || context = []); + let n = newmeta () in + let ty= match with_type with None-> NCic.Implicit (`Typeof n)| Some x ->x in + let len = List.length context in + let attrs = NCicUntrusted.set_kind kind attrs in + let menv_entry = (n, (attrs, context, ty)) in + menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty +;; + +let extend_meta metasenv n = + try + let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in + (match ty with + | 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 + in + (match NCicUntrusted.kind_of_meta attrs with + | `IsSort + | `IsType -> mk_meta [] `IsSort + | `IsTerm -> mk_meta cc `IsType) + | ty -> metasenv, ty) + with NCicUtils.Meta_not_found _ -> assert false ;; -let saturate ?(delta=0) metasenv context ty goal_arity = +let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function - | NCic.Prod (name,s,t) -> - let metasenv1, arg,_ = - mk_meta ~name:name metasenv context (`WithType s) in + | 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) in @@ -511,7 +502,7 @@ let saturate ?(delta=0) metasenv context ty goal_arity = else t, metasenv1, arg::args, pno+1 | ty -> - match NCicReduction.whd context ty ~delta with + match NCicReduction.whd ~subst context ty ~delta with | NCic.Prod _ as ty -> aux metasenv ty | ty -> ty, metasenv, [], 0 in