package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file comPrimitive.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Names

let declare id entry =
  let _ : Constant.t =
    Declare.declare_constant ~name:id ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry)
  in
  Flags.if_verbose Feedback.msg_info Pp.(Id.print id ++ str " is declared")

let do_primitive id udecl prim typopt =
  if Global.sections_are_opened () then
    CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
  if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
  let loc = id.CAst.loc in
  let id = id.CAst.v in
  match typopt with
  | None ->
    if Option.has_some udecl then
      CErrors.user_err ?loc
        Pp.(strbrk "Cannot use a universe declaration without a type when declaring primitives.");
    let e = Declare.primitive_entry prim in
    declare id e
  | Some typ ->
    let env = Global.env () in
    let evd, udecl = Constrintern.interp_univ_decl_opt env udecl in
    let auctx = CPrimitives.op_or_type_univs prim in
    let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in
    let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in
    let evd, (typ,impls) =
      Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
        env evd typ
    in
    let evd = try Evarconv.unify_delay env evd typ expected_typ
      with Evarconv.UnableToUnify (evd,e) as exn ->
        let _, info = Exninfo.capture exn in
        Exninfo.iraise (Pretype_errors.(
            PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info))
    in
    Pretyping.check_evars_are_solved ~program_mode:false env evd;
    let evd = Evd.minimize_universes evd in
    let uvars = EConstr.universes_of_constr evd typ in
    let evd = Evd.restrict_universe_context evd uvars in
    let typ = EConstr.to_constr evd typ in
    let univ_entry = Evd.check_univ_decl ~poly:(not (Univ.AbstractContext.is_empty auctx)) evd udecl in
    let entry = Declare.primitive_entry ~types:(typ, univ_entry) prim in
    declare id entry
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct