More cleanup. #148

Author: epost

src/Language/CQL/Common.hs

@@ -65,15 +65,16 @@ fromListAccum ((k,v):kvs) = Map.insert k op (fromListAccum kvs)
     op = maybe (Set.singleton v) (Set.insert v) (Map.lookup k r)
     r  = fromListAccum kvs
 
-fromList'' :: (Show k, Ord k) => [k] -> Err (Set k)
-fromList'' [] = return Set.empty
-fromList'' (k:l) = do
-  l' <- fromList'' l
+-- | Converts a 'List' to a 'Set', returning an error when there are duplicate bindings.
+toSetSafely :: (Show k, Ord k) => [k] -> Err (Set k)
+toSetSafely [] = return Set.empty
+toSetSafely (k:l) = do
+  l' <- toSetSafely l
   if Set.member k l'
   then Left $ "Duplicate binding: " ++ show k
   else pure $ Set.insert k l'
 
--- | Converts a map to a finite list, returning an error when there are duplicate bindings.
+-- | Converts an association list to a 'Map', returning an error when there are duplicate bindings.
 toMapSafely :: (Show k, Ord k) => [(k,v)] -> Err (Map k v)
 toMapSafely [] = return Map.empty
 toMapSafely ((k,v):l) = do

src/Language/CQL/Instance.hs

@@ -886,4 +886,4 @@ prettyEntityTable alg@(Algebra sch en' _ _ _ _ _ _ _) es =
     prettyAtt :: x -> (att, ty) -> String
     prettyAtt x (att,_) = prettyTerm $ aAtt alg att x
 
-    prettyTerm = show
+    prettyTerm = show

src/Language/CQL/Typeside.hs

@@ -39,6 +39,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 
 module Language.CQL.Typeside where
 import           Control.DeepSeq
+import           Data.Bifunctor        (first)
 import           Data.List             (nub)
 import           Data.Map.Strict       hiding (foldr)
 import qualified Data.Map.Strict       as Map
@@ -88,13 +89,15 @@ typecheckTypeside = typeOfCol . tsToCol
 
 -- | Converts a typeside to a collage.
 tsToCol :: (Ord var, Ord ty, Ord sym) => Typeside var ty sym -> Collage var ty sym Void Void Void Void Void
-tsToCol (Typeside t s e _) = Collage e' t Set.empty s Map.empty Map.empty Map.empty Map.empty
-  where e' = Set.map (\(g,x)->(Map.map Left g, x)) e
+tsToCol (Typeside tys syms eqs _) =
+  Collage (leftify eqs) tys Set.empty syms mempty mempty mempty mempty
+  where
+    leftify = Set.map (first (fmap Left))
 
 data TypesideEx :: * where
   TypesideEx
-    :: forall var ty sym. (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym]) =>
-    Typeside var ty sym
+    :: forall var ty sym. (MultiTyMap '[Show, Ord, Typeable, NFData] '[var, ty, sym])
+    => Typeside var ty sym
     -> TypesideEx
 
 instance NFData TypesideEx where
@@ -119,42 +122,50 @@ data TypesideRaw' = TypesideRaw'
   , tsraw_imports :: [TypesideExp]
   } deriving (Eq, Show)
 
+
 evalTypesideRaw :: Options -> TypesideRaw' -> [TypesideEx] -> Err TypesideEx
-evalTypesideRaw ops t a' = do
-  a <- doImports a'
-  r <- evalTypesideRaw' t a
-  l <- toOptions ops $ tsraw_options t
-  p <- createProver (tsToCol r) l
-  pure $ TypesideEx $ Typeside (tys r) (syms r) (eqs r) (f p)
+evalTypesideRaw opts tsRaw imports = do
+  imports' <- doImports imports
+  ts       <- evalTypesideRaw' tsRaw imports'
+  opts'    <- toOptions opts $ tsraw_options tsRaw
+  prover   <- createProver (tsToCol ts) opts'
+  let eq   =  \ctx -> prove prover (Map.map Left ctx)
+  pure $ TypesideEx $ Typeside (tys ts) (syms ts) (eqs ts) eq
   where
-    f p ctx = prove p (Map.map Left ctx)
     doImports :: forall var ty sym. (Typeable var, Typeable ty, Typeable sym) => [TypesideEx] -> Err [Typeside var ty sym]
-    doImports [] = return []
-    doImports (TypesideEx ts : r) = case cast ts of
-      Nothing  -> Left "Bad import"
-      Just ts' -> do { r'  <- doImports r ; return $ ts' : r' }
-
-evalTypesideRaw' :: TypesideRaw'  -> [Typeside Var Ty Sym] -> Err (Typeside Var Ty Sym)
-evalTypesideRaw' (TypesideRaw' ttys tsyms teqs _ _) is = do
-  tys'  <- fromList''  ttys
-  syms' <- toMapSafely   tsyms
+    doImports []                    = return []
+    doImports (TypesideEx imp:imps) = do
+      imp'  <- note "Bad import" $ cast imp
+      imps' <- doImports imps
+      return $ imp' : imps'
+
+evalTypesideRaw' :: TypesideRaw' -> [Typeside Var Ty Sym] -> Err (Typeside Var Ty Sym)
+evalTypesideRaw' (TypesideRaw' ttys tsyms teqs _ _) importedTys = do
+  tys'  <- toSetSafely ttys
+  syms' <- toMapSafely tsyms
   eqs'  <- evalEqs (addImportedSyms syms') teqs
