--- /dev/null
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 14/06/2000 *)
+(* *)
+(* This module defines the internal representation of the objects (variables, *)
+(* blocks of (co)inductive definitions and constants) and the terms of cic *)
+(* *)
+(******************************************************************************)
+
+(* STUFF TO MANAGE IDENTIFIERS *)
+type id = string (* the abstract type of the (annotated) node identifiers *)
+type anntarget =
+ Object of annobj
+ | Term of annterm
+
+(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
+and sort =
+ Prop
+ | Set
+ | Type
+and name =
+ Name of string
+ | Anonimous
+and term =
+ Rel of int (* DeBrujin index *)
+ | Var of UriManager.uri (* uri *)
+ | Meta of int (* numeric id *)
+ | Sort of sort (* sort *)
+ | Implicit (* *)
+ | 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*)
+ | Abst of UriManager.uri (* uri *)
+ | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*)
+ | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
+ int * int (* typeno, consno *)
+ (*CSC: serve cookingsno?*)
+ | 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 *)
+
+and annterm =
+ ARel of id * annotation option ref *
+ int * string option (* DeBrujin index, binder *)
+ | AVar of id * annotation option ref *
+ UriManager.uri (* uri *)
+ | AMeta of id * annotation option ref * int (* numeric id *)
+ | ASort of id * annotation option ref * sort (* sort *)
+ | AImplicit of id * annotation option ref (* *)
+ | ACast of id * annotation option ref *
+ annterm * annterm (* value, type *)
+ | AProd of id * annotation option ref *
+ name * annterm * annterm (* binder, source, target *)
+ | ALambda of id * annotation option ref *
+ name * annterm * annterm (* binder, source, target *)
+ | AAppl of id * annotation option ref *
+ annterm list (* arguments *)
+ | AConst of id * annotation option ref *
+ UriManager.uri * int (* uri, number of cookings*)
+ | AAbst of id * annotation option ref *
+ UriManager.uri (* uri *)
+ | AMutInd of id * annotation option ref *
+ UriManager.uri * int * int (* uri, cookingsno, typeno*)
+ | AMutConstruct of id * annotation option ref *
+ UriManager.uri * int * (* uri, cookingsno, *)
+ int * int (* typeno, consno *)
+ (*CSC: serve cookingsno?*)
+ | AMutCase of id * annotation option ref *
+ UriManager.uri * int * (* ind. uri, cookingsno *)
+ int * (* ind. typeno, *)
+ annterm * annterm * (* outtype, ind. term *)
+ annterm list (* patterns *)
+ | AFix of id * annotation option ref *
+ int * anninductiveFun list (* funno, functions *)
+ | ACoFix of id * annotation option ref *
+ int * anncoInductiveFun list (* funno, functions *)
+and annobj =
+ ADefinition of id * annotation option ref *
+ string * (* id, *)
+ annterm * annterm * (* value, type, *)
+ (int * UriManager.uri list) list exactness (* parameters *)
+ | AAxiom of id * annotation option ref *
+ string * annterm * (* id, type *)
+ (int * UriManager.uri list) list (* parameters *)
+ | AVariable of id * annotation option ref *
+ string * annterm (* name, type *)
+ | ACurrentProof of id * annotation option ref *
+ string * (int * annterm) list * (* name, conjectures, *)
+ annterm * annterm (* value, type *)
+ | AInductiveDefinition of id *
+ annotation option ref * anninductiveType list * (* inductive types , *)
+ (int * UriManager.uri list) list * int (* parameters,n ind. pars*)
+and anninductiveType =
+ string * bool * annterm * (* typename, inductive, arity *)
+ annconstructor list (* constructors *)
+and annconstructor =
+ string * annterm * bool list option ref (* id, type, really recursive *)
+and anninductiveFun =
+ string * int * annterm * annterm (* name, ind. index, type, body *)
+and anncoInductiveFun =
+ string * annterm * annterm (* name, type, body *)
+and annotation =
+ string
+and 'a exactness =
+ Possible of 'a (* an approximation to something *)
+ | Actual of 'a (* something *)
+;;
projects / helm.git / blobdiff