diff src/elab_print.sml @ 11:e97c6d335869

Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents 14b533dbe6cc
children d89477f07c1e
line wrap: on
line diff
--- a/src/elab_print.sml	Fri Mar 28 13:59:03 2008 -0400
+++ b/src/elab_print.sml	Fri Mar 28 15:20:46 2008 -0400
@@ -36,6 +36,8 @@
 
 structure E = ElabEnv
 
+val debug = ref false
+
 fun p_kind' par (k, _) =
     case k of
         KType => string "Type"
@@ -85,8 +87,16 @@
       | TRecord c => box [string "$",
                           p_con' true env c]
 
-      | CRel n => string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
-      | CNamed n => string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
+      | CRel n =>
+        if !debug then
+            string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
+        else
+            string (#1 (E.lookupCRel env n))
+      | CNamed n =>
+        if !debug then
+            string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
+        else
+            string (#1 (E.lookupCNamed env n))
 
       | CApp (c1, c2) => parenIf par (box [p_con env c1,
                                            space,
@@ -130,8 +140,16 @@
 
 fun p_exp' par env (e, _) =
     case e of
-        ERel n => string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
-      | ENamed n => string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
+        ERel n =>
+        if !debug then
+            string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
+        else
+            string (#1 (E.lookupERel env n))
+      | ENamed n =>
+        if !debug then
+            string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
+        else
+            string (#1 (E.lookupENamed env n))
       | EApp (e1, e2) => parenIf par (box [p_exp env e1,
                                            space,
                                            p_exp' true env e2])
@@ -169,32 +187,48 @@
 
 fun p_decl env ((d, _) : decl) =
     case d of
-        DCon (x, n, k, c) => box [string "con",
-                                  space,
-                                  string x,
-                                  string "__",
-                                  string (Int.toString n),
-                                  space,
-                                  string "::",
-                                  space,
-                                  p_kind k,
-                                  space,
-                                  string "=",
-                                  space,
-                                  p_con env c]
-      | DVal (x, n, t, e) => box [string "val",
-                                  space,
-                                  string x,
-                                  string "__",
-                                  string (Int.toString n),
-                                  space,
-                                  string ":",
-                                  space,
-                                  p_con env t,
-                                  space,
-                                  string "=",
-                                  space,
-                                  p_exp env e]
+        DCon (x, n, k, c) =>
+        let
+            val xp = if !debug then
+                         box [string x,
+                              string "__",
+                              string (Int.toString n)]
+                     else
+                         string x
+        in
+            box [string "con",
+                 space,
+                 xp,
+                 space,
+                 string "::",
+                 space,
+                 p_kind k,
+                 space,
+                 string "=",
+                 space,
+                 p_con env c]
+        end
+      | DVal (x, n, t, e) =>
+        let
+            val xp = if !debug then
+                         box [string x,
+                              string "__",
+                              string (Int.toString n)]
+                     else
+                         string x        
+        in
+            box [string "val",
+                 space,
+                 xp,
+                 space,
+                 string ":",
+                 space,
+                 p_con env t,
+                 space,
+                 string "=",
+                 space,
+                 p_exp env e]
+        end
 
 fun p_file env file =
     let