packages feed

narc (empty) → 0.1

raw patch · 26 files changed

+2447/−0 lines, 26 filesdep +HDBCdep +HUnitdep +QuickChecksetup-changed

Dependencies added: HDBC, HUnit, QuickCheck, base, mtl, random

Files

+ Gensym.hs view
@@ -0,0 +1,30 @@+module Gensym (+    Gensym(..), gensym, runGensym+  ) where++import Control.Applicative++-- Gensym monad++data Gensym a = G (Int -> (Int, a))++instance Monad Gensym where+    return v = G(\x -> (x,v))+    m >>= k = G(\x -> let G f = m in+                      let (x', v) = f x in +                      let G f' = k v in f' x')++instance Functor Gensym where+    fmap f x = x >>= (return . f)++instance Control.Applicative.Applicative Gensym where+    pure = return+    f <*> x = do f' <- f ; x' <- x ; return (f' x')++gensym :: Gensym Int+gensym = G(\x -> (x+1, x))++runGensym (G f) = snd $ f 0++instance Show a => Show (Gensym a) where+    show x = show $ runGensym x
+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2008-2011, Ezra e. k. Cooper++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.++"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.
+ Narc.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++-- | Query SQL databases using Nested Relational Calculus embedded in+-- Haskell.+-- +-- The primed functions in this module are in fact the syntactic +-- forms of the embedded language. Use them as, for example:+-- +-- >  foreach (table "employees" []) $ \emp ->+-- >    having (primApp "<" [cnst 20000, project emp "salary"]) $+-- >    singleton (record [(project emp "name")])++module Narc (+  -- * The type of the embedded terms+  NarcTerm,+  -- * Translation to an SQL representation+  narcTermToSQL,+  -- * The language itself+  unit, Const, primApp, abs, app, ifthenelse, singleton,+  nil, union, record, project, foreach, having+) where++import Prelude hiding (abs, catch)+import Control.Exception (catch, throwIO, evaluate, SomeException)+import Control.Monad.State hiding (when, join)+import Control.Monad.Error (throwError, runErrorT, Error(..))+import Data.List (nub, (\\), sort, sortBy, groupBy, intersperse)+import Data.Maybe (fromJust, isJust, fromMaybe)++import Control.Applicative ((<$>), (<*>))+import Foreign (unsafePerformIO)            -- FIXME++import Test.QuickCheck hiding (promote, Failure)+import QCUtils+import Test.HUnit hiding (State, assert)++import Debug.Trace++import Gensym++import Narc.AST+import Narc.Common+import Narc.Compile+import Narc.Debug+import Narc.Eval+import Narc.Failure+import Narc.Pretty+import Narc.AST.Pretty+import Narc.SQL.Pretty+import qualified Narc.SQL as SQL+import Narc.Type as Type+import Narc.TypeInfer+import Narc.Util++import Narc.HDBC++-- THE AWESOME FULL COMPILATION FUNCTION -------------------------------++typeCheckAndCompile :: Term a -> SQL.Query+typeCheckAndCompile = compile [] . runTyCheck []++-- The Narc embedded langauge-------------------------------------------++-- Example query++example_dull = (Comp "x" (Table "foo" [("a", TBool)], ())+                (If (Project (Var "x", ()) "a", ())+                 (Singleton (Var "x", ()), ())+                 (Nil, ()), ()), ())++-- HOAS-ish embedded language.++type NarcTerm = Gensym (Term ()) -- ^ Bleck. Rename.++-- | Translate a Narc term to an SQL query string--perhaps the central+-- | function of the interface.+narcTermToSQLString :: NarcTerm -> String+narcTermToSQLString = SQL.serialize . narcTermToSQL++-- | Translate a Narc term to an SQL query.+narcTermToSQL :: NarcTerm -> SQL.Query+narcTermToSQL = typeCheckAndCompile . realize++-- | Turn a HOAS representation of a Narc term into a concrete,+-- | named-binder representation.+realize :: NarcTerm -> Term ()+realize = runGensym++-- | A dummy value, or zero-width record.+unit :: NarcTerm+unit = return $ (!) Unit++-- | A polymorphic way of embedding constants into a term.+class Const' a where cnst' :: a -> NarcTerm+instance Const' Bool where cnst' b = return ((!)(Bool b))+instance Const' Integer where cnst' n = return ((!)(Num n))++-- | Apply some primitive function, such as @(+)@ or @avg@, to a list+-- of arguments.+primApp :: String -> [NarcTerm] -> NarcTerm+primApp f args =  (!) . PrimApp f <$> sequence args++-- | Create a functional abstraction.+abs :: (String -> NarcTerm) -> NarcTerm+abs fn = do+  n <- gensym+  let x = '_' : show n+  body <- fn x+  return $ (!) $ Abs x body++-- | Apply a functional term to an argument.+app :: NarcTerm -> NarcTerm -> NarcTerm+app l m = (!) <$> (App <$> l <*> m)++-- | A reference to a named database table; second argument is its+-- schema type.+table :: Tabname -> [(Field, Type)] -> NarcTerm+table tbl ty = return $ (!) $ Table tbl ty++-- | A condition between two terms, as determined by the boolean value+-- of the first term.+ifthenelse :: NarcTerm -> NarcTerm -> NarcTerm -> NarcTerm+ifthenelse c t f = (!) <$> (If <$> c <*> t <*> f)++-- | A singleton collection of one item.+singleton :: NarcTerm -> NarcTerm+singleton x = (!) . Singleton <$> x++-- | An empty collection.+nil :: NarcTerm+nil = return $ (!) $ Nil++-- | The union of two collections+union :: NarcTerm -> NarcTerm -> NarcTerm+union l r = (!) <$> (Union <$> l <*> r)++-- | Construct a record (name-value pairs) out of other terms; usually+-- used, with base values for the record elements, as the final+-- result of a query, corresponding to the @select@ clause of a SQL+-- query, but can also be used with nested results internally in a+-- query.+record :: [(String, NarcTerm)] -> NarcTerm+record fields = (!) <$> (Record <$> sequence [do expr' <- expr ; return (lbl, expr') | (lbl, expr) <- fields])++-- | Project a field out of a record value.+project :: NarcTerm -> String -> NarcTerm+project expr field = (!) <$> (Project <$> expr <*> return field)++-- | For each item in the collection resulting from the first+-- argument, give it to the function which is the second argument+-- and evaluate--this corresponds to a loop, or two one part of a+-- cross in traditional SQL queries.+foreach :: NarcTerm -> (NarcTerm -> NarcTerm) -> NarcTerm+foreach src k = do+  src' <- src+  n <- gensym+  let x = '_' : show n+  body' <- k (return (var_ x))+  return $ (!)(Comp x src' body')++-- | Filter the current iteration as per the condition in the first+-- argument. Corresponds to a @where@ clause in a SQL query.+having :: NarcTerm -> NarcTerm -> NarcTerm+having cond body = ifthenelse cond body nil++-- Example query++example' = let t = (table "foo" [("a", TBool)]) in+           foreach t $ \x -> +           (having (project x "a")+             (singleton x))++example2' = let t = (table "foo" [("a", TNum)]) in+            let s = (table "bar" [("a", TNum)]) in+            foreach t $ \x -> +            foreach s $ \y -> +            ifthenelse (primApp "<" [project x "a", project y "a"])+             (singleton x)+             (singleton y)++example3' =+    let t = table "employees" [("name", TString), ("salary", TNum)] in+    foreach t $ \emp ->+    having (primApp "<" [cnst' (20000::Integer), project emp "salary"]) $+      singleton (record [("nom", project emp "name")])++-- Unit tests ----------------------------------------------------------++test_example =+    TestList [+        SQL.serialize (typeCheckAndCompile (realize example'))+        ~?= "select _0.a as a from foo as _0 where _0.a"+        ,+        SQL.serialize (typeCheckAndCompile (realize example2'))+        ~?= "(select _0.a as a from foo as _0, bar as _1 where _0.a < _1.a) union (select _1.a as a from foo as _0, bar as _1 where not(_0.a < _1.a))"+        ,+        SQL.serialize (typeCheckAndCompile (realize example3'))+        ~?= "select _0.name as nom from employees as _0 where 20000 < _0.salary"+    ]
+ Narc/AST.hs view
@@ -0,0 +1,298 @@+{-# LANGUAGE FlexibleInstances #-}++module Narc.AST (+  Term'(..),+  Term,+  Var,+  PlainTerm,+  TypedTerm,+  fvs,+  substTerm,+  strip,+  retagulate,+  rename,+  variables,+  (!),+  unit_, Const, cnst_, primApp_, var_, abs_, app_, table_, ifthenelse_,+  singleton_, nil_, union_, record_, project_, foreach_ +) where++import Data.List as List ((\\), nub)++import Prelude hiding (abs)++import Narc.Common+import Narc.Type+import Narc.Util (alistmap, u)+import Narc.Var++-- | Terms in the nested relational calculus (represented concretely+-- | with named variables)+data Term' a = Unit | Bool Bool | Num Integer | String String+             | PrimApp String [Term a]+             | Var Var | Abs Var (Term a) | App (Term a) (Term a)+             | Table Tabname [(Field, Type)]+             | If (Term a) (Term a) (Term a)+             | Singleton (Term a) | Nil | Union (Term a) (Term a)+             | Record [(String, Term a)]+             | Project (Term a) String+             | Comp Var (Term a) (Term a)+--           | IsEmpty (Term a)+    deriving (Eq,Show)++-- | Terms whose every subexpression is annotated with a value of some+-- | particular type.+type Term a = (Term' a, a)++-- TBD: use term ::: type or similar instead of (term, type).++type PlainTerm = Term ()++type TypedTerm = Term Type++-- Operations on terms -------------------------------------------------++fvs (Unit, _) = []+fvs (Bool _, _) = []+fvs (Num _, _) = []+fvs (String _, _) = []+fvs (PrimApp prim args, _) = nub $ concat $ map fvs args+fvs (Var x, _) = [x]+fvs (Abs x n, _) = fvs n \\ [x]+fvs (App l m, _) = fvs l `u` fvs m+fvs (Table _ _, _) = []+fvs (If c a b, _) = fvs c `u` fvs a `u` fvs b+fvs (Nil, _) = []+fvs (Singleton elem, _) = fvs elem+fvs (Union m n, _) = fvs m `u` fvs n+fvs (Record fields, _) = nub $ concat $ map (fvs . snd) fields+fvs (Project targ _, _) = fvs targ+fvs (Comp x src body, _) = fvs src `u` (fvs body \\ [x])++variables = map ('y':) $ map show [0..]++rename x y (Var z, q) | x == z    = (Var y, q)+                      | otherwise = (Var z, q)+rename x y (l@(Abs z n, q)) | x == z    = l+                            | otherwise = (Abs z (rename x y n), q)+rename x y (App l m, q) = (App (rename x y l) (rename x y m), q)+rename x y (PrimApp prim args, q) = (PrimApp prim (map (rename x y) args), q)+rename x y (Singleton elem, q) = (Singleton (rename x y elem), q)+rename x y (Project targ label, q) = (Project (rename x y targ) label, q)+rename x y (Record fields, q) = (Record (alistmap (rename x y) fields), q)+rename x y (Comp z src body, q) +    | x == z = (Comp z src body, q)+    | y == z = let y' = head $ variables \\ [y] in+               let body' = rename y y' body in+                 (Comp z (rename x y src) (rename x y body'), q)+    | otherwise= (Comp z (rename x y src) (rename x y body), q)+rename x y (String n, q) = (String n, q)+rename x y (Bool b, q) = (Bool b, q)+rename x y (Table s t, q) = (Table s t, q)+rename x y (If c a b, q) = (If (rename x y c) (rename x y a) (rename x y b), q)+rename x y (Unit, q) = (Unit, q)+rename x y (Nil, q) = (Nil, q)+rename x y (Union a b, q) = (Union (rename x y a) (rename x y b), q)++-- | substTerm x v m: substite v for x in term m+-- (Actually incorrect because it does not make substitutions in the q.)+substTerm :: Var -> Term t -> Term t -> Term t+substTerm x v (m@(Unit, _))       = m+substTerm x v (m@(Bool b, _))     = m+substTerm x v (m@(Num n, _))      = m+substTerm x v (m@(String s, _))   = m+substTerm x v (m@(Table s t, _))  = m+substTerm x v (m@(Nil, _))        = m+substTerm x v (Singleton elem, q) = (Singleton (substTerm x v elem), q)+substTerm x v (Union m n, q) = (Union (substTerm x v m) (substTerm x v n), q)+substTerm x v (m@(Var y, _)) | y == x    = v+                             | otherwise = m+substTerm x v (l @ (Abs y n, q))+    | x == y            = l+    | y `notElem` fvs v = (Abs y (substTerm x v n), q) +    | otherwise = +        let y' = head $ variables \\ fvs v in+        let n' = rename y y' n in+        (Abs y' (substTerm x v n'), q)+substTerm x v (App l m, q) = (App (substTerm x v l) (substTerm x v m), q)+substTerm x v (PrimApp prim args,q)= (PrimApp prim (map (substTerm x v) args),q)+substTerm x v (Project targ label, q) = (Project (substTerm x v targ) label, q)+substTerm x v (Record fields, q) = (Record (alistmap (substTerm x v) fields), q)+substTerm x v (Comp y src body, q) +    | x == y    =+        (Comp y src' body, q)+    | y `notElem` fvs v =+        (Comp y src' (substTerm x v body), q)+    | otherwise = +        let y' = head $ variables \\ fvs v in+        let body' = rename y y' body in+        (Comp y' src' (substTerm x v body'), q)+    where src' = (substTerm x v src)+substTerm x v (If c a b, q) = +    (If (substTerm x v c) (substTerm x v a) (substTerm x v b), q)++-- | lazyDepth: calculate a list (poss. inf.) whose sum is the depth+-- of the term. (unused)+lazyDepth :: Term a -> [Int]+lazyDepth (Abs _ n, _) = 1 : lazyDepth n+lazyDepth (App l m, _) = 1 : zipWith max (lazyDepth l) (lazyDepth m)+lazyDepth (Project m _, _) = 1 : lazyDepth m+lazyDepth (Singleton m, _) = 1 : lazyDepth m+lazyDepth (PrimApp prim args, _) =+    1 : foldr1 (zipWith max) (map lazyDepth args)+lazyDepth (Record fields, _) =+    1 : foldr1 (zipWith max) (map (lazyDepth . snd) fields)+lazyDepth (Comp _ src body, _) =+    1 : zipWith max (lazyDepth src) (lazyDepth body)+lazyDepth _ = 1 : []++-- Generic term-recursion functions ------------------------------------++entagulate :: (Term a -> b) -> Term a -> Term b+entagulate f (Bool b, d) = (Bool b, f (Bool b, d))+entagulate f (Num n, d) = (Num n, f (Num n, d))+entagulate f (String s, d) = (String s, f (String s, d))+entagulate f (Var x, d) = (Var x, f (Var x, d))+entagulate f (Abs x n, d) = (Abs x (entagulate f n), f (Abs x n, d))+entagulate f (App l m, d) = (App (entagulate f l) (entagulate f m),+                          f (App l m, d))+entagulate f (If c a b, d) =+    (If (entagulate f c)+     (entagulate f a)+     (entagulate f b),+     f (If c a b, d))+entagulate f (Table tab fields, d) = (Table tab fields, f (Table tab fields, d))+entagulate f (Nil, d) = (Nil, f (Nil,d))+entagulate f (Singleton m, d) = (Singleton (entagulate f m),+                              f (Singleton m, d))+entagulate f (Union a b, d) =+    (Union+     (entagulate f a)+     (entagulate f b),+     f (Union a b, d))+entagulate f (Record fields, d) = (Record (alistmap (entagulate f) fields), +                                f (Record fields, d))+entagulate f (Project m a, d) = (Project (entagulate f m) a,+                              f (Project m a, d))+entagulate f (Comp x src body, d) = +    (Comp x (entagulate f src) (entagulate f body),+     f (Comp x src body, d))++retagulate :: (Term a -> a) -> Term a -> Term a+retagulate f (Unit, d) = (Unit, f (Unit, d))+retagulate f (Bool b, d) = (Bool b, f (Bool b, d))+retagulate f (Num n, d) = (Num n, f (Num n, d))+retagulate f (String s, d) = (String s, f (String s, d))+retagulate f (Var x, d) = (Var x, f (Var x, d))+retagulate f (Abs x n, d) = (Abs x (retagulate f n),+                             f (Abs x (retagulate f n), d))+retagulate f (App l m, d) = (App (retagulate f l) (retagulate f m),+                          f (App (retagulate f l) (retagulate f m), d))+retagulate f (PrimApp fn ar, d) = (PrimApp fn (map (retagulate f) ar),+                                   f (PrimApp fn (map (retagulate f) ar), d))+retagulate f (If c a b, d) =+    (If (retagulate f c)+     (retagulate f a)+     (retagulate f b),+     f (If (retagulate f c)+        (retagulate f a)+        (retagulate f b), d))+retagulate f (Table tab fields, d) = (Table tab fields, f (Table tab fields, d))+retagulate f (Nil, d) = (Nil, f (Nil, d))+retagulate f (Singleton m, d) = (Singleton (retagulate f m),+                              f (Singleton (retagulate f m), d))+retagulate f (Union l m, d) = (Union (retagulate f l) (retagulate f m),+                               f (Union (retagulate f l) (retagulate f m), d))+retagulate f (Record fields, d) = (Record (alistmap (retagulate f) fields), +                                f (Record (alistmap (retagulate f) fields), d))+retagulate f (Project m a, d) = (Project (retagulate f m) a,+                              f (Project (retagulate f m) a, d))+retagulate f (Comp x src body, d) = +    (Comp x (retagulate f src) (retagulate f body),+     f (Comp x (retagulate f src) (retagulate f body), d))++strip = entagulate (const ())++-- | numComps: Number of comprehensions in an expression, a measure of+-- the complexity of the query.+numComps (Comp x src body, _) = 1 + numComps src + numComps body+numComps (PrimApp _ args, _) = sum $ map numComps args+numComps (Abs _ n, _) = numComps n+numComps (App l m, _) = numComps l + numComps m+numComps (Singleton body, _) = numComps body+numComps (Record fields, _) = sum $ map (numComps . snd) fields+numComps (Project m _, _) = numComps m+numComps (Union a b, _) = numComps a + numComps b+numComps (Unit, _) = 0+numComps (Bool _, _) = 0+numComps (Num _, _) = 0+numComps (String _, _) = 0+numComps (Var _, _) = 0+numComps (Table _ _, _) = 0+numComps (If c a b, _) = numComps c + numComps a + numComps b+numComps (Nil, _) = 0++-- | An interface for semanticizing the Narc concrete language as+-- | desired (as per "Unembedding domain specific languages" by Atkey,+-- | Lindley and Yallop).+class NarcSem result where+    unit :: result+    bool :: Bool -> result+    num :: Integer -> result+    string :: String -> result+    primApp :: String -> [result] -> result+    var :: Var -> result+    abs :: Var -> result -> result+    app :: result -> result -> result+    table :: Tabname -> [(Field, Type)] -> result+    ifthenelse :: result -> result -> result -> result+    singleton :: result -> result+    nil :: result+    union :: result -> result -> result+    record :: [(String, result)] -> result+    project :: result -> String -> result+    foreach :: result -> Var -> result -> result+--    cnst :: Constable t => t -> result+class Constable t where cnst :: NarcSem result => t -> result+instance Constable Bool where cnst b = bool b+instance Constable Integer where cnst n = num n++-- Explicit-named builders++(!) x = (x, ())++instance NarcSem (Term'(),()) where+  unit = (!)Unit+  bool b = (!)(Bool b)+  num n = (!)(Num n)+  string n = (!)(String n)+  primApp f args = (!)(PrimApp f args)+  var x = (!)(Var x)+  abs x body = (!)(Abs x body)+  app l m = (!)(App l m)+  table tbl ty = (!)(Table tbl ty)+  ifthenelse c t f = (!)(If c t f)+  singleton x = (!)(Singleton x)+  nil = (!)Nil+  union a b = (!)(Union a b)+  record fields = (!)(Record fields)+  project body field = (!)(Project body field)+  foreach src x body = (!)(Comp x src body)+-- class Const a where cnst_ :: a -> Term ()++unit_ = (!)Unit+class Const a where cnst_ :: a -> Term ()+instance Const Bool where cnst_ b = (!)(Bool b)+instance Const Integer where cnst_ n = (!)(Num n)+primApp_ f args = (!)(PrimApp f args)+var_ x = (!)(Var x)+abs_ x body = (!)(Abs x body)+app_ l m = (!)(App l m)+table_ tbl ty = (!)(Table tbl ty)+ifthenelse_ c t f = (!)(If c t f)+singleton_ x = (!)(Singleton x)+nil_ = (!)Nil+union_ a b = (!)(Union a b)+record_ fields = (!)(Record fields)+project_ body field = (!)(Project body field)+foreach_ src x body = (!)(Comp x src body)
+ Narc/AST/Pretty.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE TypeSynonymInstances #-}++module Narc.AST.Pretty where++import Narc.AST+import Narc.Pretty+import Narc.Util (mapstrcat)++-- Pretty-printing ------------------------------------------------=====++instance Pretty (Term' a) where+  pretty (Unit) = "()"+  pretty (Bool b) = show b+  pretty (Num n) = show n+  pretty (PrimApp f args) = f ++ "(" ++ mapstrcat "," pretty args ++ ")"+  pretty (Var x) = x+  pretty (Abs x n) = "(fun " ++ x ++ " -> " ++ pretty n ++ ")"+  pretty (App l m) = pretty l ++ " " ++ pretty m+  pretty (Table tbl t) = "(table " ++ tbl ++ " : " ++ show t ++ ")"+  pretty (If c a b) =+      "(if " ++ pretty c ++ " then " ++ pretty a ++ +      " else " ++ pretty b ++ " )"+  pretty (Singleton m) = "[" ++ pretty m ++ "]" +  pretty (Nil) = "[]"+  pretty (Union m n) = "(" ++ pretty n ++ " ++ " ++ pretty n ++ ")"+  pretty (Record fields) = +      "{" ++ mapstrcat "," (\(l,m) -> l ++ "=" ++ pretty m) fields ++ "}"+  pretty (Project m l) = "(" ++ pretty m ++ "." ++ l ++ ")"+  pretty (Comp x m n) =+      "(for (" ++ x ++ " <- " ++ pretty m ++ ") " ++ pretty n ++ ")"++instance Pretty (Term a) where+  pretty (m, t) = pretty m
+ Narc/Common.hs view
@@ -0,0 +1,6 @@+module Narc.Common where++type Tabname = String++type Field = String+
+ Narc/Compile.hs view
@@ -0,0 +1,226 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Narc.Compile (compile) where++import Data.List ((\\))++import Narc.AST+import Narc.AST.Pretty ()+import Narc.Contract+import Narc.Debug (forceAndReport)+import Narc.Pretty+import Narc.SQL+import Narc.Type as Type+import Narc.TypeInfer+import Narc.Util (image, maps, alistmap)++-- -- Testing-related imports+-- import Test.QuickCheck (Property, forAll, sized)+-- import Narc.TermGen+-- import Narc.Eval+-- import Narc.Failure++-- { Compilation } -----------------------------------------------------++etaExpand :: TypedTerm -> [(String, Type)] -> TypedTerm+etaExpand expr fieldTys =+    let exprTy = TRecord fieldTys in+    (Record [(field, ((Project expr field), fTy))+             | (field, fTy) <- fieldTys], +     exprTy)++-- | Normalize DB terms in a nearly call-by-value way.+normTerm :: [(String, QType)] -- ^ An environment, typing all free vars.+         -> TypedTerm         -- ^ The term to normalize.+         -> TypedTerm+normTerm _env (m@(Unit, _ty))   = m+normTerm _env (m@(Bool _, _))   = m+normTerm _env (m@(Num _, _))    = m+normTerm _env (m@(String _, _)) = m+normTerm env (PrimApp fun args, t) = (PrimApp fun (map (normTerm env) args), t)+normTerm env (expr@(Var x, t)) = +    -- Eta-expand at record type.+    if (maps x) env then +        case t of+          TRecord t' -> etaExpand expr t'+          _ -> (Var x, t) +    else+      error $ "Free variable "++ x ++ " in normTerm"+normTerm _env (Abs x n, t) =+    (Abs x n, t)+normTerm env (App l m, t) = +    let w = normTerm env m in+    case normTerm env l of +      (Abs x n, _) -> +          forceAndReport (+            let !n' = substTerm x w n in+            normTerm env (runTyCheck env $ n')+          ) ("susbtituting "++show w++" for "++x++" in "++show n)+      (If b l1 l2, _) ->+          (normTerm env (If b (App l1 w, t) (App l2 w, t), t))+      v@(Var _, _) -> (App v w, t)+      v -> error $ "unexpected normal form in appl posn in normTerm " ++ show v+normTerm _env (Table s t, t') = (Table s t, t')+normTerm env (If b m (Nil, _), t@(TList _)) =+    let b' = normTerm env b in+    case normTerm env m of+      (Nil, _)           -> (Nil, t)+      (Singleton m', _)  -> (If b' (Singleton m', t) (Nil, t), t)+      (Table s fTys, _)  -> (If b' (Table s fTys, t) (Nil, t), t)+      (Comp x l m', _)   -> normTerm env (Comp x l (If b' m' (Nil, t), t), t)+      (m1 `Union` m2, _) -> ((normTerm env (If b' m1 (Nil, t), t)) `Union`+                             (normTerm env (If b' m2 (Nil, t), t)), t)+      v@(If _ _ _, _)    -> (If b' v (Nil, t), t)+      v -> error $ "Unexpected normal form in conditional body in normTerm: " +++                    show v+normTerm env (If b@(_,bTy) m n, t@(TList _)) = -- The case where n /= Nil+    ((normTerm env (If b m (Nil, t), t)) `Union` +     (normTerm env (If (PrimApp "not" [b], bTy) n (Nil, t), t)), t)+normTerm env (If b m n, t@(TRecord fTys)) =+    let b' = normTerm env b in+    let (Record mFields, _) = normTerm env m+        (Record nFields, _) = normTerm env n in+    (Record [(l, (If b' (image l mFields) (image l nFields), (image l fTys)))+             | (l, _) <- mFields],+     t)+normTerm env (If b m n, t) = +    (If (normTerm env b) (normTerm env m) (normTerm env n), t)+normTerm env (Singleton m, t) = (Singleton (normTerm env m), t)+normTerm _env (Nil, t) = (Nil, t)+normTerm env (m `Union` n, t) = ((normTerm env m) `Union` (normTerm env n), t)+normTerm env (Record fields, t) =+    (Record [(a, normTerm env m) | (a, m) <- fields], t)+normTerm env (Project argTerm label, t) = +    case normTerm env argTerm of+      (Record fields, _) -> case (lookup label fields) of +                              Just x -> x +                              Nothing -> error $ "no field " ++ label+      -- Ah, the following not necessary because If pushes into records.+      (If condn v1 v2,_) ->+          normTerm env (If condn+                        (Project v1 label, t)+                        (Project v2 label, t), t)+      v@(Var _x, _) -> (Project v label, t)+      v -> error $ "Unexpected normal form in body of Project in normTerm: " ++ +                    show v+normTerm env (Comp x src body, t) =+    case normTerm env src of+      (Nil, _) -> (Nil, t)+      (Singleton src', _) -> +          forceAndReport (+            let !n' = substTerm x src' body in+            normTerm env (runTyCheck env n')+          ) ("Substituting " ++ show src' ++ " for " ++ x ++ " in " ++ show body)+      (Comp y src2 body2, _) ->+          -- Freshen @y@ over @src@ with respect to @body@ (that of+          -- the outer comprehension), because we're widening the+          -- scope of @y@ to include @body@.+          let (y', body') = if y `elem` fvs body then+                              let newY = minFreeFor body in+                              (newY, rename y newY body)+                         else (y, body)+          in+            (normTerm env (Comp y' src2 (Comp x body2 body', t), t))+      (srcL `Union` srcR, _) ->+          ((normTerm env (Comp x srcL body, t)) `Union` +           (normTerm env (Comp x srcR body, t)), t)+      (tbl @ (Table _tableName fieldTys, _)) ->+          insert (\(v',t') -> (Comp x tbl (v',t'), t')) $+                 let env' = Type.bind x ([],TList(TRecord fieldTys)) env in +                 normTerm env' body+      (If cond' src' (Nil, _), _) ->+          assert (x `notElem` fvs cond') $+          let v = normTerm env (Comp x src' body, t) in+          insertFurther (\(v',t') -> (If cond' (v',t') (Nil, t'), t')) v+      v -> error $+             "unexpected normal form in source part of comprehension: " +++             show v++-- Insertion functions for rebuilding a term, dropping a+-- reconstructor k down through unions and compr'ns (there must be+-- a better way!).+insert :: (TypedTerm -> TypedTerm) -> TypedTerm -> TypedTerm+insert k ((v,t) :: TypedTerm) =+    case v of+      Nil -> (Nil, t)+      n1 `Union` n2 -> ((insert k n1) `Union` (insert k n2), t)+      _ -> k (v,t)++insertFurther :: (TypedTerm -> TypedTerm) -> TypedTerm -> TypedTerm+insertFurther k ((v,t) :: TypedTerm) =+    case v of+      Nil -> (Nil, t)+      n1 `Union` n2 -> +          ((insertFurther k n1) `Union` (insertFurther k n2), t)+      Comp x m n -> (Comp x m (insertFurther k n), t)+      _ -> k (v,t)++-- See (Bird 2010) for a better algorithm here.+minFreeFor :: Term a -> Var+minFreeFor n = head $ variables \\ fvs n ++-- | @translateTerm@ homomorphically translates a normal-form Term to an+-- | SQL Query.+translateTerm :: TypedTerm -> Query+translateTerm (v `Union` u, _) = (translateTerm v) `QUnion` (translateTerm u)+translateTerm (Nil, _)         = Narc.SQL.emptyQuery+translateTerm (f@(Comp _ (Table _ _, _) _, _))                  = translateF f+translateTerm (f@(If _ _ (Nil, _), _))                          = translateF f+translateTerm (f@(Singleton (Record _, _), _))                  = translateF f+translateTerm (f@(Table _ _, _))                                = translateF f+translateTerm x = +    error $ "translateTerm got unexpected term: " ++ (pretty.fst) x++-- translateF, translateZ and translateB are named after the syntactic+-- classes (in the grammar of the normalized form) which they handle.+-- (F for "for comprehension", Z for "final bit of a nest of+-- comprehensions", and B for "base type"+translateF :: Term b -> Query+translateF (Comp x (Table tabname fTys, _) n, _) =+    let q@(Select _ _ _) = translateF n in+    Select {rslt = rslt q,+            tabs = (tabname, x, TRecord fTys):tabs q,+            cond = cond q}+translateF (z@(If _ _ (Nil, _), _))                             = translateZ z+translateF (z@(Singleton (Record _, _), _))                     = translateZ z+translateF (z@(Table _ _, _))                                   = translateZ z+translateF m = error $ "translateF for unexpected term: " ++ pretty (fst m)++translateZ :: Term b -> Query+translateZ (If b z (Nil, _), _) =+    let q@(Select _ _ _) = translateZ z in+    Select {rslt=rslt q, tabs = tabs q, cond = translateB b : cond q}+translateZ (Singleton (Record fields, _), _) = +    Select {rslt = QRecord(alistmap translateB fields), tabs = [], cond = []}+translateZ (Table tabname fTys, _) =+    Select {rslt = QRecord[(l,QField tabname l)| (l,_ty) <- fTys],+            tabs = [(tabname, tabname, TRecord fTys)], cond = []}+translateZ z = error$ "translateZ got unexpected term: " ++ (pretty.fst) z++translateB :: Term b -> Query+translateB (If b b' b'', _)            = QIf (translateB b)+                                           (translateB b') (translateB b'') +translateB (Bool n, _)                 = (QBool n)+translateB (Num n, _)                  = (QNum n)+translateB (Project (Var x, _) l, _)   = QField x l+translateB (PrimApp "not" [arg], _)    = QNot (translateB arg)+translateB (PrimApp "<" [l, r], _)     = QOp (translateB l) Less (translateB r)+translateB b = error$ "translateB got unexpected term: " ++ (pretty.fst) b++compile :: TyEnv -> TypedTerm -> Query+compile env = translateTerm . normTerm env++-- -- Tests++-- -- FIXME: where does this belong? It tests a function internal to this+-- -- module (normTerm) but uses testing apparatus that is defined at a+-- -- "higher" layer (Narc.Test) and uses an otherwise unrelated module+-- -- (Narc.Eval).+-- prop_norm_sound :: TyEnv -> Env -> Property+-- prop_norm_sound tyEnv env =+--   forAll (sized (typeGen [])) $ \t ->+--   forAll (sized (typedTermGen tyEnv t)) $ \m ->+--       isErrorMSuccess $ tryErrorGensym $ +--       do m' <- infer m+--          return (eval env (normTerm tyEnv m') == eval env m')
+ Narc/Contract.hs view
@@ -0,0 +1,7 @@+module Narc.Contract where++-- Contractual assertions ----------------------------------------------++contract p x = if p x then x else error "Contract broken"++assert x e = if x then e else error "assertion failed"
+ Narc/Debug.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Narc.Debug where++import Prelude hiding (catch)+import Control.Exception (catch, evaluate, throwIO, SomeException)+import Debug.Trace (trace)+import Foreign (unsafePerformIO)++-- | Enable/disable debugging messages+debugFlag :: Bool+debugFlag = False++-- | Trace the given string if debugging is on, or do nothing if not.+debug :: String -> a -> a+debug str = if debugFlag then trace str else id++breakFlag x = x     -- a hook for a breakpoint in GHCi debugger++-- | Force an arbitrary expression, tracing the @String@ arg if+-- forcing produces an exception.+forceAndReport :: a -> String -> a+forceAndReport expr msg = +          unsafePerformIO $+          catch (evaluate $+                 expr `seq` expr+          ) (\(exc::SomeException) ->+            breakFlag $ +            debug msg $ +             Control.Exception.throwIO exc+          )
+ Narc/Eval.hs view
@@ -0,0 +1,119 @@+module Narc.Eval where++import Narc.AST+import Narc.Debug (debug)+import Narc.Util (alistmap)++--+-- Evaluation ----------------------------------------------------------+--++-- { Values and value environments } -----------------------------------++bind x v env = (x,v):env++-- type RuntimeTerm = Term (Maybe Query)++type Env = [(Var, Value)]++data Value = VUnit | VBool Bool | VNum Integer+            | VList [Value]+            | VRecord [(String, Value)]+            | VAbs Var TypedTerm Env+        deriving (Eq, Show)++fromValue :: Value -> TypedTerm+fromValue VUnit = (Unit, undefined)+fromValue (VBool b) = (Bool b, undefined)+fromValue (VNum n) = (Num n, undefined)+fromValue (VList xs) = foldr1 union (map singleton $ map fromValue xs)+    where union x y = (x `Union` y, undefined)+          singleton x = (Singleton x, undefined)+fromValue (VRecord fields) = (Record (alistmap fromValue fields), undefined)+fromValue (VAbs x n env) = foldr (\(y,v) -> substTerm y (fromValue v))+                           (Abs x n, undefined) env++concatVLists xs = VList $ concat [x | (VList x)<-xs]++initialEnv :: Env+initialEnv =+    []+--     [("+",+--       ((VAbs "x" (Abs "y"+--                   (PrimApp "+" [(Var "x", (TNum, openEpe), (Var "y", TNum)],+--                    Just (QOp (QVar "x") Plus (QVar "y"))), TNum) []),+--        Just (QAbs "x" (QAbs "y" (QOp (QVar "x") Plus (QVar "y"))))))]++-- | appPrim: apply a primitive function to a list of value arguments.+appPrim :: String -> [Value] -> Value+appPrim "+" [VNum a, VNum b] = VNum (a+b)+appPrim p _ = error("Unknown primitive" ++ p)++-- | eval: Evaluate a typed term in a closing environment. Captures the+-- effects performed by the term. (NB: type info is not actually used;+-- should eliminate this.)+eval :: Env -> TypedTerm -> Value+eval env (Unit, _) = (VUnit)+eval env (Bool b, q) = (VBool b)+eval env (Num n, q) = (VNum n)+eval env (PrimApp prim args, q) = +    let (vArgs) = map (eval env) args in+    (appPrim prim vArgs)+eval env (Var x, q) =+    case lookup x env of+      Nothing -> error+                 ("Variable " ++ x ++ " not found in env " ++ show env ++ +                  " while evaluating term.")+      Just v -> v+eval env (Abs x n, q) = (VAbs x n env')+    where env' = filter (\(a,b) -> a `elem` fvs n) env+eval env (App l m, q) = +    let (v) = eval env l in+    let (w) = eval env m in+    case v of+      (VAbs x n env') -> +          let env'' = bind x w env' in+          let (r) = eval env'' n in+          (r)+      _ -> error "non-function applied"+eval env (Table name fields, q) = +    (VList [])+eval env (If c a b, _) =+    let (VBool t) = eval env c in+    let (result) = if t then eval env a else eval env b in+    (result)+eval env (Nil, _) =+    (VList [])+eval env (Singleton body, q) =+    let (v) = eval env body in+    (VList [v])+eval env (Union m n, _) =+    let (VList v) = eval env m in+    let (VList w) = eval env n in+    (VList $ v ++ w)+eval env (Record fields, q) =+    let (vFields) = [let (value) = eval env term in+                     ((name, value))+                     | (name, term) <- fields] in+    (VRecord vFields)+eval env (Project m f, q) =+    let (v) = eval env m in+    case v of+      VRecord fields -> +          case lookup f fields of {+            Nothing -> error $ "No field " ++ f ++ " in " ++ +                               show v ++ "(" ++ show m ++ ")" ;+            Just vField -> vField+          }+      _ -> error("Non-record value " ++ show v ++ " target of projection " ++ +                 show(Project m f))+eval env (Comp x src body, q) =+    let (vSrc) = eval env src in+    case vSrc of+      (VList elems) -> +          let (results) = [eval (bind x v env) body+                           | v <- elems] in+          (concatVLists results)+      _ -> error("Comprehension source was not a list.")++run = eval initialEnv
+ Narc/Failure.hs view
@@ -0,0 +1,46 @@+module Narc.Failure where++import Narc.Debug+import Control.Monad.Error hiding (when, join)+import Gensym++-- Failure and ErrorGensym monads --------------------------------------+-- (TBD: this is more general than Narc; factor it out.)++type Failure a = Either String a++fayl = Left -- TBD: would be better to make Failure a newtype & use+            -- fail from Monad.++-- instance Monad Failure where+--     return = Failure . Right+--     fail = Failure . Left+--     x >>= k = case x of Failure(Left err) -> Failure(Left err)+--                         Failure(Right x') -> k x'++runError :: Either String t -> t+runError (Left e) = breakFlag $ error e+runError (Right x) = x++isError (Left x) = True+isError (Right _) = False++isSuccess (Left _) = False+isSuccess (Right _) = True++type ErrorGensym a = ErrorT String Gensym a++-- | Run an ErrorGensym action, raising errors with `error'.+runErrorGensym = runError . runGensym . runErrorT++-- | Try running an ErrorGensym action, packaging result in an Either+-- | with Left as failure, Right as success.+tryErrorGensym = runGensym . runErrorT++under x = either throwError return x++isErrorMSuccess = either (const False) (const True) ++instance Error () where+    noMsg = ()+    strMsg _ = ()
+ Narc/Failure/QuickCheck.hs view
@@ -0,0 +1,17 @@+module Narc.Failure.QuickCheck where++import Test.QuickCheck++import QCUtils+import Narc.Failure++-- QuickCheck property utilities ---------------------------------------++failureToProperty :: Test.QuickCheck.Testable a => Failure a -> Property+failureToProperty (Left _) = failProp+failureToProperty (Right x) = property x++failureToPropertyIgnoreFailure :: Test.QuickCheck.Testable a => +                                  Failure a -> Property+failureToPropertyIgnoreFailure (Left _) = ignore+failureToPropertyIgnoreFailure (Right x) = property x
+ Narc/HDBC.hs view
@@ -0,0 +1,13 @@+module Narc.HDBC where++import Database.HDBC++import Narc.AST+import Narc.SQL+import Narc.Compile+import Narc.TypeInfer++run :: IConnection conn => Term a -> conn -> IO [[SqlValue]]+run t conn =+    let sql = serialize (compile [] (runTyCheck [] t)) in+    quickQuery conn sql []
+ Narc/Pretty.hs view
@@ -0,0 +1,8 @@+module Narc.Pretty where++import Narc.Common++-- Pretty-printing ------------------------------------------------=====++class Pretty t where+  pretty :: t -> String
+ Narc/Rewrite.hs view
@@ -0,0 +1,67 @@+module Narc.Rewrite where++import Data.Maybe (fromMaybe)++import Narc.AST+import Narc.Type+import Narc.Util (alistmap)++-- Rewrite -------------------------------------------------------------+--+-- Small-step version of compilation: local rewrite rules applied+-- willy-nilly.++perhaps :: (a -> Maybe a) -> a -> a+perhaps f x = fromMaybe x (f x)++bu :: (Term a -> Maybe (Term a)) -> Term a -> Term a+bu f (Unit, d) = perhaps f (Unit, d)+bu f (Bool b, d) = perhaps f (Bool b, d)+bu f (Num n, d) = perhaps f (Num n, d)+bu f (Var x, d) = perhaps f (Var x, d)+bu f (Abs x n, d) = perhaps f (Abs x (bu f n), d)+bu f (App l m, d) = perhaps f (App (bu f l) (bu f m), d)+bu f (If c a b, d) =+    perhaps f (If (bu f c)+          (bu f a)+          (bu f b), d)+bu f (Table tab fields, d) = perhaps f (Table tab fields, d)+bu f (Singleton m, d) = perhaps f (Singleton (bu f m), d)+bu f (Record fields, d) = perhaps f (Record (alistmap (bu f) fields), d)+bu f (Project m a, d) = perhaps f (Project (bu f m) a, d)+bu f (Comp x src body, d) = perhaps f (Comp x (bu f src) (bu f body), d)+bu f (PrimApp fun args, d) = perhaps f (PrimApp fun args, d)+bu f (Nil, d) = perhaps f (Nil, d)+bu f (Union a b, d) = perhaps f (Union a b, d)++rw (Comp x (Singleton m, _) n, t) = Just (substTerm x m n)+rw (App (Abs x n, st) m, t) = Just (substTerm x m n)+rw (Project (Record fields, rect) fld, t) = lookup fld fields+rw (Singleton (Var x, xT), t) = Nothing -- for now+rw (Comp x (Nil, _) n, t) = Just (Nil, t)+rw (Comp x m (Nil, _), t) = Just (Nil, t)+rw (Comp x (Comp y l m, s) n, t) = +    if y `notElem` fvs n then+        Just (Comp y l (Comp x m n, t), t)+    else Nothing+rw (Comp x (m1 `Union` m2, s) n, t) =+    Just ((Comp x m1 n, t) `Union` (Comp x m2 n, t), t)+rw (Comp x m (n1 `Union` n2, _), t) =+    Just ((Comp x m n1, t) `Union` (Comp x m n2, t), t)+rw (Comp x (If b m (Nil, _), _) n, t) =+    Just (Comp x m (If b n (Nil, t), t), t)+rw (If (b, bTy) m n, t@(TList _, _)) | fst n /= Nil =+                      Just((If (b,bTy) m (Nil, t), t) `Union`+                           (If (PrimApp "not" [(b, bTy)], bTy) n (Nil, t), t), t)+rw (If b (Nil, _) (Nil, _), t) = Just (Nil, t)+rw (If b (Comp x m n, _) (Nil, _), t) = Just (Comp x m (If b n (Nil, t), t), t) +rw (If b (m1 `Union` m2, _) (Nil, _), t) =+    Just ((If b m1 (Nil, t), t) `Union` (If b m2 (Nil, t), t), t)+-- push App inside If+-- push Project inside If+-- push If inside Record+-- rw (IsEmpty m, t) +--     | lorob t   = Nothing+--     | otherwise = +--         IsEmpty (Comp "x" m (Singleton (Unit, TUnit), TList Tunit), TList TUnit)+rw _ = Nothing
+ Narc/SQL.hs view
@@ -0,0 +1,155 @@+module Narc.SQL where++import Data.List (nub, intercalate)++import Narc.Common+import Narc.Type+import Narc.Util (u, mapstrcat)++--+-- SQL Queries ---------------------------------------------------------+--++data Op = Eq | Less+        | Plus | Minus | Times | Divide+        deriving(Eq, Show)++data UnOp = Min | Max | Count | Sum | Average+        deriving (Eq, Show)++-- | Query: the type of SQL queries ("select R from Ts where B")+-- (This is unpleasant; it should probably be organized into various+-- syntactic classes.)+data Query = Select {rslt :: Query,                  -- make this a list+                     tabs :: [(Field, Field, Type)], -- use [(Field,Type)]+                     cond :: [Query]+                    }+           | QNum Integer+           | QBool Bool+           | QNot Query+           | QOp Query Op Query+           | QField String String+           | QRecord [(Field, Query)]+           | QUnion Query Query+           | QIf Query Query Query+           | QExists Query+        deriving(Eq, Show)++emptyQuery = Select {rslt = QRecord [], tabs = [], cond = [QBool False]}++-- | @sizeQuery@ approximates the size of a query by calling giving up+-- | its node count past a certain limit (currently limit = 100, below).+sizeQueryExact :: Query -> Integer+sizeQueryExact (q@(Select _ _ _)) =+    sizeQueryExact (rslt q) + (sum $ map sizeQueryExact (cond q))+sizeQueryExact (QNum n) = 1+sizeQueryExact (QBool b) = 1+sizeQueryExact (QNot q) = 1 + sizeQueryExact q+sizeQueryExact (QOp a op b) = 1 + sizeQueryExact a + sizeQueryExact b+sizeQueryExact (QField t f) = 1+sizeQueryExact (QRecord fields) = sum [sizeQueryExact n | (a, n) <- fields]+sizeQueryExact (QUnion m n) = sizeQueryExact m + sizeQueryExact n+sizeQueryExact (QIf c a b) = sizeQueryExact c + sizeQueryExact a + sizeQueryExact b+sizeQueryExact (QExists q) = 1 + sizeQueryExact q++-- | @sizeQuery@ approximates the size of a query by calling giving up+-- | its node count past a certain limit (currently limit = 100, below).+sizeQuery :: Query -> Integer+sizeQuery qy = loop 0 qy+    where+      loop' :: Integer -> Query -> Integer+      loop' n qy = if n > limit then n else loop n qy++      loop :: Integer -> Query -> Integer+      loop n (q@(Select _ _ _)) = +          let n' = foldr (\r n -> loop' n r) n (cond q) in+          loop' n' (rslt q)+      loop n (QNum i) = n + 1+      loop n (QBool b) = n + 1+      loop n (QNot q) = loop' (n+1) q+      loop n (QOp a op b) = let n' = loop' (n+1) a in loop' n' b+      loop n (QField t f) = n + 1+      loop n (QRecord fields) = foldr (\r n -> loop' n r) n (map snd fields)+      loop n (QUnion a b) = let n' = loop' (n+1) a in loop' n' b+      loop n (QIf c a b) = +          let n' = loop' (n+1) c in+          let n'' = loop' n' a in+          loop' n'' b+      loop n (QExists q) = loop' (n+1) q++      limit = 100++-- Basic functions on query expressions --------------------------------++freevarsQuery (q@(Select _ _ _)) = +    (freevarsQuery (rslt q))+    `u`+    (nub $ concat $ map freevarsQuery (cond q))+freevarsQuery (QOp lhs op rhs) = nub (freevarsQuery lhs ++ freevarsQuery rhs)+freevarsQuery (QRecord fields) = concatMap (freevarsQuery . snd) fields+freevarsQuery _ = []++isQRecord (QRecord _) = True+isQRecord _ = False++-- | a groundQuery is a *real* SQL query--one without variables or appl'ns.+groundQuery :: Query -> Bool+groundQuery (qry@(Select _ _ _)) =+    all groundQueryExpr (cond qry) &&+    groundQueryExpr (rslt qry) &&+    isQRecord (rslt qry)+groundQuery (QUnion a b) = groundQuery a && groundQuery b+groundQuery (QExists qry) = groundQuery qry+groundQuery (QRecord fields) = all (groundQuery . snd) fields+groundQuery (QOp b1 _ b2) = groundQuery b1 && groundQuery b2+groundQuery (QNum _) = True+groundQuery (QBool _) = True+groundQuery (QField _ _) = True+groundQuery (QNot a) = groundQuery a++-- | a groundQueryExpr is an atomic-type expression.+groundQueryExpr :: Query -> Bool+groundQueryExpr (qry@(Select _ _ _)) = False+groundQueryExpr (QUnion a b) = False+groundQueryExpr (QExists qry) = groundQuery qry+groundQueryExpr (QRecord fields) = all (groundQueryExpr . snd) fields+groundQueryExpr (QOp b1 _ b2) = groundQueryExpr b1 && groundQueryExpr b2+groundQueryExpr (QNot a) = groundQueryExpr a+groundQueryExpr (QNum _) = True+groundQueryExpr (QBool _) = True+groundQueryExpr (QField _ _) = True+groundQueryExpr (QIf c a b) = all groundQueryExpr [c,a,b]++serialize :: Query -> String+serialize q@(Select _ _ _) =+    "select " ++ serializeRow (rslt q) +++    " from " ++ mapstrcat ", " (\(a, b, _) -> a ++ " as " ++ b) (tabs q) +++    " where " ++ if null (cond q) then+                     "true"+                 else mapstrcat " and " serializeAtom (cond q)+serialize (QUnion l r) =+    "(" ++ serialize l ++ ") union (" ++ serialize r ++ ")"++serializeRow (QRecord flds) =+    mapstrcat ", " (\(x, expr) -> serializeAtom expr ++ " as " ++ x) flds++serializeAtom (QNum i) = show i+serializeAtom (QBool b) = show b+serializeAtom (QNot expr) = "not(" ++ serializeAtom expr ++ ")"+serializeAtom (QOp l op r) = +    serializeAtom l ++ " " ++ serializeOp op ++ " " ++ serializeAtom r+serializeAtom (QField rec fld) = rec ++ "." ++ fld+serializeAtom (QIf cond l r) = +    "case when " ++ serializeAtom cond +++    " then " ++ serializeAtom l +++    " else " ++ serializeAtom r +++    " end)"+serializeAtom (QExists q) =+    "exists (" ++ serialize q ++ ")"++serializeOp Eq = "="+serializeOp Less = "<"+serializeOp Plus = "<"+serializeOp Minus = "<"+serializeOp Times = "<"+serializeOp Divide = "<"
+ Narc/SQL/Pretty.hs view
@@ -0,0 +1,39 @@+module Narc.SQL.Pretty where++import Narc.Pretty+import Narc.SQL+import Narc.Util (mapstrcat)++instance Pretty Query where+  pretty (Select{rslt=QRecord flds, tabs=tabs, cond=cond}) = +         "select " ++ mapstrcat ", " (\(alias, expr) -> +                                          pretty expr ++ " as " ++ alias)+                      flds ++ +         (if null tabs then "" else+         " from " ++ mapstrcat ", " (\(name, al, ty) -> name ++ " as " ++ al) +                         tabs) ++ +         " where " ++ pretty_cond cond+                   where pretty_cond [] = "true"+                         pretty_cond cond = mapstrcat " and " pretty cond+  pretty (QOp lhs op rhs) = pretty lhs ++ pretty op ++ pretty rhs+  pretty (QRecord fields) = "{"++ mapstrcat ", "+                               (\(lbl,expr) -> +                                    lbl ++ "=" ++ show expr) fields+                          ++ "}"+  pretty (QNum n) = show n+  pretty (QBool True) = "true"+  pretty (QBool False) = "false"+   +  pretty (QField a b) = a ++ "." ++ b++  pretty (QUnion a b) = pretty a ++ " union all " ++ pretty b+  pretty (QNot b) = "not " ++ pretty b+  pretty (QIf c t f) = "if " ++ pretty c ++ " then " ++ pretty t+                       ++ " else " ++ pretty f++-- Pretty-printing for Op, common to both AST and SQL languages.++instance Pretty Op where+  pretty Plus = " + "+  pretty Eq = " = "+  pretty Less = " < "
+ Narc/TermGen.hs view
@@ -0,0 +1,196 @@+module Narc.TermGen where++import Control.Monad hiding (when)++import Test.QuickCheck hiding (promote, Failure)++import Gensym+import QCUtils++import Narc.AST+import Narc.SQL+import Narc.Type as Type+import Narc.Util++--+-- QuickCheck term generators ------------------------------------------+--++smallIntGen :: Gen Int+smallIntGen = elements [0..5]++typeGen :: [TyVar] -> Int -> Gen Type+typeGen tyEnv size =+    oneof $ [return TBool,+             return TNum+            ] +++    [do x <- elements tyEnv; return $ TVar x | length tyEnv > 0] +++    whens (size > 0)+        [+         do s <- typeGen tyEnv (size-1)+            t <- typeGen tyEnv (size-1)+            return $ TArr s t,+         do t <- typeGen tyEnv (size-1)+            return $ TList t,+         do n <- smallIntGen :: Gen Int+            fields <- sequence [do t <- typeGen tyEnv (size-1)+                                   return ('f':show i, t) | i <- [0..n]]+            return $ TRecord fields+        ]++-- | Generate a random term, unlikely to be well-typed.+termGen :: [Var] -> Int -> Gen (Term ())+termGen fvs size = frequency $+    [(1,                    return (Unit, ())),+     (1, do b <- arbitrary; return (Bool b, ())),+     (1, do n <- arbitrary; return (Num n, ()))+    ]+    +++    (whens (not (null fvs)) [(3, do x <- elements fvs;+                                    return (Var x, ()))])+    +++    whens (size > 0) [+     (3, do x <- varGen+            n <- termGen (x:fvs) (size-1)+            return (Abs x n, ())),+     (6, do m <- termGen fvs (size-1)+            n <- termGen fvs (size-1)+            return $ (App m n, ())),+     (6, do m <- termGen fvs (size-1)+            f <- identGen+            return $ (Project m f, ())),+     (6, do m <- termGen fvs (size-1)+            return $ (Singleton m, ())),+     (18, do n <- smallIntGen+             tableName <- identGen+             fields <- sequence $ replicate n $+                       do name <- identGen+                          ty <- elements [TBool, TNum]+                          return (name, ty)+             return $ (Table tableName fields, ())),+     (9, do n <- smallIntGen+            fields <- sequence $ replicate n $+                      do name <- identGen+                         term <- termGen fvs (size-1)+                         return (name, term)+            return $ (Record fields, ())),+     (72, do x <- varGen  -- Overwhelmingly favor comprehensions when+                          -- we have enough size remaining, since+                          -- we'll be favoring other stuff when we run+                          -- out of size.+             l <- termGen fvs (size-1)+             m <- termGen (x:fvs) (size-1)+             return $ (Comp x l m, ()))+    ]++closedTermGen :: Int -> Gen (Term' (), ())+closedTermGen size = +    termGen [] size++oneofMaybe :: [Gen(Maybe a)] -> Gen (Maybe a)+oneofMaybe [] = return Nothing+oneofMaybe (x:xs) = do x' <- x+                       xs' <- oneofMaybe xs+                       case (x', xs') of+                         (Nothing, Nothing) -> return Nothing+                         _ -> oneof (map (return . Just) $ +                                         asList x' ++ asList xs')++-- Why isn't this bloody thing generating deconstructors??+typedTermGen :: TyEnv -> Type -> Int -> Gen (Term ())+typedTermGen env ty sz = +--    debug ("generating term (type " ++ show ty ++ ") at size " ++ show sz) $+    frequency (+    -- variables+    -- (NOTE: presently only gens vars that have ground type, sans quant'rs)+    [(2, return $ (Var x, ())) | (x, (xQs, xTy)) <- env,+                                 xQs == [] && xTy == ty] +++    -- constructors+    (case ty of+      TNum  -> [(1, do n <- arbitrary; return (Num n, ()))]+      TBool -> [(1, do b <- arbitrary; return (Bool b, ()))]+      TArr s t -> +          [(2, do x <- varGen +                  n <- typedTermGen ((x, ([], s)):(unassoc x env)) t decSz+                  return $ (Abs x n, ()))]+      TRecord fTys -> +          [(2, do fields <- forM fTys $ \(lbl, ty) ->+                              do m <- typedTermGen env ty decSz+                                 return (lbl, m)+                  return $ (Record fields, ()))]+      TList ty ->+          [(2, do m <- typedTermGen env ty decSz +                  return $ (Singleton m, ()))]+          ++ case ty of +                TRecord fTys ->+                  if not (and [isBaseTy ty | (_, ty) <- fTys]) then [] else+                  [(2, do tab <- identGen+                          return $ (Table ('T':tab) fTys, ()))]+                _ -> []+      _ -> error("Strange type while generating term: " ++ +                 show ty ++ " (size " ++ show sz ++ ")")+    ) +++    -- deconstructors+    if (sz <= 0) then [] else (+     [+      (10, do s <- typeGen [] (intSqrt sz)+              m <- typedTermGen env (TArr s ty) decSz+              n <- typedTermGen env s decSz+              return $ (App m n, ())),+      (10, do c <- typedTermGen env TBool decSz+              a <- typedTermGen env ty decSz+              b <- typedTermGen env ty decSz+              return $ (If c a b, ()))+     ] +++     -- Comprehension: a constructor and a destructor+     case ty of+      (TList _) ->+          [(20, do x <- varGen+                   s <- typeGen [] (intSqrt sz)+                   src <- typedTermGen env (TList s) decSz+                   let env' = Type.bind x ([], s) env+                   body <- typedTermGen env' ty decSz+                   return (Comp x src body, ()))+          ]+      _ -> []+    )+  )+  where decSz = max (sz-1) 0++closedTypedTermGen :: Type -> Int -> Gen (Term ())+closedTypedTermGen ty size = +--    let tyEnv = runErrorGensym makeInitialTyEnv in+    let tyEnv = [] in+    typedTermGen tyEnv ty size++dbTableTypeGen :: Gen Type+dbTableTypeGen = +    do n <- nonNegInt :: Gen Int+       ty <- elements [TBool, TNum]+       return $ TList (TRecord [('t': show i, ty) | i <- [0..n-1]])+++-- Generators++instance Arbitrary Op where+    arbitrary = oneof [return Eq, return Less]++listGen :: Int -> Gen a -> Gen [a]+listGen 0 gen = oneof [ return [], do x <- gen+                                      xs <- listGen 0 gen+                                      return (x : xs)]+listGen n gen = do x <- gen+                   xs <- listGen (n-1) gen+                   return (x : xs)++identCharGen :: Gen Char+identCharGen = oneof $ map return (['a'..'z'] ++ ['A'..'Z'] ++ ['_'])++identGen :: Gen String+identGen = listGen 1 identCharGen++varGen :: Gen String+varGen = (return ('x':)) `ap` identGen++pairGen :: Gen a -> Gen b -> Gen (a, b)+pairGen aGen bGen = do a <- aGen; b <- bGen; return (a, b)
+ Narc/Test.hs view
@@ -0,0 +1,82 @@+{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}++module Narc.Test where++import Prelude hiding (catch)+import Control.Monad.State hiding (when, join)+import Control.Monad.Error ({- Error(..), throwError, -} runErrorT)++import Test.QuickCheck hiding (promote, Failure)+import Test.HUnit hiding (State, assert)++import Gensym+import QCUtils++import Narc.AST+import Narc.Compile+import Narc.Failure+import Narc.SQL+import Narc.Type as Type+import Narc.TypeInfer+import Narc.TermGen++makeNormalizerTests :: ErrorGensym Test+makeNormalizerTests = +    do initialTyEnv <- makeInitialTyEnv +       return$ TestList +                 [TestCase $ unitAssert $ +                  let term = (Comp "x" (Table "foo" [("fop", TNum)], ())+                              (If (Bool True,())+                               (Singleton (Record+                                           [("f0", (Project (Var "x", ())+                                                    "fop",()))],()),())+                               (Singleton (Record +                                           [("f0", (Num 3, ()))], ()), ()), +                               ()), ()) in+                  let tyTerm = runErrorGensym $ infer $ term in+                  groundQuery $ compile initialTyEnv $ tyTerm+                 ]++unitTests :: ErrorGensym Test+unitTests = do normalizerTests <- makeNormalizerTests +               return $ TestList [tyCheckTests, normalizerTests, typingTest]++runUnitTests :: IO Counts+runUnitTests = runErrorGensym $ liftM runTestTT unitTests++--+-- Big QuickCheck properties+--++-- | Assertion that well-typed terms evaluate without throwing.+prop_eval_safe :: Property+prop_eval_safe = +    forAll dbTableTypeGen $ \ty ->+    forAll (sized (closedTypedTermGen ty)) $ \m ->+    case tryErrorGensym (infer m) of+      Left _ -> label "ill-typed" $ property True -- ignore ill-typed terms+                                                  -- but report their occurence.+      Right (m'@(_, ty)) -> +          isDBTableTy ty ==>+            let q = (compile [] $! m') in+            collect (sizeQuery q) $  -- NB: Counts sizes only up to ~100.+                    excAsFalse (q == q) -- Self-comparison forces the+                                        -- value (?) thus surfacing+                                        -- any @error@s that might be+                                        -- raised.++prop_typedTermGen_tyCheck :: Property+prop_typedTermGen_tyCheck =+  forAll (sized $ typeGen []) $ \ty ->+  forAll (sized $ typedTermGen (runErrorGensym makeInitialTyEnv) ty) $ \m ->+  case runGensym $ runErrorT $ infer m of+    Left _ -> False+    Right (_m', ty') -> isErrorMSuccess $ unify ty ty'++-- Main ----------------------------------------------------------------++main :: IO ()+main = do+  quickCheckWith tinyArgs prop_eval_safe+  _ <- runUnitTests+  return ()
+ Narc/Type.hs view
@@ -0,0 +1,245 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Narc.Type where++import Test.QuickCheck++import Gensym+import QCUtils++import Data.List ((\\))+import Control.Monad.State (State(..), get, put, evalState) -- TBD: use Gensym monad instead+import Control.Applicative ((<$>))+import Narc.Failure (Failure, fayl)+import Narc.Failure.QuickCheck+import Narc.Util (dom, rng, image, alistmap, sortAlist, onCorresponding,+                     disjointAlist, validEnv, eqUpTo)+import Narc.Var++type TyVar = Int++data Type = TBool | TNum | TString | TUnit | TList Type+          | TArr Type Type+          | TRecord [(String, Type)]+          | TVar TyVar+    deriving (Eq, Show)++type QType = ([TyVar], Type)++type TySubst = [(Int, Type)]++type TyEnv = [(Var, QType)]++-- Operations on types, rows and substitutions ------------------------++isBaseTy TBool = True+isBaseTy TNum  = True+isBaseTy TString  = True+isBaseTy _     = False++isTyVar (TVar _) = True+isTyVar _        = False++isDBRecordTy (TRecord fields) = all (isBaseTy . snd) fields+isDBRecordTy _                = False++isRecordTy (TRecord fields) = True+isRecordTy _                = False++isDBTableTy (TList ty) = isDBRecordTy ty+isDBTableTy _          = False++emptyTySubst :: (TySubst)+emptyTySubst = ([])++-- | ftvs: free type variables+ftvs TBool = []+ftvs TNum = []+ftvs TString = []+ftvs TUnit = []+ftvs (TList t) = ftvs t+ftvs (TArr s t) = ftvs s ++ ftvs t+ftvs (TRecord fields) = concat [ftvs t | (lbl, t) <- fields]+ftvs (TVar a) = [a]++numFtvs = length . ftvs++-- | ftvsSubst: the free type variables of a type substitution--that is,+-- the type variables free in the types in the range of the substitution.+ftvsSubst a = concatMap ftvs $ rng a++-- | occurs x ty: does variable x appear in type ty? (Note there are no+-- type-variable binders).+occurs x (TVar y) | x == y    = True+                  | otherwise = False+occurs x (TArr s t) = x `occurs` s || x `occurs` t+occurs x (TList t) = x `occurs` t+occurs x (TRecord t) = any (occurs x) (map snd t)+occurs x (TUnit) = False+occurs x (TBool) = False+occurs x (TNum) = False+occurs x (TString) = False++applyTySubst :: TySubst -> Type -> Type+applyTySubst subst (TUnit) = TUnit+applyTySubst subst (TBool) = TBool+applyTySubst subst (TNum) = TNum+applyTySubst subst (TString) = TString+applyTySubst subst (TVar a) = case lookup a subst of+                              Nothing -> TVar a+                              Just ty -> ty+applyTySubst subst (TArr a b) =+    TArr (applyTySubst subst a) (applyTySubst subst b)+applyTySubst subst (TList a) = TList (applyTySubst subst a)+applyTySubst subst (TRecord a) = TRecord (alistmap (applyTySubst subst) a)+++-- Type operations -----------------------------------------------------++instantiate (qs, ty) =+    do subst <- sequence [do y <- gensym ; return (q, TVar y) | q <- qs]+       return $ applyTySubst subst ty++{- | normalizeType:+   Renumber all the type variables in a normal way to allow+   comparing types.+-}+normalizeType :: Type -> State (Int, [(Int, Int)]) Type+normalizeType TBool = return TBool+normalizeType TNum = return TNum+normalizeType TString = return TString+normalizeType TUnit = return TUnit+normalizeType (TList ty) = TList <$> normalizeType ty+normalizeType (TRecord recTy) = undefined+normalizeType (TVar a) = do (ctr, env) <- Control.Monad.State.get+                            case lookup a env of+                              Nothing -> do put (ctr+1, (a, ctr):env)+                                            return $ TVar ctr+                              Just b -> return $ TVar b+normalizeType (TArr s t) =+    do s' <- normalizeType s+       t' <- normalizeType t+       return $ TArr s' t'++runNormalizeType ty = evalState (normalizeType ty) (0, [])++-- instanceOf: is there a substitution that turns ty2 into ty1? Useful in tests+instanceOf :: Type -> Type -> Failure ()+instanceOf ty1 (TVar x) = return ()+instanceOf TBool TBool = return ()+instanceOf TNum TNum = return ()+instanceOf TString TString = return ()+instanceOf (TArr s t) (TArr u v) = +    instanceOf t v >>+    instanceOf s u+instanceOf (TList a) (TList b) = instanceOf a b+instanceOf (TRecord a) (TRecord b) = +    let a' = sortAlist a +        b' = sortAlist b+    in+      do result <- sequence [if ax == bx then instanceOf ay by else fayl "Record mismatch"+                             | ((ax, ay), (bx, by)) <- zip a' b']+         return ()+instanceOf a b = fayl ""++unify :: Type -> Type -> Failure (TySubst)+unify s t | s == t = return ([])+unify (TVar x) t | not (x `occurs` t) = return ([(x, t)])+                 | otherwise = fayl("Occurs check failed on " ++ +                                    show (TVar x) ++ " and " ++ show t)+unify t (TVar x) | not (x `occurs` t) = return ([(x, t)])+                 | otherwise = fayl("Occurs check failed on " ++ +                                    show t ++ " and " ++ show (TVar x))+unify TBool TBool = return ([])+unify TNum TNum = return ([])+unify TString TString = return ([])+unify (TArr s t) (TArr u v) = +    do substSU <- unify s u+       substTV <- unify (applyTySubst substSU t)+                        (applyTySubst substSU v)+       composeTySubst [substTV, substSU]+unify (TList a) (TList b) = unify a b+unify (TRecord a) (TRecord b) = +    let a' = sortAlist a +        b' = sortAlist b+    in+      do substs <- sequence+                [if ax == bx then unify ay by else+                     fayl ("Record types " ++ show a' ++ +                           " and " ++ show b' ++ +                           " mismatched.")+                 | ((ax, ay), (bx, by)) <- zip a' b']+         let (tySubsts) = substs+         subst <- composeTySubst tySubsts+         return (subst)+unify a b = fayl("Type mismatch between " ++ +                 show a ++ " and " ++ show b)++unifyAll :: [Type] -> Failure TySubst+unifyAll [] = return ([])+unifyAll [x] = return ([])+unifyAll (x1:x2:xs) = do (tySubst) <- x1 `unify` x2+                         unifyAll (map (applyTySubst tySubst)+                                   (x2:xs))++composeTySubst :: [TySubst] -> Failure TySubst+composeTySubst [] = return $ ([])+composeTySubst subst =+    let (tySubsts) = subst in+    do addlSubsts <- sequence $+                         onCorresponding unifyAll $ concat tySubsts+       let (addlTySubsts) = addlSubsts+       let substs' = tySubsts ++ addlTySubsts+       let tySubst = flip foldr1 substs'+                 (\s1 s2 -> s1 ++ alistmap (applyTySubst s1) s2)+       if any (\(a,b) -> occurs a b) tySubst then +          fayl "Circular type substitution in composeTySubst" +        else +            return (tySubst)++prop_composeTySubst = +    forAll (genEnv 0) $ \a ->+    forAll (genEnv (length a)) $ \b ->+    forAll arbitrary $ \ty ->+    disjointAlist a b && validEnv a && validEnv b ==>+    (do ab <- composeTySubst[a, b]+        return $ applyTySubst ab ty)+    == (return $ (applyTySubst a $ applyTySubst b ty) :: Failure Type)++-- unused+disjoinSubst :: TySubst -> TySubst -> TySubst+disjoinSubst a b =+  [(image bx mapping, applyTySubst subst by) | (bx, by) <- b]+    where mapping = (dom b ++ ftvsSubst b) `zip`+                      ([0..] \\ (dom a ++ ftvsSubst a))+          subst = alistmap TVar mapping++instance Arbitrary Type where+    arbitrary = +        oneof+          [ return TBool+          , return TNum+          , return TString+          , do s <- arbitrary+               t <- arbitrary+               return (TArr s t)+          , do x <- posInt+               return (TVar x)+          ]++-- Check that unification produces a substitution which actually+-- unifies the two types. (Currently fails; something wrong with the way+-- substitutions are composed or not.)+prop_unify_apply_subst = +  forAll arbitrary $ \(a :: Type) ->+  forAll arbitrary $ \(b :: Type) -> +    collect (numFtvs a, numFtvs b) $+    failureToPropertyIgnoreFailure $+    do (subst) <- a `unify` b+       let e = applyTySubst subst a+       let f = applyTySubst subst b+       return $ eqUpTo runNormalizeType e f++-- { Typing environments } ---------------------------------------------++bind x v env = (x,v):env
+ Narc/TypeInfer.hs view
@@ -0,0 +1,233 @@+module Narc.TypeInfer where++import Data.Maybe (fromMaybe)+import Data.Either++import Control.Monad.State (lift)++import Test.HUnit++import Gensym+import Narc.AST+import Narc.Type+import Narc.Failure+import Narc.Debug (debug)++--+-- Type inference ------------------------------------------------------+--++tyCheckTerms env terms = +    do results <- sequence [tyCheck env term | term <- terms]+       let (tySubsts, terms') = unzip results+       let (terms'', termTys) = unzip terms'+       tySubst <- under $ composeTySubst tySubsts+       return (tySubst, terms')++-- | tyCheck env term infers a type for term in environment env.+-- The environment has type [(Var, QType)];+-- an entry (x, qty) indicates that variable x has the quantified type qty;+-- a QType (ys, ty) indicates the type "forall ys, ty".+tyCheck :: TyEnv -> Term a+        -> ErrorGensym (TySubst, Term Type)+tyCheck env (Unit, _) = +    do let ty = (TUnit)+       return (emptyTySubst, (Unit, ty))+tyCheck env (Bool b, _) = +    do let ty = (TBool)+       return (emptyTySubst, (Bool b, ty))+tyCheck env (Num n, _) = +    do let ty = (TNum)+       return (emptyTySubst, (Num n, ty))+tyCheck env (String s, _) = +    do let ty = (TString)+       return (emptyTySubst, (String s, ty))+tyCheck env (Table t tys, _) =+    do let ty = (TList (TRecord tys))+       return (emptyTySubst, (Table t tys, ty))+tyCheck env (Var x, _) =+    do let qTy = fromMaybe (error("Type error: no var " ++ x))+                 $ lookup x env+       ty <- lift $ instantiate qTy+       debug ("*** instantiated " ++ show qTy ++ " to " ++ show ty) $+        return (emptyTySubst, (Var x, (ty)))+tyCheck env (PrimApp fun args, _) = +    do (tySubst, args) <- tyCheckTerms env args+       return(tySubst, (PrimApp fun args, (TBool))) -- TBD+tyCheck env (Abs x n, _) = +    do argTyVar <- lift gensym+       (tySubst, n'@(_, (nTy))) <- +           tyCheck ((x, ([], TVar argTyVar)) : env) n+       let argTy = applyTySubst tySubst $ TVar argTyVar+       return(tySubst,+              (Abs x n', (TArr argTy nTy)))+tyCheck env (If c a b, _) =+    do (cTySubst, c'@(_, (cTy))) <- tyCheck env c+       (aTySubst, a'@(_, (aTy))) <- tyCheck env a+       (bTySubst, b'@(_, (bTy))) <- tyCheck env b+       cBaseTySubst <- under (unify cTy TBool)+       abTySubst <- under $ unify aTy bTy+       tySubst <- under $ composeTySubst+                             [aTySubst, bTySubst, cTySubst,+                              cBaseTySubst, abTySubst]+       let ty = applyTySubst tySubst bTy+       return (tySubst,+               (If c' a' b', (ty)))+tyCheck env (Nil, _) = +    do t <- lift gensym+       return (emptyTySubst, (Nil, (TList (TVar t))))+tyCheck env (Singleton m, _) =+    do (tySubst, m'@(_, (mTy))) <- tyCheck env m+       return (tySubst,+               (Singleton m', (TList mTy)))+tyCheck env (Union a b, _) =+    do (aTySubst, a'@(_, (aTy))) <- tyCheck env a+       (bTySubst, b'@(_, (bTy))) <- tyCheck env b+       abTySubst <- under $ unify aTy bTy+       tySubst <- under $ composeTySubst+                             [aTySubst, bTySubst, abTySubst]+       let ty = applyTySubst tySubst bTy+       return (tySubst,+               (Union a' b', (ty)))+tyCheck env (Record fields, _) =+    let (fieldNames, terms) = unzip fields in+    do (tySubst, terms) <- tyCheckTerms env terms+       let fieldTys = map snd terms+       return (tySubst,+               (Record (zip fieldNames terms),+                (TRecord [(name,ty)| (ty, name) <- zip fieldTys fieldNames])))+tyCheck env (Project m f, _) =+    do rowVar <- lift gensym; a <- lift gensym+       (tySubst, m'@(_, mTy)) <- tyCheck env m+       case mTy of+         TVar x ->     -- Note: bogus+                return (((x, TRecord [(f, TVar a)]):tySubst),+                        (Project m' f, (TVar a)))+         TRecord fieldTys ->+                case lookup f fieldTys of+                  Nothing -> fail("no field " ++ f ++ " in record " ++ +                                  show (strip m))+                  Just fieldTy ->+                      return (tySubst,+                              (Project m' f, fieldTy))+         _ -> fail("Project from non-record type.")+tyCheck env (App m n, _) = +    do a <- lift gensym; b <- lift gensym;+       (mTySubst, m'@(_, (mTy))) <- tyCheck env m+       (nTySubst, n'@(_, (nTy))) <- tyCheck env n+       let nTy' = applyTySubst mTySubst $ nTy+       let mTy' = applyTySubst nTySubst $ mTy+       subExprTySubst <- under $ composeTySubst [mTySubst, nTySubst]+       +       let mArrTy = TArr (nTy') (TVar b)+       mArrTySubst <- under $ unify mArrTy mTy'+       +       let resultTy = applyTySubst mArrTySubst $ TVar b+       +       tySubst <- under $ composeTySubst [mArrTySubst,+                                          subExprTySubst]+       +       return (tySubst,+               (App m' n', (resultTy)))++tyCheck env term@(Comp x src body, d) =+    do (substSrc, src') <- tyCheck env src+       let srcTy = typeAnno src'+       a <- lift gensym+       srcTySubst <- under $ unify (TList (TVar a)) srcTy+       let srcTy' = applyTySubst srcTySubst (TVar a)+       (substBody, body') <- tyCheck ((x, unquantType srcTy') : env) body+       let bodyTy = typeAnno body'+       resultSubst <- under $ composeTySubst [substSrc, substBody]+       return (resultSubst, (Comp x src' body', bodyTy))++unquantType ty = ([], ty)++typeAnno :: Term Type -> Type+typeAnno (_, ty) = ty++makeInitialTyEnv :: ErrorGensym [(String, QType)]+makeInitialTyEnv = return []++infer :: Term a -> ErrorGensym TypedTerm -- FIXME broken, discards subst'n+infer term =+    do initialTyEnv <- makeInitialTyEnv+       (_, term') <-+        --    runErrorGensym $ +               tyCheck initialTyEnv term+       return term'++infer' :: Term' a -> ErrorGensym TypedTerm+infer' term = infer (term, undefined)++runInfer = runErrorGensym . infer++runTyCheck env m = runErrorGensym $ +    do initialTyEnv <- makeInitialTyEnv+       (subst, m') <- tyCheck (initialTyEnv++env) m+       return $ retagulate (applyTySubst subst . snd) m'++inferTys :: Term () -> ErrorGensym Type+inferTys m = +    do (_, (ty)) <- infer m+       return (ty)++inferType :: Term () -> ErrorGensym Type+inferType m = infer m >>= (return . snd)++runInferType = runErrorGensym . inferType++inferType' :: Term' () -> ErrorGensym Type+inferType' m = infer' m >>= (return . snd)++-- UNIT TESTS ----------------------------------------------------------++unitAssert b = assertEqual "." b True++tyCheckTests =+    TestList ["Simple application of id to table" ~:+                     (runErrorGensym $ +                       inferTys (App (Abs "x" (Var "x", ()), ())+                              (Table "wine" [], ()), ()))+                       ~?= (TList (TRecord [])),+              "Curried application of id to table" ~:+                     (runErrorGensym . inferTys)+                     (App (App+                              (Abs "x" (Abs "y" (App (Var "x", ())+                                                     (Var "y", ()), ()), ()), ())+                                 (Abs "x" (Var "x", ()), ()), ())+                                 (Table "wine" [], ()), ())+                       ~?= (TList (TRecord [])),+              "Curried application, de/reconstructing record" ~:+                     (runErrorGensym . inferTys) +                     (App (App+                      (Abs "f" (Abs "x" (App (Var "f",()) (Var "x",()),()),()),())+                      (Abs "x"+                       (Record[("baz", (Project(Var "x",()) "foo", ()))],+                        ()),+                       ()), ())+                      (Record [("foo", (Num 47, ()))], ()), ())+                      ~?= (TRecord[("baz", TNum)]),+              "omega" ~:+                    unitAssert $ isError $+                      (tryErrorGensym . inferType)+                      (Abs "x" (App (Var "x", ()) (Var "x", ()), ()), ())+                  ]++typingTest1 = +  let idTy = (TArr (TVar 9) (TVar 9)) in+  let concatMapTy = (TArr (TArr (TVar 2) (TList (TVar 3)))+                     (TArr (TList (TVar 2))+                               (TList (TVar 3)))) in+  let Right mArrSubst = unify concatMapTy  (TArr (TVar 4) (TVar 5)) in+  let argTy = applyTySubst mArrSubst (TVar 4) in+             -- TArr (TVar 2) ([],Just 0) (TList (TVar 3))+  let Right funcArgSubst = unify argTy idTy in+  let resultTy = (applyTySubst funcArgSubst $ applyTySubst mArrSubst (TVar 5)) +  in+  (resultTy, funcArgSubst,+   case resultTy of+   TArr (TList (TList (TVar a))) (TList (TVar b)) -> a == b)++typingTest = let (_,_,x) = typingTest1 in +             TestCase (unitAssert x)
+ Narc/Util.hs view
@@ -0,0 +1,111 @@+module Narc.Util where++import Data.Maybe (fromJust, isJust)+import Data.List as List ((\\), nub, intersperse, groupBy, sortBy, sort)++--+-- List Utilities+--++dom alist = map fst alist+rng alist = map snd alist++collate proj = groupBy (\x y -> proj x == proj y) . +               sortBy (\x y -> proj x `compare` proj y)++sortAlist :: [(String, b)] -> [(String, b)]+sortAlist = sortBy (\a b -> fst a `compare` fst b)++cross f g (x,y) = (f x, g y)++onRight f = cross id f+onLeft f = cross f id++-- | shadow: given two alists, return the elements of the first that+-- are NOT mapped by the second+shadow as bs = [(a,x) | (a,x) <- as, a `notElem` domBs]+    where domBs = map fst bs++-- | Tests that an alist or environment is well-formed: that its first+-- | components are all unique.+validEnv xs = length (nub $ map fst xs) == length xs++mr agg xs = map reduceGroup (collate fst xs)+    where reduceGroup xs = let (as, bs) = unzip xs in+                             (the as, agg bs)+          the xs | allEq xs = head xs++onCorresponding :: Ord a => ([b]->c) -> [(a,b)] -> [c]+onCorresponding agg xs = map reduceGroup (collate fst xs)+    where reduceGroup xs = agg $ map snd xs++($>) x f = f x++image x = fromJust . lookup x++maps x = isJust . lookup x++intSqrt :: Integral a => a -> a+intSqrt = floor . sqrt . fromIntegral++unassoc a = filter ((/= a) . fst)++nubassoc [] = []+nubassoc ((x,y):xys) = (x,y) : (nubassoc $ unassoc x xys)++graph f xs = [(x, f x) | x <- xs]+alistmap f = map (\(a, b) -> (a, f b))++bagEq a b = a \\ b == [] && b \\ a == []++setEq a b = (nub a) `bagEq` (nub b)++u a b = nub (a ++ b)++contains a b = null(b \\ a)++setMinus xs ys = nub $ sort $ xs \\ ys++(\\\) xs ys = setMinus xs ys++allEq [] = True+allEq (x:xs) = all (== x) xs++disjoint :: Eq a => [a] -> [a] -> Bool+disjoint xs ys = not (any (\x-> any (==x) ys) xs)++disjointAlist xs ys = disjoint (map fst xs) (map fst ys)+-- disjointAlist [] _ = True+-- disjointAlist _ [] = True+-- disjointAlist xs ((a,b):ys) =+--     (not $ any ((== a) . fst) xs) && disjointAlist xs ys++-- | Convert a maybe to a zero-or-one-element list.+asList :: Maybe a -> [a]+asList Nothing = []+asList (Just x) = [x]++isRight :: Either a b -> Bool+isRight (Right _) = True+isRight (Left _ ) = False++isLeft :: Either a b -> Bool+isLeft (Left _) = True+isLeft (Right _ ) = False++-- | zipAlist: given two alists with the same domain,+-- returns an alist mapping each of those domain values to+-- the pair of the two corresponding values from the given lists.+zipAlist xs ys = +    let xsys = zip (sortAlist xs) (sortAlist ys) in+    if not $ and [x == y | ((x, a), (y, b)) <- xsys] then +        error "alist mismatch in zipAlist"+    else [(x, (a, b)) | ((x, a), (y, b)) <- xsys]++-- | mapstrcat: transform a list to one of strings, with a given+-- | function, and join these together with some `glue' string.+mapstrcat :: String -> (a -> String) -> [a] -> String+mapstrcat glue f xs = concat $ List.intersperse glue (map f xs)++-- Functional utilities+eqUpTo f x y = f x == f y
+ Narc/Var.hs view
@@ -0,0 +1,4 @@+module Narc.Var where++type Var = String+
+ QCUtils.hs view
@@ -0,0 +1,192 @@+{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}++module QCUtils where++import Prelude hiding (catch)+import Test.QuickCheck+import Control.Exception+import Foreign (unsafePerformIO)++import System.Random++{- Wrappers for detecting exceptions -}++-- | @propertyDefined x@ is a property asserting that @x@ can be+-- | forced without error.+propertyDefined :: a -> Property+propertyDefined exp = unsafePerformIO $ +                      catch (do x <- evaluate exp+                                return $ property True)+                            (\(exc::SomeException) -> return $ property False)++-- | @excAsFalse x@ is a property that acts like @x@, except that it+-- | is @False@ when @x@ would throw an exception (and never throws an+-- | exception itself).+excAsFalse :: Testable a => a -> Property+excAsFalse exp = unsafePerformIO $ +                     catch (do x <- evaluate exp+                               return $ property x)+                           (\(exc::SomeException) -> return $ property False)++-- | Convert an arbitrary value into a @Maybe@ by forcing it,+-- | catching errors and treating them as @Nothing@.+excAsNothing :: a -> Maybe a+excAsNothing exp = unsafePerformIO $ +                     catch (do x <- evaluate exp+                               return $ Just x)+                           (\(exc::SomeException) -> return Nothing)++-- | A predicate asserting that forcing a thunk produces an error+-- | (useful for tests that want to ensure error is thrown).+throws :: a -> Bool+throws exp = unsafePerformIO $ +             catch (do !x <- evaluate exp+                       return $ False)+                   (\(exc::SomeException) -> return True)++-- | Compare two functions at a particular input, incl. error+-- behavior.+f_equal x f g = (excAsNothing $ f x) == (excAsNothing $ g x)++{- Some simple generators -}++arbChar :: Gen Char+arbChar = elements $ ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_', ' ', '!']++arbLetter :: Gen Char+arbLetter = elements $ ['a'..'z'] ++ ['A'..'Z'] ++arbWordChar :: Gen Char+arbWordChar = frequency [(1, elements $ ['a'..'z'] ++ ['A'..'Z']),+                         (1, elements ['_'])]+++arbStringLen :: Gen Char -> Int -> Gen String+arbStringLen charGen 0 = return ""+arbStringLen charGen n = do str <- arbStringLen charGen (n-1)+                            ch <- charGen+                            return $ ch : str++-- | arbString: Generate a string of some length between 0 and 6, each length +-- with equal probability+arbString charGen = frequency [(1, arbStringLen charGen len)| len <- [0..6]]++arbStringSized charGen = sized (\n -> arbStringLen charGen n)++genIntLt n = elements [0..n-1]++vecTor :: Int -> Gen a -> Gen [a]+vecTor n _ | n < 0 = error "vector with negative # of elements"+vecTor 0 gen = return []+vecTor n gen = do x <- gen; xs <- vecTor (n-1) gen; return $ x : xs++posInt :: (Num a, Arbitrary a) => Gen a+posInt = fmap ((+1) . abs) arbitrary++nonNegInt :: (Num a, Arbitrary a) => Gen a+nonNegInt = fmap abs arbitrary++expIntGen n = frequency [(1, return n), (1, expIntGen (n+1))]++-- Combinators for writing conditional generators++whens p e = if p then e else []++{- Configurations for small, big, and huge test runs -}++small = stdArgs++big = Args {+    maxSuccess = 1000,+    maxDiscard = 1000,+    maxSize = 12,+    replay = Nothing,+    chatty = False+  }++huge = Args {+    maxSuccess = 10000,+    maxDiscard =  5000,+    maxSize = 20,+    replay = Nothing,+    chatty = False+  }++{- General list functions -}++histogram [] result = result+histogram (x : xs) result =+    histogram xs (incLookup x result)  +    where incLookup x [] = [(x, 1)]+          incLookup x ((y, yN):ys) | x == y    = (y,yN+1) : ys+                                   | otherwise = (y,yN)   : (incLookup x ys)++subsets [] = [[]]+subsets (x:xs) = +    let xsSubsets = subsets xs in+    map (x:) xsSubsets ++ xsSubsets++chooseSubset [] n = []+chooseSubset (x:xs) 0 = []+chooseSubset (x:xs) n = if n `mod` 2 == 1 then x : chooseSubset xs (n `div` 2)+                        else chooseSubset xs (n `div` 2)++arbSubset xs = do n <- posInt :: Gen Int+                  return $ chooseSubset xs n++genEnv :: (Arbitrary a, Num a, Enum a, Arbitrary b) => a -> Gen [(a, b)]+genEnv min = +    do n <- arbitrary+       sequence [do ty <- arbitrary; return (i, ty)+                 | i <- [min..min+pred(abs n)]]++failProp = property False++ignore = False ==> (undefined::Bool)++-- QuickCheck settings -------------------------------------------------++tinyArgs :: Args+tinyArgs = Args {+    maxSuccess = 100,+    maxDiscard = 100,+    maxSize = 8,+    replay = Nothing,+    chatty = False+  }++verySmallArgs :: Args+verySmallArgs = Args {+    maxSuccess = 1000,+    maxDiscard = 1000,+    maxSize = 12,+    replay = Nothing,+    chatty = False+  }++smallArgs :: Args+smallArgs = Args {+    maxSuccess = 10000,+    maxDiscard = 10000,+    maxSize = 16,+    replay = Nothing,+    chatty = False+  }++mediumArgs :: Args+mediumArgs = Args {+    maxSuccess = 100,+    maxDiscard = 100,+    maxSize = 100,+    replay = Nothing,+    chatty = False+  }++bigArgs :: Args+bigArgs = Args {+    maxSuccess = 1000,+    maxDiscard = 1000,+    maxSize = 500,+    replay = Nothing,+    chatty = False+  }
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ narc.cabal view
@@ -0,0 +1,61 @@+-- narc.cabal auto-generated by cabal init. For additional options,+-- see+-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr.+-- The name of the package.+Name:                narc++-- The package version. See the Haskell package versioning policy+-- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for+-- standards guiding when and how versions should be incremented.+Version:             0.1++-- A short (one-line) description of the package.+Synopsis:            Query SQL databases using Nested Relational Calculus embedded in Haskell.++-- A longer description of the package.+-- Description:         ++-- URL for the project homepage or repository.+Homepage:            http://ezrakilty.net/projects/narc++-- The license under which the package is released.+License:             BSD3++-- The file containing the license text.+License-file:        LICENSE++-- The package author(s).+Author:              Ezra e. k. Cooper++-- An email address to which users can send suggestions, bug reports,+-- and patches.+Maintainer:          ezra@ezrakilty.net++-- A copyright notice.+-- Copyright:           ++Category:            Database++Build-type:          Simple++-- Extra files to be distributed with the package, such as examples or+-- a README.+-- Extra-source-files:  ++-- Constraint on the version of Cabal needed to build this package.+Cabal-version:       >=1.2+++Library+  -- Modules exported by the library.+  Exposed-modules:     Narc, Narc.AST, Narc.Common, Narc.Compile, Narc.Eval, Narc.Failure, Narc.Pretty, Narc.Rewrite, Narc.SQL, Narc.Test, Narc.Type, Narc.TypeInfer, Narc.Util, Narc.AST.Pretty, Narc.Failure.QuickCheck, Narc.SQL.Pretty, Narc.HDBC+  +  -- Packages needed in order to build this package.+  Build-depends: base >=4 && < 5, HUnit, QuickCheck, mtl, random, HDBC+  +  -- Modules not exported by this package.+  Other-modules:       Gensym, QCUtils, Narc.TermGen, Narc.Var, Narc.Contract, Narc.Debug+  +  -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.+  -- Build-tools:         +