(*
    ||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 = Layer

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 = 
(* layer, name, real?, domain *)
          | Abst of N.layer * id * bool * term
(* name, bodies *)
	  | Abbr of id * term                  
(* name *)
          | Void of id

and lenv = bind list

and term =
(* level *)
         | Sort of ix
(* named level *)
         | NSrt of id
(* index, offset *)
	 | LRef of ix
(* name *)
	 | NRef of id
(* domain, element *)
	 | Cast of term * term
(* arguments, function *)
	 | Appl of term * term
(* environment, scope *)
         | Proj of lenv * term
(* function, arguments *)
	 | Inst of term * term list

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 *)
	     | Constant of bool * kind * id * info * term
(* predefined generated entity: arguments *)
             | Generate of term list