Skip to content
Snippets Groups Projects
Commit d24f5e53 authored by Samuel Hym's avatar Samuel Hym
Browse files

Rewrite coq2c. Rename it digger. 

Refactor the code parsing the JSON extracted from Coq.

Rewrite completely the conversion to C, splitting it in two stages:
- from the Coq AST to an intermediate representation corresponding to
  the part of Gallina that we can map to C,
- from that intermediate representation to C.

Use the standard Language.C library to produce the resulting C code, to
strengthen its quality.
parent 1c9e0f83
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
.gitignore
+ 5
− 1
View file @ d24f5e53
*.o
*.hi
Extractor
digger
.stack-work
dist
src/highlight.js
src/style.css
Makefile
+ 17
− 3
View file @ d24f5e53
DIGGER := ./digger
# Generic targets, building everything
default: default_message build_stack
default_message:
......@@ -8,15 +11,26 @@ default_message:
build_stack:
stack build
ln -sf $$(find .stack-work/install/ -name coq2c -type f) coq2c
ln -sf $$(stack exec which digger) digger
build_cabal:
cabal build
ln -sf dist/build/coq2c/coq2c coq2c
ln -sf dist/build/digger/digger digger
clean:
stack clean || true
cabal clean || true
rm -rf coq2c .stack-work dist
rm -rf digger .stack-work dist
.PHONY: default default_message build_stack build_cabal clean
# Default to stack for precise targets
digger: app/digger.hs $(wildcard src/Coq/*.hs)
stack build digger:exe:digger
ln -sf $$(stack exec which digger) digger
# Documentation
doc:
stack haddock
.PHONY: doc
Readme.md
+ 12
− 9
View file @ d24f5e53
# Summary
# Digger
This repository contains a tool to compile Coq code written in an
imperative style using a monad into the corresponding C code. It
starts from the Coq code extracted as JSON by the internal extraction
facility.
This repository contains a tool to convert Coq code written in a
“C-style” (imperative style based on a monad, with full application of
functions) into the corresponding C code or to an intermediate
representation (deep) output as Coq source code. It starts from the
Coq code extracted as JSON by the internal extraction facility.
The source code is covered by CeCILL-A licence, see `LICENSE`.
The CoqC Development Team is:
The source code is copyright Université de Lille 1 & Veïs Oudjail and
covered by CeCILL-A licence, see `LICENSE`.
* Veis Oudjail <veis.oudjail@etudiant.univ-lille1.fr>
* Samuel Hym <samuel.hym@univ-lille1.fr>
The development team is:
* Samuel Hym
* Veïs Oudjail
app/digger.hs 0 → 100644
+ 353
− 0
View file @ d24f5e53
-- |
-- Module : digger (Main)
-- Copyright : Université Lille 1, Veïs Oudjail, 2016-2017
-- License : CeCILL
--
-- Maintainer : samuel.hym@univ-lille1.fr
-- Stability : experimental
-- Portability : portable
--
-- Description : Convert Coq code written in a "C-style" (imperative
-- style based on a monad, with full application of
-- functions) into the corresponding C code or to an
-- intermediate representation (deep) output as Coq
-- source code.
-- Start from the Coq code extracted as JSON by the
-- internal extraction facility.
-- This software is a computer program whose purpose is to run a minimal,
-- hypervisor relying on proven properties such as memory isolation.
-- This software is governed by the CeCILL license under French law and
-- abiding by the rules of distribution of free software. You can use,
-- modify and/ or redistribute the software under the terms of the CeCILL
-- license as circulated by CEA, CNRS and INRIA at the following URL
-- "http://www.cecill.info".
-- As a counterpart to the access to the source code and rights to copy,
-- modify and redistribute granted by the license, users are provided only
-- with a limited warranty and the software's author, the holder of the
-- economic rights, and the successive licensors have only limited
-- liability.
-- In this respect, the user's attention is drawn to the risks associated
-- with loading, using, modifying and/or developing or reproducing the
-- software by the user in light of its specific status of free software,
-- that may mean that it is complicated to manipulate, and that also
-- therefore means that it is reserved for developers and experienced
-- professionals having in-depth computer knowledge. Users are therefore
-- encouraged to load and test the software's suitability as regards their
-- requirements in conditions enabling the security of their systems and/or
-- data to be ensured and, more generally, to use and operate it in the
-- same conditions as regards security.
-- The fact that you are presently reading this means that you have had
-- knowledge of the CeCILL license and that you accept its terms.
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Main where
import Control.Monad (when, (<=<))
import Data.Aeson (eitherDecode')
import qualified Data.ByteString.Lazy as BS
import Data.Default
import Data.List (elemIndex, intercalate)
import qualified Data.Map as Map
import Data.Monoid ((<>))
import Data.Text.Lazy (Text, pack, unpack)
import qualified Data.Text.Lazy as T
import qualified Data.Text.Lazy.IO as TIO
import Data.Version (showVersion)
import qualified Language.C as C
import Options.Applicative hiding (empty)
import System.Environment (getProgName)
import System.Exit (exitFailure)
import System.IO (IOMode (WriteMode), hPutStr,
hPutStrLn, stderr, stdout,
withFile)
import qualified Text.PrettyPrint as PP
import qualified Text.PrettyPrint.Leijen.Text as WL
import Text.Read (readMaybe)
import Language.Coq.Deep
import Language.Coq.ExtractedAST
import Paths_digger (version)
-- | Cleanup options to activate before conversion
data Cleaning = Cleaning { modulesToDrop :: [ModuleUsed]
, nameRewrites :: [(String,String)]
, dotReplacement :: String
}
deriving (Show,Eq)
instance Default Cleaning where
def = Cleaning { modulesToDrop = ["Datatypes"]
, nameRewrites = [ ("Coq_true", "true")
, ("Coq_false", "false")
, ("Coq_tt", "tt") ]
, dotReplacement = "_"
}
-- | Parse a command-line argument containing a pair of strings
-- separated with a colon
colonSeparatedPair :: ReadM (String,String)
colonSeparatedPair = eitherReader go
where go cs = case ':' `elemIndex` cs of
Just i -> Right (take i cs, drop (i+1) cs)
Nothing -> Left "Expected a colon-separated argument \"before:after\""
-- | Parse command-line options for the 'Cleaning' step
optsCleaning :: Parser Cleaning
optsCleaning = Cleaning <$> optModulesToDrop <*> optRewrites <*> optDotReplacement
where optModulesToDrop = some (strOption $ short 'm' <> long "drop-module" <> metavar "<module>"
<> help ( "module to drop from fully-qualified identifiers in source "
++ "(default, if no '-m' is given: "
++ intercalate ", " (modulesToDrop def) ++ "); "
++ "this option can be used multiple times" ))
<|> pure (modulesToDrop def)
optRewrites = some (option colonSeparatedPair $
short 'r' <> long "rename" <> metavar "<before>:<after>"
<> help ( "identifiers to rename (performed after dropping modules from "
++ "fully-qualified names) "
++ "(default, if no '-r' is given: "
++ intercalate ", " (map (\(a,b) -> a ++ ":" ++ b) $ nameRewrites def) ++ ")" ))
<|> pure (nameRewrites def)
optDotReplacement = strOption $ short 's' <> long "separator" <> metavar "<char>"
<> value (dotReplacement def) <> showDefaultWith id
<> help "separator to use in qualified names instead of dots"
-- | Parse a symbol on command-line
optSymbol :: Char -> String -> String -> String -> Parser String
optSymbol s l v h = strOption $ short s <> long l <> metavar "<symb>"
<> value v <> showDefaultWith id <> help h
-- | Parse command-line options for natural numbers
optsNat :: Parser CoqNat
optsNat = CN <$> optNatO
<*> optNatS
<*> optAdd
where optNatO = optSymbol 'O' "natO" (natO def) "how Coq's O (zero, type nat) was extracted"
optNatS = optSymbol 'S' "natS" (natS def) "how Coq's S (successor, type nat) was extracted"
optAdd = optSymbol 'A' "nat-add" (natAdd def) "how Coq's addition of natural number was extracted"
-- | Parse command-line options for the 'ConversionParams'
--
-- TODO: find a way to expose the parameters for unary and binary
-- operators, or it would not make much sense anyway?
optsCP :: Parser ConversionParams
optsCP = CP <$> optMonad
<*> optBind
<*> optRet
<*> optUnit
<*> optTt
<*> optTrue
<*> optFalse
<*> optsNat
<*> optConsts
<*> optIgnores
<*> optPrefixConst
<*> optPrefixFun
<*> optPrefixFTyp
<*> optPrefixVTyp
<*> optRecBound
<*> pure (unaryOps def)
<*> pure (binaryOps def)
where optMonad = optSymbol 'M' "monad" (monad def) "support monad"
optBind = optSymbol 'B' "bind" (bind def) "bind function of the monad"
optRet = optSymbol 'R' "ret" (ret def) "return function of the monad"
optUnit = optSymbol 'U' "unit" (unit def) "how Coq's unit (type) was extracted"
optTt = optSymbol 't' "tt" (tt def) "how Coq's tt (unit value) was extracted"
optTrue = optSymbol 'T' "true" (true def) "how Coq's true was extracted"
optFalse = optSymbol 'F' "false" (false def) "how Coq's false was extracted"
optRecBound = optSymbol 'v' "bound-var" (recBoundName def)
"name of the C variable used to bound recursive calls"
optConsts = some (strOption $ short 'c' <> long "const" <> metavar "<const>"
<> help ( "constructor to accept and re-export as is "
++ "(default, if no '-c' is given: "
++ intercalate ", " (consts def) ++ ")" ))
<|> pure (consts def)
optIgnores = many $ strOption $ long "ignore" <> metavar "<symb>"
<> help "symbol to ignore (do not try to convert it)"
optPrefixConst = optPref "prefix-const" (prefixConst def) "prefix for exported constructor names"
optPrefixFun = optPref "prefix-fun" (prefixFun def) "prefix for exported function names"
optPrefixFTyp = optPref "prefix-ftyp" (prefixFTyp def) "prefix for exported function types"
optPrefixVTyp = optPref "prefix-vtyp" (prefixVTyp def) "prefix for exported value types"
optPref l v h = option textR $ long l <> metavar "<pref>"
<> value v <> showDefaultWith unpack <> help h
textR :: ReadM Text
textR = eitherReader (Right . pack)
-- | All command-line options
data CLiOptions = CLO { cleaning :: Cleaning
, conversionParams :: ConversionParams
, deepOnly :: Bool
-- | Whether we should output a .h or a .c
, headerOnly :: Bool
, inputFile :: FilePath
, outputFile :: Maybe FilePath
-- | List of (prefix,Json file)
, dependencies :: [(String,FilePath)]
, headerFile :: Maybe FilePath
-- | #include or Require Import
, includes :: [String]
, includesQuote :: [String]
-- | Initial content of RecursiveBoundMap
, initRecBounds :: [(FunName, RecursiveBoundId)]
}
deriving (Show,Eq)
versionHelper :: String -> Parser (a -> a)
versionHelper progname = abortOption (InfoMsg (progname ++ " " ++ showVersion version)) $ mconcat
[ long "version"
, short 'v'
, help "Show the version of the program"
, hidden ]
-- | Command-line options
-- Take the name of the program as argument
options :: String -> ParserInfo CLiOptions
options pn = info (helper <*> versionHelper pn <*> cliopts) (fullDesc <> progDesc longDesc <> header shortDesc)
where longDesc = unwords
[ "Convert Coq code written in a \"C-style\" (imperative style"
, "based on a monad, with full application of functions) into"
, "the corresponding C code or to an intermediate representation (deep)"
, "output as Coq source code."
, "Start from the Coq code extracted as JSON by the internal extraction facility." ]
shortDesc = pn ++ " " ++ showVersion version
++ " - convert \"C-style\" Coq code into C code or an intermediate "
++ "representation in Coq"
cliopts = CLO <$> optsCleaning
<*> optsCP
<*> deepOnlyOpt
<*> headerOnlyOpt
<*> inputOpt
<*> outputOpt
<*> dependenciesOpt
<*> headerOpt
<*> includesOpt
<*> includesQuoteOpt
<*> recBoundsOpt
deepOnlyOpt = switch $ long "deep"
<> help "stop conversion at the Deep intermediate language"
headerOnlyOpt = switch $ long "header"
<> help "produce a .h file instead of a .c file"
inputOpt = strArgument $ metavar "<file.json>"
<> help "input file to convert (produced by Coq JSON extractor)"
outputOpt = optional $ strOption $ short 'o' <> metavar "<file>"
<> help "output result in <file> (default: stdout)"
dependenciesOpt = many $ option colonSeparatedPair $
short 'd' <> long "dependency" <> metavar "<namespace>:<file.json>"
<> help ( "add to the initial symbol table and to the initial set of "
++ "recursive functions the content of the given module "
++ "(produced by Coq JSON extractor) into the given namespace" )
headerOpt = optional $ strOption $ short 'H' <> metavar "<file>"
<> help "add the content of this file as header of the output"
includesOpt = many $ strOption $ short 'i' <> long "include" <> metavar "<module>"
<> help "output a #include <...> (or \"Require Import\") for the <module>"
includesQuoteOpt = many $ strOption $ short 'q' <> long "include-quote" <> metavar "<module>"
<> help "output a #include \"...\" (or \"Require Import\") for the <module>"
recBoundsOpt = many $ option (eitherReader colonNat) $
short 'b' <> long "recursive-bound" <> metavar "<fun>:<n>"
<> help ( "assume <fun> is a recursive function and that its <n>-th argument "
++ "(0-indexed) is the bound on the number of recursive calls" )
colonNat :: String -> Either String (FunName, RecursiveBoundId)
colonNat cs = case ':' `elemIndex` cs of
Nothing -> Right (cs, 0)
Just i -> case readMaybe (drop (i+1) cs) of
Just n | n >= 0 -> Right (take i cs, n)
_ -> Left msg
where msg = "Expected a colon-separated argument \"function:n\" (with n positive)"
++ " or just a function name"
cleanAST :: Cleaning -> Module -> Module
cleanAST Cleaning{..} = cleanModule modulesToDrop rewrts dotReplacement
where rewrts = Map.fromList nameRewrites
renderRequires :: [String] -> [String] -> Text
renderRequires xs ys = T.unlines $ map renderRequire $ xs ++ ys
where renderRequire i = T.concat ["Require Import ", T.pack i, "."]
renderIncludes :: [String] -> [String] -> Text
renderIncludes is qs = T.unlines $ map renderInclude is ++ map renderQuote qs
where renderInclude i = T.concat ["#include <", T.pack i, ">" ]
renderQuote i = T.concat ["#include \"", T.pack i, "\""]
readModule :: FilePath -> IO (Either String Module)
readModule = fmap eitherDecode' . BS.readFile
traverse2 :: (Applicative f, Applicative g, Traversable t) => (a -> f (g b)) -> t a -> f (g (t b))
traverse2 f = fmap sequenceA . traverse f
traverse2x2 :: (Applicative f, Applicative g, Traversable t, Traversable u) =>
(a -> f (g b)) -> t (u a) -> f (g (t (u b)))
traverse2x2 f = traverse2 (traverse2 f)
zipEither :: Either a b -> Either a c -> Either [a] (b,c)
zipEither (Right x) (Right y) = Right (x,y)
zipEither (Left x) (Right _) = Left [x]
zipEither (Right _) (Left y) = Left [y]
zipEither (Left x) (Left y) = Left [x,y]
infoDependency :: ConversionParams -> Cleaning -> (String, Module) -> (SymbolTable, RecursiveBoundMap)
infoDependency cp cleanOpts (prefix, modul) = (go syms, go recs)
where modul' = cleanAST cleanOpts modul
syms = extractSymbolTable cp $ declarationsMod modul'
recs = detectBounds (nats cp) modul'
go = Map.mapKeys (prefix ++)
main :: IO ()
main = do progname <- getProgName
CLO{..} <- execParser (options progname)
input <- readModule inputFile
deps <- traverse2x2 readModule dependencies
case zipEither input deps of
Right (input', deps') -> do
let (symss, recss) = unzip $ map (infoDependency conversionParams cleaning) deps'
recs = Map.unions (Map.fromList initRecBounds : recss)
syms = Map.unions symss
deepMod = fromCoq conversionParams recs syms $ cleanAST cleaning input'
maybe ($ stdout) (`withFile` WriteMode) outputFile $ \out -> do
let putText = TIO.hPutStrLn out
putWL = WL.displayIO out . WL.renderPretty 0.8 110
putPP = hPutStr out . PP.render
-- Header
let renderIncs = if deepOnly then renderRequires else renderIncludes
mapM_ (putText <=< TIO.readFile) headerFile
putText $ renderIncs includes includesQuote
-- Body
if deepOnly
then putWL $ prettyModule conversionParams deepMod
else do let (errs, src) = convert conversionParams deepMod
convert = if headerOnly then toCHeader else toCSource
mapM_ (hPutStrLn stderr) errs
putPP (C.pretty src)
when (not $ null errs) exitFailure
Left errs -> mapM_ (hPutStrLn stderr) errs >> exitFailure
coq2c.cabal deleted 100644 → 0
+ 0
− 33
View file @ 1c9e0f83
name: coq2c
version: 0.1.0.0
synopsis: compile some monadic Coq code into C code
description: Compile Coq code written in an imperative style
using a monad into the corresponding C code.
Start from the Coq code extracted as JSON by the
internal extraction facility.
license: OtherLicense
license-file: LICENSE
author: Veïs Oudjail <veis.oudjail@gmail.com>
maintainer: Samuel Hym <samuel.hym+bugs@rustyne.lautre.net>
copyright: Université Lille 1, Veïs Oudjail
category: Language
build-type: Simple
extra-source-files: Readme.md
cabal-version: >=1.10
executable coq2c
main-is: coq2c.hs
other-extensions: OverloadedStrings
build-depends: base >=4.7 && <4.9,
aeson >=0.11 && <0.12,
split >=0.2 && <0.3,
optparse-applicative >=0.12 && <0.13,
regex-posix >=0.95 && <0.96,
bytestring >=0.10 && <0.11
default-language: Haskell2010
coq2c.hs deleted 100644 → 0
+ 0
− 1367
View file @ 1c9e0f83
-- |
-- Module : Extractor (Main)
-- Copyright : Veïs Oudjail 2016
-- License : CeCILL
--
-- Maintainer : veis.oudjail@gmail.com
-- samuel.hym+bugs@rustyne.lautre.net
-- Stability : experimental
-- Portability : multi plateform
--
-- Description : Compiler Coq (AST JSON) -> subset C
--
-- This software is a computer program whose purpose is to run a minimal,
-- hypervisor relying on proven properties such as memory isolation.
-- This software is governed by the CeCILL license under French law and
-- abiding by the rules of distribution of free software. You can use,
-- modify and/ or redistribute the software under the terms of the CeCILL
-- license as circulated by CEA, CNRS and INRIA at the following URL
-- "http://www.cecill.info".
-- As a counterpart to the access to the source code and rights to copy,
-- modify and redistribute granted by the license, users are provided only
-- with a limited warranty and the software's author, the holder of the
-- economic rights, and the successive licensors have only limited
-- liability.
-- In this respect, the user's attention is drawn to the risks associated
-- with loading, using, modifying and/or developing or reproducing the
-- software by the user in light of its specific status of free software,
-- that may mean that it is complicated to manipulate, and that also
-- therefore means that it is reserved for developers and experienced
-- professionals having in-depth computer knowledge. Users are therefore
-- encouraged to load and test the software's suitability as regards their
-- requirements in conditions enabling the security of their systems and/or
-- data to be ensured and, more generally, to use and operate it in the
-- same conditions as regards security.
-- The fact that you are presently reading this means that you have had
-- knowledge of the CeCILL license and that you accept its terms.
{-# LANGUAGE OverloadedStrings #-}
module Main where
import Control.Applicative
import Control.Monad (zipWithM, join)
import Data.Aeson
import Data.Bool (bool)
import Data.Char (toUpper)
import Data.List (intercalate, union, find)
import Data.List.Split (splitOn)
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
import Options.Applicative (strArgument,strOption,short,long,metavar,optional,help)
import System.Environment (getProgName)
import Text.Regex.Posix ((=~))
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Options.Applicative as OA
concatMapM :: (Functor m, Monad m) => (a -> m [b]) -> [a] -> m [b]
concatMapM f = fmap concat . mapM f
----------- Module ASTCoq -----------------
-- Ce type peut-être interprété comme une énumération.
-- Chacun de ses éléments représente une entité de l'arbre syntaxique Coq.
data WhatT = DeclT DeclT | FixgrpT FixgrpT | TypeT TypeT
| ExprT ExprT | CaseT | PatT PatT
| ModuleT
deriving (Show)
data DeclT = TermDT | FixgrpDT
deriving (Show)
data FixgrpT = ItemFT
deriving (Show)
data TypeT = ArrowTT | GlobTT | VaridxTT
deriving (Show)
data ExprT = LambdaET| ApplyET | GlobalET | ConstructorET | RelET | CaseET | LetET
deriving (Show)
data PatT = ConstructorPT | WildPT
deriving (Show)
instance FromJSON WhatT where
parseJSON (Object v) = toWhatType <$> v .: "what"
parseJSON _ = fail "Error, WhatType : undefined !"
-- Fonction qui permet de transformer les étiquettes dans le type enuméré
toWhatType :: String -> WhatT
toWhatType strType =
case strType of
"case" -> CaseT
"module" -> ModuleT
"decl:term" -> DeclT TermDT
"decl:fixgroup" -> DeclT FixgrpDT
"fixgroup:item" -> FixgrpT ItemFT
"type:arrow" -> TypeT ArrowTT
"type:glob" -> TypeT GlobTT
"type:varidx" -> TypeT VaridxTT
"expr:lambda" -> ExprT LambdaET
"expr:apply" -> ExprT ApplyET
"expr:global" -> ExprT GlobalET
"expr:constructor" -> ExprT ConstructorET
"expr:rel" -> ExprT RelET
"expr:case" -> ExprT CaseET
"expr:let" -> ExprT LetET
"pat:constructor" -> PatT ConstructorPT
"pat:wild" -> PatT WildPT
strError -> error $ "Error WhatType : " ++ strError ++ " format undefined"
--------------------------------------------------------------
data Decl = Term { nameTerm :: String
, typeTerm :: Type
, valueTerm :: Expr
}
| Fixgroup { fixlistFixgroup :: [Fixgroup]
}
deriving (Show)
instance FromJSON Decl where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
DeclT TermDT ->
Term <$>
v .: "name" <*>
v .: "type" <*>
v .: "value"
DeclT FixgrpDT ->
Fixgroup <$>
v .: "fixlist"
_ -> fail "Error, Decl : case undefined !"
parseJSON _ = fail "Error, Decl : undefined !"
data Fixgroup = Item { nameItem :: String
, typeItem :: Type
, valueItem :: Expr
}
deriving (Show)
instance FromJSON Fixgroup where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
FixgrpT ItemFT ->
Item <$>
v .: "name" <*>
v .: "type" <*>
v .: "value"
_ -> fail "Error, Fixgroup : case undefined !"
parseJSON _ = fail "Error, Fixgroup : undefined !"
data Type = Arrow { leftArrow :: Type
, rightLeft :: Type
}
| Glob { nameGlob :: String
, argsGlob :: [Type]
}
| Varidx { nameVaridx :: Integer
}
deriving (Show)
instance FromJSON Type where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
TypeT ArrowTT ->
Arrow <$>
v .: "left" <*>
v .: "right"
TypeT GlobTT ->
Glob <$>
v .: "name" <*>
v .: "args"
TypeT VaridxTT ->
Varidx <$>
v .: "name"
_ -> fail "Error, Type : case undefined !"
parseJSON _ = fail "Error, Type : undefined !"
data Expr = Lambda { argnamesLambda :: [String]
, bodyLambda :: Expr
}
| Apply { funcApply :: Expr
, argsApply :: [Expr]
}
| Global { nameGlobal :: String
}
| ConstructorE { nameConstructorE :: String
, argsConstructorE :: [Expr]
}
| Rel { nameRel :: String
}
| Case { exprCase :: Expr
, casesCase :: [Case]
}
| Let { nameLet :: String
, namevalLet :: Expr
, bodyLet :: Expr
}
deriving (Show)
instance FromJSON Expr where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
ExprT LambdaET ->
Lambda <$>
v .: "argnames" <*>
v .: "body"
ExprT ApplyET ->
Apply <$>
v .: "func" <*>
v .: "args"
ExprT GlobalET ->
Global <$>
v .: "name"
ExprT ConstructorET ->
ConstructorE <$>
v .: "name" <*>
v .: "args"
ExprT RelET ->
Rel <$>
v .: "name"
ExprT CaseET ->
Case <$>
v .: "expr" <*>
v .: "cases"
ExprT LetET ->
Let <$>
v .: "name" <*>
v .: "nameval" <*>
v .: "body"
_ -> fail "Error, Expr : case undefined !"
parseJSON _ = fail "Error, Expr : undefined !"
data Case = C { patC :: Pat
, bodyC :: Expr
}
deriving (Show)
instance FromJSON Case where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
CaseT ->
C <$>
v .: "pat" <*>
v .: "body"
_ -> fail "Error, Case : case undefined !"
parseJSON _ = fail "Error, Case : undefined !"
data Pat = ConstructorP { nameConstructorP :: String
, argnamesConstructorP :: [String]
}
| WildP
deriving (Show)
instance FromJSON Pat where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
PatT ConstructorPT ->
ConstructorP <$>
v .: "name" <*>
v .: "argnames"
PatT WildPT -> return WildP
_ -> fail "Error, Pat : case undefined !"
parseJSON _ = fail "Error, Pat : undefined !"
data Module = Mod { nameMod :: String
, needMagicMod :: Bool
, needDummyMod :: Bool
, usedModulesMod :: [ModuleUsed]
, declarationsMod :: [Decl]
}
deriving (Show)
type ModuleUsed = String
type FileName = String
instance FromJSON Module where
parseJSON (Object v) =
do what <- toWhatType <$> v .: "what"
case what of
ModuleT ->
Mod <$>
v .: "name" <*>
v .: "need_magic" <*>
v .: "need_dummy" <*>
v .: "used_modules" <*>
v .: "declarations"
_ -> fail "Error, Module : case undefined !"
parseJSON _ = fail "Error, Module : undefined !"
data ASTCoq = ModuleAST Module
| TypeAST Type
| ExprAST Expr
| CaseAST Case
| DeclAST Decl
| FixgroupAST Fixgroup
| PatAST Pat
--------------------- Monad MyEither -----------------------------------
-- Définition du type Monadique, représente le resultat de transformation.
-- Cela marche comme la monade Maybe. La différence vient du fait que lorsque l'on echoue
-- on peut l'associé à un message d'erreur.
-- Pour ce faire on definie un nouveau type, qui est un wrapper sur le type Either
newtype MyEither a = MyEith (Either String a)
deriving (Show)
instance Functor MyEither where
fmap f (MyEith me) = case me of
Left l -> MyEith $ Left l
Right r -> MyEith $ Right (f r)
instance Applicative MyEither where
pure = MyEith . Right
(MyEith f) <*> (MyEith (Right r)) = case f of
Left l -> MyEith $ Left l
Right f' -> MyEith $ Right (f' r)
_ <*> (MyEith (Left l)) = MyEith $ Left l
instance Monad MyEither where
return = pure
fail = MyEith . Left
(MyEith me) >>= f = case me of
Left l -> MyEith $ Left l
Right r -> f r
-- Fonction qui permet de transformer une monade Maybe en une monade MyEither
-- @param strErr : Représente le message d'erreur, si la monade est dans un etat d'echec
-- @param maybe : Représente la monade Maybe qui sera convertit
-- @return : On retourne une entité MyEither construite à partir des param fixé
toMyEith :: String -> Maybe a -> MyEither a
toMyEith strErr Nothing = fail strErr
toMyEith _ (Just x) = return x
-- Même principe que pour la fonction toMyEith, à la différence que le message d'erreur n'est pas renseigné
toMyEith' :: Maybe a -> MyEither a
toMyEith' = toMyEith ""
-- Getteur, permet d'extraire du type MyEither l'objet de type either
myEither :: MyEither a -> Either String a
myEither (MyEith x) = x
-- Cette fonction permet d'ajouter un message d'erreur si le contexte générale est dans un etat d'echec
-- @param trace : Message d'erreur à ajouter
-- @param myEith : Représente le contexte, si l'etat est dans un mode echec, on ajoute un message d'erreur
-- @return : Retourne le contexte, avec potentiellement l'ajout d'un nouveau message
addTraceMyEith :: String -> MyEither b -> MyEither b
addTraceMyEith trace (MyEith (Left x)) = fail $ trace ++ "\n" ++ x
addTraceMyEith _ x = x
-- Cet opérateur permet de combiner different contexte. La combinaison ce fait comme un 'ou'.
-- Si le contexte de gauche echoue, on renvoie le contexte de droite, et inversemement.
infixr 2 |||
(|||) :: MyEither a -> MyEither a -> MyEither a
(MyEith (Left err)) ||| y = addTraceMyEith err y
x ||| _ = x
------------------- Module ASTC -----------------------------------------
-- Définition des différente entité correspondant à l'arbre syntaxique du sous-ensemble C
data FunctionC = FunctionC { prototypeFun :: PrototypeC
, bodyFun :: [InstructionC]
}
deriving (Show, Eq)
data PrototypeC = PrototypeC { nameProto :: String
, returnTypeProto :: TypeC
, argsProto :: [DeclVarC]
}
deriving (Show, Eq)
data InstructionC = CSC { cSC :: ControlStructC
}
| ExprC { exprC :: ExprC
}
| DeclVarC { declVarC :: DeclVarC
}
| ReturnC { returnC :: ExprC
}
deriving (Show, Eq)
data ControlStructC = Iter { iterC :: IterativeStructC
}
| Cond { condC :: ConditionalStructC
}
deriving (Show, Eq)
data IterativeStructC = WhileC { conditionWhile :: ExprC
, bodyWhile :: [InstructionC]
}
deriving (Show, Eq)
data ConditionalStructC = IfThenElseC { conditionIf :: ExprC
, bodyThen :: [InstructionC]
, bodyElse :: [InstructionC]
}
deriving (Show, Eq)
data ExprC = ApplyFunC { funApplyFun :: String
, argsApplyFun :: [ExprC]
}
| BinOp { leftBO :: ExprC
, symboleBO :: String
, rightBO :: ExprC
}
| VarC { varC :: VarC
}
| ValC { valC :: ValC
}
deriving (Show, Eq)
data DeclC = VarCDecl { varCDecl :: DeclVarC
}
| FunDecl { funDecl :: FunctionC
}
| ObjectDecl { objectDecl :: DeclObjectC
}
| ProtoDecl { protoDecl :: PrototypeC
}
| CommDecl { commDecl :: CommentaryC
}
deriving (Show, Eq)
data DeclVarC = VarEmptyDecl { lvalueEDecl :: VarC
}
| VarDecl { lvalueDecl :: VarC
, rvalueDecl :: ExprC
}
deriving (Show, Eq)
data DeclObjectC = StructDecl { nameStructDecl :: String
, bodyStructDecl :: [DeclVarC]
}
| EnumDecl { nameEnumDecl :: String
, bodyEnumDecl :: [String]
}
deriving (Show, Eq)
data ModuleC = ModuleC FileName FileH FileC
deriving (Show, Eq)
data FileC = FileC { includeFC :: [IncludeC]
, bodyFC :: [DeclC]
}
deriving (Show, Eq)
type FileH = FileC
data IncludeC = GloIncC String
| LocIncC String
deriving (Show, Eq, Read)
data TypeC = TypeC String
| TypeCFun [TypeC]
deriving (Show, Eq)
type CommentaryC = String
type DataC = String
type NameC = String
type MacroIncBegin = String
type MacroIncEnd = String
type VarC = (NameC, TypeC)
type ValC = (DataC, TypeC)
----------- Definition du type Parser ----------------------
data ParseError = PE_NOT_IF_THEN_ELSE
type Parser a b = (a -> MyEither b)
typeVoid :: TypeC
typeVoid = TypeC "void"
bodyLambdaM :: Expr -> MyEither Expr
bodyLambdaM (Lambda _ b) = (MyEith . Right) b
bodyLambdaM _ = fail "bodyLambdaM, fail : "
lvalueOfDeclV :: DeclVarC -> VarC
lvalueOfDeclV (VarEmptyDecl v) = v
lvalueOfDeclV (VarDecl v _) = v
isDeclFun :: DeclC -> Bool
isDeclFun (FunDecl _) = True
isDeclFun _ = False
isDeclObjectC :: DeclC -> Bool
isDeclObjectC (ObjectDecl _) = True
isDeclObjectC _ = False
isTypeCFun :: TypeC -> Bool
isTypeCFun (TypeCFun _) = True
isTypeCFun _ = False
typeRetTypeC :: TypeC -> TypeC
typeRetTypeC (TypeCFun t) = last t
typeRetTypeC t@TypeC{} = t
elmTypeC :: TypeC -> [TypeC]
elmTypeC (TypeCFun t) = t
elmTypeC t@TypeC{} = [t]
prototypeOfDeclC :: [DeclC] -> [PrototypeC]
prototypeOfDeclC ldecl = map (prototypeFun . funDecl) lfun
where lfun = filter isDeclFun ldecl
objectCOfDeclC :: [DeclC] -> [DeclObjectC]
objectCOfDeclC ldecl = map objectDecl (filter isDeclObjectC ldecl)
clearPref :: NameCoq -> NameC
clearPref = last . (splitOn ".")
addDeclCToFileC :: FileC -> [DeclC] -> FileH
addDeclCToFileC (FileC incC's declC'ss) declC's = FileC incC's (declC's ++ declC'ss)
addDeclCToModCFileH :: ModuleC -> [DeclC] -> ModuleC
addDeclCToModCFileH (ModuleC n fH fC) declC's = ModuleC n (addDeclCToFileC fH declC's) fC
------------- Module Env -----------------------------------
-- Ce module permet de definir les structures modélisant l'environnement du traducteur.
-- Definition des synonymes de types utilisés pour définir l'environnement
type NameCoqType = String
type NameCoqFun = String
type NameCoqConstruct = String
type SymbolBinOp = String
type NameCFun = String
type NameCoq = String
-------------------------------------------------------------------------------
-- Cette objet represente les differente formes que l'on peux prendre dans l'environnement utilisateur
-- Forme NewTypeEUI :
---- Cela représente ...
-- Forme NewFunEUI
---- Cela représente ...
-- Forme NewVarEUI
---- Cela représente ...
-- Forme OpBinEUI
---- Cela représente ...
-- Forme IncludeListEUI
---- Cela représente ...
data EnvUserItem = NewTypeEUI { nameCoqNNEUI :: NameCoq
, pTypeNNEUI :: EnvG -> Parser (Either Type Expr) TypeC
, pValCNNEUI :: [(NameCoqConstruct, NameCoq -> EnvG -> Parser Expr ExprC)]
}
| NewFunEUI { nameCoqNNEUI :: NameCoq
, nameCNNEUI :: NameC
, pTypeNNEUI :: EnvG -> Parser (Either Type Expr) TypeC
, nArgsNNEUI :: Int
}
| NewVarEUI { nameCoqNVEUI :: NameCoq
, newDeclVarC :: DeclVarC
}
| OpBinEUI { nameCoqOBEUI :: NameCoq
, nameCOBEUI :: SymbolBinOp
, pTypeOBEUI :: EnvG -> Parser (Either Type Expr) TypeC
}
| IncludeListEUI { nameModuleEUI :: ModuleUsed
, includeListEUI :: [(NameCoq, [IncludeC])]
}
data EnvArgs = EnvArgs { importOpt :: [String]
, gloIncOpt :: [String]
, locIncOpt :: [String]
, headerOpt :: Maybe String
, outputOpt :: Maybe String
, outputHOpt :: Maybe String
, inputOpt :: String
}
data EnvTypeItem = ETI { idET :: String, funET :: EnvG -> Parser (Either Type Expr) TypeC }
instance Eq EnvTypeItem where
(ETI id' _) == (ETI id'' _) = id' == id''
instance Show EnvTypeItem where
show (ETI id' _) = id'
type EnvVarC = [DeclVarC]
type EnvType = [EnvTypeItem]
type EnvChangeName = [(NameCoqFun, NameCFun)]
newtype EnvValC = EVC { evc :: [(NameCoqConstruct, EnvG -> Parser Expr ExprC)]}
newtype EnvFunApply = EFA [EnvG -> Parser Expr ExprC]
type EnvG = (EnvVarC, EnvType, EnvValC, EnvFunApply, EnvChangeName)
type EnvUser = [EnvUserItem]
instance Show EnvValC where
show (EVC l) = show $ map fst l
----------------------------------------------
type EnvIncG = [(String, [IncludeC])]
type EnvBinOp = [(NameCoqFun, SymbolBinOp)]
newtype EnvCondC = EC [EnvG -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)]
----------------------------------------------
type ExprValC = ExprC
lookupEnvV :: Expr -> EnvG -> MyEither (Parser Expr ExprValC)
lookupEnvV (ConstructorE k _) env@(_,_,ev,_,_) = toMyEith "lookupEnvV undefined, constructor case" $ lookup (clearPref k) (evc ev) <*> return env
lookupEnvV _ _ = fail "lookupEnvV undefined"
lookupEnvT :: String -> EnvG -> MyEither (Parser (Either Type Expr) TypeC)
lookupEnvT k env@(_,et,_,_,_) = toMyEith ("lookupEnvT undefined, key : " ++ (clearPref k)) $ lookup (clearPref k) $ map (\(ETI k' f )-> (k', f env)) et
lookupEnvVar :: NameCoq -> EnvG -> MyEither TypeC
lookupEnvVar name (ev,_,_,_,_) = toMyEith "lookupEnvVar undefined" $ lookup (clearPref name) (map lvalueOfDeclV ev)
lookupEnvN :: NameCoq -> EnvG -> MyEither NameC
lookupEnvN nCoq (_,_,_,_,en) = toMyEith "lookupEnvN undefined" $ lookup (clearPref nCoq) en
lookupEnvBinOp :: NameCoq -> EnvBinOp -> MyEither NameC
lookupEnvBinOp k envbop = toMyEith "lookupEnvBinOp undefined" $ lookup (clearPref k) envbop
lookupEnvInc :: ModuleUsed -> ModuleUsed -> EnvUser -> MyEither [IncludeC]
lookupEnvInc mu minc eu = toMyEith "lookupEnvInc undefined" body
where inclL = filter (\x -> case x of {IncludeListEUI{} -> True; _ -> False}) eu
itemInc = find ((mu ==) . nameModuleEUI) inclL
body = do einc <- includeListEUI <$> itemInc
lookup minc einc
lookupEnvIncG :: ModuleUsed -> EnvIncG -> MyEither [IncludeC]
lookupEnvIncG minc einc = toMyEith "lookupEnvInc undefined" $ lookup minc einc
-- lookupReverseEnvN :: NameC -> EnvG -> MyEither NameCoq
-- lookupReverseEnvN nC (_,_,_,_,en) = toMyEith "lookupReverseEnvN undefined" $ lookup (clearPref nC) $ map (\(a,b) -> (b,a)) en
-- existNameCEnvN :: NameC -> EnvG -> Bool
-- existNameCEnvN nC env = (isRight . myEither) . lookupReverseEnvN nC env
runParserEnvT :: String -> EnvG -> Parser (Either Type Expr) TypeC
runParserEnvT k env eith = join $ (\f -> f eith) <$> lookupEnvT k env
runParserEnvV :: EnvG -> Parser Expr ExprValC
runParserEnvV env expr = join $ (\f -> f expr) <$> lookupEnvV expr env
runParserEnvFApply :: EnvG -> Parser Expr ExprC
runParserEnvFApply env@(_,_,_,EFA efa,_) c = foldr (\f fs -> f env c ||| fs) (fail "runParserEnvFApply undefined") efa
runParserEnvCondC :: EnvG -> EnvCondC -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)
runParserEnvCondC env (EC envc) expr pat = foldr (\f fs -> f env expr pat ||| fs) (fail "runParserEnvCondC undefined") envc
retConstPType :: String -> TypeC -> EnvTypeItem
retConstPType nameCoq typeC = ETI nameCoq (\_ _ -> return typeC)
retValC :: DataC -> NameCoq -> Expr -> EnvG -> MyEither ExprC
retValC dataC nC c@(ConstructorE _ args) env = ValC . (,) dataC <$> pCaseIfArgs
where pCaseIfArgs = bool (parseExprOfTypeC env c) -- case False
(parseTypeC env (Glob nC [])) $ null args
retValC _ _ _ _ = fail "retValC undefined"
mergeEnvG :: EnvG -> EnvG -> EnvG
mergeEnvG (ev, et, ec, ef, en) (ev', et', _, _, _) = (ev' `union` ev, et `union` et', ec, ef, en)
addVarsCEnvG :: EnvG -> EnvVarC -> EnvG
addVarsCEnvG (v, t, ec, ef, en) e = (e ++ v, t, ec, ef, en)
addTypeCEnvT :: EnvG -> EnvType -> EnvG
addTypeCEnvT (v, t, ec, ef, en) e = (v, t `union` e, ec, ef, en)
envTypeG :: EnvG -> EnvType
envTypeG (_, envt, _, _, _) = envt
----------------------
envUser :: EnvUser
envUser = [ NewTypeEUI "bool" pBoolC [("Coq_true", pTrueValC), ("Coq_false", pFalseValC)]
, NewTypeEUI "unit" pVoidC [("Coq_tt", pVoidValC)]
, NewTypeEUI "nat" pUnsignedC [("O", pOValC), ("S", pSValC)]
, NewTypeEUI "coq_LLI" pLLIOfTypeC []
, NewTypeEUI "index" pUint32C []
, NewTypeEUI "page" pUintPtrC []
, NewTypeEUI "vaddr" pUintPtrC []
, NewTypeEUI "level" pUint32C []
, NewTypeEUI "count" pUint32C []
, OpBinEUI "orb" "||" pBoolC
, OpBinEUI "eqb" "==" pBoolC
, OpBinEUI "andb" "&&" pBoolC
--, OpBinEUI "sub" "-" pUnsignedC
, OpBinEUI "gtbLevel" ">" pBoolC
, OpBinEUI "gtbIndex" ">" pBoolC
, OpBinEUI "ltbIndex" "<" pBoolC
, OpBinEUI "gebIndex" ">=" pBoolC
, OpBinEUI "lebIndex" "<=" pBoolC
, OpBinEUI "indexEq" "==" pBoolC
, OpBinEUI "levelEq" "==" pBoolC
, OpBinEUI "gebCount" ">=" pBoolC
--, NewFunEUI "coq_Kidx" "Kidx" pUint32C 0
, NewFunEUI "negb" "!" pBoolC 1
, NewFunEUI "ret" "" pRetOfTypeC 1
, NewFunEUI "i" "" pIOfTypeC 1
----------------------------- Mal --------------------------------------------
, NewFunEUI "nb_level" "nb_level" pUnsignedC 0
, NewFunEUI "table_size" "table_size" pUnsignedC 0
, NewFunEUI "fstLevel" "fstLevel" pUint32C 0
{-
, NewFunEUI "writePhyEntry" "writePhysicalWithLotsOfFlags" pVoidC 8
, NewFunEUI "writeVirEntry" "writePhysical" pVoidC 3
, NewFunEUI "readPhyEntry" "readPhysical" pUintPtrC 2
, NewFunEUI "readVirEntry" "readPhysical" pUintPtrC 2
, NewFunEUI "getNbLevel" "getNbIndex" pUint32C 0
, NewFunEUI "getIndexOfAddr" "getIndexOfAddr" pUint32C 2
, NewFunEUI "readPhysical" "readPhysical" pUintPtrC 2
, NewFunEUI "writePhysical" "writePhysical" pVoidC 3
, NewFunEUI "readVirtual" "readPhysical" pUintPtrC 2
, NewFunEUI "writeVirtual" "writePhysical" pVoidC 3
, NewFunEUI "fetchVirtual" "readVirtual" pUintPtrC 2
, NewFunEUI "storeVirtual" "writeVirtual" pVoidC 3
, NewFunEUI "readIndex" "readIndex" pUint32C 2
, NewFunEUI "writeIndex" "writeIndex" pVoidC 3
, NewFunEUI "readPresent" "readPresent" pBoolC 2
, NewFunEUI "writePresent" "writePresent" pVoidC 3
, NewFunEUI "readAccessible" "readAccessible" pBoolC 2
, NewFunEUI "writeAccessible" "writeAccessible" pVoidC 3
, NewFunEUI "derivated" "derivated" pBoolC 2
, NewFunEUI "writePDflag" "writePDflag" pVoidC 3
, NewFunEUI "readPDflag" "readPDflag" pBoolC 2
, NewFunEUI "getCurPartition" "get_current_pd" pUintPtrC 0
, NewFunEUI "defaultPhysical" "defaultAddr" pUintPtrC 0
, NewFunEUI "defaultVirtual" "defaultAddr" pUintPtrC 0
, NewFunEUI "getMaxIndex" "getMaxIndex" pUint32C 0
, NewFunEUI "addressEqualsPhy" "addressEquals" pBoolC 2
, NewFunEUI "addressEqualsVir" "addressEquals" pBoolC 2
, NewFunEUI "getIndex" "toAddr" pUint32C 1
, NewFunEUI "checkRights" "checkRights" pBoolC 3
, NewFunEUI "levelPred" "sub" pUint32C 1
, NewFunEUI "levelSucc" "inc" pUint32C 1
, NewFunEUI "indexZero" "indexZero" pUint32C 0
, NewFunEUI "indexKernel" "kernelIndex" pUint32C 0
, NewFunEUI "indexPR" "kernelIndex" pUint32C 0
, NewFunEUI "indexPD" "kernelIndex" pUint32C 0
, NewFunEUI "indexSh1" "kernelIndex" pUint32C 0
, NewFunEUI "indexSh2" "kernelIndex" pUint32C 0
, NewFunEUI "indexSh3" "kernelIndex" pUint32C 0
, NewFunEUI "indexPRP" "kernelIndex" pUint32C 0
, NewFunEUI "indexPred" "sub" pUint32C 1
, NewFunEUI "indexSucc" "inc" pUint32C 1
, NewFunEUI "levelToCountProd3" "levelToCountProd3" pUint32C 1
, NewFunEUI "countZero" "indexZero" pUint32C 0
, NewFunEUI "countSucc" "inc" pUint32C 1 -}
]
where pBoolC _ = const $ return (TypeC "uint32_t")
pUintPtrC _ = const $ return (TypeC "uintptr_t")
pUint32C _ = const $ return (TypeC "uint32_t")
pVoidC _ = const $ return (TypeC "void")
pUnsignedC _ = const $ return (TypeC "unsigned")
pUndefTypeC _ _ = fail ""
pRetOfTypeC env x = case x of
Right (Apply _ [arg]) -> parseExprOfTypeC env arg
_ -> fail "pRetOfTypeC undefined"
pIOfTypeC env x = case x of
Right (Apply _ [arg]) -> parseExprOfTypeC env arg
_ -> fail "pIOfTypeC undefined"
pLLIOfTypeC env x = case x of
Left (Glob _ [arg]) -> parseTypeC env arg
_ -> fail "pLLIOfTypeC undefined"
------------------------ Parser ValC ----------------------------------------------------
pTrueValC nt env c@(ConstructorE _ []) = retValC "1" nt c env
pTrueValC _ _ _ = fail "pTrueValC undefined"
pFalseValC nt env c@(ConstructorE _ []) = retValC "0" nt c env
pFalseValC _ _ _ = fail "pFalseValC undefined"
pVoidValC nt env c@(ConstructorE _ []) = retValC "" nt c env
pVoidValC _ _ _ = fail "pVoidValC undefined"
pOValC nt env c@(ConstructorE _ []) = retValC "0" nt c env
pOValC _ _ _ = fail "pOValC undefined"
pSValC nt env (ConstructorE _ [p]) =
do res <- parseExprC env p
case res of
ValC (d, t) -> return $ ValC (show $ 1 + (read d :: Int), t)
expr -> do tC <- parseTypeC env tCoq
return $ BinOp (ValC ("1", tC)) "+" expr
where tCoq = Glob nt []
pSValC _ _ _ = fail "pSValC undefined"
envFunApply :: EnvUser -> EnvFunApply
envFunApply eu = EFA [ pRet
, pI
, parseOpBinOPC (envBinOp eu)
]
where pRet env (Apply (Global "Hardware.ret") [expr]) = parseExprC env expr
pRet _ _ = fail "pRet undefined"
pI env (Apply (Global "Parameters.i") [expr]) = parseExprC env expr
pI _ _ = fail "pI undefined"
envChangeName :: EnvUser -> EnvChangeName
envChangeName = foldr (\x y -> case x of { NewFunEUI nCoq nC _ _ -> [(nCoq, nC)]; _ -> []} ++ y) []
envBinOp :: EnvUser -> EnvBinOp
envBinOp = foldr (\x y -> case x of { OpBinEUI nCoq symb _ -> [(nCoq, symb)]; _ -> []} ++ y) []
envCondC :: EnvCondC
envCondC = EC [pPatOExprC, pPatTrueExprC, pPatFalseExprC, pPatSExprC]
envIncG :: ModuleUsed -> EnvUser -> MyEither EnvIncG
envIncG mu eu = toMyEith "envIncG construct undefined" body
where inclL = filter (\x -> case x of {IncludeListEUI{} -> True; _ -> False}) eu
body = includeListEUI <$> find ((mu ==) . nameModuleEUI) inclL
envType :: EnvUser -> EnvType
envType = foldr (\x y -> case x of
NewTypeEUI tCoq tC ev -> ETI tCoq tC : foldr (\(tCoq',_) y' -> ETI tCoq' tC : y') [] ev
OpBinEUI nCoq _ tC -> [ETI nCoq tC]
NewFunEUI nCoq _ tC n -> [ETI nCoq (f n tC)] -- TypeCFun tC
NewVarEUI _ _ -> []
_ -> []
--NewVarEUI nCoq (VarEmptyDecl (_, tC)) -> [retConstPType nCoq tC]
--NewVarEUI nCoq (VarDecl (_, tC) _) -> [retConstPType nCoq tC]
++ y) []
where f :: Int -> (EnvG -> Parser (Either Type Expr) TypeC) -> (EnvG -> Parser (Either Type Expr) TypeC)
f n p env e = TypeCFun . (replicate n (TypeC "") ++) . (:[]) <$> p env e
envValC :: EnvUser -> EnvValC
envValC = EVC . foldr (\x y -> case x of {NewTypeEUI nt _ ev -> map (\(n, f) -> (n, f nt) ) ev; _ -> []} ++ y) []
envVarC :: EnvUser -> EnvVarC
envVarC _ = []
envArgs :: OA.Parser EnvArgs
envArgs = EnvArgs <$> imports <*> gloincs <*> locincs <*> header <*> output <*> outputH <*> input
where input = strArgument $ metavar "INPUT.json"
<> help "Coq module (extracted as JSON) to compile into C code"
imports = many $ strOption $
short 'm'
<> long "module"
<> metavar "MODULE.json"
<> help "load function names and types from the given Coq MODULE (extracted as JSON)"
gloincs = many $ strOption $
short 'i'
<> long "include"
<> metavar "INCL.h"
<> help "add #include directive for this (global) header file"
locincs = many $ strOption $
short 'I'
<> long "locinclude"
<> metavar "INCL.h"
<> help "add #include directive for this local header file"
header = optional $ strOption $
long "header"
<> metavar "FILE"
<> help "add the content of FILE to the header of the generated C file"
output = optional $ strOption $
short 'o'
<> long "output"
<> metavar "FILE.c"
<> help "output extracted C code into FILE.c (defaults to INPUT.c)"
outputH = optional $ strOption $
short 'O'
<> long "output-h"
<> metavar "FILE.h"
<> help "output extracted C code headers into FILE.h"
envG :: EnvUser -> EnvG
envG eu = (envVarC eu, envType eu, envValC eu, envFunApply eu, envChangeName eu)
------------------------------------------
parseMacroTypeC :: Parser Type TypeC
parseMacroTypeC type' = TypeC <$> f type'
where f :: Parser Type String
f t = case t of
Glob n [] -> parseNameC n
Glob n (p:ps) -> do nm <- parseNameC n
p1 <- f p
pn <- concatMapM (\p' -> (", "++) <$> f p') ps
return $ nm ++ "(" ++ p1 ++ pn ++ ")"
_ -> fail "parseMacroTypeC undefined"
parseError :: ParseError -> String
parseError PE_NOT_IF_THEN_ELSE = "The pattern matching is not possible to parse in the conditionnal struct"
parseOpBinOPC :: EnvBinOp -> EnvG -> Parser Expr ExprC
parseOpBinOPC envb env (Apply (Global op) args) = if length args /= 2
then fail "parseOpBinOPC : Arguments > 2"
else do yop <- lookupEnvBinOp op envb
le <- parseExprC env (head args)
re <- parseExprC env (args !! 1)
return $ BinOp le yop re
parseOpBinOPC _ _ _ = fail "parseOpBinOPC undefined"
parseTypeC :: EnvG -> Parser Type TypeC
parseTypeC env tp = do r <- pType tp
return (if length r == 1
then head r
else TypeCFun r
)
where pType :: Parser Type [TypeC]
pType t = case t of
Varidx{} -> fail "Exception, error variable type"
Glob n _ -> (:[]) <$> (runParserEnvT n env (Left t) ||| parseMacroTypeC t)
Arrow l@Arrow{} r -> (:) <$> (TypeCFun <$> pType l) <*> pType r
Arrow l r -> (++) <$> pType l <*> pType r
parseNameC :: Parser NameCoq NameC
parseNameC nameCoq = if nameC == nameCoq'
then return nameC
else fail $ "parseNameC fail, the identifier is not correct : " ++ nameCoq
where nameCoq' = clearPref nameCoq
pattern' = "[a-zA-Z_](_?[a-zA-Z0-9]+)*" :: String
nameC = (nameCoq' =~ pattern') :: String
parseExprOfTypeC :: EnvG -> Parser Expr TypeC
parseExprOfTypeC env expr = case expr of
Rel name -> lookupEnvVar name env -- Regarde dans l'environnement des variables locales
Global name -> typeRetTypeC <$> runParserEnvT name env (Right expr) -- Regarde dans l'environnement des types
Apply (Global fname) _ -> typeRetTypeC <$> runParserEnvT fname env (Right expr) -- idem
Apply (Rel fname) _ -> typeRetTypeC <$> lookupEnvVar fname env -- idem
ConstructorE name _ -> runParserEnvT name env (Right expr) -- idem
_ -> fail "parseExprOfTypeC undefined" -- Echoue en renvoyant Nothing
parseDeclVarC :: EnvG -> Parser (Either Decl Expr) (EnvG, DeclVarC)
parseDeclVarC env decl = case decl of
Left (Term n t@Glob{} (Lambda _ e@ConstructorE{})) -> do typeV <- parseTypeC env t
expr <- parseExprC env e
n' <- parseNameC n
let var = (n', typeV)
return ( addTypeCEnvT env [retConstPType n' typeV]
, VarDecl var expr
)
Right (Let n expr _) -> do rvalue <- parseExprC env expr
lvalType <- parseExprOfTypeC env expr
if lvalType == typeVoid
then fail "Exception parseDeclVar, the type of rvalue is void"
else do n' <- parseNameC n
let var = VarDecl (n', lvalType) rvalue -- Pas de reference sur la variable
return (addVarsCEnvG env [var], var)
_ -> fail $ "parseDeclVarC undefined, decl : " ++ take debugRender (show decl)
parseDeclC :: EnvG -> Parser Decl [DeclC]
parseDeclC e decl = case decl of
Term{} -> (:[]) . VarCDecl . snd <$> parseDeclVarC e (Left decl) |||
(:[]) . FunDecl <$> parseFunctionC e decl
Fixgroup{} -> map FunDecl <$> parseFunctionCFX e decl
parseDeclH :: EnvG -> Parser Decl (EnvG, [DeclC])
parseDeclH e decl = case decl of
Term{} -> parseDVar ||| parseProtoT
Fixgroup{} -> parseProtoTFX e transf
where parseDVar = do (eg,d) <- parseDeclVarC e (Left decl)
let var = VarEmptyDecl (lvalueDecl d)
return (addVarsCEnvG eg [var], [VarCDecl var])
parseProtoT = parsePrototypeC e (Left decl) >>= (\(eg,p) -> return (eg, [ProtoDecl p]))
transf = map Right (fixlistFixgroup decl) :: [Either Decl Fixgroup]
parseProtoTFX env d = case d of
[] -> return (env, [])
x:xs -> do (en1, proto) <- parsePrototypeC env x
let envn1 = addTypeCEnvT env (envTypeG en1)
(en, protos) <- parseProtoTFX envn1 xs
return (addTypeCEnvT envn1 (envTypeG en), ProtoDecl proto:protos)
parseAllDeclC :: EnvG -> Parser [Decl] [DeclC]
parseAllDeclC e = concatMapM (parseDeclC e)
parseAllDeclH :: EnvG -> Parser [Decl] (EnvG, [DeclC])
parseAllDeclH env decl = case decl of
[] -> return (env, [])
d:ds -> do (e1, ds1) <- parseDeclH env d
(en, dsn) <- parseAllDeclH env ds
return (mergeEnvG e1 en, ds1 ++ dsn)
parsePrototypeC :: EnvG -> Parser (Either Decl Fixgroup) (EnvG, PrototypeC)
parsePrototypeC env term =
case term of
(Left (Term n t v)) -> construct n t v
(Right (Item n t v)) -> construct n t v
_ -> fail "parsePrototypeC undefined"
where construct n' t' v' = do typeC <- parseTypeC env t'
argsProto' <- args n' (elmTypeC typeC) v'
name <- parseNameC n'
let retProto = typeRetTypeC typeC
return ( addTypeCEnvT env [retConstPType name typeC]
, PrototypeC name retProto argsProto'
)
args n' t (Lambda prm _) = if length t - 1 == length prm
then mergeParam t prm
else fail $ "Exception, detection of partiel application (definition) : function " ++ n'
args _ _ _ = fail "parsePrototypeC - args, undefined"
mergeParam = zipWithM (\a b -> VarEmptyDecl . flip (,) a <$> parseNameC b)
parseFunctionC :: EnvG -> Parser Decl FunctionC
parseFunctionC env t@Term{} = do prototype <- snd <$> parsePrototypeC env (Left t)
body <- bodyLambdaM (valueTerm t)
instructions <- parseInstructionC (addVarsCEnvG env (argsProto prototype)) body
return $ FunctionC prototype instructions
parseFunctionC _ _ = fail "parseFunctionC undefined"
parseFunctionCFX :: EnvG -> Parser Decl [FunctionC]
parseFunctionCFX env (Fixgroup l) = mapM (parseFunctionC env) lterm
where reformate (Item n t v) = Term n t v
lterm = map reformate l
parseFunctionCFX _ _ = fail "parseFunctionCFX"
parseInstructionC :: EnvG -> Parser Expr [InstructionC]
parseInstructionC env expr = case expr of
Rel{} -> multicase
Global{} -> multicase
ConstructorE{} -> multicase
Apply{} -> parseMonadBlockC env expr ||| multicase
Case{} -> (:[]) . CSC . Cond <$> parseConditionnalC envCondC env expr
(Let _ _ body) -> do (newEnv, varLet) <- parseDeclVarC env (Right expr)
instructions <- parseInstructionC newEnv body
return $ DeclVarC varLet : instructions
_ -> fail $ "parseInstructionC undefined " ++ take debugRender (show expr)
where multicase = do typeC <- parseExprOfTypeC env expr
if typeC == typeVoid
then (:[]) . ExprC <$> parseExprC env expr
else (:[]) . ReturnC <$> parseExprC env expr
parseMonadBlockC :: EnvG -> Parser Expr [InstructionC]
parseMonadBlockC env exprCoq = case exprCoq of
Apply (Global "Hardware.bind") [expr, Lambda [nameV] ninstr] ->
do rvalue <- parseExprC env expr
typeRvalue <- parseExprOfTypeC env expr
if nameV == "_"
then (ExprC rvalue:) <$> parseInstructionC env ninstr
else do nameC <- parseNameC nameV
let lvalue = (nameC, typeRvalue)
newEnv = addVarsCEnvG env [VarEmptyDecl lvalue]
(DeclVarC (VarDecl lvalue rvalue):) <$> parseInstructionC newEnv ninstr
_ -> fail "parseMonadBlockC undefined"
parseConditionnalC :: EnvCondC -> EnvG -> Parser Expr ConditionalStructC
parseConditionnalC envC env match = condC . cSC . head <$> if length (casesCase match) == 1 then fail "parseConditionnalC, error : l case < 1" else pC' match
where pC' :: Parser Expr [InstructionC]
pC' (Case expr cases) = case cases of
[] -> return []
[C pat body] -> -- else only
do exprC' <- parseExprC env expr
(declVM, _) <- runParserEnvCondC env envC exprC' pat
pInstr declVM body
C pat body:cs ->
do exprC' <- parseExprC env expr
(declVM, exprM) <- runParserEnvCondC env envC exprC' pat
exprB <- toMyEith' exprM
bThen <- pInstr declVM body
bElse <- pC' $ Case expr cs
return $ ((:[]) . CSC . Cond) $ IfThenElseC exprB bThen bElse
pC' _ = fail "parseConditionnalC undefined"
pInstr :: [DeclVarC] -> Parser Expr [InstructionC]
pInstr declV' body' = (++) (map DeclVarC declV') <$> parseInstructionC (addVarsCEnvG env declV') body'
---------- Pattern Conditionnal -------------------------------
pPatOExprC :: EnvG -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)
pPatOExprC _ match (ConstructorP "Datatypes.O" []) = return ([], return $ BinOp match "==" (ValC ("0", TypeC "unsigned")))
pPatOExprC _ _ _ = fail "pPatOExprC undefined"
pPatSExprC :: EnvG -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)
pPatSExprC _ match (ConstructorP "Datatypes.S" [p]) = do p' <- parseNameC p
return ([VarDecl (p', TypeC "unsigned") (BinOp match "-" (ValC ("1", TypeC "uint32_t")))], Nothing)
pPatSExprC _ _ _ = fail "pPatSExprC undefined"
pPatTrueExprC :: EnvG -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)
pPatTrueExprC _ match (ConstructorP "Datatypes.Coq_true" []) = return ([], return match)
pPatTrueExprC _ _ _ = fail "pPatTrueExprC undefined"
pPatFalseExprC :: EnvG -> ExprC -> Parser Pat ([DeclVarC], Maybe ExprC)
pPatFalseExprC _ match (ConstructorP "Datatypes.Coq_false" []) = return ([], return $ BinOp match "==" (ValC ("0", TypeC "uint32_t")))
pPatFalseExprC _ _ _ = fail "pPatFalseExprC undefined"
----------------------------------------------------------
parseExprC :: EnvG -> Parser Expr ExprC
parseExprC env expr = case expr of
Rel{} -> VarC <$> parseVarC env expr
Global{} -> VarC <$> parseVarC env expr ||| parseApplyFunC env expr
ConstructorE{} -> parseValC env expr
Apply{} -> parseApplyFunC env expr
_ -> fail $ "parseExprC undefined" ++ take (debugRender + 200) (show expr)
parseVarC :: EnvG -> Parser Expr VarC
parseVarC env expr = case expr of
(Rel var) -> construct var $ lookupEnvVar var env
(Global var) -> construct var (lookupEnvVar var env) ||| construct' var
_ -> fail "parseVarC undefined"
where construct var getType = do nVar <- parseNameC var
typeVar <- getType
return (nVar, typeVar)
construct' var = do let tm = runParserEnvT var env (Right expr)
t <- tm
if length (elmTypeC t) == 1
then fail "parseVarC fail, it's a function"
else construct var tm
parseValC :: EnvG -> Parser Expr ExprValC
parseValC env c@ConstructorE{} = runParserEnvV env c
parseValC _ _ = fail "parseValC undefined"
parseApplyFunC :: EnvG -> Parser Expr ExprC
parseApplyFunC env apply = runParserEnvFApply env apply ||| pApplyFunC
where pApplyFunC = case apply of
(Apply fun args) -> do f <- transformFun fun
a <- transformArgs args
status <- checkApplyPart f args
if status
then construct f a
else fail $ "Exception, detection of partiel application (application) : function " ++ f
(Global fun) -> construct fun []
_ -> fail "parseApplyFunC undefined"
transformFun (Global f) = return f
transformFun (Rel f) = return f
transformFun _ = fail "It's not function"
transformFun' f = lookupEnvN f env ||| parseNameC f
transformArgs = mapM (parseExprC env)
checkApplyPart nfun a = do t <- runParserEnvT nfun env (Right apply)
return $ length a == length (elmTypeC t) - 1
construct f a = do f' <- transformFun' f
return $ ApplyFunC f' a
parseFileC :: EnvArgs -> EnvG -> Parser Module FileC
parseFileC eargs eg m = do ldecl <- parseAllDeclC eg (declarationsMod m)
return $ FileC includes ldecl
where includes = map GloIncC (gloIncOpt eargs)
++ map LocIncC (locIncOpt eargs)
parseFileH :: EnvArgs -> EnvG -> Parser Module (EnvG, FileH)
parseFileH eargs eg m = do (env, ldecl) <- parseAllDeclH eg (declarationsMod m)
return (env, FileC includes ldecl)
where includes = map GloIncC (gloIncOpt eargs) ++ map LocIncC (locIncOpt eargs)
parseModuleC :: EnvArgs -> EnvG -> Parser Module (EnvG, ModuleC)
parseModuleC eargs env m = do (envH, fileH) <- parseFileH eargs env m
fileC <- parseFileC eargs envH m
return (envH, ModuleC nm fileH fileC)
where nm = nameMod m
parseMacroInc :: FileName -> (MacroIncBegin, MacroIncEnd)
parseMacroInc name = ( "#ifndef " ++ define ++ "\n"
++ "#define " ++ define ++ "\n"
, "#endif\n")
where define = "__" ++ map ((\ x -> if x == '.' then '_' else x) . toUpper) name ++ "_H__"
parseImportC :: EnvG -> Parser Module (EnvG, DeclC)
parseImportC env m = do (nenv, declH's) <- parseAllDeclH env (declarationsMod m)
let comDeclH's = concatMap ((++"\n") . showDeclC) declH's
header = "************* Expected symbols from " ++ nameMod m ++ " *************\n"
footer = replicate (length header) '*'
return (nenv, CommDecl $ header ++ comDeclH's ++ footer)
parseAllImportC :: EnvG -> Parser [Module] (EnvG, [DeclC])
parseAllImportC env m's = case m's of
[] -> return (env, [])
m:ms -> do (e1, ds1) <- parseImportC env m
(en, dsn) <- parseAllImportC env ms
return (mergeEnvG e1 en, ds1 : dsn)
-------------- Show -------------------------------
type Indent = Int
showCommentaryC :: CommentaryC -> String
showCommentaryC commentary = "/*\n" ++ commentary ++ "\n*/"
showIndent :: Indent -> String
showIndent indent = if indent < 0 then "" else replicate indent '\t'
showIncludeC :: IncludeC -> String
showIncludeC inc = case inc of
(GloIncC name) -> "#include <" ++ name ++ ">" ++ "\n"
(LocIncC name) -> "#include \"" ++ name ++ "\"" ++ "\n"
showVarC :: Indent -> VarC -> String
showVarC ind (n, _) = showIndent ind ++ n
showValC :: Indent -> ValC -> String
showValC ind (n, _) = showIndent ind ++ n
showExprC :: Indent -> ExprC -> String
showExprC ind (ValC l) = showValC ind l
showExprC ind (VarC v) = showVarC ind v
showExprC ind (ApplyFunC nameFun args) = showIndent ind ++ nameFun ++ "(" ++ intercalate ", " (map (showExprC 0) args) ++ ")"
showExprC ind (BinOp el symb er) = showIndent ind ++ "(" ++ showExprC 0 el ++ " " ++ symb ++ " " ++ showExprC 0 er ++ ")"
showTypeC :: NameC -> TypeC -> String
showTypeC _ (TypeC typeC) = typeC
showTypeC n (TypeCFun typeC@(t:ts)) = ret ++ idt ++ args
where ret = showTypeC "" $ last typeC
idt = "(*" ++ n ++ ")"
args = "(" ++ showTypeC "" t ++ foldr (\x y -> ", " ++ showTypeC "" x ++ y) "" (init' ts) ++ ")"
init' l = if null l then [] else init l
showTypeC _ _ = error "error, showTypeC"
showPrototypeC :: PrototypeC -> String
showPrototypeC (PrototypeC name ret args) =
showTypeC name ret ++ " " ++ name ++ "(" ++ intercalate ", " (map (showDeclVarC eDECLVARINPROTOTYPE) args) ++ ")"
showOnlyPrototypeC :: PrototypeC -> String
showOnlyPrototypeC pro = "extern " ++ showPrototypeC pro ++ ";"
eDECLVARINPROTOTYPE :: Int
eDECLVARINPROTOTYPE = -1
showDeclVarC :: Indent -> DeclVarC -> String
showDeclVarC ind decl = case decl of
(VarEmptyDecl (n, t)) -> let isFun = isTypeCFun t in begin ++ extern ++ identif isFun t n ++ end
(VarDecl (n, t) expr) -> let isFun = isTypeCFun t in begin ++ constI isFun ++ showTypeC n t ++ " " ++ n ++ " = " ++ showExprC 0 expr ++ end
where begin = showIndent ind
end = if ind == 0 then ";" else ""
extern = if ind == 0 then "extern " else ""
constI isFun' = if isFun' then "" else "const "
identif isFun' t' n' = if isFun' then showTypeC n' t' else constI isFun' ++ showTypeC "" t' ++ " " ++ n'
showConditionnalC :: Indent -> ConditionalStructC -> String
showConditionnalC ind (IfThenElseC cond ifB elseB) = showIndent ind ++
"if (" ++ showExprC 0 cond ++ ") {\n" ++
concatMap (showInstructionC (ind + 1)) ifB ++ showIndent ind ++
"} else {\n" ++
concatMap (showInstructionC (ind + 1)) elseB ++ showIndent ind ++
"}"
showControlStructC :: Indent -> ControlStructC -> String
showControlStructC ind (Cond struct) = showConditionnalC ind struct
showControlStructC _ (Iter _) = undefined
showFunctionC :: FunctionC -> String
showFunctionC (FunctionC proto body) =
showPrototypeC proto ++
"\n{\n" ++
concatMap (showInstructionC 1) body ++
"}"
debugRender :: Int
debugRender = 120
showDeclC :: DeclC -> String
showDeclC decl = case decl of
VarCDecl var -> showDeclVarC 0 var
FunDecl fun -> showFunctionC fun
ProtoDecl proto -> showOnlyPrototypeC proto
CommDecl comm -> showCommentaryC comm
_ -> error $ "showDeclC undefined" ++ take debugRender (show decl)
showInstructionC :: Indent -> InstructionC -> String
showInstructionC ind instr =
case instr of
(CSC csc) -> showControlStructC ind csc ++ "\n"
(ExprC expr) -> showExprC ind expr ++ ";\n"
(DeclVarC declVar) -> showDeclVarC ind declVar ++ ";\n"
(ReturnC expr) -> showIndent ind ++ "return " ++ showExprC 0 expr ++ ";\n"
showFileC :: FileC -> String
showFileC (FileC incl body) = concatMap showIncludeC incl ++ "\n" ++
concatMap (\x -> showDeclC x ++ "\n\n") body
showFileH :: FileName -> FileH -> String
showFileH name (FileC incl body) =
let (begin, end) = parseMacroInc name
includes = concatMap showIncludeC incl
in
begin ++ "\n" ++
includes ++ (if null includes then "" else "\n") ++
concatMap (\d -> showDeclC d ++ "\n") body ++ "\n" ++
end ++ "\n"
type ShowFileC = String
type ShowFileH = String
showModuleC :: ModuleC -> (ShowFileH, ShowFileC)
showModuleC (ModuleC name fileH fileC) =
( showFileH name fileH
, showFileC fileC
)
------------------- Main Module ----------------------
type ContentFile = String
type ImportFile = ContentFile
extractor :: EnvArgs -> [ImportFile] -> ContentFile -> MyEither (ModuleUsed, (ShowFileH, ShowFileC))
extractor eargs impFile's contFile = do astImpFile's <- mapM decodeModule impFile's
astCoqFile <- decodeModule contFile
(envImp's, declComm's) <- parseAllImportC env astImpFile's
(_, m) <- parseModuleC eargs (mergeEnvG env envImp's) astCoqFile
let moduleC = addDeclCToModCFileH m declComm's
return $ (nameMod astCoqFile, showModuleC moduleC)
where decodeModule content = MyEith $ (eitherDecode (BS.pack content) :: Either String Module)
env = envG envUser
main :: IO ()
main = do namePrg <- getProgName
eargs <- OA.execParser (opts namePrg)
fileImp's <- mapM readFile $ importOpt eargs
fileCoq <- readFile $ inputOpt eargs
let (nm, (contentFileH, contentFileC)) = eith . myEither $ extractor eargs fileImp's fileCoq
output = fromMaybe (nm ++ ".c") (outputOpt eargs)
writeFile output contentFileC
case outputHOpt eargs of
Just fileH -> writeFile fileH contentFileH
Nothing -> return ()
where eith = either error id
opts nm = OA.info (OA.helper <*> envArgs)
( OA.fullDesc
<> OA.progDesc ( "Compile Coq source code written in a specific monadic style "
++ "(and extracted to its JSON representation by the standard "
++ "Coq extracting facility) into the corresponding C code" )
<> OA.header (nm ++ " - a simple compiler from Coq monadic code into C")
)
digger.cabal 0 → 100644
+ 54
− 0
View file @ d24f5e53
name: digger
version: 0.2.0.0
synopsis: convert "C-style" Coq code into C code or an
intermediate representation in Coq
description: Convert Coq code written in a "C-style"
(imperative style based on a monad, with full
application of functions) into the corresponding
C code or to an intermediate representation
(deep) output as Coq source code.
Start from the Coq code extracted as JSON by the
internal extraction facility.
license: OtherLicense
license-file: LICENSE
author: Samuel Hym, Veïs Oudjail
maintainer: samuel.hym@univ-lille1.fr
copyright: 2016-2017 Université Lille 1, Veïs Oudjail
category: Language
build-type: Simple
extra-source-files: Readme.md
cabal-version: >=1.10
library
hs-source-dirs: src
exposed-modules: Language.Coq.ExtractedAST,
Language.Coq.Deep
build-depends: base >=4.9 && <4.10,
aeson >=0.11 && <1.1,
containers >= 0.5.7 && <0.6,
bytestring >=0.10 && <0.11,
data-default >= 0.7 && < 0.8,
text >= 1.2 && < 1.3,
wl-pprint-text >= 1.1 && < 1.2,
language-c >= 0.5 && < 0.6,
pretty >= 1.1 && < 1.2
default-language: Haskell2010
executable digger
main-is: digger.hs
hs-source-dirs: app
other-modules: Paths_digger
build-depends: base >=4.9 && <4.10,
aeson >=0.11 && <1.1,
containers >= 0.5.7 && <0.6,
bytestring >=0.10 && <0.11,
data-default >= 0.7 && < 0.8,
optparse-applicative >=0.12 && <0.14,
text >= 1.2 && < 1.3,
wl-pprint-text >= 1.1 && < 1.2,
pretty >= 1.1 && < 1.2,
language-c >= 0.5 && < 0.6,
digger
default-language: Haskell2010
src/Language/Coq/Deep.hs 0 → 100644
+ 766
− 0
View file @ d24f5e53
-- This software is governed by the CeCILL license under French law and
-- abiding by the rules of distribution of free software. You can use,
-- modify and/ or redistribute the software under the terms of the CeCILL
-- license as circulated by CEA, CNRS and INRIA at the following URL
-- "http://www.cecill.info".
-- As a counterpart to the access to the source code and rights to copy,
-- modify and redistribute granted by the license, users are provided only
-- with a limited warranty and the software's author, the holder of the
-- economic rights, and the successive licensors have only limited
-- liability.
-- In this respect, the user's attention is drawn to the risks associated
-- with loading, using, modifying and/or developing or reproducing the
-- software by the user in light of its specific status of free software,
-- that may mean that it is complicated to manipulate, and that also
-- therefore means that it is reserved for developers and experienced
-- professionals having in-depth computer knowledge. Users are therefore
-- encouraged to load and test the software's suitability as regards their
-- requirements in conditions enabling the security of their systems and/or
-- data to be ensured and, more generally, to use and operate it in the
-- same conditions as regards security.
-- The fact that you are presently reading this means that you have had
-- knowledge of the CeCILL license and that you accept its terms.
{-# LANGUAGE OverloadedStrings #-}
module Language.Coq.Deep (
-- * Deep intermediate representation
-- $deep
Id
, VId
, FId
, Const
, VTyp
, ValTC
, Fun (..)
, Exp (..)
, DeepModule (..)
-- * Parameters for the conversions
, ConversionParams (..)
-- * Conversion from Coq.ExtractedAST syntax to Deep
-- $coq2deep
, SymbolTable
, extractSymbolTable
, fromCoq
-- * Pretty-print a Deep module into Coq syntax
-- $deep2coq
, prettyModule
-- * Conversion from Deep intermediate representation to C
-- $deep2c
, toCSource
, toCHeader
) where
import Control.Arrow (second, (&&&))
import Data.Default
import Data.Either (partitionEithers)
import qualified Data.Map as Map
import Data.Maybe (catMaybes, fromJust, fromMaybe,
isJust, maybeToList)
import qualified Data.Set as Set
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as Text
import Language.C hiding (Name)
import Language.C.Data.Ident (Ident (..))
import Text.PrettyPrint.Leijen.Text (Doc, dquotes, empty, enclose,
encloseSep, hang, hcat, lbracket,
line, lparen, nest, parens,
rbracket, rparen, semi, sep,
space, text, tupled, vcat, vsep,
(<+>), (</>), (<>))
import qualified Text.PrettyPrint.Leijen.Text as PP
import Language.Coq.ExtractedAST
-- $deep
-- Define the Deep intermediate language.
-- This intermediate language only captures the part of the Gallina
-- language that can be converted into C because it is structured just
-- like C code (using a monad to represent sequence).
-- | Identifiers
type Id = String
-- | Variable identifiers
type VId = Id
-- | Function identifiers
type FId = Id
-- | Constants
type Const = String
-- | Types for base values (i.e. not functions)
-- As far as we are concerned, these will be only manipulated as
-- strings in the converter
type VTyp = String
-- | Typing contexts for values
-- In particular, a typing context describes the types of the argument
-- of a function
type ValTC = [(VId, VTyp)]
-- | Actual term (content) of a function
--
-- Built with:
--
-- * the name of the function itself (it will be bound in the body for
-- the recursive case)
-- * a list of functions it can call (and their recursive bounds,
-- given by their names, when applicable)
-- * a list of arguments (and their types)
-- * a return type
--
-- and, if the function is recursive:
--
-- * the body of the function on the base case
-- * the body of the function on the recursive case
--
-- otherwise, the body of the function.
--
-- Compared with Deep syntax, this does not give the bound of
-- recursive functions since it will be defined only in calling
-- functions
--
-- TODO: Should 'calls' be replaced with something containing also the
-- global variables?
data Fun = FunRec { self :: FId
, calls :: [(FId, Maybe RecursiveBound)]
, args :: ValTC
, resTyp :: VTyp
, bodyO :: Exp
, bodyS :: Exp }
| Fun { self :: FId
, calls :: [(FId, Maybe RecursiveBound)]
, args :: ValTC
, resTyp :: VTyp
, body :: Exp }
deriving (Show,Eq)
-- | Syntax of expressions
-- Bind and Return are the standard monadic operators
-- BindN is Bind ignoring the value produced by the first expression
-- Call applies (fully) a function to its arguments
-- IfThenElse, Var and Const are surpriseless
data Exp = Bind VId (Maybe VTyp) Exp Exp
| BindN Exp Exp
| Return Exp
| Call FId [Exp]
| IfThenElse Exp Exp Exp
| Var VId -- ^ TODO: Should this be called differently?
| Const VId -- ^ TODO: Should this be specialised to Bool?
deriving (Show,Eq)
-- | A full module in the Deep world
-- Its symbol table and recursive-bounds map contain also information
-- about its dependencies, not only about the module itself
data DeepModule = DeepModule { nameDeepMod :: Name
, symbolTableDeepMod :: SymbolTable
, recursiveBoundsDeepMod :: RecursiveBoundMap
, functionsDeepMod :: [Either ErrorMsg (Name,Fun)]
}
-- | Parameters for the conversion
--
-- Provide various parameters:
--
-- * the constants to recognize in the Coq source (in particular what
-- is the name of the support monad used to represent C sequence)
-- * the prefixes to use when outputting Deep intermediate language in
-- Gallina (so that source definition "func" becomes "prefix_func")
-- * a few parameters to translate Deep into C: how the recursive
-- bound should be named in C code and which Coq functions should be
-- mapped to native C operators
data ConversionParams = CP
{ monad :: Name -- ^ Name (type) of the support monad
, bind :: Name -- ^ Bind of the support monad
, ret :: Name -- ^ Return of the support monad
, unit :: Name -- ^ How Coq’s unit (type) is extracted
, tt :: Name -- ^ How Coq’s tt (value of type unit) is extracted
, true :: Name -- ^ How Coq’s true is extracted
, false :: Name -- ^ How Coq’s false is extracted
, nats :: CoqNat -- ^ How Coq’s nat are extracted
, consts :: [Name] -- ^ Constructors that should be preserved
, ignores :: [Name] -- ^ Declarations that should be ignored in Coq source
-- (for instance because they cannot be translated)
, prefixConst :: Text -- ^ Prefix of Deep versions of constructors
, prefixFun :: Text -- ^ Prefix added to function names in their Deep versions
, prefixFTyp :: Text -- ^ Prefix for function types definition
, prefixVTyp :: Text -- ^ Prefix for value types
, recBoundName :: Name -- ^ Name of the recursive-bound variable in generated C
, unaryOps :: Map.Map FId CUnaryOp -- ^ Map from Coq functions to C unary operators
, binaryOps :: Map.Map FId CBinaryOp -- ^ Map from Coq functions to C binary operators
}
deriving (Show,Eq)
instance Default ConversionParams where
def = CP { monad = "Monad"
, bind = "bind"
, ret = "ret"
, unit = "unit"
, tt = "tt"
, true = "true"
, false = "false"
, nats = def
, consts = ["true","false","tt"]
, ignores = []
, prefixConst = "deepConst_"
, prefixFun = "deepFun_"
, prefixFTyp = "deepFTyp_"
, prefixVTyp = "deepVTyp_"
, recBoundName = "rec_bound"
, unaryOps = Map.fromList [("negb",CNegOp)]
, binaryOps = Map.fromList [("andb",CLndOp)
,("orb", CLorOp)]
}
-- $coq2deep
-- Define the conversion from the extracted Coq AST into the Deep
-- intermediate representation.
-- | Symbol table
--
-- Maps to every known symbol:
--
-- * the type of the value it returns if it is a function,
-- * its type otherwise.
--
-- Warning: this assumes that the VId and FId types are indeed synonyms
type SymbolTable = Map.Map Id VTyp
-- | Extract the "symbol type"
--
-- * if it is a function, the type of the value it returns
-- * if it is a global variable, its type
extractSymbolType :: ConversionParams -> Type -> Either ErrorMsg VTyp
extractSymbolType _ (Glob ty []) = pure ty
extractSymbolType cp typ = go typ
where go (Arrow _ ty) = go ty
go (Glob m [Glob ty []]) | m == monad cp = pure ty
go ty = Left $ impossibleType ty
impossibleType ty = "Impossible to extract symbol type of: " ++ show ty
-- | Extract the symbol table from a list of declarations
extractSymbolTable :: ConversionParams -> [Decl] -> SymbolTable
extractSymbolTable cp = Map.fromList . go . concatMap open
where open :: Decl -> [(Id, Type)]
open t@Term{} = [(nameTerm t, typeTerm t)]
open (Fixgroup fis) = map (nameItem &&& typeItem) fis
go :: [(Id, Type)] -> [(Id, VTyp)]
go xs = [ (n,t) | (n, Right t) <- map (second (extractSymbolType cp)) xs]
-- | Infer the result type of an expression
-- Use a very simple strategy, since the set of expressions is really
-- limited
-- Return the modified expression (in case some included type
-- annotations were modified) and the result type, when possible
inferExpTypes :: SymbolTable -> Exp -> (Maybe VTyp, Exp)
inferExpTypes st (Bind v _ e1 e2) = let (ty1, e1') = inferExpTypes st e1
st' = maybe st (\t -> Map.insert v t st) ty1
in Bind v ty1 e1' <$> inferExpTypes st' e2
inferExpTypes st (BindN e1 e2) = let (_, e1') = inferExpTypes st e1
in BindN e1' <$> inferExpTypes st e2
inferExpTypes st (Return e) = Return <$> inferExpTypes st e
inferExpTypes st (Call f es) = (Map.lookup f st, Call f (map (snd . inferExpTypes st) es))
inferExpTypes st (IfThenElse i t e) = let (_, i') = inferExpTypes st i
(tyt, t') = inferExpTypes st t
(tye, e') = inferExpTypes st e
ty = if isJust tyt then tyt else tye
in (ty, IfThenElse i' t' e')
inferExpTypes st e@(Var v) = (Map.lookup v st, e)
inferExpTypes st e@(Const v) = (Map.lookup v st, e)
inferTypes :: SymbolTable -> Fun -> Fun
inferTypes st fun@Fun{} = fun{body = snd $ inferExpTypes st (body fun)}
inferTypes st fun@FunRec{} = fun{bodyO = snd $ inferExpTypes st (bodyO fun)
,bodyS = snd $ inferExpTypes st (bodyS fun)}
-- | Convert the type of a function
-- The types that can be converted are of the form
-- x -> y -> z -> Monad t
-- where x, y, z and t are global names, not variables.
-- This function only converts the original type, the actual argument
-- names are required to build a FTyp
convertFunType :: ConversionParams -> Type -> Either ErrorMsg ([VTyp], VTyp)
convertFunType cp = go
where go (Arrow (Glob n []) ty2) = go ty2 >>= \(tys, ty) -> pure (n:tys, ty)
go (Glob m' [Glob t []]) | m == m' = pure ([], t)
go ty = Left $ impossibleType ty
m = monad cp
impossibleType ty = "Impossible to convert type: " ++ show ty
-- | Convert the body of a function
-- Return either the resulting Deep expression or some (Coq AST)
-- sub-expression that could not be converted
--
-- Handle the following possible cases:
-- - monadic bind
-- - monadic bind where the second action ignores the value generated
-- by the first
-- - monadic return
-- - application of a function to some arguments (since we are not
-- compiling a functional language, that function can only be a
-- globally existing function)
-- - using a global or local name
-- - if then else, which is represented in Coq by a pattern-matching
-- on boolean, so we unfold them to recover the two branches and
-- check the two constructors
-- - constructors for inline booleans
convertFunBody :: ConversionParams -> Expr -> Either ErrorMsg Exp
convertFunBody cp = go True
where -- | Translate an expression
-- Take as first argument whether the expression is monadic
-- or not
go :: Bool -> Expr -> Either ErrorMsg Exp
go True (Apply (Global b) [e1, Lambda ["_"] e2]) | b == bind cp = BindN <$> go True e1 <*> go True e2
go True (Apply (Global b) [e1, Lambda [v] e2]) | b == bind cp = Bind v Nothing <$> go True e1 <*> go True e2
go True (Apply (Global r) [e]) | r == ret cp = Return <$> go False e
go _ (Apply (Global f) as) = Call f <$> traverse (go False) as
go True (Global v) = Right (Call v [])
go False (Global v) = Right (Var v)
go False (Rel v) = Right (Var v)
go True (Case cond [C (ConstructorP c1 []) e1
,C (ConstructorP c2 []) e2]) | checkIFT = IfThenElse <$> go False cond
<*> go True thenE
<*> go True elseE
where checkIFT = c1 == true cp && c2 == false cp
|| c1 == false cp && c2 == true cp
(thenE,elseE) = if c1 == true cp then (e1,e2) else (e2,e1)
go False (ConstructorE c []) | c `elem` consts cp = Right (Const c)
go monadic e = Left $ impossibleExpr monadic e
impossibleExpr m ex = "Impossible to convert expression \"" ++ show ex ++ "\" " ++
"in " ++ prefix m ++ "monadic context"
prefix True = ""
prefix False = "non-"
-- | Complete the list of calls in a function declaration
-- Add the calls to all the functions (including the non-recursive
-- ones) to the list of calls
completeCalls :: Fun -> Fun
completeCalls fun = fun{calls = calls fun ++ map (\f -> (f, Nothing)) newUnique}
where extract (Bind _ _ e1 e2) = concatMap extract [e1,e2]
extract (BindN e1 e2) = concatMap extract [e1,e2]
extract (Return e) = extract e
extract (Call f as) = f : concatMap extract as
extract (IfThenElse i t e) = concatMap extract [i,t,e]
extract _ = []
allCalled Fun{} = extract (body fun)
allCalled FunRec{} = concatMap extract [bodyO fun, bodyS fun]
allCalled' = Set.fromList . allCalled
already = Set.fromList (self fun : map fst (calls fun))
newCalled = Set.filter (`Set.notMember` already) (allCalled' fun)
newUnique = Set.toList newCalled
-- | Convert a declaration (a function or a fixgroup)
--
-- FIXME? here there are some cases of inconsistency between the
-- RecursiveBoundMap and the actual number of arguments encountered
-- that are _not_ detected (and would result in exceptions)
convertDecl :: ConversionParams -> RecursiveBoundMap -> SymbolTable -> Decl -> Either ErrorMsg [(Name, Fun)]
convertDecl cp recs syms = go
where -- | Base case of transformation of one function
base nam typ ex = do (tyArgs, tyRes) <- convertFunType cp typ
(recCalls, ex') <- extractRecCalls (nats cp) nam recs ex
(args', bodyO', bodyS') <- unLambda nam ex'
bodyO'' <- convertFunBody cp bodyO'
bodyS'' <- maybe (Right Nothing) (fmap Just . convertFunBody cp) bodyS'
let args'' = zip args' tyArgs
args''' = case Map.lookup nam recs of
Just pos -> case splitAt pos args'' of
(args1, _:args2) -> args1 ++ args2
Nothing -> args''
recCalls' = map (second Just) recCalls
whole = case bodyS'' of
Just bodyS''' -> FunRec nam recCalls' args''' tyRes bodyO'' bodyS'''
Nothing -> Fun nam recCalls' args''' tyRes bodyO''
pure (nam, inferTypes syms $ completeCalls whole)
ignores' = Set.fromList (ignores cp)
base' nam typ ex | Set.member nam ignores' = Right []
| otherwise = case base nam typ ex of
Left err -> Left $ "Error in " ++ nam ++ ": " ++ err
Right r -> Right [r]
unLambda _
(Lambda args'
(Case (Rel _) [C (ConstructorP o []) bodyO'
,C (ConstructorP s [_]) bodyS']))
| o == natO (nats cp)
&& s == natS (nats cp) = pure (args', bodyO', Just bodyS')
unLambda _ (Lambda args' body') = pure (args', body', Nothing)
unLambda nam e = Left $ "Lambda expected in " ++ nam
++ " in expression: " ++ show e
go (Term nam typ ex) = base' nam typ ex
go (Fixgroup funs) = concat <$> traverse (\(FixItem nam typ ex) -> base' nam typ ex) funs
-- | Convert a "ExtractedAST" Coq 'Module' to Deep language
-- Takes as arguments the 'RecursiveBoundMap' and 'SymbolTable'
-- corresponding to the modules the converted one requires
fromCoq :: ConversionParams -> RecursiveBoundMap -> SymbolTable -> Module -> DeepModule
fromCoq cp recs syms modul = DeepModule{ nameDeepMod = nameMod modul
, symbolTableDeepMod = syms'
, recursiveBoundsDeepMod = recs'
, functionsDeepMod = funs
}
where recs' = Map.union recs $ detectBounds (nats cp) modul
syms' = Map.union syms $ extractSymbolTable cp decls
decls = declarationsMod modul
funs = concatMap (sequence . convertDecl cp recs' syms') decls
-- $deep2coq
-- Define the conversion of the Deep intermediate language into an
-- explicit representation of Deep in Coq.
-- | Pretty-print Id
prettyId :: Id -> Doc
prettyId = text . Text.pack
quoteId :: Id -> Doc
quoteId = dquotes . prettyId
-- | Pretty-print a recursive bound constant (Coq nat number)
prettyBoundConst :: RecursiveBoundConst -> Doc
prettyBoundConst = text . Text.pack . show
-- | Pretty-print a recursive bound
prettyBound :: RecursiveBound -> Doc
prettyBound (b, vs) = go vs''
where vs' = map prettyId vs
vs'' | b == 0 = vs'
| otherwise = vs' ++ [prettyBoundConst b]
go [] = text "0"
go [x] = x
go xs = encloseSep lparen rparen (text " + ") xs
-- | Pretty-print a constructor
prettyConst :: ConversionParams -> Id -> Doc
prettyConst cp x = text (prefixConst cp) <> prettyId x
-- | Pretty-print a VTyp
prettyVTyp :: ConversionParams -> VTyp -> Doc
prettyVTyp cp typ = text (prefixVTyp cp) <> prettyId typ
-- | Pretty-print a Coq list
list :: [Doc] -> Doc
list = encloseSep lbracket rbracket semi
-- | Pretty-print a sub-expression
sub :: ConversionParams -> Exp -> Doc
sub cp = nest 2 . parens . prettyExp cp
-- | Pretty-print an expression
prettyExp :: ConversionParams -> Exp -> Doc
prettyExp cp (Bind v _ e1 e2) = nest 2 ( sep [ text "BindS" </> quoteId v
, sub cp e1 ] )
PP.<$> sub cp e2
prettyExp cp (BindN e1 e2) = nest 2 ( sep [ text "BindN"
, sub cp e1 ] )
PP.<$> sub cp e2
-- | Special cases of return
prettyExp _ (Return (Var x)) = text "Return RR" </> parens (text "Var" </> quoteId x)
prettyExp cp (Return (Const c)) = text "Return RR" </> prettyConst cp c
-- | Strangest of all special cases: if it is not a Var or a Const, we
-- handle it as if it were a boolean expression, to bypass current
-- limitations in Return
prettyExp cp (Return x) = prettyExp cp (IfThenElse x (Return (Const (true cp)))
(Return (Const (false cp))))
-- The following should be the actual normal case for return
-- prettyExp cp (Return x) = text "Return RR" </> sub cp x
prettyExp cp (Call f as) = sep [ text "Apply"
, parens (text "FVar" </> quoteId f)
, parens (text "PS" </> list (map (prettyExp cp) as)) ]
prettyExp cp (IfThenElse e1 e2 e3) = sep ["IfThenElse", sub cp e1, sub cp e2, sub cp e3]
prettyExp _ (Var x) = text "Return LL" </> parens (text "Var" </> quoteId x)
prettyExp cp (Const c) = text "Return LL" </> prettyConst cp c
-- | Pretty-print an argument list
prettyArgs :: ConversionParams -> ValTC -> Doc
prettyArgs cp = list . map prettyArg
where prettyArg (var, typ) = tupled [quoteId var, prettyVTyp cp typ]
-- | Pretty-print a Fun
prettyFun :: ConversionParams -> Fun -> Maybe Doc -> Doc
prettyFun cp fun bnd =
nest 2 $ vsep [ sep [ text "FC"
, list (map prettyCalled (calls fun))
, prettyArgs cp (args fun) ]
, prettyBody (bodyO' fun)
, prettyBody (bodyS' fun)
, quoteId (self fun) <+> fromMaybe empty bnd ]
where prettyCalled (fun', bnd') = tupled [ quoteId fun'
, hcat [ text (prefixFun cp)
, prettyId fun'
, maybe empty (const space) bnd'
, maybe empty prettyBound bnd' ] ]
prettyBody = hang 2 . enclose (text "( ") (text " )") . prettyExp cp
bodyO' (FunRec _ _ _ _ b _) = b
bodyO' (Fun _ _ _ _ b) = b
bodyS' (FunRec _ _ _ _ _ b) = b
bodyS' (Fun n _ as _ _) = Call n (map (Var . fst) as)
-- | Pretty-print a FTyp
prettyFTyp :: ConversionParams -> Fun -> Doc
prettyFTyp cp fun = nest 2 $ sep [ text "FT"
, prettyArgs cp (args fun)
, prettyVTyp cp (resTyp fun) ]
-- | Pretty-print a definition
prettyDef :: ConversionParams -> RecursiveBoundMap -> (Name, Fun) -> Doc
prettyDef cp recs (nam, fun) = hang 2 deffun PP.<$> hang 2 deftyp
where isRec = isJust $ Map.lookup nam recs
bnd | isRec = Nothing
| otherwise = Just $ prettyId $ natO $ nats cp
typ | isRec = text "nat -> Fun"
| otherwise = text "Fun"
deffun = text "Definition" </> text (prefixFun cp) <>
prettyId nam </> text ":" </> typ </> text ":=" <> line <>
prettyFun cp fun bnd <> text "." <> line
deftyp = text "Definition" </> text (prefixFTyp cp) <>
prettyId nam </> text ": FTyp" </> text ":=" <> line <>
prettyFTyp cp fun <> text "." <> line
-- | Pretty-print a 'Doc' as a Coq comment
comment :: Doc -> Doc
comment = hang 3 . enclose (text "(* ") (text " *)")
-- | Pretty-print an error
-- When a function fails to convert, pretty-print the error message
prettyErr :: ErrorMsg -> Doc
prettyErr err = comment (text (Text.pack err)) <> line
-- | Pretty-print a definition whose convertion could have failed
prettyDefErr :: ConversionParams -> RecursiveBoundMap -> Either ErrorMsg (Name, Fun) -> Doc
prettyDefErr cp recs = either prettyErr (prettyDef cp recs)
-- | Pretty-print a module
prettyModule :: ConversionParams -> DeepModule -> Doc
prettyModule cp modul = vcat $ map (prettyDefErr cp recs) funs
where recs = recursiveBoundsDeepMod modul
funs = functionsDeepMod modul
-- $deep2c
-- Define the conversion from the Deep intermediate representation
-- into C code, using the "Language.C" library to represent the result
-- of that conversion.
-- | Define an identifier without any node information
-- To build an AST, the information would not be much use
ident :: String -> Ident
ident n = let Ident n' i _ = internalIdent n
in Ident n' i undefNode
-- | Return an unsigned int constant
unsignedConst :: Integer -> CExpr
unsignedConst n = CConst (CIntConst (CInteger n DecRepr flagUnsigned) undefNode)
where flagUnsigned = setFlag FlagUnsigned noFlags
-- | Convert a Deep type into a C type declaration
cVTyp :: ConversionParams -> VTyp -> CDeclSpec
cVTyp cp = cMaybeVTyp cp . Just
-- | Convert a possibly-absent Deep type into a C type declaration
-- When absent, generate an "auto" type instead of a type
cMaybeVTyp :: ConversionParams -> Maybe VTyp -> CDeclSpec
cMaybeVTyp cp (Just typ) | typ == unit cp = CTypeSpec $ CVoidType undefNode
| otherwise = CTypeSpec $ CTypeDef (ident typ) undefNode
cMaybeVTyp _ Nothing = CStorageSpec $ CAuto undefNode
-- | Convert function arguments into C
cFunArgs :: ConversionParams -> Fun -> Either [Ident] ([CDecl],Bool)
cFunArgs cp fun = Right (argsDefs, False)
where argDef (i,t) = CDecl [cVTyp cp t]
[(Just (CDeclr (Just (ident i)) [] Nothing [] undefNode),Nothing,Nothing)]
undefNode
argsDefs = let defs = map argDef (args fun)
in case fun of
Fun{} -> defs
FunRec{} -> boundarg : defs
boundarg = CDecl [CTypeSpec (CUnsigType undefNode),CTypeSpec (CIntType undefNode)]
[(Just (CDeclr (Just (ident (recBoundName cp))) [] Nothing [] undefNode)
,Nothing,Nothing)]
undefNode
-- | Convert a function prototype into C
toCPrototype :: ConversionParams -> Fun -> CExtDecl
toCPrototype cp fun = CDeclExt (CDecl [CStorageSpec (CExtern undefNode)
,cVTyp cp (resTyp fun)]
[(Just (CDeclr (Just (ident (self fun)))
[CFunDeclr (cFunArgs cp fun) [] undefNode]
Nothing [] undefNode)
,Nothing,Nothing)]
undefNode)
-- | Convert a Deep expression into a C expression
-- Take as arguments the conversion parameters and the enclosing
-- function
-- It might result in no expression at all, when the expression is Coq
-- unit (since no expression should be of type void)
--
-- TODO: Should we accept IfThenElse in expressions (we might turn
-- them into ternary expressions)?
cExpression :: ConversionParams -> Fun -> Exp -> Either ErrorMsg (Maybe CExpr)
cExpression cp fun (Return e) = cExpression cp fun e
cExpression cp _ (Const v) | v == tt cp = pure Nothing
| otherwise = pure $ Just $ CVar (ident v) undefNode
cExpression _ _ (Var v) = pure $ Just $ CVar (ident v) undefNode
-- | Call of a unary operator
cExpression cp fun e@(Call f [a]) | Map.member f (unaryOps cp) = do
a' <- cExpression cp fun a
case a' of
Nothing -> Left $ "Impossible to convert unary op " ++ show e
Just a'' -> pure $ Just $ CUnary (fromJust $ Map.lookup f $ unaryOps cp) a'' undefNode
-- | Call of a binary operator
cExpression cp fun e@(Call f as@[_,_]) | Map.member f (binaryOps cp) = do
as' <- traverse (cExpression cp fun) as
case as' of
[Just a1, Just a2] -> pure $ Just $ CBinary (fromJust $ Map.lookup f $ binaryOps cp) a1 a2 undefNode
_ -> Left $ "Impossible to convert binary op " ++ show e
-- | Call, general case
-- This must handle in particular whether we are performing a
-- recursive call, or a call to another recursive function
cExpression cp fun (Call f as) = do as' <- traverse (cExpression cp fun) as
let as'' = catMaybes (recBound:as')
pure $ Just $ CCall (CVar (ident f) undefNode) as'' undefNode
where recBound | f == self fun = -- recBoundName - 1
Just $ CBinary CSubOp
(CVar (ident (recBoundName cp)) undefNode)
(unsignedConst 1)
undefNode
| otherwise = case lookup f (calls fun) of
Just (Just v) -> Just $ boundExp v
_ -> Nothing
boundExp (c, vs) = let vs' = map (flip CVar undefNode . ident) vs
vs'' = if c == 0 then vs' else vs' ++ [unsignedConst c]
in if null vs''
then unsignedConst 0
else foldr1 (\e1 e2 -> CBinary CAddOp e1 e2 undefNode) vs''
cExpression _ _ e = Left $ "Impossible to convert expression \"" ++ show e ++ "\" to C"
-- | Convert an expression into statements
-- Take as arguments the conversion parameters, the enclosing
-- function and whether the result should be returned or not
-- It will result in 0, 1 or 2 statements
-- It will result in two statements when it should return
-- and the expression is of type void
cExprStmt :: ConversionParams -> Fun -> Bool -> Exp -> Either ErrorMsg [CStat]
cExprStmt cp fun tailRet e = do e' <- cExpression cp fun e
pure $ case tailRet of
True | resTyp fun == unit cp
&& isJust e' -> [ CExpr e' undefNode
, CReturn Nothing undefNode ]
| otherwise -> [ CReturn e' undefNode ]
_ | isJust e' -> [ CExpr e' undefNode ]
| otherwise -> []
-- | Convert a Deep expression into a block of statements
-- Take as arguments the conversion parameters and the enclosing function
cBlock :: ConversionParams -> Fun -> Exp -> Either ErrorMsg CStat
cBlock cp fun = goBlock True
where goStmt :: Bool -> Exp -> Either ErrorMsg [CStat]
-- | The Return case is ready for the Return-less Deep
-- language
goStmt tailRet (Return e) = goStmt tailRet e
goStmt tailRet (IfThenElse i t e) = do i' <- cExpression cp fun i
case i' of
Just i'' -> do
t' <- goBlock tailRet t
e' <- goBlock tailRet e
pure [CIf i'' t' (Just e') undefNode]
Nothing -> Left $ "Impossible to convert " ++ show i
goStmt tailRet e@(Var _) = cExprStmt cp fun tailRet e
goStmt tailRet e@(Const _) = cExprStmt cp fun tailRet e
goStmt tailRet e@(Call _ _) = cExprStmt cp fun tailRet e
-- | Flatten a sequence of binds into a list of triples
-- ('tailRet', 'VId' if named 'Bind', 'exp')
-- Note that 'tailRet' is always 'False' when 'VId' is not
-- 'Nothing'
flatten :: Bool -> Exp -> [(Bool, Maybe (VId, Maybe VTyp), Exp)]
flatten tailRet (Bind v t e1 e2) = (False, Just (v, t), e1) : flatten tailRet e2
flatten tailRet (BindN e1 e2) = (False, Nothing, e1) : flatten tailRet e2
flatten tailRet e = [(tailRet, Nothing, e)]
goBlock :: Bool -> Exp -> Either ErrorMsg CStat
goBlock tailRet e = block <$> traverse entry (flatten tailRet e)
where block stmts = CCompound [] (concat stmts) undefNode
entry (tailRet', Nothing, e') = map CBlockStmt <$> goStmt tailRet' e'
entry ( _, Just vt, e') = maybeToList . fmap (CBlockDecl . decl vt)
<$> cExpression cp fun e'
decl (v,t) e' = CDecl [cMaybeVTyp cp t]
[(Just (CDeclr (Just (ident v)) [] Nothing [] undefNode)
,Just (CInitExpr e' undefNode)
,Nothing)]
undefNode
-- | Convert a function body into C
cFunBody :: ConversionParams -> Fun -> Either ErrorMsg CStat
cFunBody cp fun@(Fun _ _ _ _ b) = cBlock cp fun b
cFunBody cp fun@(FunRec _ _ _ _ bO bS) = do bO' <- cBlock cp fun bO
bS' <- cBlock cp fun bS
pure $ CCompound []
[CBlockStmt $
CIf (CBinary CEqOp bnd zero undefNode)
bO' (Just bS') undefNode]
undefNode
where zero = unsignedConst 0
bnd = CVar (ident (recBoundName cp)) undefNode
-- | Convert a function definition into C
toCDefinition :: ConversionParams -> Fun -> Either ErrorMsg CFunDef
toCDefinition cp fun = do b <- cFunBody cp fun
pure $ CFunDef [cVTyp cp (resTyp fun)]
(CDeclr (Just (ident (self fun)))
[CFunDeclr (cFunArgs cp fun) [] undefNode]
Nothing [] undefNode)
[] b undefNode
-- | Convert a module from its Deep intermediate representation into C
-- source code
toCSource :: ConversionParams -> DeepModule -> ([ErrorMsg], CTranslUnit)
toCSource cp modul = second buildUnit $ partitionEithers $ map go funs
where funs = functionsDeepMod modul
go :: Either ErrorMsg (Name,Fun) -> Either ErrorMsg CExtDecl
go funErr = do (_,fun) <- funErr
fun' <- toCDefinition cp fun
pure (CFDefExt fun')
buildUnit defs = CTranslUnit defs undefNode
-- | Convert a module from its Deep intermediate representation into a
-- C header file
toCHeader :: ConversionParams -> DeepModule -> ([ErrorMsg], CTranslUnit)
toCHeader cp modul = second (buildUnit . map (toCPrototype cp . snd)) $ partitionEithers funs
where funs = functionsDeepMod modul
buildUnit defs = CTranslUnit defs undefNode
src/Language/Coq/ExtractedAST.hs 0 → 100644
+ 537
− 0
View file @ d24f5e53
-- This software is governed by the CeCILL license under French law and
-- abiding by the rules of distribution of free software. You can use,
-- modify and/ or redistribute the software under the terms of the CeCILL
-- license as circulated by CEA, CNRS and INRIA at the following URL
-- "http://www.cecill.info".
-- As a counterpart to the access to the source code and rights to copy,
-- modify and redistribute granted by the license, users are provided only
-- with a limited warranty and the software's author, the holder of the
-- economic rights, and the successive licensors have only limited
-- liability.
-- In this respect, the user's attention is drawn to the risks associated
-- with loading, using, modifying and/or developing or reproducing the
-- software by the user in light of its specific status of free software,
-- that may mean that it is complicated to manipulate, and that also
-- therefore means that it is reserved for developers and experienced
-- professionals having in-depth computer knowledge. Users are therefore
-- encouraged to load and test the software's suitability as regards their
-- requirements in conditions enabling the security of their systems and/or
-- data to be ensured and, more generally, to use and operate it in the
-- same conditions as regards security.
-- The fact that you are presently reading this means that you have had
-- knowledge of the CeCILL license and that you accept its terms.
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Language.Coq.ExtractedAST where
import Control.Arrow (first)
import Data.Aeson
import Data.Aeson.Types (Parser)
import Data.Default
import Data.List (elemIndex, find, isPrefixOf)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe, isJust, mapMaybe)
import qualified Data.Set as Set
-- | Type (and sub-types) of the elements of the CoqAST as named in
-- JSON document
data WhatT = DeclT DeclT
| FixgrpT FixgrpT
| TypeT TypeT
| ExprT ExprT
| CaseT
| PatT PatT
| ModuleT
deriving (Show,Eq)
data DeclT = TermDT | FixgrpDT
deriving (Show,Eq)
data FixgrpT = ItemFT
deriving (Show,Eq)
data TypeT = ArrowTT | GlobTT | VaridxTT
deriving (Show,Eq)
data ExprT = LambdaET| ApplyET | GlobalET | ConstructorET | RelET | CaseET | LetET
deriving (Show,Eq)
data PatT = ConstructorPT | WildPT
deriving (Show,Eq)
-- | Parse the type of an element in the JSON document
toWhatType :: String -> Parser WhatT
toWhatType strType =
case strType of
"case" -> pure CaseT
"module" -> pure ModuleT
"decl:term" -> pure $ DeclT TermDT
"decl:fixgroup" -> pure $ DeclT FixgrpDT
"fixgroup:item" -> pure $ FixgrpT ItemFT
"type:arrow" -> pure $ TypeT ArrowTT
"type:glob" -> pure $ TypeT GlobTT
"type:varidx" -> pure $ TypeT VaridxTT
"expr:lambda" -> pure $ ExprT LambdaET
"expr:apply" -> pure $ ExprT ApplyET
"expr:global" -> pure $ ExprT GlobalET
"expr:constructor" -> pure $ ExprT ConstructorET
"expr:rel" -> pure $ ExprT RelET
"expr:case" -> pure $ ExprT CaseET
"expr:let" -> pure $ ExprT LetET
"pat:constructor" -> pure $ PatT ConstructorPT
"pat:wild" -> pure $ PatT WildPT
strError -> fail $ "Error: WhatType \"" ++ strError ++ "\" undefined"
instance FromJSON WhatT where
parseJSON (Object v) = toWhatType =<< v .: "what"
parseJSON _ = fail "Error: WhatType undefined"
type Name = String
type FunName = Name
type ArgName = Name
-- | Apply a function on all the names of an AST
class Renamable a where
rename :: (Name -> Name) -> a -> a
data Decl = Term { nameTerm :: Name
, typeTerm :: Type
, valueTerm :: Expr
}
| Fixgroup { fixItems :: [FixItem]
}
deriving (Show,Eq)
instance Renamable Decl where
rename f (Term n t v) = Term (f n) (rename f t) (rename f v)
rename f (Fixgroup gs) = Fixgroup (map (rename f) gs)
instance FromJSON Decl where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
DeclT TermDT -> Term <$> v .: "name" <*> v .: "type" <*> v .: "value"
DeclT FixgrpDT -> Fixgroup <$> v .: "fixlist"
_ -> fail "Error: Decl case undefined"
parseJSON _ = fail "Error: Decl kind undefined"
data FixItem = FixItem { nameItem :: Name
, typeItem :: Type
, valueItem :: Expr
}
deriving (Show,Eq)
instance Renamable FixItem where
rename f (FixItem n t v) = FixItem (f n) (rename f t) (rename f v)
instance FromJSON FixItem where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
FixgrpT ItemFT -> FixItem <$> v .: "name" <*> v .: "type" <*> v .: "value"
_ -> fail "Error: Fixgroup case undefined"
parseJSON _ = fail "Error: Fixgroup kind undefined"
data Type = Arrow { leftArrow :: Type
, rightArrow :: Type
}
| Glob { nameGlob :: Name
, argsGlob :: [Type]
}
| Varidx { nameVaridx :: Integer
}
deriving (Show,Eq)
instance Renamable Type where
rename f (Arrow l r) = Arrow (rename f l) (rename f r)
rename f (Glob n ts) = Glob (f n) (map (rename f) ts)
rename _ v = v
instance FromJSON Type where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
TypeT ArrowTT -> Arrow <$> v .: "left" <*> v .: "right"
TypeT GlobTT -> Glob <$> v .: "name" <*> v .: "args"
TypeT VaridxTT -> Varidx <$> v .: "name"
_ -> fail "Error: Type case undefined"
parseJSON _ = fail "Error: Type kind undefined"
data Expr = Lambda { argnamesLambda :: [Name]
, bodyLambda :: Expr
}
| Apply { funcApply :: Expr
, argsApply :: [Expr]
}
| Global { nameGlobal :: Name
}
| ConstructorE { nameConstructorE :: Name
, argsConstructorE :: [Expr]
}
| Rel { nameRel :: Name
}
| Case { exprCase :: Expr
, casesCase :: [Case]
}
| Let { nameLet :: Name
, namevalLet :: Expr
, bodyLet :: Expr
}
deriving (Show,Eq)
instance Renamable Expr where
rename f (Lambda ns e) = Lambda (map f ns) (rename f e)
rename f (Apply fun as) = Apply (rename f fun) (map (rename f) as)
rename f (Global n) = Global (f n)
rename f (ConstructorE n as) = ConstructorE (f n) (map (rename f) as)
rename f (Rel n) = Rel (f n)
rename f (Case e cs) = Case (rename f e) (map (rename f) cs)
rename f (Let n v b) = Let (f n) (rename f v) (rename f b)
instance FromJSON Expr where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
ExprT LambdaET -> Lambda <$> v .: "argnames" <*> v .: "body"
ExprT ApplyET -> Apply <$> v .: "func" <*> v .: "args"
ExprT GlobalET -> Global <$> v .: "name"
ExprT ConstructorET -> ConstructorE <$> v .: "name" <*> v .: "args"
ExprT RelET -> Rel <$> v .: "name"
ExprT CaseET -> Case <$> v .: "expr" <*> v .: "cases"
ExprT LetET -> Let <$> v .: "name" <*> v .: "nameval" <*> v .: "body"
_ -> fail "Error: Expr case undefined"
parseJSON _ = fail "Error: Expr kind undefined"
data Case = C { patC :: Pat
, bodyC :: Expr
}
deriving (Show,Eq)
instance Renamable Case where
rename f (C p b) = C (rename f p) (rename f b)
instance FromJSON Case where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
CaseT -> C <$> v .: "pat" <*> v .: "body"
_ -> fail "Error: Case case undefined"
parseJSON _ = fail "Error: Case kind undefined"
data Pat = ConstructorP { nameConstructorP :: Name
, argnamesConstructorP :: [Name]
}
| WildP
deriving (Show,Eq)
instance Renamable Pat where
rename f (ConstructorP n as) = ConstructorP (f n) (map f as)
rename _ w = w
instance FromJSON Pat where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
PatT ConstructorPT -> ConstructorP <$> v .: "name" <*> v .: "argnames"
PatT WildPT -> return WildP
_ -> fail "Error: Pat case undefined"
parseJSON _ = fail "Error: Pat kind undefined"
type ModuleUsed = Name
type FileName = String
data Module = Mod { nameMod :: Name
, needMagicMod :: Bool
, needDummyMod :: Bool
, usedModulesMod :: [ModuleUsed]
, declarationsMod :: [Decl]
}
deriving (Show,Eq)
instance Renamable Module where
rename f (Mod n m d mus ds) = Mod (f n) m d (map f mus) (map (rename f) ds)
instance FromJSON Module where
parseJSON (Object v) = do
what <- toWhatType =<< v .: "what"
case what of
ModuleT -> Mod <$>
v .: "name" <*>
v .: "need_magic" <*>
v .: "need_dummy" <*>
v .: "used_modules" <*>
v .: "declarations"
_ -> fail "Error: Module case undefined"
parseJSON _ = fail "Error: Module kind undefined"
-- | == Cleaning up the AST
-- | Drop the full qualification of names in the given 'Renamable' for
-- all the modules of 'modNames'
--
-- >>> unqualify ["Module"] (Global "Module.Test.val")
-- Global {nameGlobal = "Test.val"}
-- >>> unqualify ["Module"] (Global "Module2.val")
-- Global {nameGlobal = "Module2.val"}
-- >>> unqualify ["Module"] (Global "Module.Module.val")
-- Global {nameGlobal = "Module.val"}
-- >>> unqualify ["M"] (Mod "M.Test" False False [] [])
-- Mod {nameMod = "Test", needMagicMod = False, needDummyMod = False, usedModulesMod = [], declarationsMod = []}
-- >>> unqualify ["M"] (Mod "Mo.Test" False False [] [])
-- Mod {nameMod = "Mo.Test", needMagicMod = False, needDummyMod = False, usedModulesMod = [], declarationsMod = []}
--
unqualify :: Renamable r => [ModuleUsed] -> r -> r
unqualify modNames = rename go
where go n = case find (\m -> (m ++ ".") `isPrefixOf` n) modNames of
Just modName -> drop (length modName + 1) n
Nothing -> n
-- | Rename according to the given map
--
-- >>> rewriteNames (Map.fromList [("coq_true", "true")]) (Global "coq_true")
-- Global {nameGlobal = "true"}
-- >>> rewriteNames (Map.fromList [("coq_true", "true")]) (Global "coq_false")
-- Global {nameGlobal = "coq_false"}
rewriteNames :: Renamable r => Map Name Name -> r -> r
rewriteNames nameMap = rename f
where f n = fromMaybe n $ Map.lookup n nameMap
-- | Replace dots (qualified names) with a given string
--
-- >>> undotify "_" (Global "Module.function")
-- Global {nameGlobal = "Module_function"}
undotify :: Renamable r => String -> r -> r
undotify "." = id
undotify subst = rename (concatMap f)
where f '.' = subst
f x = [x]
-- | Clean up the source AST
--
-- Do:
--
-- * drop module names
-- * rewrite names according to the given map
-- * replace dots by the given string
clean :: Renamable r => [ModuleUsed] -> Map Name Name -> String -> r -> r
clean mods rewrts dot = undotify dot . rewriteNames rewrts . unqualify mods
-- | Clean up the source AST of a full module
--
-- Do a standard 'clean' /after/ a first pass to remove the name of
-- the module itself.
-- This is necessary because, when extracting a module @A@, the JSON
-- extractor extracts a definition @d@ as is (not with as @A.d@ but as
-- @d@); but it extracts a definition @d'@ in a submodule @B@ as
-- @A.B.d'@.
cleanModule :: [ModuleUsed] -> Map Name Name -> String -> Module -> Module
cleanModule mods rewrts dot modul = clean mods rewrts dot $ unqualify [nameMod modul] modul
-- | Description of how Coq’s nat constructors and addition function
-- are represented in the extracted AST
-- Recursive-function bounds are of type nat, these parameters define
-- how they will be identified in the extracted AST
data CoqNat = CN { natO :: FunName -- ^ How Coq’s O (nat) is extracted
, natS :: FunName -- ^ How Coq’s S (nat) is extracted
, natAdd :: FunName -- ^ How Coq’s addition function on nat is extracted
}
deriving (Show,Eq)
instance Default CoqNat where
def = CN { natO = "O"
, natS = "S"
, natAdd = "add"
}
-- | Type of the map associating function with their bound of
-- recursive calls (the name of the argument and its position)
type RecursiveBoundMap = Map FunName RecursiveBoundId
type Position = Int
type RecursiveBoundId = Position
-- | Type of a recursive-function bound and of its constant part
-- A recursive-function bound is the sum of a constant natural number
-- with some global values
type RecursiveBound = (RecursiveBoundConst, [Name])
type RecursiveBoundConst = Integer
-- | Detect bounds for all the recursive functions of a module
--
-- Recursive functions are accepted only whenever they have an
-- argument that is bounding the number of recursive steps and when
-- they always start by checking whether that bound is 0 or not
-- When a fixitem does have a recursive bound, return the name of the
-- fixitem and the pair of the name of the argument and its position
-- in the argument list
--
-- >>> :{
-- detectBounds def (Mod "Simple" False False []
-- [Fixgroup
-- [FixItem "recursive"
-- (Arrow (Glob "nat" []) (Glob "unit" []))
-- (Lambda ["bound"]
-- (Case (Rel "bound")
-- [C (ConstructorP "O" []) (ConstructorE "tt" [])
-- ,C (ConstructorP "S" ["n"]) (Apply (Global "recursive") [Rel "n"])]))]])
-- :}
-- fromList [("recursive",0)]
detectBounds :: CoqNat -> Module -> RecursiveBoundMap
detectBounds nats = Map.fromList . concatMap f . declarationsMod
where f (Fixgroup is) = mapMaybe (detectBoundFixItem nats) is
f _ = []
-- | Detect which argument is the bound in a FixItem
--
-- >>> :{
-- detectBoundFixItem def
-- (FixItem "recursive"
-- (Arrow (Glob "nat" []) (Glob "unit" []))
-- (Lambda ["bound"]
-- (Case (Rel "bound")
-- [C (ConstructorP "O" []) (ConstructorE "tt" [])
-- ,C (ConstructorP "S" ["n"]) (Apply (Global "recursive") [Rel "n"])])))
-- :}
-- Just ("recursive",0)
detectBoundFixItem :: CoqNat -> FixItem -> Maybe (FunName, RecursiveBoundId)
detectBoundFixItem CN{..} (FixItem ni _
(Lambda args
(Case (Rel na)
[C (ConstructorP o []) _
,C (ConstructorP s [_]) _])))
| o == natO && s == natS = do pos <- elemIndex na args
pure (ni, pos)
detectBoundFixItem _ _ = Nothing
type ErrorMsg = String
-- | Extract a recursive-function bound from an expression, when
-- possible
-- Recognize an expression as a recursive-function bound if it is
-- composed of (natural numbers) additions, S, O and global values
--
-- For example, we can have \( n + 1 \), written as preferred, or even
-- some more complex expression, like \( (n+1) + ((1+m) + 2) \),
-- reduced to \( n + m + 4 \).
--
-- >>> :{
-- extractRecBoundExpr
-- def
-- (ConstructorE "S" [Global "n"])
-- :}
-- Just (1,["n"])
--
-- >>> :{
-- extractRecBoundExpr
-- def
-- (Apply
-- (Global "add")
-- [Global "n"
-- ,ConstructorE "S" [ConstructorE "O" []]])
-- :}
-- Just (1,["n"])
--
-- >>> :{
-- extractRecBoundExpr
-- def
-- (Apply
-- (Global "add")
-- [ConstructorE "S" [Global "n"]
-- ,Apply (Global "add")
-- [Apply (Global "add")
-- [ConstructorE "S" [ConstructorE "O" []]
-- ,Global "m"]
-- ,ConstructorE "S" [ConstructorE "S" [ConstructorE "O" []]]]])
-- :}
-- Just (4,["n","m"])
--
extractRecBoundExpr :: CoqNat -> Expr -> Maybe (RecursiveBoundConst, [Name])
extractRecBoundExpr CN{..} = go
where go (Global n) = Just (0, [n])
go (ConstructorE o []) | o == natO = Just (0, [])
go (ConstructorE s [e]) | s == natS = first (+1) <$> go e
go (Apply (Global f) [e1,e2]) | f == natAdd = do (c1, ns1) <- go e1
(c2, ns2) <- go e2
pure (c1 + c2, ns1 ++ ns2)
go _ = Nothing
-- | Extract and rewrite recursive-function calls
-- Extract the list of recursive functions a given function calls;
-- also extract the bound (if there are more than one call to a given
-- recursive function, they must use the same bound)
-- Rewrite the expression to remove the recursive bounds from the calls
--
-- TODO: should the behaviour be to fail when various bounds are used
-- (to report the error), or extract one randomly, or?
--
-- >>> :{
-- extractRecCalls
-- def
-- "recursive"
-- (Map.fromList [("recursive",0)])
-- (Apply (Global "recursive") [Rel "n"])
-- :}
-- Right ([],Apply {funcApply = Global {nameGlobal = "recursive"}, argsApply = []})
--
-- >>> :{
-- extractRecCalls
-- def
-- "callrec"
-- (Map.fromList [("recursive",0)])
-- (Apply (Global "recursive") [Global "bnd"])
-- :}
-- Right ([("recursive",(0,["bnd"]))],Apply {funcApply = Global {nameGlobal = "recursive"}, argsApply = []})
--
extractRecCalls :: CoqNat -> FunName -> RecursiveBoundMap -> Expr -> Either ErrorMsg ([(FunName, RecursiveBound)], Expr)
extractRecCalls cn self recs expr = deDup <$> isConsistent (go expr)
where go :: Expr -> Either ErrorMsg ([(FunName, RecursiveBound)], Expr)
go e@(Apply fun@(Global f) args) = do
(nm, args') <- case Map.lookup f recs of
Just pos | pos < length args ->
case splitAt pos args of
(a1, _ : a2) | f == self -> pure (Nothing, a1 ++ a2)
(a1, a : a2) | isJust bnd -> pure (bnd, a1 ++ a2)
where bnd = extractRecBoundExpr cn a
_ -> Left $ expectedBound f pos e
| otherwise -> Left $ missingArgs f pos e
Nothing -> pure (Nothing, args)
(calls, expr') <- drills (Apply fun) args'
case nm of
Just nm' -> pure ((f, nm') : calls, expr')
Nothing -> pure (calls, expr')
go (Apply f args) = drills (Apply f) args
go (Lambda args body) = drill (Lambda args) body
go (ConstructorE n args) = drills (ConstructorE n) args
go (Case expr' cases) = do (calls, exprs) <- drills id (map bodyC cases)
let cases' = zipWith (\c e -> C (patC c) e) cases exprs
pure (calls, Case expr' cases')
go (Let var val body) = do (calls, let') <- drill (Let var) val
(calls', let'') <- drill let' body
pure (calls ++ calls', let'')
go e@(Global _) = pure ([], e)
go e@(Rel _) = pure ([], e)
drills f exprs = do (calls, exprs') <- unzip <$> traverse go exprs
pure (concat calls, f exprs')
drill f e = do (calls, e') <- go e
pure (calls, f e')
isConsistent r@(Right (calls, _)) = let assoc = Map.fromList calls
check = map (\(f, v) -> (f, Just v /= Map.lookup f assoc)) calls
in case find snd check of
Just (f, _) -> Left $ inconsistentCall f expr
Nothing -> r
isConsistent r = r
deDup (as, b) = (Set.toList (Set.fromList as), b)
missingArgs f nb e = "Not enough arguments: \"" ++ f ++ "\" expects at least " ++ show nb
++ " arguments; in " ++ show e
expectedBound f nb e = "Recursive bound argument expected: \"" ++ f ++ "\"'s "
++ show nb ++"th argument should be an expression containing only "
++ "natural numbers, additions and global values; in " ++ show e
inconsistentCall f e = "Inconsistent calls of " ++ f ++ " with different recursive bounds; in "
++ show e
stack.yaml
+ 1
− 1
View file @ d24f5e53
resolver: lts-6.17
resolver: lts-7.8
packages:
- '.'
......
version
+ 1
− 1
View file @ d24f5e53
v0.1
v0.2
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment