Some con reducing

13 files changed, 285 insertions, 18 deletions

diff --git a/src/compiler.sig b/src/compiler.sig
index 6a4fa466..cafb3d20 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -32,9 +32,11 @@ signature COMPILER = sig
     val parse : string -> Source.file option
     val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option
     val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
+    val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
 
     val testParse : string -> unit
     val testElaborate : string -> unit
     val testCorify : string -> unit
+    val testReduce : string -> unit
 
 end
diff --git a/src/compiler.sml b/src/compiler.sml
index 51fef453..28b92ac8 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -72,6 +72,11 @@ fun corify eenv cenv filename =
         NONE => NONE
       | SOME (_, file) => SOME (Corify.corify file)
 
+fun reduce eenv cenv filename =
+    case corify eenv cenv filename of
+        NONE => NONE
+      | SOME file => SOME (Reduce.reduce file)
+
 fun testParse filename =
     case parse filename of
         NONE => print "Failed\n"
@@ -97,4 +102,13 @@ fun testCorify filename =
     handle CoreEnv.UnboundNamed n =>
            print ("Unbound named " ^ Int.toString n ^ "\n")
 
+fun testReduce filename =
+    (case reduce ElabEnv.basis CoreEnv.basis filename of
+         NONE => print "Failed\n"
+       | SOME file =>
+         (Print.print (CorePrint.p_file CoreEnv.basis file);
+          print "\n"))
+    handle CoreEnv.UnboundNamed n =>
+           print ("Unbound named " ^ Int.toString n ^ "\n")
+
 end
diff --git a/src/core_env.sig b/src/core_env.sig
index 88cb253b..1766b3d1 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -27,6 +27,8 @@
 
 signature CORE_ENV = sig
 
+    val liftConInCon : int -> Core.con -> Core.con
+
     type env
 
     val empty : env
@@ -44,8 +46,8 @@ signature CORE_ENV = sig
     val pushERel : env -> string -> Core.con -> env
     val lookupERel : env -> int -> string * Core.con
 
-    val pushENamed : env -> string -> int -> Core.con -> env
-    val lookupENamed : env -> int -> string * Core.con
+    val pushENamed : env -> string -> int -> Core.con -> Core.exp option -> env
+    val lookupENamed : env -> int -> string * Core.con * Core.exp option
 
     val declBinds : env -> Core.decl -> env
                                                  
