GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-24 06:52:44 +03:00
Code Issues Projects Releases Wiki Activity

Add support for user-defined infix operators

Browse Source 
Squashed commit of the following:

commit 9f03b7cd1a1f169ea192d735890fd6a3503ecb39
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:40:27 2015 -0700

    Add a test for user-defined infix operators

commit 31656a4640e8189b880fa1ce39779c07872ebe18
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:39:43 2015 -0700

    Forgot to initialize some fields in the parser

commit 73bcb2e5961691f2258f5a7a12ee2dc92d1a1ad3
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:20:40 2015 -0700

    Fix unnecessary panics in the renamer

commit 03cd8130901fb7aeb12d41cc03ce970ce6571423
Author: Trevor Elliott <trevor@galois.com>
Date:   Mon Jun 1 01:29:36 2015 -0700

    Remove a debug print

commit 2934a56b31d51ac971204d3fea9f62bf8829573d
Author: Trevor Elliott <trevor@galois.com>
Date:   Mon Jun 1 01:26:32 2015 -0700

    User-defined operators

commit 47f4b37fc75accaf0284addc2382c341167b8b6b
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 23:44:51 2015 -0700

    Parse signatures for infix operators

commit a1a11705c2eec6e669159756de2eb2cb19bcfa83
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 23:28:56 2015 -0700

    Plumb fixity information through

commit 56134ac0d9fb919f280dabfcdab6506195816340
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 22:03:55 2015 -0700

    Parse fixity declarations

commit f2db0ad5d47d478799dabf03a6cad9be7aec2191
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 16:00:57 2015 -0700

    Update test output for location changes

commit 15949018865d3ac8efca1a081334a7213c25775c
Merge: 1bd7f16 52f3a83
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:36:20 2015 -0700

    Merge remote-tracking branch 'origin/master' into wip/infix-operators

commit 1bd7f1602bd6bbf5693871f01ca65a4cf3ed3bf8
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:30:14 2015 -0700

    Forgot to consider EParens in translateExprToNumT

commit d63435270d5ca5bdf37584e4781a655a685c9c3b
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:29:47 2015 -0700

    Add | to the operator character set

commit 7be23372c4625bf20b8f8ccf94a148563417f6cb
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 14:49:07 2015 -0700

    Fix the printing of #Uniq variables

commit f9110e159aa0c3ae7450fe7a4db2a8d275d9bc1a
Author: Trevor Elliott <trevor@galois.com>
Date:   Thu May 28 17:04:26 2015 -0700

    Fix some failing tests

commit 0582fd08cc402c7bfd2de2c02df14fa77906e37e
Author: Trevor Elliott <trevor@galois.com>
Date:   Thu May 28 16:12:18 2015 -0700

    Remove more primitives from the parser

commit f5dafd1ea7954b64f7949c754e0c94abd2598679
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed May 27 18:02:52 2015 -0700

    Do fixity resolution during renaming
This commit is contained in:
Trevor Elliott 2015-06-03 11:42:33 -07:00
parent 28960c1b68
commit ae6b5dc3e8
24 changed files with 502 additions and 317 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Cryptol/ModuleSystem/Env.hs
View File

@ -129,6 +129,11 @@ focusedEnv me = fold $ do
let (local,lns) = unqualified (ifPublic iface `mappend` ifPrivate iface)
return (local `shadowing` imports,lns `mappend` names)
-- | The unqualified declarations and name environment for the dynamic
-- environment.
dynamicEnv :: ModuleEnv -> (IfaceDecls,NameEnv)
dynamicEnv me = unqualified (deIfaceDecls (meDynEnv me))
-- | Produce an ifaceDecls that represents the internal environment of the
-- module, used for typechecking.
qualifiedEnv :: ModuleEnv -> IfaceDecls

