added records pp, ast and fixed a bug in match with only one branch

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index c82f0fb8add1cfa8366d68a4b2740b89f8e25171..f0f9d934f580fcf4f5e58720453b38ecba70f7d0 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -230,7 +230,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                       append_tail ~tail (Box.Object([],rhs))]) in
         let plbox =
           match pl with
-            [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [r] -> (make_rule ~tail:("]" :: tail) "[" r)
           | r::tl -> 
               Box.V([],
                 (make_rule ~tail:[] "[" r) ::

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 7fabafda3e5f1707172048a54e7e327d7a3984e7..9023b48692c85aa578f8dcd118f93bf030bc0548 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -133,6 +133,8 @@ type 'term command =
        *)
   | Coercion of loc * 'term
   | Alias of loc * alias_spec
+      (** parameters, name, type, fields *) 
+  | Record of loc * (string * 'term) list * string * 'term * (string * 'term) list
 
 type ('term, 'ident) tactical =
   | Tactic of loc * ('term, 'ident) tactic

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 822618eb4a18d0c70616086f287ccb21d4f438fb..a5c0478acc65b9e2b24e6ef3f795285b5c05be63 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -42,7 +42,7 @@ let pp_reduction_kind = function
   | `Simpl -> "simplify"
   | `Whd -> "whd"
   | `Normalize -> "normalize"
-
+  
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term
   | Apply (_, term) -> "apply " ^ pp_term_ast term
@@ -149,19 +149,24 @@ let pp_alias = function
   | Number_alias (instance,desc) ->
       sprintf "alias num (instance %d) = \"%s\"" instance desc
   
+let pp_params = function
+  | [] -> ""
+  | params ->
+      " " ^
+      String.concat " "
+        (List.map
+          (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
+          params)
+      
+let pp_fields fields =
+  (if fields <> [] then "\n" else "") ^ 
+  String.concat ";\n" 
+    (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields)
+        
 let pp_command = function
   | Qed _ -> "qed"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
   | Inductive (_, params, types) ->
-      let pp_params = function
-        | [] -> ""
-        | params ->
-            " " ^
-            String.concat " "
-              (List.map
-                (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
-                params)
-      in
       let pp_constructors constructors =
         String.concat "\n"
           (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
@@ -190,6 +195,10 @@ let pp_command = function
         | Some body -> "\\def " ^ pp_term_ast body)
   | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
   | Alias (_,s) -> pp_alias s
+  | Record (_,params,name,ty,fields) ->
+      "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
+      pp_fields fields ^ "}"
+      
 
 let rec pp_tactical = function
   | Tactic (_, tac) -> pp_tactic tac