-  return $ Typeside (Set.union imported_tys' tys') (addImportedSyms syms') (Set.union imported_eqs eqs') undefined -- leave prover blank
+  return $ Typeside (Set.union importedTys' tys') (addImportedSyms syms') (Set.union importedEqs eqs') prover
   where
-    imported_tys' = foldr Set.union Set.empty $ fmap tys is
-    addImportedSyms syms' = foldr (\(f',(s,t)) m -> Map.insert f' (s,t) m) syms' $ concatMap (Map.toList . syms) is
-    imported_eqs = foldr Set.union Set.empty $ fmap eqs is
+    prover                = undefined -- intentionally left blank; is there a less explosive way to do this?
+    importedTys'          = foldMap tys importedTys
+    importedEqs           = foldMap eqs importedTys
+    addImportedSyms syms' = foldr (\(f',(s,t)) m -> Map.insert f' (s,t) m) syms' $ concatMap (Map.toList . syms) importedTys
+
     evalEqs _ [] = pure Set.empty
     evalEqs syms' ((ctx, lhs, rhs):eqs') = do
-      ctx' <- check syms' ctx lhs rhs
+      ctx' <- check    syms' ctx  lhs rhs
       lhs' <- evalTerm syms' ctx' lhs
       rhs' <- evalTerm syms' ctx' rhs
-      rest <- evalEqs syms' eqs'
+      rest <- evalEqs  syms' eqs'
       pure $ Set.insert (ctx', EQ (lhs', rhs')) rest
-    evalTerm _ ctx (RawApp v []) | Map.member v ctx = pure $ Var v
-    evalTerm syms' ctx (RawApp v l) = do { l' <- mapM (evalTerm syms' ctx) l ; pure $ Sym v l' }
+
+    evalTerm :: Monad m => t -> Ctx String a -> RawTerm -> m (Term String ty String en fk att gen sk)
+    evalTerm _     ctx (RawApp v []) | Map.member v ctx = pure $ Var v
+    evalTerm syms' ctx (RawApp v l)                     = Sym v <$> mapM (evalTerm syms' ctx) l
+
     check _ [] _ _ = pure Map.empty
     check syms' ((v,t):l) lhs rhs = do {x <- check syms' l lhs rhs; t' <- infer v t syms' lhs rhs; pure $ Map.insert v t' x}
+
     infer _ (Just t) _ _ _  = return t
     infer v _ syms' lhs rhs = case (t1s, t2s) of
       ([t1]       , [t2]       ) -> if t1 == t2 then return t1 else Left $ "Type mismatch on " ++ show v ++ " in " ++ show lhs ++ " = " ++ show rhs ++ ", types are " ++ show t1 ++ " and " ++ show t2
@@ -166,6 +177,7 @@ evalTypesideRaw' (TypesideRaw' ttys tsyms teqs _ _) is = do
       where
         t1s = nub $ typesOf v syms' lhs
         t2s = nub $ typesOf v syms' rhs
+
     typesOf _ _     (RawApp _  []) = []
     typesOf v syms' (RawApp f' as) = concatMap fn $ zip as $ maybe [] fst $ Map.lookup f' syms'
       where
@@ -195,17 +207,18 @@ sqlTypeNames =
   , "Real"
   , "Smallint", "String"
   , "Text", "Time", "Timestamp", "Tinyint"
-  , "Varbinary", "Varchar" ]
+  , "Varbinary", "Varchar"
+  ]
 
 -----------------------------------------------------------------------------------------------------------
 -- Expression syntax
 
--- there are practical haskell type system related reasons to not want this to be a gadt
+-- There are practical haskell type system related reasons to not want this to be a GADT.
 data TypesideExp where
-  TypesideVar :: String -> TypesideExp
-  TypesideInitial :: TypesideExp
-  TypesideRaw :: TypesideRaw' -> TypesideExp
-  TypesideSql :: TypesideExp
+  TypesideVar     :: String       -> TypesideExp
+  TypesideInitial ::                 TypesideExp
+  TypesideRaw     :: TypesideRaw' -> TypesideExp
+  TypesideSql     ::                 TypesideExp
 
 deriving instance Eq TypesideExp
 deriving instance Show TypesideExp
@@ -217,7 +230,6 @@ instance Deps TypesideExp where
     TypesideSql                          -> []
     TypesideRaw (TypesideRaw' _ _ _ _ i) -> concatMap deps i
 
-
 getOptionsTypeside :: TypesideExp -> [(String, String)]
 getOptionsTypeside x = case x of
   TypesideSql                          -> []