diff options
Diffstat (limited to 'vernac')
38 files changed, 2517 insertions, 1825 deletions
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 0e2b0c80e8..751e79d89c 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -23,7 +23,7 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (Label.t * Context.Rel.t * types) list Refmap_env.t) + (Label.t * Constr.rel_context * types) list Refmap_env.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index ee578669c2..e33aa38173 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -355,7 +355,7 @@ let destruct_ind sigma c = then avoid should be [| lb_An ... lb _A1 (resp. bl_An ... bl_A1) eq_An .... eq_A1 An ... A1 |] -so from Ai we can find the the correct eq_Ai bl_ai or lb_ai +so from Ai we can find the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) let do_replace_lb mode lb_scheme_key aavoid narg p q = diff --git a/vernac/class.ml b/vernac/class.ml index 1337267020..614b2181d9 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -73,7 +73,7 @@ let check_reference_arity ref = let check_arity = function | CL_FUN | CL_SORT -> () | CL_CONST cst -> check_reference_arity (ConstRef cst) - | CL_PROJ cst -> check_reference_arity (ConstRef cst) + | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p)) | CL_SECVAR id -> check_reference_arity (VarRef id) | CL_IND kn -> check_reference_arity (IndRef kn) @@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt = let class_of_global = function | ConstRef sp -> - if Environ.is_projection sp (Global.env ()) - then CL_PROJ sp else CL_CONST sp + (match Recordops.find_primitive_projection sp with + | Some p -> CL_PROJ p | None -> CL_CONST sp) | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id | ConstructRef _ as c -> @@ -143,8 +143,8 @@ let get_target t ind = CL_FUN else match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with - | CL_CONST p when Environ.is_projection p (Global.env ()) -> - CL_PROJ p + | CL_CONST p when Recordops.is_primitive_projection p -> + CL_PROJ (Option.get @@ Recordops.find_primitive_projection p) | x -> x let strength_of_cl = function @@ -165,7 +165,8 @@ let get_strength stre ref cls clt = let ident_key_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" - | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp) + | CL_CONST sp -> Label.to_string (Constant.label sp) + | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp) | CL_IND (sp,_) -> Label.to_string (MutInd.label sp) | CL_SECVAR id -> Id.to_string id @@ -303,12 +304,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false let add_coercion_hook poly local ref = - let stre = match local with + let local = match local with + | Discharge | Local -> true | Global -> false - | Discharge -> assert false in - let () = try_add_new_coercion ref ~local:stre poly in + let () = try_add_new_coercion ref ~local poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg diff --git a/vernac/classes.ml b/vernac/classes.ml index 382d18b095..bf734ab36d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,7 +42,7 @@ let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] - (Hints.HintsTransparencyEntry ([c], b)) + (Hints.HintsTransparencyEntry (Vernacexpr.HintsReferences [c], b)) let _ = Hook.set Typeclasses.add_instance_hint_hook @@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let env = Global.env () in - let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) - (Univops.universes_of_constr env term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in diff --git a/vernac/classes.mli b/vernac/classes.mli index bd30b2d60e..9c37364cb0 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -16,9 +16,9 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a -val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a8ac528466..750ed35cbc 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -163,7 +163,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in uvars, (coe,t,imps)) Univ.LSet.empty l in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index f55c852c0d..a8d7946429 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt = let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = - Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) + Univ.LSet.union uvars (universes_of_constr evd (of_constr c)) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1d1cc62dea..37258c2d45 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let env = Global.env () in - let vars = Univops.universes_of_constr env (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index f51bfbad59..b1a9c8a5a3 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -82,12 +82,12 @@ val interp_fixpoint : val declare_fixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Very private function, do not use *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 6057c05f58..ad1ffa35a1 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly = else sigma let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) + u = Prop || (is_impredicative_set env && u = Set) let interp_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in @@ -146,7 +146,6 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - on_snd (on_fst EConstr.Unsafe.to_constr) @@ interp_type_evars_impls env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) @@ -245,7 +244,7 @@ let solve_constraints_system levels level_bounds = let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> - if a = Prop Null then None + if a = Prop then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = @@ -298,14 +297,14 @@ let inductive_levels env evd poly arities inds = (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du + Evd.set_leq_sort env evd Set du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du + Evd.set_eq_sort env evd Prop du else evd else Evd.set_eq_sort env evd (Type cu) du in @@ -327,14 +326,17 @@ let check_param = function | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") -let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; - let env0 = Global.env() in + if not (List.is_empty uparamsl) && not (List.is_empty notations) + then user_err (str "Inductives with uniform parameters may not have attached notations."); let pl = (List.hd indl).ind_univs in let sigma, decl = interp_univ_decl_opt env0 pl in + let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = + interp_context_evars env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars env0 sigma paramsl + interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -346,15 +348,15 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in - let env_ar = push_types env0 indnames fullarities in + let env_ar = push_types env_uparams indnames fullarities in let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in + let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in let sigma, constructors = @@ -365,6 +367,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) () in + (* generalize over the uniform parameters *) + let nparams = Context.Rel.length ctx_params in + let nuparams = Context.Rel.length ctx_uparams in + let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in + let uparam_subst = + List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs)) + @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in + let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in + let constructors = List.map (fun (cnames,ctypes,cimpls) -> + (cnames,List.map generalize_constructor ctypes,cimpls)) + constructors + in + let ctx_params = ctx_params @ ctx_uparams in + let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in + let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in + let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in + let env_ar = push_types env0 indnames fullarities in + let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in (* Compute renewed arities *) @@ -423,6 +444,9 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = + interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite + (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 @@ -505,10 +529,15 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl cum poly prv finite = - let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + +let do_mutual_inductive indl cum poly prv ~uniform finite = + let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in + let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7ae8e8f716..4e30ed7de5 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -19,9 +19,14 @@ open Decl_kinds (** Entry points for the vernacular commands Inductive and CoInductive *) +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + Declarations.recursivity_kind -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index eef7afbfba..102a98f046 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -187,7 +187,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, def = let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in let sigma, h_e_term = Evarutil.new_evar env sigma - ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in + ~src:(Loc.tag @@ Evar_kinds.QuestionMark { + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false; + }) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in let sigma, def = Typing.solve_evars env sigma def in diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index cc9be7b0e5..16101396cf 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -54,6 +54,17 @@ let default_pattern_levels = let default_constr_levels = (default_levels, default_pattern_levels) +let find_levels levels = function + | InConstrEntry -> levels, String.Map.find "constr" levels + | InCustomEntry s -> + try levels, String.Map.find s levels + with Not_found -> + String.Map.add s ([],[]) levels, ([],[]) + +let save_levels levels custom lev = + let s = match custom with InConstrEntry -> "constr" | InCustomEntry s -> s in + String.Map.add s lev levels + (* At a same level, LeftA takes precedence over RightA and NoneA *) (* In case, several associativity exists for a level, we make two levels, *) (* first LeftA, then RightA and NoneA together *) @@ -125,24 +136,24 @@ let rec list_mem_assoc_triple x = function let register_empty_levels accu forpat levels = let rec filter accu = function | [] -> ([], accu) - | n :: rem -> + | (where,n) :: rem -> let rem, accu = filter accu rem in - let (clev, plev) = accu in + let accu, (clev, plev) = find_levels accu where in let levels = if forpat then plev else clev in if not (list_mem_assoc_triple n levels) then let nlev, ans = find_position_gen levels true None (Some n) in let nlev = if forpat then (clev, nlev) else (nlev, plev) in - ans :: rem, nlev + (where, ans) :: rem, save_levels accu where nlev else rem, accu in filter accu levels -let find_position accu forpat assoc level = - let (clev, plev) = accu in +let find_position accu custom forpat assoc level = + let accu, (clev, plev) = find_levels accu custom in let levels = if forpat then plev else clev in let nlev, ans = find_position_gen levels false assoc level in let nlev = if forpat then (clev, nlev) else (nlev, plev) in - (ans, nlev) + (ans, save_levels accu custom nlev) (**************************************************************************) (* @@ -231,7 +242,7 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry -| TTConstr : prod_info * 'r target -> ('r, 'r) entry +| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry | TTOpenBinderList : ('self, local_binder_expr list) entry @@ -239,17 +250,58 @@ type (_, _) entry = type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry +let constr_custom_entry : (string, Constrexpr.constr_expr) entry_command = + create_entry_command "constr" (fun s st -> [s], st) +let pattern_custom_entry : (string, Constrexpr.cases_pattern_expr) entry_command = + create_entry_command "pattern" (fun s st -> [s], st) + +let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.empty +(** If the entry is present then local *) + +let create_custom_entry ~local s = + if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then + user_err Pp.(quote (str s) ++ str " is a reserved entry name."); + let sc = "constr:"^s in + let sp = "pattern:"^s in + let _ = extend_entry_command constr_custom_entry sc in + let _ = extend_entry_command pattern_custom_entry sp in + let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in + () + +let find_custom_entry s = + let sc = "constr:"^s in + let sp = "pattern:"^s in + try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp) + with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".") + +let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality + (* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = - fun forpat level -> match forpat with +let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option = + fun custom forpat level -> + match custom with + | InCustomEntry s -> + (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in + match forpat with + | ForConstr -> entry_for_constr, Some level + | ForPattern -> entry_for_patttern, Some level) + | InConstrEntry -> + match forpat with | ForConstr -> if level = 200 then Constr.binder_constr, None else Constr.operconstr, Some level | ForPattern -> Constr.pattern, Some level -let target_entry : type s. s target -> s Gram.entry = function -| ForConstr -> Constr.operconstr -| ForPattern -> Constr.pattern +let target_entry : type s. notation_entry -> s target -> s Entry.t = function +| InConstrEntry -> + (function + | ForConstr -> Constr.operconstr + | ForPattern -> Constr.pattern) +| InCustomEntry s -> + let (entry_for_constr, entry_for_patttern) = find_custom_entry s in + function + | ForConstr -> entry_for_constr + | ForPattern -> entry_for_patttern let is_self from e = match e with | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false @@ -273,25 +325,25 @@ let make_sep_rules = function let r = mkrule (List.rev tkl) in Arules [r] -let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> - if is_binder_level from p then Aentryl (target_entry forpat, 200) +let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat -> + if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200") else if is_self from p then Aself else - let g = target_entry forpat in + let g = target_entry custom forpat in let lev = adjust_level assoc from p in begin match lev with | None -> Aentry g | Some None -> Anext - | Some (Some (lev, cur)) -> Aentryl (g, lev) + | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with -| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat +| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat | TTConstrList (typ', [], forpat) -> - Alist1 (symbol_of_target typ' assoc from forpat) + Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat) | TTConstrList (typ', tkl, forpat) -> - Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) -| TTPattern p -> Aentryl (Constr.pattern, p) + Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl) +| TTPattern p -> Aentryl (Constr.pattern, string_of_int p) | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) | TTName -> Aentry Prim.name @@ -303,9 +355,8 @@ let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint -| ETProdConstr p -> TTAny (TTConstr (p, forpat)) +| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) -| ETProdOther _ -> assert false (** not used *) | ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) @@ -420,20 +471,23 @@ let target_to_bool : type r. r target -> bool = function | ForConstr -> false | ForPattern -> true -let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = +let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = let empty = (pos, [(name, p4assoc, [])]) in - if forpat then ExtendRule (Constr.pattern, reinit, empty) - else ExtendRule (Constr.operconstr, reinit, empty) - -let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with -| Stop -> [] -| Next (rem, Aentryl (_, i)) -> - let rem = pure_sublevels level rem in - begin match level with - | Some j when Int.equal i j -> rem - | _ -> i :: rem - end -| Next (rem, _) -> pure_sublevels level rem + ExtendRule (target_entry where forpat, reinit, empty) + +let rec pure_sublevels' custom assoc from forpat level = function +| [] -> [] +| GramConstrNonTerminal (e,_) :: rem -> + let rem = pure_sublevels' custom assoc from forpat level rem in + let push where p rem = + match symbol_of_target custom p assoc from forpat with + | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem + | _ -> rem in + (match e with + | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem + | ETProdConstr (s,p) -> push s p rem + | _ -> rem) +| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' custom assoc from forpat level rem let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> @@ -444,17 +498,17 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = - let n,_,_ = ng.notgram_level in + let custom,n,_,_ = ng.notgram_level in let assoc = ng.notgram_assoc in - let (entry, level) = interp_constr_entry_key forpat n in + let (entry, level) = interp_constr_entry_key custom forpat n in let fold (accu, state) pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in let symbs = ty_erase r in - let pure_sublevels = pure_sublevels level symbs in + let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in let isforpat = target_to_bool forpat in let needed_levels, state = register_empty_levels state isforpat pure_sublevels in - let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in - let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in + let (pos,p4assoc,name,reinit), state = find_position state custom isforpat assoc level in + let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in @@ -467,7 +521,7 @@ let constr_levels = GramState.field () let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with - | None -> default_constr_levels + | None -> String.Map.add "constr" default_constr_levels String.Map.empty | Some lev -> lev in (* Add the notation in constr *) diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index b0341e6a17..3a6f8ae015 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -17,3 +17,6 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) + +val create_custom_entry : local:bool -> string -> unit +val locality_of_custom_entry : string -> bool diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 048d4d93a0..c5dedc880e 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -64,6 +64,15 @@ let make_rule f prod = let act = ty_eval ty_rule f in Extend.Rule (symb, act) +let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function +| TUentry a -> ExtraArg a +| TUentryl (a,l) -> ExtraArg a +| TUopt(o) -> OptArg (proj_symbol o) +| TUlist1 l -> ListArg (proj_symbol l) +| TUlist1sep (l,_) -> ListArg (proj_symbol l) +| TUlist0 l -> ListArg (proj_symbol l) +| TUlist0sep (l,_) -> ListArg (proj_symbol l) + (** Vernac grammar extensions *) let vernac_exts = ref [] diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 31aa1a9891..c4f4fcfaa4 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,11 +21,13 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type + (** Utility function reused in Egramcoq : *) val make_rule : diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 deleted file mode 100644 index 4b11276af3..0000000000 --- a/vernac/g_proofs.ml4 +++ /dev/null @@ -1,131 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Glob_term -open Constrexpr -open Vernacexpr -open Proof_global - -open Pcoq -open Pcoq.Prim -open Pcoq.Constr -open Pvernac.Vernac_ - -let thm_token = G_vernac.thm_token - -let hint = Gram.entry_create "hint" - -let warn_deprecated_focus = - CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" - (fun () -> - Pp.strbrk - "The Focus command is deprecated; use bullets or focusing brackets instead" - ) - -let warn_deprecated_focus_n n = - CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" - (fun () -> - Pp.(str "The Focus command is deprecated;" ++ spc () - ++ str "use '" ++ int n ++ str ": {' instead") - ) - -let warn_deprecated_unfocus = - CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" - (fun () -> Pp.strbrk "The Unfocus command is deprecated") - -(* Proof commands *) -GEXTEND Gram - GLOBAL: hint command; - - opt_hintbases: - [ [ -> [] - | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] - ; - command: - [ [ IDENT "Goal"; c = lconstr -> - VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) - | IDENT "Proof" -> VernacProof (None,None) - | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn - | IDENT "Proof"; c = lconstr -> VernacExactProof c - | IDENT "Abort" -> VernacAbort None - | IDENT "Abort"; IDENT "All" -> VernacAbortAll - | IDENT "Abort"; id = identref -> VernacAbort (Some id) - | IDENT "Existential"; n = natural; c = constr_body -> - VernacSolveExistential (n,c) - | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) - | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque, Some id)) - | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) - | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (Transparent,Some id)) - | IDENT "Restart" -> VernacRestart - | IDENT "Undo" -> VernacUndo 1 - | IDENT "Undo"; n = natural -> VernacUndo n - | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n - | IDENT "Focus" -> - warn_deprecated_focus ~loc:!@loc (); - VernacFocus None - | IDENT "Focus"; n = natural -> - warn_deprecated_focus_n n ~loc:!@loc (); - VernacFocus (Some n) - | IDENT "Unfocus" -> - warn_deprecated_unfocus ~loc:!@loc (); - VernacUnfocus - | IDENT "Unfocused" -> VernacUnfocused - | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) - | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) - | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript - | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials - | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses - | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames - | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof - | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) - | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) - | IDENT "Guarded" -> VernacCheckGuard - (* Hints for Auto and EAuto *) - | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> true | -> false ] -> - VernacCreateHintDb (id, b) - | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> - VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> - VernacHints (dbnames, h) - ] ]; - reference_or_constr: - [ [ r = global -> HintsReference r - | c = constr -> HintsConstr c ] ] - ; - hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> - HintsResolve (List.map (fun x -> (info, true, x)) lc) - | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural -> - HintsResolveIFF (true, lc, n) - | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> - HintsResolveIFF (false, lc, n) - | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc - | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) - | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) - | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) - | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid - | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ] - ; - constr_body: - [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] - ; - mode: - [ [ l = LIST1 [ "+" -> ModeInput - | "!" -> ModeNoHeadEvar - | "-" -> ModeOutput ] -> l ] ] - ; -END diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg new file mode 100644 index 0000000000..dacef6e211 --- /dev/null +++ b/vernac/g_proofs.mlg @@ -0,0 +1,139 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +{ + +open Glob_term +open Constrexpr +open Vernacexpr +open Proof_global + +open Pcoq +open Pcoq.Prim +open Pcoq.Constr +open Pvernac.Vernac_ + +let thm_token = G_vernac.thm_token + +let hint = Entry.create "hint" + +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") + +} + +(* Proof commands *) +GRAMMAR EXTEND Gram + GLOBAL: hint command; + + opt_hintbases: + [ [ -> { [] } + | ":"; l = LIST1 [id = IDENT -> { id } ] -> { l } ] ] + ; + command: + [ [ IDENT "Goal"; c = lconstr -> + { VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) } + | IDENT "Proof" -> { VernacProof (None,None) } + | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn } + | IDENT "Proof"; c = lconstr -> { VernacExactProof c } + | IDENT "Abort" -> { VernacAbort None } + | IDENT "Abort"; IDENT "All" -> { VernacAbortAll } + | IDENT "Abort"; id = identref -> { VernacAbort (Some id) } + | IDENT "Existential"; n = natural; c = constr_body -> + { VernacSolveExistential (n,c) } + | IDENT "Admitted" -> { VernacEndProof Admitted } + | IDENT "Qed" -> { VernacEndProof (Proved (Opaque,None)) } + | IDENT "Save"; id = identref -> + { VernacEndProof (Proved (Opaque, Some id)) } + | IDENT "Defined" -> { VernacEndProof (Proved (Transparent,None)) } + | IDENT "Defined"; id=identref -> + { VernacEndProof (Proved (Transparent,Some id)) } + | IDENT "Restart" -> { VernacRestart } + | IDENT "Undo" -> { VernacUndo 1 } + | IDENT "Undo"; n = natural -> { VernacUndo n } + | IDENT "Undo"; IDENT "To"; n = natural -> { VernacUndoTo n } + | IDENT "Focus" -> + { warn_deprecated_focus ~loc (); + VernacFocus None } + | IDENT "Focus"; n = natural -> + { warn_deprecated_focus_n n ~loc (); + VernacFocus (Some n) } + | IDENT "Unfocus" -> + { warn_deprecated_unfocus ~loc (); + VernacUnfocus } + | IDENT "Unfocused" -> { VernacUnfocused } + | IDENT "Show" -> { VernacShow (ShowGoal OpenSubgoals) } + | IDENT "Show"; n = natural -> { VernacShow (ShowGoal (NthGoal n)) } + | IDENT "Show"; id = ident -> { VernacShow (ShowGoal (GoalId id)) } + | IDENT "Show"; IDENT "Script" -> { VernacShow ShowScript } + | IDENT "Show"; IDENT "Existentials" -> { VernacShow ShowExistentials } + | IDENT "Show"; IDENT "Universes" -> { VernacShow ShowUniverses } + | IDENT "Show"; IDENT "Conjectures" -> { VernacShow ShowProofNames } + | IDENT "Show"; IDENT "Proof" -> { VernacShow ShowProof } + | IDENT "Show"; IDENT "Intro" -> { VernacShow (ShowIntros false) } + | IDENT "Show"; IDENT "Intros" -> { VernacShow (ShowIntros true) } + | IDENT "Show"; IDENT "Match"; id = reference -> { VernacShow (ShowMatch id) } + | IDENT "Guarded" -> { VernacCheckGuard } + (* Hints for Auto and EAuto *) + | IDENT "Create"; IDENT "HintDb" ; + id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] -> + { VernacCreateHintDb (id, b) } + | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> + { VernacRemoveHints (dbnames, ids) } + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> + { VernacHints (dbnames, h) } + ] ]; + reference_or_constr: + [ [ r = global -> { HintsReference r } + | c = constr -> { HintsConstr c } ] ] + ; + hint: + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + { HintsResolve (List.map (fun x -> (info, true, x)) lc) } + | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural -> + { HintsResolveIFF (true, lc, n) } + | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> + { HintsResolveIFF (false, lc, n) } + | IDENT "Immediate"; lc = LIST1 reference_or_constr -> { HintsImmediate lc } + | IDENT "Variables"; IDENT "Transparent" -> { HintsTransparency (HintsVariables, true) } + | IDENT "Variables"; IDENT "Opaque" -> { HintsTransparency (HintsVariables, false) } + | IDENT "Constants"; IDENT "Transparent" -> { HintsTransparency (HintsConstants, true) } + | IDENT "Constants"; IDENT "Opaque" -> { HintsTransparency (HintsConstants, false) } + | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, true) } + | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, false) } + | IDENT "Mode"; l = global; m = mode -> { HintsMode (l, m) } + | IDENT "Unfold"; lqid = LIST1 global -> { HintsUnfold lqid } + | IDENT "Constructors"; lc = LIST1 global -> { HintsConstructors lc } ] ] + ; + constr_body: + [ [ ":="; c = lconstr -> { c } + | ":"; t = lconstr; ":="; c = lconstr -> { CAst.make ~loc @@ CCast(c,CastConv t) } ] ] + ; + mode: + [ [ l = LIST1 [ "+" -> { ModeInput } + | "!" -> { ModeNoHeadEvar } + | "-" -> { ModeOutput } ] -> { l } ] ] + ; +END diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 deleted file mode 100644 index 16934fc868..0000000000 --- a/vernac/g_vernac.ml4 +++ /dev/null @@ -1,1156 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Glob_term -open Vernacexpr -open Constrexpr -open Constrexpr_ops -open Extend -open Decl_kinds -open Declaremods -open Declarations -open Namegen -open Tok (* necessary for camlp5 *) - -open Pcoq -open Pcoq.Prim -open Pcoq.Constr -open Pcoq.Module -open Pvernac.Vernac_ - -let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - -(* Rem: do not join the different GEXTEND into one, it breaks native *) -(* compilation on PowerPC and Sun architectures *) - -let query_command = Gram.entry_create "vernac:query_command" - -let subprf = Gram.entry_create "vernac:subprf" - -let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" -let thm_token = Gram.entry_create "vernac:thm_token" -let def_body = Gram.entry_create "vernac:def_body" -let decl_notation = Gram.entry_create "vernac:decl_notation" -let record_field = Gram.entry_create "vernac:record_field" -let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" - -let make_bullet s = - let open Proof_bullet in - let n = String.length s in - match s.[0] with - | '-' -> Dash n - | '+' -> Plus n - | '*' -> Star n - | _ -> assert false - -let parse_compat_version ?(allow_old = true) = let open Flags in function - | "8.8" -> Current - | "8.7" -> V8_7 - | "8.6" -> V8_6 - | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - CErrors.user_err ~hdr:"get_compat_version" - Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> - CErrors.user_err ~hdr:"get_compat_version" - Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") - -GEXTEND Gram - GLOBAL: vernac_control gallina_ext noedit_mode subprf; - vernac_control: FIRST - [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c) - | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) - | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) - | IDENT "Fail"; v = vernac_control -> VernacFail v - | (f, v) = vernac -> VernacExpr(f, v) ] - ] - ; - vernac: - [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v) - | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v) - - | v = vernac_poly -> v ] - ] - ; - vernac_poly: - [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v) - | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v) - | v = vernac_aux -> v ] - ] - ; - vernac_aux: - (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) - (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g) - | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g) - | g = gallina; "." -> ([], g) - | g = gallina_ext; "." -> ([], g) - | c = command; "." -> ([], c) - | c = syntax; "." -> ([], c) - | c = subprf -> ([], c) - ] ] - ; - vernac_aux: LAST - [ [ prfcom = command_entry -> ([], prfcom) ] ] - ; - noedit_mode: - [ [ c = query_command -> c None] ] - ; - - subprf: - [ [ s = BULLET -> VernacBullet (make_bullet s) - | "{" -> VernacSubproof None - | "}" -> VernacEndSubproof - ] ] - ; - - located_vernac: - [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ] - ; -END - -let warn_plural_command = - CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled - (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) - -let test_plural_form loc kwd = function - | [(_,([_],_))] -> - warn_plural_command ~loc:!@loc kwd - | _ -> () - -let test_plural_form_types loc kwd = function - | [([_],_)] -> - warn_plural_command ~loc:!@loc kwd - | _ -> () - -let lname_of_lident : lident -> lname = - CAst.map (fun s -> Name s) - -let name_of_ident_decl : ident_decl -> name_decl = - on_fst lname_of_lident - -(* Gallina declarations *) -GEXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl univ_decl; - - gallina: - (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr; - l = LIST0 - [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr -> - (id,(bl,c)) ] -> - VernacStartTheoremProof (thm, (id,(bl,c))::l) - | stre = assumption_token; nl = inline; bl = assum_list -> - VernacAssumption (stre, nl, bl) - | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> - test_plural_form loc kwd bl; - VernacAssumption (stre, nl, bl) - | d = def_token; id = ident_decl; b = def_body -> - VernacDefinition (d, name_of_ident_decl id, b) - | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) - (* Gallina inductive declarations *) - | cum = OPT cumulativity_token; priv = private_token; f = finite_token; - indl = LIST1 inductive_definition SEP "with" -> - let (k,f) = f in - let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (cum, priv,f,indl) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (NoDischarge, recs) - | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (DoDischarge, recs) - | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (NoDischarge, corecs) - | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (DoDischarge, corecs) - | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l - | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; - l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) - | IDENT "Register"; IDENT "Inline"; id = identref -> - VernacRegister(id, RegisterInline) - | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l - | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l - | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l - ] ] - ; - - thm_token: - [ [ "Theorem" -> Theorem - | IDENT "Lemma" -> Lemma - | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark - | IDENT "Corollary" -> Corollary - | IDENT "Proposition" -> Proposition - | IDENT "Property" -> Property ] ] - ; - def_token: - [ [ "Definition" -> (NoDischarge,Definition) - | IDENT "Example" -> (NoDischarge,Example) - | IDENT "SubClass" -> (NoDischarge,SubClass) ] ] - ; - assumption_token: - [ [ "Hypothesis" -> (DoDischarge, Logical) - | "Variable" -> (DoDischarge, Definitional) - | "Axiom" -> (NoDischarge, Logical) - | "Parameter" -> (NoDischarge, Definitional) - | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ] - ; - assumptions_token: - [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical)) - | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional)) - | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical)) - | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional)) - | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ] - ; - inline: - [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) - | IDENT "Inline" -> DefaultInline - | -> NoInline] ] - ; - univ_constraint: - [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = universe_level -> (l, ord, r) ] ] - ; - univ_decl : - [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ]; - cs = [ "|"; l' = LIST0 univ_constraint SEP ","; - ext = [ "+" -> true | -> false ]; "}" -> (l',ext) - | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] - -> - let open UState in - { univdecl_instance = l; - univdecl_extensible_instance = ext; - univdecl_constraints = fst cs; - univdecl_extensible_constraints = snd cs } - ] ] - ; - ident_decl: - [ [ i = identref; l = OPT univ_decl -> (i, l) - ] ] - ; - finite_token: - [ [ IDENT "Inductive" -> (Inductive_kw,Finite) - | IDENT "CoInductive" -> (CoInductive,CoFinite) - | IDENT "Variant" -> (Variant,BiFinite) - | IDENT "Record" -> (Record,BiFinite) - | IDENT "Structure" -> (Structure,BiFinite) - | IDENT "Class" -> (Class true,BiFinite) ] ] - ; - cumulativity_token: - [ [ IDENT "Cumulative" -> VernacCumulative - | IDENT "NonCumulative" -> VernacNonCumulative ] ] - ; - private_token: - [ [ IDENT "Private" -> true | -> false ] ] - ; - (* Simple definitions *) - def_body: - [ [ bl = binders; ":="; red = reduce; c = lconstr -> - if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = mkCLambdaN ~loc:!@loc bl c in - DefineBody ([], red, c, None) - else - (match c with - | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) - | _ -> DefineBody (bl, red, c, None)) - | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - let ((bl, c), tyo) = - if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in - (([],mkCLambdaN ~loc:!@loc bl c), None) - else ((bl, c), Some t) - in - DefineBody (bl, red, c, tyo) - | bl = binders; ":"; t = lconstr -> - ProveBody (bl, t) ] ] - ; - reduce: - [ [ IDENT "Eval"; r = red_expr; "in" -> Some r - | -> None ] ] - ; - one_decl_notation: - [ [ ntn = ne_lstring; ":="; c = constr; - scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] - ; - decl_notation: - [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l - | -> [] ] ] - ; - (* Inductives and records *) - opt_constructors_or_fields: - [ [ ":="; lc = constructor_list_or_record_decl -> lc - | -> RecordDecl (None, []) ] ] - ; - inductive_definition: - [ [ oc = opt_coercion; id = ident_decl; indpar = binders; - c = OPT [ ":"; c = lconstr -> c ]; - lc=opt_constructors_or_fields; ntn = decl_notation -> - (((oc,id),indpar,c,lc),ntn) ] ] - ; - constructor_list_or_record_decl: - [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> - Constructors ((c id)::l) - | id = identref ; c = constructor_type -> Constructors [ c id ] - | cstr = identref; "{"; fs = record_fields; "}" -> - RecordDecl (Some cstr,fs) - | "{";fs = record_fields; "}" -> RecordDecl (None,fs) - | -> Constructors [] ] ] - ; -(* - csort: - [ [ s = sort -> CSort (loc,s) ] ] - ; -*) - opt_coercion: - [ [ ">" -> true - | -> false ] ] - ; - (* (co)-fixpoints *) - rec_definition: - [ [ id = ident_decl; - bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> - let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] - ; - corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> - ((id,bl,ty,def),ntn) ] ] - ; - type_cstr: - [ [ ":"; c=lconstr -> c - | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ] - ; - (* Inductive schemes *) - scheme: - [ [ kind = scheme_kind -> (None,kind) - | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] - ; - scheme_kind: - [ [ IDENT "Induction"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) - | IDENT "Minimality"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) - | IDENT "Elimination"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) - | IDENT "Case"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) - | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] - ; - (* Various Binders *) -(* - (* ... without coercions *) - binder_nodef: - [ [ b = binder_let -> - (match b with - CLocalAssum(l,ty) -> (l,ty) - | CLocalDef _ -> - Util.user_err_loc - (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] - ; -*) - (* ... with coercions *) - record_field: - [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; - ntn = decl_notation -> (bd,pri),ntn ] ] - ; - record_fields: - [ [ f = record_field; ";"; fs = record_fields -> f :: fs - | f = record_field; ";" -> [f] - | f = record_field -> [f] - | -> [] - ] ] - ; - record_binder_body: - [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN ~loc:!@loc l t)) - | l = binders; oc = of_type_with_opt_coercion; - t = lconstr; ":="; b = lconstr -> fun id -> - (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t))) - | l = binders; ":="; b = lconstr -> fun id -> - match b.CAst.v with - | CCast(b', (CastConv t|CastVM t|CastNative t)) -> - (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t))) - | _ -> - (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] - ; - record_binder: - [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) - | id = name; f = record_binder_body -> f id ] ] - ; - assum_list: - [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] - ; - assum_coe: - [ [ "("; a = simple_assum_coe; ")" -> a ] ] - ; - simple_assum_coe: - [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr -> - (not (Option.is_empty oc),(idl,c)) ] ] - ; - - constructor_type: - [[ l = binders; - t= [ coe = of_type_with_opt_coercion; c = lconstr -> - fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) - | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ] - -> t l - ]] -; - - constructor: - [ [ id = identref; c=constructor_type -> c id ] ] - ; - of_type_with_opt_coercion: - [ [ ":>>" -> Some false - | ":>"; ">" -> Some false - | ":>" -> Some true - | ":"; ">"; ">" -> Some false - | ":"; ">" -> Some true - | ":" -> None ] ] - ; -END - -let only_starredidentrefs = - Gram.Entry.of_parser "test_only_starredidentrefs" - (fun strm -> - let rec aux n = - match Util.stream_nth n strm with - | KEYWORD "." -> () - | KEYWORD ")" -> () - | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) - | _ -> raise Stream.Failure in - aux 0) -let starredidentreflist_to_expr l = - match l with - | [] -> SsEmpty - | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x - -let warn_deprecated_include_type = - CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" - (fun () -> strbrk "Include Type is deprecated; use Include instead") - -(* Modules and Sections *) -GEXTEND Gram - GLOBAL: gallina_ext module_expr module_type section_subset_expr; - - gallina_ext: - [ [ (* Interactive module declaration *) - IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; sign = of_module_type; - body = is_module_expr -> - VernacDefineModule (export, id, bl, sign, body) - | IDENT "Module"; "Type"; id = identref; - bl = LIST0 module_binder; sign = check_module_types; - body = is_module_type -> - VernacDeclareModuleType (id, bl, sign, body) - | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; ":"; mty = module_type_inl -> - VernacDeclareModule (export, id, bl, mty) - (* Section beginning *) - | IDENT "Section"; id = identref -> VernacBeginSection id - | IDENT "Chapter"; id = identref -> VernacBeginSection id - - (* This end a Section a Module or a Module Type *) - | IDENT "End"; id = identref -> VernacEndSegment id - - (* Naming a set of section hyps *) - | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> - VernacNameSectionHypSet (id, expr) - - (* Requiring an already compiled module *) - | IDENT "Require"; export = export_token; qidl = LIST1 global -> - VernacRequire (None, export, qidl) - | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token - ; qidl = LIST1 global -> - VernacRequire (Some ns, export, qidl) - | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) - | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> - VernacInclude(e::l) - | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - warn_deprecated_include_type ~loc:!@loc (); - VernacInclude(e::l) ] ] - ; - export_token: - [ [ IDENT "Import" -> Some false - | IDENT "Export" -> Some true - | -> None ] ] - ; - ext_module_type: - [ [ "<+"; mty = module_type_inl -> mty ] ] - ; - ext_module_expr: - [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ] - ; - check_module_type: - [ [ "<:"; mty = module_type_inl -> mty ] ] - ; - check_module_types: - [ [ mtys = LIST0 check_module_type -> mtys ] ] - ; - of_module_type: - [ [ ":"; mty = module_type_inl -> Enforce mty - | mtys = check_module_types -> Check mtys ] ] - ; - is_module_type: - [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l) - | -> [] ] ] - ; - is_module_expr: - [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) - | -> [] ] ] - ; - functor_app_annot: - [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> - InlineAt (int_of_string i) - | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline - | -> DefaultInline - ] ] - ; - module_expr_inl: - [ [ "!"; me = module_expr -> (me,NoInline) - | me = module_expr; a = functor_app_annot -> (me,a) ] ] - ; - module_type_inl: - [ [ "!"; me = module_type -> (me,NoInline) - | me = module_type; a = functor_app_annot -> (me,a) ] ] - ; - (* Module binder *) - module_binder: - [ [ "("; export = export_token; idl = LIST1 identref; ":"; - mty = module_type_inl; ")" -> (export,idl,mty) ] ] - ; - (* Module expressions *) - module_expr: - [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2) - ] ] - ; - module_expr_atom: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ] - ; - with_declaration: - [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> - CWith_Definition (fqid,udecl,c) - | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> - CWith_Module (fqid,qid) - ] ] - ; - module_type: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid - | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> - CAst.make ~loc:!@loc @@ CMapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> - CAst.make ~loc:!@loc @@ CMwith (mty,decl) - ] ] - ; - (* Proof using *) - section_subset_expr: - [ [ only_starredidentrefs; l = LIST0 starredidentref -> - starredidentreflist_to_expr l - | e = ssexpr -> e ]] - ; - starredidentref: - [ [ i = identref -> SsSingl i - | i = identref; "*" -> SsFwdClose(SsSingl i) - | "Type" -> SsType - | "Type"; "*" -> SsFwdClose SsType ]] - ; - ssexpr: - [ "35" - [ "-"; e = ssexpr -> SsCompl e ] - | "50" - [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) - | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] - | "0" - [ i = starredidentref -> i - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> - starredidentreflist_to_expr l - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> - SsFwdClose(starredidentreflist_to_expr l) - | "("; e = ssexpr; ")"-> e - | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ] - ; -END - -(* Extensions: implicits, coercions, etc. *) -GEXTEND Gram - GLOBAL: gallina_ext instance_name hint_info; - - gallina_ext: - [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 smart_global -> - VernacSetOpacity (Conv_oracle.transparent, l) - | IDENT "Opaque"; l = LIST1 smart_global -> - VernacSetOpacity (Conv_oracle.Opaque, l) - | IDENT "Strategy"; l = - LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> - VernacSetStrategy l - (* Canonical structure *) - | IDENT "Canonical"; IDENT "Structure"; qid = global -> - VernacCanonical CAst.(make ~loc:!@loc @@ AN qid) - | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> - VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn) - | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> - let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) - - (* Coercions *) - | IDENT "Coercion"; qid = global; d = def_body -> - let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) - | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (f, s, t) - | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; - t = class_rawexpr -> - VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t) - | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; - t = class_rawexpr -> - VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - - | IDENT "Context"; c = LIST1 binder -> - VernacContext (List.flatten c) - - | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - info = hint_info ; - props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | - ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) - - | IDENT "Existing"; IDENT "Instance"; id = global; - info = hint_info -> - VernacDeclareInstances [id, info] - - | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in - let insts = List.map (fun i -> (i, info)) ids in - VernacDeclareInstances insts - - | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is - - (* Arguments *) - | IDENT "Arguments"; qid = smart_global; - args = LIST0 argument_spec_block; - more_implicits = OPT - [ ","; impl = LIST1 - [ impl = LIST0 more_implicits_block -> List.flatten impl] - SEP "," -> impl - ]; - mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> - let mods = match mods with None -> [] | Some l -> List.flatten l in - let slash_position = ref None in - let rec parse_args i = function - | [] -> [] - | `Id x :: args -> x :: parse_args (i+1) args - | `Slash :: args -> - if Option.is_empty !slash_position then - (slash_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"/\" modifier can occur only once") - in - let args = parse_args 0 (List.flatten args) in - let more_implicits = Option.default [] more_implicits in - VernacArguments (qid, args, more_implicits, !slash_position, mods) - - | IDENT "Implicit"; "Type"; bl = reserv_list -> - VernacReserve bl - - | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plural_form_types loc "Implicit Types" bl; - VernacReserve bl - - | IDENT "Generalizable"; - gen = [IDENT "All"; IDENT "Variables" -> Some [] - | IDENT "No"; IDENT "Variables" -> None - | ["Variable" | IDENT "Variables"]; - idl = LIST1 identref -> Some idl ] -> - VernacGeneralizable gen ] ] - ; - arguments_modifier: - [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase] - | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold] - | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] - | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] - | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] - | IDENT "rename" -> [`Rename] - | IDENT "assert" -> [`Assert] - | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] - | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> - [`ClearImplicits; `ClearScopes] - | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> - [`ClearImplicits; `ClearScopes] - ] ] - ; - scope: - [ [ "%"; key = IDENT -> key ] ] - ; - argument_spec: [ - [ b = OPT "!"; id = name ; s = OPT scope -> - id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s - ] - ]; - (* List of arguments implicit status, scope, modifiers *) - argument_spec_block: [ - [ item = argument_spec -> - let name, recarg_like, notation_scope = item in - [`Id { name=name; recarg_like=recarg_like; - notation_scope=notation_scope; - implicit_status = NotImplicit}] - | "/" -> [`Slash] - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = NotImplicit}) items - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = Implicit}) items - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = MaximallyImplicit}) items - ] - ]; - (* Same as [argument_spec_block], but with only implicit status and names *) - more_implicits_block: [ - [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)] - | "["; items = LIST1 name; "]" -> - List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items - | "{"; items = LIST1 name; "}" -> - List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items - ] - ]; - strategy_level: - [ [ IDENT "expand" -> Conv_oracle.Expand - | IDENT "opaque" -> Conv_oracle.Opaque - | n=INT -> Conv_oracle.Level (int_of_string n) - | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) - | IDENT "transparent" -> Conv_oracle.transparent ] ] - ; - instance_name: - [ [ name = ident_decl; sup = OPT binders -> - (CAst.map (fun id -> Name id) (fst name), snd name), - (Option.default [] sup) - | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ] - ; - hint_info: - [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> - { Typeclasses.hint_priority = i; hint_pattern = pat } - | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ] - ; - reserv_list: - [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] - ; - reserv_tuple: - [ [ "("; a = simple_reserv; ")" -> a ] ] - ; - simple_reserv: - [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ] - ; - -END - -GEXTEND Gram - GLOBAL: command query_command class_rawexpr gallina_ext; - - gallina_ext: - [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> - VernacSetOption (true, table, v) - | IDENT "Export"; IDENT "Unset"; table = option_table -> - VernacUnsetOption (true, table) - ] ]; - - command: - [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l - - (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) - | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - info = hint_info -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) - - (* System directory *) - | IDENT "Pwd" -> VernacChdir None - | IDENT "Cd" -> VernacChdir None - | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) - - | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; - s = [ s = ne_string -> s | s = IDENT -> s ] -> - VernacLoad (verbosely, s) - | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> - VernacDeclareMLModule l - - | IDENT "Locate"; l = locatable -> VernacLocate l - - (* Managing load paths *) - | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> - VernacAddLoadPath (false, dir, alias) - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; - alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) - | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> - VernacRemoveLoadPath dir - - (* For compatibility *) - | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> - VernacAddLoadPath (false, dir, alias) - | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> - VernacAddLoadPath (true, dir, alias) - | IDENT "DelPath"; dir = ne_string -> - VernacRemoveLoadPath dir - - (* Type-Checking (pas dans le refman) *) - | "Type"; c = lconstr -> VernacGlobalCheck c - - (* Printing (careful factorization of entries) *) - | IDENT "Print"; p = printable -> VernacPrint p - | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l)) - | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> - VernacPrint (PrintModuleType qid) - | IDENT "Print"; IDENT "Module"; qid = global -> - VernacPrint (PrintModule qid) - | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> - VernacPrint (PrintNamespace ns) - | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) - - | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - VernacAddMLPath (false, dir) - | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - VernacAddMLPath (true, dir) - - (* For acting on parameter tables *) - | "Set"; table = option_table; v = option_value -> - VernacSetOption (false, table, v) - | IDENT "Unset"; table = option_table -> - VernacUnsetOption (false, table) - - | IDENT "Print"; IDENT "Table"; table = option_table -> - VernacPrintOption table - - | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value - -> VernacAddOption ([table;field], v) - (* A global value below will be hidden by a field above! *) - (* In fact, we give priority to secondary tables *) - (* No syntax for tertiary tables due to conflict *) - (* (but they are unused anyway) *) - | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> - VernacAddOption ([table], v) - - | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value - -> VernacMemOption (table, v) - | IDENT "Test"; table = option_table -> - VernacPrintOption table - - | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value - -> VernacRemoveOption ([table;field], v) - | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption ([table], v) ]] - ; - query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Compute"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) - | IDENT "Check"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (None, g, c) - (* Searching the environment *) - | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> - fun g -> VernacPrint (PrintAbout (qid,l,g)) - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchHead c,g, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchPattern c,g, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchRewrite c,g, l) - | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> - let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchAbout sl,g, l) - ] ] - ; - printable: - [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l) - | IDENT "All" -> PrintFullContext - | IDENT "Section"; s = global -> PrintSectionContext s - | IDENT "Grammar"; ent = IDENT -> - (* This should be in "syntax" section but is here for factorization*) - PrintGrammar ent - | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir - | IDENT "Modules" -> - user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") - | IDENT "Libraries" -> PrintModules - - | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath - | IDENT "ML"; IDENT "Modules" -> PrintMLModules - | IDENT "Debug"; IDENT "GC" -> PrintDebugGC - | IDENT "Graph" -> PrintGraph - | IDENT "Classes" -> PrintClasses - | IDENT "TypeClasses" -> PrintTypeClasses - | IDENT "Instances"; qid = smart_global -> PrintInstances qid - | IDENT "Coercions" -> PrintCoercions - | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr - -> PrintCoercionPaths (s,t) - | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions - | IDENT "Tables" -> PrintTables - | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) - | IDENT "Hint" -> PrintHintGoal - | IDENT "Hint"; qid = smart_global -> PrintHint qid - | IDENT "Hint"; "*" -> PrintHintDb - | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | IDENT "Scopes" -> PrintScopes - | IDENT "Scope"; s = IDENT -> PrintScope s - | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s - | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid - | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt) - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt) - | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid) - | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid) - | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid) - | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) - | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid) - | IDENT "Strategies" -> PrintStrategy None ] ] - ; - class_rawexpr: - [ [ IDENT "Funclass" -> FunClass - | IDENT "Sortclass" -> SortClass - | qid = smart_global -> RefClass qid ] ] - ; - locatable: - [ [ qid = smart_global -> LocateAny qid - | IDENT "Term"; qid = smart_global -> LocateTerm qid - | IDENT "File"; f = ne_string -> LocateFile f - | IDENT "Library"; qid = global -> LocateLibrary qid - | IDENT "Module"; qid = global -> LocateModule qid ] ] - ; - option_value: - [ [ -> BoolValue true - | n = integer -> IntValue (Some n) - | s = STRING -> StringValue s ] ] - ; - option_ref_value: - [ [ id = global -> QualidRefValue id - | s = STRING -> StringRefValue s ] ] - ; - option_table: - [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] - ; - as_dirpath: - [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] - ; - ne_in_or_out_modules: - [ [ IDENT "inside"; l = LIST1 global -> SearchInside l - | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ] - ; - in_or_out_modules: - [ [ m = ne_in_or_out_modules -> m - | -> SearchOutside [] ] ] - ; - comment: - [ [ c = constr -> CommentConstr c - | s = STRING -> CommentString s - | n = natural -> CommentInt n ] ] - ; - positive_search_mark: - [ [ "-" -> false | -> true ] ] - ; - scope: - [ [ "%"; key = IDENT -> key ] ] - ; - searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> - (b, SearchString (s,sc)) - | b = positive_search_mark; p = constr_pattern -> - (b, SearchSubPattern p) - ] ] - ; - searchabout_queries: - [ [ m = ne_in_or_out_modules -> ([],m) - | s = searchabout_query; l = searchabout_queries -> - let (sl,m) = l in (s::sl,m) - | -> ([],SearchOutside []) - ] ] - ; - univ_name_list: - [ [ "@{" ; l = LIST0 name; "}" -> l ] ] - ; -END; - -GEXTEND Gram - command: - [ [ -(* State management *) - IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s - | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s - | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s - | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s - -(* Resetting *) - | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial - | IDENT "Reset"; id = identref -> VernacResetName id - | IDENT "Back" -> VernacBack 1 - | IDENT "Back"; n = natural -> VernacBack n - | IDENT "BackTo"; n = natural -> VernacBackTo n - -(* Tactic Debugger *) - | IDENT "Debug"; IDENT "On" -> - VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) - - | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) - -(* registration of a custom reduction *) - - | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; - r = red_expr -> - VernacDeclareReduction (s,r) - - ] ]; - END -;; - -(* Grammar extensions *) - -GEXTEND Gram - GLOBAL: syntax; - - syntax: - [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (true,sc) - - | IDENT "Close"; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (false,sc) - - | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc, Some key) - | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> - VernacDelimiters (sc, None) - - | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; - refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - - | IDENT "Infix"; op = ne_lstring; ":="; p = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; - sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix ((op,modl),p,sc) - | IDENT "Notation"; id = identref; - idl = LIST0 ident; ":="; c = constr; b = only_parsing -> - VernacSyntacticDefinition - (id,(idl,c),b) - | IDENT "Notation"; s = lstring; ":="; - c = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; - sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (c,(s,modl),sc) - | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> - VernacNotationAddFormat (n,s,fmt) - - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - let s = CAst.map (fun s -> "x '"^s^"' y") s in - VernacSyntaxExtension (true,(s,l)) - - | IDENT "Reserved"; IDENT "Notation"; - s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (false, (s,l)) - - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) - ] ] - ; - only_parsing: - [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> - Some Flags.Current - | "("; IDENT "compat"; s = STRING; ")" -> - Some (parse_compat_version s) - | -> None ] ] - ; - level: - [ [ IDENT "level"; n = natural -> NumLevel n - | IDENT "next"; IDENT "level" -> NextLevel ] ] - ; - syntax_modifier: - [ [ "at"; IDENT "level"; n = natural -> SetLevel n - | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA - | IDENT "right"; IDENT "associativity" -> SetAssoc RightA - | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "printing" -> SetOnlyPrinting - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing - | IDENT "compat"; s = STRING -> - SetCompatVersion (parse_compat_version s) - | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s]; - s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] -> - begin match s1, s2 with - | { CAst.v = k }, Some s -> SetFormat(k,s) - | s, None -> SetFormat ("text",s) end - | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; - lev = level -> SetItemLevel (x::l,lev) - | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) - | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) - | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) - ] ] - ; - syntax_extension_type: - [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference - | IDENT "bigint" -> ETBigint - | IDENT "binder" -> ETBinder true - | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n) - | IDENT "pattern" -> ETPattern (false,None) - | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n) - | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None) - | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n) - | IDENT "closed"; IDENT "binder" -> ETBinder false - ] ] - ; - at_level: - [ [ "at"; n = level -> n ] ] - ; - constr_as_binder_kind: - [ [ "as"; IDENT "ident" -> Notation_term.AsIdent - | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern - | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ] - ; -END diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg new file mode 100644 index 0000000000..74516e320c --- /dev/null +++ b/vernac/g_vernac.mlg @@ -0,0 +1,1208 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +{ + +open Pp +open CErrors +open Util +open Names +open Glob_term +open Vernacexpr +open Constrexpr +open Constrexpr_ops +open Extend +open Decl_kinds +open Declaremods +open Declarations +open Namegen +open Tok (* necessary for camlp5 *) + +open Pcoq +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Module +open Pvernac.Vernac_ + +let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] +let _ = List.iter CLexer.add_keyword vernac_kw + +(* Rem: do not join the different GEXTEND into one, it breaks native *) +(* compilation on PowerPC and Sun architectures *) + +let query_command = Entry.create "vernac:query_command" + +let subprf = Entry.create "vernac:subprf" + +let class_rawexpr = Entry.create "vernac:class_rawexpr" +let thm_token = Entry.create "vernac:thm_token" +let def_body = Entry.create "vernac:def_body" +let decl_notation = Entry.create "vernac:decl_notation" +let record_field = Entry.create "vernac:record_field" +let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" +let instance_name = Entry.create "vernac:instance_name" +let section_subset_expr = Entry.create "vernac:section_subset_expr" + +let make_bullet s = + let open Proof_bullet in + let n = String.length s in + match s.[0] with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false + +let parse_compat_version = let open Flags in function + | "8.8" -> Current + | "8.7" -> V8_7 + | "8.6" -> V8_6 + | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + +} + +GRAMMAR EXTEND Gram + GLOBAL: vernac_control gallina_ext noedit_mode subprf; + vernac_control: FIRST + [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) } + | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) } + | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) } + | IDENT "Fail"; v = vernac_control -> { VernacFail v } + | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ] + ] + ; + decorated_vernac: + [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) } + | fv = vernac -> { fv } ] + ] + ; + attributes: + [ [ "#[" ; a = attribute_list ; "]" -> { a } ] + ] + ; + attribute_list: + [ [ a = LIST0 attribute SEP "," -> { a } ] + ] + ; + attribute: + [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ] + ] + ; + attribute_value: + [ [ "=" ; v = string -> { VernacFlagLeaf v } + | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } + | -> { VernacFlagEmpty } ] + ] + ; + vernac: + [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) } + | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) } + + | v = vernac_poly -> { v } ] + ] + ; + vernac_poly: + [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (("polymorphic", VernacFlagEmpty) :: f, v) } + | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (("monomorphic", VernacFlagEmpty) :: f, v) } + | v = vernac_aux -> { v } ] + ] + ; + vernac_aux: + (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) + (* "." is still in the stream and discard_to_dot works correctly *) + [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) } + | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) } + | g = gallina; "." -> { ([], g) } + | g = gallina_ext; "." -> { ([], g) } + | c = command; "." -> { ([], c) } + | c = syntax; "." -> { ([], c) } + | c = subprf -> { ([], c) } + ] ] + ; + vernac_aux: LAST + [ [ prfcom = command_entry -> { ([], prfcom) } ] ] + ; + noedit_mode: + [ [ c = query_command -> { c None } ] ] + ; + + subprf: + [ [ s = BULLET -> { VernacBullet (make_bullet s) } + | "{" -> { VernacSubproof None } + | "}" -> { VernacEndSubproof } + ] ] + ; + + located_vernac: + [ [ v = vernac_control -> { CAst.make ~loc v } ] ] + ; +END + +{ + +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function + | [(_,([_],_))] -> + warn_plural_command ~loc kwd + | _ -> () + +let test_plural_form_types loc kwd = function + | [([_],_)] -> + warn_plural_command ~loc kwd + | _ -> () + +let lname_of_lident : lident -> lname = + CAst.map (fun s -> Name s) + +let name_of_ident_decl : ident_decl -> name_decl = + on_fst lname_of_lident + +} + +(* Gallina declarations *) +GRAMMAR EXTEND Gram + GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion + record_field decl_notation rec_definition ident_decl univ_decl; + + gallina: + (* Definition, Theorem, Variable, Axiom, ... *) + [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr; + l = LIST0 + [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr -> + { (id,(bl,c)) } ] -> + { VernacStartTheoremProof (thm, (id,(bl,c))::l) } + | stre = assumption_token; nl = inline; bl = assum_list -> + { VernacAssumption (stre, nl, bl) } + | tk = assumptions_token; nl = inline; bl = assum_list -> + { let (kwd,stre) = tk in + test_plural_form loc kwd bl; + VernacAssumption (stre, nl, bl) } + | d = def_token; id = ident_decl; b = def_body -> + { VernacDefinition (d, name_of_ident_decl id, b) } + | IDENT "Let"; id = identref; b = def_body -> + { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) } + (* Gallina inductive declarations *) + | cum = OPT cumulativity_token; priv = private_token; f = finite_token; + indl = LIST1 inductive_definition SEP "with" -> + { let (k,f) = f in + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in + VernacInductive (cum, priv,f,indl) } + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + { VernacFixpoint (NoDischarge, recs) } + | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + { VernacFixpoint (DoDischarge, recs) } + | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + { VernacCoFixpoint (NoDischarge, corecs) } + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + { VernacCoFixpoint (DoDischarge, corecs) } + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l } + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } + | IDENT "Register"; IDENT "Inline"; id = identref -> + { VernacRegister(id, RegisterInline) } + | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l } + | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l } + | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l } + ] ] + ; + + thm_token: + [ [ "Theorem" -> { Theorem } + | IDENT "Lemma" -> { Lemma } + | IDENT "Fact" -> { Fact } + | IDENT "Remark" -> { Remark } + | IDENT "Corollary" -> { Corollary } + | IDENT "Proposition" -> { Proposition } + | IDENT "Property" -> { Property } ] ] + ; + def_token: + [ [ "Definition" -> { (NoDischarge,Definition) } + | IDENT "Example" -> { (NoDischarge,Example) } + | IDENT "SubClass" -> { (NoDischarge,SubClass) } ] ] + ; + assumption_token: + [ [ "Hypothesis" -> { (DoDischarge, Logical) } + | "Variable" -> { (DoDischarge, Definitional) } + | "Axiom" -> { (NoDischarge, Logical) } + | "Parameter" -> { (NoDischarge, Definitional) } + | IDENT "Conjecture" -> { (NoDischarge, Conjectural) } ] ] + ; + assumptions_token: + [ [ IDENT "Hypotheses" -> { ("Hypotheses", (DoDischarge, Logical)) } + | IDENT "Variables" -> { ("Variables", (DoDischarge, Definitional)) } + | IDENT "Axioms" -> { ("Axioms", (NoDischarge, Logical)) } + | IDENT "Parameters" -> { ("Parameters", (NoDischarge, Definitional)) } + | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ] + ; + inline: + [ [ IDENT "Inline"; "("; i = INT; ")" -> { InlineAt (int_of_string i) } + | IDENT "Inline" -> { DefaultInline } + | -> { NoInline } ] ] + ; + univ_constraint: + [ [ l = universe_level; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ]; + r = universe_level -> { (l, ord, r) } ] ] + ; + univ_decl : + [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ]; + cs = [ "|"; l' = LIST0 univ_constraint SEP ","; + ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) } + | ext = [ "}" -> { true } | "|}" -> { false } ] -> { ([], ext) } ] + -> + { let open UState in + { univdecl_instance = l; + univdecl_extensible_instance = ext; + univdecl_constraints = fst cs; + univdecl_extensible_constraints = snd cs } } + ] ] + ; + ident_decl: + [ [ i = identref; l = OPT univ_decl -> { (i, l) } + ] ] + ; + finite_token: + [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) } + | IDENT "CoInductive" -> { (CoInductive,CoFinite) } + | IDENT "Variant" -> { (Variant,BiFinite) } + | IDENT "Record" -> { (Record,BiFinite) } + | IDENT "Structure" -> { (Structure,BiFinite) } + | IDENT "Class" -> { (Class true,BiFinite) } ] ] + ; + cumulativity_token: + [ [ IDENT "Cumulative" -> { VernacCumulative } + | IDENT "NonCumulative" -> { VernacNonCumulative } ] ] + ; + private_token: + [ [ IDENT "Private" -> { true } | -> { false } ] ] + ; + (* Simple definitions *) + def_body: + [ [ bl = binders; ":="; red = reduce; c = lconstr -> + { if List.exists (function CLocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = mkCLambdaN ~loc bl c in + DefineBody ([], red, c, None) + else + (match c with + | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) + | _ -> DefineBody (bl, red, c, None)) } + | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> + { let ((bl, c), tyo) = + if List.exists (function CLocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = CAst.make ~loc @@ CCast (c, CastConv t) in + (([],mkCLambdaN ~loc bl c), None) + else ((bl, c), Some t) + in + DefineBody (bl, red, c, tyo) } + | bl = binders; ":"; t = lconstr -> + { ProveBody (bl, t) } ] ] + ; + reduce: + [ [ IDENT "Eval"; r = red_expr; "in" -> { Some r } + | -> { None } ] ] + ; + one_decl_notation: + [ [ ntn = ne_lstring; ":="; c = constr; + scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,scopt) } ] ] + ; + decl_sep: + [ [ IDENT "and" -> { () } ] ] + ; + decl_notation: + [ [ "where"; l = LIST1 one_decl_notation SEP decl_sep -> { l } + | -> { [] } ] ] + ; + (* Inductives and records *) + opt_constructors_or_fields: + [ [ ":="; lc = constructor_list_or_record_decl -> { lc } + | -> { RecordDecl (None, []) } ] ] + ; + inductive_definition: + [ [ oc = opt_coercion; id = ident_decl; indpar = binders; + c = OPT [ ":"; c = lconstr -> { c } ]; + lc=opt_constructors_or_fields; ntn = decl_notation -> + { (((oc,id),indpar,c,lc),ntn) } ] ] + ; + constructor_list_or_record_decl: + [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } + | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + { Constructors ((c id)::l) } + | id = identref ; c = constructor_type -> { Constructors [ c id ] } + | cstr = identref; "{"; fs = record_fields; "}" -> + { RecordDecl (Some cstr,fs) } + | "{";fs = record_fields; "}" -> { RecordDecl (None,fs) } + | -> { Constructors [] } ] ] + ; +(* + csort: + [ [ s = sort -> CSort (loc,s) ] ] + ; +*) + opt_coercion: + [ [ ">" -> { true } + | -> { false } ] ] + ; + (* (co)-fixpoints *) + rec_definition: + [ [ id = ident_decl; + bl = binders_fixannot; + ty = type_cstr; + def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> + { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + ; + corec_definition: + [ [ id = ident_decl; bl = binders; ty = type_cstr; + def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> + { ((id,bl,ty,def),ntn) } ] ] + ; + type_cstr: + [ [ ":"; c=lconstr -> { c } + | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] + ; + (* Inductive schemes *) + scheme: + [ [ kind = scheme_kind -> { (None,kind) } + | id = identref; ":="; kind = scheme_kind -> { (Some id,kind) } ] ] + ; + scheme_kind: + [ [ IDENT "Induction"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> { InductionScheme(true,ind,s) } + | IDENT "Minimality"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> { InductionScheme(false,ind,s) } + | IDENT "Elimination"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> { CaseScheme(true,ind,s) } + | IDENT "Case"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> { CaseScheme(false,ind,s) } + | IDENT "Equality"; "for" ; ind = smart_global -> { EqualityScheme(ind) } ] ] + ; + (* Various Binders *) +(* + (* ... without coercions *) + binder_nodef: + [ [ b = binder_let -> + (match b with + CLocalAssum(l,ty) -> (l,ty) + | CLocalDef _ -> + Util.user_err_loc + (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] + ; +*) + (* ... with coercions *) + record_field: + [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> { n } ]; + ntn = decl_notation -> { (bd,pri),ntn } ] ] + ; + record_fields: + [ [ f = record_field; ";"; fs = record_fields -> { f :: fs } + | f = record_field; ";" -> { [f] } + | f = record_field -> { [f] } + | -> { [] } + ] ] + ; + record_binder_body: + [ [ l = binders; oc = of_type_with_opt_coercion; + t = lconstr -> { fun id -> (oc,AssumExpr (id,mkCProdN ~loc l t)) } + | l = binders; oc = of_type_with_opt_coercion; + t = lconstr; ":="; b = lconstr -> { fun id -> + (oc,DefExpr (id,mkCLambdaN ~loc l b,Some (mkCProdN ~loc l t))) } + | l = binders; ":="; b = lconstr -> { fun id -> + match b.CAst.v with + | CCast(b', (CastConv t|CastVM t|CastNative t)) -> + (None,DefExpr(id,mkCLambdaN ~loc l b',Some (mkCProdN ~loc l t))) + | _ -> + (None,DefExpr(id,mkCLambdaN ~loc l b,None)) } ] ] + ; + record_binder: + [ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } + | id = name; f = record_binder_body -> { f id } ] ] + ; + assum_list: + [ [ bl = LIST1 assum_coe -> { bl } | b = simple_assum_coe -> { [b] } ] ] + ; + assum_coe: + [ [ "("; a = simple_assum_coe; ")" -> { a } ] ] + ; + simple_assum_coe: + [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr -> + { (not (Option.is_empty oc),(idl,c)) } ] ] + ; + + constructor_type: + [[ l = binders; + t= [ coe = of_type_with_opt_coercion; c = lconstr -> + { fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc l c)) } + | -> + { fun l id -> (false,(id,mkCProdN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ] + -> { t l } + ]] +; + + constructor: + [ [ id = identref; c=constructor_type -> { c id } ] ] + ; + of_type_with_opt_coercion: + [ [ ":>>" -> { Some false } + | ":>"; ">" -> { Some false } + | ":>" -> { Some true } + | ":"; ">"; ">" -> { Some false } + | ":"; ">" -> { Some true } + | ":" -> { None } ] ] + ; +END + +{ + +let only_starredidentrefs = + Gram.Entry.of_parser "test_only_starredidentrefs" + (fun strm -> + let rec aux n = + match Util.stream_nth n strm with + | KEYWORD "." -> () + | KEYWORD ")" -> () + | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) + | _ -> raise Stream.Failure in + aux 0) +let starredidentreflist_to_expr l = + match l with + | [] -> SsEmpty + | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x + +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + +} + +(* Modules and Sections *) +GRAMMAR EXTEND Gram + GLOBAL: gallina_ext module_expr module_type section_subset_expr; + + gallina_ext: + [ [ (* Interactive module declaration *) + IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; sign = of_module_type; + body = is_module_expr -> + { VernacDefineModule (export, id, bl, sign, body) } + | IDENT "Module"; "Type"; id = identref; + bl = LIST0 module_binder; sign = check_module_types; + body = is_module_type -> + { VernacDeclareModuleType (id, bl, sign, body) } + | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; ":"; mty = module_type_inl -> + { VernacDeclareModule (export, id, bl, mty) } + (* Section beginning *) + | IDENT "Section"; id = identref -> { VernacBeginSection id } + | IDENT "Chapter"; id = identref -> { VernacBeginSection id } + + (* This end a Section a Module or a Module Type *) + | IDENT "End"; id = identref -> { VernacEndSegment id } + + (* Naming a set of section hyps *) + | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> + { VernacNameSectionHypSet (id, expr) } + + (* Requiring an already compiled module *) + | IDENT "Require"; export = export_token; qidl = LIST1 global -> + { VernacRequire (None, export, qidl) } + | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token + ; qidl = LIST1 global -> + { VernacRequire (Some ns, export, qidl) } + | IDENT "Import"; qidl = LIST1 global -> { VernacImport (false,qidl) } + | IDENT "Export"; qidl = LIST1 global -> { VernacImport (true,qidl) } + | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> + { VernacInclude(e::l) } + | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> + { warn_deprecated_include_type ~loc (); + VernacInclude(e::l) } ] ] + ; + export_token: + [ [ IDENT "Import" -> { Some false } + | IDENT "Export" -> { Some true } + | -> { None } ] ] + ; + ext_module_type: + [ [ "<+"; mty = module_type_inl -> { mty } ] ] + ; + ext_module_expr: + [ [ "<+"; mexpr = module_expr_inl -> { mexpr } ] ] + ; + check_module_type: + [ [ "<:"; mty = module_type_inl -> { mty } ] ] + ; + check_module_types: + [ [ mtys = LIST0 check_module_type -> { mtys } ] ] + ; + of_module_type: + [ [ ":"; mty = module_type_inl -> { Enforce mty } + | mtys = check_module_types -> { Check mtys } ] ] + ; + is_module_type: + [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> { (mty::l) } + | -> { [] } ] ] + ; + is_module_expr: + [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> { (mexpr::l) } + | -> { [] } ] ] + ; + functor_app_annot: + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + { InlineAt (int_of_string i) } + | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline } + | -> { DefaultInline } + ] ] + ; + module_expr_inl: + [ [ "!"; me = module_expr -> { (me,NoInline) } + | me = module_expr; a = functor_app_annot -> { (me,a) } ] ] + ; + module_type_inl: + [ [ "!"; me = module_type -> { (me,NoInline) } + | me = module_type; a = functor_app_annot -> { (me,a) } ] ] + ; + (* Module binder *) + module_binder: + [ [ "("; export = export_token; idl = LIST1 identref; ":"; + mty = module_type_inl; ")" -> { (export,idl,mty) } ] ] + ; + (* Module expressions *) + module_expr: + [ [ me = module_expr_atom -> { me } + | me1 = module_expr; me2 = module_expr_atom -> { CAst.make ~loc @@ CMapply (me1,me2) } + ] ] + ; + module_expr_atom: + [ [ qid = qualid -> { CAst.make ~loc @@ CMident qid } | "("; me = module_expr; ")" -> { me } ] ] + ; + with_declaration: + [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> + { CWith_Definition (fqid,udecl,c) } + | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> + { CWith_Module (fqid,qid) } + ] ] + ; + module_type: + [ [ qid = qualid -> { CAst.make ~loc @@ CMident qid } + | "("; mt = module_type; ")" -> { mt } + | mty = module_type; me = module_expr_atom -> + { CAst.make ~loc @@ CMapply (mty,me) } + | mty = module_type; "with"; decl = with_declaration -> + { CAst.make ~loc @@ CMwith (mty,decl) } + ] ] + ; + (* Proof using *) + section_subset_expr: + [ [ only_starredidentrefs; l = LIST0 starredidentref -> + { starredidentreflist_to_expr l } + | e = ssexpr -> { e } ]] + ; + starredidentref: + [ [ i = identref -> { SsSingl i } + | i = identref; "*" -> { SsFwdClose(SsSingl i) } + | "Type" -> { SsType } + | "Type"; "*" -> { SsFwdClose SsType } ]] + ; + ssexpr: + [ "35" + [ "-"; e = ssexpr -> { SsCompl e } ] + | "50" + [ e1 = ssexpr; "-"; e2 = ssexpr-> { SsSubstr(e1,e2) } + | e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ] + | "0" + [ i = starredidentref -> { i } + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + { starredidentreflist_to_expr l } + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + { SsFwdClose(starredidentreflist_to_expr l) } + | "("; e = ssexpr; ")"-> { e } + | "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ] + ; +END + +(* Extensions: implicits, coercions, etc. *) +GRAMMAR EXTEND Gram + GLOBAL: gallina_ext instance_name hint_info; + + gallina_ext: + [ [ (* Transparent and Opaque *) + IDENT "Transparent"; l = LIST1 smart_global -> + { VernacSetOpacity (Conv_oracle.transparent, l) } + | IDENT "Opaque"; l = LIST1 smart_global -> + { VernacSetOpacity (Conv_oracle.Opaque, l) } + | IDENT "Strategy"; l = + LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] -> + { VernacSetStrategy l } + (* Canonical structure *) + | IDENT "Canonical"; IDENT "Structure"; qid = global -> + { VernacCanonical CAst.(make ~loc @@ AN qid) } + | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> + { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) } + | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> + { let s = coerce_reference_to_id qid in + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) } + + (* Coercions *) + | IDENT "Coercion"; qid = global; d = def_body -> + { let s = coerce_reference_to_id qid in + VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) } + | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; + s = class_rawexpr; ">->"; t = class_rawexpr -> + { VernacIdentityCoercion (f, s, t) } + | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; + t = class_rawexpr -> + { VernacCoercion (CAst.make ~loc @@ AN qid, s, t) } + | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; + t = class_rawexpr -> + { VernacCoercion (CAst.make ~loc @@ ByNotation ntn, s, t) } + + | IDENT "Context"; c = LIST1 binder -> + { VernacContext (List.flatten c) } + + | IDENT "Instance"; namesup = instance_name; ":"; + expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + info = hint_info ; + props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } | + ":="; c = lconstr -> { Some (false,c) } | -> { None } ] -> + { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) } + + | IDENT "Existing"; IDENT "Instance"; id = global; + info = hint_info -> + { VernacDeclareInstances [id, info] } + + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; + pri = OPT [ "|"; i = natural -> { i } ] -> + { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts } + + | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is } + + (* Arguments *) + | IDENT "Arguments"; qid = smart_global; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> { List.flatten impl } ] + SEP "," -> { impl } + ]; + mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] -> + { let mods = match mods with None -> [] | Some l -> List.flatten l in + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + user_err Pp.(str "The \"/\" modifier can occur only once") + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) } + + | IDENT "Implicit"; "Type"; bl = reserv_list -> + { VernacReserve bl } + + | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> + { test_plural_form_types loc "Implicit Types" bl; + VernacReserve bl } + + | IDENT "Generalizable"; + gen = [IDENT "All"; IDENT "Variables" -> { Some [] } + | IDENT "No"; IDENT "Variables" -> { None } + | ["Variable" -> { () } | IDENT "Variables" -> { () } ]; + idl = LIST1 identref -> { Some idl } ] -> + { VernacGeneralizable gen } ] ] + ; + arguments_modifier: + [ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] } + | IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] } + | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] } + | IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] } + | IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] } + | IDENT "rename" -> { [`Rename] } + | IDENT "assert" -> { [`Assert] } + | IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] } + | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> + { [`ClearImplicits; `ClearScopes] } + | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> + { [`ClearImplicits; `ClearScopes] } + ] ] + ; + scope: + [ [ "%"; key = IDENT -> { key } ] ] + ; + argument_spec: [ + [ b = OPT "!"; id = name ; s = OPT scope -> + { id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc x) s } + ] + ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + { let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = NotImplicit}] } + | "/" -> { [`Slash] } + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + { let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = NotImplicit}) items } + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + { let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = Implicit}) items } + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + { let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items } + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ name = name -> { [(name.CAst.v, Vernacexpr.NotImplicit)] } + | "["; items = LIST1 name; "]" -> + { List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items } + | "{"; items = LIST1 name; "}" -> + { List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items } + ] + ]; + strategy_level: + [ [ IDENT "expand" -> { Conv_oracle.Expand } + | IDENT "opaque" -> { Conv_oracle.Opaque } + | n=INT -> { Conv_oracle.Level (int_of_string n) } + | "-"; n=INT -> { Conv_oracle.Level (- int_of_string n) } + | IDENT "transparent" -> { Conv_oracle.transparent } ] ] + ; + instance_name: + [ [ name = ident_decl; sup = OPT binders -> + { (CAst.map (fun id -> Name id) (fst name), snd name), + (Option.default [] sup) } + | -> { ((CAst.make ~loc Anonymous), None), [] } ] ] + ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { { Typeclasses.hint_priority = i; hint_pattern = pat } } + | -> { { Typeclasses.hint_priority = None; hint_pattern = None } } ] ] + ; + reserv_list: + [ [ bl = LIST1 reserv_tuple -> { bl } | b = simple_reserv -> { [b] } ] ] + ; + reserv_tuple: + [ [ "("; a = simple_reserv; ")" -> { a } ] ] + ; + simple_reserv: + [ [ idl = LIST1 identref; ":"; c = lconstr -> { (idl,c) } ] ] + ; + +END + +GRAMMAR EXTEND Gram + GLOBAL: command query_command class_rawexpr gallina_ext; + + gallina_ext: + [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + { VernacSetOption (true, table, v) } + | IDENT "Export"; IDENT "Unset"; table = option_table -> + { VernacUnsetOption (true, table) } + ] ]; + + command: + [ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l } + + (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) + | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; + expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200"; + info = hint_info -> + { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + + (* System directory *) + | IDENT "Pwd" -> { VernacChdir None } + | IDENT "Cd" -> { VernacChdir None } + | IDENT "Cd"; dir = ne_string -> { VernacChdir (Some dir) } + + | IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ]; + s = [ s = ne_string -> { s } | s = IDENT -> { s } ] -> + { VernacLoad (verbosely, s) } + | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> + { VernacDeclareMLModule l } + + | IDENT "Locate"; l = locatable -> { VernacLocate l } + + (* Managing load paths *) + | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> + { VernacAddLoadPath (false, dir, alias) } + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; + alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) } + | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> + { VernacRemoveLoadPath dir } + + (* For compatibility *) + | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> + { VernacAddLoadPath (false, dir, alias) } + | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> + { VernacAddLoadPath (true, dir, alias) } + | IDENT "DelPath"; dir = ne_string -> + { VernacRemoveLoadPath dir } + + (* Type-Checking (pas dans le refman) *) + | "Type"; c = lconstr -> { VernacGlobalCheck c } + + (* Printing (careful factorization of entries) *) + | IDENT "Print"; p = printable -> { VernacPrint p } + | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacPrint (PrintName (qid,l)) } + | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> + { VernacPrint (PrintModuleType qid) } + | IDENT "Print"; IDENT "Module"; qid = global -> + { VernacPrint (PrintModule qid) } + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + { VernacPrint (PrintNamespace ns) } + | IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) } + + | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> + { VernacAddMLPath (false, dir) } + | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> + { VernacAddMLPath (true, dir) } + + (* For acting on parameter tables *) + | "Set"; table = option_table; v = option_value -> + { VernacSetOption (false, table, v) } + | IDENT "Unset"; table = option_table -> + { VernacUnsetOption (false, table) } + + | IDENT "Print"; IDENT "Table"; table = option_table -> + { VernacPrintOption table } + + | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value + -> { VernacAddOption ([table;field], v) } + (* A global value below will be hidden by a field above! *) + (* In fact, we give priority to secondary tables *) + (* No syntax for tertiary tables due to conflict *) + (* (but they are unused anyway) *) + | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> + { VernacAddOption ([table], v) } + + | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value + -> { VernacMemOption (table, v) } + | IDENT "Test"; table = option_table -> + { VernacPrintOption table } + + | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value + -> { VernacRemoveOption ([table;field], v) } + | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> + { VernacRemoveOption ([table], v) } ]] + ; + query_command: (* TODO: rapprocher Eval et Check *) + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> + { fun g -> VernacCheckMayEval (Some r, g, c) } + | IDENT "Compute"; c = lconstr; "." -> + { fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) } + | IDENT "Check"; c = lconstr; "." -> + { fun g -> VernacCheckMayEval (None, g, c) } + (* Searching the environment *) + | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> + { fun g -> VernacPrint (PrintAbout (qid,l,g)) } + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> + { fun g -> VernacSearch (SearchHead c,g, l) } + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> + { fun g -> VernacSearch (SearchPattern c,g, l) } + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> + { fun g -> VernacSearch (SearchRewrite c,g, l) } + | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> + { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) } + (* compatibility: SearchAbout *) + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> + { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } + (* compatibility: SearchAbout with "[ ... ]" *) + | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; + l = in_or_out_modules; "." -> + { fun g -> VernacSearch (SearchAbout sl,g, l) } + ] ] + ; + printable: + [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> { PrintName (qid,l) } + | IDENT "All" -> { PrintFullContext } + | IDENT "Section"; s = global -> { PrintSectionContext s } + | IDENT "Grammar"; ent = IDENT -> + (* This should be in "syntax" section but is here for factorization*) + { PrintGrammar ent } + | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir } + | IDENT "Modules" -> + { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") } + | IDENT "Libraries" -> { PrintModules } + + | IDENT "ML"; IDENT "Path" -> { PrintMLLoadPath } + | IDENT "ML"; IDENT "Modules" -> { PrintMLModules } + | IDENT "Debug"; IDENT "GC" -> { PrintDebugGC } + | IDENT "Graph" -> { PrintGraph } + | IDENT "Classes" -> { PrintClasses } + | IDENT "TypeClasses" -> { PrintTypeClasses } + | IDENT "Instances"; qid = smart_global -> { PrintInstances qid } + | IDENT "Coercions" -> { PrintCoercions } + | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr + -> { PrintCoercionPaths (s,t) } + | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Tables" -> { PrintTables } + | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } + | IDENT "Hint" -> { PrintHintGoal } + | IDENT "Hint"; qid = smart_global -> { PrintHint qid } + | IDENT "Hint"; "*" -> { PrintHintDb } + | IDENT "HintDb"; s = IDENT -> { PrintHintDbName s } + | IDENT "Scopes" -> { PrintScopes } + | IDENT "Scope"; s = IDENT -> { PrintScope s } + | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s } + | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid } + | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) } + | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) } + | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) } + | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) } + | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } + | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) } + | IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) } + | IDENT "Strategies" -> { PrintStrategy None } ] ] + ; + class_rawexpr: + [ [ IDENT "Funclass" -> { FunClass } + | IDENT "Sortclass" -> { SortClass } + | qid = smart_global -> { RefClass qid } ] ] + ; + locatable: + [ [ qid = smart_global -> { LocateAny qid } + | IDENT "Term"; qid = smart_global -> { LocateTerm qid } + | IDENT "File"; f = ne_string -> { LocateFile f } + | IDENT "Library"; qid = global -> { LocateLibrary qid } + | IDENT "Module"; qid = global -> { LocateModule qid } ] ] + ; + option_value: + [ [ -> { BoolValue true } + | n = integer -> { IntValue (Some n) } + | s = STRING -> { StringValue s } ] ] + ; + option_ref_value: + [ [ id = global -> { QualidRefValue id } + | s = STRING -> { StringRefValue s } ] ] + ; + option_table: + [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]] + ; + as_dirpath: + [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ] + ; + ne_in_or_out_modules: + [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l } + | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ] + ; + in_or_out_modules: + [ [ m = ne_in_or_out_modules -> { m } + | -> { SearchOutside [] } ] ] + ; + comment: + [ [ c = constr -> { CommentConstr c } + | s = STRING -> { CommentString s } + | n = natural -> { CommentInt n } ] ] + ; + positive_search_mark: + [ [ "-" -> { false } | -> { true } ] ] + ; + scope: + [ [ "%"; key = IDENT -> { key } ] ] + ; + searchabout_query: + [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> + { (b, SearchString (s,sc)) } + | b = positive_search_mark; p = constr_pattern -> + { (b, SearchSubPattern p) } + ] ] + ; + searchabout_queries: + [ [ m = ne_in_or_out_modules -> { ([],m) } + | s = searchabout_query; l = searchabout_queries -> + { let (sl,m) = l in (s::sl,m) } + | -> { ([],SearchOutside []) } + ] ] + ; + univ_name_list: + [ [ "@{" ; l = LIST0 name; "}" -> { l } ] ] + ; +END + +GRAMMAR EXTEND Gram + GLOBAL: command; + + command: + [ [ +(* State management *) + IDENT "Write"; IDENT "State"; s = IDENT -> { VernacWriteState s } + | IDENT "Write"; IDENT "State"; s = ne_string -> { VernacWriteState s } + | IDENT "Restore"; IDENT "State"; s = IDENT -> { VernacRestoreState s } + | IDENT "Restore"; IDENT "State"; s = ne_string -> { VernacRestoreState s } + +(* Resetting *) + | IDENT "Reset"; IDENT "Initial" -> { VernacResetInitial } + | IDENT "Reset"; id = identref -> { VernacResetName id } + | IDENT "Back" -> { VernacBack 1 } + | IDENT "Back"; n = natural -> { VernacBack n } + | IDENT "BackTo"; n = natural -> { VernacBackTo n } + +(* Tactic Debugger *) + | IDENT "Debug"; IDENT "On" -> + { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) } + + | IDENT "Debug"; IDENT "Off" -> + { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) } + +(* registration of a custom reduction *) + + | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; + r = red_expr -> + { VernacDeclareReduction (s,r) } + +(* factorized here, though relevant for syntax extensions *) + + | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT -> + { VernacDeclareCustomEntry s } + + ] ]; + END + +(* Grammar extensions *) + +GRAMMAR EXTEND Gram + GLOBAL: syntax; + + syntax: + [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> + { VernacOpenCloseScope (true,sc) } + + | IDENT "Close"; IDENT "Scope"; sc = IDENT -> + { VernacOpenCloseScope (false,sc) } + + | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> + { VernacDelimiters (sc, Some key) } + | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> + { VernacDelimiters (sc, None) } + + | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; + refl = LIST1 class_rawexpr -> { VernacBindScope (sc,refl) } + + | IDENT "Infix"; op = ne_lstring; ":="; p = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]; + sc = OPT [ ":"; sc = IDENT -> { sc } ] -> + { VernacInfix ((op,modl),p,sc) } + | IDENT "Notation"; id = identref; + idl = LIST0 ident; ":="; c = constr; b = only_parsing -> + { VernacSyntacticDefinition + (id,(idl,c),b) } + | IDENT "Notation"; s = lstring; ":="; + c = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]; + sc = OPT [ ":"; sc = IDENT -> { sc } ] -> + { VernacNotation (c,(s,modl),sc) } + | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> + { VernacNotationAddFormat (n,s,fmt) } + + | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; + l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> + { let s = CAst.map (fun s -> "x '"^s^"' y") s in + VernacSyntaxExtension (true,(s,l)) } + + | IDENT "Reserved"; IDENT "Notation"; + s = ne_lstring; + l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] + -> { VernacSyntaxExtension (false, (s,l)) } + + (* "Print" "Grammar" should be here but is in "command" entry in order + to factorize with other "Print"-based vernac entries *) + ] ] + ; + only_parsing: + [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> + { Some Flags.Current } + | "("; IDENT "compat"; s = STRING; ")" -> + { Some (parse_compat_version s) } + | -> { None } ] ] + ; + level: + [ [ IDENT "level"; n = natural -> { NumLevel n } + | IDENT "next"; IDENT "level" -> { NextLevel } ] ] + ; + syntax_modifier: + [ [ "at"; IDENT "level"; n = natural -> { SetLevel n } + | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) } + | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural -> + { SetCustomEntry (x,Some n) } + | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA } + | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA } + | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA } + | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting } + | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing } + | IDENT "compat"; s = STRING -> + { SetCompatVersion (parse_compat_version s) } + | IDENT "format"; s1 = [s = STRING -> { CAst.make ~loc s } ]; + s2 = OPT [s = STRING -> { CAst.make ~loc s } ] -> + { begin match s1, s2 with + | { CAst.v = k }, Some s -> SetFormat(k,s) + | s, None -> SetFormat ("text",s) end } + | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; + lev = level -> { SetItemLevel (x::l,None,Some lev) } + | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) } + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> + { SetItemLevel ([x],Some b,Some lev) } + | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) } + | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } + ] ] + ; + syntax_extension_type: + [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } + | IDENT "bigint" -> { ETBigint } + | IDENT "binder" -> { ETBinder true } + | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) } + | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } + | IDENT "pattern" -> { ETPattern (false,None) } + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) } + | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) } + | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) } + | IDENT "closed"; IDENT "binder" -> { ETBinder false } + | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind -> + { ETConstr (InCustomEntry x,b,n) } + ] ] + ; + at_level: + [ [ "at"; n = level -> { n } ] ] + ; + constr_as_binder_kind: + [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } + | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern } + | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ] + ; +END diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5d671ef529..b9c47ff475 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -194,12 +194,6 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let pr_puniverses f env (c,u) = - f env c ++ - (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then - str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" - else mt()) - let explain_elim_arity env sigma ind sorts c pj okinds = let open EConstr in let env = make_all_name_different env sigma in @@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty = let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ spc () ++ strbrk "the branch for constructor" ++ spc () ++ - quote (pr_puniverses pr_constructor env ci) ++ + quote (pr_pconstructor env sigma ci) ++ spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." @@ -520,11 +514,15 @@ let pr_trailing_ne_context_of env sigma = then str "." else (str " in environment:"++ pr_context_unlimited env sigma) -let rec explain_evar_kind env sigma evk ty = function +let rec explain_evar_kind env sigma evk ty = + let open Evar_kinds in + function | Evar_kinds.NamedHole id -> strbrk "the existential variable named " ++ Id.print id - | Evar_kinds.QuestionMark _ -> + | Evar_kinds.QuestionMark {qm_record_field=None} -> strbrk "this placeholder of type " ++ ty + | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} -> + str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname) | Evar_kinds.CasesType false -> strbrk "the type of this pattern-matching problem" | Evar_kinds.CasesType true -> @@ -871,9 +869,6 @@ let explain_not_match_error = function pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" - | NoTypeConstraintExpected -> - strbrk "a definition whose type is constrained can only be subtype " ++ - strbrk "of a definition whose type is itself constrained" | CumulativeStatusExpected b -> let status b = if b then str"cumulative" else str"non-cumulative" in str "a " ++ status b ++ str" declaration was expected, but a " ++ @@ -1232,12 +1227,7 @@ let explain_wrong_numarg_inductive env ind n = str " expects " ++ decline_string n "argument" ++ str "." let explain_unused_clause env pats = -(* Without localisation - let s = if List.length pats > 1 then "s" else "" in - (str ("Unused clause with pattern"^s) ++ spc () ++ - hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")") -*) - str "This clause is redundant." + str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause." let explain_non_exhaustive env pats = str "Non exhaustive pattern-matching: no clause found for " ++ diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 1d38075022..91caddcf13 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t val explain_typeclass_error : env -> typeclass_error -> Pp.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef5..d66a121437 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -49,7 +49,7 @@ let entry_buf = Buffer.create 64 let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Pcoq.Gram.entry_print ft e in + let () = Pcoq.Entry.print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = @@ -283,20 +283,30 @@ let error_not_same_scope x y = (**********************************************************************) (* Build pretty-printing rules *) +let pr_notation_entry = function + | InConstrEntry -> str "constr" + | InCustomEntry s -> str "custom " ++ str s + let prec_assoc = function | RightA -> (L,E) | LeftA -> (E,L) | NonA -> (L,L) -let precedence_of_position_and_level from = function +let precedence_of_position_and_level from_level = function | NumLevel n, BorderProd (_,None) -> n, Prec n | NumLevel n, BorderProd (b,Some a) -> n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp | NumLevel n, InternalProd -> n, Prec n - | NextLevel, _ -> from, L - -let precedence_of_entry_type from = function - | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x + | NextLevel, _ -> from_level, L + +let precedence_of_entry_type (from_custom,from_level) = function + | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> + precedence_of_position_and_level from_level x + | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n + | ETConstr (custom,_,(NextLevel,_)) -> + user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++ + quote (pr_notation_entry custom) ++ strbrk " is different from " ++ + quote (pr_notation_entry from_custom) ++ str ").") | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n | _ -> 0, E (* should not matter *) @@ -367,15 +377,14 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = snd (precedence_of_entry_type from x) in match x with - | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint -> + | ETConstr _ | ETGlobal | ETBigint -> UnpMetaVar (i,prec) | ETPattern _ -> UnpBinderMetaVar (i,prec) - | ETName -> - UnpBinderMetaVar (i,Prec 0) + | ETIdent -> + UnpBinderMetaVar (i,prec) | ETBinder isopen -> assert false - | ETOther _ -> failwith "TODO" (* Heuristics for building default printing rules *) @@ -487,6 +496,15 @@ and check_no_ldots_in_box = function let error_not_same ?loc () = user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".") +let find_prod_list_loc sfmt fmt = + (* [fmt] is some [UnpTerminal x :: sfmt @ UnpTerminal ".." :: sfmt @ UnpTerminal y :: rest] *) + if List.is_empty sfmt then + (* No separators; we highlight the sequence "x .." *) + Loc.merge_opt (fst (List.hd fmt)) (fst (List.hd (List.tl fmt))) + else + (* A separator; we highlight the separating sequence *) + Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) + let skip_var_in_recursive_format = function | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> (* To do, though not so important: check that the names match @@ -496,6 +514,8 @@ let skip_var_in_recursive_format = function | [] -> assert false let read_recursive_format sl fmt = + (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) + (* into [(some-list,rest)] *) let get_head fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in @@ -528,10 +548,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in - let slfmt,fmt = read_recursive_format sl fmt in - let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) (); - let symbs, l = aux (symbs,fmt) in + let loc_slfmt,rfmt = read_recursive_format sl fmt in + let sl, slfmt = aux (sl,loc_slfmt) in + if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); + let symbs, l = aux (symbs,rfmt) in let hunk = match typ with | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) | ETBinder isopen -> @@ -550,11 +570,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = (**********************************************************************) (* Build parsing rules *) -let assoc_of_type n (_,typ) = precedence_of_entry_type n typ +let assoc_of_type from n (_,typ) = precedence_of_entry_type (from,n) typ let is_not_small_constr = function ETProdConstr _ -> true - | ETProdOther("constr","binder_constr") -> true | _ -> false let rec define_keywords_aux = function @@ -584,9 +603,9 @@ let distribute a ll = List.map (fun l -> a @ l) ll t;sep;t;...;t;sep;t;...;t;sep;t (p+n times) t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) -let expand_list_rule typ tkl x n p ll = +let expand_list_rule s typ tkl x n p ll = let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_message_name) in + let main = GramConstrNonTerminal (ETProdConstr (s,typ), camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll @@ -602,7 +621,7 @@ let expand_list_rule typ tkl x n p ll = let is_constr_typ typ x etyps = match List.assoc x etyps with - | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ' + | ETConstr (_,_,typ') -> typ = typ' | _ -> false let include_possible_similar_trailing_pattern typ etyps sl l = @@ -616,13 +635,12 @@ let include_possible_similar_trailing_pattern typ etyps sl l = try_aux 0 l let prod_entry_type = function - | ETName -> ETProdName - | ETReference -> ETProdReference + | ETIdent -> ETProdName + | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint | ETBinder _ -> assert false (* See check_binder_type *) - | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p + | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) - | ETOther (s,t) -> ETProdOther (s,t) let make_production etyps symbols = let rec aux = function @@ -640,9 +658,9 @@ let make_production etyps symbols = | Break _ -> [] | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in match List.assoc x etyps with - | ETConstr typ -> + | ETConstr (s,_,typ) -> let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in - expand_list_rule typ tkl x 1 p (aux l') + expand_list_rule s typ tkl x 1 p (aux l') | ETBinder o -> check_open_binder o sl x; let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in @@ -664,8 +682,7 @@ let rec find_symbols c_current c_next c_last = function (x,c_next)::(find_symbols c_next c_next c_last sl') let border = function - | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a - | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a + | (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a | _ -> None let recompute_assoc typs = @@ -687,23 +704,24 @@ let pr_arg_level from (lev,typ) = | (n,_) -> str "Unknown level" in Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ (match typ with - | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev + | ETConstr _ | ETPattern _ -> spc () ++ pplev lev | _ -> mt ()) -let pr_level ntn (from,args,typs) = - str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ - prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs) +let pr_level ntn (from,fromlevel,args,typs) = + (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ + str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++ + prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs) let error_incompatible_level ntn oldprec prec = user_err - (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++ + (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") let error_parsing_incompatible_level ntn ntn' oldprec prec = user_err - (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++ + (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++ str " which is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ @@ -727,7 +745,7 @@ type syntax_extension_obj = locality_flag * syntax_extension let check_and_extend_constr_grammar ntn rule = try let ntn_for_grammar = rule.notgram_notation in - if String.equal ntn ntn_for_grammar then raise Not_found; + if notation_eq ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; @@ -749,7 +767,7 @@ let cache_one_syntax_extension se = if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram + ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram end let cache_syntax_extension (_, (_, sy)) = @@ -786,7 +804,9 @@ module NotationMods = struct type notation_modifier = { assoc : gram_assoc option; level : int option; + custom : notation_entry; etyps : (Id.t * simple_constr_prod_entry_key) list; + subtyps : (Id.t * production_level) list; (* common to syn_data below *) only_parsing : bool; @@ -799,7 +819,9 @@ type notation_modifier = { let default = { assoc = None; level = None; + custom = InConstrEntry; etyps = []; + subtyps = []; only_parsing = false; only_printing = false; compat = None; @@ -810,53 +832,75 @@ let default = { end let interp_modifiers modl = let open NotationMods in - let rec interp acc = function - | [] -> acc + let rec interp subtyps acc = function + | [] -> subtyps, acc | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id acc.etyps then user_err ~hdr:"Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); - interp { acc with etyps = (id,typ) :: acc.etyps; } l - | SetItemLevel ([],n) :: l -> - interp acc l - | SetItemLevelAsBinder ([],_,_) :: l -> - interp acc l - | SetItemLevel (s::idl,n) :: l -> + interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l + | SetItemLevel ([],bko,n) :: l -> + interp subtyps acc l + | SetItemLevel (s::idl,bko,n) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id acc.etyps then user_err ~hdr:"Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); - let typ = ETConstr (Some n) in - interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l) - | SetItemLevelAsBinder (s::idl,bk,n) :: l -> - let id = Id.of_string s in - if Id.List.mem_assoc id acc.etyps then - user_err ~hdr:"Metasyntax.interp_modifiers" - (str s ++ str " is already assigned to an entry or constr level."); - let typ = ETConstrAsBinder (bk,n) in - interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l) + interp ((id,bko,n)::subtyps) acc (SetItemLevel (idl,bko,n)::l) | SetLevel n :: l -> - interp { acc with level = Some n; } l + (match acc.custom with + | InCustomEntry s -> + if acc.level <> None then + user_err (str ("isolated \"at level " ^ string_of_int n ^ "\" unexpected.")) + else + user_err (str ("use \"in custom " ^ s ^ " at level " ^ string_of_int n ^ + "\"") ++ spc () ++ str "rather than" ++ spc () ++ + str ("\"at level " ^ string_of_int n ^ "\"") ++ + spc () ++ str "isolated.") + | InConstrEntry -> + if acc.level <> None then + user_err (str "A level is already assigned."); + interp subtyps { acc with level = Some n; } l) + | SetCustomEntry (s,n) :: l -> + if acc.level <> None then + (if n = None then + user_err (str ("use \"in custom " ^ s ^ " at level " ^ + string_of_int (Option.get acc.level) ^ + "\"") ++ spc () ++ str "rather than" ++ spc () ++ + str ("\"at level " ^ + string_of_int (Option.get acc.level) ^ "\"") ++ + spc () ++ str "isolated.") + else + user_err (str ("isolated \"at level " ^ string_of_int (Option.get acc.level) ^ "\" unexpected."))); + if acc.custom <> InConstrEntry then + user_err (str "Entry is already assigned to custom " ++ str s ++ (match acc.level with None -> mt () | Some lev -> str " at level " ++ int lev) ++ str "."); + interp subtyps { acc with custom = InCustomEntry s; level = n } l | SetAssoc a :: l -> if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); - interp { acc with assoc = Some a; } l + interp subtyps { acc with assoc = Some a; } l | SetOnlyParsing :: l -> - interp { acc with only_parsing = true; } l + interp subtyps { acc with only_parsing = true; } l | SetOnlyPrinting :: l -> - interp { acc with only_printing = true; } l + interp subtyps { acc with only_printing = true; } l | SetCompatVersion v :: l -> - interp { acc with compat = Some v; } l + interp subtyps { acc with compat = Some v; } l | SetFormat ("text",s) :: l -> if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once."); - interp { acc with format = Some s; } l - | SetFormat (k,{CAst.v=s}) :: l -> - interp { acc with extra = (k,s)::acc.extra; } l - in interp default modl + interp subtyps { acc with format = Some s; } l + | SetFormat (k,s) :: l -> + interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l + in + let subtyps,mods = interp [] default modl in + (* interpret item levels wrt to main entry *) + let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in + { mods with etyps = extra_etyps@mods.etyps } let check_infix_modifiers modifiers = - let t = (interp_modifiers modifiers).NotationMods.etyps in - if not (List.is_empty t) then + let mods = interp_modifiers modifiers in + let t = mods.NotationMods.etyps in + let u = mods.NotationMods.subtyps in + if not (List.is_empty t) || not (List.is_empty u) then user_err Pp.(str "Explicit entry level or type unexpected in infix notation.") let check_useless_entry_types recvars mainvars etyps = @@ -897,21 +941,18 @@ let get_compat_version mods = (* Compute precedences from modifiers (or find default ones) *) -let set_entry_type etyps (x,typ) = +let set_entry_type from etyps (x,typ) = let typ = try match List.assoc x etyps, typ with - | ETConstr (Some n), (_,BorderProd (left,_)) -> - ETConstr (n,BorderProd (left,None)) - | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd) - | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) -> - ETConstrAsBinder (bk, (n,BorderProd (left,None))) - | ETConstrAsBinder (bk, Some n), (_,InternalProd) -> - ETConstrAsBinder (bk, (n,InternalProd)) + | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) -> + ETConstr (s,bko,(n,BorderProd (left,None))) + | ETConstr (s,bko,Some n), (_,InternalProd) -> + ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x - | ETConstr None, _ -> ETConstr typ - | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ) - with Not_found -> ETConstr typ + | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x + | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ) + with Not_found -> + ETConstr (from,None,typ) in (x,typ) let join_auxiliary_recursive_types recvars etyps = @@ -931,8 +972,8 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference - | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny + | ETConstr _ | ETBigint | ETGlobal + | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -943,20 +984,28 @@ let make_internalization_vars recvars mainvars typs = maintyps @ extratyps let make_interpretation_type isrec isonlybinding = function - | ETConstr _ -> - if isrec then NtnTypeConstrList else - if isonlybinding then - (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *) - NtnTypeBinder (NtnBinderParsedAsConstr AsIdent) - else NtnTypeConstr - | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk) - | ETName -> NtnTypeBinder NtnParsedAsIdent + (* Parsed as constr list *) + | ETConstr (_,None,_) when isrec -> NtnTypeConstrList + (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *) + | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk) + | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent) + (* Parsed as constr, interpreted as constr *) + | ETConstr (_,None,_) -> NtnTypeConstr + (* Others *) + | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETReference | ETOther _ -> NtnTypeConstr + | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") +let subentry_of_constr_prod_entry = function + | ETConstr (InCustomEntry s,_,(NumLevel n,_)) -> InCustomEntryLevel (s,n) + (* level and use of parentheses for coercion is hard-wired for "constr"; + we don't remember the level *) + | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel + | _ -> InConstrEntrySomeLevel + let make_interpretation_vars recvars allvars typs = let eq_subscope (sc1, l1) (sc2, l2) = Option.equal String.equal sc1 sc2 && @@ -972,7 +1021,9 @@ let make_interpretation_vars recvars allvars typs = let mainvars = Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in Id.Map.mapi (fun x (isonlybinding, sc) -> - (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars + let typ = Id.List.assoc x typs in + ((subentry_of_constr_prod_entry typ,sc), + make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars let check_rule_productivity l = if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then @@ -998,17 +1049,42 @@ let warn_non_reversible_notation = str " not occur in the right-hand side." ++ spc() ++ strbrk "The notation will not be used for printing as it is not reversible.") -let is_not_printable onlyparse reversibility = function -| NVar _ -> - if not onlyparse then warn_notation_bound_to_variable (); - true +let make_custom_entry custom level = + match custom with + | InConstrEntry -> InConstrEntrySomeLevel + | InCustomEntry s -> InCustomEntryLevel (s,level) + +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +let is_coercion = function + | Some (custom,n,_,[e]) -> + (match e, custom with + | ETConstr _, _ -> + let customkey = make_custom_entry custom n in + let subentry = subentry_of_constr_prod_entry e in + if notation_entry_level_eq subentry customkey then None + else Some (IsEntryCoercion subentry) + | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) + | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) + | _ -> None) + | Some _ -> assert false + | None -> None + +let printability level onlyparse reversibility = function +| NVar _ when reversibility = APrioriReversible -> + let coe = is_coercion level in + if not onlyparse && coe = None then + warn_notation_bound_to_variable (); + true, coe | _ -> - if not onlyparse && reversibility <> APrioriReversible then + (if not onlyparse && reversibility <> APrioriReversible then (warn_non_reversible_notation reversibility; true) - else onlyparse - + else onlyparse),None -let find_precedence lev etyps symbols onlyprint = +let find_precedence custom lev etyps symbols onlyprint = let first_symbol = let rec aux = function | Break _ :: t -> aux t @@ -1032,10 +1108,9 @@ let find_precedence lev etyps symbols onlyprint = else [],Option.get lev else user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in - (try match List.assoc x etyps with - | ETConstr _ -> test () - | ETConstrAsBinder (_,Some _) -> test () - | (ETName | ETBigint | ETReference) -> + (try match List.assoc x etyps, custom with + | ETConstr (s,_,Some _), s' when s = s' -> test () + | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) @@ -1044,7 +1119,7 @@ let find_precedence lev etyps symbols onlyprint = | _ -> user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end - | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) -> + | (ETPattern _ | ETBinder _ | ETConstr _), _ -> (* Give a default ? *) if Option.is_empty lev then user_err Pp.(str "Need an explicit level.") @@ -1062,7 +1137,7 @@ let find_precedence lev etyps symbols onlyprint = [],Option.get lev let check_curly_brackets_notation_exists () = - try let _ = Notgram_ops.level_of_notation "{ _ }" in () + try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in () with Not_found -> user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved.") @@ -1092,7 +1167,7 @@ let remove_curly_brackets l = module SynData = struct - type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list + type subentry_types = (Id.t * constr_entry_key) list (* XXX: Document *) type syn_data = { @@ -1126,7 +1201,7 @@ module SynData = struct end -let find_subentry_types n assoc etyps symbols = +let find_subentry_types from n assoc etyps symbols = let innerlevel = NumLevel 200 in let typs = find_symbols @@ -1134,11 +1209,21 @@ let find_subentry_types n assoc etyps symbols = (innerlevel,InternalProd) (NumLevel n,BorderProd(Right,assoc)) symbols in - let sy_typs = List.map (set_entry_type etyps) typs in - let prec = List.map (assoc_of_type n) sy_typs in + let sy_typs = List.map (set_entry_type from etyps) typs in + let prec = List.map (assoc_of_type from n) sy_typs in sy_typs, prec -let compute_syntax_data df modifiers = +let check_locality_compatibility local custom i_typs = + if not local then + let subcustom = List.map_filter (function _,ETConstr (InCustomEntry s,_,_) -> Some s | _ -> None) i_typs in + let allcustoms = match custom with InCustomEntry s -> s::subcustom | _ -> subcustom in + List.iter (fun s -> + if Egramcoq.locality_of_custom_entry s then + user_err (strbrk "Notation has to be declared local as it depends on custom entry " ++ str s ++ + strbrk " which is local.")) + (List.uniquize allcustoms) + +let compute_syntax_data local df modifiers = let open SynData in let open NotationMods in let mods = interp_modifiers modifiers in @@ -1151,25 +1236,28 @@ let compute_syntax_data df modifiers = let _ = check_binder_type recvars mods.etyps in (* Notations for interp and grammar *) - let ntn_for_interp = make_notation_key symbols in - let symbols_for_grammar = remove_curly_brackets symbols in + let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in + let custom = make_custom_entry mods.custom n in + let ntn_for_interp = make_notation_key custom symbols in + let symbols_for_grammar = + if custom = InConstrEntrySomeLevel then remove_curly_brackets symbols else symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in - let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in - if not onlyprint then check_rule_productivity symbols_for_grammar; - let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in + let ntn_for_grammar = if need_squash then make_notation_key custom symbols_for_grammar else ntn_for_interp in + if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar; (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = - find_subentry_types n assoc etyps symbols in + find_subentry_types mods.custom n assoc etyps symbols in let sy_typs_for_grammar, prec_for_grammar = if need_squash then - find_subentry_types n assoc etyps symbols_for_grammar + find_subentry_types mods.custom n assoc etyps symbols_for_grammar else sy_typs, prec in let i_typs = set_internalization_type sy_typs in + check_locality_compatibility local mods.custom sy_typs; let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in let pp_sy_data = (sy_typs,symbols) in - let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in + let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in let i_data = ntn_for_interp, df' in @@ -1188,15 +1276,15 @@ let compute_syntax_data df modifiers = mainvars; intern_typs = i_typs; - level = (n,prec,List.map snd sy_typs); + level = (mods.custom,n,prec,List.map snd sy_typs); pa_syntax_data = pa_sy_data; pp_syntax_data = pp_sy_data; not_data = sy_fulldata; } -let compute_pure_syntax_data df mods = +let compute_pure_syntax_data local df mods = let open SynData in - let sd = compute_syntax_data df mods in + let sd = compute_syntax_data local df mods in let msgs = if sd.only_parsing then (Feedback.msg_warning ?loc:None, @@ -1211,6 +1299,7 @@ type notation_obj = { notobj_local : bool; notobj_scope : scope_name option; notobj_interp : interpretation; + notobj_coercion : entry_coercion_kind option; notobj_onlyparse : bool; notobj_onlyprint : bool; notobj_compat : Flags.compat_version option; @@ -1232,7 +1321,13 @@ let open_notation i (_, nobj) = let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in (* Declare the uninterpretation *) if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat + Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat; + (* Declare a possible coercion *) + (match nobj.notobj_coercion with + | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry + | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n + | None -> ()) end let cache_notation o = @@ -1290,7 +1385,7 @@ let recover_notation_syntax ntn = raise NoSyntaxRule let recover_squash_syntax sy = - let sq = recover_notation_syntax "{ _ }" in + let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in sy :: sq.synext_notgram.notgram_rules (**********************************************************************) @@ -1312,14 +1407,22 @@ let make_pa_rule level (typs,symbols) ntn need_squash = let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] - | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + | None -> + let hunks = make_hunks typs symbols level in + if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then + [UnpBox (PpHOVB 0,hunks)] + else + (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *) + List.map snd hunks (* drop locations which are dummy *) + | Some fmt -> + hunks_of_format (level, List.split typs) (symbols, parse_format fmt) (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in + let custom,level,_,_ = sd.level in let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in - let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in { + let pp_rule = make_pp_rule (custom,level) sd.pp_syntax_data sd.format in { synext_level = sd.level; synext_notation = fst sd.info; synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; @@ -1337,7 +1440,7 @@ let to_map l = let add_notation_in_scope local df env c mods scope = let open SynData in - let sd = compute_syntax_data df mods in + let sd = compute_syntax_data local df mods in (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) let sy_rules = make_syntax_rules sd in @@ -1349,13 +1452,14 @@ let add_notation_in_scope local df env c mods scope = let (acvars, ac, reversibility) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable sd.only_parsing reversibility ac in + let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (** Order is important here! *) notobj_onlyparse = onlyparse; + notobj_coercion = coe; notobj_onlyprint = sd.only_printing; notobj_compat = sd.compat; notobj_notation = sd.info; @@ -1369,16 +1473,17 @@ let add_notation_in_scope local df env c mods scope = let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let i_typs, onlyprint = if not (is_numeral symbs) then begin - let sy = recover_notation_syntax (make_notation_key symbs) in + let level, i_typs, onlyprint = if not (is_numeral symbs) then begin + let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (** If the only printing flag has been explicitly requested, put it back *) let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in - pi3 sy.synext_level, onlyprint - end else [], false in + let _,_,_,typs = sy.synext_level in + Some sy.synext_level, typs, onlyprint + end else None, [], false in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in - let df' = (make_notation_key symbs, (path,df)) in + let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in let nenv = { ninterp_var_type = to_map i_vars; @@ -1387,13 +1492,14 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse reversibility ac in + let onlyparse,coe = printability level onlyparse reversibility ac in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (** Order is important here! *) notobj_onlyparse = onlyparse; + notobj_coercion = coe; notobj_onlyprint = onlyprint; notobj_compat = compat; notobj_notation = df'; @@ -1404,7 +1510,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in - let psd = compute_pure_syntax_data df mods in + let psd = compute_pure_syntax_data local df mods in let sy_rules = make_syntax_rules {psd with compat = None} in Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) @@ -1444,7 +1550,7 @@ let add_notation local env c ({CAst.loc;v=df},modifiers) sc = let add_notation_extra_printing_rule df k v = let notk = let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in - make_notation_key symbs in + make_notation_key InConstrEntrySomeLevel symbs in add_notation_extra_printing_rule notk k v (* Infix notations *) @@ -1528,7 +1634,35 @@ let add_syntactic_definition env ident (vars,c) local onlyparse = List.map map vars, reversibility, pat in let onlyparse = match onlyparse with - | None when (is_not_printable false reversibility pat) -> Some Flags.Current + | None when fst (printability None false reversibility pat) -> Some Flags.Current | p -> p in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) + +(**********************************************************************) +(* Declaration of custom entry *) + +let load_custom_entry _ _ = () + +let open_custom_entry _ (_,(local,s)) = + Egramcoq.create_custom_entry ~local s + +let cache_custom_entry o = + load_custom_entry 1 o; + open_custom_entry 1 o + +let subst_custom_entry (subst,x) = x + +let classify_custom_entry (local,s as o) = + if local then Dispose else Substitute o + +let inCustomEntry : locality_flag * string -> obj = + declare_object {(default_object "CUSTOM-ENTRIES") with + cache_function = cache_custom_entry; + open_function = open_custom_entry; + load_function = load_custom_entry; + subst_function = subst_custom_entry; + classify_function = classify_custom_entry} + +let declare_custom_entry local s = + Lib.add_anonymous_leaf (inCustomEntry (local,s)) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index f6de75b079..73bee7121b 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -60,3 +60,5 @@ val pr_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit val with_syntax_protection : ('a -> 'b) -> 'a -> 'b + +val declare_custom_entry : locality_flag -> string -> unit diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml index ae725efaaf..ef9cd3c351 100644 --- a/vernac/misctypes.ml +++ b/vernac/misctypes.ml @@ -17,10 +17,10 @@ type 'a or_by_notation = 'a Constrexpr.or_by_notation [@@ocaml.deprecated "use [Constrexpr.or_by_notation]"] type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr = - | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"] -[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"] + | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"] +[@@ocaml.deprecated "use [Namegen.intro_pattern_naming_expr]"] type 'a or_var = 'a Locus.or_var = | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"] diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1ab24b670b..14d7642328 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty = in let loc, k = evar_source id evm in let status = match k with - | Evar_kinds.QuestionMark (o,_) -> o + | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o | _ -> match status with | Some o -> o | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) @@ -480,10 +480,9 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let env = Global.env () in let uvars = Univ.LSet.union - (Univops.universes_of_constr env typ) - (Univops.universes_of_constr env body) in + (Univops.universes_of_constr typ) + (Univops.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -865,7 +864,7 @@ let obligation_terminator name num guard hook auto pf = else UState.union prg.prg_ctx ctx in let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in let prg_ctx = @@ -874,10 +873,12 @@ let obligation_terminator name num guard hook auto pf = polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx else - (** The first obligation declares the univs of the constant, + (** The first obligation, if defined, + declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - UState.make (Global.universes ()) + if defined then UState.make (Global.universes ()) + else ctx in let prg = { prg with prg_ctx } in try diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 56dfaa54a1..93e4e89a12 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -97,25 +97,27 @@ open Pputils let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() + let pr_notation_entry = function + | InConstrEntry -> keyword "constr" + | InCustomEntry s -> keyword "custom" ++ spc () ++ str s + let pr_at_level = function | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" let pr_constr_as_binder_kind = let open Notation_term in function - | AsIdent -> keyword "as ident" - | AsIdentOrPattern -> keyword "as pattern" - | AsStrictPattern -> keyword "as strict pattern" + | AsIdent -> spc () ++ keyword "as ident" + | AsIdentOrPattern -> spc () ++ keyword "as pattern" + | AsStrictPattern -> spc () ++ keyword "as strict pattern" let pr_strict b = if b then str "strict " else mt () let pr_set_entry_type pr = function - | ETName -> str"ident" - | ETReference -> str"global" + | ETIdent -> str"ident" + | ETGlobal -> str"global" | ETPattern (b,None) -> pr_strict b ++ str"pattern" | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) - | ETConstr lev -> str"constr" ++ pr lev - | ETOther (_,e) -> str e - | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk + | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" @@ -153,8 +155,6 @@ open Pputils | SearchAbout sl -> keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b - let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id | StringRefValue s -> qs s @@ -210,7 +210,10 @@ open Pputils | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_qualid l + ++ (match l with + | HintsVariables -> keyword "Variables" + | HintsConstants -> keyword "Constants" + | HintsReferences l -> prlist_with_sep sep pr_qualid l) | HintsMode (m, l) -> keyword "Mode" ++ spc () @@ -377,12 +380,11 @@ open Pputils let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) let pr_syntax_modifier = function - | SetItemLevel (l,n) -> - prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n - | SetItemLevelAsBinder (l,bk,n) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk + | SetItemLevel (l,bko,n) -> + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ + pr_opt pr_constr_as_binder_kind bko | SetLevel n -> pr_at_level (NumLevel n) + | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n)) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" @@ -673,6 +675,10 @@ open Pputils return ( keyword "Format Notation " ++ qs s ++ spc () ++ qs k ++ spc() ++ qs v ) + | VernacDeclareCustomEntry s -> + return ( + keyword "Declare Custom Entry " ++ str s + ) (* Gallina *) | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) @@ -1192,21 +1198,24 @@ open Pputils | VernacEndSubproof -> return (str "}") -let pr_vernac_flag = +let rec pr_vernac_flag (k, v) = + let k = keyword k in + match v with + | VernacFlagEmpty -> k + | VernacFlagLeaf v -> k ++ str " = " ++ qs v + | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" +and pr_vernac_flags m = + prlist_with_sep (fun () -> str ", ") pr_vernac_flag m + +let pr_vernac_attributes = function - | VernacPolymorphic true -> keyword "Polymorphic" - | VernacPolymorphic false -> keyword "Monomorphic" - | VernacProgram -> keyword "Program" - | VernacLocal local -> pr_locality local + | [] -> mt () + | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr (f, v') -> - List.fold_right - (fun f a -> pr_vernac_flag f ++ spc() ++ a) - f - (pr_vernac_expr v' ++ sep_end v') + | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, {v}) -> diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index f8b085f3ef..3e2bd98720 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration let known_names = Summary.ref [] ~name:"proofusing-nameset" -let in_nameset = - let open Libobject in - declare_object { (default_object "proofusing-nameset") with - cache_function = (fun (_,x) -> known_names := x :: !known_names); - classify_function = (fun _ -> Dispose); - discharge_function = (fun _ -> None) - } - let rec close_fwd e s = let s' = List.fold_left (fun s decl -> @@ -73,7 +65,7 @@ let process_expr env e ty = let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s -let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) +let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = let rec aux ids = @@ -178,7 +170,7 @@ let suggest_variable env id = let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) -let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us))) +let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) let _ = Goptions.declare_stringopt_option diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index bac8823811..b2fa8ec99f 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -10,13 +10,11 @@ open Pcoq -let uncurry f (x,y) = f x y - let uvernac = create_universe "vernac" module Vernac_ = struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + let gec_vernac s = Entry.create ("vernac:" ^ s) (* The different kinds of vernacular commands *) let gallina = gec_vernac "gallina" @@ -28,22 +26,23 @@ module Vernac_ = let red_expr = new_entry utactic "red_expr" let hint_info = gec_vernac "hint_info" (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" + let main_entry = Entry.create "vernac" let noedit_mode = gec_vernac "noedit_command" let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in + let open Extend in + let act_vernac v loc = Some (loc, v) in + let act_eoi _ loc = None in let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); + Rule (Next (Stop, Atoken Tok.EOI), act_eoi); + Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in - uncurry (Gram.extend main_entry) (None, [None, None, rule]) + Pcoq.grammar_extend main_entry None (None, [None, None, rule]) let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) end diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 2993a1661b..b2f8f71462 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -16,21 +16,21 @@ val uvernac : gram_universe module Vernac_ : sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Hints.hint_info_expr Gram.entry + val gallina : vernac_expr Entry.t + val gallina_ext : vernac_expr Entry.t + val command : vernac_expr Entry.t + val syntax : vernac_expr Entry.t + val vernac_control : vernac_control Entry.t + val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val noedit_mode : vernac_expr Entry.t + val command_entry : vernac_expr Entry.t + val red_expr : raw_red_expr Entry.t + val hint_info : Hints.hint_info_expr Entry.t end (** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry +val main_entry : (Loc.t * vernac_control) option Entry.t (** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit +val get_command_entry : unit -> vernac_expr Entry.t +val set_command_entry : vernac_expr Entry.t -> unit diff --git a/vernac/record.ml b/vernac/record.ml index a97a1662e5..6b5c538df2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -100,7 +100,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id poly pl t ps nots fs = +let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let _ = @@ -117,7 +117,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in - let sigma, typ, sort, template = match t with + let fold (sigma, template) (_, t, _, _) = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = @@ -132,28 +132,36 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match Evd.is_sort_variable sigma s' with | Some l -> let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in - sigma, s, s', true + (sigma, template), (s, s') | None -> - sigma, s, s', false - else sigma, s, s', false) + (sigma, false), (s, s') + else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in let sigma, s = Evd.new_sort_variable uvarkind sigma in - sigma, EConstr.mkSort s, s, true + (sigma, template), (EConstr.mkSort s, s) in - let arity = EConstr.it_mkProd_or_LetIn typ newps in - let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in + let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in + let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in + let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in + let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in let assums = List.filter is_local_assum newps in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params,(finite != Declarations.BiFinite)) in - let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in - let env2,sigma,impls,newfs,data = - interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) + let impls_env = + let params = List.map (RelDecl.get_name %> Name.get_id) assums in + let ty = Inductive (params, (finite != Declarations.BiFinite)) in + let ids = List.map (fun (id, _, _, _) -> id) records in + let imps = List.map (fun _ -> imps) arities in + compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps in + let fold sigma (_, _, nots, fs) arity = + let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in + (sigma, (impls, newfs)) + in + let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in - let sigma, typ = + let fold sigma (typ, sort) (_, newfs) = let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || (Sorts.is_set sort && is_impredicative_set env0)) then @@ -164,20 +172,24 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in + let (sigma, typs) = List.fold_left2_map fold sigma typs data in let sigma = Evd.minimize_universes sigma in - let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in - let typ = EConstr.to_constr sigma typ in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - List.iter (iter_constr ce) (List.rev newps); + let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let () = List.iter (iter_constr ce) (List.rev newps) in + let map (impls, newfs) typ = + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let typ = EConstr.to_constr sigma typ in List.iter (iter_constr ce) (List.rev newfs); - ubinders, univs, typ, template, imps, newps, impls, newfs + (typ, impls, newfs) + in + let ans = List.map2 map data typs in + ubinders, univs, template, newps, imps, ans let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -261,9 +273,10 @@ let subst_projection fid l c = raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' -let instantiate_possibly_recursive_type indu paramdecls fields = +let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in - Termops.substl_rel_context (subst@[mkIndU indu]) fields + let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in + Termops.substl_rel_context (subst @ subst') fields let warn_non_primitive_record = CWarnings.create ~name:"non-primitive-record" ~category:"record" @@ -281,12 +294,11 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u | Monomorphic_const_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in - let fields = instantiate_possibly_recursive_type indu paramdecls fields in + let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = if !primitive_flag then @@ -312,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u | Name fid -> try let kn, term = if is_local_assum decl && primitive then - (** Already defined in the kernel silently *) - let gr = Nametab.locate (Libnames.qualid_of_ident fid) in - let kn = destConstRef gr in + let p = Projection.Repr.make indsp + ~proj_npars:mib.mind_nparams + ~proj_arg:i + (Label.of_id fid) + in + (** Already defined by declare_mind silently *) + let kn = Projection.Repr.constant p in Declare.definition_message fid; - UnivNames.register_universe_binders gr ubinders; - kn, mkProj (Projection.make kn false,mkRel 1) + UnivNames.register_universe_binders (ConstRef kn) ubinders; + kn, mkProj (Projection.make p false,mkRel 1) else let ccl = subst_projection fid subst ti in let body = match decl with @@ -374,12 +390,9 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u open Typeclasses -let declare_structure finite ubinders univs id idbuild paramimpls params arity template - fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = - let nparams = List.length params and nfields = List.length fields in - let args = Context.Rel.to_extended_list mkRel nfields params in - let ind = applist (mkRel (1+nparams+nfields), args) in - let type_constructor = it_mkProd_or_LetIn ind fields in + +let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = + let nparams = List.length params in let template, ctx = match univs with | Monomorphic_ind_entry ctx -> @@ -389,37 +402,51 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t | Cumulative_ind_entry cumi -> false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in - let binder_name = + let binder_name = match name with - | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + | None -> + let map (id, _, _, _, _, _, _) = + Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + in + Array.map_of_list map record_data | Some n -> n in - let mie_ind = + let ntypes = List.length record_data in + let mk_block i (id, idbuild, arity, _, fields, _, _) = + let nfields = List.length fields in + let args = Context.Rel.to_extended_list mkRel nfields params in + let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in + let type_constructor = it_mkProd_or_LetIn ind fields in { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in + let blocks = List.mapi mk_block record_data in let mie = { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = Some (if !primitive_flag then Some [|binder_name|] else None); + mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; - mind_entry_inds = [mie_ind]; + mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; } in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in - let rsp = (kn,0) in (* This is ind path of idstruc *) - let cstr = (rsp,1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in - let build = ConstructRef cstr in - let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in - let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - rsp + let impls = List.map (fun _ -> paramimpls, []) record_data in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in + let map i (_, _, _, fieldimpls, fields, is_coe, coers) = + let rsp = (kn, i) in (* This is ind path of idstruc *) + let cstr = (rsp, 1) in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in + let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in + let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in + let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in + rsp + in + List.mapi map record_data let implicits_of_context ctx = List.map_i (fun i name -> @@ -431,22 +458,22 @@ let implicits_of_context ctx = 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities = + template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let len = List.length params in let impls = implicits_of_context params in List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls in - let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in - let impl, projs = + let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in + let data = match fields with | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in - let cst = Declare.declare_constant (snd id) + let cst = Declare.declare_constant id (DefinitionEntry class_entry, IsDefinition Definition) in let cstu = (cst, match univs with @@ -473,7 +500,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in - cref, [Name proj_name, sub, Some proj_cst] + [cref, [Name proj_name, sub, Some proj_cst]] | _ -> let univs = match univs with @@ -485,18 +512,21 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls - params arity template fieldimpls fields - ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) - in + let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in + let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls + params template ~kind:Method ~name:[|binder_name|] record_data + in let coers = List.map2 (fun coe pri -> Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) - (List.rev fields) coers (Recordops.lookup_projections ind) - in IndRef ind, l + let map ind = + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l + in + List.map map inds in let ctx_context = List.map (fun decl -> @@ -517,16 +547,19 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry _ -> Univ.AUContext.empty, ctx_context, fields in - let k = - { cl_univs = univs; - cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; - cl_context = ctx_context; - cl_props = fields; - cl_projs = projs } - in + let map (impl, projs) = + let k = + { cl_univs = univs; + cl_impl = impl; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in add_class k; impl + in + List.map map data let add_constant_class cst = @@ -562,48 +595,87 @@ let add_inductive_class ind = cl_unique = !typeclasses_unique } in add_class k +let warn_already_existing_class = + CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g -> + Printer.pr_global g ++ str " is already declared as a typeclass.") + let declare_existing_class g = - match g with - | ConstRef x -> add_constant_class x - | IndRef x -> add_inductive_class x - | _ -> user_err ~hdr:"declare_existing_class" - (Pp.str"Unsupported class type, only constants and inductives are allowed") + if Typeclasses.is_class g then warn_already_existing_class g + else + match g with + | ConstRef x -> add_constant_class x + | IndRef x -> add_inductive_class x + | _ -> user_err ~hdr:"declare_existing_class" + (Pp.str"Unsupported class type, only constants and inductives are allowed") open Vernacexpr -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a - list telling if the corresponding fields must me declared as coercions - or subinstances. *) -let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) = - let cfs,notations = List.split cfs in - let cfs,priorities = List.split cfs in - let coers,fs = List.split cfs in - let extract_name acc = function +let check_unique_names records = + let extract_name acc (((_, bnd), _), _) = match bnd with Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in - let allnames = idstruc::(List.fold_left extract_name [] fs) in - let () = match List.duplicates Id.equal allnames with + let allnames = + List.fold_left (fun acc (_, id, _, _, cfs, _, _) -> + id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records + in + match List.duplicates Id.equal allnames with | [] -> () | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id)) - in + +let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - user_err Pp.(str "Priorities only allowed for type class substructures"); - (* Now, younger decl in params and fields is on top *) - let pl, univs, arity, template, implpars, params, implfs, fields = + let has_priority (_, _, _, _, cfs, _, _) = + List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs + in + if isnot_class && List.exists has_priority records then + user_err Pp.(str "Priorities only allowed for type class substructures") + +let extract_record_data records = + let map (is_coe, id, _, _, cfs, idbuild, s) = + let fs = List.map (fun (((_, f), _), _) -> f) cfs in + id.CAst.v, s, List.map snd cfs, fs + in + let data = List.map map records in + let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in + let ps = match pss with + | [] -> CErrors.anomaly (str "Empty record block") + | ps :: rem -> + let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in + let () = + if not (List.for_all (eq_local_binders ps) rem) then + user_err (str "Parameters should be syntactically the \ + same for each inductive type.") + in + ps + in + (** FIXME: Same issue as #7754 *) + let _, _, pl, _, _, _, _ = List.hd records in + pl, ps, data + +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances. *) +let definition_structure kind cum poly finite records = + let () = check_unique_names records in + let () = check_priorities kind records in + let pl, ps, data = extract_record_data records in + let pl, univs, template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities + let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + | [r], [d] -> r, d + | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") + in + let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in + let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + declare_class finite def cum pl univs id.CAst.v idbuild + implpars params arity template implfs fields coers priorities | _ -> - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits - (succ (List.length params)) impls) implfs - in + let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in + let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let univs = match univs with | Polymorphic_const_entry univs -> @@ -614,7 +686,11 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure finite pl univs idstruc - idbuild implpars params arity template implfs - fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind + let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) = + let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in + id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe + in + let data = List.map2 map data records in + let inds = declare_structure finite pl univs implpars params template data in + List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index b2c039f0b5..567f2b3138 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,13 +22,18 @@ val declare_projections : bool list -> UnivNames.universe_binders -> Impargs.manual_implicits list -> - Context.Rel.t -> + Constr.rel_context -> (Name.t * bool) list * Constant.t option list val definition_structure : - inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> + Declarations.recursivity_kind -> + (coercion_flag * + Names.lident * + universe_decl_expr option * + local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> GlobRef.t + Id.t * constr_expr option) list -> + GlobRef.t list val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 609dac69aa..f842ca5ead 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -181,6 +181,10 @@ let default_tag_map () = let open Terminal in [ ; "tactic.keyword" , make ~bold:true () ; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN () ; "tactic.string" , make ~fg_color:`LIGHT_RED () + ; "diff.added" , make ~bg_color:(`RGB(0,141,0)) ~underline:true () + ; "diff.removed" , make ~bg_color:(`RGB(170,0,0)) ~underline:true () + ; "diff.added.bg" , make ~bg_color:(`RGB(0,91,0)) () + ; "diff.removed.bg" , make ~bg_color:(`RGB(91,0,0)) () ] let tag_map = ref CString.Map.empty @@ -198,72 +202,103 @@ let parse_color_config file = let dump_tags () = CString.Map.bindings !tag_map +let empty = Terminal.make () +let default_style = Terminal.reset_style + +let get_style tag = + try CString.Map.find tag !tag_map + with Not_found -> empty;; + +let get_open_seq tags = + let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in + Terminal.eval (Terminal.diff default_style style);; + +let get_close_seq tags = + let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in + Terminal.eval (Terminal.diff style default_style);; + +let diff_tag_stack = ref [] (* global, just like std_ft *) + (** Not thread-safe. We should put a lock somewhere if we print from different threads. Do we? *) let make_style_stack () = (** Default tag is to reset everything *) - let empty = Terminal.make () in - let default_tag = Terminal.({ - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; - prefix = None; - suffix = None; - }) - in let style_stack = ref [] in let peek () = match !style_stack with - | [] -> default_tag (** Anomalous case, but for robustness *) + | [] -> default_style (** Anomalous case, but for robustness *) | st :: _ -> st in - let push tag = - let style = - try CString.Map.find tag !tag_map - with | Not_found -> empty - in - (** Use the merging of the latest tag and the one being currently pushed. - This may be useful if for instance the latest tag changes the background and - the current one the foreground, so that the two effects are additioned. *) + let open_tag tag = + let (tpfx, ttag) = split_tag tag in + if tpfx = end_pfx then "" else + let style = get_style ttag in + (** Merge the current settings and the style being pushed. This allows + restoring the previous settings correctly in a pop when both set the same + attribute. Example: current settings have red FG, the pushed style has + green FG. When popping the style, we should set red FG, not default FG. *) let style = Terminal.merge (peek ()) style in + let diff = Terminal.diff (peek ()) style in style_stack := style :: !style_stack; - Terminal.eval style + if tpfx = start_pfx then diff_tag_stack := ttag :: !diff_tag_stack; + Terminal.eval diff in - let pop _ = match !style_stack with - | [] -> (** Something went wrong, we fallback *) - Terminal.eval default_tag - | _ :: rem -> style_stack := rem; - Terminal.eval (peek ()) + let close_tag tag = + let (tpfx, _) = split_tag tag in + if tpfx = start_pfx then "" else begin + if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []); + match !style_stack with + | [] -> (** Something went wrong, we fallback *) + Terminal.eval default_style + | cur :: rem -> style_stack := rem; + if cur = (peek ()) then "" else + if rem = [] then Terminal.reset else + Terminal.eval (Terminal.diff cur (peek ())) + end in let clear () = style_stack := [] in - push, pop, clear + open_tag, close_tag, clear let make_printing_functions () = - let empty = Terminal.make () in let print_prefix ft tag = - let style = - try CString.Map.find tag !tag_map - with | Not_found -> empty - in - match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () - in + let (tpfx, ttag) = split_tag tag in + if tpfx <> end_pfx then + let style = get_style ttag in + match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in + let print_suffix ft tag = - let style = - try CString.Map.find tag !tag_map - with | Not_found -> empty - in - match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () - in + let (tpfx, ttag) = split_tag tag in + if tpfx <> start_pfx then + let style = get_style ttag in + match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in + print_prefix, print_suffix +let init_output_fns () = + let reopen_highlight = ref "" in + let open Format in + let fns = Format.pp_get_formatter_out_functions !std_ft () in + let newline () = + if !diff_tag_stack <> [] then begin + let close = get_close_seq !diff_tag_stack in + fns.out_string close 0 (String.length close); + reopen_highlight := get_open_seq (List.rev !diff_tag_stack); + end; + fns.out_string "\n" 0 1 in + let string s off n = + if !reopen_highlight <> "" && String.trim (String.sub s off n) <> "" then begin + fns.out_string !reopen_highlight 0 (String.length !reopen_highlight); + reopen_highlight := "" + end; + fns.out_string s off n in + let new_fns = { fns with out_string = string; out_newline = newline } in + Format.pp_set_formatter_out_functions !std_ft new_fns;; + let init_terminal_output ~color = - let push_tag, pop_tag, clear_tag = make_style_stack () in + let open_tag, close_tag, clear_tag = make_style_stack () in let print_prefix, print_suffix = make_printing_functions () in let tag_handler ft = { - Format.mark_open_tag = push_tag; - Format.mark_close_tag = pop_tag; + Format.mark_open_tag = open_tag; + Format.mark_close_tag = close_tag; Format.print_open_tag = print_prefix ft; Format.print_close_tag = print_suffix ft; } in @@ -271,6 +306,7 @@ let init_terminal_output ~color = (* Use 0-length markers *) begin std_logger_cleanup := clear_tag; + init_output_fns (); Format.pp_set_mark_tags !std_ft true; Format.pp_set_mark_tags !err_ft true end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 479482095c..e1c9712135 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace @@ -433,6 +431,10 @@ let vernac_notation ~atts = let local = enforce_module_locality atts.locality in Metasyntax.add_notation local (Global.env()) +let vernac_custom_entry ~atts s = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_custom_entry local s + (***********) (* Gallina *) @@ -539,25 +541,43 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let vernac_record cum k poly finite struc binders sort nameopt cfs = +let uniform_inductive_parameters = ref false + +let should_treat_as_uniform () = + if !uniform_inductive_parameters + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters + +let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let const = match nameopt with - | None -> add_prefix "Build_" (fst (snd struc)).v - | Some ({v=id} as lid) -> - Dumpglob.dump_definition lid false "constr"; id in - if Dumpglob.dump () then ( - Dumpglob.dump_definition (fst (snd struc)) false "rec"; - List.iter (fun (((_, x), _), _) -> - match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) + let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let const = match nameopt with + | None -> add_prefix "Build_" id.v + | Some lid -> + let () = Dumpglob.dump_definition lid false "constr" in + lid.v + in + let () = + if Dumpglob.dump () then + let () = Dumpglob.dump_definition id false "rec" in + let iter (((_, x), _), _) = match x with + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + Dumpglob.dump_definition (make ?loc id) false "proj" + | _ -> () + in + List.iter iter cfs + in + coe, id, pl, binders, cfs, const, sort + in + let records = List.map map records in + ignore(Record.definition_structure k is_cumulative poly finite records) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = + let open Pp in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -567,35 +587,86 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function + | ((_ , _ , _ , _, RecordDecl _), _) -> true + | _ -> false + in + let is_constructor = function + | ((_ , _ , _ , _, Constructors _), _) -> true + | _ -> false + in + let is_defclass = match indl with + | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + | _ -> None + in + if Option.has_some is_defclass then + (** Definitional class case *) + let (id, bl, c, l) = Option.get is_defclass in + let (coe, (lid, ce)) = l in + let coe' = if coe then Some true else None in + let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in + vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + else if List.for_all is_record indl then + (** Mutual record case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_where ((_, _, _, _, _), wh) = match wh with + | [] -> () + | _ :: _ -> + user_err (str "where clause not supported for records") + in + let () = List.iter check_where indl in + let unpack ((id, bl, c, _, decl), _) = match decl with + | RecordDecl (oc, fs) -> + (id, bl, c, oc, fs) + | Constructors _ -> assert false (** ruled out above *) + in + let ((_, _, _, kind, _), _) = List.hd indl in + let kind = match kind with Class _ -> Class false | _ -> kind in + let recordl = List.map unpack indl in + vernac_record cum kind atts.polymorphic finite recordl + else if List.for_all is_constructor indl then + (** Mutual inductive case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | (Record | Structure) -> + user_err (str "The Record keyword is for types defined using the syntax { ... }.") + | Class _ -> + user_err (str "Inductive classes not supported") + | Variant | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_name ((na, _, _, _, _), _) = match na with + | (true, _) -> + user_err (str "Variant types do not handle the \"> Name\" \ + syntax, which is reserved for records. Use the \":>\" \ + syntax on constructors instead.") + | _ -> () + in + let () = List.iter check_name indl in + let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + | Constructors l -> (id, bl, c, l), ntn + | RecordDecl _ -> assert false (* ruled out above *) + in + let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite + else + user_err (str "Mixed record-inductive definitions are not allowed") +(* + match indl with - | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") - | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - user_err Pp.(str "The Variant keyword does not support syntax { ... }.") - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record cum (match b with Class _ -> Class false | _ -> b) - atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] - | [ ( _ , _, _, Class _, Constructors _), [] ] -> - user_err Pp.(str "Inductive classes not supported") - | [ ( id , bl , c , Class _, _), _ :: _ ] -> - user_err Pp.(str "where clause not supported for classes") - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - user_err Pp.(str "where clause not supported for (co)inductive records") - | _ -> let unpack = function - | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn - | ( (true,_),_,_,_,Constructors _),_ -> - user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") - | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") - in - let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + *) let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in @@ -1412,6 +1483,14 @@ let _ = optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = + declare_bool_option + { optdepr = false; + optname = "Uniform inductive parameters"; + optkey = ["Uniform"; "Inductive"; "Parameters"]; + optread = (fun () -> !uniform_inductive_parameters); + optwrite = (fun b -> uniform_inductive_parameters := b) } + +let _ = declare_int_option { optdepr = false; optname = "the level of inlining during functor application"; @@ -1426,8 +1505,8 @@ let _ = { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !CClosure.share); - optwrite = (fun b -> CClosure.share := b) } + optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); + optwrite = (fun b -> Global.set_reduction_sharing b) } let _ = declare_bool_option @@ -1908,8 +1987,9 @@ let vernac_subproof gln = match gln with | None -> Proof.focus subproof_cond () 1 p | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" - (str "Brackets only support the single numbered goal selector.")) + (str "Brackets do not support multi-goal selectors.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> @@ -1965,7 +2045,7 @@ let vernac_load interp fname = interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Gram.entry_parse Pvernac.main_entry po with + match Pcoq.Entry.parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = @@ -1974,7 +2054,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in begin try while true do interp (snd (parse_sentence input)) done with End_of_input -> () @@ -2021,6 +2101,8 @@ let interp ?proof ~atts ~st c = vernac_notation ~atts c infpl sc | VernacNotationAddFormat(n,k,v) -> Metasyntax.add_notation_extra_printing_rule n k v + | VernacDeclareCustomEntry s -> + vernac_custom_entry ~atts s (* Gallina *) | VernacDefinition ((discharge,kind),lid,d) -> @@ -2030,7 +2112,7 @@ let interp ?proof ~atts ~st c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> vernac_assumption ~atts discharge kind l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l @@ -2149,6 +2231,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ @@ -2244,32 +2327,62 @@ let with_fail st b f = | _ -> assert false end +let attributes_of_flags f atts = + let assert_empty k v = + if v <> VernacFlagEmpty + then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") + in + List.fold_left + (fun (polymorphism, atts) (k, v) -> + match k with + | "program" when not atts.program -> + assert_empty k v; + (polymorphism, { atts with program = true }) + | "program" -> + user_err Pp.(str "Program mode specified twice") + | "polymorphic" when polymorphism = None -> + assert_empty k v; + (Some true, atts) + | "monomorphic" when polymorphism = None -> + assert_empty k v; + (Some false, atts) + | ("polymorphic" | "monomorphic") -> + user_err Pp.(str "Polymorphism specified twice") + | "local" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some true }) + | "global" when Option.is_empty atts.locality -> + assert_empty k v; + (polymorphism, { atts with locality = Some false }) + | ("local" | "global") -> + user_err Pp.(str "Locality specified twice") + | "deprecated" when Option.is_empty atts.deprecated -> + begin match v with + | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] + | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + let since = Some since and note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) }) + | VernacFlagList [ "since", VernacFlagLeaf since ] -> + let since = Some since in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) }) + | VernacFlagList [ "note", VernacFlagLeaf note ] -> + let note = Some note in + (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) }) + | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") + end + | "deprecated" -> + user_err Pp.(str "Deprecation specified twice") + | _ -> user_err Pp.(str "Unknown attribute " ++ str k) + ) + (None, atts) + f + let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in - let flags f atts = - List.fold_left - (fun (polymorphism, atts) f -> - match f with - | VernacProgram when not atts.program -> - (polymorphism, { atts with program = true }) - | VernacProgram -> - user_err Pp.(str "Program mode specified twice") - | VernacPolymorphic b when polymorphism = None -> - (Some b, atts) - | VernacPolymorphic _ -> - user_err Pp.(str "Polymorphism specified twice") - | VernacLocal b when Option.is_empty atts.locality -> - (polymorphism, { atts with locality = Some b }) - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") - ) - (None, atts) - f - in let rec control = function | VernacExpr (f, v) -> - let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> @@ -2331,3 +2444,121 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn + +(** VERNAC EXTEND registering *) + +open Genarg +open Extend + +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (_, tu, ty) -> fun f args -> + begin match args with + | [] -> type_error () + | Genarg.GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (id, tu, ty) -> + let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol + +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ + new vernacular command does not alter the system state;\n\ + - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ + new vernacular command alters the system state but not the \ + parser nor it starts a proof or ends one;\n\ + - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ + a global function f. The function f will be called passing\ + \"%s\" as the only argument;\n\ + - Add a specific classifier in each clause using the syntax:\n\ + '[...] => [ f ] -> [...]'.\n\ + Specific classifiers have precedence over global \ + classifiers. Only one classifier is called." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 02a3b2bd61..fb2a30bac7 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -38,3 +38,37 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr Evd.evar_map * Redexpr.red_expr) Hook.t val universe_polymorphism_option_name : string list + +(** Elaborate a [atts] record out of a list of flags. + Also returns whether polymorphism is explicitly (un)set. *) +val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts + +(** {5 VERNAC EXTEND} *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + string option * + ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> + ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +(** Wrapper to dynamically extend vernacular commands. *) +val vernac_extend : + command:string -> + ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> + ty_ml list -> unit + +(** {5 STM classifiers} *) + +val get_vernac_classifier : + Vernacexpr.extend_name -> classifier + +(** Low-level API, not for casual user. *) +val declare_vernac_classifier : + string -> classifier array -> unit diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f74383b026..8fb74e6d78 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -121,12 +121,17 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = type hint_info_expr = Hints.hint_info_expr [@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] +type 'a hints_transparency_target = 'a Hints.hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of qualid list - | HintsTransparency of qualid list * bool + | HintsTransparency of qualid hints_transparency_target * bool | HintsMode of qualid * Hints.hint_mode list | HintsConstructors of qualid list | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument @@ -206,9 +211,9 @@ type proof_expr = ident_decl * (local_binder_expr list * constr_expr) type syntax_modifier = - | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option + | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option | SetLevel of int + | SetCustomEntry of string * int option | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing @@ -328,6 +333,7 @@ type nonrec vernac_expr = constr_expr * (lstring * syntax_modifier list) * scope_name option | VernacNotationAddFormat of string * string * string + | VernacDeclareCustomEntry of string (* Gallina *) | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr @@ -454,13 +460,14 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool +type vernac_flags = (string * vernac_flag_value) list +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr + | VernacExpr of vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control CAst.t diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index d4f2a753ff..1bb1414f3d 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -12,15 +12,22 @@ open Util open Pp open CErrors -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +let mk_deprecation ?(since=None) ?(note=None) () = + { since ; note } type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; + deprecated : deprecation option; } +let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts = + { loc ; locality ; polymorphic ; program ; deprecated } + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list @@ -28,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) let vinterp_add depr s f = try diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 935cacf77b..46468b3098 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -10,21 +10,27 @@ (** Interpretation of extended vernac phrases. *) -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; + deprecated : deprecation option; } +val mk_atts : ?loc: Loc.t option -> ?locality: bool option -> + ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts + type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list val vinterp_init : unit -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit +val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t |