diff options
| -rw-r--r-- | intf/vernacexpr.mli | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
8 files changed, 45 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 138ef5cbb..f0f565b53 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -203,6 +203,11 @@ type scheme = | CaseScheme of bool * reference or_by_notation * sort_expr | EqualityScheme of reference or_by_notation +(* This type allows to register inline of constants in native compiler. + It will be extended with primitive inductive types and operators *) +type register_kind = + | RegisterInline + type bullet = | Dash | Star @@ -373,6 +378,7 @@ type vernac_expr = | VernacPrint of printable | VernacSearch of searchable * search_restriction | VernacLocate of locatable + | VernacRegister of lident * register_kind | VernacComments of comment list | VernacNop diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 62e2d46a8..636644ec3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -771,3 +771,18 @@ let j_type j = j.uj_type let safe_infer senv = infer (env_of_senv senv) let typing senv = Typeops.typing (env_of_senv senv) + +(* This function serves only for inlining constants in native compiler for now, +but it is meant to become a replacement for environ.register *) +let register_inline kn senv = + if not (evaluable_constant kn senv.env) then + Errors.error "Register inline: an evaluable constant is expected"; + let env = pre_env senv.env in + let (cb,r) = Cmap_env.find kn env.Pre_env.env_globals.Pre_env.env_constants in + let cb = {cb with const_inline_code = true} in + let new_constants = + Cmap_env.add kn (cb,r) env.Pre_env.env_globals.Pre_env.env_constants + in + let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in + let env = { env with Pre_env.env_globals = new_globals } in + { senv with env = env_of_pre_env env } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 31bb8143e..7ca033383 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -136,3 +136,5 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : safe_environment -> field -> Retroknowledge.entry -> constr -> safe_environment + +val register_inline : constant -> safe_environment -> safe_environment diff --git a/library/global.ml b/library/global.ml index f120ef195..28b691769 100644 --- a/library/global.ml +++ b/library/global.ml @@ -162,4 +162,5 @@ let register field value by_clause = let senv = Safe_typing.register !global_env field entry by_clause in global_env := senv - +let register_inline c = + global_env := Safe_typing.register_inline c !global_env diff --git a/library/global.mli b/library/global.mli index 531526846..3238294f2 100644 --- a/library/global.mli +++ b/library/global.mli @@ -104,3 +104,5 @@ val env_of_context : Environ.named_context_val -> Environ.env (** spiwack: register/unregister function for retroknowledge *) val register : Retroknowledge.field -> constr -> constr -> unit + +val register_inline : constant -> unit diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7a78a7dae..bc07fe896 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -177,7 +177,10 @@ GEXTEND Gram VernacCoFixpoint (Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; - l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) + | IDENT "Register"; IDENT "Inline"; id = identref -> + VernacRegister(id, RegisterInline) + ] ] ; gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 427317a45..d8ddb275d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -920,6 +920,9 @@ let rec pr_vernac = function | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid in str"Locate" ++ spc() ++ pr_locate loc + | VernacRegister (id, RegisterInline) -> + hov 2 + (str "Register Inline" ++ spc() ++ pr_lident id) | VernacComments l -> hov 2 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 526aa9230..bac1fcd48 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1513,6 +1513,16 @@ let vernac_locate = function | LocateTactic qid -> print_located_tactic qid | LocateFile f -> msg_notice (locate_file f) +let vernac_register id r = + if Pfedit.refining () then + error "Cannot register a primitive while in proof editing mode."; + let t = (Constrintern.global_reference (snd id)) in + if not (isConst t) then + error "Register inline: a constant is expected"; + let kn = destConst t in + match r with + | RegisterInline -> Global.register_inline kn + (****************) (* Backtracking *) @@ -1823,6 +1833,7 @@ let interp locality c = match c with | VernacPrint p -> vernac_print p | VernacSearch (s,r) -> vernac_search s r | VernacLocate l -> vernac_locate l + | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> if_verbose msg_info (str "Comments ok\n") | VernacNop -> () |