Allow type annotations on expressions (#60)

* compiler: wip - allow type annotations on exprs

[skip ci] it won't pass!

* compiler: mostly working now

* cogent: use type annotation for #31.

reenable tc test in ci

.travis.yml

@@ -82,7 +82,7 @@ script:
 - echo 'Installing Cogent'
 - cabal --ignore-sandbox install
 - echo 'Running tests'
-  # - make test-tc
+- make test-tc
   # - make test-ds
   # - make test-an
   # - make test-mn

cogent/src/Cogent/Parser.hs

@@ -148,47 +148,67 @@ basicExpr' = avoidInitial >> buildExpressionParser
             , [binary ">>" AssocLeft, binary "<<" AssocLeft]
             , [binary "&&" AssocRight]
             , [binary "||" AssocRight]
-            ] term <?> "basic expression"
+            ] annot <?> "basic expression"
   where binary name = Infix (reservedOp name *> pure (\a b -> LocExpr (posOfE a) (PrimOp name [a,b])))
 
-        term = avoidInitial >> (LocExpr <$> getPosition <*>
-                  (var <$> optionMaybe (reserved "inline")
-                       <*> variableName
-                       <*> optionMaybe (brackets (commaSep1 ((char '_' >> return Nothing)
-                                                         <|> (Just <$> monotype))))
-               <|> BoolLit <$> boolean
-               <|> Con <$> typeConName <*> many term
-               <|> IntLit <$> natural
-               <|> CharLit <$> charLiteral
-               <|> StringLit <$> stringLiteral
-               <|> tuple <$> parens (commaSep $ expr 1)
-               <|> UnboxedRecord <$ reservedOp "#" <*> braces (commaSep1 recordAssignment)))
-            <?> "term"
-        var Nothing  v Nothing = Var v
-        var (Just _) v Nothing = TypeApp v [] Inline
-        var Nothing  v (Just ts) = TypeApp v ts NoInline
-        var (Just _) v (Just ts) = TypeApp v ts Inline
-        tuple [] = Unitel
-        tuple [e] = exprOfLE e
-        tuple es  = Tuple es
-        recordAssignment = (\p n m -> (n, fromMaybe (LocExpr p (Var n)) m))
-                        <$> getPosition <*> variableName <*> optionMaybe (reservedOp "=" *> expr 1)
-                        <?> "record assignment"
-        wildcard = reservedOp ".." >> return Nothing
-        recAssign = Just <$> recordAssignment
-        recAssignsAndOrWildcard = ((:[]) <$> wildcard)
-                              <|> ((:) <$> recAssign <*> ((++) <$> many (try (comma >> recAssign)) <*> (liftM maybeToList . optionMaybe) (comma >> wildcard)))
-
-expr m = do avoidInitial; LocExpr <$> getPosition <*>
-                 (Let <$ reserved "let" <*> bindings <* reserved "in" <*> expr m
-              <|> If  <$ reserved "if" <*> expr m <*> many (reservedOp "!" >> variableName)
-                      <* reserved "then" <*> expr m <* reserved "else" <*> expr m)
-    <|> matchExpr m
-    <?> "expression"
+term = avoidInitial >> (LocExpr <$> getPosition <*>
+          (var <$> optionMaybe (reserved "inline")
+               <*> variableName
+               <*> optionMaybe (brackets (commaSep1 ((char '_' >> return Nothing)
+                                                 <|> (Just <$> monotype))))
+       <|> BoolLit <$> boolean
+       <|> Con <$> typeConName <*> many term
+       <|> IntLit <$> natural
+       <|> CharLit <$> charLiteral
+       <|> StringLit <$> stringLiteral
+       <|> tuple <$> parens (commaSep $ expr 1)
+       <|> UnboxedRecord <$ reservedOp "#" <*> braces (commaSep1 recordAssignment)))
+    <?> "term"
+
+var Nothing  v Nothing = Var v
+var (Just _) v Nothing = TypeApp v [] Inline
+var Nothing  v (Just ts) = TypeApp v ts NoInline
+var (Just _) v (Just ts) = TypeApp v ts Inline
+
+tuple [] = Unitel
+tuple [e] = exprOfLE e
+tuple es  = Tuple es
+
+recordAssignment = (\p n m -> (n, fromMaybe (LocExpr p (Var n)) m))
+                <$> getPosition <*> variableName <*> optionMaybe (reservedOp "=" *> expr 1)
+                <?> "record assignment"
+
+wildcard = reservedOp ".." >> return Nothing
+
+recAssign = Just <$> recordAssignment
+
+recAssignsAndOrWildcard = ((:[]) <$> wildcard)
+                      <|> ((:) <$> recAssign
+                               <*> ((++) <$> many (try (comma >> recAssign))
+                                         <*> (liftM maybeToList . optionMaybe) (comma >> wildcard)))
+
+expr m = try (expr' m) <|> annot
+
+expr' m = do avoidInitial
+             LocExpr <$> getPosition <*>
+                  (Let <$ reserved "let" <*> bindings <* reserved "in" <*> expr m
+               <|> try (If <$ reserved "if" <*> parens (expr m) <*> many (reservedOp "!" >> variableName)
+                           <* reserved "then" <*> expr m <* reserved "else" <*> expr m)
+               <|> If  <$ reserved "if" <*> expr' m <*> many (reservedOp "!" >> variableName)
+                       <* reserved "then" <*> expr m <* reserved "else" <*> expr m)
+          <|> matchExpr m
+          <?> "expression"
   where binding = Binding <$> irrefutablePattern <*> optionMaybe (reservedOp ":" *> monotype)
                           <*  reservedOp "=" <*> expr 1 <*> many (reservedOp "!" >> variableName)
         bindings = binding `sepBy1` reserved "and"
 
+annot = do avoidInitial
+           p <- getPosition
+           e <- term
+           mt <- optionMaybe (reservedOp ":" >> monotype)
+           case mt of Nothing -> return e
+                      Just t  -> return $ LocExpr p (Annot e t)
+
 
 -- monotype ::= typeA1 ("->" typeA1)?
 -- typeA1   ::= Con typeA2*

cogent/src/Cogent/PrettyPrint.hs

@@ -119,7 +119,16 @@ instance ExprType (Expr t p ip e) where
   levelExpr (StringLit {}) = 0
   levelExpr (Tuple {}) = 0
   levelExpr (Unitel) = 0
-  levelExpr _ = 100
+  levelExpr (Con {}) = 1
+  levelExpr (Annot {}) = 50
+  levelExpr (UnboxedRecord {}) = 100
+  levelExpr (Put {}) = 100
+  levelExpr (TypeApp {}) = 100
+  levelExpr (Upcast {}) = 100
+  levelExpr (Seq {}) = 100
+  levelExpr (Match {}) = 100
+  levelExpr (If {}) = 100
+  levelExpr (Let {}) = 100
   isVar (Var n) s = (n == s)
   isVar _ _ = False
 
@@ -313,6 +322,7 @@ instance (ExprType e, Pretty t, Pretty p, PatnType ip, Pretty ip, Pretty e) => P
                                              <$> vsep (map ((keyword "and" <+>) . indent . pretty) bs)
                                              <$> keyword "in" <+> indent (pretty e)
   pretty (Put e fs)          = pretty' 1 e <+> record (map handlePutAssign fs)
+  pretty (Annot e t)         = pretty' 50 e <+> symbol ":" <+> pretty t
 
 instance Pretty RawExpr where
   pretty (RE e) = pretty e

cogent/src/Cogent/Surface.hs

@@ -72,6 +72,7 @@ data Expr t p ip e = PrimOp OpName [e]
                    | Upcast e
 --                   | Widen  e
                    | Put e [Maybe (FieldName, e)]  -- Note: `Nothing' will be desugared to `Just' in TypeCheck / zilinc
+                   | Annot e t
                    deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
 
 type Banged = Bool
@@ -182,6 +183,7 @@ instance Traversable (Flip (Expr t p) e) where  -- ip
   traverse _ (Flip (UnboxedRecord es))  = pure $ Flip (UnboxedRecord es)
   traverse _ (Flip (Put e es))          = pure $ Flip (Put e es)
   traverse _ (Flip (Upcast e))          = pure $ Flip (Upcast e)
+  traverse _ (Flip (Annot e t))         = pure $ Flip (Annot e t)
   -- traverse _ (Flip (Widen e))           = pure $ Flip (Widen e)
 instance Traversable (Flip2 (Expr t) e ip) where  -- p
   traverse f (Flip2 (Match e v alt))    = Flip2 <$> (Match e v <$> traverse (ttraverse f) alt)
@@ -203,10 +205,12 @@ instance Traversable (Flip2 (Expr t) e ip) where  -- p
   traverse _ (Flip2 (Put e es))         = pure $ Flip2 (Put e es)
   traverse _ (Flip2 (Let bs e))         = pure $ Flip2 (Let bs e)
   traverse _ (Flip2 (Upcast e))         = pure $ Flip2 (Upcast e)
+  traverse _ (Flip2 (Annot e t))        = pure $ Flip2 (Annot e t)
   --traverse _ (Flip2 (Widen e))          = pure $ Flip2 (Widen e)
 instance Traversable (Flip3 Expr e ip p) where  -- t
   traverse f (Flip3 (Let bs e))          = Flip3 <$> (Let <$> (traverse (tttraverse f) bs) <*> pure e)
   traverse f (Flip3 (TypeApp v ts nt))   = Flip3 <$> (TypeApp v <$> traverse (traverse f) ts <*> pure nt)
+  traverse f (Flip3 (Annot e t))         = Flip3 <$> (Annot <$> pure e <*> f t)
   traverse _ (Flip3 (Match e v alt))     = pure $ Flip3 (Match e v alt)
   traverse _ (Flip3 (Member e f))        = pure $ Flip3 (Member e f)
   traverse _ (Flip3 (PrimOp op e))       = pure $ Flip3 (PrimOp op e)

cogent/src/Cogent/TypeCheck/Generator.hs

@@ -309,6 +309,15 @@ cg' (Match e bs alts) top = do
       e = Match e' bs alts'
   return (c, e)
 
+cg' (Annot e tau) t = do
+  tvs <- use knownTypeVars
+  let t' = stripLocT tau
+  (c,t'') <- zoom tc (validateType' tvs t') >>= \case
+    Left e -> return (Unsat e, t)
+    Right t'' -> return (F t :< F t'', t'')
+  (c', e') <- cg e t''
+  return (c <> c', Annot e' t'')
+
 integral :: TCType -> Constraint
 integral a = Upcastable (T (TCon "U8" [] Unboxed)) a
 

cogent/tests/pass_ticket-e31.cogent

@@ -25,6 +25,17 @@ ostore_read ostore_st =
   | Success obj -> let _ = deep_freeObj obj in (ostore_st, Error ())
   | Error _ -> (ostore_st, Error ())
 
+ostore_read': OstoreState -> RR OstoreState Obj ()
+ostore_read' ostore_st =
+  let addr = index_get_addr ()
+  and (ostore_st, r) = 
+     let obj = get_Obj ()
+      in (ostore_st, Success obj)
+  in r : R Obj ()
+  | Success obj -> let _ = deep_freeObj obj in (ostore_st, Error ())
+  | Error _ -> (ostore_st, Error ())
+
+
 {--------------------------------------
      [Notes 21/11/16 by zilinc]
 1. We don't have polymorphic let-binding, thus the free type var `b' is something we never know.

cogent/tests/pass_type-annot-expr.cogent

@@ -0,0 +1,27 @@
+type OstoreState
+
+type Obj
+
+type R a b = <Success a | Error b>
+type RR c a b = (c, R a b)
+
+type BufOffs = U32
+deep_freeObj: Obj -> ()
+get_Obj : () -> Obj
+
+type ObjAddr
+index_get_addr : () -> #ObjAddr
+
+success : all (b, a). a -> R a b
+success a = Success a
+
+ostore_read: OstoreState -> RR OstoreState Obj ()
+ostore_read ostore_st =
+  let addr = index_get_addr ()
+  and (ostore_st, r) = 
+     (let obj = get_Obj ()
+      in (ostore_st, success[U8] obj) : RR OstoreState Obj U8) : RR OstoreState Obj U8 
+  in (r : R Obj U8)
+  | Success obj -> let _ = deep_freeObj obj in (ostore_st : OstoreState, Error ())
+  | Error _ -> (ostore_st, Error (() : ()) : R Obj ())
+