diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 45 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 12 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 6 | ||||
| -rw-r--r-- | vernac/himsg.ml | 16 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 360 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 43 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 7 |
9 files changed, 291 insertions, 210 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index d711c9aea0..edb03a5c89 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -433,32 +433,33 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let indnames = List.map (fun ind -> ind.ind_name) indl in - let sigma, env_params, infos = + + (* In case of template polymorphism, we need to compute more constraints *) + let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in + + let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) = interp_params env0 udecl uparamsl paramsl in (* Interpret the arities *) let arities = List.map (intern_ind_arity env_params sigma) indl in - let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template = - let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in - if not poly && is_template then - (* In case of template polymorphism, we need to compute more constraints *) - let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in - let sigma, env_params, infos = - interp_params env0 udecl uparamsl paramsl - in - let arities = List.map (intern_ind_arity env_params sigma) indl in - sigma, env_params, infos, arities, is_template - else sigma, env_params, infos, arities, is_template - in - let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in - let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in + let lift1_ctx ctx = + let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in + let t = EConstr.Vars.lift 1 t in + let ctx, _ = EConstr.decompose_prod_assum sigma t in + ctx + in + let ctx_params_lifted, fullarities = CList.fold_left_map + (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params) + ctx_params + arities + in let env_ar = push_types env_uparams indnames relevances fullarities in - let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in @@ -509,6 +510,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 +let eq_params (up1,p1) (up2,p2) = + eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2 + let extract_coercions indl = let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in @@ -519,7 +523,7 @@ let extract_params indl = match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); params @@ -544,7 +548,12 @@ type uniform_inductive_flag = let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let indl = match params with + | uparams, Some params -> (uparams, params, indl) + | params, None -> match uniform with + | UniformParameters -> (params, [], indl) + | NonUniformParameters -> ([], params, indl) + in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5e98f5ddc0..72e6d41969 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -249,7 +249,6 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry -| TTString : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) | TTBigint -> MayRecNo (Aentry Prim.bigint) -| TTString -> MayRecNo (Aentry Prim.string) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint -| ETProdString -> TTAny TTString | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) @@ -417,11 +414,6 @@ match e with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end -| TTString -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v)) - end | TTReference -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) @@ -537,10 +529,10 @@ let rec pure_sublevels' assoc from forpat level = function let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in - CAst.make ~loc @@ CNotation (notation, env) + CAst.make ~loc @@ CNotation (None, notation, env) | ForPattern -> fun notation loc env -> let env = (env.constrs, env.constrlists) in - CAst.make ~loc @@ CPatNotation (notation, env, []) + CAst.make ~loc @@ CPatNotation (None, notation, env, []) let extend_constr state forpat ng = let custom,n,_,_ = ng.notgram_level in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 97c9d23c68..def4ed942a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -395,13 +395,14 @@ GRAMMAR EXTEND Gram ; inductive_definition: [ [ oc = opt_coercion; id = ident_decl; indpar = binders; + extrapar = OPT [ "|"; p = binders -> { p } ]; c = OPT [ ":"; c = lconstr -> { c } ]; lc=opt_constructors_or_fields; ntn = decl_notation -> - { (((oc,id),indpar,c,lc),ntn) } ] ] + { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ] ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { Constructors ((c id)::l) } | id = identref ; c = constructor_type -> { Constructors [ c id ] } | cstr = identref; "{"; fs = record_fields; "}" -> @@ -1234,7 +1235,6 @@ GRAMMAR EXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } - | IDENT "string" -> { ETString } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index dfc4631572..f6f6c4f1eb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk ": cannot ensure that " ++ t ++ strbrk " is a subtype of " ++ u] | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] - else - [str "universe inconsistency"] + [str "universe inconsistency: " ++ + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] | CannotSolveConstraint ((pb,env,t,u),e) -> let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ @@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> - let msg = - if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i - else - mt() in - str "Universe inconsistency" ++ msg ++ str "." + str "Universe inconsistency." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d39ee60c25..afff0347f5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -286,32 +286,30 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = let open Gramlib.Gramext in function - | RightA -> (L,E) - | LeftA -> (E,L) - | NonA -> (L,L) - 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_level, L - | DefaultLevel, _ -> - (* Fake value, waiting for PR#5 at herbelin's fork *) 200, - Any + (let open Gramlib.Gramext in + match a, b with + | RightA, Left -> LevelLt n + | RightA, Right -> LevelLe n + | LeftA, Left -> LevelLe n + | LeftA, Right -> LevelLt n + | NonA, _ -> LevelLt n) + | NumLevel n, _ -> LevelLe n + | NextLevel, _ -> LevelLt from_level + | DefaultLevel, _ -> LevelSome (** Computing precedences of subentries for parsing *) 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,_,(NumLevel n,_)) -> LevelLe 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 *) + | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n + | _ -> LevelSome (* should not matter *) (** Computing precedences for future insertion of parentheses at the time of printing using hard-wired constr levels *) @@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function (* Possible insertion of parentheses at printing time to deal with precedence in a constr entry is managed using [prec_less] in [ppconstr.ml] *) - snd (precedence_of_position_and_level from_level x) + precedence_of_position_and_level from_level x | ETConstr (custom,_,_) -> (* Precedence of printing for a custom entry is managed using explicit insertion of entry coercions at the time of building a [constr_expr] *) - Any - | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0) - | _ -> Any (* should not matter *) + LevelSome + | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0) + | _ -> LevelSome (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -396,12 +394,12 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint | ETString -> - UnpMetaVar (i,prec) + | ETConstr _ | ETGlobal | ETBigint -> + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level = (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,List.map snd sl') + UnpBinderListMetaVar (isopen,List.map snd sl') | _ -> assert false in (None, hunk) :: make_with_space b prods @@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = 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) + | ETConstr _ -> UnpListMetaVar (prec,slfmt) | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) + UnpBinderListMetaVar (isopen,slfmt) | _ -> assert false in symbs, hunk :: l | symbs, (_,UnpBox (a,b)) :: fmt -> @@ -686,7 +684,6 @@ let prod_entry_type = function | ETIdent -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint - | ETString -> ETProdString | ETBinder _ -> assert false (* See check_binder_type *) | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) @@ -746,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in let pr_arg_level from (lev,typ) = let pplev = function - | (n,L) when Int.equal n from -> str "at next level" - | (n,E) -> str "at level " ++ int n - | (n,L) -> str "at level below " ++ int n - | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" in - Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ - (match typ with - | ETConstr _ | ETPattern _ -> spc () ++ pplev lev - | _ -> mt ()) + | LevelLt n when Int.equal n from -> spc () ++ str "at next level" + | LevelLe n -> spc () ++ str "at level " ++ int n + | LevelLt n -> spc () ++ str "at level below " ++ int n + | LevelSome -> mt () in + Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev let pr_level ntn (from,fromlevel,args,typs) = (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ @@ -776,43 +769,97 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec = spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") -type syntax_extension = { +let warn_incompatible_format = + CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing" + (fun (specific,ntn) -> + let head,scope = match specific with + | None -> str "Notation", mt () + | Some LastLonelyNotation -> str "Lonely notation", mt () + | Some (NotationInScope sc) -> str "Notation", strbrk (" in scope " ^ sc) in + head ++ spc () ++ pr_notation ntn ++ + strbrk " was already defined with a different format" ++ scope ++ str ".") + +type syntax_parsing_extension = { synext_level : Notation_gram.level; synext_notation : notation; - synext_notgram : notation_grammar; - synext_unparsing : unparsing list; + synext_notgram : notation_grammar option; +} + +type syntax_printing_extension = { + synext_reserved : bool; + synext_unparsing : unparsing_rule; synext_extra : (string * string) list; } -type syntax_extension_obj = locality_flag * syntax_extension +let generic_format_to_declare ntn {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (generic_rules,_),reserved,generic_extra_rules = + Ppextend.find_generic_notation_printing_rule ntn in + if reserved && + (not (List.for_all2eq unparsing_eq rules generic_rules) + || extra_rules <> generic_extra_rules) + then + (warn_incompatible_format (None,ntn); true) + else + false + with Not_found -> true + +let check_reserved_format ntn = function + | None -> () + | Some sy_pp_rules -> let _ = generic_format_to_declare ntn sy_pp_rules in () + +let specific_format_to_declare (specific,ntn as specific_ntn) + {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (specific_rules,_),specific_extra_rules = + Ppextend.find_specific_notation_printing_rule specific_ntn in + if not (List.for_all2eq unparsing_eq rules specific_rules) + || extra_rules <> specific_extra_rules then + (warn_incompatible_format (Some specific,ntn); true) + else false + with Not_found -> true + +type syntax_extension_obj = + locality_flag * (syntax_parsing_extension * syntax_printing_extension option) let check_and_extend_constr_grammar ntn rule = try let ntn_for_grammar = rule.notgram_notation in 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; + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + if oldparsing = None then raise Not_found with Not_found -> Egramcoq.extend_constr_grammar rule -let cache_one_syntax_extension se = - let ntn = se.synext_notation in - let prec = se.synext_level in - let onlyprint = se.synext_notgram.notgram_onlyprinting in - try - let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in - if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; - with Not_found -> - begin - (* Reserve the notation level *) - Notgram_ops.declare_notation_level ntn prec ~onlyprint; - (* Declare the parsing rule *) - 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, let (_,lev,_,_) = prec in lev) se.synext_notgram - end +let cache_one_syntax_extension (pa_se,pp_se) = + let ntn = pa_se.synext_notation in + let prec = pa_se.synext_level in + (* Check and ensure that the level and the precomputed parsing rule is declared *) + let oldparsing = + try + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in + if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec; + oldparsing + with Not_found -> + (* Declare the level and the precomputed parsing rule *) + let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in + None in + (* Declare the parsing rule *) + begin match oldparsing, pa_se.synext_notgram with + | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams + | _ -> (* The grammars rules are canonically derived from the string and the precedence*) () + end; + (* Printing *) + match pp_se with + | None -> () + | Some pp_se -> + (* Check compatibility of format in case of two Reserved Notation *) + (* and declare or redeclare printing rule *) + if generic_format_to_declare ntn pp_se then + declare_generic_notation_printing_rules ntn + ~extra:pp_se.synext_extra ~reserved:pp_se.synext_reserved pp_se.synext_unparsing let cache_syntax_extension (_, (_, sy)) = cache_one_syntax_extension sy @@ -821,11 +868,11 @@ let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (subst, (local, sy)) = - (local, { sy with - synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules }; - synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - }) +let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) = + (local, ({ pa_sy with + synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram }, + Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy) + ) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -990,7 +1037,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1012,7 +1059,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETString | ETGlobal + | ETConstr _ | ETBigint | ETGlobal | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = @@ -1034,7 +1081,7 @@ let make_interpretation_type isrec isonlybinding = function (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETString | ETGlobal -> NtnTypeConstr + | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") @@ -1098,8 +1145,6 @@ type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int - | IsEntryNumeral of string * int - | IsEntryString of string * int let is_coercion = function | Some (custom,n,_,[e]) -> @@ -1111,8 +1156,6 @@ let is_coercion = function else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) - | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n)) - | ETString, InCustomEntry s -> Some (IsEntryString (s,n)) | _ -> None) | Some _ -> assert false | None -> None @@ -1154,10 +1197,10 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETString | ETGlobal), _ -> + | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) | Some 0 -> ([],0) | _ -> @@ -1174,7 +1217,7 @@ let find_precedence custom lev etyps symbols onlyprint = else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")], 0) else [],Option.get lev | Some _ -> if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); @@ -1227,7 +1270,7 @@ module SynData = struct extra : (string * string) list; (* XXX: Callback to printing, must remove *) - msgs : ((Pp.t -> unit) * Pp.t) list; + msgs : (unit -> unit) list; (* Fields for internalization *) recvars : (Id.t * Id.t) list; @@ -1325,15 +1368,19 @@ let compute_syntax_data ~local deprecation df modifiers = not_data = sy_fulldata; } +let warn_only_parsing_reserved_notation = + CWarnings.create ~name:"irrelevant-reserved-notation-only-parsing" ~category:"parsing" + (fun () -> strbrk "The only parsing modifier has no effect in Reserved Notation.") + let compute_pure_syntax_data ~local df mods = let open SynData in let sd = compute_syntax_data ~local None df mods in - let msgs = - if sd.only_parsing then - (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::sd.msgs - else sd.msgs in - { sd with msgs } + if sd.only_parsing + then + let msgs = (fun () -> warn_only_parsing_reserved_notation ?loc:None ())::sd.msgs in + { sd with msgs; only_parsing = false } + else + sd (**********************************************************************) (* Registration of notations interpretation *) @@ -1347,6 +1394,7 @@ type notation_obj = { notobj_onlyprint : bool; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; + notobj_specific_pp_rules : syntax_printing_extension option; } let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = @@ -1363,26 +1411,35 @@ let load_notation = load_notation_common true let open_notation i (_, nobj) = - let scope = nobj.notobj_scope in - let (ntn, df) = nobj.notobj_notation in - let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in - let deprecation = nobj.notobj_deprecation in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if Int.equal i 1 && fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - 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 - | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n - | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n - | None -> ()) + if Int.equal i 1 then begin + let scope = nobj.notobj_scope in + let (ntn, df) = nobj.notobj_notation in + let pat = nobj.notobj_interp in + let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in + let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let specific_ntn = (specific,ntn) in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in + if fresh then begin + (* Declare the interpretation *) + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in + (* Declare the uninterpretation *) + if not nobj.notobj_onlyparse then + Notation.declare_uninterpretation (NotationRule specific_ntn) pat; + (* Declare a possible coercion *) + (match nobj.notobj_coercion with + | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_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; + (* Declare specific format if any *) + match nobj.notobj_specific_pp_rules with + | Some pp_sy -> + if specific_format_to_declare specific_ntn pp_sy then + Ppextend.declare_specific_notation_printing_rules + specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> () end let cache_notation o = @@ -1424,23 +1481,30 @@ let with_syntax_protection f x = exception NoSyntaxRule let recover_notation_syntax ntn = - try - let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in - let pp_rule,_ = find_notation_printing_rule ntn in - let pp_extra_rules = find_notation_extra_printing_rules ntn in - let pa_rule = find_notation_parsing_rules ntn in - { synext_level = prec; - synext_notation = ntn; - synext_notgram = pa_rule; - synext_unparsing = pp_rule; - synext_extra = pp_extra_rules; - } - with Not_found -> - raise NoSyntaxRule + let pa = + try + let pa_rule,prec = Notgram_ops.level_of_notation ntn in + { synext_level = prec; + synext_notation = ntn; + synext_notgram = pa_rule } + with Not_found -> + raise NoSyntaxRule in + let pp = + try + let pp_rule,reserved,pp_extra_rules = find_generic_notation_printing_rule ntn in + Some { + synext_reserved = reserved; + synext_unparsing = pp_rule; + synext_extra = pp_extra_rules; + } + with Not_found -> None in + pa,pp let recover_squash_syntax sy = - let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in - sy :: sq.synext_notgram.notgram_rules + let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in + match sq.synext_notgram with + | Some gram -> sy :: gram + | None -> raise NoSyntaxRule (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -1471,16 +1535,28 @@ let make_pp_rule level (typs,symbols) fmt = | 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 make_parsing_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 level sd.pp_syntax_data sd.format in { + let pa_rule = + if sd.only_printing then None + else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) + in { synext_level = sd.level; synext_notation = fst sd.info; - synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; - synext_unparsing = pp_rule; + synext_notgram = pa_rule; + } + +let warn_irrelevant_format = + CWarnings.create ~name:"irrelevant-format-only-parsing" ~category:"parsing" + (fun () -> str "The format modifier is irrelevant for only parsing rules.") + +let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in + let custom,level,_,_ = sd.level in + let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in + if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) + else Some { + synext_reserved = reserved; + synext_unparsing = (pp_rule,level); synext_extra = sd.extra; } @@ -1494,9 +1570,10 @@ let to_map l = let add_notation_in_scope ~local deprecation df env c mods scope = let open SynData in let sd = compute_syntax_data ~local deprecation df mods in - (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sd in + let sy_pa_rules = make_parsing_rules sd in + let sy_pp_rules = make_printing_rules false sd in + (* Prepare the interpretation *) let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1516,24 +1593,29 @@ let add_notation_in_scope ~local deprecation df env c mods scope = notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = sd.info; + notobj_specific_pp_rules = sy_pp_rules; } in + let gen_sy_pp_rules = + if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None + else sy_pp_rules (* We use the format of this notation as the default *) in + let _ = check_reserved_format (fst sd.info) sy_pp_rules in (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) sd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); + List.iter (fun f -> f ()) sd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules))); Lib.add_anonymous_leaf (inNotation notation); sd.info let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let level, i_typs, onlyprint = if not (is_numeral symbs) then begin - let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in + let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin + let (pa_sy,pp_sy as 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 - let _,_,_,typs = sy.synext_level in - Some sy.synext_level, typs, onlyprint - end else None, [], false in + let onlyprint = onlyprint || pa_sy.synext_notgram = None in + let _,_,_,typs = pa_sy.synext_level in + Some pa_sy.synext_level, typs, onlyprint, pp_sy + end else None, [], false, None in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in @@ -1556,6 +1638,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; + notobj_specific_pp_rules = pp_sy; } in Lib.add_anonymous_leaf (inNotation notation); df' @@ -1563,10 +1646,11 @@ 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 ~local df mods in - let sy_rules = make_syntax_rules {psd with deprecation = None} in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) + let psd = {(compute_pure_syntax_data ~local df mods) with deprecation = None} in + let pa_rules = make_parsing_rules psd in + let pp_rules = make_printing_rules true psd in + List.iter (fun f -> f ()) psd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension(local,(pa_rules,pp_rules))) (* Notations with only interpretation *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 0cf407619b..314c423f65 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -126,7 +126,6 @@ open Pputils | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" - | ETString -> str "string" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" @@ -811,11 +810,12 @@ let string_of_definition_object_kind = let open Decls in function | RecordDecl (c,fs) -> pr_record_decl c fs in - let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) = + let pr_oneind key (((coe,iddecl),(indupar,indpar),s,lc),ntn) = hov 0 ( str key ++ spc() ++ (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++ - pr_and_type_binders_arg indpar ++ + pr_and_type_binders_arg indupar ++ + pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++ pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++ str" :=") ++ pr_constructor_list lc ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 32c438c724..cdd93db884 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -547,7 +547,7 @@ let print_located_qualid ref = print_located_qualid "object" LocAny ref (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_leconstr_env env sigma trm ++ fnl () ++ + (pr_leconstr_env ~inctx:true env sigma trm ++ fnl () ++ str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the @@ -556,7 +556,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = synthesizes the type nat of the abstraction on u *) let print_named_def env sigma name body typ = - let pbody = pr_lconstr_env env sigma body in + let pbody = pr_lconstr_env ~inctx:true env sigma body in let ptyp = pr_ltype_env env sigma typ in let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ @@ -598,7 +598,7 @@ let gallina_print_section_variable env sigma id = with_line_skip (print_name_infos (GlobRef.VarRef id)) let print_body env evd = function - | Some c -> pr_lconstr_env env evd c + | Some c -> pr_lconstr_env ~inctx:true env evd c | None -> (str"<no body>") let print_typed_body env evd (val_0,typ) = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e469323f50..63fc587f71 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -623,18 +623,16 @@ 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 && is_polymorphic_inductive_cumulativity () -let uniform_att = - let get_uniform_inductive_parameters = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Uniform"; "Inductive"; "Parameters"] - ~value:false - in - let open Attributes.Notations in - Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u -> - let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in - let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in - return u +let get_uniform_inductive_parameters = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Uniform"; "Inductive"; "Parameters"] + ~value:false + +let should_treat_as_uniform () = + if get_uniform_inductive_parameters () + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in @@ -682,6 +680,7 @@ let finite_of_kind = let open Declarations in function indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo kind indl = + let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in let open Pp in let udecl, indl = extract_inductive_udecl indl in if Dumpglob.dump () then @@ -710,12 +709,14 @@ let vernac_inductive ~atts cum lo kind indl = if Option.has_some is_defclass then (* Definitional class case *) let (id, bl, c, l) = Option.get is_defclass in + let bl = match bl with + | bl, None -> bl + | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.") + in let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } - in - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) @@ -732,12 +733,15 @@ let vernac_inductive ~atts cum lo kind indl = let () = List.iter check_where indl in let unpack ((id, bl, c, decl), _) = match decl with | RecordDecl (oc, fs) -> + let bl = match bl with + | bl, None -> bl + | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.") + in (id, bl, c, oc, fs) | Constructors _ -> assert false (* ruled out above *) in let kind = match kind with Class _ -> Class false | _ -> kind in let recordl = List.map unpack indl in - let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in vernac_record ~template udecl cum kind poly finite recordl else if List.for_all is_constructor indl then (* Mutual inductive case *) @@ -761,12 +765,9 @@ let vernac_inductive ~atts cum lo kind indl = | RecordDecl _ -> assert false (* ruled out above *) in let indl = List.map unpack indl in - let (template, poly), uniform = - Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts) - in let cumulative = should_treat_as_cumulative cum poly in - ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly - ~private_ind:lo ~uniform finite + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 3610240634..45018a246c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -163,12 +163,15 @@ type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * (local_decl_expr * record_field_attr) list +type inductive_params_expr = local_binder_expr list * local_binder_expr list option +(** If the option is nonempty the "|" marker was used *) + type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * + ident_decl with_coercion * inductive_params_expr * constr_expr option * constructor_list_or_record_decl_expr type one_inductive_expr = - lident * local_binder_expr list * constr_expr option * constructor_expr list + lident * inductive_params_expr * constr_expr option * constructor_expr list type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list |