helm/software/components/ng_kernel/nCic.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 type sort =
  27  | Prop
  28  | Set
  29  | Type of int
  30  | CProp
  31
  32 type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
  33
  34 type name = Name of string | Anonymous
  35
  36 type local_context = int * (term list) option         (* shift (0 -> no shift),
  37                                                          subst (None means id) *)
  38
  39 and term =
  40  | Rel      of int                                    (* DeBruijn index, 1 based         *)
  41  | Meta     of int * string option * local_context
  42  | Appl     of term list                              (* arguments                       *)
  43  | Prod     of name * term * term                     (* binder, source, target          *)
  44  | Lambda   of name * term * term                     (* binder, source, target          *)
  45  | LetIn    of name * term * term * term              (* binder, type, term, body        *)
  46  | Const    of NUriManager.reference                         (* reference contains indtypeno/constrno *)
  47  | Sort     of sort                                   (* sort                            *)
  48  | Implicit of implicit_annotation                    (* ... *)
  49  | MutCase  of NUriManager.reference *                      (* ind. reference,             *)
  50     term * term *                                   (*  outtype, ind. term   *)
  51     term list                                       (*  patterns             *)
  52
  53 and obj =
  54  | Constant of term option * term
  55  | InductiveDefinition of inductiveType list    (* inductive types,         *)
  56
  57 and inductiveType =
  58  string * bool * term *                       (* typename, inductive, arity *)
  59   constructor list                            (*  constructors              *)
  60
  61 and constructor =
  62  string * term                                (* id, type *)
  63