From 3b80614a09fbd46e63a52f2d55788ec5f3dd65cf Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Wed, 14 Jun 2017 15:45:28 -0700 Subject: [PATCH 01/17] added :ast command, working on printing out all definitions --- src/Cryptol/Parser/AST.hs | 186 ++++++++++++++++++++++++++++++--- src/Cryptol/Parser/Position.hs | 5 +- src/Cryptol/REPL/Command.hs | 16 +++ 3 files changed, 192 insertions(+), 15 deletions(-) diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 51bf0305..ab6963bb 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -64,6 +64,7 @@ module Cryptol.Parser.AST , Located(..) , LPName, LString, LIdent , NoPos(..) + , CoqAst(..) -- * Pretty-printing , cppKind, ppSelector @@ -131,7 +132,7 @@ data Decl name = DSignature [Located name] (Schema name) | DPatBind (Pattern name) (Expr name) | DType (TySyn name) | DLocated (Decl name) Range - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) -- | An import declaration. data Import = Import { iModule :: !ModName @@ -149,7 +150,7 @@ data ImportSpec = Hiding [Ident] deriving (Eq, Show, Generic, NFData) data TySyn n = TySyn (Located n) [TParam n] (Type n) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) {- | Bindings. Notes: @@ -172,17 +173,23 @@ data Bind name = Bind { bName :: Located name -- ^ Defined thing , bPragmas :: [Pragma] -- ^ Optional pragmas , bMono :: Bool -- ^ Is this a monomorphic binding , bDoc :: Maybe String -- ^ Optional doc string - } deriving (Eq, Show, Generic, NFData) + } deriving (Eq, Generic, NFData, Functor) + +instance (Show name) => Show (Bind name) where + show b = "(Bind (" ++ show (bName b) ++ ") (" ++ show (bDef b) ++ "))" type LBindDef = Located (BindDef PName) data BindDef name = DPrim | DExpr (Expr name) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data Fixity = Fixity { fAssoc :: !Assoc , fLevel :: !Int - } deriving (Eq, Show, Generic, NFData) + } deriving (Eq, Generic, NFData) + +instance Show Fixity where + show _ = "" data FixityCmp = FCError | FCLeft @@ -293,11 +300,11 @@ data Expr n = EVar n -- ^ @ x @ | EParens (Expr n) -- ^ @ (e) @ (Removed by Fixity) | EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data TypeInst name = NamedInst (Named (Type name)) | PosInst (Type name) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) {- | Selectors are used for projecting from various components. Each selector has an option spec to specify the shape of the thing @@ -320,7 +327,7 @@ data Selector = TupleSel Int (Maybe Int) data Match name = Match (Pattern name) (Expr name) -- ^ p <- e | MatchLet (Bind name) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data Pattern n = PVar (Located n) -- ^ @ x @ | PWild -- ^ @ _ @ @@ -330,13 +337,13 @@ data Pattern n = PVar (Located n) -- ^ @ x @ | PTyped (Pattern n) (Type n) -- ^ @ x : [8] @ | PSplit (Pattern n) (Pattern n)-- ^ @ (x # y) @ | PLocated (Pattern n) Range -- ^ Location information - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data Named a = Named { name :: Located Ident, value :: a } deriving (Eq, Show, Foldable, Traversable, Generic, NFData, Functor) data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range) - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data Kind = KNum | KType deriving (Eq, Show, Generic, NFData) @@ -345,7 +352,7 @@ data TParam n = TParam { tpName :: n , tpKind :: Maybe Kind , tpRange :: Maybe Range } - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@ | TSeq (Type n) (Type n) -- ^ @[8] a@ @@ -361,7 +368,7 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@ | TLocated (Type n) Range -- ^ Location information | TParens (Type n) -- ^ @ (ty) @ | TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @ - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) tconNames :: Map.Map PName (Type PName) tconNames = Map.fromList @@ -376,7 +383,7 @@ data Prop n = CFin (Type n) -- ^ @ fin x @ | CCmp (Type n) -- ^ @ Cmp a @ | CLocated (Prop n) Range -- ^ Location information | CType (Type n) -- ^ After parsing - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Functor) -------------------------------------------------------------------------------- -- Note: When an explicit location is missing, we could use the sub-components @@ -902,7 +909,6 @@ instance NoPos Pragma where - instance NoPos (TySyn name) where noPos (TySyn x y z) = TySyn (noPos x) (noPos y) (noPos z) @@ -985,4 +991,156 @@ instance NoPos (Prop name) where CLocated c _ -> noPos c CType t -> CType (noPos t) +--Typeclass for prettying up the AST for exporting to Coq +--Similar to NoPos above +class CoqAst t where + coqAst :: t -> t + +-- WARNING: This does not call `coqAst` on the `thing` inside +instance CoqAst (Located t) where + coqAst x = x { srcRange = rng } + where rng = Range { from = Position 0 0, to = Position 0 0, source = "" } + +instance CoqAst t => CoqAst (Named t) where + coqAst t = Named { name = coqAst (name t), value = coqAst (value t) } + +instance CoqAst t => CoqAst [t] where coqAst = fmap coqAst +instance CoqAst t => CoqAst (Maybe t) where coqAst = fmap coqAst + +instance CoqAst (Program name) where + coqAst (Program x) = Program (coqAst x) + +instance CoqAst (Module name) where + coqAst m = Module { mName = mName m + , mImports = coqAst (mImports m) + , mDecls = coqAst (mDecls m) + } + +instance CoqAst (TopDecl name) where + coqAst decl = + case decl of + Decl x -> Decl (coqAst x) + TDNewtype n -> TDNewtype(coqAst n) + Include x -> Include (coqAst x) + +instance CoqAst a => CoqAst (TopLevel a) where + coqAst tl = tl { tlValue = coqAst (tlValue tl) } + +instance CoqAst (Decl name) where + coqAst decl = + case decl of + DSignature x y -> DSignature (coqAst x) (coqAst y) + DPragma x y -> DPragma (coqAst x) (coqAst y) + DPatBind x y -> DPatBind (coqAst x) (coqAst y) + DFixity f ns -> DFixity f (coqAst ns) + DBind x -> DBind (coqAst x) + DType x -> DType (coqAst x) + DLocated x _ -> coqAst x + +instance CoqAst (Newtype name) where + coqAst n = Newtype { nName = coqAst (nName n) + , nParams = nParams n + , nBody = coqAst (nBody n) + } + +instance CoqAst (Bind name) where + coqAst x = Bind { bName = coqAst (bName x) + , bParams = coqAst (bParams x) + , bDef = coqAst (bDef x) + , bSignature = coqAst (bSignature x) + , bInfix = bInfix x + , bFixity = bFixity x + , bPragmas = coqAst (bPragmas x) + , bMono = bMono x + , bDoc = bDoc x + } + +instance CoqAst Pragma where + coqAst p@(PragmaNote {}) = p + coqAst p@(PragmaProperty) = p + + + +instance CoqAst (TySyn name) where + coqAst (TySyn x y z) = TySyn (coqAst x) (coqAst y) (coqAst z) + +instance CoqAst (Expr name) where + coqAst expr = + case expr of + EVar x -> EVar x + ELit x -> ELit x + ETuple x -> ETuple (coqAst x) + ERecord x -> ERecord (coqAst x) + ESel x y -> ESel (coqAst x) y + EList x -> EList (coqAst x) + EFromTo x y z -> EFromTo (coqAst x) (coqAst y) (coqAst z) + EInfFrom x y -> EInfFrom (coqAst x) (coqAst y) + EComp x y -> EComp (coqAst x) (coqAst y) + EApp x y -> EApp (coqAst x) (coqAst y) + EAppT x y -> EAppT (coqAst x) (coqAst y) + EIf x y z -> EIf (coqAst x) (coqAst y) (coqAst z) + EWhere x y -> EWhere (coqAst x) (coqAst y) + ETyped x y -> ETyped (coqAst x) (coqAst y) + ETypeVal x -> ETypeVal (coqAst x) + EFun x y -> EFun (coqAst x) (coqAst y) + ELocated x _ -> coqAst x + + EParens e -> EParens (coqAst e) + EInfix x y f z-> EInfix (coqAst x) y f (coqAst z) + +instance CoqAst (TypeInst name) where + coqAst (PosInst ts) = PosInst (coqAst ts) + coqAst (NamedInst fs) = NamedInst (coqAst fs) + +instance CoqAst (Match name) where + coqAst (Match x y) = Match (coqAst x) (coqAst y) + coqAst (MatchLet b) = MatchLet (coqAst b) + +instance CoqAst (Pattern name) where + coqAst pat = + case pat of + PVar x -> PVar (coqAst x) + PWild -> PWild + PTuple x -> PTuple (coqAst x) + PRecord x -> PRecord (coqAst x) + PList x -> PList (coqAst x) + PTyped x y -> PTyped (coqAst x) (coqAst y) + PSplit x y -> PSplit (coqAst x) (coqAst y) + PLocated x _ -> coqAst x + +instance CoqAst (Schema name) where + coqAst (Forall x y z _) = Forall (coqAst x) (coqAst y) (coqAst z) Nothing + +instance CoqAst (TParam name) where + coqAst (TParam x y _) = TParam x y Nothing + +instance CoqAst (Type name) where + coqAst ty = + case ty of + TWild -> TWild + TApp x y -> TApp x (coqAst y) + TUser x y -> TUser x (coqAst y) + TRecord x -> TRecord (coqAst x) + TTuple x -> TTuple (coqAst x) + TFun x y -> TFun (coqAst x) (coqAst y) + TSeq x y -> TSeq (coqAst x) (coqAst y) + TBit -> TBit + TInf -> TInf + TNum n -> TNum n + TChar n -> TChar n + TLocated x _ -> coqAst x + TParens x -> TParens (coqAst x) + TInfix x y f z-> TInfix (coqAst x) y f (coqAst z) + +instance CoqAst (Prop name) where + coqAst prop = + case prop of + CEqual x y -> CEqual (coqAst x) (coqAst y) + CGeq x y -> CGeq (coqAst x) (coqAst y) + CFin x -> CFin (coqAst x) + CArith x -> CArith (coqAst x) + CCmp x -> CCmp (coqAst x) + CLocated c _ -> coqAst c + CType t -> CType (coqAst t) + diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index 14edb916..f5798b22 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -22,7 +22,10 @@ import Control.DeepSeq import Cryptol.Utils.PP data Located a = Located { srcRange :: !Range, thing :: !a } - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Generic, NFData) + +instance (Show a) => Show (Located a) where + show l = show (thing l) data Position = Position { line :: !Int, col :: !Int } deriving (Eq, Ord, Show, Generic, NFData) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 5e0afc4f..c1fb6e04 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -55,6 +55,8 @@ import qualified Cryptol.ModuleSystem.Name as M import qualified Cryptol.ModuleSystem.NamingEnv as M import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed)) import qualified Cryptol.Utils.Ident as M +import qualified Cryptol.ModuleSystem.Env as M +import qualified Cryptol.ModuleSystem.Monad as M import qualified Cryptol.Eval.Monad as E import qualified Cryptol.Eval.Value as E @@ -183,6 +185,8 @@ nbCommandList = "do type specialization on a closed expression" , CommandDescr [ ":eval" ] (ExprArg refEvalCmd) "evaluate an expression with the reference evaluator" + , CommandDescr [ ":ast" ] (ExprArg astOfCmd) + "print out an AST of a given term" ] commandList :: [CommandDescr] @@ -589,6 +593,18 @@ refEvalCmd str = do val <- liftModuleCmd (rethrowEvalError . R.evaluate expr) rPrint $ R.ppValue val +nameToNumber :: M.Name -> Int +nameToNumber n = M.nameUnique n + +astOfCmd :: String -> REPL () +astOfCmd str = do +-- expr <- replParseExpr str +-- (re,_,_) <- replCheckExpr (P.coqAst expr) +-- rPrint (fmap nameToNumber re) + me <- getModuleEnv + let decls = (concatMap T.mDecls (M.loadedModules me)) in + rPrint decls + typeOfCmd :: String -> REPL () typeOfCmd str = do From c568c32855336cc7337d19447fe7f6f291dc61c4 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Wed, 14 Jun 2017 16:41:47 -0700 Subject: [PATCH 02/17] :all command and :ast command work --- src/Cryptol/ModuleSystem/Name.hs | 5 ++++- src/Cryptol/REPL/Command.hs | 15 +++++++++------ src/Cryptol/TypeCheck/AST.hs | 5 ++++- src/Cryptol/TypeCheck/Type.hs | 4 +++- 4 files changed, 20 insertions(+), 9 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index ed3ae643..002e8897 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -88,7 +88,10 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int , nLoc :: !Range -- ^ Where this name was defined - } deriving (Show, Generic, NFData) + } deriving (Generic, NFData) + +instance Show Name where + show n = show (nUnique n) instance Eq Name where a == b = compare a b == EQ diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c1fb6e04..c40bca2e 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -56,7 +56,6 @@ import qualified Cryptol.ModuleSystem.NamingEnv as M import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed)) import qualified Cryptol.Utils.Ident as M import qualified Cryptol.ModuleSystem.Env as M -import qualified Cryptol.ModuleSystem.Monad as M import qualified Cryptol.Eval.Monad as E import qualified Cryptol.Eval.Value as E @@ -187,6 +186,8 @@ nbCommandList = "evaluate an expression with the reference evaluator" , CommandDescr [ ":ast" ] (ExprArg astOfCmd) "print out an AST of a given term" + , CommandDescr [ ":all" ] (ExprArg allTerms) + "print out the AST of all defined terms" ] commandList :: [CommandDescr] @@ -598,12 +599,14 @@ nameToNumber n = M.nameUnique n astOfCmd :: String -> REPL () astOfCmd str = do --- expr <- replParseExpr str --- (re,_,_) <- replCheckExpr (P.coqAst expr) --- rPrint (fmap nameToNumber re) + expr <- replParseExpr str + (re,_,_) <- replCheckExpr (P.coqAst expr) + rPrint (fmap nameToNumber re) + +allTerms :: String -> REPL () +allTerms _ = do me <- getModuleEnv - let decls = (concatMap T.mDecls (M.loadedModules me)) in - rPrint decls + rPrint (T.mDecls (last (M.loadedModules me))) typeOfCmd :: String -> REPL () typeOfCmd str = do diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index d6d5cacf..8d9b10e7 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -119,7 +119,10 @@ data Decl = Decl { dName :: !Name , dInfix :: !Bool , dFixity :: Maybe Fixity , dDoc :: Maybe String - } deriving (Show, Generic, NFData) + } deriving (Generic, NFData) + +instance Show Decl where + show d = "(Decl (" ++ show (dName d) ++ ") (" ++ show (dDefinition d) ++ ")" data DeclDef = DPrim | DExpr Expr diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index c0a31f7b..58589f88 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -45,8 +45,10 @@ data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier , tpKind :: Kind -- ^ Kind of parameter , tpName :: Maybe Name -- ^ Name from source, if any. } - deriving (Show, Generic, NFData) + deriving (Generic, NFData) +instance Show TParam where + show tp = show (tpUnique tp) -- | The internal representation of types. -- These are assumed to be kind correct. From a0cf0543c0784691eb29d3e6836f270f542fba69 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 15 Jun 2017 14:32:40 -0700 Subject: [PATCH 03/17] no longer defining new versions of Show, using different typeclass --- src/Cryptol/ModuleSystem/Name.hs | 4 +- src/Cryptol/Parser/AST.hs | 269 +++++++++++++++---------------- src/Cryptol/REPL/Command.hs | 4 +- src/Cryptol/TypeCheck/AST.hs | 78 ++++++++- src/Cryptol/TypeCheck/Type.hs | 4 +- 5 files changed, 211 insertions(+), 148 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 002e8897..2509feab 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -88,10 +88,8 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int , nLoc :: !Range -- ^ Where this name was defined - } deriving (Generic, NFData) + } deriving (Generic, NFData, Show) -instance Show Name where - show n = show (nUnique n) instance Eq Name where a == b = compare a b == EQ diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index ab6963bb..8b259ce5 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -64,7 +64,6 @@ module Cryptol.Parser.AST , Located(..) , LPName, LString, LIdent , NoPos(..) - , CoqAst(..) -- * Pretty-printing , cppKind, ppSelector @@ -173,10 +172,10 @@ data Bind name = Bind { bName :: Located name -- ^ Defined thing , bPragmas :: [Pragma] -- ^ Optional pragmas , bMono :: Bool -- ^ Is this a monomorphic binding , bDoc :: Maybe String -- ^ Optional doc string - } deriving (Eq, Generic, NFData, Functor) + } deriving (Eq, Generic, NFData, Functor, Show) -instance (Show name) => Show (Bind name) where - show b = "(Bind (" ++ show (bName b) ++ ") (" ++ show (bDef b) ++ "))" +-- instance (Show name) => Show (Bind name) where +-- show b = "(Bind (" ++ show (bName b) ++ ") (" ++ show (bDef b) ++ "))" type LBindDef = Located (BindDef PName) @@ -186,10 +185,10 @@ data BindDef name = DPrim data Fixity = Fixity { fAssoc :: !Assoc , fLevel :: !Int - } deriving (Eq, Generic, NFData) + } deriving (Eq, Generic, NFData, Show) -instance Show Fixity where - show _ = "" +-- instance Show Fixity where +-- show _ = "" data FixityCmp = FCError | FCLeft @@ -991,156 +990,156 @@ instance NoPos (Prop name) where CLocated c _ -> noPos c CType t -> CType (noPos t) ---Typeclass for prettying up the AST for exporting to Coq ---Similar to NoPos above -class CoqAst t where - coqAst :: t -> t +-- --Typeclass for prettying up the AST for exporting to Coq +-- --Similar to NoPos above +-- class CoqAst t where +-- coqAst :: t -> t --- WARNING: This does not call `coqAst` on the `thing` inside -instance CoqAst (Located t) where - coqAst x = x { srcRange = rng } - where rng = Range { from = Position 0 0, to = Position 0 0, source = "" } +-- -- WARNING: This does not call `coqAst` on the `thing` inside +-- instance CoqAst (Located t) where +-- coqAst x = x { srcRange = rng } +-- where rng = Range { from = Position 0 0, to = Position 0 0, source = "" } -instance CoqAst t => CoqAst (Named t) where - coqAst t = Named { name = coqAst (name t), value = coqAst (value t) } +-- instance CoqAst t => CoqAst (Named t) where +-- coqAst t = Named { name = coqAst (name t), value = coqAst (value t) } -instance CoqAst t => CoqAst [t] where coqAst = fmap coqAst -instance CoqAst t => CoqAst (Maybe t) where coqAst = fmap coqAst +-- instance CoqAst t => CoqAst [t] where coqAst = fmap coqAst +-- instance CoqAst t => CoqAst (Maybe t) where coqAst = fmap coqAst -instance CoqAst (Program name) where - coqAst (Program x) = Program (coqAst x) +-- instance CoqAst (Program name) where +-- coqAst (Program x) = Program (coqAst x) -instance CoqAst (Module name) where - coqAst m = Module { mName = mName m - , mImports = coqAst (mImports m) - , mDecls = coqAst (mDecls m) - } +-- instance CoqAst (Module name) where +-- coqAst m = Module { mName = mName m +-- , mImports = coqAst (mImports m) +-- , mDecls = coqAst (mDecls m) +-- } -instance CoqAst (TopDecl name) where - coqAst decl = - case decl of - Decl x -> Decl (coqAst x) - TDNewtype n -> TDNewtype(coqAst n) - Include x -> Include (coqAst x) +-- instance CoqAst (TopDecl name) where +-- coqAst decl = +-- case decl of +-- Decl x -> Decl (coqAst x) +-- TDNewtype n -> TDNewtype(coqAst n) +-- Include x -> Include (coqAst x) -instance CoqAst a => CoqAst (TopLevel a) where - coqAst tl = tl { tlValue = coqAst (tlValue tl) } +-- instance CoqAst a => CoqAst (TopLevel a) where +-- coqAst tl = tl { tlValue = coqAst (tlValue tl) } -instance CoqAst (Decl name) where - coqAst decl = - case decl of - DSignature x y -> DSignature (coqAst x) (coqAst y) - DPragma x y -> DPragma (coqAst x) (coqAst y) - DPatBind x y -> DPatBind (coqAst x) (coqAst y) - DFixity f ns -> DFixity f (coqAst ns) - DBind x -> DBind (coqAst x) - DType x -> DType (coqAst x) - DLocated x _ -> coqAst x +-- instance CoqAst (Decl name) where +-- coqAst decl = +-- case decl of +-- DSignature x y -> DSignature (coqAst x) (coqAst y) +-- DPragma x y -> DPragma (coqAst x) (coqAst y) +-- DPatBind x y -> DPatBind (coqAst x) (coqAst y) +-- DFixity f ns -> DFixity f (coqAst ns) +-- DBind x -> DBind (coqAst x) +-- DType x -> DType (coqAst x) +-- DLocated x _ -> coqAst x -instance CoqAst (Newtype name) where - coqAst n = Newtype { nName = coqAst (nName n) - , nParams = nParams n - , nBody = coqAst (nBody n) - } +-- instance CoqAst (Newtype name) where +-- coqAst n = Newtype { nName = coqAst (nName n) +-- , nParams = nParams n +-- , nBody = coqAst (nBody n) +-- } -instance CoqAst (Bind name) where - coqAst x = Bind { bName = coqAst (bName x) - , bParams = coqAst (bParams x) - , bDef = coqAst (bDef x) - , bSignature = coqAst (bSignature x) - , bInfix = bInfix x - , bFixity = bFixity x - , bPragmas = coqAst (bPragmas x) - , bMono = bMono x - , bDoc = bDoc x - } +-- instance CoqAst (Bind name) where +-- coqAst x = Bind { bName = coqAst (bName x) +-- , bParams = coqAst (bParams x) +-- , bDef = coqAst (bDef x) +-- , bSignature = coqAst (bSignature x) +-- , bInfix = bInfix x +-- , bFixity = bFixity x +-- , bPragmas = coqAst (bPragmas x) +-- , bMono = bMono x +-- , bDoc = bDoc x +-- } -instance CoqAst Pragma where - coqAst p@(PragmaNote {}) = p - coqAst p@(PragmaProperty) = p +-- instance CoqAst Pragma where +-- coqAst p@(PragmaNote {}) = p +-- coqAst p@(PragmaProperty) = p -instance CoqAst (TySyn name) where - coqAst (TySyn x y z) = TySyn (coqAst x) (coqAst y) (coqAst z) +-- instance CoqAst (TySyn name) where +-- coqAst (TySyn x y z) = TySyn (coqAst x) (coqAst y) (coqAst z) -instance CoqAst (Expr name) where - coqAst expr = - case expr of - EVar x -> EVar x - ELit x -> ELit x - ETuple x -> ETuple (coqAst x) - ERecord x -> ERecord (coqAst x) - ESel x y -> ESel (coqAst x) y - EList x -> EList (coqAst x) - EFromTo x y z -> EFromTo (coqAst x) (coqAst y) (coqAst z) - EInfFrom x y -> EInfFrom (coqAst x) (coqAst y) - EComp x y -> EComp (coqAst x) (coqAst y) - EApp x y -> EApp (coqAst x) (coqAst y) - EAppT x y -> EAppT (coqAst x) (coqAst y) - EIf x y z -> EIf (coqAst x) (coqAst y) (coqAst z) - EWhere x y -> EWhere (coqAst x) (coqAst y) - ETyped x y -> ETyped (coqAst x) (coqAst y) - ETypeVal x -> ETypeVal (coqAst x) - EFun x y -> EFun (coqAst x) (coqAst y) - ELocated x _ -> coqAst x +-- instance CoqAst (Expr name) where +-- coqAst expr = +-- case expr of +-- EVar x -> EVar x +-- ELit x -> ELit x +-- ETuple x -> ETuple (coqAst x) +-- ERecord x -> ERecord (coqAst x) +-- ESel x y -> ESel (coqAst x) y +-- EList x -> EList (coqAst x) +-- EFromTo x y z -> EFromTo (coqAst x) (coqAst y) (coqAst z) +-- EInfFrom x y -> EInfFrom (coqAst x) (coqAst y) +-- EComp x y -> EComp (coqAst x) (coqAst y) +-- EApp x y -> EApp (coqAst x) (coqAst y) +-- EAppT x y -> EAppT (coqAst x) (coqAst y) +-- EIf x y z -> EIf (coqAst x) (coqAst y) (coqAst z) +-- EWhere x y -> EWhere (coqAst x) (coqAst y) +-- ETyped x y -> ETyped (coqAst x) (coqAst y) +-- ETypeVal x -> ETypeVal (coqAst x) +-- EFun x y -> EFun (coqAst x) (coqAst y) +-- ELocated x _ -> coqAst x - EParens e -> EParens (coqAst e) - EInfix x y f z-> EInfix (coqAst x) y f (coqAst z) +-- EParens e -> EParens (coqAst e) +-- EInfix x y f z-> EInfix (coqAst x) y f (coqAst z) -instance CoqAst (TypeInst name) where - coqAst (PosInst ts) = PosInst (coqAst ts) - coqAst (NamedInst fs) = NamedInst (coqAst fs) +-- instance CoqAst (TypeInst name) where +-- coqAst (PosInst ts) = PosInst (coqAst ts) +-- coqAst (NamedInst fs) = NamedInst (coqAst fs) -instance CoqAst (Match name) where - coqAst (Match x y) = Match (coqAst x) (coqAst y) - coqAst (MatchLet b) = MatchLet (coqAst b) +-- instance CoqAst (Match name) where +-- coqAst (Match x y) = Match (coqAst x) (coqAst y) +-- coqAst (MatchLet b) = MatchLet (coqAst b) -instance CoqAst (Pattern name) where - coqAst pat = - case pat of - PVar x -> PVar (coqAst x) - PWild -> PWild - PTuple x -> PTuple (coqAst x) - PRecord x -> PRecord (coqAst x) - PList x -> PList (coqAst x) - PTyped x y -> PTyped (coqAst x) (coqAst y) - PSplit x y -> PSplit (coqAst x) (coqAst y) - PLocated x _ -> coqAst x +-- instance CoqAst (Pattern name) where +-- coqAst pat = +-- case pat of +-- PVar x -> PVar (coqAst x) +-- PWild -> PWild +-- PTuple x -> PTuple (coqAst x) +-- PRecord x -> PRecord (coqAst x) +-- PList x -> PList (coqAst x) +-- PTyped x y -> PTyped (coqAst x) (coqAst y) +-- PSplit x y -> PSplit (coqAst x) (coqAst y) +-- PLocated x _ -> coqAst x -instance CoqAst (Schema name) where - coqAst (Forall x y z _) = Forall (coqAst x) (coqAst y) (coqAst z) Nothing +-- instance CoqAst (Schema name) where +-- coqAst (Forall x y z _) = Forall (coqAst x) (coqAst y) (coqAst z) Nothing -instance CoqAst (TParam name) where - coqAst (TParam x y _) = TParam x y Nothing +-- instance CoqAst (TParam name) where +-- coqAst (TParam x y _) = TParam x y Nothing -instance CoqAst (Type name) where - coqAst ty = - case ty of - TWild -> TWild - TApp x y -> TApp x (coqAst y) - TUser x y -> TUser x (coqAst y) - TRecord x -> TRecord (coqAst x) - TTuple x -> TTuple (coqAst x) - TFun x y -> TFun (coqAst x) (coqAst y) - TSeq x y -> TSeq (coqAst x) (coqAst y) - TBit -> TBit - TInf -> TInf - TNum n -> TNum n - TChar n -> TChar n - TLocated x _ -> coqAst x - TParens x -> TParens (coqAst x) - TInfix x y f z-> TInfix (coqAst x) y f (coqAst z) +-- instance CoqAst (Type name) where +-- coqAst ty = +-- case ty of +-- TWild -> TWild +-- TApp x y -> TApp x (coqAst y) +-- TUser x y -> TUser x (coqAst y) +-- TRecord x -> TRecord (coqAst x) +-- TTuple x -> TTuple (coqAst x) +-- TFun x y -> TFun (coqAst x) (coqAst y) +-- TSeq x y -> TSeq (coqAst x) (coqAst y) +-- TBit -> TBit +-- TInf -> TInf +-- TNum n -> TNum n +-- TChar n -> TChar n +-- TLocated x _ -> coqAst x +-- TParens x -> TParens (coqAst x) +-- TInfix x y f z-> TInfix (coqAst x) y f (coqAst z) -instance CoqAst (Prop name) where - coqAst prop = - case prop of - CEqual x y -> CEqual (coqAst x) (coqAst y) - CGeq x y -> CGeq (coqAst x) (coqAst y) - CFin x -> CFin (coqAst x) - CArith x -> CArith (coqAst x) - CCmp x -> CCmp (coqAst x) - CLocated c _ -> coqAst c - CType t -> CType (coqAst t) +-- instance CoqAst (Prop name) where +-- coqAst prop = +-- case prop of +-- CEqual x y -> CEqual (coqAst x) (coqAst y) +-- CGeq x y -> CGeq (coqAst x) (coqAst y) +-- CFin x -> CFin (coqAst x) +-- CArith x -> CArith (coqAst x) +-- CCmp x -> CCmp (coqAst x) +-- CLocated c _ -> coqAst c +-- CType t -> CType (coqAst t) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c40bca2e..2fa447b3 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -600,13 +600,13 @@ nameToNumber n = M.nameUnique n astOfCmd :: String -> REPL () astOfCmd str = do expr <- replParseExpr str - (re,_,_) <- replCheckExpr (P.coqAst expr) + (re,_,_) <- replCheckExpr (P.noPos expr) rPrint (fmap nameToNumber re) allTerms :: String -> REPL () allTerms _ = do me <- getModuleEnv - rPrint (T.mDecls (last (M.loadedModules me))) + rPutStrLn (T.showAst (T.mDecls (last (M.loadedModules me)))) typeOfCmd :: String -> REPL () typeOfCmd str = do diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 8d9b10e7..145cdc04 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -44,6 +44,9 @@ import Control.DeepSeq import Data.Map (Map) import qualified Data.IntMap as IntMap + + + -- | A Cryptol module. data Module = Module { mName :: !ModName , mExports :: ExportSpec Name @@ -54,7 +57,6 @@ data Module = Module { mName :: !ModName } deriving (Show, Generic, NFData) - data Expr = EList [Expr] Type -- ^ List value (with type of elements) | ETuple [Expr] -- ^ Tuple value | ERec [(Ident,Expr)] -- ^ Record value @@ -112,6 +114,7 @@ groupDecls dg = case dg of Recursive ds -> ds NonRecursive d -> [d] + data Decl = Decl { dName :: !Name , dSignature :: Schema , dDefinition :: DeclDef @@ -119,15 +122,80 @@ data Decl = Decl { dName :: !Name , dInfix :: !Bool , dFixity :: Maybe Fixity , dDoc :: Maybe String - } deriving (Generic, NFData) - -instance Show Decl where - show d = "(Decl (" ++ show (dName d) ++ ") (" ++ show (dDefinition d) ++ ")" + } deriving (Generic, NFData, Show) data DeclDef = DPrim | DExpr Expr deriving (Show, Generic, NFData) +-- ShowAST prints out just enough information to model the program in Coq +class ShowAST t where + showAst :: t -> String + +instance ShowAST Expr where + showAst (EList es _) = "(EList " ++ showAst es ++ ")" + showAst (ETuple es) = "(ETuple " ++ showAst es ++ ")" + showAst (ERec ides) = "(ERec " ++ showAst ides ++ ")" + showAst (ESel e s) = "(ESel " ++ showAst e ++ " " ++ showAst s ++ ")" + showAst (EIf c t f) = "(EIf " ++ showAst c ++ " " ++ showAst t ++ " " ++ showAst f ++ ")" + showAst (EComp _ _ e mss) = "(EComp " ++ showAst e ++ " " ++ showAst mss ++ ")" + showAst (EVar n) = "(EVar " ++ showAst n ++ ")" + showAst (EApp fe ae) = "(EApp " ++ showAst fe ++ " " ++ showAst ae ++ ")" + showAst (EAbs n _ e) = "(EAbs " ++ showAst n ++ " " ++ showAst e ++ ")" + showAst (EProofAbs p e) = "(EProofAbs " ++ show p ++ showAst e ++ ")" + showAst (EProofApp e) = "(EProofApp " ++ showAst e ++ ")" + showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" + --NOTE: erase all types for now, so these don't matter + showAst (ETAbs {-tp-}_ e) = showAst e --"(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" + showAst (ETApp e {-t-}_) = showAst e -- "(ETapp " ++ showAst e ++ " " ++ showAst t ++ ")" + + +instance (ShowAST a, ShowAST b) => ShowAST (a,b) where + showAst (x,y) = "(" ++ showAst x ++ "," ++ showAst y ++ ")" + +instance ShowAST Ident where + showAst i = show i + +instance ShowAST Type where + showAst t = show t + +instance ShowAST Selector where + showAst s = show s + +instance ShowAST Match where + showAst (From n _ _ e) = "(From " ++ showAst n ++ " " ++ showAst e ++ ")" + showAst (Let d) = "(Let " ++ showAst d ++ ")" + +instance ShowAST Decl where + showAst d = "(Decl " ++ showAst (dName d) ++ " " ++ showAst (dDefinition d) ++ ")" + +instance ShowAST DeclDef where + showAst DPrim = show DPrim + showAst (DExpr e) = "(DExpr " ++ (showAst e) ++ ")" + +instance ShowAST DeclGroup where + showAst (Recursive ds) = showAst ds + showAst (NonRecursive d) = showAst d + +showASTList :: (ShowAST a) => [a] -> String +showASTList [] = "" +showASTList [x] = showAst x +showASTList (x : y) = (showAst x) ++ "," ++ showASTList y + +instance (ShowAST a) => ShowAST [a] where + showAst a = "[" ++ showASTList a ++ "]" + +instance ShowAST TParam where + showAst tp = show (tpUnique tp) + +instance ShowAST Name where + showAst n = show (nameUnique n) + +-- instance ShowAST Expr where +-- showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ showAst e ++ ")" +-- showAst e = show e + + -------------------------------------------------------------------------------- diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 58589f88..fc47ee3d 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -45,10 +45,8 @@ data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier , tpKind :: Kind -- ^ Kind of parameter , tpName :: Maybe Name -- ^ Name from source, if any. } - deriving (Generic, NFData) + deriving (Generic, NFData, Show) -instance Show TParam where - show tp = show (tpUnique tp) -- | The internal representation of types. -- These are assumed to be kind correct. From 237a1bac7ebee92814c9f4a21ca4d7586c339e34 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 15 Jun 2017 17:01:17 -0700 Subject: [PATCH 04/17] don't print out proof things for now --- src/Cryptol/TypeCheck/AST.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 145cdc04..b2fce718 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -142,10 +142,10 @@ instance ShowAST Expr where showAst (EVar n) = "(EVar " ++ showAst n ++ ")" showAst (EApp fe ae) = "(EApp " ++ showAst fe ++ " " ++ showAst ae ++ ")" showAst (EAbs n _ e) = "(EAbs " ++ showAst n ++ " " ++ showAst e ++ ")" - showAst (EProofAbs p e) = "(EProofAbs " ++ show p ++ showAst e ++ ")" - showAst (EProofApp e) = "(EProofApp " ++ showAst e ++ ")" showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" --NOTE: erase all types for now, so these don't matter + showAst (EProofAbs {-p-}_ e) = showAst e --"(EProofAbs " ++ show p ++ showAst e ++ ")" + showAst (EProofApp e) = showAst e --"(EProofApp " ++ showAst e ++ ")" showAst (ETAbs {-tp-}_ e) = showAst e --"(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" showAst (ETApp e {-t-}_) = showAst e -- "(ETapp " ++ showAst e ++ " " ++ showAst t ++ ")" From ab0926e4eb1e29cffc71ee7ff4fe474ce42db785 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 15 Jun 2017 17:20:32 -0700 Subject: [PATCH 05/17] print out all the declarations, not just current module --- src/Cryptol/REPL/Command.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 2fa447b3..c2e214d4 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -606,7 +606,7 @@ astOfCmd str = do allTerms :: String -> REPL () allTerms _ = do me <- getModuleEnv - rPutStrLn (T.showAst (T.mDecls (last (M.loadedModules me)))) + rPutStrLn (T.showAst (concatMap T.mDecls (M.loadedModules me))) typeOfCmd :: String -> REPL () typeOfCmd str = do From e28c0c43db1d20d9bcd4000683705bd5a9c8f893 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Fri, 16 Jun 2017 17:37:54 -0700 Subject: [PATCH 06/17] explicit printing of decl groups --- src/Cryptol/TypeCheck/AST.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index b2fce718..65532e92 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -174,8 +174,8 @@ instance ShowAST DeclDef where showAst (DExpr e) = "(DExpr " ++ (showAst e) ++ ")" instance ShowAST DeclGroup where - showAst (Recursive ds) = showAst ds - showAst (NonRecursive d) = showAst d + showAst (Recursive ds) = "(Recursive " ++ showAst ds ++ ")" + showAst (NonRecursive d) = "(NonRecursive " ++ showAst d ++ ")" showASTList :: (ShowAST a) => [a] -> String showASTList [] = "" From 76dacbe1cdc838a003763db6853fee54527d5c69 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Tue, 20 Jun 2017 12:20:56 -0700 Subject: [PATCH 07/17] types print out correctly --- src/Cryptol/TypeCheck/AST.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 65532e92..96c7a68d 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -143,11 +143,11 @@ instance ShowAST Expr where showAst (EApp fe ae) = "(EApp " ++ showAst fe ++ " " ++ showAst ae ++ ")" showAst (EAbs n _ e) = "(EAbs " ++ showAst n ++ " " ++ showAst e ++ ")" showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" - --NOTE: erase all types for now, so these don't matter + showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" + showAst (ETApp e t) = "(ETApp " ++ showAst e ++ " " ++ showAst t ++ ")" + --NOTE: erase all proofs for now, so these don't matter showAst (EProofAbs {-p-}_ e) = showAst e --"(EProofAbs " ++ show p ++ showAst e ++ ")" showAst (EProofApp e) = showAst e --"(EProofApp " ++ showAst e ++ ")" - showAst (ETAbs {-tp-}_ e) = showAst e --"(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" - showAst (ETApp e {-t-}_) = showAst e -- "(ETapp " ++ showAst e ++ " " ++ showAst t ++ ")" instance (ShowAST a, ShowAST b) => ShowAST (a,b) where @@ -157,7 +157,7 @@ instance ShowAST Ident where showAst i = show i instance ShowAST Type where - showAst t = show t + showAst t = "(" ++ show t ++ ")" instance ShowAST Selector where showAst s = show s From b45683160293a807a3208d7a448d1d4a3677ee77 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Mon, 26 Jun 2017 13:23:08 -0700 Subject: [PATCH 08/17] give better names to type variables,and include a tool to print the AST --- cryptol-ast | 6 ++++++ src/Cryptol/TypeCheck/AST.hs | 30 ++++++++++++++++-------------- 2 files changed, 22 insertions(+), 14 deletions(-) create mode 100755 cryptol-ast diff --git a/cryptol-ast b/cryptol-ast new file mode 100755 index 00000000..ff61862a --- /dev/null +++ b/cryptol-ast @@ -0,0 +1,6 @@ +#!/bin/bash +CRYPTOL=/Users/emullen/cryptol/dist/build/Cryptol/cryptol +IN="$1" + +echo ":all" | "$CRYPTOL" "$IN" | cut -c 7- + diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 96c7a68d..baa250b4 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -34,7 +34,7 @@ import Cryptol.Parser.AST ( Selector(..),Pragma(..) , Import(..), ImportSpec(..), ExportType(..) , ExportSpec(..), isExportedBind , isExportedType, Fixity(..) ) -import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent) +import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent,unpackIdent) import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Type @@ -145,22 +145,27 @@ instance ShowAST Expr where showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" showAst (ETApp e t) = "(ETApp " ++ showAst e ++ " " ++ showAst t ++ ")" - --NOTE: erase all proofs for now, so these don't matter + --NOTE: erase all proofs for now (change the following two lines to change that) showAst (EProofAbs {-p-}_ e) = showAst e --"(EProofAbs " ++ show p ++ showAst e ++ ")" showAst (EProofApp e) = showAst e --"(EProofApp " ++ showAst e ++ ")" - instance (ShowAST a, ShowAST b) => ShowAST (a,b) where showAst (x,y) = "(" ++ showAst x ++ "," ++ showAst y ++ ")" -instance ShowAST Ident where +instance ShowAST Int where showAst i = show i +instance ShowAST Ident where + showAst i = show (unpackIdent i) + instance ShowAST Type where + showAst (TUser n lt t) = "(TUser " ++ showAst n ++ " " ++ showAst lt ++ " " ++ showAst t ++ ")" showAst t = "(" ++ show t ++ ")" instance ShowAST Selector where - showAst s = show s + showAst (TupleSel n _) = "(TupleSel " ++ showAst n ++ ")" + showAst (RecordSel n _) = "(RecordSel " ++ showAst n ++ ")" + showAst (ListSel n _) = "(ListSel " ++ showAst n ++ ")" instance ShowAST Match where showAst (From n _ _ e) = "(From " ++ showAst n ++ " " ++ showAst e ++ ")" @@ -185,21 +190,18 @@ showASTList (x : y) = (showAst x) ++ "," ++ showASTList y instance (ShowAST a) => ShowAST [a] where showAst a = "[" ++ showASTList a ++ "]" +instance (ShowAST a) => ShowAST (Maybe a) where + showAst Nothing = "" + showAst (Just x) = showAst x + instance ShowAST TParam where - showAst tp = show (tpUnique tp) + showAst tp = showAst (tpName tp) instance ShowAST Name where - showAst n = show (nameUnique n) - --- instance ShowAST Expr where --- showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ showAst e ++ ")" --- showAst e = show e - + showAst n = "(" ++ show (nameUnique n) ++ "," ++ showAst (nameIdent n) ++ ")" -------------------------------------------------------------------------------- - - -- | Construct a primitive, given a map to the unique names of the Cryptol -- module. ePrim :: PrimMap -> Ident -> Expr From a67e3501757bda906bf8d8168b4844689d89c1ce Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Mon, 26 Jun 2017 13:32:31 -0700 Subject: [PATCH 09/17] got rid of the pesky ascii logo --- cryptol-ast | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-ast b/cryptol-ast index ff61862a..d1b8505b 100755 --- a/cryptol-ast +++ b/cryptol-ast @@ -2,5 +2,5 @@ CRYPTOL=/Users/emullen/cryptol/dist/build/Cryptol/cryptol IN="$1" -echo ":all" | "$CRYPTOL" "$IN" | cut -c 7- +echo ":all" | "$CRYPTOL" "$IN" | cut -c 7- | tail -n 1 From 3dfb3e147eb08402d113031acaccbeabfaf1d520 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Mon, 26 Jun 2017 15:27:36 -0700 Subject: [PATCH 10/17] adding some examples --- examples/HMAC.cry | 72 +++++++++++++++++++++++++++++++++++++++++++ examples/builtins.cry | 38 +++++++++++++++++++++++ examples/mini.cry | 28 +++++++++++++++++ 3 files changed, 138 insertions(+) create mode 100644 examples/HMAC.cry create mode 100644 examples/builtins.cry create mode 100644 examples/mini.cry diff --git a/examples/HMAC.cry b/examples/HMAC.cry new file mode 100644 index 00000000..58378f45 --- /dev/null +++ b/examples/HMAC.cry @@ -0,0 +1,72 @@ +//////////////////////////////////////////////////////////////// +// Copyright 2016 Galois, Inc. All Rights Reserved +// +// Authors: +// Aaron Tomb : atomb@galois.com +// Nathan Collins : conathan@galois.com +// Joey Dodds : jdodds@galois.com +// +// Licensed under the Apache License, Version 2.0 (the "License"). +// You may not use this file except in compliance with the License. +// A copy of the License is located at +// +// http://aws.amazon.com/apache2.0 +// +// or in the "license" file accompanying this file. This file is distributed +// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either +// express or implied. See the License for the specific language governing +// permissions and limitations under the License. +// +//////////////////////////////////////////////////////////////// + +module HMAC where + +import SHA256 + +//////// Functional version //////// + +hmacSHA256 : {pwBytes, msgBytes} + (fin pwBytes, fin msgBytes + , 32 >= width msgBytes + , 64 >= width (8*pwBytes) + , 64 >= width (8 * (64 + msgBytes)) + ) => [pwBytes][8] -> [msgBytes][8] -> [256] +hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256 + +kinit : { pwBytes, blockLength, digest } + ( fin pwBytes, fin blockLength, fin digest ) + => ([pwBytes][8] -> [8*digest]) + -> [pwBytes][8] + -> [blockLength][8] +kinit hash key = + if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)]) + then take `{blockLength} (split (hash key) # (zero : [blockLength][8])) + else take `{blockLength} (key # (zero : [blockLength][8])) + +// Due to limitations of the type system we must accept two +// separate arguments (both aledgedly the same) for two +// separate length inputs. +hmac : { msgBytes, pwBytes, digest, blockLength } + ( fin pwBytes, fin digest, fin blockLength ) + => ([blockLength + msgBytes][8] -> [8*digest]) + -> ([blockLength + digest][8] -> [8*digest]) + -> ([pwBytes][8] -> [8*digest]) + -> [pwBytes][8] + -> [msgBytes][8] + -> [digest*8] +hmac hash hash2 hash3 key message = hash2 (okey # internal) + where + ks : [blockLength][8] + ks = kinit hash3 key + okey = [k ^ 0x5C | k <- ks] + ikey = [k ^ 0x36 | k <- ks] + internal = split (hash (ikey # message)) + + + + + + + + + diff --git a/examples/builtins.cry b/examples/builtins.cry new file mode 100644 index 00000000..85e2061f --- /dev/null +++ b/examples/builtins.cry @@ -0,0 +1,38 @@ +//Here's a test of some builtin operators +//nothing too deep, just making sure they all work out + +t : [8] +t = if True then 5 else 4 //5 + +f : [8] +f = if False then 3 else 5 //5 + +times : [8] +times = 5 * 1 * 2 * 3 //30 + +div : [8] +div = (((30/1)/2)/3) //5 + +mod : [8] +mod = 205%10 //5 + +exp : [8] +exp = 2^^7 //128 + +lgtest : [8] +lgtest = lg2 128 //7 + +p : [8] +p = 3+2 //5 + +m : [8] +m = 8-3 //5 + +neg : [8] +neg = -(-5) //5 + +comp : [8] +comp = ~250 //5 + + + diff --git a/examples/mini.cry b/examples/mini.cry new file mode 100644 index 00000000..3e9bb1c8 --- /dev/null +++ b/examples/mini.cry @@ -0,0 +1,28 @@ +id : [32] -> [32] +id x = rec x + where rec k = if (k == 0) then 0 else 1 + rec (k + (-1)) + + +inflist = [1 ... ] : [_][8] + +rc = {x = 3 : [8], y = 5 : [8]} + +my_true = rc.x + +tup = (1 : [8], 2 : [8], 3 : [8], 4 : [8]) + +my_3 = tup.2 + +sup = y where y = 3 : [8] + + +gf28Add : {n} (fin n) => [n][8] -> [8] +gf28Add ps = sums ! 0 + where sums = [zero] # [ p ^ s | p <- ps | s <- sums ] + +gex = gf28Add [1,2] + +sum : [_][8] -> [_][8] +sum x = rec + where rec = [ p + q | p <- x | q <- [1,2,3,4] ] + \ No newline at end of file From f80d791c97ec4eda3029ec80139e326bb37d9dcc Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Tue, 27 Jun 2017 14:00:45 -0700 Subject: [PATCH 11/17] HMAC example now loads into cryptol --- examples/SHA256.cry | 194 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) create mode 100644 examples/SHA256.cry diff --git a/examples/SHA256.cry b/examples/SHA256.cry new file mode 100644 index 00000000..36a663e2 --- /dev/null +++ b/examples/SHA256.cry @@ -0,0 +1,194 @@ +/* + * Copyright (c) 2013-2016 Galois, Inc. + * Distributed under the terms of the BSD3 license (see LICENSE file) + * + * @tmd - 24 April 2015 - took Ian's SHA512, converted to SHA256 + * @ian - 15 August 2015 - he lies, probably ment 2014. + * + * This is a very simple implementation of SHA256, designed to be as clearly + * mathced to the specification in NIST's FIPS-PUB-180-4 as possible + * + * * The output correctly matches on all test vectors from + * http://csrc.nist.gov/groups/ST/toolkit/documents/Examples/SHA256.pdf + */ +module SHA256 where + +/* + * SHA256 Functions : Section 4.1.2 + */ + +Ch : [32] -> [32] -> [32] -> [32] +Ch x y z = (x && y) ^ (~x && z) + +Maj : [32] -> [32] -> [32] -> [32] +Maj x y z = (x && y) ^ (x && z) ^ (y && z) + +S0 : [32] -> [32] +S0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22) + +S1 : [32] -> [32] +S1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25) + +s0 : [32] -> [32] +s0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3) + +s1 : [32] -> [32] +s1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10) + +/* + * SHA256 Constants : Section 4.2.2 + */ + +K : [64][32] +K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, + 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, + 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, + 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, + 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, + 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, + 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, + 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2 + ] + +/* + * Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1 + */ +preprocess : {msgLen,contentLen,chunks,padding} + ( fin msgLen + , 64 >= width msgLen // message width fits in a word + , contentLen == msgLen + 65 // message + header + , chunks == (contentLen+511) / 512 + , padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0 + ) + => [msgLen] -> [chunks][512] +preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64])) + +/* + * SHA256 Initial Hash Value : Section 5.3.3 + */ + +H0 : [8][32] +H0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, + 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19] + +/* + * The SHA256 Hash computation : Section 6.2.2 + * + * We have split the computation into a message scheduling function, corresponding + * to step 1 in the documents loop, and a compression function, corresponding to steps 2-4. + */ + +SHA256MessageSchedule : [16][32] -> [64][32] +SHA256MessageSchedule M = W where + W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ] + + + +SHA256Compress : [8][32] -> [64][32] -> [8][32] +SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where + T1 = [h + S1 e + Ch e f g + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W] + T2 = [S0 a + Maj a b c | a <- as | b <- bs | c <- cs] + hs = take `{65} ([H@7] # gs) + gs = take `{65} ([H@6] # fs) + fs = take `{65} ([H@5] # es) + es = take `{65} ([H@4] # [d + t1 | d <- ds | t1 <- T1]) + ds = take `{65} ([H@3] # cs) + cs = take `{65} ([H@2] # bs) + bs = take `{65} ([H@1] # as) + as = take `{65} ([H@0] # [t1 + t2 | t1 <- T1 | t2 <- T2]) + +SHA256Block : [8][32] -> [16][32] -> [8][32] +SHA256Block H M = SHA256Compress H (SHA256MessageSchedule M) + +//////// Functional/idiomatic top level //////// + +/* + * The SHA256' function hashes a preprocessed sequence of blocks with the + * compression function. The SHA256 function hashes a sequence of bytes, and + * is more likely the function that will be similar to those seein in an + * implementation to be verified. + */ + +SHA256' : {a} (fin a) => [a][16][32] -> [8][32] +SHA256' blocks = hash!0 where + hash = [H0] # [SHA256Block h b | h <- hash | b <- blocks] + +SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256] +SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)]) + +property katsPass = ~zero == [test == kat | (test,kat) <- kats ] + +kats = [ (SHA256 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" + , 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1) + , (SHA256 "" + ,0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) + , (SHA256 "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + , 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1) + // , ([0x61 | i <- [1..1000000] : [_][32]] + // , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0) + ] + +//////// Imperative top level //////// + +type SHA256State = { h : [8][32] + , block : [64][8] + , n : [16] + , sz : [64] + } + +SHA256Init : SHA256State +SHA256Init = { h = H0 + , block = zero + , n = 0 + , sz = 0 + } + +SHA256Update1 : SHA256State -> [8] -> SHA256State +SHA256Update1 s b = + if s.n == 64 + then { h = SHA256Block s.h (split (join s.block)) + , block = [b] # zero + , n = 1 + , sz = s.sz + 8 + } + else { h = s.h + , block = update s.block s.n b + , n = s.n + 1 + , sz = s.sz + 8 + } + +SHA256Update : {n} (fin n) => SHA256State -> [n][8] -> SHA256State +SHA256Update sinit bs = ss!0 + where ss = [sinit] # [ SHA256Update1 s b | s <- ss | b <- bs ] + +update : {a, b, c} (fin c, c >= width (2 ^^ c - 1)) => [b]a -> [c] -> a -> [min b (2 ^^ c)]a +update a i x = [ if j == i then x else e | e <- a | j <- [0 ..] ] + +// Add padding and size and process the final block. +SHA256Final : SHA256State -> [256] +SHA256Final s = join (SHA256Block h b') + // Because the message is always made up of bytes, and the size is a + // fixed number of bytes, the 1 pad will always be at least a byte. + where s' = SHA256Update1 s 0x80 + // Don't need to add zeros. They're already there. Just update + // the count of bytes in this block. After adding the 1 pad, there + // are two possible cases: the size will fit in the current block, + // or it won't. + (h, b) = if s'.n <= 56 then (s'.h, s'.block) + else (SHA256Block s'.h (split (join s'.block)), zero) + b' = split (join b || (zero # s.sz)) + +SHA256Imp : {a} (64 >= width (8*a)) => [a][8] -> [256] +SHA256Imp msg = SHA256Final (SHA256Update SHA256Init msg) + +property katsPassImp = ~zero == [test == kat | (test,kat) <- katsImp ] + +katsImp = [ (SHA256Imp "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1), (SHA256Imp "" + , 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855) + , (SHA256Imp "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + , 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1) + // , ([0x61 | i <- [1..1000000] : [_][32]] + // , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0) + ] + +property imp_correct msg = SHA256 msg == SHA256Imp msg \ No newline at end of file From 3eab3eb6cbd24f749cef9742cba27a398fc89610 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 6 Jul 2017 16:51:25 -0700 Subject: [PATCH 12/17] lots of running examples --- examples/append.cry | 13 ++++++++++ examples/builtin_lifting.cry | 48 ++++++++++++++++++++++++++++++++++++ examples/demote.cry | 5 ++++ examples/props.cry | 27 ++++++++++++++++++++ examples/split.cry | 10 ++++++++ examples/splitAt.cry | 9 +++++++ examples/zero_weird.cry | 12 +++++++++ 7 files changed, 124 insertions(+) create mode 100644 examples/append.cry create mode 100644 examples/builtin_lifting.cry create mode 100644 examples/demote.cry create mode 100644 examples/props.cry create mode 100644 examples/split.cry create mode 100644 examples/splitAt.cry create mode 100644 examples/zero_weird.cry diff --git a/examples/append.cry b/examples/append.cry new file mode 100644 index 00000000..ccb7cd9b --- /dev/null +++ b/examples/append.cry @@ -0,0 +1,13 @@ +x : [_][8] +x = [1,2,3,4,5,19,12,38,5,3] + +y : [_][8] +y = [19,3,27,5,12] + +z = x # y + +m = z @ (0 : [1]) //1 +w = z @ 2 //3 + +t = z @ 10 //19 (0x13) +v = z @ 11 //3 diff --git a/examples/builtin_lifting.cry b/examples/builtin_lifting.cry new file mode 100644 index 00000000..aae8ee10 --- /dev/null +++ b/examples/builtin_lifting.cry @@ -0,0 +1,48 @@ +//builtins lift over tuples, seqs, and records + +//this file uses addition to model a builtin +//but this should work for any builtin operators + +x = [True,False] +y = [False,True] + +//make sure bitvectors are numbers +property p1 = x == (2 : [2]) + +//same thing written 2 different ways +property p2 = x + y == 3 +property p3 = x + y == [True,True] + + +xx = [[True,False]] +yy = [[False,True]] + +//addition lifts pointwise over sequences +property p4 = xx + yy == [3] + +//negation is a unary operator that also lifts over sequences +property p5 = ~ xx == yy + + +xinf = [2 ... ] +yinf = [3 ... ] + +//addition lifts pointwise over infinite lists +property p6 = (xinf + yinf) @ (0 : [0]) == (1 : [2]) + +//negation lifts pointwise over an infinite list +property p7 = (~ xinf) @ (0 : [0]) == (1 : [2]) + +xrec = { x = 2 : [2], y = 2 : [2] } : {x : [2], y : [2]} + +property p8 = xrec + xrec + xrec == xrec + +//lift over tuples and records at the same time +property p9 = (2,2,xrec) + (2,2,xrec) + (2,2,xrec) == (2:[2],2:[2],xrec) + +//lift unary over tuples and lists +property p10 = (~ { x = (1,2), y = [3,4,5] }) == {x = (0:[1],1:[2]), y = [4, 3, 2] : [3][3] } + + + + diff --git a/examples/demote.cry b/examples/demote.cry new file mode 100644 index 00000000..bb01bbec --- /dev/null +++ b/examples/demote.cry @@ -0,0 +1,5 @@ +x : {a}(fin a) => [a] -> [(a*2)+3] +x v = 0 + 1 + +y = x (2 : [3]) + diff --git a/examples/props.cry b/examples/props.cry new file mode 100644 index 00000000..9b1b5965 --- /dev/null +++ b/examples/props.cry @@ -0,0 +1,27 @@ +x = [True, False] +y = [False, True] +z = x + y + +property p1 = z == 3 + +xx = [[True,False]] +yy = [[False, True]] +zz = xx + yy + + + +t : {a} [a*3] -> [a*3][a*3] +t d = zero +/* + + +t1 : [8] -> [2][2][2] +t1 x = split (split x) + +t2 : [8] -> ([4],[4]) +t2 x = splitAt x + +t3 : [8] ->[8] -> [16] +t3 x y = x # y + +*/ \ No newline at end of file diff --git a/examples/split.cry b/examples/split.cry new file mode 100644 index 00000000..b5212949 --- /dev/null +++ b/examples/split.cry @@ -0,0 +1,10 @@ +x = [1,2,3,4] : [_][8] + +y = (split x) : [2][2][8] + +a = (y@0) @ 0 +b = (y@0) @ 1 +c = (y@1) @ 0 +d = (y@1) @ 1 + + diff --git a/examples/splitAt.cry b/examples/splitAt.cry new file mode 100644 index 00000000..5d389e94 --- /dev/null +++ b/examples/splitAt.cry @@ -0,0 +1,9 @@ +x = [1,2,3,4] : [_][8] + +y = (splitAt x) : ([2][8],[2][8]) + +a = y.0 @ 0 +b = y.0 @ 1 +c = y.1 @ 0 +d = y.1 @ 1 + diff --git a/examples/zero_weird.cry b/examples/zero_weird.cry new file mode 100644 index 00000000..b9eef494 --- /dev/null +++ b/examples/zero_weird.cry @@ -0,0 +1,12 @@ +x : {a}() => a -> [16] +x v = zero v + +property xprop v = x v == 0 + +y : [12] -> [4] -> [17] +y a b = zero a b + +property yprop v w = y v w == 0 + +t1 = x 13 +t2 = y 2 3 From 92d904908231a4196781ae5db5543f4157380e6a Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 6 Jul 2017 16:52:11 -0700 Subject: [PATCH 13/17] correctly print out uids for type variables --- src/Cryptol/TypeCheck/AST.hs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index baa250b4..7a2c1de5 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -144,7 +144,7 @@ instance ShowAST Expr where showAst (EAbs n _ e) = "(EAbs " ++ showAst n ++ " " ++ showAst e ++ ")" showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" - showAst (ETApp e t) = "(ETApp " ++ showAst e ++ " " ++ showAst t ++ ")" + showAst (ETApp e t) = "(ETApp " ++ showAst e ++ " (ETyp " ++ showAst t ++ "))" --NOTE: erase all proofs for now (change the following two lines to change that) showAst (EProofAbs {-p-}_ e) = showAst e --"(EProofAbs " ++ show p ++ showAst e ++ ")" showAst (EProofApp e) = showAst e --"(EProofApp " ++ showAst e ++ ")" @@ -160,6 +160,7 @@ instance ShowAST Ident where instance ShowAST Type where showAst (TUser n lt t) = "(TUser " ++ showAst n ++ " " ++ showAst lt ++ " " ++ showAst t ++ ")" + showAst (TRec lidt) = "(TRec " ++ showAst lidt ++ ")" showAst t = "(" ++ show t ++ ")" instance ShowAST Selector where @@ -169,7 +170,7 @@ instance ShowAST Selector where instance ShowAST Match where showAst (From n _ _ e) = "(From " ++ showAst n ++ " " ++ showAst e ++ ")" - showAst (Let d) = "(Let " ++ showAst d ++ ")" + showAst (Let d) = "(MLet " ++ showAst d ++ ")" instance ShowAST Decl where showAst d = "(Decl " ++ showAst (dName d) ++ " " ++ showAst (dDefinition d) ++ ")" @@ -191,12 +192,16 @@ instance (ShowAST a) => ShowAST [a] where showAst a = "[" ++ showASTList a ++ "]" instance (ShowAST a) => ShowAST (Maybe a) where - showAst Nothing = "" + showAst Nothing = "(0,\"\")" --empty ident, won't shadow demote showAst (Just x) = showAst x instance ShowAST TParam where - showAst tp = showAst (tpName tp) + showAst tp = "(" ++ show (tpUnique tp) ++ "," ++ maybeNameStr (tpName tp) ++ ")" +maybeNameStr :: Maybe Name -> String +maybeNameStr Nothing = show "" +maybeNameStr (Just n) = showAst (nameIdent n) + instance ShowAST Name where showAst n = "(" ++ show (nameUnique n) ++ "," ++ showAst (nameIdent n) ++ ")" From 50c645448297500fcce9520a2f22cd76f179549b Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Thu, 13 Jul 2017 10:55:44 -0700 Subject: [PATCH 14/17] more example --- examples/comp.cry | 10 ++++++++++ examples/inflist.cry | 10 ++++++++++ examples/width.cry | 2 ++ examples/xor_cipher.cry | 7 +++++++ 4 files changed, 29 insertions(+) create mode 100644 examples/comp.cry create mode 100644 examples/inflist.cry create mode 100644 examples/width.cry create mode 100644 examples/xor_cipher.cry diff --git a/examples/comp.cry b/examples/comp.cry new file mode 100644 index 00000000..23b14d12 --- /dev/null +++ b/examples/comp.cry @@ -0,0 +1,10 @@ +x : [_]([2],[3],[3],[4]) +x = [(a,b,c,d) | a <- [1,2], b <- [3,4] | c <- [5,6], d <- [7,8,9] ] + +property t1 = x @ 0 == (1,3,5,7) +property t2 = x @ 2 == (2,3,5,9) +property t3 = x @ 3 == (2,4,6,7) + +y = [(a,b,c) | a <- [1,2,3], b <- [1,2] | c <- [1 ... ] ] + +property t4 = y @ 3 == (2,2,0) diff --git a/examples/inflist.cry b/examples/inflist.cry new file mode 100644 index 00000000..1b537f56 --- /dev/null +++ b/examples/inflist.cry @@ -0,0 +1,10 @@ +a = [1 ... ] +b = [1,2 ... ] +c = [1 .. 5] +d = [1,3 .. 9] + +property t1 = a @ 3 == 1 +property t2 = b @ 3 == 1 +property t3 = c @ 3 == 4 +property t4 = d @ 3 == 4 + diff --git a/examples/width.cry b/examples/width.cry new file mode 100644 index 00000000..18dd248c --- /dev/null +++ b/examples/width.cry @@ -0,0 +1,2 @@ +x : [8] +x = width (252 : [8]) \ No newline at end of file diff --git a/examples/xor_cipher.cry b/examples/xor_cipher.cry new file mode 100644 index 00000000..c20b2273 --- /dev/null +++ b/examples/xor_cipher.cry @@ -0,0 +1,7 @@ +encrypt : {a}(fin a) => [8] -> [a][8] -> [a][8] +encrypt key plaintext = [pt ^ key | pt <- plaintext ] + +decrypt : {a}(fin a) => [8] -> [a][8] -> [a][8] +decrypt key ciphertext = [ct ^ key | ct <- ciphertext ] + +property roundtrip k ip = decrypt k (encrypt k ip) == ip \ No newline at end of file From 505e565bbeca360c606740ff693387eb43b46410 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Mon, 14 Aug 2017 13:28:09 -0700 Subject: [PATCH 15/17] performed all suggested changes except new module for ShowAST --- cryptol-ast | 6 ------ src/Cryptol/Parser/AST.hs | 6 ------ src/Cryptol/Parser/Position.hs | 4 +--- src/Cryptol/REPL/Command.hs | 15 ++++++--------- src/Cryptol/TypeCheck/AST.hs | 5 ++++- 5 files changed, 11 insertions(+), 25 deletions(-) delete mode 100755 cryptol-ast diff --git a/cryptol-ast b/cryptol-ast deleted file mode 100755 index d1b8505b..00000000 --- a/cryptol-ast +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/bash -CRYPTOL=/Users/emullen/cryptol/dist/build/Cryptol/cryptol -IN="$1" - -echo ":all" | "$CRYPTOL" "$IN" | cut -c 7- | tail -n 1 - diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 8b259ce5..31cda396 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -174,9 +174,6 @@ data Bind name = Bind { bName :: Located name -- ^ Defined thing , bDoc :: Maybe String -- ^ Optional doc string } deriving (Eq, Generic, NFData, Functor, Show) --- instance (Show name) => Show (Bind name) where --- show b = "(Bind (" ++ show (bName b) ++ ") (" ++ show (bDef b) ++ "))" - type LBindDef = Located (BindDef PName) data BindDef name = DPrim @@ -187,9 +184,6 @@ data Fixity = Fixity { fAssoc :: !Assoc , fLevel :: !Int } deriving (Eq, Generic, NFData, Show) --- instance Show Fixity where --- show _ = "" - data FixityCmp = FCError | FCLeft | FCRight diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index f5798b22..33d1bc9a 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -22,10 +22,8 @@ import Control.DeepSeq import Cryptol.Utils.PP data Located a = Located { srcRange :: !Range, thing :: !a } - deriving (Eq, Generic, NFData) + deriving (Eq, Show, Generic, NFData) -instance (Show a) => Show (Located a) where - show l = show (thing l) data Position = Position { line :: !Int, col :: !Int } deriving (Eq, Ord, Show, Generic, NFData) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c2e214d4..3ddfaf44 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -185,9 +185,9 @@ nbCommandList = , CommandDescr [ ":eval" ] (ExprArg refEvalCmd) "evaluate an expression with the reference evaluator" , CommandDescr [ ":ast" ] (ExprArg astOfCmd) - "print out an AST of a given term" - , CommandDescr [ ":all" ] (ExprArg allTerms) - "print out the AST of all defined terms" + "print out the pre-typechecked AST of a given term" + , CommandDescr [ ":extract-coq" ] (NoArg allTerms) + "print out the post-typechecked AST of all currently defined terms, in a Coq parseable format" ] commandList :: [CommandDescr] @@ -594,17 +594,14 @@ refEvalCmd str = do val <- liftModuleCmd (rethrowEvalError . R.evaluate expr) rPrint $ R.ppValue val -nameToNumber :: M.Name -> Int -nameToNumber n = M.nameUnique n - astOfCmd :: String -> REPL () astOfCmd str = do expr <- replParseExpr str (re,_,_) <- replCheckExpr (P.noPos expr) - rPrint (fmap nameToNumber re) + rPrint (fmap M.nameUnique re) -allTerms :: String -> REPL () -allTerms _ = do +allTerms :: REPL () +allTerms = do me <- getModuleEnv rPutStrLn (T.showAst (concatMap T.mDecls (M.loadedModules me))) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 7a2c1de5..69d7f687 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -33,7 +33,7 @@ import Cryptol.Prims.Syntax import Cryptol.Parser.AST ( Selector(..),Pragma(..) , Import(..), ImportSpec(..), ExportType(..) , ExportSpec(..), isExportedBind - , isExportedType, Fixity(..) ) + , isExportedType, Fixity(..), Located(..) ) import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent,unpackIdent) import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Type @@ -195,6 +195,9 @@ instance (ShowAST a) => ShowAST (Maybe a) where showAst Nothing = "(0,\"\")" --empty ident, won't shadow demote showAst (Just x) = showAst x +instance (ShowAST a) => ShowAST (Located a) where + showAst l = showAst (thing l) + instance ShowAST TParam where showAst tp = "(" ++ show (tpUnique tp) ++ "," ++ maybeNameStr (tpName tp) ++ ")" From 05b8f0f3c11755a5c0612a9ad09c488ac61e6344 Mon Sep 17 00:00:00 2001 From: Eric Mullen Date: Mon, 14 Aug 2017 15:45:37 -0700 Subject: [PATCH 16/17] more polished --- cryptol.cabal | 1 + src/Cryptol/Parser/AST.hs | 153 ----------------------------- src/Cryptol/REPL/Command.hs | 3 +- src/Cryptol/TypeCheck/AST.hs | 83 +--------------- src/Cryptol/TypeCheck/Parseable.hs | 105 ++++++++++++++++++++ 5 files changed, 110 insertions(+), 235 deletions(-) create mode 100644 src/Cryptol/TypeCheck/Parseable.hs diff --git a/cryptol.cabal b/cryptol.cabal index 6626ae34..16b0bba5 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -111,6 +111,7 @@ library Cryptol.TypeCheck.TypePat, Cryptol.TypeCheck.SimpType, Cryptol.TypeCheck.AST, + Cryptol.TypeCheck.Parseable, Cryptol.TypeCheck.Monad, Cryptol.TypeCheck.Infer, Cryptol.TypeCheck.InferTypes, diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 31cda396..b4959512 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -984,156 +984,3 @@ instance NoPos (Prop name) where CLocated c _ -> noPos c CType t -> CType (noPos t) --- --Typeclass for prettying up the AST for exporting to Coq --- --Similar to NoPos above --- class CoqAst t where --- coqAst :: t -> t - --- -- WARNING: This does not call `coqAst` on the `thing` inside --- instance CoqAst (Located t) where --- coqAst x = x { srcRange = rng } --- where rng = Range { from = Position 0 0, to = Position 0 0, source = "" } - --- instance CoqAst t => CoqAst (Named t) where --- coqAst t = Named { name = coqAst (name t), value = coqAst (value t) } - --- instance CoqAst t => CoqAst [t] where coqAst = fmap coqAst --- instance CoqAst t => CoqAst (Maybe t) where coqAst = fmap coqAst - --- instance CoqAst (Program name) where --- coqAst (Program x) = Program (coqAst x) - --- instance CoqAst (Module name) where --- coqAst m = Module { mName = mName m --- , mImports = coqAst (mImports m) --- , mDecls = coqAst (mDecls m) --- } - --- instance CoqAst (TopDecl name) where --- coqAst decl = --- case decl of --- Decl x -> Decl (coqAst x) --- TDNewtype n -> TDNewtype(coqAst n) --- Include x -> Include (coqAst x) - --- instance CoqAst a => CoqAst (TopLevel a) where --- coqAst tl = tl { tlValue = coqAst (tlValue tl) } - --- instance CoqAst (Decl name) where --- coqAst decl = --- case decl of --- DSignature x y -> DSignature (coqAst x) (coqAst y) --- DPragma x y -> DPragma (coqAst x) (coqAst y) --- DPatBind x y -> DPatBind (coqAst x) (coqAst y) --- DFixity f ns -> DFixity f (coqAst ns) --- DBind x -> DBind (coqAst x) --- DType x -> DType (coqAst x) --- DLocated x _ -> coqAst x - --- instance CoqAst (Newtype name) where --- coqAst n = Newtype { nName = coqAst (nName n) --- , nParams = nParams n --- , nBody = coqAst (nBody n) --- } - --- instance CoqAst (Bind name) where --- coqAst x = Bind { bName = coqAst (bName x) --- , bParams = coqAst (bParams x) --- , bDef = coqAst (bDef x) --- , bSignature = coqAst (bSignature x) --- , bInfix = bInfix x --- , bFixity = bFixity x --- , bPragmas = coqAst (bPragmas x) --- , bMono = bMono x --- , bDoc = bDoc x --- } - --- instance CoqAst Pragma where --- coqAst p@(PragmaNote {}) = p --- coqAst p@(PragmaProperty) = p - - - --- instance CoqAst (TySyn name) where --- coqAst (TySyn x y z) = TySyn (coqAst x) (coqAst y) (coqAst z) - --- instance CoqAst (Expr name) where --- coqAst expr = --- case expr of --- EVar x -> EVar x --- ELit x -> ELit x --- ETuple x -> ETuple (coqAst x) --- ERecord x -> ERecord (coqAst x) --- ESel x y -> ESel (coqAst x) y --- EList x -> EList (coqAst x) --- EFromTo x y z -> EFromTo (coqAst x) (coqAst y) (coqAst z) --- EInfFrom x y -> EInfFrom (coqAst x) (coqAst y) --- EComp x y -> EComp (coqAst x) (coqAst y) --- EApp x y -> EApp (coqAst x) (coqAst y) --- EAppT x y -> EAppT (coqAst x) (coqAst y) --- EIf x y z -> EIf (coqAst x) (coqAst y) (coqAst z) --- EWhere x y -> EWhere (coqAst x) (coqAst y) --- ETyped x y -> ETyped (coqAst x) (coqAst y) --- ETypeVal x -> ETypeVal (coqAst x) --- EFun x y -> EFun (coqAst x) (coqAst y) --- ELocated x _ -> coqAst x - --- EParens e -> EParens (coqAst e) --- EInfix x y f z-> EInfix (coqAst x) y f (coqAst z) - --- instance CoqAst (TypeInst name) where --- coqAst (PosInst ts) = PosInst (coqAst ts) --- coqAst (NamedInst fs) = NamedInst (coqAst fs) - --- instance CoqAst (Match name) where --- coqAst (Match x y) = Match (coqAst x) (coqAst y) --- coqAst (MatchLet b) = MatchLet (coqAst b) - --- instance CoqAst (Pattern name) where --- coqAst pat = --- case pat of --- PVar x -> PVar (coqAst x) --- PWild -> PWild --- PTuple x -> PTuple (coqAst x) --- PRecord x -> PRecord (coqAst x) --- PList x -> PList (coqAst x) --- PTyped x y -> PTyped (coqAst x) (coqAst y) --- PSplit x y -> PSplit (coqAst x) (coqAst y) --- PLocated x _ -> coqAst x - --- instance CoqAst (Schema name) where --- coqAst (Forall x y z _) = Forall (coqAst x) (coqAst y) (coqAst z) Nothing - --- instance CoqAst (TParam name) where --- coqAst (TParam x y _) = TParam x y Nothing - --- instance CoqAst (Type name) where --- coqAst ty = --- case ty of --- TWild -> TWild --- TApp x y -> TApp x (coqAst y) --- TUser x y -> TUser x (coqAst y) --- TRecord x -> TRecord (coqAst x) --- TTuple x -> TTuple (coqAst x) --- TFun x y -> TFun (coqAst x) (coqAst y) --- TSeq x y -> TSeq (coqAst x) (coqAst y) --- TBit -> TBit --- TInf -> TInf --- TNum n -> TNum n --- TChar n -> TChar n --- TLocated x _ -> coqAst x --- TParens x -> TParens (coqAst x) --- TInfix x y f z-> TInfix (coqAst x) y f (coqAst z) - --- instance CoqAst (Prop name) where --- coqAst prop = --- case prop of --- CEqual x y -> CEqual (coqAst x) (coqAst y) --- CGeq x y -> CGeq (coqAst x) (coqAst y) --- CFin x -> CFin (coqAst x) --- CArith x -> CArith (coqAst x) --- CCmp x -> CCmp (coqAst x) --- CLocated c _ -> coqAst c --- CType t -> CType (coqAst t) - - diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 3ddfaf44..2725bf39 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -66,6 +66,7 @@ import Cryptol.Parser (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig ,parseModName,parseHelpName) import qualified Cryptol.TypeCheck.AST as T +import qualified Cryptol.TypeCheck.Parseable as T import qualified Cryptol.TypeCheck.Subst as T import qualified Cryptol.TypeCheck.InferTypes as T import Cryptol.TypeCheck.Solve(defaultReplExpr) @@ -603,7 +604,7 @@ astOfCmd str = do allTerms :: REPL () allTerms = do me <- getModuleEnv - rPutStrLn (T.showAst (concatMap T.mDecls (M.loadedModules me))) + rPrint $ T.showParseable $ concatMap T.mDecls $ M.loadedModules me typeOfCmd :: String -> REPL () typeOfCmd str = do diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 69d7f687..a118a6bb 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -33,8 +33,8 @@ import Cryptol.Prims.Syntax import Cryptol.Parser.AST ( Selector(..),Pragma(..) , Import(..), ImportSpec(..), ExportType(..) , ExportSpec(..), isExportedBind - , isExportedType, Fixity(..), Located(..) ) -import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent,unpackIdent) + , isExportedType, Fixity(..)) +import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent) import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Type @@ -128,85 +128,6 @@ data DeclDef = DPrim | DExpr Expr deriving (Show, Generic, NFData) --- ShowAST prints out just enough information to model the program in Coq -class ShowAST t where - showAst :: t -> String - -instance ShowAST Expr where - showAst (EList es _) = "(EList " ++ showAst es ++ ")" - showAst (ETuple es) = "(ETuple " ++ showAst es ++ ")" - showAst (ERec ides) = "(ERec " ++ showAst ides ++ ")" - showAst (ESel e s) = "(ESel " ++ showAst e ++ " " ++ showAst s ++ ")" - showAst (EIf c t f) = "(EIf " ++ showAst c ++ " " ++ showAst t ++ " " ++ showAst f ++ ")" - showAst (EComp _ _ e mss) = "(EComp " ++ showAst e ++ " " ++ showAst mss ++ ")" - showAst (EVar n) = "(EVar " ++ showAst n ++ ")" - showAst (EApp fe ae) = "(EApp " ++ showAst fe ++ " " ++ showAst ae ++ ")" - showAst (EAbs n _ e) = "(EAbs " ++ showAst n ++ " " ++ showAst e ++ ")" - showAst (EWhere e dclg) = "(EWhere " ++ showAst e ++ " " ++ showAst dclg ++ ")" - showAst (ETAbs tp e) = "(ETAbs " ++ showAst tp ++ " " ++ showAst e ++ ")" - showAst (ETApp e t) = "(ETApp " ++ showAst e ++ " (ETyp " ++ showAst t ++ "))" - --NOTE: erase all proofs for now (change the following two lines to change that) - showAst (EProofAbs {-p-}_ e) = showAst e --"(EProofAbs " ++ show p ++ showAst e ++ ")" - showAst (EProofApp e) = showAst e --"(EProofApp " ++ showAst e ++ ")" - -instance (ShowAST a, ShowAST b) => ShowAST (a,b) where - showAst (x,y) = "(" ++ showAst x ++ "," ++ showAst y ++ ")" - -instance ShowAST Int where - showAst i = show i - -instance ShowAST Ident where - showAst i = show (unpackIdent i) - -instance ShowAST Type where - showAst (TUser n lt t) = "(TUser " ++ showAst n ++ " " ++ showAst lt ++ " " ++ showAst t ++ ")" - showAst (TRec lidt) = "(TRec " ++ showAst lidt ++ ")" - showAst t = "(" ++ show t ++ ")" - -instance ShowAST Selector where - showAst (TupleSel n _) = "(TupleSel " ++ showAst n ++ ")" - showAst (RecordSel n _) = "(RecordSel " ++ showAst n ++ ")" - showAst (ListSel n _) = "(ListSel " ++ showAst n ++ ")" - -instance ShowAST Match where - showAst (From n _ _ e) = "(From " ++ showAst n ++ " " ++ showAst e ++ ")" - showAst (Let d) = "(MLet " ++ showAst d ++ ")" - -instance ShowAST Decl where - showAst d = "(Decl " ++ showAst (dName d) ++ " " ++ showAst (dDefinition d) ++ ")" - -instance ShowAST DeclDef where - showAst DPrim = show DPrim - showAst (DExpr e) = "(DExpr " ++ (showAst e) ++ ")" - -instance ShowAST DeclGroup where - showAst (Recursive ds) = "(Recursive " ++ showAst ds ++ ")" - showAst (NonRecursive d) = "(NonRecursive " ++ showAst d ++ ")" - -showASTList :: (ShowAST a) => [a] -> String -showASTList [] = "" -showASTList [x] = showAst x -showASTList (x : y) = (showAst x) ++ "," ++ showASTList y - -instance (ShowAST a) => ShowAST [a] where - showAst a = "[" ++ showASTList a ++ "]" - -instance (ShowAST a) => ShowAST (Maybe a) where - showAst Nothing = "(0,\"\")" --empty ident, won't shadow demote - showAst (Just x) = showAst x - -instance (ShowAST a) => ShowAST (Located a) where - showAst l = showAst (thing l) - -instance ShowAST TParam where - showAst tp = "(" ++ show (tpUnique tp) ++ "," ++ maybeNameStr (tpName tp) ++ ")" - -maybeNameStr :: Maybe Name -> String -maybeNameStr Nothing = show "" -maybeNameStr (Just n) = showAst (nameIdent n) - -instance ShowAST Name where - showAst n = "(" ++ show (nameUnique n) ++ "," ++ showAst (nameIdent n) ++ ")" -------------------------------------------------------------------------------- diff --git a/src/Cryptol/TypeCheck/Parseable.hs b/src/Cryptol/TypeCheck/Parseable.hs new file mode 100644 index 00000000..baa03a7c --- /dev/null +++ b/src/Cryptol/TypeCheck/Parseable.hs @@ -0,0 +1,105 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2013-2017 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + +{-# LANGUAGE Safe #-} + +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-} +module Cryptol.TypeCheck.Parseable + ( module Cryptol.TypeCheck.Parseable + , ShowParseable(..) + ) where + +import Cryptol.TypeCheck.AST +import Cryptol.Utils.Ident (Ident,unpackIdent) +import Cryptol.Parser.AST ( Located(..)) +import Cryptol.ModuleSystem.Name +import Text.PrettyPrint + +-- ShowParseable prints out a cryptol program in a way that it's parseable by Coq (and likely other things) +-- Used mainly for reasoning about the semantics of cryptol programs in Coq (https://github.com/GaloisInc/cryptol-semantics) +class ShowParseable t where + showParseable :: t -> Doc + +instance ShowParseable Expr where + showParseable (EList es _) = parens (text "EList" <+> showParseable es) + showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es) + showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides) + showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s) + showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c <+> showParseable t <+> showParseable f) + showParseable (EComp _ _ e mss) = parens (text "EComp" <+> showParseable e <+> showParseable mss) + showParseable (EVar n) = parens (text "EVar" <+> showParseable n) + showParseable (EApp fe ae) = parens (text "EApp" <+> showParseable fe <+> showParseable ae) + showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n <+> showParseable e) + showParseable (EWhere e dclg) = parens (text "EWhere" <+> showParseable e <+> showParseable dclg) + showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp <+> showParseable e) + showParseable (ETApp e t) = parens (text "ETApp" <+> showParseable e <+> parens (text "ETyp" <+> showParseable t)) + --NOTE: erase all "proofs" for now (change the following two lines to change that) + showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")" + showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")" + +instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where + showParseable (x,y) = parens (showParseable x <> comma <> showParseable y) + +instance ShowParseable Int where + showParseable i = int i + +instance ShowParseable Ident where + showParseable i = text $ show $ unpackIdent i + +instance ShowParseable Type where + showParseable (TUser n lt t) = parens (text "TUser" <+> showParseable n <+> showParseable lt <+> showParseable t) + showParseable (TRec lidt) = parens (text "TRec" <+> showParseable lidt) + showParseable t = parens $ text $ show t + +instance ShowParseable Selector where + showParseable (TupleSel n _) = parens (text "TupleSel" <+> showParseable n) + showParseable (RecordSel n _) = parens (text "RecordSel" <+> showParseable n) + showParseable (ListSel n _) = parens (text "ListSel" <+> showParseable n) + +instance ShowParseable Match where + showParseable (From n _ _ e) = parens (text "From" <+> showParseable n <+> showParseable e) + showParseable (Let d) = parens (text "MLet" <+> showParseable d) + +instance ShowParseable Decl where + showParseable d = parens (text "Decl" <+> showParseable (dName d) <+> showParseable (dDefinition d)) + +instance ShowParseable DeclDef where + showParseable DPrim = text (show DPrim) + showParseable (DExpr e) = parens (text "DExpr" <+> showParseable e) + +instance ShowParseable DeclGroup where + showParseable (Recursive ds) = parens (text "Recursive" <+> showParseable ds) + showParseable (NonRecursive d) = parens (text "NonRecursive" <+> showParseable d) + +showParseableList :: (ShowParseable a) => [a] -> Doc +showParseableList [] = empty +showParseableList [x] = showParseable x +showParseableList (x : y) = (showParseable x) <> comma <> showParseableList y + +instance (ShowParseable a) => ShowParseable [a] where + showParseable a = brackets $ showParseableList a + +instance (ShowParseable a) => ShowParseable (Maybe a) where + showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote + showParseable (Just x) = showParseable x + +instance (ShowParseable a) => ShowParseable (Located a) where + showParseable l = showParseable (thing l) + +instance ShowParseable TParam where + showParseable tp = parens (text (show (tpUnique tp)) <> comma <> maybeNameDoc (tpName tp)) + +maybeNameDoc :: Maybe Name -> Doc +maybeNameDoc Nothing = doubleQuotes empty +maybeNameDoc (Just n) = showParseable (nameIdent n) + +instance ShowParseable Name where + showParseable n = parens (text (show (nameUnique n)) <> comma <> showParseable (nameIdent n)) From b3f605d9f46d3f79b0e5d16907450fadf646419e Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 15 Aug 2017 10:52:32 -0700 Subject: [PATCH 17/17] Pretty print with a bit more space, so we can see what's going on. --- src/Cryptol/TypeCheck/Parseable.hs | 38 +++++++++++++++++------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/Cryptol/TypeCheck/Parseable.hs b/src/Cryptol/TypeCheck/Parseable.hs index baa03a7c..e04a4f59 100644 --- a/src/Cryptol/TypeCheck/Parseable.hs +++ b/src/Cryptol/TypeCheck/Parseable.hs @@ -33,14 +33,15 @@ instance ShowParseable Expr where showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es) showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides) showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s) - showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c <+> showParseable t <+> showParseable f) - showParseable (EComp _ _ e mss) = parens (text "EComp" <+> showParseable e <+> showParseable mss) + showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c $$ showParseable t $$ showParseable f) + showParseable (EComp _ _ e mss) = parens (text "EComp" $$ showParseable e $$ showParseable mss) showParseable (EVar n) = parens (text "EVar" <+> showParseable n) - showParseable (EApp fe ae) = parens (text "EApp" <+> showParseable fe <+> showParseable ae) - showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n <+> showParseable e) - showParseable (EWhere e dclg) = parens (text "EWhere" <+> showParseable e <+> showParseable dclg) - showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp <+> showParseable e) - showParseable (ETApp e t) = parens (text "ETApp" <+> showParseable e <+> parens (text "ETyp" <+> showParseable t)) + showParseable (EApp fe ae) = parens (text "EApp" $$ showParseable fe $$ showParseable ae) + showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n $$ showParseable e) + showParseable (EWhere e dclg) = parens (text "EWhere" $$ showParseable e $$ showParseable dclg) + showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp + $$ showParseable e) + showParseable (ETApp e t) = parens (text "ETApp" $$ showParseable e $$ parens (text "ETyp" <+> showParseable t)) --NOTE: erase all "proofs" for now (change the following two lines to change that) showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")" showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")" @@ -69,23 +70,26 @@ instance ShowParseable Match where showParseable (Let d) = parens (text "MLet" <+> showParseable d) instance ShowParseable Decl where - showParseable d = parens (text "Decl" <+> showParseable (dName d) <+> showParseable (dDefinition d)) + showParseable d = parens (text "Decl" <+> showParseable (dName d) + $$ showParseable (dDefinition d)) instance ShowParseable DeclDef where showParseable DPrim = text (show DPrim) - showParseable (DExpr e) = parens (text "DExpr" <+> showParseable e) + showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e) instance ShowParseable DeclGroup where - showParseable (Recursive ds) = parens (text "Recursive" <+> showParseable ds) - showParseable (NonRecursive d) = parens (text "NonRecursive" <+> showParseable d) - -showParseableList :: (ShowParseable a) => [a] -> Doc -showParseableList [] = empty -showParseableList [x] = showParseable x -showParseableList (x : y) = (showParseable x) <> comma <> showParseableList y + showParseable (Recursive ds) = + parens (text "Recursive" $$ showParseable ds) + showParseable (NonRecursive d) = + parens (text "NonRecursive" $$ showParseable d) instance (ShowParseable a) => ShowParseable [a] where - showParseable a = brackets $ showParseableList a + showParseable a = case a of + [] -> text "[]" + [x] -> brackets (showParseable x) + x : xs -> text "[" <+> showParseable x $$ + vcat [ comma <+> showParseable y | y <- xs ] $$ + text "]" instance (ShowParseable a) => ShowParseable (Maybe a) where showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote