diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 45 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 87 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 25 | ||||
| -rw-r--r-- | vernac/himsg.ml | 16 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 393 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 23 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 43 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 9 |
9 files changed, 388 insertions, 259 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 07656f9715..72e6d41969 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,35 +507,40 @@ 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 -> 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 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..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; "}" -> @@ -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/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 0c39aba70a..afff0347f5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -286,28 +286,46 @@ 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 - + (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 *) +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] *) + 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] *) + 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) *) @@ -374,14 +392,14 @@ 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) + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -389,12 +407,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,17 +446,17 @@ 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 [] (* 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 @@ -555,7 +573,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,22 +583,22 @@ 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) (); 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 -> @@ -725,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()) ++ @@ -755,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 @@ -800,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 @@ -955,18 +1023,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,11 +1196,11 @@ 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 -> - ([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) | _ -> @@ -1144,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."); @@ -1197,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; @@ -1216,14 +1289,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 @@ -1296,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 *) @@ -1318,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) = @@ -1334,24 +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 - | 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 = @@ -1393,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 *) @@ -1440,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 (custom,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; } @@ -1463,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; @@ -1485,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 @@ -1525,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' @@ -1532,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 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/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 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 |