diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 9 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 265 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 18 |
3 files changed, 145 insertions, 147 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index e04bebe33b..32ab5401a0 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -241,7 +241,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = else l in (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) - let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> + let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) -> let t,imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in @@ -367,7 +367,7 @@ let prepare_param = function let rec check_anonymous_type ind = let open Glob_term in - match ind.CAst.v with + match DAst.get ind with | GSort (GType []) -> true | GProd ( _, _, _, e) | GLetIn (_, _, _, e) @@ -393,8 +393,9 @@ let is_impredicative env u = let interp_ind_arity env evdref ind = let c = intern_gen IsType env ind.ind_arity in - let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in + let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in + let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in + evdref := evd; let pseudo_poly = check_anonymous_type c in let () = if not (Reductionops.is_arity env !evdref t) then user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c0974d0a7c..c424b1d501 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -98,8 +98,7 @@ let pr_grammar = function quote (except a single quote alone) must be quoted) *) let parse_format ((loc, str) : lstring) = - let str = " "^str in - let l = String.length str in + let len = String.length str in let push_token a = function | cur::l -> (a::cur)::l | [] -> [[a]] in @@ -109,16 +108,16 @@ let parse_format ((loc, str) : lstring) = | a::(_::_ as l) -> push_token (UnpBox (b,a)) l | _ -> user_err Pp.(str "Non terminated box in format.") in let close_quotation i = - if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ') + if i < len && str.[i] == '\'' && (Int.equal (i+1) len || str.[i+1] == ' ') then i+1 else user_err Pp.(str "Incorrectly terminated quoted expression.") in let rec spaces n i = - if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1) + if i < len && str.[i] == ' ' then spaces (n+1) (i+1) else n in let rec nonspaces quoted n i = - if i < String.length str && str.[i] != ' ' then + if i < len && str.[i] != ' ' then if str.[i] == '\'' && quoted && - (i+1 >= String.length str || str.[i+1] == ' ') + (i+1 >= len || str.[i+1] == ' ') then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n else nonspaces quoted (n+1) (i+1) else @@ -126,26 +125,26 @@ let parse_format ((loc, str) : lstring) = else n in let rec parse_non_format i = let n = nonspaces false 0 i in - push_token (UnpTerminal (String.sub str i n)) (parse_token (i+n)) + push_token (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) and parse_quoted n i = - if i < String.length str then match str.[i] with + if i < len then match str.[i] with (* Parse " // " *) - | '/' when i <= String.length str && str.[i+1] == '/' -> + | '/' when i <= len && str.[i+1] == '/' -> (* We forget the useless n spaces... *) push_token (UnpCut PpFnl) - (parse_token (close_quotation (i+2))) + (parse_token 1 (close_quotation (i+2))) (* Parse " .. / .. " *) - | '/' when i <= String.length str -> + | '/' when i <= len -> let p = spaces 0 (i+1) in push_token (UnpCut (PpBrk (n,p))) - (parse_token (close_quotation (i+p+1))) + (parse_token 1 (close_quotation (i+p+1))) | c -> (* The spaces are real spaces *) push_white n (match c with | '[' -> - if i <= String.length str then match str.[i+1] with + if i <= len then match str.[i+1] with (* Parse " [h .. ", *) - | 'h' when i+1 <= String.length str && str.[i+2] == 'v' -> + | 'h' when i+1 <= len && str.[i+2] == 'v' -> (parse_box (fun n -> PpHVB n) (i+3)) (* Parse " [v .. ", *) | 'v' -> @@ -157,39 +156,39 @@ let parse_format ((loc, str) : lstring) = else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.") (* Parse "]" *) | ']' -> - ([] :: parse_token (close_quotation (i+1))) + ([] :: parse_token 1 (close_quotation (i+1))) (* Parse a non formatting token *) | c -> let n = nonspaces true 0 i in push_token (UnpTerminal (String.sub str (i-1) (n+2))) - (parse_token (close_quotation (i+n)))) + (parse_token 1 (close_quotation (i+n)))) else if Int.equal n 0 then [] else user_err Pp.(str "Ending spaces non part of a format annotation.") and parse_box box i = let n = spaces 0 i in - close_box i (box n) (parse_token (close_quotation (i+n))) - and parse_token i = + close_box i (box n) (parse_token 1 (close_quotation (i+n))) + and parse_token k i = let n = spaces 0 i in let i = i+n in - if i < l then match str.[i] with + if i < len then match str.[i] with (* Parse a ' *) - | '\'' when i+1 >= String.length str || str.[i+1] == ' ' -> - push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1))) + | '\'' when i+1 >= len || str.[i+1] == ' ' -> + push_white (n-k) (push_token (UnpTerminal "'") (parse_token 1 (i+1))) (* Parse the beginning of a quoted expression *) | '\'' -> - parse_quoted (n-1) (i+1) + parse_quoted (n-k) (i+1) (* Otherwise *) | _ -> - push_white (n-1) (parse_non_format i) + push_white (n-k) (parse_non_format i) else push_white n [[]] in try - if not (String.is_empty str) then match parse_token 0 with + if not (String.is_empty str) then match parse_token 0 0 with | [l] -> l | _ -> user_err Pp.(str "Box closed without being opened in format.") else - user_err Pp.(str "Empty format.") + [] with reraise -> let (e, info) = CErrors.push reraise in let info = Option.cata (Loc.add_loc info) info loc in @@ -522,35 +521,11 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let warn_skip_spaces_curly = - CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" - (fun () ->strbrk "Skipping spaces inside curly brackets") - -let rec drop_spacing = function - | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt - | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt - | fmt -> fmt - -let has_closing_curly_brace symbs fmt = - (* TODO: recognize and fail in case a box overlaps a pair of curly braces *) - let fmt = drop_spacing fmt in - match symbs, fmt with - | NonTerminal s :: symbs, (UnpTerminal s' as u) :: fmt when Id.equal s (Id.of_string s') -> - let fmt = drop_spacing fmt in - (match fmt with - | UnpTerminal "}" :: fmt -> Some (u :: fmt) - | _ -> None) - | _ -> None - let hunks_of_format (from,(vars,typs)) symfmt = - let a = ref None in let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when String.equal s' (String.make (String.length s') ' ') -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | symbs, (UnpTerminal "{") :: fmt when (a := has_closing_curly_brace symbs fmt; !a <> None) -> - let newfmt = Option.get !a in - aux (symbs,newfmt) | Terminal s :: symbs, (UnpTerminal s') :: fmt when String.equal s (String.drop_simple_quotes s') -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l @@ -705,26 +680,40 @@ let recompute_assoc typs = (**************************************************************************) (* Registration of syntax extensions (parsing/printing, no interpretation)*) -let pr_arg_level from = function +let pr_arg_level from (lev,typ) = + let pplev = match lev with | (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" - -let pr_level ntn (from,args) = + | (n,_) -> str "Unknown level" in + let pptyp = match typ with + | NtnInternTypeConstr -> mt () + | NtnInternTypeBinder -> str " " ++ surround (str "binder") + | NtnInternTypeIdent -> str " " ++ surround (str "ident") in + pplev ++ pptyp + +let pr_level ntn (from,args,typs) = str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ - prlist_with_sep pr_comma (pr_arg_level from) args + prlist_with_sep pr_comma (pr_arg_level from) (List.combine args typs) let error_incompatible_level ntn oldprec prec = user_err - (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ + (str "Notation " ++ qstring ntn ++ str " is already defined" ++ spc() ++ + pr_level ntn oldprec ++ + spc() ++ str "while it is now required to be" ++ spc() ++ + pr_level ntn prec ++ str ".") + +let error_parsing_incompatible_level ntn ntn' oldprec prec = + user_err + (str "Notation " ++ qstring ntn ++ str " relies on a parsing rule for " ++ qstring ntn' ++ spc() ++ + str " which is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") type syntax_extension = { - synext_level : Notation.level; + synext_level : Notation_term.level; synext_notation : notation; synext_notgram : notation_grammar; synext_unparsing : unparsing list; @@ -736,7 +725,17 @@ let is_active_compat = function | None -> true | Some v -> 0 <= Flags.version_compare v !Flags.compat_version -type syntax_extension_obj = locality_flag * syntax_extension list +type syntax_extension_obj = locality_flag * syntax_extension + +let check_and_extend_constr_grammar ntn rule = + try + let ntn_for_grammar = rule.notgram_notation in + if String.equal ntn ntn_for_grammar then raise Not_found; + let prec = rule.notgram_level in + let oldprec = Notation.level_of_notation ntn_for_grammar in + if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + with Not_found -> + Egramcoq.extend_constr_grammar rule let cache_one_syntax_extension se = let ntn = se.synext_notation in @@ -744,31 +743,30 @@ let cache_one_syntax_extension se = let onlyprint = se.synext_notgram.notgram_onlyprinting in try let oldprec = Notation.level_of_notation ntn in - if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec + if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram end let cache_syntax_extension (_, (_, sy)) = - List.iter cache_one_syntax_extension sy + cache_one_syntax_extension sy let subst_parsing_rule subst x = x let subst_printing_rule subst x = x let subst_syntax_extension (subst, (local, sy)) = - let map sy = { sy with - synext_notgram = subst_parsing_rule subst sy.synext_notgram; + (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; - } in - (local, List.map map sy) + }) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -1049,13 +1047,10 @@ let remove_curly_brackets l = | Terminal "{" as t1 :: l -> let br,next = skip_break [] l in (match next with - | NonTerminal _ as x :: l' as l0 -> + | NonTerminal _ as x :: l' -> let br',next' = skip_break [] l' in (match next' with - | Terminal "}" as t2 :: l'' as l1 -> - if not (List.equal Notation.symbol_eq l l0) || - not (List.equal Notation.symbol_eq l' l1) then - warn_skip_spaces_curly (); + | Terminal "}" as t2 :: l'' -> if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' @@ -1067,6 +1062,8 @@ let remove_curly_brackets l = module SynData = struct + type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list + (* XXX: Document *) type syn_data = { @@ -1089,17 +1086,28 @@ module SynData = struct intern_typs : notation_var_internalization_type list; (* Notation data for parsing *) - - level : int; - syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) - symbol list; (* symbols *) + level : level; + pa_syntax_data : subentry_types * symbol list; + pp_syntax_data : subentry_types * symbol list; not_data : notation * (* notation *) - (int * parenRelation) list * (* precedence *) + level * (* level, precedence, types *) bool; (* needs_squash *) } end +let find_subentry_types 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)) + symbols in + let sy_typs = List.map (set_entry_type etyps) typs in + let prec = List.map (assoc_of_type n) sy_typs in + sy_typs, prec + let compute_syntax_data df modifiers = let open SynData in let open NotationMods in @@ -1115,27 +1123,24 @@ let compute_syntax_data df modifiers = (* Notations for interp and grammar *) let ntn_for_interp = make_notation_key symbols in - let symbols' = remove_curly_brackets symbols in - let ntn_for_grammar = make_notation_key symbols' in - if not onlyprint then check_rule_productivity symbols'; - - (* Misc *) - let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in - let msgs,n = find_precedence mods.level mods.etyps symbols' in - let innerlevel = NumLevel 200 in - let typs = - find_symbols - (NumLevel n,BorderProd(Left,assoc)) - (innerlevel,InternalProd) - (NumLevel n,BorderProd(Right,assoc)) - symbols' in + let symbols_for_grammar = remove_curly_brackets symbols in + let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in + let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in + if not onlyprint then check_rule_productivity symbols_for_grammar; + let msgs,n = find_precedence mods.level mods.etyps symbols in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in - let sy_typs = List.map (set_entry_type etyps) typs in - let prec = List.map (assoc_of_type n) sy_typs in + let sy_typs, prec = + find_subentry_types n assoc etyps symbols in + let sy_typs_for_grammar, prec_for_grammar = + if need_squash then + find_subentry_types n assoc etyps symbols_for_grammar + else + sy_typs, prec in let i_typs = set_internalization_type sy_typs in - let sy_data = (sy_typs,symbols') in - let sy_fulldata = (ntn_for_grammar,prec,need_squash) in + let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in + let pp_sy_data = (sy_typs,symbols) in + let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in let i_data = ntn_for_interp, df' in @@ -1154,8 +1159,9 @@ let compute_syntax_data df modifiers = mainvars; intern_typs = i_typs; - level = n; - syntax_data = sy_data; + level = (n,prec,i_typs); + pa_syntax_data = pa_sy_data; + pp_syntax_data = pp_sy_data; not_data = sy_fulldata; } @@ -1236,25 +1242,9 @@ let with_syntax_protection f x = (**********************************************************************) (* Recovering existing syntax *) -let contract_notation ntn = - if String.equal ntn "{ _ }" then ntn else - let rec aux ntn i = - if i <= String.length ntn - 5 then - let ntn' = - if String.is_sub "{ _ }" ntn i && - (i = 0 || ntn.[i-1] = ' ') && - (i = String.length ntn - 5 || ntn.[i+5] = ' ') - then - String.sub ntn 0 i ^ "_" ^ - String.sub ntn (i+5) (String.length ntn -i-5) - else ntn in - aux ntn' (i+1) - else ntn in - aux ntn 0 - exception NoSyntaxRule -let recover_syntax ntn = +let recover_notation_syntax ntn = try let prec = Notation.level_of_notation ntn in let pp_rule,_ = Notation.find_notation_printing_rule ntn in @@ -1271,29 +1261,25 @@ let recover_syntax ntn = raise NoSyntaxRule let recover_squash_syntax sy = - let sq = recover_syntax "{ _ }" in - [sy; sq] - -let recover_notation_syntax rawntn = - let ntn = contract_notation rawntn in - let sy = recover_syntax ntn in - let need_squash = not (String.equal ntn rawntn) in - let rules = if need_squash then recover_squash_syntax sy else [sy] in - sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting + let sq = recover_notation_syntax "{ _ }" in + sy :: sq.synext_notgram.notgram_rules (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule i_typs level (typs,symbols) ntn onlyprint = +let make_pa_rule level (typs,symbols) ntn need_squash = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - { notgram_level = level; + let sy = { + notgram_level = level; notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; - notgram_typs = i_typs; - notgram_onlyprinting = onlyprint; - } + } in + (* By construction, the rule for "{ _ }" is declared, but we need to + redeclare it because the file where it is declared needs not be open + when the current file opens (especially in presence of -nois) *) + if need_squash then recover_squash_syntax sy else [sy] let make_pp_rule level (typs,symbols) fmt = match fmt with @@ -1302,21 +1288,16 @@ let make_pp_rule level (typs,symbols) fmt = (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in - let ntn, prec, need_squash = sd.not_data in - let pa_rule = make_pa_rule sd.intern_typs sd.level sd.syntax_data ntn sd.only_printing in - let pp_rule = make_pp_rule sd.level sd.syntax_data sd.format in - let sy = { - synext_level = (sd.level, prec); - synext_notation = ntn; - synext_notgram = pa_rule; + let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in + let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in + let pp_rule = make_pp_rule (pi1 sd.level) sd.pp_syntax_data sd.format in { + 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_extra = sd.extra; synext_compat = sd.compat; - } in - (* By construction, the rule for "{ _ }" is declared, but we need to - redeclare it because the file where it is declared needs not be open - when the current file opens (especially in presence of -nois) *) - if need_squash then recover_squash_syntax sy else [sy] + } (**********************************************************************) (* Main functions about notations *) @@ -1361,11 +1342,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin - let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in - let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in + let sy = recover_notation_syntax (make_notation_key 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 || onlyprint' in - i_typs, onlyprint + let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in + pi3 sy.synext_level, onlyprint end else [], false in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f63ed6f48..d2ba9eb1cc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1230,7 +1230,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in + let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1457,6 +1457,22 @@ let _ = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } +let _ = + declare_string_option + { optdepr = false; + optname = "native_compute profiler output"; + optkey = ["NativeCompute"; "Profile"; "Filename"]; + optread = Nativenorm.get_profile_filename; + optwrite = Nativenorm.set_profile_filename } + +let _ = + declare_bool_option + { optdepr = false; + optname = "enable native compute profiling"; + optkey = ["NativeCompute"; "Profiling"]; + optread = Nativenorm.get_profiling_enabled; + optwrite = Nativenorm.set_profiling_enabled } + let vernac_set_strategy locality l = let local = make_locality locality in let glob_ref r = |