Add 'Logic' typeclass with operations complement, &&, ||, ^, zero.

Left and right shift operations also gain a Logic constraint,
since they shift in zero values.

lib/Cryptol.cry

@@ -100,7 +100,7 @@ primitive negate : {a} (Arith a) => a -> a
  * Bitwise complement. The prefix notation '~ x'
  * is syntactic sugar for 'complement x'.
  */
-primitive complement : {a} a -> a
+primitive complement : {a} (Logic a) => a -> a
 
 /**
  * Less-than. Only works on comparable arguments.
@@ -259,35 +259,35 @@ a ==> b = if a then b else True
 /**
  * Logical `and' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (&&) : {a} a -> a -> a
+primitive (&&) : {a} (Logic a) => a -> a -> a
 
 /**
  * Logical `or' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (||) : {a} a -> a -> a
+primitive (||) : {a} (Logic a) => a -> a -> a
 
 /**
  * Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
  */
-primitive (^) : {a} a -> a -> a
+primitive (^) : {a} (Logic a) => a -> a -> a
 
 /**
  * Gives an arbitrary shaped value whose bits are all False.
  * ~zero likewise gives an arbitrary shaped value whose bits are all True.
  */
-primitive zero : {a} a
+primitive zero : {a} (Logic a) => a
 
 /**
  * Left shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
 */
