From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Sep 2014 00:03:46 +0200 Subject: Revert specific syntax for primitive projections, avoiding ugly contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now. --- interp/constrextern.ml | 130 ++++++++++++----------------------------- interp/constrextern.mli | 7 ++- interp/constrintern.ml | 63 ++------------------ interp/implicit_quantifiers.ml | 1 - interp/notation_ops.ml | 15 +---- interp/reserve.ml | 2 +- 6 files changed, 49 insertions(+), 169 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2e6ab4354..b774da356 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -437,28 +437,14 @@ let occur_name na aty = | Name id -> occur_var_constr_expr id aty | Anonymous -> false -let is_projection primprojapp nargs cf = - let env = Global.env () in - match primprojapp with - | Some r -> - let pb = Environ.lookup_projection r env in - Some pb.Declarations.proj_npars, Some 1 - | None -> - match cf with - | Some (ConstRef p) when Environ.is_projection p (Global.env()) -> - let pb = Environ.lookup_projection p env in - (* For primitive projections, r.(p) and r.(@p) are reserved to the - non-eta-expanded version of the constant, we disallow printing - of the eta-expanded projection as a projection *) - Some pb.Declarations.proj_npars, None - | Some r when not !in_debugger && not !Flags.raw_print && !print_projections -> - (try - let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then None, None - else None, Some n - with Not_found -> None, None) - | _ -> None, None - +let is_projection nargs = function + | Some r when not !in_debugger && not !Flags.raw_print && !print_projections -> + (try + let n = Recordops.find_projection_nparams r + 1 in + if n <= nargs then None + else Some n + with Not_found -> None) + | _ -> None let is_hole = function CHole _ | CEvar _ -> true | _ -> false @@ -481,7 +467,7 @@ let params_implicit n impl = (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) -let explicitize loc inctx impl (cf,primprojapp,f) args = +let explicitize loc inctx impl (cf,f) args = let impl = if !Constrintern.parsing_explicit then [] else impl in let n = List.length args in let rec exprec q = function @@ -506,44 +492,27 @@ let explicitize loc inctx impl (cf,primprojapp,f) args = raise Expl | [], _ -> [] in - let primproj, ip = is_projection primprojapp (List.length args) cf in + let ip = is_projection (List.length args) cf in let expl () = match ip with | Some i -> - (match primproj with - | Some npars -> (* Primitive projection in projection notation *) - let projimpl = CList.skipn_at_least npars impl in - if not !print_projections && not !Flags.raw_print && params_implicit npars impl then - (* Printing primitive projection as application *) - let args = exprec 1 (args,projimpl) in - CApp (loc, (None, f), args) - else (** Printing as projection *) - let args = exprec 1 (args,projimpl) in - CApp (loc, (Some i,f),args) - | None -> (** Regular constant in projection notation *) - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl - else - let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in - let args1 = exprec 1 (args1,impl1) in - let args2 = exprec (i+1) (args2,impl2) in - let ip = Some (List.length args1) in - CApp (loc,(ip,f),args1@args2)) - | None -> - match primproj with - | Some npars when List.length args > npars && params_implicit npars impl -> - (* Eta-expanded version of projection, print explicited if the implicit - application would be parsed as a primitive projection application. *) + if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then raise Expl - | _ -> - let args = exprec 1 (args,impl) in - if List.is_empty args then f else CApp (loc, (None, f), args) + else + let (args1,args2) = List.chop i args in + let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let args1 = exprec 1 (args1,impl1) in + let args2 = exprec (i+1) (args2,impl2) in + let ip = Some (List.length args1) in + CApp (loc,(ip,f),args1@args2) + | None -> + let args = exprec 1 (args,impl) in + if List.is_empty args then f else CApp (loc, (None, f), args) in try expl () with Expl -> let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in - let ip = if primprojapp != None || !print_projections then ip else None in + let ip = if !print_projections then ip else None in CAppExpl (loc, (ip, f', us), args) let is_start_implicit = function @@ -557,7 +526,7 @@ let extern_global loc impl f us = else CRef (f,us) -let extern_app loc inctx impl (cf,primproj,f) us args = +let extern_app loc inctx impl (cf,f) us args = if List.is_empty args then (* If coming from a notation "Notation a := @b" *) CAppExpl (loc, (None, f, us), []) @@ -566,12 +535,9 @@ let extern_app loc inctx impl (cf,primproj,f) us args = (!print_implicits && not !print_implicits_explicit_args)) && List.exists is_status_implicit impl) then - if primproj != None then - CAppExpl (loc, (Some 1,f,us), args) - else - CAppExpl (loc, (snd (is_projection primproj (List.length args) cf),f,us), args) + CAppExpl (loc, (is_projection (List.length args) cf,f,us), args) else - explicitize loc inctx impl (cf,primproj,CRef (f,us)) args + explicitize loc inctx impl (cf,CRef (f,us)) args let rec extern_args extern scopes env args subscopes = match args with @@ -585,12 +551,6 @@ let rec extern_args extern scopes env args subscopes = let match_coercion_app = function | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args) - | GProj (loc, r, arg) -> - let pars = Inductiveops.projection_nparams r in - Some (loc, ConstRef r, pars, [arg]) - | GApp (loc,GProj (_, r, c), args) -> - let pars = Inductiveops.projection_nparams r in - Some (loc, ConstRef r, pars, c :: args) | _ -> None let rec remove_coercions inctx c = @@ -728,27 +688,13 @@ let rec extern inctx scopes vars r = | Not_found | No_match | Exit -> extern_app loc inctx (select_stronger_impargs (implicits_of_global ref)) - (Some ref,None,extern_reference rloc vars ref) (extern_universes us) args + (Some ref,extern_reference rloc vars ref) (extern_universes us) args end - - | GProj (loc,p,c) -> - let ref = ConstRef p in - let subscopes = find_arguments_scope ref in - let args = - extern_args (extern true) (snd scopes) vars (c :: args) subscopes - in - extern_app loc inctx - (select_stronger_impargs (implicits_of_global ref)) - (Some ref, Some p, extern_reference loc vars ref) - None args | _ -> - explicitize loc inctx [] (None,None,sub_extern false scopes vars f) + explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) - | GProj (loc,p,c) -> - extern inctx scopes vars (GApp (loc,r',[])) - | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) @@ -967,7 +913,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function if List.is_empty args then e else let args = extern_args (extern true) scopes vars args argsscopes in - explicitize loc false argsimpls (None,None,e) args + explicitize loc false argsimpls (None,e) args with No_match -> extern_symbol allscopes vars t rules @@ -989,7 +935,7 @@ let extern_glob_type vars c = let loc = Loc.ghost (* for constr and pattern, locations are lost *) -let extern_constr_gen goal_concl_style scopt env sigma t = +let extern_constr_gen lax goal_concl_style scopt env sigma t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) (* i.e.: avoid using the names of goal/section/rel variables and the short *) (* names of global definitions of current module when computing names for *) @@ -998,21 +944,19 @@ let extern_constr_gen goal_concl_style scopt env sigma t = (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then ids_of_context env else [] in - let rel_env_names = names_of_rel_context env in - let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in + let r = Detyping.detype ~lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r let extern_constr_in_scope goal_concl_style scope env sigma t = - extern_constr_gen goal_concl_style (Some scope) env sigma t + extern_constr_gen false goal_concl_style (Some scope) env sigma t -let extern_constr goal_concl_style env sigma t = - extern_constr_gen goal_concl_style None env sigma t +let extern_constr ?(lax=false) goal_concl_style env sigma t = + extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in - let rel_env_names = names_of_rel_context env in - let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in + let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort s = extern_glob_sort (detype_sort s) @@ -1076,14 +1020,14 @@ let rec glob_of_pat env sigma = function | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> Detyping.detype false [] env sigma (mkFix f) - | PCoFix c -> Detyping.detype false [] env sigma (mkCoFix c) + | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *) + | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c) | PSort s -> GSort (loc,s) let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = - let a = detype_rel_context where [] (names_of_rel_context env) sigma sign in + let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index a994d8693..023c5be22 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -30,9 +30,12 @@ val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr (** If [b=true] in [extern_constr b env c] then the variables in the first - level of quantification clashing with the variables in [env] are renamed *) + level of quantification clashing with the variables in [env] are renamed. + ~lax is for debug printing, when the constr might not be well typed in + env, sigma +*) -val extern_constr : bool -> env -> Evd.evar_map -> constr -> constr_expr +val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 66f51b19e..56780e240 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1312,7 +1312,6 @@ let get_implicit_name n imps = let set_hole_implicit i b = function | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None) - | GProj (loc,p,_) -> (loc,Evar_kinds.ImplicitArg (ConstRef p,i,b),None) | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None) | _ -> anomaly (Pp.str "Only refs have implicits") @@ -1463,14 +1462,8 @@ let internalize globalenv env allow_patvar lvar c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref in - (match isproj, isprojf with - | Some i, Some (r, n) -> (* Explicit application of primitive projection *) - let scopes = proj_scopes n args_scopes in - let args = intern_args env scopes (List.map fst args) in - GApp (loc, GProj (loc, r, List.hd args), List.tl args) - | _ -> - (* Rem: GApp(_,f,[]) stands for @f *) - GApp (loc, f, intern_args env args_scopes (List.map fst args))) + (* Rem: GApp(_,f,[]) stands for @f *) + GApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with @@ -1726,58 +1719,10 @@ let internalize globalenv env allow_patvar lvar c = intern_args env subscopes rargs in aux 1 l subscopes eargs rargs - and make_first_explicit l = - match l with - | hd :: tl -> None :: tl - | [] -> [] - - and projection_application_implicits n noargs l = - if n == 0 then Some l - else match l with - | hd :: tl when is_status_implicit hd -> - if maximal_insertion_of hd || not noargs then - projection_application_implicits (pred n) noargs tl - else None - | _ -> None - and apply_impargs (isproj,isprojf) c env imp subscopes l loc = let imp = select_impargs_size (List.length l) imp in - let default () = - let l = intern_impargs c env imp subscopes l in - smart_gapp c loc l - in - match isprojf with - | Some (r, n) -> (* A primitive projection *) - let subscopes = proj_scopes n subscopes in - if isproj != None then (* In projection notation: we remove the parameters *) - let imp = projection_implicits (Global.env()) r imp in - let imp = make_first_explicit imp in (* For the record argument *) - let l = intern_impargs c env imp subscopes l in - (match c, l with - | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest -> - let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in - if List.is_empty tl then smart_gapp proj loc rest - else GApp (loc, proj, tl @ rest) - | GRef (loc', ConstRef f, _), hd :: tl -> - let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in - smart_gapp proj loc tl - | _ -> assert false) - else (* Not in projection notation, parse as primitive only if the implicits - allow *) - (match projection_application_implicits n (List.is_empty l) imp with - | Some imp -> - let l = intern_impargs c env imp subscopes l in - (match c, l with - | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest -> - let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in - if List.is_empty tl then smart_gapp proj loc rest - else GApp (loc, proj, tl @ rest) - | GRef (loc', ConstRef f, _), hd :: tl -> - let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in - smart_gapp proj loc tl - | _ -> default ()) - | None -> default ()) - | None -> default () + let l = intern_impargs c env imp subscopes l in + smart_gapp c loc l and smart_gapp f loc = function | [] -> f diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index c69eb629d..90303cc92 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -127,7 +127,6 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GProj (loc,p,c) -> vars bound vs c | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1aac1c53d..81e2ac810 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -55,7 +55,6 @@ let ldots_var = Id.of_string ".." let glob_constr_of_notation_constr_with_binders loc g f e = function | NVar id -> GVar (loc,id) | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) - | NProj (p,c) -> GProj (loc,p,f e c) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in @@ -150,7 +149,6 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2 | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 - | GProj (_,p1,c1), GProj (_, p2, c2) -> eq_constant p1 p2 && f c1 c2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 @@ -166,7 +164,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GProj _ | GLambda _ | GProd _ + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -261,7 +259,6 @@ let notation_constr_and_vars_of_glob_constr a = and aux' = function | GVar (_,id) -> add_id found id; NVar id | GApp (_,g,args) -> NApp (aux g, List.map aux args) - | GProj (_,p,c) -> NProj (p, aux c) | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) @@ -356,7 +353,7 @@ let notation_constr_of_glob_constr nenv a = (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = - let t = Detyping.detype false avoiding [] Evd.empty t in + let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -388,12 +385,6 @@ let rec subst_notation_constr subst bound raw = if r' == r && rl' == rl then raw else NApp(r',rl') - | NProj (p,c) -> - let p' = subst_constant subst p in - let c' = subst_notation_constr subst bound c in - if p == p' && c == c' then raw else - NProj (p',c') - | NList (id1,id2,r1,r2,b) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in @@ -669,8 +660,6 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma - | GProj (loc,f1,c1), NProj (f2,c2) when Constant.equal f1 f2 -> - match_in u alp metas sigma c1 c2 | GApp (loc,f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = diff --git a/interp/reserve.ml b/interp/reserve.ml index 33c21eea5..bb4109009 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -108,7 +108,7 @@ let constr_key c = let revert_reserved_type t = try let reserved = KeyMap.find (constr_key t) !reserve_revtable in - let t = Detyping.detype false [] [] Evd.empty t in + let t = Detyping.detype false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = -- cgit v1.2.3