From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 15 Jun 2005 16:54:46 +0000 (+0000)
Subject: DTD for attributes revised.
X-Git-Tag: INDEXING_NO_PROOFS~140
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb5c964ba2d0fbea5988efec610ba49fca84376d;p=helm.git

DTD for attributes revised.
New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>
---

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index 3051fb81f..2c4ded396 100644
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -66,6 +66,9 @@ type stack_entry =
   | Inductive_type of string * string * bool * Cic.annterm *
       (string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
   | Meta_subst of Cic.annterm option
+  | Obj_class of Cic.object_class
+  | Obj_field of string (* field name *)
+  | Obj_generated
   | Tag of string * (string * string) list  (* tag name, attributes *)
       (* ZACK TODO add file position to tag stack entry so that when attribute
        * errors occur, the position of their _start_tag_ could be printed
@@ -98,6 +101,9 @@ let string_of_stack ctxt =
       | Inductive_type (id, name, _, _, _) ->
           sprintf "Inductive_type %s (id=%s)" name id
       | Meta_subst _ -> "Meta_subst"
+      | Obj_class _ -> "Obj_class"
+      | Obj_field name -> "Obj_field " ^ name
+      | Obj_generated -> "Obj_generated"
       | Tag (tag, _) -> "Tag " ^ tag)
       ctxt.stack)) ^ "]"
 
@@ -168,6 +174,18 @@ let pop_cics ctxt =
   ctxt.stack <- new_stack;
   values
 
+let pop_class_modifiers ctxt =
+  let rec aux acc stack =
+    match stack with
+    | (Cic_term (Cic.ASort _) as m) :: tl
+    | (Obj_field _ as m) :: tl ->
+        aux (m :: acc) tl
+    | tl -> acc, tl
+  in
+  let values, new_stack = aux [] ctxt.stack in
+  ctxt.stack <- new_stack;
+  values
+
 let pop_meta_substs ctxt =
   let rec aux acc stack =
     match stack with
@@ -279,9 +297,9 @@ let uri_list_of_string =
 let sort_of_string ctxt = function
   | "Prop" -> Cic.Prop
   | "Set"  -> Cic.Set
-  | "Type" ->
-(*      CicUniv.restart_numbering (); |+ useful only to test parser +| *)
-      Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+  | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+(*   | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
+  | "CProp" -> Cic.CProp
   | _ -> parse_error ctxt "sort expected"
 
 let patch_subst ctxt subst = function
@@ -598,29 +616,44 @@ let end_element ctxt tag =
         (* replace <instantiate> *)
       set_top ctxt (Cic_term (patch_subst ctxt subst term))
   | "attributes" ->
-      let (_, attrs) = pop_tag ctxt in
-      let rec mk_obj_attributes acc = function
-        | [] -> acc
-        | ("generated", "true") :: tl ->
-            mk_obj_attributes (`Generated :: acc) tl
-        | ("class", "coercion") :: tl ->
-            mk_obj_attributes (`Class `Coercion :: acc) tl
-        | ("class", "record") :: tl ->
-            mk_obj_attributes (`Class (`Record []) :: acc) tl
-        | ("class", "projection") :: tl ->
-            mk_obj_attributes (`Class `Projection :: acc) tl
-        | ("class", "elimProp") :: tl ->
-            mk_obj_attributes (`Class (`Elim Cic.Prop) :: acc) tl
-        | ("class", "elimCProp") :: tl ->
-            mk_obj_attributes (`Class (`Elim Cic.CProp) :: acc) tl
-        | ("class", "elimSet") :: tl ->
-            mk_obj_attributes (`Class (`Elim Cic.Set) :: acc) tl
-        | ("class", "elimType") :: tl ->
-            let univ = CicUniv.fresh ~uri:ctxt.uri () in
-            mk_obj_attributes (`Class (`Elim (Cic.Type univ)) :: acc) tl
-        | _ -> attribute_error ()
+      let rec aux acc = function  (* retrieve object attributes *)
+        | Obj_class c :: tl -> aux (`Class c :: acc) tl
+        | Obj_generated :: tl -> aux (`Generated :: acc) tl
+        | tl -> acc, tl
       in
-      push ctxt (Cic_attributes (mk_obj_attributes [] attrs))
+      let obj_attrs, new_stack = aux [] ctxt.stack in
+      ctxt.stack <- new_stack;
+      set_top ctxt (Cic_attributes obj_attrs)
+  | "generated" -> set_top ctxt Obj_generated
+  | "field" ->
+      push ctxt
+        (match pop_tag_attrs ctxt with
+        | ["name", name] -> Obj_field name
+        | _ -> attribute_error ())
+  | "class" ->
+      let class_modifiers = pop_class_modifiers ctxt in
+      push ctxt
+        (match pop_tag_attrs ctxt with
+        | ["value", "coercion"] -> Obj_class `Coercion
+        | ["value", "elim"] ->
+            (match class_modifiers with
+            | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
+            | _ ->
+                parse_error
+                  "unexpected extra content for \"elim\" object class")
+        | ["value", "record"] ->
+            let fields =
+              List.map
+                (function
+                  | Obj_field name -> name
+                  | _ ->
+                      parse_error
+                        "unexpected extra content for \"record\" object class")
+                class_modifiers
+            in
+            Obj_class (`Record fields)
+        | ["value", "projection"] -> Obj_class `Projection
+        | _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))