helm/software/lambda-delta/src/text/txt.ml

   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 type ix = int (* index *)
  13
  14 type id = string (* identifier *)
  15
  16 type desc = string (* description *)
  17
  18 type kind = Decl (* generic declaration *)
  19           | Ax   (* axiom               *)
  20           | Def  (* generic definition  *)
  21           | Th   (* theorem             *)
  22
  23 type bind = Abst of (id * bool * term) list (* name, real?, domain *)
  24           | Abbr of (id * term) list        (* name, bodies        *)
  25           | Void of id list                 (* names               *)
  26
  27 and term = Sort of ix                      (* level                          *)
  28          | NSrt of id                      (* named level                    *)
  29          | LRef of ix * ix                 (* index, offset                  *)
  30          | NRef of id                      (* name                           *)
  31          | Cast of term * term             (* domain, element                *)
  32          | Appl of term list * term        (* arguments, function            *)
  33          | Bind of bind * term             (* binder, scope                  *)
  34          | Inst of term * term list        (* function, arguments            *)
  35          | Impl of bool * id * term * term (* strong?, label, source, target *)
  36
  37 type command = Require of id list                (* required files: names *)
  38              | Graph of id                       (* hierarchy graph: name *)
  39              | Sorts of (int option * id) list   (* sorts: index, name *)
  40              | Section of id option              (* section: Some id = open, None = close last *)
  41              | Entity of kind * id * desc * term (* entity: class, name, description, contents *)
  42              | Generate of term list             (* predefined generated entity: arguments *)