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 comm = string (* comment *)
  17
  18 type bind = Abst of (id * term) list (* name, domain *)
  19           | Abbr of (id * term) list (* name, bodies *)
  20           | Void of id list          (* names        *)
  21
  22 and term = Sort of ix               (* level               *)
  23          | NSrt of id               (* named level         *)
  24          | LRef of ix * ix          (* index, offset       *)
  25          | NRef of id               (* name                *)
  26          | Cast of term * term      (* domain, element     *)
  27          | Appl of term list * term (* arguments, function *)
  28          | Bind of bind * term      (* binder, scope       *)
  29
  30 type entity = Section of id option              (* section: Some id = open, None = close last *)
  31             | Global of bool * id * comm * term (* global entity: false = decl, true = def    *)