From 27bce1d83422883b6415862ec92e75baf4f87186 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Sep 2008 16:26:08 +0000 Subject: [PATCH] snapshot --- .../components/ng_refiner/nCicMetaSubst.ml | 484 ++++++++---------- .../components/ng_refiner/nCicMetaSubst.mli | 81 +-- 2 files changed, 222 insertions(+), 343 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 4441fa169..57a1b7be7 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -11,151 +11,10 @@ (* $Id$ *) - -(*open Printf - -(* PROFILING *) -(* -let deref_counter = ref 0 -let apply_subst_context_counter = ref 0 -let apply_subst_metasenv_counter = ref 0 -let lift_counter = ref 0 -let subst_counter = ref 0 -let whd_counter = ref 0 -let are_convertible_counter = ref 0 -let metasenv_length = ref 0 -let context_length = ref 0 -let reset_counters () = - apply_subst_counter := 0; - apply_subst_context_counter := 0; - apply_subst_metasenv_counter := 0; - lift_counter := 0; - subst_counter := 0; - whd_counter := 0; - are_convertible_counter := 0; - metasenv_length := 0; - context_length := 0 -let print_counters () = - debug_print (lazy (Printf.sprintf -"apply_subst: %d -apply_subst_context: %d -apply_subst_metasenv: %d -lift: %d -subst: %d -whd: %d -are_convertible: %d -metasenv length: %d (avg = %.2f) -context length: %d (avg = %.2f) -" - !apply_subst_counter !apply_subst_context_counter - !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter - !are_convertible_counter !metasenv_length - ((float !metasenv_length) /. (float !apply_subst_metasenv_counter)) - !context_length - ((float !context_length) /. (float !apply_subst_context_counter)) - ))*) - - - exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t -exception AssertFailure of string Lazy.t -exception DeliftingARelWouldCaptureAFreeVariable;; - -let debug_print = fun _ -> () - -type substitution = (int * (Cic.context * Cic.term)) list - -(* -let rec deref subst = - let third _,_,a = a in - function - Cic.Meta(n,l) as t -> - (try - deref subst - (CicSubstitution.subst_meta - l (third (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | t -> t -;; -*) - -let lookup_subst = CicUtil.lookup_subst -;; - -(* clean_up_meta take a metasenv and a term and make every local context -of each occurrence of a metavariable consistent with its canonical context, -with respect to the hidden hipothesis *) (* -let clean_up_meta subst metasenv t = - let module C = Cic in - let rec aux t = - match t with - C.Rel _ - | C.Sort _ -> t - | C.Implicit _ -> assert false - | C.Meta (n,l) as t -> - let cc = - (try - let (cc,_) = lookup_subst n subst in cc - with CicUtil.Subst_not_found _ -> - try - let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc - with CicUtil.Meta_not_found _ -> assert false) in - let l' = - (try - List.map2 - (fun t1 t2 -> - match t1,t2 with - None , _ -> None - | _ , t -> t) cc l - with - Invalid_argument _ -> assert false) in - C.Meta (n, l') - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest) - | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest) - | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | C.Appl l -> C.Appl (List.map aux l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux out, aux te, List.map aux pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl - in - C.CoFix (i, fl') - in - aux t *) - (*** Functions to apply a substitution ***) let apply_subst_gen ~appl_fun subst term = @@ -281,116 +140,27 @@ match subst with (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv) -(***** Pretty printing functions ******) - -let ppterm ~metasenv subst term = - CicPp.ppterm ~metasenv (apply_subst subst term) - -let ppterm_in_name_context ~metasenv subst term name_context = - CicPp.pp ~metasenv (apply_subst subst term) name_context - -let ppterm_in_context ~metasenv subst term context = - let name_context = - List.map (function None -> None | Some (n,_) -> Some n) context - in - ppterm_in_name_context ~metasenv subst term name_context - -let ppterm_in_context_ref = ref ppterm_in_context -let set_ppterm_in_context f = - ppterm_in_context_ref := f -let use_low_level_ppterm_in_context = ref false - -let ppterm_in_context ~metasenv subst term context = - if !use_low_level_ppterm_in_context then - ppterm_in_context ~metasenv subst term context - else - !ppterm_in_context_ref ~metasenv subst term context - -let ppcontext' ~metasenv ?(sep = "\n") subst context = - let separate s = if s = "" then "" else s ^ sep in - List.fold_right - (fun context_entry (i,name_context) -> - match context_entry with - Some (n,Cic.Decl t) -> - sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_name_context ~metasenv subst t name_context), - (Some n)::name_context - | Some (n,Cic.Def (bo,ty)) -> - sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) - (ppterm_in_name_context ~metasenv subst ty name_context) - (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context - | None -> - sprintf "%s_ :? _" (separate i), None::name_context - ) context ("",[]) - -let ppsubst_unfolded ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t,ty)) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d : %s := %s" context idx -(ppterm_in_name_context ~metasenv [] ty name_context) - (ppterm_in_name_context ~metasenv subst t name_context)) - subst) -(* - Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) - subst) *) -;; - -let ppsubst ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t, ty)) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in - sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context) - (ppterm_in_name_context ~metasenv [] t name_context)) - subst) -;; - -let ppcontext ~metasenv ?sep subst context = - fst (ppcontext' ~metasenv ?sep subst context) - -let ppmetasenv ?(sep = "\n") subst metasenv = - String.concat sep - (List.map - (fun (i, c, t) -> - let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d: %s" context i - (ppterm_in_name_context ~metasenv subst t name_context)) - (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;; +*) -(**** DELIFT ****) -(* the delift function takes in input a metavariable index, an ordered list of - * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some - * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit - * substitution that is applied to a metavariable occurrence and the result of - * the delift function is a term the implicit variable can be substituted with - * to make the term [t] unifiable with the metavariable occurrence. In general, - * the problem is undecidable if we consider equivalence in place of alpha - * convertibility. Our implementation, though, is even weaker than alpha - * convertibility, since it replace the term [tk] if and only if [tk] is a Rel - * (missing all the other cases). Does this matter in practice? - * The metavariable index is the index of the metavariable that must not occur - * in the term (for occur check). - *) exception NotInTheList;; -let position n = - let rec aux k = - function - [] -> raise NotInTheList - | (Some (Cic.Rel m))::_ when m=n -> k - | _::tl -> aux (k+1) tl in - aux 1 +let position n (shift, lc) = + match lc with + | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList + | NCic.Itl len -> n - shift + | NCic.Ctx tl -> + let rec aux k = function + | [] -> raise NotInTheList + | (Cic.Rel m)::_ when m + shift = n -> k + | _::tl -> aux (k+1) tl + in + aux 1 tl ;; - +(* exception Occur;; let rec force_does_not_occur subst to_be_restricted t = @@ -599,34 +369,200 @@ let rec restrict subst to_be_restricted metasenv = in restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv ;; +*) -(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*) - -let delift n subst context metasenv l t = -(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), - otherwise the occur check does not make sense *) +let newmeta = + let maxmeta = ref 0 in + fun () -> incr maxmeta; !maxmeta +;; -(* - debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto - al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))))); +let restrict metasenv subst i to_be_restricted = + let force_does_not_occur_in_context to_be_restricted = function + | None -> [], None + | Some (name, Cic.Decl t) -> + let (more_to_be_restricted, t') = + force_does_not_occur subst to_be_restricted t + in + more_to_be_restricted, Some (name, Cic.Decl t') + | Some (name, Cic.Def (bo, ty)) -> + let (more_to_be_restricted, bo') = + force_does_not_occur subst to_be_restricted bo + in + let more_to_be_restricted, ty' = + let more_to_be_restricted', ty' = + force_does_not_occur subst to_be_restricted ty + in + more_to_be_restricted @ more_to_be_restricted', + ty' + in + more_to_be_restricted, Some (name, Cic.Def (bo', ty')) + in + let rec erase i to_be_restricted n = function + | [] -> [], to_be_restricted, [] + | hd::tl -> + let more_to_be_restricted,restricted,tl' = + erase (i+1) to_be_restricted n tl + in + let restrict_me = List.mem i restricted in + if restrict_me then + more_to_be_restricted, restricted, None:: tl' + else + (try + let more_to_be_restricted', hd' = + let delifted_restricted = + let rec aux = + function + [] -> [] + | j::tl when j > i -> (j - i)::aux tl + | _::tl -> aux tl + in + aux restricted + in + force_does_not_occur_in_context delifted_restricted hd + in + more_to_be_restricted @ more_to_be_restricted', + restricted, hd' :: tl' + with Occur -> + more_to_be_restricted, (i :: restricted), None :: tl') + in + let (more_to_be_restricted, metasenv) = (* restrict metasenv *) + List.fold_right + (fun (n, context, t) (more, metasenv) -> + let to_be_restricted = + List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) + in + let (more_to_be_restricted, restricted, context') = + (* just an optimization *) + if to_be_restricted = [] then + [],[],context + else + erase 1 to_be_restricted n context + in + try + let more_to_be_restricted', t' = + force_does_not_occur subst restricted t + in + let metasenv' = (n, context', t') :: metasenv in + (more @ more_to_be_restricted @ more_to_be_restricted', + metasenv') + with Occur -> + raise (MetaSubstFailure (lazy (sprintf + "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" + n (names_of_context_indexes context to_be_restricted))))) + metasenv ([], []) + in + let (more_to_be_restricted', subst) = (* restrict subst *) + List.fold_right + (* TODO: cambiare dopo l'aggiunta del ty *) + (fun (n, (context, term,ty)) (more, subst') -> + let to_be_restricted = + List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) + in + (try + let (more_to_be_restricted, restricted, context') = + (* just an optimization *) + if to_be_restricted = [] then + [], [], context + else + erase 1 to_be_restricted n context + in + let more_to_be_restricted', term' = + force_does_not_occur subst restricted term + in + let more_to_be_restricted'', ty' = + force_does_not_occur subst restricted ty in + let subst' = (n, (context', term',ty')) :: subst' in + let more = + more @ more_to_be_restricted + @ more_to_be_restricted'@more_to_be_restricted'' in + (more, subst') + with Occur -> + let error_msg = lazy (sprintf + "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" + n (names_of_context_indexes context to_be_restricted) n + (ppterm ~metasenv subst term)) + in + (* DEBUG + debug_print (lazy error_msg); + debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); + debug_print (lazy ("subst = \n" ^ (ppsubst subst))); + debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) + raise (MetaSubstFailure error_msg))) + subst ([], []) + in + restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv +;; *) +;; - let module S = CicSubstitution in - let l = - let (_, canonical_context, _) = - try - CicUtil.lookup_meta n metasenv - with CicUtil.Meta_not_found _ -> - raise (MetaSubstFailure (lazy - ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^ - "declared in the metasenv"))) - in - List.map2 (fun ct lt -> - match (ct, lt) with - | None, _ -> None - | Some _, _ -> lt) - canonical_context l +(* 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 to_be_restricted = ref [] in + let rec aux k = function + | NCic.Rel n as t when n <= k -> t + | NCic.Rel n -> + (try + match List.nth context (n-k-1) with + | _,NCic.Def (bo,_) -> + (try C.Rel ((position (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 (NCicSubstitution.lift n bo)) + | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k) + with Failure _ -> assert false) (*Unbound variable found in delift*) + | NCic.Meta (i,l1) as orig -> + (try + let _,_,t,_ = NCicUtil.lookup_subst i subst in + aux k (NCicSubstitution.subst_meta l1 t) + with NCicUtil.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)))) + else + let shift1,lc1 = l1 in + let shift,lc = l in + match lc, lc1 with + | NCic.Irl len, NCic.Irl len1 + when shift1 < shift || len1 + shift1 > len + shift -> + (* new meta with shortened l1 + (1 -> shift - shift1 /\ shift + len + 1 -> shift1+len1) + subst += (i,new meta) + restrict checks (deleted entry cannot occur in the type...) + return that meta *) + assert false + | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig + | NCic.Irl len, NCic.Irl len1 -> + NCic.Meta (i, (shift1 - shift, lc1)) + | _ -> + let lc1 = NCicUtils.expand_local_context lc1 in + let rec deliftl j = function + | [] -> [] + | t::tl -> + let tl = deliftl (j+1) tl in + try (aux (k+shift1) t)::tl + with + | NotInTheList | MetaSubstFailure _ -> + to_be_restricted := (i,j)::!to_be_restricted; + tl + in + let l1 = deliftl 1 l1 in + C.Meta(i,l1)) (* or another ?k and possibly compress l1 *) + | t -> NCicUtils.map (fun _ k -> k+1) k aux t in + let t = aux 0 t in + let metasenv, subst = restrict subst !to_be_restricted metasenv in + metasenv, subst, t +;; + + let to_be_restricted = ref [] in let rec deliftaux k = let module C = Cic in @@ -673,8 +609,6 @@ let delift n subst context metasenv l t = i (ppterm ~metasenv subst t)))) else begin - (* I do not consider the term associated to ?i in subst since *) - (* in this way I can restrict if something goes wrong. *) let rec deliftl j = function [] -> [] @@ -914,17 +848,3 @@ let delift_rels subst metasenv n t = delift_rels_from subst metasenv 1 n t -(**** END OF DELIFT ****) - - -(** {2 Format-like pretty printers} *) - -let fpp_gen ppf s = - Format.pp_print_string ppf s; - Format.pp_print_newline ppf (); - Format.pp_print_flush ppf () - -let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) -let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) -let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) -*) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index e03180564..322330488 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -11,80 +11,39 @@ (* $Id$ *) -(* - exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t + +(* exception AssertFailure of string Lazy.t exception DeliftingARelWouldCaptureAFreeVariable;; - -(* The entry (i,t) in a substitution means that *) -(* (META i) have been instantiated with t. *) -(* type substitution = (int * (Cic.context * Cic.term)) list *) - - (** @raise SubstNotFound *) - -(* apply_subst subst t *) -(* applies the substitution [subst] to [t] *) -(* [subst] must be already unwinded *) - val apply_subst : Cic.substitution -> Cic.term -> Cic.term val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv (*** delifting ***) -val delift : - int -> Cic.substitution -> Cic.context -> Cic.metasenv -> - (Cic.term option) list -> Cic.term -> - Cic.term * Cic.metasenv * Cic.substitution val restrict : Cic.substitution -> (int * int) list -> Cic.metasenv -> Cic.metasenv * Cic.substitution +*) -(** delifts the Rels in t of n - * @raise DeliftingARelWouldCaptureAFreeVariable +(* the delift function takes in input a metavariable index, a local_context + * and a term t, and substitutes every Rel in t with its position in + * the local_context (which is the Rel moved to the canonical context). + * Typically, the list of optional terms is the explicit + * substitution that is applied to a metavariable occurrence and the result of + * the delift function is a term the implicit variable can be substituted with + * to make the term [t] unifiable with the metavariable occurrence. In general, + * the problem is undecidable if we consider equivalence in place of alpha + * convertibility. Our implementation, though, is even weaker than alpha + * convertibility, since it replace the term [tk] if and only if [tk] is a Rel + * (missing all the other cases). Does this matter in practice? + * The metavariable index is the index of the metavariable that must not occur + * in the term (for occur check). *) -val delift_rels : - Cic.substitution -> Cic.metasenv -> int -> Cic.term -> - Cic.term * Cic.substitution * Cic.metasenv +val delift : + NCic.metasenv -> NCic.substitution -> NCic.context -> + int -> NCic.local_context -> NCic.term -> + Cic.metasenv * Cic.substitution * Cic.term -(** {2 Pretty printers} *) -val use_low_level_ppterm_in_context : bool ref -val set_ppterm_in_context : - (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> - string) -> unit - -val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string -val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string -val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string -val ppcontext: - metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context -> - string -val ppterm_in_name_context: - metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> - (Cic.name option) list -> string -val ppterm_in_context: - metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string -val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string - -(** {2 Format-like pretty printers} - * As above with prototypes suitable for toplevel/ocamldebug printers. No - * subsitutions are applied here since such printers are required to be invoked - * with only one argument. - *) - -val fppsubst: Format.formatter -> Cic.substitution -> unit -val fppterm: Format.formatter -> Cic.term -> unit -val fppmetasenv: Format.formatter -> Cic.metasenv -> unit - -(* -(* DEBUG *) -val print_counters: unit -> unit -val reset_counters: unit -> unit -*) - -(* val clean_up_meta : - Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term -*) -*) -- 2.39.2