matitaB/components/ng_kernel/nCicEnvironment.mli

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 exception CircularDependency of string Lazy.t;;
  15 exception ObjectNotFound of string Lazy.t;;
  16 exception BadDependency of string Lazy.t * exn;;
  17 exception AlreadyDefined of string Lazy.t;;
  18
  19 type item =
  20   [ `Obj of NUri.uri * NCic.obj
  21   | `Constr of NCic.universe * NCic.universe ]
  22 ;;
  23
  24 type obj_exn =
  25   [ `WellTyped of NCic.obj
  26   | `Exn of exn ]
  27 ;;
  28
  29 type db
  30
  31 class type g_status =
  32   object
  33     method env_db : db
  34   end
  35
  36 class virtual status : string option ->
  37  object('self)
  38   inherit NCic.status
  39   inherit g_status
  40   method set_env_db : db -> 'self
  41   method set_env_status : #g_status -> 'self
  42  end
  43
  44 val set_get_obj : (status -> NUri.uri -> NCic.obj) -> unit
  45 val set_typecheck_obj : (status -> NCic.obj -> unit) -> unit
  46
  47 val get_checked_obj: #status -> NUri.uri -> NCic.obj
  48
  49 val check_and_add_obj: #status -> NCic.obj -> unit
  50
  51 val get_relevance: #status -> NReference.reference -> bool list
  52
  53 val get_checked_def:
  54     #status -> NReference.reference ->
  55     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
  56
  57 (* the last integer is the index of the inductive type in the reference *)
  58 val get_checked_indtys:
  59     #status -> NReference.reference ->
  60     bool * int * NCic.inductiveType list * NCic.i_attr * int
  61
  62 val get_checked_fixes_or_cofixes:
  63    #status -> NReference.reference ->
  64    NCic.inductiveFun list * NCic.f_attr * int
  65
  66 val invalidate_item:
  67       #status ->
  68       [ `Obj of NUri.uri * NCic.obj
  69       | `Constr of NCic.universe * NCic.universe ] -> unit
  70
  71 val invalidate: #status -> unit
  72
  73 (* =========== universes ============= *)
  74
  75 (* utils *)
  76 val ppsort : Format.formatter -> NCic.sort -> unit
  77 val pp_constraints: #status -> string
  78 val get_universes: #status -> NCic.universe list
  79
  80 (* use to type products *)
  81 val max: NCic.universe -> NCic.universe -> NCic.universe
  82
  83 (* raise BadConstraints if the second arg. is an inferred universe or
  84  * if the added constraint gives circularity *)
  85 exception BadConstraint of string Lazy.t;;
  86 val add_lt_constraint: #status -> NCic.universe -> NCic.universe -> unit
  87 val universe_eq: NCic.universe -> NCic.universe -> bool
  88 val universe_leq: #status -> NCic.universe -> NCic.universe -> bool
  89 val universe_lt: #status -> NCic.universe -> NCic.universe -> bool
  90
  91 (* checks if s1 <= s2 *)
  92 val are_sorts_convertible: #status -> test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
  93
  94 (* to type a Match *)
  95 val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
  96
  97 (* algebraic successor function *)
  98 exception UntypableSort of string Lazy.t
  99 exception AssertFailure of string Lazy.t
 100 val typeof_sort: #status -> NCic.sort -> NCic.sort
 101
 102 (* looks for a declared universe that is the least one above the input *)
 103 val sup : #status -> NCic.universe -> NCic.universe option
 104 val inf : #status -> strict:bool -> NCic.universe -> NCic.universe option
 105 val family_of : NCic.universe -> [ `CProp | `Type ]
 106
 107 (* =========== /universes ============= *)
 108
 109 (* EOF *)