14
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -38,9 +38,9 @@ data Iface = Iface
} deriving (Show)
data IfaceDecls = IfaceDecls
{ ifTySyns :: Map.Map QName [IfaceTySyn]
, ifNewtypes :: Map.Map QName [IfaceNewtype]
, ifDecls :: Map.Map QName [IfaceDecl]
{ ifTySyns :: Map.Map QName [IfaceTySyn]
, ifNewtypes :: Map.Map QName [IfaceNewtype]
, ifDecls :: Map.Map QName [IfaceDecl]
} deriving (Show)
instance Monoid IfaceDecls where
@ -65,9 +65,9 @@ mergeByName f ls rs
-- | Like mappend for IfaceDecls, but preferring entries on the left.
shadowing :: IfaceDecls -> IfaceDecls -> IfaceDecls
shadowing l r = IfaceDecls
{ ifTySyns = Map.union (ifTySyns l) (ifTySyns r)
{ ifTySyns = Map.union (ifTySyns l) (ifTySyns r)
, ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r)
, ifDecls = Map.union (ifDecls l) (ifDecls r)
, ifDecls = Map.union (ifDecls l) (ifDecls r)
}
type IfaceTySyn = TySyn
@ -81,6 +81,8 @@ data IfaceDecl = IfaceDecl
{ ifDeclName :: QName
, ifDeclSig :: Schema
, ifDeclPragmas :: [Pragma]
, ifDeclInfix :: Bool
, ifDeclFixity :: Maybe Fixity
} deriving (Show)
mkIfaceDecl :: Decl -> IfaceDecl
@ -88,6 +90,8 @@ mkIfaceDecl d = IfaceDecl
{ ifDeclName = dName d
, ifDeclSig = dSignature d
, ifDeclPragmas = dPragmas d
, ifDeclInfix = dInfix d
, ifDeclFixity = dFixity d
}
-- | Like mapIfaceDecls, but gives you back a NameEnv that describes the

47
src/Cryptol/ModuleSystem/NamingEnv.hs
View File

@ -16,6 +16,7 @@ import qualified Cryptol.TypeCheck.AST as T
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Data.Maybe (catMaybes)
import qualified Data.Map as Map
#if __GLASGOW_HASKELL__ < 710
@ -85,24 +86,30 @@ instance HasQName EName where
-- Naming Environment ----------------------------------------------------------
-- XXX The fixity environment should be removed, and EName should include fixity
-- information.
data NamingEnv = NamingEnv { neExprs :: Map.Map QName [EName]
-- ^ Expr renaming environment
, neTypes :: Map.Map QName [TName]
-- ^ Type renaming environment
, neFixity:: Map.Map QName [Fixity]
} deriving (Show)
instance Monoid NamingEnv where
mempty =
NamingEnv { neExprs = Map.empty
, neTypes = Map.empty }
NamingEnv { neExprs = Map.empty
, neTypes = Map.empty
, neFixity = Map.empty }
mappend l r =
NamingEnv { neExprs = Map.unionWith (++) (neExprs l) (neExprs r)
, neTypes = Map.unionWith (++) (neTypes l) (neTypes r) }
NamingEnv { neExprs = Map.unionWith (++) (neExprs l) (neExprs r)
, neTypes = Map.unionWith (++) (neTypes l) (neTypes r)
, neFixity = Map.union (neFixity l) (neFixity r) }
mconcat envs =
NamingEnv { neExprs = Map.unionsWith (++) (map neExprs envs)
, neTypes = Map.unionsWith (++) (map neTypes envs) }
NamingEnv { neExprs = Map.unionsWith (++) (map neExprs envs)
, neTypes = Map.unionsWith (++) (map neTypes envs)
, neFixity = Map.unions (map neFixity envs) }
-- | Singleton type renaming environment.
singletonT :: QName -> TName -> NamingEnv
@ -115,11 +122,12 @@ singletonE qn en = mempty { neExprs = Map.singleton qn [en] }
-- | Like mappend, but when merging, prefer values on the lhs.
shadowing :: NamingEnv -> NamingEnv -> NamingEnv
shadowing l r = NamingEnv
{ neExprs = Map.union (neExprs l) (neExprs r)
, neTypes = Map.union (neTypes l) (neTypes r) }
{ neExprs = Map.union (neExprs l) (neExprs r)
, neTypes = Map.union (neTypes l) (neTypes r)
, neFixity = Map.union (neFixity l) (neFixity r) }
travNamingEnv :: Applicative f => (QName -> f QName) -> NamingEnv -> f NamingEnv
travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes'
travNamingEnv f ne = NamingEnv <$> neExprs' <*> neTypes' <*> pure (neFixity ne)
where
neExprs' = traverse (traverse travE) (neExprs ne)
neTypes' = traverse (traverse travT) (neTypes ne)
@ -173,7 +181,11 @@ instance BindsNames IfaceDecls where
}
vars = mempty
{ neExprs = Map.map (map (EFromMod . ifDeclName)) (ifDecls binds)
{ neExprs = Map.map (map (EFromMod . ifDeclName)) (ifDecls binds)
, neFixity = Map.fromList [ (n,fs) | ds <- Map.elems (ifDecls binds)
, all ifDeclInfix ds
, let fs = catMaybes (map ifDeclFixity ds)
n = ifDeclName (head ds) ]
}
@ -185,10 +197,14 @@ instance BindsNames Match where
MatchLet b -> namingEnv b
instance BindsNames Bind where
namingEnv b = singletonE (thing qn) (EFromBind qn)
namingEnv b = singletonE (thing qn) (EFromBind qn) `mappend` fixity
where
qn = bName b
fixity = case bFixity b of
Just f -> mempty { neFixity = Map.singleton (thing qn) [f] }
Nothing -> mempty
-- | Generate the naming environment for a type parameter.
instance BindsNames TParam where
namingEnv p = singletonT qn (TFromParam qn)
@ -220,11 +236,17 @@ instance BindsNames Module where
declEnv d = case d of
DSignature ns _sig -> foldMap qualBind ns
DPragma ns _p -> foldMap qualBind ns
DBind b -> qualBind (bName b)
DBind b -> qualBind (bName b) `mappend` fixity b
DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"]
DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"]
DType (TySyn lqn _ _) -> qualType lqn
DLocated d' _ -> declEnv d'
fixity b =
case bFixity b of
Just f -> mempty { neFixity = Map.singleton (thing (qual (bName b))) [f] }
Nothing -> mempty
newtypeEnv n = singletonT (thing qn) (TFromNewtype (qual qn))
`mappend` singletonE (thing qn) (EFromNewtype (qual qn))
where
@ -238,6 +260,7 @@ instance BindsNames Decl where
DPragma ns _p -> foldMap qualBind ns
DBind b -> qualBind (bName b)
DPatBind _pat _e -> panic "ModuleSystem" ["Unexpected pattern binding"]
DFixity{} -> panic "ModuleSystem" ["Unexpected fixity declaration"]
DType (TySyn lqn _ _) -> qualType lqn
DLocated d' _ -> namingEnv d'
where

110
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -8,6 +8,7 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
module Cryptol.ModuleSystem.Renamer (
NamingEnv(), shadowing
@ -58,6 +59,8 @@ data RenamerError
| ExpectedType (Located QName)
-- ^ When a type is missing from the naming environment, but one or more
-- values exist with the same name.
| FixityError (Located QName) (Located QName)
deriving (Show)
instance PP RenamerError where
@ -92,6 +95,12 @@ instance PP RenamerError where
4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))
, text "but found a value instead" ])
FixityError o1 o2 ->
hang (text "[error]")
4 (fsep [ text "The fixities of", pp o1, text "and", pp o2
, text "are not compatible. "
, text "You may use explicit parenthesis to disambiguate" ])
-- Warnings --------------------------------------------------------------------
data RenamerWarning
@ -268,6 +277,7 @@ instance Rename Decl where
DType syn -> DType <$> rename syn
DLocated d' r -> withLoc r
$ DLocated <$> rename d' <*> pure r
DFixity{} -> panic "Renamer" ["Unexpected fixity declaration", show d]
instance Rename Newtype where
rename n = do
@ -277,26 +287,32 @@ instance Rename Newtype where
, nParams = nParams n
, nBody = body' }
renameExpr :: QName -> RenameM QName
renameExpr qn = do
renameVar :: QName -> RenameM Expr
renameVar qn = do
ro <- RenameM ask
case Map.lookup qn (neExprs (roNames ro)) of
Just [en] -> return (qname en)
Just [] -> panic "Renamer" ["Invalid expression renaming environment"]
Just [en] -> return (EVar (qname en))
Just [] ->
panic "Renamer" ["Invalid expression renaming environment"]
Just syms ->
do n <- located qn
record (MultipleSyms n (map origin syms))
return qn
Nothing ->
do n <- located qn
return (EVar qn)
Nothing
case Map.lookup qn (neTypes (roNames ro)) of
-- types existed with the name of the value expected
Just _ -> record (ExpectedValue n)
| Just prim <- Map.lookup qn primNames ->
return (ECon prim)
-- the value is just missing
Nothing -> record (UnboundExpr n)
return qn
| otherwise ->
do n <- located qn
case Map.lookup qn (neTypes (roNames ro)) of
-- types existed with the name of the value expected
Just _ -> record (ExpectedValue n)
-- the value is just missing
Nothing -> record (UnboundExpr n)
return (EVar qn)
renameType :: QName -> RenameM QName
renameType qn = do
@ -385,7 +401,11 @@ bindingTypeEnv b = patParams `shadowing` sigParams
-- to allow for top-level renaming
instance Rename Bind where
rename b = do
n' <- renameLoc renameExpr (bName b)
le <- renameLoc renameVar (bName b)
n' <- case thing le of
EVar n' -> return le { thing = n' }
_ -> panic "Renamer" [ "Invalid name in binding:", show le ]
shadowNames (bindingTypeEnv b) $ do
(patenv,pats') <- renamePats (bParams b)
sig' <- traverse renameSchema (bSignature b)
@ -414,7 +434,7 @@ instance Rename Pattern where
instance Rename Expr where
rename e = case e of
EVar n -> EVar <$> renameExpr n
EVar n -> renameVar n
ECon _ -> return e
ELit _ -> return e
ETuple es -> ETuple <$> rename es
@ -437,6 +457,64 @@ instance Rename Expr where
ELocated e' r -> withLoc r
$ ELocated <$> rename e' <*> pure r
EParens p -> rename p
EInfix x y z -> do op <- renameOp y
renameInfix x y op z
renameInfix :: Expr -> Located QName -> (Expr,Fixity) -> Expr -> RenameM Expr
renameInfix (EInfix e1 o1 e2) o2 opr@(o2',Fixity a2 p2) e3 =
do opl@(o1',Fixity a1 p1) <- renameOp o1
if | p1 > p2 || (p1 == p2 && a1 == LeftAssoc && a2 == LeftAssoc) ->
do el <- renameInfix e1 o1 opl e2
er <- rename e3
return (o2' `EApp` el `EApp` er)
| p1 < p2 || (p1 == p2 && a1 == RightAssoc && a2 == RightAssoc) ->
do el <- rename e1
er <- renameInfix e2 o2 opr e3
return (o1' `EApp` el `EApp` er)
| otherwise ->
do record (FixityError o1 o2)
e1' <- rename e1
e2' <- rename e2
e3' <- rename e3
return (o2' `EApp` (o1' `EApp` e1' `EApp` e2') `EApp` e3')
renameInfix (ELocated e _) o2 opr e3 =
renameInfix e o2 opr e3
renameInfix e _ (op,_) e3 =
do e' <- rename e
e3' <- rename e3
return (op `EApp` e' `EApp` e3')
renameOp :: Located QName -> RenameM (Expr,Fixity)
renameOp ln = withLoc ln $
do e <- renameVar (thing ln)
ro <- RenameM ask
case e of
-- lookup the operator in the fixed prim table
e' @ (ECon n) ->
case Map.lookup n eBinOpPrec of
Just (a,i) -> return (e',Fixity a i)
Nothing -> panic "Renamer" [ "No fixity for primitive:"
, show n
, show ln ]
-- lookup the operator in the environment
e' @ (EVar n) ->
case Map.lookup n (neFixity (roNames ro)) of
Just [fixity] -> return (e',fixity)
_ -> return (e',defaultFixity)
_ -> panic "Renamer" [ "Invalid infix operator", show e ]
instance Rename TypeInst where
rename ti = case ti of
NamedInst nty -> NamedInst <$> rename nty
@ -475,7 +553,7 @@ instance Rename TySyn where
rename (TySyn n ps ty) =
shadowNames ps (TySyn <$> renameLoc renameType n <*> pure ps <*> rename ty)
renameLoc :: (a -> RenameM a) -> Located a -> RenameM (Located a)
renameLoc :: (a -> RenameM b) -> Located a -> RenameM (Located b)
renameLoc by loc = do
a' <- by (thing loc)
return loc { thing = a' }

207
src/Cryptol/Parser.y
View File

@ -16,6 +16,7 @@ module Cryptol.Parser
, guessPreProc, PreProc(..)
) where
import Control.Applicative as A
import Data.Maybe(fromMaybe)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
@ -45,13 +46,13 @@ import Paths_cryptol
'hiding' { Located $$ (Token (KW KW_hiding) _)}
'private' { Located $$ (Token (KW KW_private) _)}
'property' { Located $$ (Token (KW KW_property) _)}
'infix' { Located $$ (Token (KW KW_infix) _)}
'infixl' { Located $$ (Token (KW KW_infixl) _)}
'infixr' { Located $$ (Token (KW KW_infixr) _)}
'False' { Located $$ (Token (KW KW_False ) _)}
'True' { Located $$ (Token (KW KW_True ) _)}
'Arith' { Located $$ (Token (KW KW_Arith ) _)}
'Bit' { Located $$ (Token (KW KW_Bit ) _)}
'Cmp' { Located $$ (Token (KW KW_Cmp ) _)}
'error' { Located $$ (Token (KW KW_error ) _)}
'fin' { Located $$ (Token (KW KW_fin ) _)}
'inf' { Located $$ (Token (KW KW_inf ) _)}
'lg2' { Located $$ (Token (KW KW_lg2 ) _)}
@ -67,17 +68,7 @@ import Paths_cryptol
'else' { Located $$ (Token (KW KW_else ) _)}
'min' { Located $$ (Token (KW KW_min ) _)}
'max' { Located $$ (Token (KW KW_max ) _)}
'zero' { Located $$ (Token (KW KW_zero ) _)}
'join' { Located $$ (Token (KW KW_join ) _)}
'reverse' { Located $$ (Token (KW KW_reverse) _)}
'split' { Located $$ (Token (KW KW_split ) _)}
'splitAt' { Located $$ (Token (KW KW_splitAt) _)}
'transpose' { Located $$ (Token (KW KW_transpose) _)}
'x' { Located $$ (Token (KW KW_x) _)}
'pmult' { Located $$ (Token (KW KW_pmult) _)}
'pmod' { Located $$ (Token (KW KW_pmod) _)}
'pdiv' { Located $$ (Token (KW KW_pdiv) _)}
'random' { Located $$ (Token (KW KW_random) _)}
'[' { Located $$ (Token (Sym BracketL) _)}
']' { Located $$ (Token (Sym BracketR) _)}
@ -109,39 +100,22 @@ import Paths_cryptol
'v}' { Located $$ (Token (Virt VCurlyR) _)}
'v;' { Located $$ (Token (Virt VSemi) _)}
'+' { Located $$ (Token (Op Plus ) _)}
'-' { Located $$ (Token (Op Minus ) _)}
'*' { Located $$ (Token (Op Mul ) _)}
'/' { Located $$ (Token (Op Div ) _)}
'^^' { Located $$ (Token (Op Exp ) _)}
'%' { Located $$ (Token (Op Mod ) _)}
'+' { Located $$ (Token (Op Plus) _)}
'-' { Located $$ (Token (Op Minus) _)}
'*' { Located $$ (Token (Op Mul) _)}
'/' { Located $$ (Token (Op Div) _)}
'^^' { Located $$ (Token (Op Exp) _)}
'%' { Located $$ (Token (Op Mod) _)}
'^' { Located $$ (Token (Op Xor ) _)}
'||' { Located $$ (Token (Op Disj ) _)}
'&&' { Located $$ (Token (Op Conj ) _)}
'~' { Located $$ (Token (Op Complement) _)}
'!=' { Located $$ (Token (Op NotEqual ) _)}
'==' { Located $$ (Token (Op Equal ) _)}
'!==' { Located $$ (Token (Op NotEqualFun ) _)}
'===' { Located $$ (Token (Op EqualFun ) _)}
'>' { Located $$ (Token (Op GreaterThan ) _)}
'<' { Located $$ (Token (Op LessThan ) _)}
'<=' { Located $$ (Token (Op LEQ ) _)}
'>=' { Located $$ (Token (Op GEQ ) _)}
'==' { Located $$ (Token (Op Equal) _)}
'<=' { Located $$ (Token (Op LEQ) _)}
'>=' { Located $$ (Token (Op GEQ) _)}
'>>' { Located $$ (Token (Op ShiftR ) _)}
'<<' { Located $$ (Token (Op ShiftL ) _)}
'>>>' { Located $$ (Token (Op RotR ) _)}
'<<<' { Located $$ (Token (Op RotL ) _)}
'~' { Located $$ (Token (Op Complement ) _)}
'@' { Located $$ (Token (Op At ) _)}
'@@' { Located $$ (Token (Op AtAt ) _)}
'!' { Located $$ (Token (Op Bang ) _)}
'!!' { Located $$ (Token (Op BangBang ) _)}
'#' { Located $$ (Token (Op Hash ) _)}
'#' { Located $$ (Token (Op Hash) _)}
OP { $$@(Located _ (Token (Op {}) _))}
%name vmodule vmodule
%name program program
@ -166,18 +140,14 @@ import Paths_cryptol
%left 'where'
%nonassoc 'then' 'else'
%nonassoc ':'
%left '||'
%left '&&'
%nonassoc '==' '!=' '===' '!=='
%nonassoc '<' '>' '<=' '>='
%left '^'
%nonassoc '=='
%nonassoc '<=' '>='
%right '#'
%left '<<' '>>' '<<<' '>>>'
%left '+' '-'
%left '*' '/' '%'
%right '^^'
%left '@' '@@' '!' '!!'
%right NEG '~'
%left OP
%%
@ -281,11 +251,29 @@ decl :: { Decl }
, bSignature = Nothing
, bPragmas = []
, bMono = False
, bInfix = False
, bFixity = Nothing
} }
| apat op apat '=' expr { at ($1,$5) $
DBind $ Bind { bName = $2
, bParams = [$1,$3]
, bDef = $5
, bSignature = Nothing
, bPragmas = []
, bMono = False
, bInfix = True
, bFixity = Nothing
} }
| 'type' name '=' type {% at ($1,$4) `fmap` mkTySyn $2 [] $4 }
| 'type' name tysyn_params '=' type
{% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5 }
| 'infixl' NUM ops {% mkFixity LeftAssoc $2 (reverse $3) }
| 'infixr' NUM ops {% mkFixity RightAssoc $2 (reverse $3) }
| 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) }
let_decl :: { Decl }
: 'let' apat '=' expr { at ($2,$4) $ DPatBind $2 $4 }
| 'let' name apats '=' expr { at ($2,$5) $
@ -295,6 +283,8 @@ let_decl :: { Decl }
, bSignature = Nothing
, bPragmas = []
, bMono = False
, bInfix = False
, bFixity = Nothing
} }
newtype :: { Newtype }
@ -307,9 +297,12 @@ newtype_body :: { [Named Type] }
: '{' '}' { [] }
| '{' field_types '}' { $2 }
vars_comma :: { [ LName ] }
: name { [ $1] }
| vars_comma ',' name { $3 : $1 }
vars_comma :: { [ LName ] }
: name { [ $1] }
| vars_comma ',' name { $3 : $1 }
| '(' op ')' { [fmap unqual $2] }
| vars_comma ',' '(' op ')' { fmap unqual $4 : $1 }
apats :: { [Pattern] }
: apat { [$1] }
@ -351,47 +344,38 @@ ifBranch :: { (Expr, Expr) }
: expr 'then' expr { ($1, $3) }
iexpr :: { Expr }
: expr10 { $1 }
| iexpr op expr10 { binOp $1 $2 $3 }
| iexpr ':' type { at ($1,$3) $ ETyped $1 $3 }
expr10 :: { Expr }
: aexprs { mkEApp $1 }
| iexpr ':' type { at ($1,$3) $ ETyped $1 $3 }
| 'if' ifBranches 'else' iexpr { at ($1,$4) $ mkIf $2 $4 }
| '\\' apats '->' iexpr { at ($1,$4) $ EFun (reverse $2) $4 }
| iexpr '@' iexpr { binOp $1 (op ECAt $2) $3 }
| iexpr '@@' iexpr { binOp $1 (op ECAtRange $2) $3 }
| iexpr '!' iexpr { binOp $1 (op ECAtBack $2) $3 }
| iexpr '!!' iexpr { binOp $1 (op ECAtRangeBack $2) $3 }
| iexpr '#' iexpr { binOp $1 (op ECCat $2) $3 }
| iexpr '+' iexpr { binOp $1 (op ECPlus $2) $3 }
| iexpr '-' iexpr { binOp $1 (op ECMinus $2) $3 }
| iexpr '*' iexpr { binOp $1 (op ECMul $2) $3 }
| iexpr '/' iexpr { binOp $1 (op ECDiv $2) $3 }
| iexpr '%' iexpr { binOp $1 (op ECMod $2) $3 }
| iexpr '^^' iexpr { binOp $1 (op ECExp $2) $3 }
| iexpr '^' iexpr { binOp $1 (op ECXor $2) $3 }
| iexpr '||' iexpr { binOp $1 (op ECOr $2) $3 }
| iexpr '&&' iexpr { binOp $1 (op ECAnd $2) $3 }
| iexpr '==' iexpr { binOp $1 (op ECEq $2) $3 }
| iexpr '!=' iexpr { binOp $1 (op ECNotEq $2) $3 }
| iexpr '===' iexpr { binOp $1 (op ECFunEq $2) $3 }
| iexpr '!==' iexpr { binOp $1 (op ECFunNotEq $2) $3 }
| iexpr '>' iexpr { binOp $1 (op ECGt $2) $3 }
| iexpr '<' iexpr { binOp $1 (op ECLt $2) $3 }
| iexpr '<=' iexpr { binOp $1 (op ECLtEq $2) $3 }
| iexpr '>=' iexpr { binOp $1 (op ECGtEq $2) $3 }
| iexpr '<<' iexpr { binOp $1 (op ECShiftL $2) $3 }
| iexpr '>>' iexpr { binOp $1 (op ECShiftR $2) $3 }
| iexpr '<<<' iexpr { binOp $1 (op ECRotL $2) $3 }
| iexpr '>>>' iexpr { binOp $1 (op ECRotR $2) $3 }
| '-' iexpr %prec NEG { unOp (op ECNeg $1) $2 }
| '~' iexpr { unOp (op ECCompl $1) $2 }
op :: { LQName }
: OP { let Token (Op (Other str)) _ = thing $1
in mkUnqual (Name str) A.<$ $1 }
-- special cases for operators that are also used at the type-level
| '*' { Located $1 $ mkUnqual (Name "*" ) }
| '+' { Located $1 $ mkUnqual (Name "+" ) }
| '-' { Located $1 $ mkUnqual (Name "-" ) }
| '/' { Located $1 $ mkUnqual (Name "/" ) }
| '%' { Located $1 $ mkUnqual (Name "%" ) }
| '^^' { Located $1 $ mkUnqual (Name "^^") }
| '#' { Located $1 $ mkUnqual (Name "#" ) }
| '>=' { Located $1 $ mkUnqual (Name ">=") }
| '==' { Located $1 $ mkUnqual (Name "==") }
| '<=' { Located $1 $ mkUnqual (Name "<=") }
ops :: { [LQName] }
: op { [$1] }
| ops ',' op { $3 : $1 }
aexprs :: { [Expr] }
: aexpr { [$1] }
@ -400,33 +384,15 @@ aexprs :: { [Expr] }
aexpr :: { Expr }
: qname { at $1 $ EVar (thing $1) }
| 'min' { at $1 $ ECon ECMin }
| 'max' { at $1 $ ECon ECMax }
| 'lg2' { at $1 $ ECon ECLg2 }
| 'zero' { at $1 $ ECon ECZero }
| 'join' { at $1 $ ECon ECJoin }
| 'split' { at $1 $ ECon ECSplit }
| 'splitAt' { at $1 $ ECon ECSplitAt }
| 'min' { at $1 $ EVar $ mkUnqual (Name "min") }
| 'max' { at $1 $ EVar $ mkUnqual (Name "max") }
| 'lg2' { at $1 $ EVar $ mkUnqual (Name "lg2") }
| NUM { at $1 $ numLit (tokenType (thing $1)) }
| STRLIT { at $1 $ ELit $ ECString $ getStr $1 }
| CHARLIT { at $1 $ ELit $ ECNum (getNum $1) CharLit }
| 'False' { at $1 $ ECon ECFalse }
| 'True' { at $1 $ ECon ECTrue }
| 'error' { at $1 $ ECon ECError }
| 'reverse' { at $1 $ ECon ECReverse }
| 'transpose' { at $1 $ ECon ECTranspose }
| 'pmult' { at $1 $ ECon ECPMul }
| 'pdiv' { at $1 $ ECon ECPDiv }
| 'pmod' { at $1 $ ECon ECPMod }
| 'random' { at $1 $ ECon ECRandom }
| '(' expr ')' { at ($1,$3) $2 }
| '(' expr ')' { at ($1,$3) $ EParens $2 }
| '(' tuple_exprs ')' { at ($1,$3) $ ETuple (reverse $2) }
| '(' ')' { at ($1,$2) $ ETuple [] }
| '{' '}' { at ($1,$2) $ ERecord [] }
@ -436,36 +402,7 @@ aexpr :: { Expr }
| '`' tick_ty { at ($1,$2) $ ETypeVal $2 }
| aexpr '.' selector { at ($1,$3) $ ESel $1 (thing $3) }
| '(' '@' ')' { at ($1,$3) $ ECon ECAt }
| '(' '@@' ')' { at ($1,$3) $ ECon ECAtRange }
| '(' '!' ')' { at ($1,$3) $ ECon ECAtBack }
| '(' '!!' ')' { at ($1,$3) $ ECon ECAtRangeBack }
| '(' '#' ')' { at ($1,$3) $ ECon ECCat }
| '(' '+' ')' { at ($1,$3) $ ECon ECPlus }
| '(' '-' ')' { at ($1,$3) $ ECon ECMinus }
| '(' '*' ')' { at ($1,$3) $ ECon ECMul }
| '(' '/' ')' { at ($1,$3) $ ECon ECDiv }
| '(' '%' ')' { at ($1,$3) $ ECon ECMod }
| '(' '^^' ')' { at ($1,$3) $ ECon ECExp }
| '(' '^' ')' { at ($1,$3) $ ECon ECXor }
| '(' '||' ')' { at ($1,$3) $ ECon ECOr }
| '(' '&&' ')' { at ($1,$3) $ ECon ECAnd }
| '(' '==' ')' { at ($1,$3) $ ECon ECEq }
| '(' '!=' ')' { at ($1,$3) $ ECon ECNotEq }
| '(' '===' ')' { at ($1,$3) $ ECon ECFunEq }
| '(' '!==' ')' { at ($1,$3) $ ECon ECFunNotEq }
| '(' '>' ')' { at ($1,$3) $ ECon ECGt }
| '(' '<' ')' { at ($1,$3) $ ECon ECLt }
| '(' '<=' ')' { at ($1,$3) $ ECon ECLtEq }
| '(' '>=' ')' { at ($1,$3) $ ECon ECGtEq }
| '(' '<<' ')' { at ($1,$3) $ ECon ECShiftL }
| '(' '>>' ')' { at ($1,$3) $ ECon ECShiftR }
| '(' '<<<' ')' { at ($1,$3) $ ECon ECRotL }
| '(' '>>>' ')' { at ($1,$3) $ ECon ECRotR }
| '(' op ')' { at ($1,$3) $ EVar $ thing $2 }
| '<|' '|>' {% mkPoly (rComb $1 $2) [] }
| '<|' poly_terms '|>' {% mkPoly (rComb $1 $3) $2 }

42
src/Cryptol/Parser/AST.hs
View File

@ -16,6 +16,7 @@ module Cryptol.Parser.AST
, Name(..)
, Named(..)
, Pass(..)
, Assoc(..)
-- * Types
, Schema(..)
@ -29,6 +30,7 @@ module Cryptol.Parser.AST
, Program(..)
, TopDecl(..)
, Decl(..)
, Fixity(..), defaultFixity
, TySyn(..)
, Bind(..)
, Pragma(..)
@ -63,6 +65,7 @@ import Cryptol.ModuleSystem.Name
import Cryptol.Parser.Position
import Cryptol.Prims.Syntax
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import qualified Data.Map as Map
import qualified Data.Set as Set
@ -109,6 +112,7 @@ data TopDecl = Decl (TopLevel Decl)
deriving (Eq,Show)
data Decl = DSignature [LQName] Schema
| DFixity !Fixity [LQName]
| DPragma [LQName] Pragma
| DBind Bind
| DPatBind Pattern Expr
@ -150,10 +154,19 @@ data Bind = Bind { bName :: LQName -- ^ Defined thing
, bParams :: [Pattern] -- ^ Parameters
, bDef :: Expr -- ^ Definition
, bSignature :: Maybe Schema -- ^ Optional type sig
, bInfix :: Bool -- ^ Infix operator?
, bFixity :: Maybe Fixity -- ^ Optional fixity info
, bPragmas :: [Pragma] -- ^ Optional pragmas
, bMono :: Bool -- ^ Is this a monomorphic binding
} deriving (Eq,Show)
data Fixity = Fixity { fAssoc :: !Assoc
, fLevel :: !Int
} deriving (Eq,Show)
defaultFixity :: Fixity
defaultFixity = Fixity LeftAssoc 9
data Pragma = PragmaNote String
| PragmaProperty
deriving (Eq,Show)
@ -243,6 +256,9 @@ data Expr = EVar QName -- ^ @ x @
| ETypeVal Type -- ^ @ `(x + 1)@, @x@ is a type
| EFun [Pattern] Expr -- ^ @ \\x y -> x @
| ELocated Expr Range -- ^ position annotation
| EParens Expr -- ^ @ (e) @ (Removed by Fixity)
| EInfix Expr (LQName) Expr -- ^ @ a + b @ (Removed by Fixity)
deriving (Eq,Show)
data TypeInst = NamedInst (Named Type)
@ -474,10 +490,16 @@ instance PP Decl where
DSignature xs s -> commaSep (map ppL xs) <+> text ":" <+> pp s
DPatBind p e -> pp p <+> text "=" <+> pp e
DBind b -> ppPrec n b
DFixity f ns -> ppFixity f ns
DPragma xs p -> ppPragma xs p
DType ts -> ppPrec n ts
DLocated d _ -> ppPrec n d
ppFixity :: Fixity -> [LQName] -> Doc
ppFixity (Fixity LeftAssoc i) ns = text "infixl" <+> int i <+> commaSep (map pp ns)
ppFixity (Fixity RightAssoc i) ns = text "infixr" <+> int i <+> commaSep (map pp ns)
ppFixity (Fixity NonAssoc i) ns = text "infix" <+> int i <+> commaSep (map pp ns)
instance PP Newtype where
ppPrec _ nt = hsep
[ text "newtype", ppL (nName nt), hsep (map pp (nParams nt)), char '='
@ -511,14 +533,20 @@ ppPragma xs p =
instance PP Bind where
ppPrec _ b = sig $$ vcat [ ppPragma [f] p | p <- bPragmas b ] $$
hang (lhs <+> eq) 4 (pp (bDef b))
where f = bName b
hang (def <+> eq) 4 (pp (bDef b))
where def | bInfix b = lhsOp
| otherwise = lhs
f = bName b
sig = case bSignature b of
Nothing -> empty
Just s -> pp (DSignature [f] s)
eq = if bMono b then text ":=" else text "="
lhs = ppL f <+> fsep (map (ppPrec 3) (bParams b))
lhsOp = case bParams b of
[x,y] -> pp x <+> ppL f <+> pp y
_ -> panic "AST" [ "Malformed infix operator", show b ]
instance PP TySyn where
ppPrec _ (TySyn x xs t) = text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs)
@ -663,6 +691,10 @@ instance PP Expr where
ELocated e _ -> ppPrec n e
EParens e -> parens (pp e)
EInfix e1 op e2 -> wrap n 0 (pp e1 <+> pp (thing op) <+> pp e2)
instance PP Selector where
ppPrec _ sel =
case sel of
@ -816,6 +848,7 @@ instance NoPos Decl where
DSignature x y -> DSignature (noPos x) (noPos y)
DPragma x y -> DPragma (noPos x) (noPos y)
DPatBind x y -> DPatBind (noPos x) (noPos y)
DFixity f ns -> DFixity f (noPos ns)
DBind x -> DBind (noPos x)
DType x -> DType (noPos x)
DLocated x _ -> noPos x
@ -831,6 +864,8 @@ instance NoPos Bind where
, bParams = noPos (bParams x)
, bDef = noPos (bDef x)
, bSignature = noPos (bSignature x)
, bInfix = bInfix x
, bFixity = bFixity x
, bPragmas = noPos (bPragmas x)
, bMono = bMono x
}
@ -867,6 +902,9 @@ instance NoPos Expr where
EFun x y -> EFun (noPos x) (noPos y)
ELocated x _ -> noPos x
EParens e -> EParens (noPos e)
EInfix x y z -> EInfix (noPos x) y (noPos z)
instance NoPos TypeInst where
noPos (PosInst ts) = PosInst (noPos ts)
noPos (NamedInst fs) = NamedInst (noPos fs)

75
src/Cryptol/Parser/Lexer.x
View File

@ -6,7 +6,7 @@
module Cryptol.Parser.Lexer
( primLexer, lexer, Layout(..)
, Token(..), TokenT(..)
, TokenV(..), TokenKW(..), TokenErr(..), TokenOp(..), TokenSym(..), TokenW(..)
, TokenV(..), TokenKW(..), TokenErr(..), TokenSym(..), TokenW(..)
, Located(..)
, Config(..)
, defaultConfig
@ -32,6 +32,8 @@ $unitick = \x7
@id = @id_first @id_next*
@op = ([\!\@\#\$\%\^\&\*\~\>\<\?\+\=\|] | $unisymbol)+
@num2 = "0b" [0-1]+
@num8 = "0o" [0-7]+
@num10 = [0-9]+
@ -74,17 +76,13 @@ $white+ { emit $ White Space }
"Arith" { emit $ KW KW_Arith }
"Bit" { emit $ KW KW_Bit }
"Cmp" { emit $ KW KW_Cmp }
"False" { emit $ KW KW_False }
"Inf" { emit $ KW KW_inf }
"True" { emit $ KW KW_True }
"else" { emit $ KW KW_else }
"Eq" { emit $ KW KW_Eq }
"error" { emit $ KW KW_error }
"extern" { emit $ KW KW_extern }
"fin" { emit $ KW KW_fin }
"if" { emit $ KW KW_if }
"private" { emit $ KW KW_private }
"join" { emit $ KW KW_join }
"include" { emit $ KW KW_include }
"inf" { emit $ KW KW_inf }
"lg2" { emit $ KW KW_lg2 }
@ -96,25 +94,20 @@ $white+ { emit $ White Space }
"newtype" { emit $ KW KW_newtype }
"pragma" { emit $ KW KW_pragma }
"property" { emit $ KW KW_property }
"pmult" { emit $ KW KW_pmult }
"pdiv" { emit $ KW KW_pdiv }
"pmod" { emit $ KW KW_pmod }
"random" { emit $ KW KW_random }
"reverse" { emit $ KW KW_reverse }
"split" { emit $ KW KW_split }
"splitAt" { emit $ KW KW_splitAt }
"then" { emit $ KW KW_then }
"transpose" { emit $ KW KW_transpose }
"type" { emit $ KW KW_type }
"where" { emit $ KW KW_where }
"let" { emit $ KW KW_let }
"x" { emit $ KW KW_x }
"zero" { emit $ KW KW_zero }
"import" { emit $ KW KW_import }
"as" { emit $ KW KW_as }
"hiding" { emit $ KW KW_hiding }
"newtype" { emit $ KW KW_newtype }
"infixl" { emit $ KW KW_infixl }
"infixr" { emit $ KW KW_infixr }
"infix" { emit $ KW KW_infix }
@num2 { emitS (numToken 2 . drop 2) }
@num8 { emitS (numToken 8 . drop 2) }
@num10 { emitS (numToken 10 . drop 0) }
@ -123,39 +116,6 @@ $white+ { emit $ White Space }
"_" { emit $ Sym Underscore }
@id { mkIdent }
"+" { emit $ Op Plus }
"-" { emit $ Op Minus }
"*" { emit $ Op Mul }
"/" { emit $ Op Div }
"%" { emit $ Op Mod }
"^^" { emit $ Op Exp }
"!=" { emit $ Op NotEqual }
"==" { emit $ Op Equal }
"===" { emit $ Op EqualFun }
"!==" { emit $ Op NotEqualFun }
">" { emit $ Op GreaterThan }
"<" { emit $ Op LessThan }
"<=" { emit $ Op LEQ }
">=" { emit $ Op GEQ }
">>" { emit $ Op ShiftR }
"<<" { emit $ Op ShiftL }
">>>" { emit $ Op RotR }
"<<<" { emit $ Op RotL }
"~" { emit $ Op Complement }
"^" { emit $ Op Xor }
"||" { emit $ Op Disj }
"&&" { emit $ Op Conj }
"!" { emit $ Op Bang }
"!!" { emit $ Op BangBang }
"@" { emit $ Op At }
"@@" { emit $ Op AtAt }
"#" { emit $ Op Hash }
"\" { emit $ Sym Lambda }
"->" { emit $ Sym ArrR }
"<-" { emit $ Sym ArrL }
@ -182,6 +142,27 @@ $white+ { emit $ White Space }
\" { startString }
\' { startChar }
-- special cases for types and kinds
"+" { emit (Op Plus ) }
"-" { emit (Op Minus) }
"*" { emit (Op Mul ) }
"/" { emit (Op Div ) }
"%" { emit (Op Mod ) }
"^^" { emit (Op Exp ) }
"==" { emit (Op Equal) }
"<=" { emit (Op LEQ ) }
">=" { emit (Op GEQ ) }
"*" { emit (Op Hash ) }
-- hash is used as a kind, and as a pattern
"#" { emit (Op Hash ) }
-- ~ is used for unary complement
"~" { emit (Op Complement) }
-- all other operators
@op { emitS (Op . Other) }
}

27
src/Cryptol/Parser/LexerUtils.hs
View File

@ -314,18 +314,14 @@ data TokenW = BlockComment | LineComment | Space
data TokenKW = KW_Arith
| KW_Bit
| KW_Cmp
| KW_False
| KW_True
| KW_else
| KW_Eq
| KW_error
| KW_extern
| KW_fin
| KW_if
| KW_private
| KW_include
| KW_inf
| KW_join
| KW_lg2
| KW_lengthFromThen
| KW_lengthFromThenTo
@ -334,33 +330,26 @@ data TokenKW = KW_Arith
| KW_module
| KW_newtype
| KW_pragma
| KW_pmult
| KW_pdiv
| KW_pmod
| KW_property
| KW_random
| KW_reverse
| KW_split
| KW_splitAt
| KW_then
| KW_transpose
| KW_type
| KW_where
| KW_let
| KW_x
| KW_zero
| KW_import
| KW_as
| KW_hiding
| KW_infixl
| KW_infixr
| KW_infix
deriving (Eq,Show)
-- | The named operators are a special case for parsing types, and 'Other' is
-- used for all other cases that lexed as an operator.
data TokenOp = Plus | Minus | Mul | Div | Exp | Mod
| NotEqual | Equal | LessThan | GreaterThan | LEQ | GEQ
| EqualFun | NotEqualFun
| ShiftL | ShiftR | RotL | RotR
| Conj | Disj | Xor
| Complement
| Bang | BangBang | At | AtAt | Hash
| Equal | LEQ | GEQ
| Complement | Hash
| Other String
deriving (Eq,Show)
data TokenSym = Bar

9
src/Cryptol/Parser/Names.hs
View File

@ -46,6 +46,7 @@ namesD decl =
DBind b -> namesB b
DPatBind p e -> (namesP p, namesE e)
DSignature {} -> ([],Set.empty)
DFixity{} -> ([],Set.empty)
DPragma {} -> ([],Set.empty)
DType {} -> ([],Set.empty)
DLocated d _ -> namesD d
@ -60,6 +61,7 @@ allNamesD decl =
DBind b -> fst (namesB b)
DPatBind p _ -> namesP p
DSignature ns _ -> ns
DFixity _ ns -> ns
DPragma ns _ -> ns
DType ts -> [tsName ts]
DLocated d _ -> allNamesD d
@ -98,6 +100,9 @@ namesE expr =
EFun ps e -> boundNames (namesPs ps) (namesE e)
ELocated e _ -> namesE e
EParens e -> namesE e
EInfix a o b -> Set.insert (thing o) (Set.union (namesE a) (namesE b))
-- | The names defined by a group of patterns.
namesPs :: [Pattern] -> [Located QName]
namesPs = concatMap namesP
@ -168,6 +173,7 @@ tnamesD :: Decl -> ([Located QName], Set QName)
tnamesD decl =
case decl of
DSignature _ s -> ([], tnamesS s)
DFixity {} -> ([], Set.empty)
DPragma {} -> ([], Set.empty)
DBind b -> ([], tnamesB b)
DPatBind _ e -> ([], tnamesE e)
@ -207,6 +213,9 @@ tnamesE expr =
EFun ps e -> Set.union (Set.unions (map tnamesP ps)) (tnamesE e)
ELocated e _ -> tnamesE e
EParens e -> tnamesE e
EInfix a _ b -> Set.union (tnamesE a) (tnamesE b)
tnamesTI :: TypeInst -> Set QName
tnamesTI (NamedInst f) = tnamesT (value f)
tnamesTI (PosInst t) = tnamesT t

52
src/Cryptol/Parser/NoPat.hs
View File

@ -49,7 +49,7 @@ instance RemovePatterns [Decl] where
simpleBind :: Located QName -> Expr -> Bind
simpleBind x e = Bind { bName = x, bParams = [], bDef = e
, bSignature = Nothing, bPragmas = []
, bMono = True
, bMono = True, bInfix = False, bFixity = Nothing
}
sel :: Pattern -> QName -> Selector -> Bind
@ -162,6 +162,9 @@ noPatE expr =
return (EFun ps1 e1)
ELocated e r1 -> ELocated <$> inRange r1 (noPatE e) <*> return r1
EParens e -> EParens <$> noPatE e
EInfix x y z -> EInfix <$> noPatE x <*> pure y <*> noPatE z
where noPatF x = do e <- noPatE (value x)
return x { value = e }
@ -195,6 +198,7 @@ noMatchD decl =
case decl of
DSignature {} -> return [decl]
DPragma {} -> return [decl]
DFixity{} -> return [decl]
DBind b -> do b1 <- noMatchB b
return [DBind b1]
@ -209,6 +213,8 @@ noMatchD decl =
, bSignature = Nothing
, bPragmas = []
, bMono = False
, bInfix = False
, bFixity = Nothing
} : map DBind bs
DType {} -> return [decl]
@ -220,7 +226,8 @@ noPatDs ds =
do ds1 <- concat <$> mapM noMatchD ds
let pragmaMap = Map.fromListWith (++) $ concatMap toPragma ds1
sigMap = Map.fromListWith (++) $ concatMap toSig ds1
(ds2, (pMap,sMap)) <- runStateT (pragmaMap, sigMap) $ annotDs ds1
fixMap = Map.fromListWith (++) $ concatMap toFixity ds1
(ds2, (pMap,sMap,fMap)) <- runStateT (pragmaMap, sigMap, fixMap) $ annotDs ds1
forM_ (Map.toList pMap) $ \(n,ps) ->
forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p)
@ -230,6 +237,9 @@ noPatDs ds =
forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n })
(thing s)
forM_ (Map.toList fMap) $ \(n,fs) ->
forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n }
return ds2
noPatTopDs :: [TopLevel Decl] -> NoPatM [TopLevel Decl]
@ -239,9 +249,10 @@ noPatTopDs tds =
let allDecls = concat noPatGroups
pragmaMap = Map.fromListWith (++) $ concatMap toPragma allDecls
sigMap = Map.fromListWith (++) $ concatMap toSig allDecls
fixMap = Map.fromListWith (++) $ concatMap toFixity allDecls
let exportGroups = zipWith (\ td ds -> td { tlValue = ds }) tds noPatGroups
(tds', (pMap,sMap)) <- runStateT (pragmaMap,sigMap) (annotTopDs exportGroups)
(tds', (pMap,sMap,fMap)) <- runStateT (pragmaMap,sigMap,fixMap) (annotTopDs exportGroups)
forM_ (Map.toList pMap) $ \(n,ps) ->
forM_ ps $ \p -> recordError $ PragmaNoBind (p { thing = n }) (thing p)
@ -251,6 +262,9 @@ noPatTopDs tds =
forM_ ss $ \s -> recordError $ SignatureNoBind (s { thing = n })
(thing s)
forM_ (Map.toList fMap) $ \(n,fs) ->
forM_ fs $ \f -> recordError $ FixityNoBind f { thing = n }
return tds'
@ -279,6 +293,7 @@ noPatModule m =
type AnnotMap = ( Map.Map QName [Located Pragma]
, Map.Map QName [Located Schema]
, Map.Map QName [Located Fixity]
)
-- | Add annotations to exported declaration groups.
@ -317,6 +332,7 @@ annotD decl =
case decl of
DBind b -> DBind <$> lift (annotB b)
DSignature {} -> raise ()
DFixity{} -> raise ()
DPragma {} -> raise ()
DPatBind {} -> raise ()
DType {} -> return decl
@ -325,16 +341,19 @@ annotD decl =
-- | Add pragma/signature annotations to a binding.
annotB :: Bind -> StateT AnnotMap NoPatM Bind
annotB Bind { .. } =
do (ps,ss) <- get
do (ps,ss,fs) <- get
let name = thing bName
case ( Map.updateLookupWithKey (\_ _ -> Nothing) name ps
, Map.updateLookupWithKey (\_ _ -> Nothing) name ss
, Map.updateLookupWithKey (\_ _ -> Nothing) name fs
) of
( (thisPs, pragmas1) , (thisSigs, sigs1)) ->
( (thisPs, pragmas1), (thisSigs, sigs1), (thisFixes, fixes1)) ->
do s <- lift $ checkSigs name (jn thisSigs)
set (pragmas1,sigs1)
f <- lift $ checkFixs name (jn thisFixes)
set (pragmas1,sigs1,fixes1)
return Bind { bSignature = s
, bPragmas = map thing (jn thisPs) ++ bPragmas
, bFixity = f
, ..
}
where jn x = concat (maybeToList x)
@ -346,6 +365,12 @@ checkSigs _ [s] = return (Just (thing s))
checkSigs f xs@(s : _ : _) = do recordError $ MultipleSignatures f xs
return (Just (thing s))
checkFixs :: QName -> [Located Fixity] -> NoPatM (Maybe Fixity)
checkFixs _ [] = return Nothing
checkFixs _ [f] = return (Just (thing f))
checkFixs f fs@(x:_) = do recordError $ MultipleFixities f $ map srcRange fs
return (Just (thing x))
-- | Does this declaration provide some signatures?
toSig :: Decl -> [(QName, [Located Schema])]
@ -359,6 +384,11 @@ toPragma (DLocated d _) = toPragma d
toPragma (DPragma xs s) = [ (thing x,[Located (srcRange x) s]) | x <- xs ]
toPragma _ = []
-- | Does this declaration provide fixity information?
toFixity :: Decl -> [(QName, [Located Fixity])]
toFixity (DFixity f ns) = [ (thing n, [Located (srcRange n) f]) | n <- ns ]
toFixity _ = []
@ -370,6 +400,8 @@ data RW = RW { names :: !Int, errors :: [Error] }
data Error = MultipleSignatures QName [Located Schema]
| SignatureNoBind (Located QName) Schema
| PragmaNoBind (Located QName) Pragma
| MultipleFixities QName [Range]
| FixityNoBind (Located QName)
deriving (Show)
instance Functor NoPatM where fmap = liftM
@ -424,5 +456,11 @@ instance PP Error where
text "Pragma without a matching binding:"
$$ nest 2 (pp s)
MultipleFixities n locs ->
text "Multiple fixity declarations for" <+> quotes (pp n)
$$ nest 2 (vcat (map pp locs))
FixityNoBind n ->
text "At" <+> pp (srcRange n) <> colon <+>
text "Fixity declaration without a matching binding for:" <+>
pp (thing n)

20
src/Cryptol/Parser/ParserUtils.hs
View File

@ -19,7 +19,7 @@ import Cryptol.Utils.Panic
import Data.Maybe(listToMaybe,fromMaybe)
import Data.Bits(testBit,setBit)
import Control.Monad(liftM,ap)
import Control.Monad(liftM,ap,when)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
@ -154,6 +154,18 @@ numLit (Num x base digs)
numLit x = panic "[Parser] numLit" ["invalid numeric literal", show x]
intVal :: Located Token -> ParseM Integer
intVal tok =
case tokenType (thing tok) of
Num x _ _ -> return x
_ -> errorMessage (srcRange tok) "Expected an integer"
mkFixity :: Assoc -> Located Token -> [LQName] -> ParseM Decl
mkFixity assoc tok qns =
do l <- intVal tok
when (l < 0 || l > 10)
(errorMessage (srcRange tok) "Fixity levels must be between 0 and 10")
return (DFixity (Fixity assoc (fromInteger l)) qns)
mkTupleSel :: Range -> Integer -> ParseM (Located Selector)
mkTupleSel pos n
@ -224,8 +236,8 @@ op s r = at r (ECon s)
unOp :: Expr -> Expr -> Expr
unOp f x = at (f,x) $ EApp f x
binOp :: Expr -> Expr -> Expr -> Expr
binOp x f y = at (x,y) $ EApp (EApp f x) y
binOp :: Expr -> Located QName -> Expr -> Expr
binOp x f y = at (x,y) $ EInfix x f y
eFromTo :: Range -> Expr -> Maybe Expr -> Maybe Expr -> ParseM Expr
eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1
@ -311,6 +323,8 @@ mkProperty f ps e = DBind Bind { bName = fmap mkUnqual f
, bSignature = Nothing
, bPragmas = [PragmaProperty]
, bMono = False
, bInfix = False
, bFixity = Nothing
}
mkIf :: [(Expr, Expr)] -> Expr -> Expr

14
src/Cryptol/Parser/Utils.hs
View File

@ -14,19 +14,31 @@ module Cryptol.Parser.Utils
) where
import Cryptol.Parser.AST
import Cryptol.Parser.Position (at)
import Cryptol.Prims.Syntax
import qualified Data.Map as Map
translateExprToNumT :: Expr -> Maybe Type
translateExprToNumT expr =
case expr of
ELocated e r -> (`TLocated` r) `fmap` translateExprToNumT e
EVar (QName Nothing (Name "width")) -> mkFun TCWidth
EVar x -> return (TUser x [])
ECon x -> cvtCon x
ELit x -> cvtLit x
EApp e1 e2 -> do t1 <- translateExprToNumT e1
t2 <- translateExprToNumT e2
tApp t1 t2
EInfix a o b -> do e1 <- translateExprToNumT a
e2 <- translateExprToNumT b
ec <- cvtCon =<< Map.lookup (thing o) primNames
f <- tApp (at o ec) e1
tApp f e2
EParens e -> translateExprToNumT e
_ -> Nothing
where

136
src/Cryptol/Prims/Syntax.hs
View File

@ -12,9 +12,13 @@ module Cryptol.Prims.Syntax
, eBinOpPrec
, tBinOpPrec
, ppPrefix
, primNames
) where
import Cryptol.ModuleSystem.Name (QName,Name(Name),mkUnqual)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import qualified Data.Map as Map
-- | Built-in types.
@ -138,67 +142,81 @@ instance PP TFun where
TCLenFromThenTo -> text "lengthFromThenTo"
primNames :: Map.Map QName ECon
primDocs :: Map.Map ECon QName
(primNames,primDocs) = (Map.fromList prims, Map.fromList (map swap prims))
where
swap (a,b) = (b,a)
prim ec n = (mkUnqual (Name n), ec)
prims =
[ prim ECTrue "True"
, prim ECFalse "False"
, prim ECPlus "+"
, prim ECMinus "-"
, prim ECMul "*"
, prim ECDiv "/"
, prim ECMod "%"
, prim ECExp "^^"
, prim ECLg2 "lg2"
, prim ECLt "<"
, prim ECGt ">"
, prim ECLtEq "<="
, prim ECGtEq ">="
, prim ECEq "=="
, prim ECNotEq "!="
, prim ECFunEq "==="
, prim ECFunNotEq "!=="
, prim ECAnd "&&"
, prim ECOr "||"
, prim ECXor "^"
, prim ECCompl "~"
, prim ECShiftL "<<"
, prim ECShiftR ">>"
, prim ECRotL "<<<"
, prim ECRotR ">>>"
, prim ECCat "#"
, prim ECAt "@"
, prim ECAtRange "@@"
, prim ECAtBack "!"
, prim ECAtRangeBack "!!"
, prim ECMin "min"
, prim ECMax "max"
, prim ECSplitAt "splitAt"
, prim ECZero "zero"
, prim ECJoin "join"
, prim ECSplit "split"
, prim ECReverse "reverse"
, prim ECTranspose "transpose"
, prim ECDemote "demote"
, prim ECFromThen "fromThen"
, prim ECFromTo "fromTo"
, prim ECFromThenTo "fromThenTo"
, prim ECInfFrom "infFrom"
, prim ECInfFromThen "infFromThen"
, prim ECError "error"
, prim ECPMul "pmult"
, prim ECPDiv "pdiv"
, prim ECPMod "pmod"
, prim ECRandom "random"
]
instance PP ECon where
ppPrec _ con =
case con of
ECTrue -> text "True"
ECFalse -> text "False"
ECPlus -> text "+"
ECMinus -> text "-"
ECMul -> text "*"
ECDiv -> text "/"
ECMod -> text "%"
ECExp -> text "^^"
ECLg2 -> text "lg2"
ECNeg -> text "-"
ECLt -> text "<"
ECGt -> text ">"
ECLtEq -> text "<="
ECGtEq -> text ">="
ECEq -> text "=="
ECNotEq -> text "!="
ECFunEq -> text "==="
ECFunNotEq -> text "!=="
ECAnd -> text "&&"
ECOr -> text "||"
ECXor -> text "^"
ECCompl -> text "~"
ECShiftL -> text "<<"
ECShiftR -> text ">>"
ECRotL -> text "<<<"
ECRotR -> text ">>>"
ECCat -> text "#"
ECAt -> text "@"
ECAtRange -> text "@@"
ECAtBack -> text "!"
ECAtRangeBack -> text "!!"
ECMin -> text "min"
ECMax -> text "max"
ECSplitAt -> text "splitAt"
ECZero -> text "zero"
ECJoin -> text "join"
ECSplit -> text "split"
ECReverse -> text "reverse"
ECTranspose -> text "transpose"
ECDemote -> text "demote"
ECFromThen -> text "fromThen"
ECFromTo -> text "fromTo"
ECFromThenTo -> text "fromThenTo"
ECInfFrom -> text "infFrom"
ECInfFromThen -> text "infFromThen"
ECError -> text "error"
ECPMul -> text "pmult"
ECPDiv -> text "pdiv"
ECPMod -> text "pmod"
ECRandom -> text "random"
ppPrec _ ECNeg = text "-"
ppPrec _ con = pp (Map.findWithDefault err con primDocs)
where
err = panic "Cryptol.Prims.Syntax" [ "Primitive missing from name map"
, show con ]
ppPrefix :: ECon -> Doc
ppPrefix con = optParens (Map.member con eBinOpPrec) (pp con)

7
src/Cryptol/REPL/Command.hs
View File

@ -477,7 +477,7 @@ typeOfCmd str = do
--io (mapM_ printWarning ws)
whenDebug (rPutStrLn (dump def))
(_,names) <- getFocusedEnv
rPrint $ runDoc names $ pp expr <+> text ":" <+> pp sig
rPrint $ runDoc names $ pp def <+> text ":" <+> pp sig
reloadCmd :: REPL ()
reloadCmd = do
@ -592,7 +592,8 @@ browseVars (decls,names) pfx = do
rPutStrLn name
rPutStrLn (replicate (length name) '=')
let step k d acc =
pp k <+> char ':' <+> pp (M.ifDeclSig d) : acc
optParens (M.ifDeclInfix d) (pp k)
<+> char ':' <+> pp (M.ifDeclSig d) : acc
rPrint (runDoc names (nest 4 (vcat (Map.foldrWithKey step [] xs))))
rPutStrLn ""
@ -782,6 +783,8 @@ bindItVariable ty expr = do
, T.dSignature = schema
, T.dDefinition = expr
, T.dPragmas = []
, T.dInfix = False
, T.dFixity = Nothing
}
liftModuleCmd (M.evalDecls [dg])
denv <- getDynEnv

11
src/Cryptol/REPL/Monad.hs
View File

@ -345,12 +345,15 @@ keepOne src as = case as of
getFocusedEnv :: REPL (M.IfaceDecls,NameEnv)
getFocusedEnv = do
me <- getModuleEnv
denv <- getDynEnv
-- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound
-- variables.
let (dyDecls,dyNames) = M.dynamicEnv me
-- the subtle part here is removing the #Uniq prefix from
-- interactively-bound variables, and also excluding any that are
-- shadowed and thus can no longer be referenced
let (decls,names) = M.focusedEnv me
edecls = M.ifDecls (M.deIfaceDecls denv)
edecls = M.ifDecls dyDecls
-- is this QName something the user might actually type?
isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
case Map.lookup localName neExprs of
@ -358,14 +361,14 @@ getFocusedEnv = do
Just uniqueNames -> isNamed uniqueNames
where localName = P.QName Nothing name
isNamed us = any (== qn) (map M.qname us)
neExprs = M.neExprs (M.deNames denv)
neExprs = M.neExprs (M.deNames (M.meDynEnv me))
isShadowed _ = False
unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
edecls' = Map.fromList
. map unqual
. filter isShadowed
$ Map.toList edecls
return (decls `mappend` mempty { M.ifDecls = edecls' }, names)
return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)
getVars :: REPL (Map.Map P.QName M.IfaceDecl)
getVars = do

3
src/Cryptol/Transform/MonoValues.hs
View File

@ -290,6 +290,9 @@ rewDeclGroup rews dg =
[ Recursive monoDs ]
, dPragmas = [] -- ?
, dInfix = False
, dFixity = Nothing
}
mkProof e _ = EProofApp e

2
src/Cryptol/TypeCheck.hs
View File

@ -75,6 +75,8 @@ tcExpr e0 inp = runInferM inp
, P.bPragmas = []
, P.bSignature = Nothing
, P.bMono = False
, P.bInfix = False
, P.bFixity = Nothing
} ]
case res of

6
src/Cryptol/TypeCheck/AST.hs
View File

@ -21,13 +21,15 @@ module Cryptol.TypeCheck.AST
, ExportType(..)
, ExportSpec(..), isExportedBind, isExportedType
, Pragma(..)
, Fixity(..)
) where
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST ( Name(..), Selector(..),Pragma(..), ppSelector
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), ModName(..), isExportedBind
, isExportedType, QName(..), mkUnqual, unqual )
, isExportedType, QName(..), mkUnqual, unqual
, Fixity(..) )
import Cryptol.Utils.Panic(panic)
import Cryptol.TypeCheck.PP
@ -258,6 +260,8 @@ data Decl = Decl { dName :: QName
, dSignature :: Schema
, dDefinition :: Expr
, dPragmas :: [Pragma]
, dInfix :: !Bool
, dFixity :: Maybe Fixity
} deriving (Show)

9
src/Cryptol/TypeCheck/Infer.hs
View File

@ -141,6 +141,8 @@ appTys expr ts tGoal =
P.ETyped {} -> mono
P.ETypeVal {} -> mono
P.EFun {} -> mono
P.EParens {} -> tcPanic "appTys" [ "Unexpected EParens" ]
P.EInfix {} -> tcPanic "appTys" [ "Unexpected EInfix" ]
where mono = do e' <- checkE expr tGoal
(ie,t) <- instantiateWith e' (Forall [] [] tGoal) ts
@ -319,6 +321,9 @@ checkE expr tGoal =
P.ELocated e r -> inRange r (checkE e tGoal)
P.EParens{} -> tcPanic "checkE" [ "Unexpected EParens" ]
P.EInfix{} -> tcPanic "checkE" [ "Unexpected EInfix" ]
expectSeq :: Type -> InferM (Type,Type)
expectSeq ty =
@ -730,6 +735,8 @@ checkMonoB b t =
, dSignature = Forall [] [] t
, dDefinition = e1
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
}
-- XXX: Do we really need to do the defaulting business in two different places?
@ -787,6 +794,8 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
, dSignature = Forall as asmps t
, dDefinition = foldr ETAbs (foldr EProofAbs e2 asmps) as
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
}
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a

6
tests/issues/issue058.icry.stdout
View File

@ -9,7 +9,7 @@ Loading module Main
fin n
arising from
use of expression (!=)
at ./issue058.cry:4:12--4:14
at ./issue058.cry:4:10--4:16
[error] at ./issue058.cry:7:1--7:17:
Failed to validate user-specified signature.
In the definition of 'Main::last', at ./issue058.cry:7:1--7:5:
@ -19,7 +19,7 @@ Loading module Main
fin n
arising from
use of expression (!)
at ./issue058.cry:7:14--7:15
at ./issue058.cry:7:11--7:17
[error] at ./issue058.cry:10:1--10:17:
Failed to validate user-specified signature.
In the definition of 'Main::pad', at ./issue058.cry:10:1--10:4:
@ -27,4 +27,4 @@ Loading module Main
fin n
arising from
use of expression (#)
at ./issue058.cry:10:11--10:12
at ./issue058.cry:10:9--10:17

2
tests/mono-binds/test05.icry.stdout
View File

@ -50,7 +50,7 @@ Loading module test05
[warning] at ./test05.cry:1:1--14:21:
Defaulting 1st type parameter
of expression (#)
at ./test05.cry:14:16--14:17
at ./test05.cry:14:11--14:21
to 0
module test05
import Cryptol

9
tests/parser/infix-1.cry Normal file
View File

@ -0,0 +1,9 @@
infixl 4 ++
infixl 5 **
(++) : [8] -> [8] -> [8]
x ++ y = x + y
(**) : {a} (Arith a) => a -> a -> a
x ** y = x * y

2
tests/parser/infix-1.icry Normal file
View File

@ -0,0 +1,2 @@
:l infix-1.cry
1 ++ 2 ** 3

4
tests/parser/infix-1.icry.stdout Normal file
View File

@ -0,0 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
0x07