diff --git a/src/core_env.sml b/src/core_env.sml
index e123c9a9..904c71f5 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -62,7 +62,7 @@ type env = {
      namedC : (string * kind * con option) IM.map,
 
      relE : (string * con) list,
-     namedE : (string * con) IM.map
+     namedE : (string * con * exp option) IM.map
 }
 
 val empty = {
@@ -78,7 +78,7 @@ fun pushCRel (env : env) x k =
      namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
 
      relE = map (fn (x, c) => (x, lift c)) (#relE env),
-     namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
+     namedE = IM.map (fn (x, c, eo) => (x, lift c, eo)) (#namedE env)}
 
 fun lookupCRel (env : env) n =
     (List.nth (#relC env, n))
@@ -107,12 +107,12 @@ fun lookupERel (env : env) n =
     (List.nth (#relE env, n))
     handle Subscript => raise UnboundRel n
 
-fun pushENamed (env : env) x n t =
+fun pushENamed (env : env) x n t eo =
     {relC = #relC env,
      namedC = #namedC env,
 
      relE = #relE env,
-     namedE = IM.insert (#namedE env, n, (x, t))}
+     namedE = IM.insert (#namedE env, n, (x, t, eo))}
 
 fun lookupENamed (env : env) n =
     case IM.find (#namedE env, n) of
@@ -122,7 +122,7 @@ fun lookupENamed (env : env) n =
 fun declBinds env (d, _) =
     case d of
         DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
-      | DVal (x, n, t, _) => pushENamed env x n t
+      | DVal (x, n, t, e) => pushENamed env x n t (SOME e)
 
 val ktype = (KType, ErrorMsg.dummySpan)
 
diff --git a/src/core_print.sml b/src/core_print.sml
index 1e254862..c035ceef 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -69,7 +69,7 @@ fun p_con' par env (c, _) =
                                              p_con (E.pushCRel env x k) c])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
-                                                         box [p_con env x,
+                                                         box [p_name env x,
                                                               space,
                                                               string ":",
                                                               space,
@@ -134,6 +134,11 @@ fun p_con' par env (c, _) =
         
 and p_con env = p_con' false env
 
+and p_name env (all as (c, _)) =
+    case c of
+        CName s => string s
+      | _ => p_con env all
+
 fun p_exp' par env (e, _) =
     case e of
         EPrim p => Prim.p_t p
diff --git a/src/core_util.sig b/src/core_util.sig
index a40e0664..07350798 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -37,7 +37,7 @@ end
 structure Con : sig
     datatype binder =
              Rel of string * Core.kind
-           | Named of string * Core.kind
+           | Named of string * int * Core.kind * Core.con option
 
     val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
@@ -62,9 +62,9 @@ end
 structure Exp : sig
     datatype binder =
              RelC of string * Core.kind
-           | NamedC of string * Core.kind
+           | NamedC of string * int * Core.kind * Core.con option
            | RelE of string * Core.con
-           | NamedE of string * Core.con
+           | NamedE of string * int * Core.con * Core.exp option
 
     val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
                     con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
@@ -85,4 +85,33 @@ structure Exp : sig
                   exp : Core.exp' -> bool} -> Core.exp -> bool
 end
 
+structure Decl : sig
+    datatype binder = datatype Exp.binder
+
+    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+                    con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
+                    exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * binder -> 'context}
+                   -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB
+end
+
+structure File : sig
+    datatype binder = datatype Exp.binder
+
+    val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+                    con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
+                    exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
+                    decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * binder -> 'context}
+                   -> ('context, Core.file, 'state, 'abort) Search.mapfolderB
+
+    val mapB : {kind : Core.kind' -> Core.kind',
+                con : 'context -> Core.con' -> Core.con',
+                exp : 'context -> Core.exp' -> Core.exp',
+                decl : 'context -> Core.decl' -> Core.decl',
+                bind : 'context * binder -> 'context}
+               -> 'context -> Core.file -> Core.file
+end
+
 end
diff --git a/src/core_util.sml b/src/core_util.sml
index 0f7df403..c3e8250b 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -79,7 +79,7 @@ structure Con = struct
 
 datatype binder =
          Rel of string * kind
-       | Named of string * kind
+       | Named of string * int * kind * con option
 
 fun mapfoldB {kind = fk, con = fc, bind} =
     let
@@ -162,7 +162,7 @@ fun mapB {kind, con, bind} ctx c =
                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
                    bind = bind} ctx c () of
         S.Continue (c, ()) => c
-      | S.Return _ => raise Fail "Con.mapB: Impossible"
+      | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
 
 fun exists {kind, con} k =
     case mapfold {kind = fn k => fn () =>
@@ -184,9 +184,9 @@ structure Exp = struct
 
 datatype binder =
          RelC of string * kind
-       | NamedC of string * kind
+       | NamedC of string * int * kind * con option
        | RelE of string * con
-       | NamedE of string * con
+       | NamedE of string * int * con * exp option
 
 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
     let
@@ -294,4 +294,87 @@ fun exists {kind, con, exp} k =
 
 end
 
+structure Decl = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
+    let
+        val mfk = Kind.mapfold fk
+
+        fun bind' (ctx, b) =
+            let
+                val b' = case b of
+                             Con.Rel x => RelC x
+                           | Con.Named x => NamedC x
+            in
+                bind (ctx, b')
+            end
+        val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+        val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
+
+        fun mfd ctx d acc =
+            S.bindP (mfd' ctx d acc, fd ctx)
+
+        and mfd' ctx (dAll as (d, loc)) =
+            case d of
+                DCon (x, n, k, c) =>
+                S.bind2 (mfk k,
+                      fn k' =>
+                         S.map2 (mfc ctx c,
+                              fn c' =>
+                                 (DCon (x, n, k', c'), loc)))
+              | DVal (x, n, t, e) =>
+                S.bind2 (mfc ctx t,
+                      fn t' =>
+                         S.map2 (mfe ctx e,
+                              fn e' =>
+                                 (DVal (x, n, t', e'), loc)))
+    in
+        mfd
+    end    
+
+end
+
+structure File = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB (all as {bind, ...}) =
+    let
+        val mfd = Decl.mapfoldB all
+
+        fun mff ctx ds =
+            case ds of
+                nil => S.return2 nil
+              | d :: ds' =>
+                S.bind2 (mfd ctx d,
+                         fn d' =>
+                            let
+                                val b =
+                                    case #1 d' of
+                                        DCon (x, n, k, c) => NamedC (x, n, k, SOME c)
+                                      | DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
+                                val ctx' = bind (ctx, b)
+                            in
+                                S.map2 (mff ctx' ds',
+                                     fn ds' =>
+                                        d' :: ds')
+                            end)
+    in
+        mff
+    end
+
+fun mapB {kind, con, exp, decl, bind} ctx ds =
+    case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+                   con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+                   exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+                   decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
+                   bind = bind} ctx ds () of
+        S.Continue (ds, ()) => ds
+      | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
+
+end
+
 end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index fcf5e747..6f1c0148 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -78,7 +78,7 @@ fun p_con' par env (c, _) =
                                                 p_con (E.pushCRel env x k) c])
       | TRecord (CRecord (_, xcs), _) => box [string "{",
                                               p_list (fn (x, c) =>
-                                                         box [p_con env x,
+                                                         box [p_name env x,
                                                               space,
                                                               string ":",
                                                               space,
@@ -149,6 +149,11 @@ fun p_con' par env (c, _) =
         
 and p_con env = p_con' false env
 
+and p_name env (all as (c, _)) =
+    case c of
+        CName s => string s
+      | _ => p_con env all
+
 fun p_exp' par env (e, _) =
     case e of
         EPrim p => Prim.p_t p
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 433b19f2..46824ab9 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -26,5 +26,5 @@
  *)
 
 val () = case CommandLine.arguments () of
-             [filename] => Compiler.testElaborate filename
+             [filename] => Compiler.testReduce filename
            | _ => print "Bad arguments"
diff --git a/src/reduce.sig b/src/reduce.sig
new file mode 100644
index 00000000..0a28a59a
--- /dev/null
+++ b/src/reduce.sig
@@ -0,0 +1,34 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Simplify a Core program algebraically *)
+
+signature REDUCE = sig
+
+    val reduce : Core.file -> Core.file
+    
+end
diff --git a/src/reduce.sml b/src/reduce.sml
new file mode 100644
index 00000000..a558778c
--- /dev/null
+++ b/src/reduce.sml
@@ -0,0 +1,85 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ *   this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Simplify a Core program algebraically *)
+
+structure Reduce :> REDUCE = struct
+
+open Core
+
+structure E = CoreEnv
+structure U = CoreUtil
+
+val liftConInCon = E.liftConInCon
+
+val subConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn (xn, rep) => fn c =>
+                                  case c of
+                                      CRel xn' =>
+                                      if xn = xn' then
+                                          #1 rep
+                                      else
+                                          c
+                                    | _ => c,
+                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+                        | (ctx, _) => ctx}
+
+fun bindC (env, b) =
+    case b of
+        U.Con.Rel (x, k) => E.pushCRel env x k
+      | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co
+
+fun bind (env, b) =
+    case b of
+        U.Decl.RelC (x, k) => E.pushCRel env x k
+      | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
+      | U.Decl.RelE (x, t) => E.pushERel env x t
+      | U.Decl.NamedE (x, n, t, eo) => E.pushENamed env x n t eo
+
+fun kind k = k
+
+fun con env c =
+    case c of
+        CApp ((CAbs (_, _, c1), loc), c2) =>
+        #1 (reduceCon env (subConInCon (0, c2) c1))
+      | CNamed n =>
+        (case E.lookupCNamed env n of
+             (_, _, SOME c') => #1 c'
+           | _ => c)
+      | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2)
+      | _ => c
+
+and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
+
+fun exp env e = e
+
+fun decl env d = d
+
+val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis
+
+end
diff --git a/src/source_print.sml b/src/source_print.sml
index 90524241..9c3b870b 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -79,7 +79,7 @@ fun p_con' par (c, _) =
                                                 p_con c])
       | TRecord (CRecord xcs, _) => box [string "{",
                                          p_list (fn (x, c) =>
-                                                    box [p_con x,
+                                                    box [p_name x,
                                                          space,
                                                          string ":",
                                                          space,
@@ -127,6 +127,11 @@ fun p_con' par (c, _) =
         
 and p_con c = p_con' false c
 
+and p_name (all as (c, _)) =
+    case c of
+        CName s => string s
+      | _ => p_con all
+
 fun p_exp' par (e, _) =
     case e of
         EAnnot (e, t) => box [string "(",
diff --git a/src/sources b/src/sources
index 8c72870f..71ad71de 100644
--- a/src/sources
+++ b/src/sources
@@ -49,5 +49,8 @@ core_print.sml
 corify.sig
 corify.sml
 
+reduce.sig
+reduce.sml
+
 compiler.sig
 compiler.sml