diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 26 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 83 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 23 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 64 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 23 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 43 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 9 |
7 files changed, 163 insertions, 108 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index d711c9aea0..85f2bf3708 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -456,9 +456,19 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not 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 +519,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 +532,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 +557,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 07656f9715..3181bcc4bc 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -200,41 +200,44 @@ let assoc_eq al ar = | LeftA, LeftA -> true | _, _ -> false -(* [adjust_level assoc from prod] where [assoc] and [from] are the name +(** [adjust_level assoc from prod] where [assoc] and [from] are the name and associativity of the level where to add the rule; the meaning of the result is - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = let open Gramlib.Gramext in function + DefaultLevel = entry name + NextLevel = NEXT + NumLevel n = constr LEVEL n *) +let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with +(* If a level in a different grammar, no other choice than denoting it by absolute level *) + | (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> NumLevel n +(* If a default level in a different grammar, the entry name is ok *) + | (DefaultLevel,InternalProd) -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel + | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel (* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) + | (NumLevel n,BorderProd (_,None)) -> NumLevel n + | (DefaultLevel,BorderProd (_,None)) -> assert false (* Compute production name on the right side *) (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> - Some None + | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) -> NextLevel (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some RightA)) -> - Some (Some (n,true)) + | (NumLevel n,BorderProd (Right,Some RightA)) -> NumLevel n + | (DefaultLevel,BorderProd (Right,Some RightA)) -> NumLevel from (* Compute production name on the left side *) (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some NonA)) -> None + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> DefaultLevel (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> - None + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> + DefaultLevel (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | LeftA -> Some (Some (n, true)) - | _ -> Some None - end + | (NumLevel n,BorderProd (Left,Some LeftA)) -> NumLevel n + | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> NextLevel (* None means NEXT *) - | (NextLevel,_) -> Some None + | (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); NextLevel (* Compute production name elsewhere *) | (NumLevel n,InternalProd) -> - if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) + if from = n + 1 then NextLevel else NumLevel n type _ target = | ForConstr : constr_expr target @@ -311,13 +314,14 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function | ForConstr -> entry_for_constr | ForPattern -> entry_for_patttern -let is_self from e = match e with +let is_self custom (custom',from) e = Notation.notation_entry_eq custom custom' && match e with | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false | (NumLevel n, BorderProd (Left, _)) -> Int.equal from n | _ -> false -let is_binder_level from e = match e with -| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 +let is_binder_level custom (custom',from) e = match e with +| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> + custom = InConstrEntry && custom' = InConstrEntry && from = 200 | _ -> false let make_sep_rules = function @@ -338,15 +342,15 @@ type ('s, 'a) mayrec_symbol = | MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat -> - if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200")) - else if is_self from p then MayRecMay Aself + if is_binder_level custom from p then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200")) + else if is_self custom from p then MayRecMay Aself else let g = target_entry custom forpat in - let lev = adjust_level assoc from p in + let lev = adjust_level custom assoc from p in begin match lev with - | None -> MayRecNo (Aentry g) - | Some None -> MayRecMay Anext - | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev)) + | DefaultLevel -> MayRecNo (Aentry g) + | NextLevel -> MayRecMay Anext + | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev)) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with @@ -503,19 +507,24 @@ let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = let empty = (pos, [(name, p4assoc, [])]) in ExtendRule (target_entry where forpat, reinit, empty) -let rec pure_sublevels' custom assoc from forpat level = function +let different_levels (custom,opt_level) (custom',string_level) = + match opt_level with + | None -> true + | Some level -> not (Notation.notation_entry_eq custom custom') || level <> int_of_string string_level + +let rec pure_sublevels' assoc from forpat level = function | [] -> [] | GramConstrNonTerminal (e,_) :: rem -> - let rem = pure_sublevels' custom assoc from forpat level rem in + let rem = pure_sublevels' assoc from forpat level rem in let push where p rem = - match symbol_of_target custom p assoc from forpat with - | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem + match symbol_of_target where p assoc from forpat with + | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,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 +| (GramConstrTerminal _ | GramConstrListMark _) :: rem -> pure_sublevels' assoc from forpat level rem let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> @@ -530,8 +539,8 @@ let extend_constr state forpat ng = let assoc = ng.notgram_assoc 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 pure_sublevels = pure_sublevels' custom assoc n forpat level pt in + let AnyTyRule r = make_ty_rule assoc (custom,n) forpat pt in + let pure_sublevels = pure_sublevels' assoc (custom,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 custom isforpat assoc level in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74249301d7..d597707d12 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -395,9 +395,10 @@ 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 } @@ -1224,11 +1225,10 @@ GRAMMAR EXTEND Gram | { 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) } + lev = level -> { SetItemLevel (x::l,None,lev) } + | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind -> + { SetItemLevel ([x],b,lev) } + | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) } | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } ] ] ; @@ -1236,19 +1236,20 @@ GRAMMAR EXTEND Gram [ [ 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 "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } + | IDENT "constr"; n = at_level_opt; 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 -> + | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InCustomEntry x,b,n) } ] ] ; - at_level: - [ [ "at"; n = level -> { n } ] ] + at_level_opt: + [ [ "at"; n = level -> { n } + | -> { DefaultLevel } ] ] ; constr_as_binder_kind: [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 0c39aba70a..7794b0a37a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -297,7 +297,11 @@ let precedence_of_position_and_level from_level = function 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 +(** 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 @@ -309,6 +313,22 @@ let precedence_of_entry_type (from_custom,from_level) = function | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n | _ -> 0, E (* should not matter *) +(** Computing precedences for future insertion of parentheses at + the time of printing using hard-wired constr levels *) +let unparsing_precedence_of_entry_type from_level = function + | ETConstr (InConstrEntry,_,x) -> + (* 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) + | 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 *) + (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) (* "x =S y" : "x /1 =S /1 y" (protect from confusion; each side for symmetry)*) @@ -374,7 +394,7 @@ let check_open_binder isopen sl m = let unparsing_metavar i from typs = let x = List.nth typs (i-1) in - let prec = snd (precedence_of_entry_type from x) in + let prec = unparsing_precedence_of_entry_type from x in match x with | ETConstr _ | ETGlobal | ETBigint -> UnpMetaVar (i,prec) @@ -389,12 +409,12 @@ let unparsing_metavar i from typs = let index_id id l = List.index Id.equal id l -let make_hunks etyps symbols from = +let make_hunks etyps symbols from_level = let vars,typs = List.split etyps in let rec make b = function | NonTerminal m :: prods -> let i = index_id m vars in - let u = unparsing_metavar i from typs in + let u = unparsing_metavar i from_level typs in if is_next_non_terminal b prods then (None, u) :: add_break_if_none 1 b (make b prods) else @@ -428,7 +448,7 @@ let make_hunks etyps symbols from = | SProdList (m,sl) :: prods -> 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 prec = unparsing_precedence_of_entry_type from_level typ in let sl' = (* If no separator: add a break *) if List.is_empty sl then add_break 1 [] @@ -555,7 +575,7 @@ let read_recursive_format sl fmt = the names in the notation *) slfmt, res -let hunks_of_format (from,(vars,typs)) symfmt = +let hunks_of_format (from_level,(vars,typs)) symfmt = let rec aux = function | symbs, (_,(UnpTerminal s' as u)) :: fmt when String.equal s' (String.make (String.length s') ' ') -> @@ -565,13 +585,13 @@ let hunks_of_format (from,(vars,typs)) symfmt = let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') -> let i = index_id s vars in - let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l + let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from_level typs :: l | symbs, (_,(UnpCut _ as u)) :: fmt -> let symbs, l = aux (symbs,fmt) in symbs, u :: l | SProdList (m,sl) :: symbs, fmt when has_ldots fmt -> 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 prec = unparsing_precedence_of_entry_type from_level typ 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) (); @@ -955,18 +975,23 @@ let is_only_printing mods = (* Compute precedences from modifiers (or find default ones) *) -let set_entry_type from etyps (x,typ) = +let set_entry_type from n etyps (x,typ) = + let make_lev n s = match typ with + | BorderProd _ -> NumLevel n + | InternalProd -> DefaultLevel in let typ = try match List.assoc x etyps, typ with - | ETConstr (s,bko,Some n), (_,BorderProd (left,_)) -> + | ETConstr (s,bko,DefaultLevel), _ -> + if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ)) + else ETConstr (s,bko,(DefaultLevel,typ)) + | ETConstr (s,bko,n), BorderProd (left,_) -> ETConstr (s,bko,(n,BorderProd (left,None))) - | ETConstr (s,bko,Some n), (_,InternalProd) -> - ETConstr (s,bko,(n,InternalProd)) + | ETConstr (s,bko,n), InternalProd -> + ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x - | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ) with Not_found -> - ETConstr (from,None,typ) + ETConstr (from,None,(make_lev n from,typ)) in (x,typ) let join_auxiliary_recursive_types recvars etyps = @@ -1123,7 +1148,7 @@ let find_precedence custom lev etyps symbols onlyprint = else 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,_,Some _), s' when s = s' -> test () + | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> @@ -1216,14 +1241,13 @@ module SynData = struct end let find_subentry_types from n assoc etyps symbols = - let innerlevel = NumLevel 200 in let typs = find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) + (BorderProd(Left,assoc)) + (InternalProd) + (BorderProd(Right,assoc)) symbols in - let sy_typs = List.map (set_entry_type from etyps) typs in + let sy_typs = List.map (set_entry_type from n etyps) typs in let prec = List.map (assoc_of_type from n) sy_typs in sy_typs, prec @@ -1445,7 +1469,7 @@ 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 (custom,level) sd.pp_syntax_data sd.format in { + let pp_rule = make_pp_rule 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 }; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 6240120cb0..314c423f65 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -107,8 +107,11 @@ open Pputils | 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" + | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n + | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + | DefaultLevel -> mt () + + let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> spc () ++ keyword "as ident" @@ -120,19 +123,14 @@ open Pputils let pr_set_entry_type pr = function | 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) + | 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" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - let pr_at_level_opt = function - | None -> mt () - | Some n -> spc () ++ pr_at_level n - let pr_set_simple_entry_type = - pr_set_entry_type pr_at_level_opt + pr_set_entry_type pr_at_level let pr_comment pr_c = function | CommentConstr c -> pr_c c @@ -402,7 +400,7 @@ let string_of_theorem_kind = let open Decls in function let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> - prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++ + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level 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)) @@ -812,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/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 8ead56dfdf..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 @@ -177,7 +180,7 @@ type proof_expr = ident_decl * (local_binder_expr list * constr_expr) type syntax_modifier = - | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option + | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level | SetLevel of int | SetCustomEntry of string * int option | SetAssoc of Gramlib.Gramext.g_assoc |