X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=8cf705d0a1c098ca87375397799d1997a147b400;hb=dcdbb979433a61e2ef2842d96604098728824416;hp=55516bf34aebd02241badb49501372493227f511;hpb=d17a38ddca548c784e9efa7c55e87c80203b024d;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 55516bf34..8cf705d0a 100644
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -68,8 +68,10 @@ type pattern  = C.annterm
 type body     = C.annterm option
 type types    = C.anninductiveType list
 type lpsno    = int
+type fields   = (string * bool * int) list
 
 type step = Note of note 
+          | Record of types * lpsno * fields * note
           | Inductive of types * lpsno * note
 	  | Statement of flavour * name * what * body * note
           | Qed of note
@@ -134,7 +136,7 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_inductive types lpsno =
+let mk_pre_inductive types lpsno =
    let map1 (lps1, cons) (name, arity) = 
       let lps2, arity = strip_lps lpsno arity in
       merge_lps lps1 lps2, (name, arity) :: cons
@@ -146,10 +148,29 @@ let mk_inductive types lpsno =
    in
    let map3 (name, xw) = arel_of_name name, xw in
    let rev_lps, rev_types = List.fold_left map2 ([], []) types in
-   let lpars, types = List.rev_map map3 rev_lps, List.rev rev_types in
+   List.rev_map map3 rev_lps, List.rev rev_types
+
+let mk_inductive types lpsno =
+   let lpars, types = mk_pre_inductive types lpsno in
    let obj = N.Inductive (lpars, types) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
+let mk_record types lpsno fields =
+   match mk_pre_inductive types lpsno with
+      | lpars, [name, _, ty, [_, cty]] -> 
+         let map (fields, cty) (name, coercion, arity) =
+	    match cty with
+	       | C.AProd (_, _, w, t) ->
+	          (name, w, coercion, arity) :: fields, t
+	       | _                    ->
+	          assert false
+	 in
+	 let rev_fields, _ = List.fold_left map ([], cty) fields in 
+	 let fields = List.rev rev_fields in
+	 let obj = N.Record (lpars, name, ty, fields) in
+         G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+      | _ -> assert false
+
 let mk_statement flavour name t v =
    let name = match name with Some name -> name | None -> assert false in
    let obj = N.Theorem (flavour, name, t, v) in
@@ -247,7 +268,8 @@ let mk_vb = G.Shift floc
 let rec render_step sep a = function
    | Note s                    -> mk_notenote s a
    | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a 
-   | Inductive (lps, ts, s)    -> mk_inductive lps ts :: mk_thnote s a
+   | Inductive (ts, lps, s)    -> mk_inductive ts lps :: mk_thnote s a
+   | Record (ts, lps, fs, s)   -> mk_record ts lps fs :: mk_thnote s a
    | Qed s                     -> mk_qed :: mk_tacnote s a
    | Exact (t, s)              -> mk_exact t sep :: mk_tacnote s a   
    | Id s                      -> mk_id sep :: mk_tacnote s a
@@ -310,6 +332,7 @@ let count = I.count_nodes ~meta:false
 
 let rec count_node a = function
    | Note _
+   | Record _
    | Inductive _
    | Statement _
    | Qed _   
@@ -336,6 +359,7 @@ let rec note_of_step = function
    | Note s
    | Statement (_, _, _, _, s)
    | Inductive (_, _, s)
+   | Record (_, _, _, s)
    | Qed s
    | Exact (_, s)
    | Id s