Standard library moduls Incl and Mem; tweaks to Especialize and Unpoly

6 files changed, 156 insertions, 18 deletions

diff --git a/lib/ur/incl.ur b/lib/ur/incl.ur
new file mode 100644
index 00000000..d0f4b521
--- /dev/null
+++ b/lib/ur/incl.ur
@@ -0,0 +1,40 @@
+con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) =>
+    [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'),
+                  Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2}
+
+con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) =>
+                    tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp
+
+fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] =
+    fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) =>
+       f [r2] ! (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x,
+                                  Hide = fn [f :: ({K} -> Type)] x => x})
+       
+fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) =
+    i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') =>
+                i'.Expose [fn r => $r] r --- r')
+
+fun inv1 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
+         [f :: Name -> K -> {K} -> Type]
+         (i : incl ([nm = t] ++ r) r')
+         (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) =
+    i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
+                      i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !))
+
+fun inv2 [K] [nm :: Name] [t ::: K] [r :: {K}] [r' :: {K}] [[nm] ~ r]
+         (i : incl ([nm = t] ++ r) r') =
+    i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') =>
+                      fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) =>
+                         f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] =>
+                                                   {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x,
+                                                    Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x}))
+
+fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
+    (f : nm :: Name -> v :: K -> r' :: {K}
+         -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
+    (i : tf []) (fl : folder r) =
+    @Top.fold [fn r' => incl r' r -> tf r']
+     (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i =>
+         f [nm] [v] [r'] ! i (acc (inv2 [nm] [r'] [r] i)))
+     (fn _ => i)
+     fl (incl [r] [[]])
diff --git a/lib/ur/incl.urs b/lib/ur/incl.urs
new file mode 100644
index 00000000..d0d78b36
--- /dev/null
+++ b/lib/ur/incl.urs
@@ -0,0 +1,20 @@
+con incl :: K --> {K} -> {K} -> Type
+
+val incl : K --> r1 :: {K} -> r2 :: {K} -> [r1 ~ r2] => incl r1 (r1 ++ r2)
+val proj : r1 ::: {Type} -> r2 ::: {Type} -> incl r1 r2 -> $r2 -> $r1
+
+val inv1 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K}
+           -> [[nm] ~ r] =>
+    f :: (Name -> K -> {K} -> Type)
+    -> incl ([nm = t] ++ r) r'
+    -> (nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r))
+    -> f nm t r'
+val inv2 : K --> nm :: Name -> t ::: K -> r :: {K} -> r' :: {K}
+           -> [[nm] ~ r] =>
+    incl ([nm = t] ++ r) r' -> incl r r'
+
+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
+           -> (nm :: Name -> v :: K -> r' :: {K}
+               -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r'))
+           -> tf []
+           -> folder r -> tf r
diff --git a/lib/ur/mem.ur b/lib/ur/mem.ur
new file mode 100644
index 00000000..7f66b3c2
--- /dev/null
+++ b/lib/ur/mem.ur
@@ -0,0 +1,38 @@
+con mem' = K ==> fn (nm :: Name) (t :: K) (r :: {K}) (r' :: {K}) =>
+    [[nm] ~ r'] => {Expose : f :: ({K} -> Type) -> f r -> f ([nm = t] ++ r'),
+                    Hide : f :: ({K} -> Type) -> f ([nm = t] ++ r') -> f r}
+
+con mem = K ==> fn (nm :: Name) (t :: K) (r :: {K}) =>
+                   tp :: Type -> (r' :: {K} -> [[nm] ~ r'] => mem' nm t r r' -> tp) -> tp
+
+fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] =
+    fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) =>
+       f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x,
+                                  Hide = fn [f :: {K} -> Type] x => x})
+
+fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) =
+    m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') =>
+                                fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] =>
+                                                 mem' nm (f t) (map f r) r' -> tp) =>
+                                   f [map f r'] ! (fn [[nm] ~ map f r'] =>
+                                                      {Expose = fn [f' :: {K2} -> Type] x =>
+                                                                   m'.Expose [fn r => f' (map f r)] x,
+                                                       Hide = fn [f' :: {K2} -> Type] x =>
+                                                                 m'.Hide [fn r => f' (map f r)] x}))
+
+fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) =
+    m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
+              (m'.Expose [fn r => $r] r).nm)
+
+fun replace [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) (v : t) =
+    m [$r] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') =>
+               m'.Hide [fn r => $r] (m'.Expose [fn r => $r] r -- nm ++ {nm = v}))
+
+fun fold [K] [tf :: ({K} -> Type)] [r ::: {K}]
+    (f : nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
+     => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
+    (i : tf []) (fl : folder r) =
+    @@Incl.fold [tf] [r]
+      (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc =>
+          f [nm] [v] [r'] ! (Incl.inv1 [nm] [r'] [r] [mem] i mem) acc)
+      i fl
diff --git a/lib/ur/mem.urs b/lib/ur/mem.urs
new file mode 100644
index 00000000..78021823
--- /dev/null
+++ b/lib/ur/mem.urs
@@ -0,0 +1,13 @@
+con mem :: K --> Name -> K -> {K} -> Type
+
+val mem : K --> nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => mem nm t ([nm = t] ++ r)
+val mp : K --> K2 --> f :: (K -> K2) -> nm ::: Name -> t ::: K -> r ::: {K} -> mem nm t r -> mem nm (f t) (map f r)
+
+val proj : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t
+val replace : nm ::: Name -> t ::: Type -> r ::: {Type} -> mem nm t r -> $r -> t -> $r
+
+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
+           -> (nm :: Name -> v :: K -> r' :: {K} -> [[nm] ~ r']
+               => mem nm v r -> tf r' -> tf ([nm = v] ++ r'))
+           -> tf []
+           -> folder r -> tf r
diff --git a/src/especialize.sml b/src/especialize.sml
index 7d129b8b..4936cc61 100644
--- a/src/especialize.sml
+++ b/src/especialize.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -129,6 +129,37 @@ val mayNotSpec = ref SS.empty
 
 fun specialize' (funcs, specialized) file =
     let
