diff --git a/.gitignore b/.gitignore index 4667c9e46ba885833316fdeca82e984ce2df27f6..110336e98d8aacf83e0a452fe4ca83d2bfafa88c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,7 @@ *.o *.hi -Extractor +digger +.stack-work +dist +src/highlight.js +src/style.css diff --git a/Makefile b/Makefile index a1537c5bbdc80f604fdab19c0c0d2c7ccdc26300..3b471cfbc3f4900997020f3e140342280180c8d4 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,6 @@ +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 diff --git a/Readme.md b/Readme.md index 18c607d8858c65ee92bba00a3bc07a8d4fe67ef8..74c2faf51772f10683a2cb7ed7a52cc7aebca3cd 100644 --- a/Readme.md +++ b/Readme.md @@ -1,13 +1,16 @@ -# 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 diff --git a/app/digger.hs b/app/digger.hs new file mode 100644 index 0000000000000000000000000000000000000000..00936a28c8973e0b2a4b001c841c03d7b938d4ed --- /dev/null +++ b/app/digger.hs @@ -0,0 +1,353 @@ +-- | +-- 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 diff --git a/coq2c.cabal b/coq2c.cabal deleted file mode 100644 index ace74d24ce90688020943d269ac6ae8e3e86277c..0000000000000000000000000000000000000000 --- a/coq2c.cabal +++ /dev/null @@ -1,33 +0,0 @@ -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 diff --git a/coq2c.hs b/coq2c.hs deleted file mode 100644 index f25dcd81273ef4d3c28fe33d3f1ed3175625f8b3..0000000000000000000000000000000000000000 --- a/coq2c.hs +++ /dev/null @@ -1,1367 +0,0 @@ --- | --- 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") - ) diff --git a/digger.cabal b/digger.cabal new file mode 100644 index 0000000000000000000000000000000000000000..e7906b2319ed8f4a91272b9ddbe4f0f94238b229 --- /dev/null +++ b/digger.cabal @@ -0,0 +1,54 @@ +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 diff --git a/src/Language/Coq/Deep.hs b/src/Language/Coq/Deep.hs new file mode 100644 index 0000000000000000000000000000000000000000..31ab8f6d7177e7bdb24c2d44c37bfedc284288d9 --- /dev/null +++ b/src/Language/Coq/Deep.hs @@ -0,0 +1,766 @@ +-- 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 diff --git a/src/Language/Coq/ExtractedAST.hs b/src/Language/Coq/ExtractedAST.hs new file mode 100644 index 0000000000000000000000000000000000000000..7af363f7a4aea6ed9bf3c5f9652044ea62f11029 --- /dev/null +++ b/src/Language/Coq/ExtractedAST.hs @@ -0,0 +1,537 @@ +-- 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 diff --git a/stack.yaml b/stack.yaml index 7e0057e48aa9488a50ee1b6aed8c72098b5d54d8..baff5a58e7b7e14ec116588546732a8aaf146065 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-6.17 +resolver: lts-7.8 packages: - '.' diff --git a/version b/version index 085135ec98c54765be5be40d9501434b2ce803a4..60fe1f267badc7a9d0cb936f49f165395f00e25a 100644 --- a/version +++ b/version @@ -1 +1 @@ -v0.1 +v0.2