type implicit_annotation = [ `Closed | `Type | `Hole ]
-type anntarget =
- Object of annobj (* if annobj is a Constant, this is its type *)
- | ConstantBody of annobj
- | Term of annterm
- | Conjecture of annconjecture
- | Hypothesis of annhypothesis
-
(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
-and sort =
+
+type sort =
Prop
| Set
| Type of CicUniv.universe
| CProp
-and name =
- Name of string
+
+type name =
+ | Name of string
| Anonymous
-and term =
+
+type object_class =
+ [ `Coercion
+ | `Elim of sort (** elimination principle; if sort is Type, the universe is
+ * not relevant *)
+ | `Record (** inductive type that encodes a record *)
+ | `Projection (** record projection *)
+ ]
+
+type attribute =
+ [ `Class of object_class
+ | `Generated
+ ]
+
+type term =
Rel of int (* DeBrujin index, 1 based*)
| Var of UriManager.uri * (* uri, *)
term explicit_named_substitution (* explicit named subst. *)
| CoFix of int * coInductiveFun list (* funno (0 based), funs *)
and obj =
Constant of string * term option * term * (* id, body, type, *)
- UriManager.uri list (* parameters *)
+ UriManager.uri list * attribute list (* parameters *)
| Variable of string * term option * term * (* name, body, type *)
- UriManager.uri list (* parameters *)
- | CurrentProof of string * metasenv * (* name, conjectures, *)
- term * term * UriManager.uri list (* value, type, parameters *)
+ UriManager.uri list * attribute list (* parameters *)
+ | CurrentProof of string * metasenv * term * (* name, conjectures, value,*)
+ term * UriManager.uri list * attribute list (* type, parameters *)
| InductiveDefinition of inductiveType list * (* inductive types, *)
- UriManager.uri list * int (* params, left params no *)
+ UriManager.uri list * int * attribute list (* params, left params no *)
and inductiveType =
string * bool * term * (* typename, inductive, arity *)
constructor list (* constructors *)
and annobj =
AConstant of id * id option * string * (* name, *)
annterm option * annterm * (* body, type, *)
- UriManager.uri list (* parameters *)
+ UriManager.uri list * attribute list (* parameters *)
| AVariable of id *
string * annterm option * annterm * (* name, body, type *)
- UriManager.uri list (* parameters *)
+ UriManager.uri list * attribute list (* parameters *)
| ACurrentProof of id * id *
string * annmetasenv * (* name, conjectures, *)
- annterm * annterm * UriManager.uri list (* value,type,parameters *)
+ annterm * annterm * UriManager.uri list * (* value,type,parameters *)
+ attribute list
| AInductiveDefinition of id *
anninductiveType list * (* inductive types , *)
- UriManager.uri list * int (* parameters,n ind. pars*)
+ UriManager.uri list * int * attribute list (* parameters,n ind. pars*)
and anninductiveType =
id * string * bool * annterm * (* typename, inductive, arity *)
annconstructor list (* constructors *)
and anncontext = annhypothesis list
;;
+
+type anntarget =
+ Object of annobj (* if annobj is a Constant, this is its type *)
+ | ConstantBody of annobj
+ | Term of annterm
+ | Conjecture of annconjecture
+ | Hypothesis of annhypothesis
+
exception IllFormedXml of int;;
exception NotImplemented;;
+ (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
+ * returns the empty list of attributes reported here *)
+let obj_attributes = []
+let get_obj_attributes (n: 'a Pxp_document.node) =
+ obj_attributes
+
(* Utility functions that transform a Pxp attribute into something useful *)
let uri_list_of_attr a =
let module U = UriManager in
let module D = Pxp_document in
let module C = Cic in
+ let obj_attrs = get_obj_attributes n in
let ntype = n#node_type in
match ntype with
D.T_element "ConstantType" ->
(match nbody with
None ->
(* Axiom *)
- C.AConstant (xid, None, name, None, typ, params)
+ C.AConstant (xid, None, name, None, typ, params, obj_attrs)
| Some nbody' ->
let nbodytype = nbody'#node_type in
match nbodytype with
let xidbody = string_of_attr (nbody'#attribute "id") in
let value = (get_content nbody')#extension#to_cic_term [] in
if paramsbody = params then
- C.AConstant (xid, Some xidbody, name, Some value, typ, params)
+ C.AConstant (xid, Some xidbody, name, Some value, typ, params,
+ obj_attrs)
else
raise (IllFormedXml 6)
| D.T_element "CurrentProof" ->
let xidbody = string_of_attr (nbody'#attribute "id") in
let sons = nbody'#sub_nodes in
let (conjs, value) = get_conjs_value sons in
- C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
+ C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
+ obj_attrs)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 6)
let inductiveTypes = get_inductive_types sons
and params = uri_list_of_attr (n#attribute "params")
and nparams = int_of_attr (n#attribute "noParams") in
- C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
+ C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs)
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
and params = uri_list_of_attr (n#attribute "params")
(None, t'#extension#to_cic_term [])
| _ -> raise (IllFormedXml 6)
in
- C.AVariable (xid,name,body,typ,params)
+ C.AVariable (xid,name,body,typ,params,obj_attrs)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 7)
| Cic.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
| _ -> failwith "not enough prods"
+let params_of_obj = function
+ | Cic.Constant (_, _, _, params, _)
+ | Cic.Variable (_, _, _, params, _)
+ | Cic.CurrentProof (_, _, _, _, params, _)
+ | Cic.InductiveDefinition (_, params, _, _) ->
+ params
+
+let attributes_of_obj = function
+ | Cic.Constant (_, _, _, _, attributes)
+ | Cic.Variable (_, _, _, _, attributes)
+ | Cic.CurrentProof (_, _, _, _, _, attributes)
+ | Cic.InductiveDefinition (_, _, _, attributes) ->
+ attributes
+
(** @raise Failure "not enough prods" *)
val strip_prods: int -> Cic.term -> Cic.term
+(** {2 Cic selectors} *)
+
+val params_of_obj: Cic.obj -> UriManager.uri list
+val attributes_of_obj: Cic.obj -> Cic.attribute list
+
(** {2 Contexts}
* A context is a Cic term in which Cic.Implicit terms annotated with `Hole
* appears *)
let deannotate_obj =
let module C = Cic in
function
- C.AConstant (_, _, id, bo, ty, params) ->
+ C.AConstant (_, _, id, bo, ty, params, attrs) ->
C.Constant (id,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty, params)
- | C.AVariable (_, name, bo, ty, params) ->
+ deannotate_term ty, params, attrs)
+ | C.AVariable (_, name, bo, ty, params, attrs) ->
C.Variable (name,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
- deannotate_term ty, params)
- | C.ACurrentProof (_, _, name, conjs, bo, ty, params) ->
+ deannotate_term ty, params, attrs)
+ | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
C.CurrentProof (
name,
List.map
in
(id,context,deannotate_term con)
) conjs,
- deannotate_term bo,deannotate_term ty,params
+ deannotate_term bo,deannotate_term ty, params, attrs
)
- | C.AInductiveDefinition (_, tys, params, parno) ->
+ | C.AInductiveDefinition (_, tys, params, parno, attrs) ->
C.InductiveDefinition (List.map deannotate_inductiveType tys,
- params, parno)
+ params, parno, attrs)
;;
projects / helm.git / commitdiff