helm/software/lambda-delta/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 * term) list (* name, 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
  35 type command = Graph of id                       (* hierarchy graph: name *)
  36              | Sorts of (int option * id) list   (* sorts: index, name *)
  37              | Section of id option              (* section: Some id = open, None = close last *)
  38              | Entity of kind * id * desc * term (* entity: class, name, description, contents *)