From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- engine/namegen.ml | 116 +++++++++++++++++++++++++++++------------------------- 1 file changed, 62 insertions(+), 54 deletions(-) (limited to 'engine/namegen.ml') diff --git a/engine/namegen.ml b/engine/namegen.ml index e56ec2877c..7b73029574 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -15,12 +15,13 @@ open Util open Names open Term +open Environ +open EConstr open Vars open Nametab open Nameops open Libnames open Globnames -open Environ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -84,13 +85,20 @@ let is_section_variable id = (**********************************************************************) (* Generating "intuitive" names from its type *) -let head_name c = (* Find the head constant of a constr if any *) +let global_of_constr = function +| Const (c, _) -> ConstRef c +| Ind (i, _) -> IndRef i +| Construct (c, _) -> ConstructRef c +| Var id -> VarRef id +| _ -> assert false + +let head_name sigma c = (* Find the head constant of a constr if any *) let rec hdrec c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) - | Const _ | Ind _ | Construct _ | Var _ -> + | Const _ | Ind _ | Construct _ | Var _ as c -> Some (basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) @@ -105,9 +113,9 @@ let sort_hdchar = function | Prop(_) -> "P" | Type(_) -> "T" -let hdchar env c = +let hdchar env sigma c = let rec hdrec k c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) @@ -119,7 +127,7 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env with + try match lookup_rel (n-k) env with | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") @@ -131,41 +139,41 @@ let hdchar env c = in hdrec 0 c -let id_of_name_using_hdchar env a = function - | Anonymous -> Id.of_string (hdchar env a) +let id_of_name_using_hdchar env sigma a = function + | Anonymous -> Id.of_string (hdchar env sigma a) | Name id -> id -let named_hd env a = function - | Anonymous -> Name (Id.of_string (hdchar env a)) +let named_hd env sigma a = function + | Anonymous -> Name (Id.of_string (hdchar env sigma a)) | x -> x -let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b) -let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b) +let mkProd_name env sigma (n,a,b) = mkProd (named_hd env sigma a n, a, b) +let mkLambda_name env sigma (n,a,b) = mkLambda (named_hd env sigma a n, a, b) let lambda_name = mkLambda_name let prod_name = mkProd_name -let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) -let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) +let prod_create env sigma (a,b) = mkProd (named_hd env sigma a Anonymous, a, b) +let lambda_create env sigma (a,b) = mkLambda (named_hd env sigma a Anonymous, a, b) -let name_assumption env = function - | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) - | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) +let name_assumption env sigma = function + | LocalAssum (na,t) -> LocalAssum (named_hd env sigma t na, t) + | LocalDef (na,c,t) -> LocalDef (named_hd env sigma c na, c, t) -let name_context env hyps = +let name_context env sigma hyps = snd (List.fold_left (fun (env,hyps) d -> - let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) + let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps)) (env,[]) (List.rev hyps)) -let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b -let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b +let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b +let mkLambda_or_LetIn_name env sigma b d = mkLambda_or_LetIn (name_assumption env sigma d) b -let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn b (name_context env hyps) -let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn b (name_context env hyps) +let it_mkProd_or_LetIn_name env sigma b hyps = + it_mkProd_or_LetIn b (name_context env sigma hyps) +let it_mkLambda_or_LetIn_name env sigma b hyps = + it_mkLambda_or_LetIn b (name_context env sigma hyps) (**********************************************************************) (* Fresh names *) @@ -185,10 +193,10 @@ let restart_subscript id = *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id -let visible_ids (nenv, c) = +let visible_ids sigma (nenv, c) = let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in - let rec visible_ids n c = match kind_of_term c with - | Const _ | Ind _ | Construct _ | Var _ -> + let rec visible_ids n c = match EConstr.kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ as c -> let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (Refset_env.mem g gseen) then @@ -218,7 +226,7 @@ let visible_ids (nenv, c) = | _ -> ids in accu := (gseen, vseen, ids) - | _ -> Constr.iter_with_binders succ visible_ids n c + | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in let () = visible_ids 1 c in let (_, _, ids) = !accu in @@ -228,9 +236,9 @@ let visible_ids (nenv, c) = (* 1- Looks for a fresh name for printing in cases pattern *) -let next_name_away_in_cases_pattern env_t na avoid = +let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in - let visible = visible_ids env_t in + let visible = visible_ids sigma env_t in let bad id = Id.List.mem id avoid || is_constructor id || Id.Set.mem id visible in next_ident_away_from id bad @@ -292,7 +300,7 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string -let make_all_name_different env = +let make_all_name_different env sigma = (** FIXME: this is inefficient, but only used in printing *) let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in let sign = named_context_val env in @@ -300,7 +308,7 @@ let make_all_name_different env = let env0 = reset_with_named_context sign env in Context.Rel.fold_outside (fun decl newenv -> - let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in + let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; push_rel (RelDecl.set_name (Name id) decl) newenv) @@ -311,12 +319,12 @@ let make_all_name_different env = looks for name of same base with lower available subscript beyond current subscript *) -let next_ident_away_for_default_printing env_t id avoid = - let visible = visible_ids env_t in +let next_ident_away_for_default_printing sigma env_t id avoid = + let visible = visible_ids sigma env_t in let bad id = Id.List.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad -let next_name_away_for_default_printing env_t na avoid = +let next_name_away_for_default_printing sigma env_t na avoid = let id = match na with | Name id -> id | Anonymous -> @@ -324,7 +332,7 @@ let next_name_away_for_default_printing env_t na avoid = (* taken into account by the function compute_displayed_name_in; *) (* just in case, invent a valid name *) default_non_dependent_ident in - next_ident_away_for_default_printing env_t id avoid + next_ident_away_for_default_printing sigma env_t id avoid (**********************************************************************) (* Displaying terms avoiding bound variables clashes *) @@ -349,45 +357,45 @@ type renaming_flags = | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) -let next_name_for_display flags = +let next_name_for_display sigma flags = match flags with - | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t + | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern sigma env_t | RenamingForGoal -> next_name_away_in_goal - | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t + | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in flags avoid na c = +let compute_displayed_name_in sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in - let idopt = if noccurn 1 c then Anonymous else Name fresh_id in + let fresh_id = next_name_for_display sigma flags na avoid in + let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in (idopt, fresh_id::avoid) -let compute_and_force_displayed_name_in flags avoid na c = +let compute_and_force_displayed_name_in sigma flags avoid na c = match na with - | Anonymous when noccurn 1 c -> + | Anonymous when noccurn sigma 1 c -> (Anonymous,avoid) | _ -> - let fresh_id = next_name_for_display flags na avoid in + let fresh_id = next_name_for_display sigma flags na avoid in (Name fresh_id, fresh_id::avoid) -let compute_displayed_let_name_in flags avoid na c = - let fresh_id = next_name_for_display flags na avoid in +let compute_displayed_let_name_in sigma flags avoid na c = + let fresh_id = next_name_for_display sigma flags na avoid in (Name fresh_id, fresh_id::avoid) -let rename_bound_vars_as_displayed avoid env c = +let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (na,c1,c2) -> let na',avoid' = - compute_displayed_name_in + compute_displayed_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in mkProd (na', c1, rename avoid' (na' :: env) c2) | LetIn (na,c1,t,c2) -> let na',avoid' = - compute_displayed_let_name_in + compute_displayed_let_name_in sigma (RenamingElsewhereFor (env,c2)) avoid na c2 in mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) -- cgit v1.2.3 From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- engine/namegen.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/namegen.ml') diff --git a/engine/namegen.ml b/engine/namegen.ml index 7b73029574..3b979f206e 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -123,7 +123,7 @@ let hdchar env sigma c = | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id - | Sort s -> sort_hdchar s + | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else -- cgit v1.2.3