(*
    ||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_______________________________________________________________ *)

module N = Level

type ix = int (* index *)

type id = string (* identifier *)

type info = string * string (* language, text *)

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

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

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

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