diff src/expl_print.sml @ 162:06a98129b23f

Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 7420fa18d657
children 80192edca30d
line wrap: on
line diff
--- a/src/expl_print.sml	Thu Jul 24 16:51:24 2008 -0400
+++ b/src/expl_print.sml	Tue Jul 29 12:30:04 2008 -0400
@@ -274,6 +274,22 @@
     else
         string x
 
+fun p_datatype env (x, n, cons) =
+    let
+        val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE
+    in
+        box [string "datatype",
+             space,
+             string x,
+             space,
+             string "=",
+             space,
+             p_list_sep (box [space, string "|", space])
+                        (fn (x, _, NONE) => string x
+                          | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t])
+                        cons]
+    end
+
 fun p_sgn_item env (sgi, _) =
     case sgi of
         SgiConAbs (x, n, k) => box [string "con",
@@ -294,6 +310,22 @@
                                     string "=",
                                     space,
                                     p_con env c]
+      | SgiDatatype x => p_datatype env x
+      | SgiDatatypeImp (x, _, m1, ms, x', _) =>
+        let
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+        in
+            box [string "datatype",
+                 space,
+                 string x,
+                 space,
+                 string "=",
+                 space,
+                 string "datatype",
+                 space,
+                 p_list_sep (string ".") string (m1x :: ms @ [x'])]
+        end
       | SgiVal (x, n, c) => box [string "val",
                                  space,
                                  p_named x n,
@@ -392,6 +424,22 @@
                                   string "=",
                                   space,
                                   p_con env c]
+      | DDatatype x => p_datatype env x
+      | DDatatypeImp (x, _, m1, ms, x', _) =>
+        let
+            val m1x = #1 (E.lookupStrNamed env m1)
+                handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
+        in
+            box [string "datatype",
+                 space,
+                 string x,
+                 space,
+                 string "=",
+                 space,
+                 string "datatype",
+                 space,
+                 p_list_sep (string ".") string (m1x :: ms @ [x'])]
+        end
       | DVal vi => box [string "val",
                         space,
                         p_vali env vi]