Mercurial > urweb
changeset 1180:ac3dbbc85c6e
Standard library moduls Incl and Mem; tweaks to Especialize and Unpoly
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 06 Mar 2010 16:15:26 -0500 |
| parents | c58453683bbb |
| children | 618f9f458da9 |
| files | lib/ur/incl.ur lib/ur/incl.urs lib/ur/mem.ur lib/ur/mem.urs src/especialize.sml src/unpoly.sml |
| diffstat | 6 files changed, 156 insertions(+), 18 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/incl.ur Sat Mar 06 16:15:26 2010 -0500 @@ -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] [[]])
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/incl.urs Sat Mar 06 16:15:26 2010 -0500 @@ -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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/mem.ur Sat Mar 06 16:15:26 2010 -0500 @@ -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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/ur/mem.urs Sat Mar 06 16:15:26 2010 -0500 @@ -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
--- a/src/especialize.sml Thu Mar 04 16:59:13 2010 -0500 +++ b/src/especialize.sml Sat Mar 06 16:15:26 2010 -0500 @@ -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 @@ 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 @@ (*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 @@ 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 ())
--- a/src/unpoly.sml Thu Mar 04 16:59:13 2010 -0500 +++ b/src/unpoly.sml Sat Mar 06 16:15:26 2010 -0500 @@ -258,9 +258,9 @@ 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 @@ 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,