+        fun functionInside functiony = U.Con.exists {kind = fn _ => false,
+                                                     con = fn TFun _ => true
+                                                            | CFfi ("Basis", "transaction") => true
+                                                            | CFfi ("Basis", "eq") => true
+                                                            | CFfi ("Basis", "num") => true
+                                                            | CFfi ("Basis", "ord") => true
+                                                            | CFfi ("Basis", "show") => true
+                                                            | CFfi ("Basis", "read") => true
+                                                            | CFfi ("Basis", "sql_injectable_prim") => true
+                                                            | CFfi ("Basis", "sql_injectable") => true
+                                                            | CNamed n => IS.member (functiony, n)
+                                                            | _ => false}
+
+        val functiony = foldl (fn ((d, _), functiony) =>
+                                  case d of
+                                      DCon (_, n, _, c) =>
+                                      if functionInside functiony c then
+                                          IS.add (functiony, n)
+                                      else
+                                          functiony
+                                    | DDatatype dts =>
+                                      if List.exists (fn (_, _, _, cs) =>
+                                                         List.exists (fn (_, _, SOME c) => functionInside functiony c
+                                                                       | _ => false) cs) dts then
+                                          IS.addList (functiony, map #2 dts)
+                                      else
+                                          functiony
+                                    | _ => functiony) IS.empty file
+
+        val functionInside = functionInside functiony
+
         fun bind (env, b) =
             case b of
                 U.Decl.RelE xt => xt :: env
@@ -286,17 +317,7 @@ fun specialize' (funcs, specialized) file =
                             (*val () = Print.prefaces "Consider" [("e", CorePrint.p_exp CoreEnv.empty
                                                                                       (e, ErrorMsg.dummySpan))]*)
 
-                            val functionInside = U.Con.exists {kind = fn _ => false,
-                                                               con = fn TFun _ => true
-                                                                      | CFfi ("Basis", "transaction") => true
-                                                                      | CFfi ("Basis", "eq") => true
-                                                                      | CFfi ("Basis", "num") => true
-                                                                      | CFfi ("Basis", "ord") => true
-                                                                      | CFfi ("Basis", "show") => true
-                                                                      | CFfi ("Basis", "read") => true
-                                                                      | CFfi ("Basis", "sql_injectable_prim") => true
-                                                                      | CFfi ("Basis", "sql_injectable") => true
-                                                                      | _ => false}
+
                             val loc = ErrorMsg.dummySpan
 
                             fun findSplit av (xs, typ, fxs, fvs, fin) =
@@ -332,6 +353,8 @@ fun specialize' (funcs, specialized) file =
                                        andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs) then
                                 ((*Print.prefaces "No" [("name", Print.PD.string name),
                                                       ("f", Print.PD.string (Int.toString f)),
+                                                      ("xs",
+                                                       Print.p_list (CorePrint.p_exp CoreEnv.empty) xs),
                                                       ("fxs'",
                                                        Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*)
                                  default ())
diff --git a/src/unpoly.sml b/src/unpoly.sml
index 0d239cb9..41532b85 100644
--- a/src/unpoly.sml
+++ b/src/unpoly.sml
@@ -258,9 +258,9 @@ fun decl (d, st : state) =
                         fun kind _ = false
                         fun con _ = false
 
-                        fun exp e =
+                        fun exp (cn, e) =
                             case e of
-                                ECApp (e, c) =>
+                                orig as ECApp (e, c) =>
                                 let
                                     fun isIrregular (e, pos) =
                                         case #1 e of
@@ -268,20 +268,24 @@ fun decl (d, st : state) =
                                             IS.member (ns, n)
                                             andalso
                                             (case #1 c of
-                                                 CRel i => i <> nargs - pos
+                                                 CRel i => i <> nargs - pos + cn
                                                | _ => true)
                                           | ECApp (e, _) => isIrregular (e, pos + 1)
                                           | _ => false
                                 in
                                     isIrregular (e, 1)
                                 end
-                              | ECAbs _ => true
                               | _ => false
 
-                        val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
+                        fun bind (cn, b) =
+                            case b of
+                                U.Exp.RelC _ => cn+1
+                              | _ => cn
+
+                        val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0
                     in
                         if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
-                            (d, st)
+                            (print "Poppycock!\n"; (d, st))
                         else
                             (d, {funcs = foldl (fn (vi, funcs) =>
                                                    IM.insert (funcs, #2 vi, {kinds = cargs,