diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 43 | ||||
| -rw-r--r-- | interp/impargs.ml | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 408 | ||||
| -rw-r--r-- | interp/notation.mli | 43 | ||||
| -rw-r--r-- | interp/reserve.ml | 2 |
5 files changed, 434 insertions, 68 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index a82e6b35a6..22e6cf9d1c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -39,7 +39,6 @@ type constant_obj = { cst_decl : global_declaration option; (** [None] when the declaration is a side-effect and has already been defined in the global environment. *) - cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; } @@ -94,28 +93,20 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (Constant.make1 kn) obj.cst_kind -let discharged_hyps kn sechyps = - let (_,dir,_) = KerName.repr kn in - let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev_map (Libnames.make_path dir) args - let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; } + Some { obj with cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { cst_decl = None; - cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; } @@ -142,7 +133,6 @@ let update_tables c = let register_side_effect (c, role) = let o = inConstant { cst_decl = None; - cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; } in @@ -194,7 +184,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; - cst_hyps = [] ; cst_kind = kind; cst_locl = local; } in @@ -255,7 +244,6 @@ let cache_variable ((sp,_),o) = poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; - Dischargedhypsmap.set_discharged_hyps sp []; add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with @@ -311,15 +299,15 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names -let load_inductive i ((sp,kn),(_,mie)) = +let load_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names -let open_inductive i ((sp,kn),(_,mie)) = +let open_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,mie)) = +let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in @@ -328,17 +316,14 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let discharge_inductive ((sp,kn),(dhyps,mie)) = +let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let info = section_segment_of_mutual_inductive mind in - let sechyps = info.Lib.abstr_ctx in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive info repl mie) + Some (Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -349,30 +334,28 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,m) = ([],{ +let dummy_inductive_entry m = { mind_entry_params = []; mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; -}) +} (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = +let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - (pth, mind_ent) + mind_ent | Cumulative_ind_entry cumi -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - (pth, InferCumulativity.infer_inductive env mind_ent) + InferCumulativity.infer_inductive env mind_ent end -type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry - -let inInductive : inductive_obj -> obj = +let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -426,7 +409,7 @@ let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in + let (sp,kn as oname) = add_leaf id (inInductive mie) in let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; diff --git a/interp/impargs.ml b/interp/impargs.ml index e542b818f6..3603367cf1 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -508,11 +508,11 @@ type implicit_discharge_request = | ImplInteractive of GlobRef.t * implicits_flags * implicit_interactive_request -let implicits_table = Summary.ref Refmap.empty ~name:"implicits" +let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" let implicits_of_global ref = try - let l = Refmap.find ref !implicits_table in + let l = GlobRef.Map.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in let rec rename implicits names = match implicits, names with @@ -527,7 +527,7 @@ let implicits_of_global ref = with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = - implicits_table := Refmap.add ref imps !implicits_table + implicits_table := GlobRef.Map.add ref imps !implicits_table let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l diff --git a/interp/notation.ml b/interp/notation.ml index 6b26f66100..02c7812e21 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -264,7 +264,7 @@ type key = | Oth let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 @@ -379,23 +379,364 @@ module InnerPrimToken = struct end -(* The following two tables of (un)interpreters will *not* be synchronized. - But their indexes will be checked to be unique *) +(* The following two tables of (un)interpreters will *not* be + synchronized. But their indexes will be checked to be unique. + These tables contain primitive token interpreters which are + registered in plugins, such as string and ascii syntax. It is + essential that only plugins add to these tables, and that + vernacular commands do not. See + https://github.com/coq/coq/issues/8401 for details of what goes + wrong when vernacular commands add to these tables. *) let prim_token_interpreters = (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) let prim_token_uninterpreters = (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) +(*******************************************************) +(* Numeral notation interpretation *) +type numeral_notation_error = + | UnexpectedTerm of Constr.t + | UnexpectedNonOptionTerm of Constr.t + +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +module Numeral = struct +(** * Numeral notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotANumber + +let warn_large_num = + CWarnings.create ~name:"large-number" ~category:"numbers" + (fun ty -> + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed).") + +let warn_abstract_large_num = + CWarnings.create ~name:"abstract-large-number" ~category:"numbers" + (fun (ty,f) -> + strbrk "To avoid stack overflow, large numbers in " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ + Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: only used to decide when a + number is considered as large (see warnings above). *) + +exception Comp of int + +let rec rawnum_compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - rawnum_compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Pervasives.compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + +(***********************************************************************) + +(** ** Conversion between Coq [Decimal.int] and internal raw string *) + +(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) + +let digit_of_char c = + assert ('0' <= c && c <= '9'); + Char.code c - Char.code '0' + 2 + +let char_of_digit n = + assert (2<=n && n<=11); + Char.chr (n-2 + Char.code '0') + +let coquint_of_rawnum uint str = + let nil = mkConstruct (uint,1) in + let rec do_chars s i acc = + if i < 0 then acc + else + let dg = mkConstruct (uint, digit_of_char s.[i]) in + do_chars s (i-1) (mkApp(dg,[|acc|])) + in + do_chars str (String.length str - 1) nil + +let coqint_of_rawnum inds (str,sign) = + let uint = coquint_of_rawnum inds.uint str in + mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + +let rawnum_of_coquint c = + let rec of_uint_loop c buf = + match Constr.kind c with + | Construct ((_,1), _) (* Nil *) -> () + | App (c, [|a|]) -> + (match Constr.kind c with + | Construct ((_,n), _) (* D0 to D9 *) -> + let () = Buffer.add_char buf (char_of_digit n) in + of_uint_loop a buf + | _ -> raise NotANumber) + | _ -> raise NotANumber + in + let buf = Buffer.create 64 in + let () = of_uint_loop c buf in + if Int.equal (Buffer.length buf) 0 then + (* To avoid ambiguities between Nil and (D0 Nil), we choose + to not display Nil alone as "0" *) + raise NotANumber + else Buffer.contents buf + +let rawnum_of_coqint c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) + | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | _ -> raise NotANumber) + | _ -> raise NotANumber + + +(***********************************************************************) + +(** ** Conversion between Coq [Z] and internal bigint *) + +(** First, [positive] from/to bigint *) + +let rec pos_of_bigint posty n = + match Bigint.div2_with_rest n with + | (q, false) -> + let c = mkConstruct (posty, 2) in (* xO *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) when not (Bigint.equal q Bigint.zero) -> + let c = mkConstruct (posty, 1) in (* xI *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) -> + mkConstruct (posty, 3) (* xH *) + +let rec bigint_of_pos c = match Constr.kind c with + | Construct ((_, 3), _) -> (* xH *) Bigint.one + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) + | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | n -> assert false (* no other constructor of type positive *) + end + | x -> raise NotANumber + end + | x -> raise NotANumber + +(** Now, [Z] from/to bigint *) + +let z_of_bigint { z_ty; pos_ty } n = + if Bigint.equal n Bigint.zero then + mkConstruct (z_ty, 1) (* Z0 *) + else + let (s, n) = + if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) + else (3, Bigint.neg n) (* Zneg *) + in + let c = mkConstruct (z_ty, s) in + mkApp (c, [| pos_of_bigint pos_ty n |]) + +let bigint_of_z z = match Constr.kind z with + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 2 -> (* Zpos *) bigint_of_pos d + | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | n -> assert false (* no other constructor of type Z *) + end + | _ -> raise NotANumber + end + | _ -> raise NotANumber + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotANumber + +let rec glob_of_constr ?loc env sigma c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc env sigma c in + let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c)) + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc env sigma c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c)) + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotANumber + +let big2raw n = + if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) + else (Bigint.to_string (Bigint.neg n), false) + +let raw2big (n,s) = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + +let interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + warn_large_num o.num_ty + | _ -> () + end; + let c = match fst o.to_kind with + | Int int_ty -> coqint_of_rawnum int_ty n + | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + warn_abstract_large_num (o.num_ty,o.to_ty); + glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|])) + | _ -> + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc env sigma res + | Option -> interp_option o.num_ty ?loc env sigma res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + match fst o.of_kind with + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) +end + +(* A [prim_token_infos], which is synchronized with the document + state, either contains a unique id pointing to an unsynchronized + prim token function, or a numeral notation object describing how to + interpret and uninterpret. We provide [prim_token_infos] because + we expect plugins to provide their own interpretation functions, + rather than going through numeral notations, which are available as + a vernacular. *) + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + (* Table from scope_name to backtrack-able informations about interpreters (in particular interpreter unique id). *) let prim_token_interp_infos = - ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t) + ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t) (* Table from global_reference to backtrack-able informations about prim_token uninterpretation (in particular uninterpreter unique id). *) let prim_token_uninterp_infos = - ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) + ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t) let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with @@ -425,23 +766,14 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter register_gen_interpretation allow_overwrite uid (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) -type prim_token_infos = { - pt_local : bool; (** Is this interpretation local? *) - pt_scope : scope_name; (** Concerned scope *) - pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) - pt_required : required_module; (** Module that should be loaded first *) - pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) - pt_in_match : bool (** Is this prim token legal in match patterns ? *) -} - let cache_prim_token_interpretation (_,infos) = + let ptii = infos.pt_interp_info in let sc = infos.pt_scope in - let uid = infos.pt_uid in check_scope ~tolerant:true sc; prim_token_interp_infos := - String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; + String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := - Refmap.add r (sc,uid,infos.pt_in_match) + GlobRef.Map.add r (sc,ptii,infos.pt_in_match) !prim_token_uninterp_infos) infos.pt_refs @@ -479,7 +811,7 @@ let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = enable_prim_token_interpretation { pt_local = local; pt_scope = sc; - pt_uid = uid; + pt_interp_info = Uid uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } @@ -489,7 +821,7 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = enable_prim_token_interpretation { pt_local = local; pt_scope = sc; - pt_uid = uid; + pt_interp_info = Uid uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } @@ -605,9 +937,12 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in + let (spdir,info) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let interp = Hashtbl.find prim_token_interpreters uid in + let interp = match info with + | Uid uid -> Hashtbl.find prim_token_interpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + in let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -783,8 +1118,11 @@ let uninterp_prim_token c = | None -> raise Notation_ops.No_match | Some r -> try - let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in - let uninterp = Hashtbl.find prim_token_uninterpreters uid in + let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in + let uninterp = match info with + | Uid uid -> Hashtbl.find prim_token_uninterpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) @@ -799,12 +1137,16 @@ let availability_of_prim_token n printer_scope local_scopes = let f scope = try let uid = snd (String.Map.find scope !prim_token_interp_infos) in - let interp = Hashtbl.find prim_token_interpreters uid in let open InnerPrimToken in - match n, interp with - | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true - | String _, StringInterp _ -> true - | _ -> false + match n, uid with + | Numeral _, NumeralNotation _ -> true + | _, NumeralNotation _ -> false + | _, Uid uid -> + let interp = Hashtbl.find prim_token_interpreters uid in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false with Not_found -> false in let scopes = make_current_scopes local_scopes in @@ -924,7 +1266,7 @@ let rec update_scopes cls scl = match cls, scl with | _, [] -> List.map find_scope_class_opt cls | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl -let arguments_scope = ref Refmap.empty +let arguments_scope = ref GlobRef.Map.empty type arguments_scope_discharge_request = | ArgsScopeAuto @@ -934,7 +1276,7 @@ type arguments_scope_discharge_request = let load_arguments_scope _ (_,(_,r,n,scl,cls)) = List.iter (Option.iter check_scope) scl; let initial_stamp = ScopeClassMap.empty in - arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope + arguments_scope := GlobRef.Map.add r (scl,cls,initial_stamp) !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o @@ -1015,13 +1357,13 @@ let declare_arguments_scope local r scl = let find_arguments_scope r = try - let (scl,cls,stamp) = Refmap.find r !arguments_scope in + let (scl,cls,stamp) = GlobRef.Map.find r !arguments_scope in let cur_stamp = !scope_class_map in if stamp == cur_stamp then scl else (* Recent changes in the Bind Scope base, we re-compute the scopes *) let scl' = update_scopes cls scl in - arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope; + arguments_scope := GlobRef.Map.add r (scl',cls,cur_stamp) !arguments_scope; scl' with Not_found -> [] @@ -1350,7 +1692,7 @@ let init () = notations_key_table := KeyMap.empty; scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; - prim_token_uninterp_infos := Refmap.empty + prim_token_uninterp_infos := GlobRef.Map.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index 6e59c0fd70..734198bbf6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -102,10 +102,51 @@ val register_bignumeral_interpretation : val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit +(** * Numeral notation *) + +type numeral_notation_error = + | UnexpectedTerm of Constr.t + | UnexpectedNonOptionTerm of Constr.t + +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) - pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) diff --git a/interp/reserve.ml b/interp/reserve.ml index 071248f01f..edbdf1dbba 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -28,7 +28,7 @@ type key = (** TODO: share code from Notation *) let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 |