From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:19:02 +0000 (+0000) Subject: added attribute support (not yet in the parser) X-Git-Tag: V_0_1_0~113 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f47b833df94d134090a65653077744290438a875;p=helm.git added attribute support (not yet in the parser) --- diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 4f7051688..23bb7661b 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -41,23 +41,32 @@ type 'term explicit_named_substitution = (UriManager.uri * 'term) list 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. *) @@ -88,13 +97,13 @@ and term = | 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 *) @@ -153,16 +162,17 @@ and annterm = 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 *) @@ -193,3 +203,11 @@ and annhypothesis = 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 + diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 15bc2b935..b641c649e 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -40,6 +40,12 @@ 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 = @@ -180,6 +186,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody 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" -> @@ -190,7 +197,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody (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 @@ -202,7 +209,8 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody 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" -> @@ -212,7 +220,8 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody 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) @@ -223,7 +232,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody 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") @@ -242,7 +251,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody (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) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 5e0d6d4a9..f2ea4171b 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -253,3 +253,17 @@ let rec strip_prods n = function | 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 + diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index cfd2d813a..4deec7241 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -46,6 +46,11 @@ val unpack: Cic.term -> Cic.term list (** @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 *) diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index 289fe7db4..21e591d4e 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -90,15 +90,15 @@ let deannotate_inductiveType (_, name, isinductive, arity, cons) = 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 @@ -116,9 +116,9 @@ let deannotate_obj = 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) ;;