mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 01:13:34 +03:00
more polished
This commit is contained in:
Eric Mullen
parent
505e565bbe
commit
05b8f0f3c1
@ -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,
|
||||
|
||||
@ -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)
|
||||
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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) ++ ")"
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
||||
105
src/Cryptol/TypeCheck/Parseable.hs
Normal file
105
src/Cryptol/TypeCheck/Parseable.hs
Normal file
@ -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))
|
||||
Loading…
Reference in New Issue
Block a user