Appendix B   La rappresentazione OCaml dei termini e degli oggetti CIC

type sort =
   Prop
 | Set
 | Type
and name =
   Name of string
 | Anonimous
and term =
   Rel of int                             (* DeBrujin index *)
 | Var of UriManager.uri                  (* base uri, name *)
 | Meta of int				  (* numeric id *)
 | Sort of sort                           (* sort *)
 | Cast of term * term                    (* value, type *)
 | Prod of name * term * term             (* binder, source, target *)
 | Lambda of name * term * term           (* binder, source, target *)
 | Appl of term list                      (* arguments *)
 | Const of UriManager.uri * int          (* uri, number of cookings*)
 | MutInd of UriManager.uri * int * int   (* uri, cookingsno, typeno*)
 | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
    int * int                             (*  typeno, consno  *)
 | MutCase of UriManager.uri * int *      (* ind. uri, cookingsno, *)
    int *                                 (*  ind. typeno,         *)
    term * term *                         (*  outtype, ind. term   *)
    term list                             (*  patterns             *)
 | Fix of int * inductiveFun list         (* funno, functions *)
 | CoFix of int * coInductiveFun list     (* funno, functions *)
and obj =
   Definition of string * term * term *         (* id, value, type,         *)
    (int * UriManager.uri list) list            (*  parameters              *)
 | Axiom of string * term *
    (int * UriManager.uri list) list            (* id, type, parameters     *)
 | Variable of string * term                    (* name, type               *)
 | CurrentProof of string * (int * term) list * (* name, conjectures,       *)
    term * term                                 (*  value, type             *)
 | InductiveDefinition of inductiveType list *  (* inductive types,         *)
    (int * UriManager.uri list) list * int      (*  parameters, n ind. pars *)
and inductiveType = 
 string * bool * term *                   (* typename, inductive, arity *)
  constructor list                        (*  constructors              *)
and constructor =
 string * term * bool list option ref     (* id, type, really recursive *)
and inductiveFun =
 string * int * term * term               (* name, ind. index, type, body *)
and coInductiveFun =
 string * term * term                     (* name, type, body *)
;;