(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

type ix = int (* index *)

type id = string (* identifier *)

type desc = string (* description *)

type kind = Decl (* generic declaration *) 
          | Ax   (* axiom               *)
	  | Def  (* generic definition  *)
	  | Th   (* theorem             *)

type bind = Abst of (id * bool * term) list (* name, real?, domain *)
          | Abbr of (id * term) list        (* name, bodies        *)
          | Void of id list                 (* names               *)

and term = Sort of ix                      (* level                          *)
         | NSrt of id                      (* named level                    *)
	 | LRef of ix * ix                 (* index, offset                  *)
	 | NRef of id                      (* name                           *)
	 | Cast of term * term             (* domain, element                *)
	 | Appl of term list * term        (* arguments, function            *)
	 | Bind of bind * term             (* binder, scope                  *)
	 | Inst of term * term list        (* function, arguments            *)
	 | Impl of bool * id * term * term (* strong?, label, source, target *)

type command = Require of id list                (* required files: names *)
             | Graph of id                       (* hierarchy graph: name *) 
             | Sorts of (int option * id) list   (* sorts: index, name *)
	     | Section of id option              (* section: Some id = open, None = close last *)
	     | Entity of kind * id * desc * term (* entity: class, name, description, contents *) 
             | Generate of term list             (* predefined generated entity: arguments *)