-primitive (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+primitive (<<) : {a, b, c} (fin b, Logic c) => [a]c -> [b] -> [a]c
 
 /**
  * Right shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.
  */
-primitive (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
+primitive (>>) : {a, b, c} (fin b, Logic c) => [a]c -> [b] -> [a]c
 
 /**
  * Left rotate.  The first argument is the sequence to rotate, the second is the

src/Cryptol/ModuleSystem/Renamer.hs

@@ -494,6 +494,7 @@ instance Rename Prop where
     CFin t        -> CFin       <$> rename t
     CEqual l r    -> CEqual     <$> rename l  <*> rename r
     CGeq l r      -> CGeq       <$> rename l  <*> rename r
+    CLogic t      -> CLogic     <$> rename t
     CArith t      -> CArith     <$> rename t
     CCmp t        -> CCmp       <$> rename t
     CSignedCmp t  -> CSignedCmp <$> rename t

src/Cryptol/Parser/AST.hs

@@ -372,6 +372,7 @@ tconNames  = Map.fromList
 data Prop n   = CFin (Type n)             -- ^ @ fin x   @
               | CEqual (Type n) (Type n)  -- ^ @ x == 10 @
               | CGeq (Type n) (Type n)    -- ^ @ x >= 10 @
+              | CLogic (Type n)           -- ^ @ Logic a @
               | CArith (Type n)           -- ^ @ Arith a @
               | CCmp (Type n)             -- ^ @ Cmp a @
               | CSignedCmp (Type n)       -- ^ @ SignedCmp a @
@@ -823,6 +824,7 @@ instance PPName name => PP (Prop name) where
   ppPrec n prop =
     case prop of
       CFin t       -> text "fin"   <+> ppPrec 4 t
+      CLogic t     -> text "Logic" <+> ppPrec 4 t
       CArith t     -> text "Arith" <+> ppPrec 4 t
       CCmp t       -> text "Cmp"   <+> ppPrec 4 t
       CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
@@ -981,6 +983,7 @@ instance NoPos (Prop name) where
       CEqual  x y   -> CEqual  (noPos x) (noPos y)
       CGeq x y      -> CGeq (noPos x) (noPos y)
       CFin x        -> CFin (noPos x)
+      CLogic x      -> CLogic (noPos x)
       CArith x      -> CArith (noPos x)
       CCmp x        -> CCmp   (noPos x)
       CSignedCmp x  -> CSignedCmp (noPos x)

src/Cryptol/Parser/Names.hs

@@ -261,6 +261,7 @@ tnamesC prop =
     CFin t       -> tnamesT t
     CEqual t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
     CGeq t1 t2   -> Set.union (tnamesT t1) (tnamesT t2)
+    CLogic t     -> tnamesT t
     CArith t     -> tnamesT t
     CCmp t       -> tnamesT t
     CSignedCmp t -> tnamesT t

src/Cryptol/Parser/ParserUtils.hs

@@ -428,6 +428,7 @@ mkProp ty =
 
   -- these can be translated right away
   prefixProp r f xs
+    | i == logicIdent,     [x] <- xs = return [CLocated (CLogic x) r]
     | i == arithIdent,     [x] <- xs = return [CLocated (CArith x) r]
     | i == finIdent,       [x] <- xs = return [CLocated (CFin x) r]
     | i == cmpIdent,       [x] <- xs = return [CLocated (CCmp x) r]
@@ -436,7 +437,8 @@ mkProp ty =
     where
     i = getIdent f
 
-arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
+logicIdent, arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
+logicIdent     = mkIdent (S.pack "Logic")
 arithIdent     = mkIdent (S.pack "Arith")
 finIdent       = mkIdent (S.pack "fin")
 cmpIdent       = mkIdent (S.pack "Cmp")

src/Cryptol/TypeCheck/Kind.hs

@@ -315,6 +315,7 @@ checkProp prop =
     P.CFin t1       -> tcon (PC PFin)           [t1]    (Just KProp)
     P.CEqual t1 t2  -> tcon (PC PEqual)         [t1,t2] (Just KProp)
     P.CGeq t1 t2    -> tcon (PC PGeq)           [t1,t2] (Just KProp)
+    P.CLogic t1     -> tcon (PC PLogic)         [t1]    (Just KProp)
     P.CArith t1     -> tcon (PC PArith)         [t1]    (Just KProp)
     P.CCmp t1       -> tcon (PC PCmp)           [t1]    (Just KProp)
     P.CSignedCmp t1 -> tcon (PC PSignedCmp)     [t1]    (Just KProp)

src/Cryptol/TypeCheck/SimpleSolver.hs

@@ -7,7 +7,8 @@ import Cryptol.TypeCheck.Type hiding
 import Cryptol.TypeCheck.Solver.Types
 import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
 import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
-import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst, solveSignedCmpInst)
+import Cryptol.TypeCheck.Solver.Class
+  (solveLogicInst, solveArithInst, solveCmpInst, solveSignedCmpInst)
 
 import Cryptol.Utils.Debug(ppTrace)
 import Cryptol.TypeCheck.PP
@@ -36,6 +37,7 @@ simplifyStep ctxt prop =
     TCon (PC PTrue)  []       -> SolvedIf []
     TCon (PC PAnd)   [l,r]    -> SolvedIf [l,r]
 
+    TCon (PC PLogic) [ty]     -> solveLogicInst ty
     TCon (PC PArith) [ty]     -> solveArithInst ty
     TCon (PC PCmp)   [ty]     -> solveCmpInst   ty
     TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -11,6 +11,7 @@
 {-# LANGUAGE PatternGuards #-}
 module Cryptol.TypeCheck.Solver.Class
   ( classStep
+  , solveLogicInst
   , solveArithInst
   , solveCmpInst
   , solveSignedCmpInst
@@ -22,13 +23,38 @@ import Cryptol.TypeCheck.Solver.Types
 
 -- | Solve class constraints.
 -- If not, then we return 'Nothing'.
--- If solved, ther we return 'Just' a list of sub-goals.
+-- If solved, then we return 'Just' a list of sub-goals.
 classStep :: Prop -> Solved
 classStep p = case tNoUser p of
+  TCon (PC PLogic) [ty] -> solveLogicInst (tNoUser ty)
   TCon (PC PArith) [ty] -> solveArithInst (tNoUser ty)
   TCon (PC PCmp) [ty]   -> solveCmpInst   (tNoUser ty)
   _                     -> Unsolved
 
+-- | Solve a Logic constraint by instance, if possible.
+solveLogicInst :: Type -> Solved
+solveLogicInst ty = case tNoUser ty of
+
+  -- Logic Error -> fails
+  TCon (TError _ e) _ -> Unsolvable e
+
+  -- Logic Bit
+  TCon (TC TCBit) [] -> SolvedIf []
+
+  -- Logic a => Logic [n]a
+  TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ]
+
+  -- Logic b => Logic (a -> b)
+  TCon (TC TCFun) [_,b] -> SolvedIf [ pLogic b ]
+
+  -- (Logic a, Logic b) => Logic (a,b)
+  TCon (TC (TCTuple _)) es -> SolvedIf [ pLogic e | e <- es ]
+
+  -- (Logic a, Logic b) => Logic { x1 : a, x2 : b }
+  TRec fs -> SolvedIf [ pLogic ety | (_,ety) <- fs ]
+
+  _ -> Unsolved
+
 -- | Solve an Arith constraint by instance, if possible.
 solveArithInst :: Type -> Solved
 solveArithInst ty = case tNoUser ty of

src/Cryptol/TypeCheck/Type.hs

@@ -97,6 +97,7 @@ data PC     = PEqual        -- ^ @_ == _@
 
             -- classes
             | PHas Selector -- ^ @Has sel type field@ does not appear in schemas
+            | PLogic        -- ^ @Logic _@
             | PArith        -- ^ @Arith _@
             | PCmp          -- ^ @Cmp _@
             | PSignedCmp    -- ^ @SignedCmp _@
@@ -188,6 +189,7 @@ instance HasKind PC where
       PGeq       -> KNum :-> KNum :-> KProp
       PFin       -> KNum :-> KProp
       PHas _     -> KType :-> KType :-> KProp
+      PLogic     -> KType :-> KProp
       PArith     -> KType :-> KProp
       PCmp       -> KType :-> KProp
       PSignedCmp -> KType :-> KProp
@@ -550,6 +552,9 @@ x =#= y = TCon (PC PEqual) [x,y]
 (=/=) :: Type -> Type -> Prop
 x =/= y = TCon (PC PNeq) [x,y]
 
+pLogic :: Type -> Prop
+pLogic t = TCon (PC PLogic) [t]
+
 pArith :: Type -> Prop
 pArith t = TCon (PC PArith) [t]
 
@@ -789,6 +794,7 @@ instance PP PC where
       PGeq       -> text "(>=)"
       PFin       -> text "fin"
       PHas sel   -> parens (ppSelector sel)
+      PLogic     -> text "Logic"
       PArith     -> text "Arith"
       PCmp       -> text "Cmp"
       PSignedCmp -> text "SignedCmp"