The `Record class now records also the name of the fields

(used to generate the projections)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index d9297bce5d517c20182a8648c220995597171a08..e5bb82786a3b742989a72746aa05f7971491f44c 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -235,8 +235,8 @@ let generate_elimination_principles uri status =
  List.fold_left (fun status sort -> elim sort status) status
   [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
 
-let generate_projections uri status =
- let projections = CicRecord.projections_of uri in
+let generate_projections uri fields status =
+ let projections = CicRecord.projections_of uri fields in
   List.fold_left
    (fun status (uri, name, bo) -> 
      try 
@@ -328,12 +328,17 @@ let eval_command status cmd =
         let status = MatitaSync.add_obj uri obj status in
          match obj with
             Cic.Constant _ -> status
-          | Cic.InductiveDefinition (_,_,_,attrs)
-              when List.mem (`Class `Record) attrs ->
+          | Cic.InductiveDefinition (_,_,_,attrs) ->
              let status = generate_elimination_principles uri status in
-              generate_projections uri status
-          | Cic.InductiveDefinition (_,_,_,_) ->
-             generate_elimination_principles uri status
+             let rec get_record_attrs =
+              function
+                 [] -> None
+               | (`Class (`Record fields))::_ -> Some fields
+               | _::tl -> get_record_attrs tl
+             in
+              (match get_record_attrs attrs with
+                  None -> status (* not a record *)
+                | Some fields -> generate_projections uri fields status)
           | Cic.CurrentProof _
           | Cic.Variable _ -> assert false
 

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 23bb7661b0bb4d8b96340c032f73e67970760656..ba51157ff9f4aa24464733c0820f0b518e4d7119 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -57,7 +57,8 @@ 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 *)
+  | `Record of string list (** inductive type that encodes a record;
+                               the arguments are the record fields *)
   | `Projection     (** record projection *)
   ]
 

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index f9f14df106b971a457c2f10fbed7841bf6ab2c46..3051fb81fa3b0a0c18b15f7173ba0f44d23dc0e1 100644 (file)
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -606,7 +606,7 @@ let end_element ctxt tag =
         | ("class", "coercion") :: tl ->
             mk_obj_attributes (`Class `Coercion :: acc) tl
         | ("class", "record") :: tl ->
-            mk_obj_attributes (`Class `Record :: acc) tl
+            mk_obj_attributes (`Class (`Record []) :: acc) tl
         | ("class", "projection") :: tl ->
             mk_obj_attributes (`Class `Projection :: acc) tl
         | ("class", "elimProp") :: tl ->

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 4a12727c7df207a6b381db4e4b8ae6b680a1c27b..2f9bb97a5d799dacfc8c3251c457d3001c19f4c8 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -400,14 +400,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
       (*here the explicit_named_substituion is assumed to be of length 0 *)
       let mutind = Cic.MutInd (uri,0,[]) in
       if params = [] then mutind
-      else Cic.Appl (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
+      else
+       Cic.Appl
+        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
      let con =
       List.fold_left
        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
        concl fields' in
      let con' = add_params con in
      let tyl = [name,true,ty',["mk_" ^ name,con']] in
-      Cic.InductiveDefinition (tyl,[],List.length params,[`Class `Record])
+     let field_names = List.map fst fields in
+      Cic.InductiveDefinition
+       (tyl,[],List.length params,[`Class (`Record field_names)])
   | TacticAst.Theorem (_,name,ty,bo) ->
      let ty' = interpretate_term [] env None false ty in
      match bo with

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml
index d8dd2dc47b142cc1b7cc9df8469947c1a78080ce..a251bad87c5b5530b8253f0c8f221e51d5e3b6d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicRecord.ml
+++ b/helm/ocaml/cic_proof_checking/cicRecord.ml
@@ -40,7 +40,7 @@ let generate_one_proj uri params paramsno fields t i =
        Cic.MutCase (uri,0,outtype, Cic.Rel 1, 
         [mk_lambdas fields (Cic.Rel i)]))))
 
-let projections_of uri =
+let projections_of uri field_names =
  let buri = UriManager.buri_of_uri uri in
  let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
   match obj with
@@ -60,32 +60,32 @@ let projections_of uri =
       let fields =
        let rec aux =
         function
-           Cic.MutInd _
-         | Cic.Appl _ -> []
-         | Cic.Prod (Cic.Name name,s,t) -> (name,s)::aux t
-         | _ -> assert false
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl)
+         | _,_ -> assert false
        in
-        aux (CicSubstitution.lift 1 ty)
+        aux ((CicSubstitution.lift 1 ty),field_names)
       in
        let rec aux i =
         function
-           Cic.MutInd _
-         | Cic.Appl _ -> []
-         | Cic.Prod (Cic.Name name,s,t) ->
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl ->
             (match generate_one_proj uri leftparams paramsno fields s i with
-               Some p ->
-                let puri =
-                 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
-                in
-                 (puri,name,p) ::
-                   aux (i - 1)
-                    (CicSubstitution.subst
-                      (Cic.Appl
-                        (Cic.Const (puri,[]) ::
-                          CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
-                      ) t)
-             | None -> assert false)
-         | _ -> assert false
+                Some p ->
+                 let puri =
+                  UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+                 in
+                  (puri,name,p) ::
+                    aux (i - 1)
+                     (CicSubstitution.subst
+                       (Cic.Appl
+                         (Cic.Const (puri,[]) ::
+                           CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
+                       ) t, tl)
+              | None -> assert false)
+         | _,_ -> assert false
        in
-        aux (List.length fields) (CicSubstitution.lift 2 ty)
+        aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
    | _ -> assert false

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli
index 04ee188b52364a4be11df76c9eff5e1405021fe8..b966f317ca3a951a1a4125a76a431f4bb7c18527 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicRecord.mli
+++ b/helm/ocaml/cic_proof_checking/cicRecord.mli
@@ -24,4 +24,5 @@
  *)
 
 (** projections_of [uri] returns uri * name * term *)    
-val projections_of: UriManager.uri -> (UriManager.uri * string * Cic.term) list
+val projections_of:
+ UriManager.uri -> string list -> (UriManager.uri * string * Cic.term) list

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 1facd4fd9c59cb7c2d65af71495df96192f43ed4..8bf8d5f3b389aac676e64d9a38dbc02991b224d6 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -266,7 +266,7 @@ let xml_of_attrs attributes =
     | `Elim Cic.CProp -> "elimCProp"
     | `Elim Cic.Set -> "elimSet"
     | `Elim (Cic.Type _) -> "elimType"
-    | `Record -> "record"
+    | `Record _ -> "record"
     | `Projection -> "projection"
   in
   let xml_attr_of = function