dedukti 1.0.3 → 1.1.0
raw patch · 24 files changed
+897/−477 lines, 24 filesdep +haskell-src-exts-qqdep +stringtable-atomdep +test-frameworkdep −textdep ~Streamdep ~hmkdep ~parsecbuild-type:Customsetup-changednew-component:exe:dedukti-tests
Dependencies added: haskell-src-exts-qq, stringtable-atom, test-framework
Dependencies removed: text
Dependency ranges changed: Stream, hmk, parsec
Files
- Dedukti.hs +68/−23
- Dedukti/Analysis/Rule.hs +7/−0
- Dedukti/Analysis/Scope.hs +26/−12
- Dedukti/CodeGen.hs +4/−3
- Dedukti/CodeGen/Exts.hs +82/−130
- Dedukti/Config.hs +13/−7
- Dedukti/Core.hs +6/−5
- Dedukti/DkM.hs +13/−12
- Dedukti/Driver/Batch.hs +28/−17
- Dedukti/Driver/Compile.hs +18/−20
- Dedukti/Module.hs +43/−22
- Dedukti/Parser.hs +19/−169
- Dedukti/Parser.hs-boot +9/−0
- Dedukti/Parser/External.hs +175/−0
- Dedukti/Parser/Prefix.hs +57/−0
- Dedukti/Pretty.hs +30/−14
- Dedukti/Rule.hs +5/−5
- Dedukti/Runtime.hs +21/−9
- Setup.lhs +13/−2
- Test.hs +90/−0
- dedukti.cabal +39/−14
- doc/manual.texi.in +129/−11
- doc/mkfile +1/−1
- scripts/dkrun +1/−1
Dedukti.hs view
@@ -6,6 +6,7 @@ -- arguments the appropriate driver is invoked. Everything is coordinated by -- the driver. This module is also the place where global configuration data -- is initialized.+ module Main where import System.Environment@@ -15,28 +16,66 @@ import Dedukti.Driver.Batch import Dedukti.Driver.Compile import Text.PrettyPrint.Leijen-import Control.Monad (unless, when)-import System.Console.GetOpt+import Data.List (partition, isPrefixOf)+import Data.Either (partitionEithers) import System.Exit import System.IO-import qualified Data.Text.Lazy.Encoding as T-import qualified Data.Text.Lazy as T-import qualified Data.ByteString.Lazy as B+import qualified Data.ByteString.Lazy.Char8 as B+import qualified Paths_dedukti as Cabal (version)+import Data.Version -data Flag = FlagMake | FlagHelp | FlagVersion | FlagVerbose | FlagVeryVerbose+data Flag = FlagMake+ | FlagJobs Int+ | FlagFormat Config.Format+ | FlagHelp | FlagVersion+ | FlagVerbose | FlagVeryVerbose deriving (Eq, Ord, Show) -options = [ Option [] ["make"] (NoArg FlagMake)- "Build MODULE and all its dependencies in one go."- , Option ['v'] [] (OptArg verb "v")- "Be verbose. -vv to be even more verbose."- , Option ['h'] ["help"] (NoArg FlagHelp) "This usage information."- , Option [] ["version"] (NoArg FlagVersion) "Output version information then exit." ]- where verb Nothing = FlagVerbose- verb (Just "v") = FlagVeryVerbose- verb _ = error "Unrecognized verbosity level."+data FlagArity a = Nullary String Flag+ | Unary String (String -> Flag) +flagDescriptions =+ [ ([Nullary "--make" FlagMake],+ "Build MODULE and all its dependencies in one go.")+ , ([Unary "-jN" (FlagJobs . read)],+ "Perform N jobs at once.")+ , ([Nullary "-fexternal" (FlagFormat Config.External)],+ "Force recognizing input as (human-readable) external format.")+ , ([Nullary "-fprefix-notation" (FlagFormat Config.Prefix)],+ "Force recognizing input as (fast) prefix format.")+ , ([Unary "-v[v]" $ \arg -> if null arg then FlagVerbose else FlagVeryVerbose],+ "Be verbose, -vv to be even more verbose.")+ , (zipWith ($) [Nullary "-h", Nullary "--help"] (repeat FlagHelp),+ "This usage information.")+ , ([Nullary "--version" FlagVersion],+ "Output version information then exit.") ]++-- Flag descriptions obey the following conventions:+--+-- - double hyphen flags don't have arguments.+--+-- - Everything after the first letter of a hyphen flag is part of the+-- argument.+parseCmdline args =+ let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args+ (errors, flags) = partitionEithers $ map toFlag hyphened+ in (flags, rest, errors)+ where flagmap = concatMap fst flagDescriptions+ unpack ('-':'-':name) = (name, "")+ unpack ('-':name:arg) = ([name], arg)+ unpack x = error $ "Malformed argument: " ++ x+ lookupFlag name arg (Nullary n f : desc)+ | fst (unpack n) == name =+ if null arg+ then Right f+ else Left $ "No argument expected for flag " ++ n+ lookupFlag name arg (Unary n f : desc)+ | fst (unpack n) == name = Right (f arg)+ lookupFlag name _ [] = Left $ "Flag not found: " ++ name+ lookupFlag name arg (_:desc) = lookupFlag name arg desc+ toFlag x | (name, arg) <- unpack x = lookupFlag name arg flagmap+ printUsage = do self <- parameter Config.imageName let header = show $ text "Usage:" <+>@@ -45,18 +84,22 @@ printHelp = do self <- parameter Config.imageName- let header = show $ text "Usage:" <+>+ let header = text "Usage:" <+> (text self <+> text "[OPTION]..." <+> text "MODULE") <$> text "Options:"- io $ putStrLn (usageInfo header options)+ flags = vsep (map pflag flagDescriptions)+ io $ putStrLn $ show $ header <$> indent 4 flags+ where pflag (flags, desc) = fillBreak 14 (hcat $ punctuate (text ", ") $+ map (text . name) flags) <+> text desc+ name (Nullary n _) = n+ name (Unary n _) = n bailout = printUsage >> io exitFailure printVersion = do self <- parameter Config.imageName- version <- parameter Config.version- io $ B.putStrLn $ T.encodeUtf8 $ T.pack $ flip displayS "" $ renderPretty 0.70 100 $- text "Dedukti" <+> text version <> line <> line <>+ io $ B.putStrLn $ B.pack $ flip displayS "" $ renderPretty 0.70 100 $+ text "Dedukti" <+> text (showVersion Cabal.version) <> line <> line <> text "Copyright (c) 2009 CNRS - École Polytechnique - INRIA." <> line <> line <> fillText "You may redistribute copies of Dedukti under the terms of \ \the GNU General Public License. For more information about \@@ -65,15 +108,17 @@ initializeConfiguration = foldr aux Config.defaultConfig where aux FlagVerbose c = c { Config.verbosity = Verbose } aux FlagVeryVerbose c = c { Config.verbosity = Debug }+ aux (FlagFormat f) c = c { Config.format = Just f }+ aux (FlagJobs n) c = c { Config.jobs = n } aux _ c = c main = do args <- getArgs- let (opts, files, errs) = getOpt RequireOrder options args+ let (opts, files, errs) = parseCmdline args when (not (null errs)) $ do- hPutDoc stderr (vsep (map text errs))+ hPutDoc stderr (vcat (map text errs) <> line) exitFailure- runDkM (initializeConfiguration opts) $+ (`runDkM` initializeConfiguration opts) $ case undefined of _ | FlagHelp `elem` opts -> printHelp | FlagVersion `elem` opts -> printVersion
Dedukti/Analysis/Rule.hs view
@@ -1,3 +1,9 @@+-- |+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA+-- License : GPL+--+-- Various checks on rules.+ module Dedukti.Analysis.Rule where import Dedukti.Core@@ -20,6 +26,7 @@ checkOrdering :: [TyRule Qid a] -> DkM () checkOrdering rules = do+ say Verbose $ text "Checking rule contiguity ..." mapM_ (\x -> when (length x > 1) (throw $ NonContiguousRules (head x))) $ group $ sort $ map head $ group $ map Rule.headConstant rules
Dedukti/Analysis/Scope.hs view
@@ -4,8 +4,7 @@ -- -- Check that all occurrences of variables are in scope of their definitions. -- Other well-formedness checks can also be found here, such as rejecting--- duplicate top-level definitions and enforcing contiguity of rule--- defnitions.+-- duplicate top-level definitions. module Dedukti.Analysis.Scope where @@ -15,7 +14,8 @@ import Dedukti.Pretty () import Dedukti.DkM import Data.List (sort, group)-import qualified Data.Set as Set+import qualified Data.Map as Map+import qualified StringTable.AtomSet as AtomSet newtype DuplicateDefinition = DuplicateDefinition Qid@@ -45,32 +45,46 @@ checkUniqueness :: Module Qid a -> DkM () checkUniqueness (decls, rules) = do+ say Verbose $ text "Checking that variables only appear once in rule environments ..." chk decls mapM_ (\(env :@ _) -> chk (env_bindings env)) rules where chk bs = mapM_ (\x -> when (length x > 1) (throw $ DuplicateDefinition (head x))) $ group $ sort $ map bind_name bs -checkScopes :: forall a. Show a => Set.Set Qid -> Module Qid a -> DkM ()+type Context = Map.Map MName AtomSet.AtomSet++-- | Initial environment to pass to 'checkScopes'.+initContext :: [Qid] -- ^ declarations from other modules.+ -> Context+initContext qids =+ Map.fromListWith AtomSet.union $ map (\qid -> (qid_qualifier qid, AtomSet.singleton (qid_stem qid))) qids++checkScopes :: forall a. Show a => Context -> Module Qid a -> DkM () checkScopes env (decls, rules) = do+ say Verbose $ text "Checking that all declarations are well scoped ..." topenv <- foldM chkBinding env decls mapM_ (chkRule topenv) rules- where chkBinding env (x ::: ty) = do+ where ins qid env = Map.insertWith' AtomSet.union (qid_qualifier qid)+ (AtomSet.singleton (qid_stem qid)) env+ mem qid env = maybe False (AtomSet.notMember (qid_stem qid))+ (Map.lookup (qid_qualifier qid) env)+ chkBinding env (x ::: ty) = do chkExpr env ty- return $ Set.insert x env+ return $ ins x env chkRule topenv r@(env :@ rule) = do- let lhsvars = Set.fromList [ x | Var x _ <- everyone (Rule.head r) ]- mapM_ (\x -> when (x `Set.notMember` lhsvars) $+ let lhsvars = AtomSet.fromList [ qid_stem x | Var x _ <- everyone (Rule.head r) ]+ mapM_ (\x -> when (qid_stem x `AtomSet.notMember` lhsvars) $ throw (IllegalEnvironment x)) (map bind_name $ env_bindings env) ruleenv <- foldM chkBinding topenv $ env_bindings env- descendM (chkExpr (topenv `Set.union` ruleenv)) rule+ descendM (chkExpr (Map.unionWith AtomSet.union topenv ruleenv)) rule chkExpr env t@(Var x _) = do- when (x `Set.notMember` env) (throw $ ScopeError x)+ when (x `mem` env) (throw $ ScopeError x) return (t :: Expr Qid a) chkExpr env (Lam (x ::: ty) t _) = do chkExpr env ty- chkExpr (Set.insert x env) t+ chkExpr (ins x env) t chkExpr env (Pi (x ::: ty) t _) = do chkExpr env ty- chkExpr (Set.insert x env) t+ chkExpr (ins x env) t chkExpr env t = descendM (chkExpr env) t
Dedukti/CodeGen.hs view
@@ -3,11 +3,12 @@ -- License : GPL -- -- Interface for all code generators.-module Dedukti.CodeGen (CodeGen(..)) where +module Dedukti.CodeGen where+ import Dedukti.Core import Dedukti.Module-import qualified Data.Text.Lazy as T+import Data.ByteString.Lazy.Char8 (ByteString) class CodeGen o where@@ -23,4 +24,4 @@ serialize :: MName -- ^ The module name -> [MName] -- ^ Dependencies -> Bundle o -- ^ Code- -> T.Text+ -> ByteString
Dedukti/CodeGen/Exts.hs view
@@ -13,13 +13,19 @@ import Dedukti.Pretty import qualified Dedukti.Rule as Rule import qualified Language.Haskell.Exts.Syntax as Hs+import qualified Language.Haskell.Exts.Build as Hs import Language.Haskell.Exts.Pretty-import qualified Data.Text.Lazy as T+import Language.Haskell.Exts.QQ+import qualified Data.ByteString.Lazy.Char8 as B import Data.Char (toUpper)+import Data.List (foldl') import qualified Data.Stream as Stream import Prelude hiding ((*)) +(*) :: Hs.SrcLoc -- dummy source location.+(*) = Hs.SrcLoc "" 0 0+ type Em a = a (Id Record) (A Record) type instance Id Record = Qid@@ -38,73 +44,68 @@ emit rs@(RS x ty rules) = Rec x (length rules) (function rs : def_ty : def_box : zipWith defs_rule [0..] rules)- where def_ty = value (x .$ "ty") (code ty)- def_box = value (x .$ "box")- (primbbox (term ty) (var (x .$ "ty")) (var x))+ where (tyname, boxname) = (varName (x .$ "ty"), varName (x .$ "box"))+ def_ty = [dec| ((tyname)) = $(code ty) |]+ def_box = [dec| ((boxname)) = bbox $(term ty) $(Hs.var tyname) $(var x) |] -- Checking rules involves much of the same work as checking all -- declarations at top-level, so let's just call the code -- generation functions recursively. defs_rule n (env :@ lhs :--> rhs) =- let rec (x ::: ty) rs = (emit (RS x ty []) :: Record) : rs- Bundle decls = coalesce $ foldr rec [ruleCheck] (env_bindings env)- in Hs.FunBind [Hs.Match (*) (varName (x .$ "rule" .$ T.pack (show n)))- []- Nothing- (Hs.UnGuardedRhs (primitiveVar "main" []))- (Hs.BDecls decls)]- where ruleCheck = Rec (qid "rule") 0- [value (qid "rule" .$ "box")- (primitiveVar "checkRule" [term lhs, term rhs])]+ let f (x ::: ty) rs = (emit (RS x ty []) :: Record) : rs+ ruleCheck = let rule_box = varName (qid "rule" .$ "box")+ in Rec (qid "rule") 0 [[dec| ((rule_box)) = checkRule $(term lhs) $(term rhs) |]]+ Bundle decls = coalesce $ foldr f [ruleCheck] (env_bindings env)+ rule = varName (x .$ "rule" .$ B.pack (show n))+ body = Hs.letE decls [hs| main |]+ in [dec| ((rule)) = $body |] coalesce records = Bundle $ concatMap rec_code records ++ [main]- where main = Hs.FunBind [Hs.Match (*) (Hs.Ident "main") []- Nothing (Hs.UnGuardedRhs checks) (Hs.BDecls [])]+ where main = [dec| main = $checks |] checks = Hs.Do (concatMap rules records ++ map declaration records)- declaration rec = Hs.Qualifier (primitiveVar "checkDeclaration"- [ Hs.Lit $ Hs.String $ show $ pretty $ unqualify $ rec_name rec- , var (rec_name rec .$ "box") ])+ declaration r = let desc = Hs.strE $ show $ pretty $ unqualify $ rec_name r+ in Hs.qualStmt [hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |] rules (Rec _ 0 _) = [] rules (Rec x nr _) =- [Hs.Qualifier $ primitiveVar "putStrLn" [Hs.Lit $ Hs.String ("Starting rule " ++ show (pretty (unqualify x)))]] ++- map (\n -> Hs.Qualifier $ var (x .$ "rule" .$ T.pack (show n))) [0..nr-1] ++- [Hs.Qualifier $ primitiveVar "putStrLn" [Hs.Lit $ Hs.String ("Finished rule " ++ show (pretty (unqualify x)))]]+ let startmsg = Hs.strE $ "Starting rule " ++ show (pretty (unqualify x)) ++ "."+ finishmsg = Hs.strE $ "Finished rule " ++ show (pretty (unqualify x)) ++ "."+ in [Hs.qualStmt [hs| putStrLn $startmsg |]]+ ++ map (\n -> Hs.qualStmt $ var (x .$ "rule" .$ B.pack (show n))) [0..nr-1]+ ++ [Hs.qualStmt [hs| putStrLn $finishmsg |]] serialize mod deps (Bundle decls) =- T.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $+ B.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $ Hs.Module (*) (modname mod) [] Nothing Nothing imports decls where imports = runtime : map (\m -> Hs.ImportDecl (*) (modname m) True False Nothing Nothing Nothing) deps runtime = Hs.ImportDecl (*) (Hs.ModuleName "Dedukti.Runtime") False False Nothing Nothing Nothing- modname m = Hs.ModuleName $ T.unpack $ T.intercalate "." $ map capitalize $ toList m+ modname m = Hs.ModuleName $ B.unpack $ B.intercalate "." $ map capitalize $ toList m -- | A similar encoding of names as the z-encoding of GHC. Non-letter -- characters are escaped with an x. xencode :: Qid -> String xencode qid =- T.unpack $- joinQ (qid_qualifier qid) `T.append`+ B.unpack $+ joinQ (qid_qualifier qid) `B.append` -- Prepend all idents with an x to avoid clash with runtime functions.- T.cons 'x' (enc (qid_stem qid)) `T.append`+ B.cons 'x' (enc $ fromAtom $ qid_stem qid) `B.append` joinS (qid_suffix qid) where joinQ Root = ""- joinQ (h :. x) = joinQ h `T.append` capitalize x `T.append` "."+ joinQ (h :. x) = joinQ h `B.append` capitalize (fromAtom x) `B.append` "." joinS Root = ""- joinS (h :. x) = joinS h `T.append` "_" `T.append` x- enc = T.concatMap f where+ joinS (h :. x) = joinS h `B.append` "_" `B.append` fromAtom x+ enc = B.concatMap f where f 'x' = "xx" f '\'' = "xq" f '_' = "xu"- f x | x >= '0', x <= '9' = 'x' `T.cons` T.singleton x- | otherwise = T.singleton x+ f x | x >= '0', x <= '9' = 'x' `B.cons` B.singleton x+ | otherwise = B.singleton x function :: Em RuleSet -> Hs.Decl-function (RS x _ []) =- Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs (primCon x)) (Hs.BDecls [])]-function (RS x _ rs) =- Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs rhs) (Hs.BDecls [f])]+function (RS x _ []) = Hs.nameBind (*) (varName x) (constant x)+function (RS x _ rs) = Hs.sfun (*) (varName x) [] (Hs.UnGuardedRhs rhs) (Hs.binds [f]) where n = Rule.arity (head rs)- rhs = foldr primLam- (application (Hs.Var (Hs.UnQual (Hs.Ident "__")) : Stream.take n variables))- (Stream.take n pvariables)+ occs = Stream.take n (Stream.map Hs.var variables)+ pats = Stream.take n variables+ rhs = foldr (\x y -> [hs| Lam (\((x)) -> $y) |]) (Hs.metaFunction "__" occs) pats f | n > 0 = Hs.FunBind (map clause rs ++ [defaultClause x n]) | otherwise = Hs.FunBind (map clause rs) @@ -112,120 +113,71 @@ clause rule = let (lrule@(env :@ _ :--> rhs), constraints) = Rule.linearize qids rule in if null constraints- then Hs.Match (*) (Hs.Ident "__") (map (pattern env) (Rule.patterns lrule))- Nothing (Hs.UnGuardedRhs (code rhs)) (Hs.BDecls [])- else Hs.Match (*) (Hs.Ident "__") (map (pattern env) (Rule.patterns lrule))- Nothing (Hs.GuardedRhss [Hs.GuardedRhs (*) (guards constraints) (code rhs)]) (Hs.BDecls [])- where guards constraints =- map (\(x, x') -> Hs.Qualifier $- primitiveVar "convertible" [Hs.Lit (Hs.Int 0), var x, var x']) constraints- qids = Stream.unfold (\i -> ((qid $ T.pack $ show i) .$ "fresh", i + 1)) 0+ then Hs.Match (*) (Hs.name "__") (map (pattern env) (Rule.patterns lrule))+ Nothing (Hs.UnGuardedRhs (code rhs)) Hs.noBinds+ else Hs.Match (*) (Hs.name "__") (map (pattern env) (Rule.patterns lrule))+ Nothing (Hs.GuardedRhss [Hs.GuardedRhs (*) (guards constraints) (code rhs)]) Hs.noBinds+ where guards = map (\(x, x') -> Hs.qualStmt $+ [hs| convertible 0 $(var x) $(var x') |])+ qids = Stream.unfold (\i -> ((qid $ B.pack $ show i) .$ "fresh", i + 1)) 0 defaultClause :: Id Record -> Int -> Hs.Match defaultClause x n =- Hs.Match (*) (Hs.Ident "__") (Stream.take n pvariables) Nothing- (Hs.UnGuardedRhs (primApps x (Stream.take n variables))) (Hs.BDecls [])--value :: Id Record -> Hs.Exp -> Hs.Decl-value x rhs =- Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs rhs) (Hs.BDecls [])]+ Hs.Match (*) (Hs.name "__") (Stream.take n (Stream.map Hs.pvar variables)) Nothing+ (Hs.UnGuardedRhs (foldl' (\e x -> [hs| App $e $x |]) (constant x) (Stream.take n (Stream.map Hs.var variables)))) Hs.noBinds +constant c = [hs| Con $(Hs.strE $ show $ pretty c) |] pattern :: Em Env -> Em Expr -> Hs.Pat-pattern env (Var x _) | x `isin` env = pvar x+pattern env (Var x _) | x `isin` env = Hs.pvar (varName x) pattern env expr = case unapply expr of Var x _ : xs -> primAppsP x (map (pattern env) xs) +-- | Build a pattern matching constant.+primConP c = Hs.PParen (Hs.pApp (Hs.name "Con") [Hs.strP (show (pretty c))])+primAppP t1 t2 = Hs.PParen (Hs.pApp (Hs.name "App") [t1, t2])+primAppsP c = foldl' primAppP (primConP c)+ -- | Turn an expression into object code with types erased. code :: Em Expr -> Hs.Exp code (Var x _) = var x-code (Lam (x ::: ty) t _) = primLam (pvar x) (code t)-code (Lam (Hole ty) t _) = primLam Hs.PWildCard (code t)-code (Pi (x ::: ty) t _) = primPi (code ty) (pvar x) (code t)-code (Pi (Hole ty) t _) = primPi (code ty) Hs.PWildCard (code t)-code (App t1 t2 _) = primap (code t1) (code t2)-code Type = primType+code (Lam (x ::: ty) t _) | n <- varName x = [hs| Lam (\((n)) -> $(code t)) |]+code (Lam (Hole ty) t _) = [hs| Lam (\_ -> $(code t)) |]+code (Pi (x ::: ty) t _) | n <- varName x = [hs| Pi $(code ty) (\((n)) -> $(code t)) |]+code (Pi (Hole ty) t _) = [hs| Pi $(code ty) (\_ -> $(code t)) |]+code (App t1 t2 _) = [hs| ap $(code t1) $(code t2) |]+code Type = [hs| Type |] -- | Turn a term into its Haskell representation, including all types. term :: Em Expr -> Hs.Exp term (Var x _) = var (x .$ "box")-term (Lam b t _) = primTLam b (term t)-term (Pi b t _) = primTPi b (term t)-term (App t1 t2 _) = primTApp (term t1) (primUBox (term t2) (code t2))-term Type = primTType-term Kind = primTKind+term (Lam b t _) = typedAbstraction [hs| TLam |] b (term t)+term (Pi b t _) = typedAbstraction [hs| TPi |] b (term t)+term (App t1 t2 _) = [hs| TApp $(term t1) (UBox $(term t2) $(code t2)) |]+term Type = [hs| TType |] -(*) :: Hs.SrcLoc-(*) = Hs.SrcLoc "" 0 0+typedAbstraction c b t =+ case b of+ x ::: ty -> [hs| $c $(dom ty) (\((box)) -> $ran) |]+ where box = varName (x .$ "box")+ ran = let n = varName x+ in [hs| let ((n)) = obj $(Hs.var box) in $t |]+ Hole ty -> [hs| $c $(dom ty) (\_ -> $t) |]+ where dom ty = if isVariable ty+ then term ty else [hs| sbox $(term ty) Type $(code ty) |] varName :: Id Record -> Hs.Name-varName = Hs.Ident . xencode . unqualify+varName = Hs.name . xencode . unqualify -- | Smart variable constructor. var :: Id Record -> Hs.Exp-var = Hs.Var . Hs.UnQual . Hs.Ident . xencode--pvar :: Id Record -> Hs.Pat-pvar = Hs.PVar . varName+var = Hs.var . Hs.name . xencode -- | Produce a set of variables y1, ..., yn-variables =- Stream.unfold (\i -> (Hs.Var $ Hs.UnQual $ Hs.Ident $ ('y':) $ show i, i + 1)) 0--pvariables =- Stream.unfold (\i -> (Hs.PVar $ Hs.Ident $ ('y':) $ show i, i + 1)) 0--application :: [Hs.Exp] -> Hs.Exp-application = foldl1 Hs.App---- Primitives--primitiveVar s [] = Hs.Var $ Hs.UnQual $ Hs.Ident s-primitiveVar s xs = Hs.Paren $ application $ (Hs.Var $ Hs.UnQual $ Hs.Ident s) : xs--primitiveCon s [] = Hs.Con $ Hs.UnQual $ Hs.Ident s-primitiveCon s xs = Hs.Paren $ application $ (Hs.Con $ Hs.UnQual $ Hs.Ident s) : xs--primap t1 t2 = primitiveVar "ap" [t1, t2]-primApp t1 t2 = primitiveCon "App" [t1, t2]-primCon c = primitiveCon "Con" [Hs.Lit (Hs.String (show (pretty c)))]-primType = primitiveCon "Type" []--primLam pat t = primitiveCon "Lam" [Hs.Paren (Hs.Lambda (*) [pat] t)]-primPi dom pat range = primitiveCon "Pi" [dom, Hs.Paren (Hs.Lambda (*) [pat] range)]--primApps c = foldl primApp (primCon c)--typedAbstraction c b t =- let (pat, ty, ran) =- case b of- x ::: ty -> ( pvar (x .$ "box")- , ty- , Hs.Let (Hs.BDecls [value x (primobj (var (x .$ "box")))]) t )- Hole ty -> (Hs.PWildCard, ty, t)- dom = if isVariable ty- then term ty else primsbox (term ty) primType (code ty)- in primitiveCon c [dom, Hs.Paren (Hs.Lambda (*) [pat] ran)]--primTLam = typedAbstraction "TLam"-primTPi = typedAbstraction "TPi"-primTApp t1 t2 = primitiveCon "TApp" [t1, t2]-primTType = primitiveCon "TType" []-primTKind = primitiveCon "TKind" []--primUBox ty obj_code = primitiveCon "UBox" [ty, obj_code]-primbbox ty ty_code obj_code = primitiveVar "bbox" [ty, ty_code, obj_code]-primsbox ty ty_code obj_code = primitiveVar "sbox" [ty, ty_code, obj_code]--primobj t = primitiveVar "obj" [t]---- | Build a pattern matching a constant.-primConP c = Hs.PParen $ Hs.PApp (Hs.UnQual $ Hs.Ident "Con") [Hs.PLit (Hs.String (show (pretty c)))]-primAppP t1 t2 = Hs.PParen $ Hs.PApp (Hs.UnQual $ Hs.Ident "App") [t1, t2]-primAppsP c = foldl primAppP (primConP c)+variables = Stream.unfold (\i -> (Hs.name $ ('y':) $ show i, i + 1)) 0 -- | Capitalize a word.-capitalize :: T.Text -> T.Text-capitalize s = case T.uncons s of- Nothing -> T.empty- Just (x, xs) -> toUpper x `T.cons` xs+capitalize :: B.ByteString -> B.ByteString+capitalize s = case B.uncons s of+ Nothing -> B.empty+ Just (x, xs) -> toUpper x `B.cons` xs
Dedukti/Config.hs view
@@ -6,22 +6,28 @@ module Dedukti.Config where +import System.Environment (getProgName)+import System.IO.Unsafe (unsafePerformIO) + data Verbosity = Quiet | Verbose | Debug deriving (Eq, Ord, Show) +data Format = External | Prefix+ deriving (Eq, Ord, Show)+ data Config = Config- { homeDir :: FilePath- , imageName :: FilePath- , version :: String+ { imageName :: FilePath , hsCompiler :: FilePath , verbosity :: Verbosity+ , format :: Maybe Format -- ^ @Just format@ if input format is forced.+ , jobs :: Int -- ^ Number of simultaneous jobs to run. } defaultConfig =- Config { homeDir = "."- , imageName = "dedukti"+ Config { imageName = unsafePerformIO $ getProgName , hsCompiler = "ghc"- , version = "0.1"- , verbosity = Quiet }+ , verbosity = Quiet+ , format = Nothing+ , jobs = 1 }
Dedukti/Core.hs view
@@ -16,7 +16,8 @@ , bind_name, bind_type , isAbstraction, isApplication, isVariable, isAtomic, isApplicative -- * Environments- , emptyEnv, env_bindings, env_domain, env_codomain, (&), (!), isin+ , emptyEnv, env_bindings, env_domain, env_codomain, (&), (!)+ , isin, fromBindings -- * Annotations , Unannot, nann, (%%), (%%%), (<%%>), (<%%%>) -- * Smart constructors@@ -45,8 +46,8 @@ -- | A type decorating a variable, or a type on its own. data Binding id a = id ::: Expr id a- | Hole (Expr id a)- deriving (Eq, Ord, Show)+ | Hole (Expr id a)+ deriving (Eq, Ord, Show) -- | A rewrite rule. data Rule id a = Expr id a :--> Expr id a@@ -186,10 +187,10 @@ class Ord (Id t) => Transform t where -- | Effectful bottom-up transformation on terms.- transformM :: (Monad m, Ord (Id t)) => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t+ transformM :: Monad m => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t -- | Helper function for top-down transformations.- descendM :: (Monad m, Ord (Id t)) => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t+ descendM :: Monad m => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t instance Ord id => Transform (Module id a) where transformM f (decls, rules) =
Dedukti/DkM.hs view
@@ -7,15 +7,16 @@ -- facilities and an interface to the system are also provided. module Dedukti.DkM ( module Control.Monad- , DkM, runDkM, warn, warnings, say- , Verbosity(..)- , configuration, parameter- , command- -- pretty-printing combinators.- , Pretty(..), text, (<+>), (<>), int- , fillText- , E.Exception(..), Typeable, E.throw, io- , onException) where+ , DkM, runDkM, warn, warnings, say+ , Verbosity(..)+ , configuration, parameter+ , command+ -- * pretty-printing combinators.+ , Pretty(..), text, (<+>), (<>), int+ , fillText+ , E.Exception(..), Typeable, E.throw, io+ -- * Wrappers around IO primitives.+ , onException) where import Dedukti.Config as Config import Control.Monad@@ -36,8 +37,8 @@ newtype DkM a = DkM (ReaderT Config IO a) deriving (Monad, MonadIO, Functor, Applicative, MonadReader Config) -runDkM :: Config -> DkM a -> IO a-runDkM conf (DkM m) = runReaderT m conf+runDkM :: DkM a -> Config -> IO a+runDkM (DkM m) = runReaderT m -- | Get all global parameters. configuration :: DkM Config@@ -78,4 +79,4 @@ onException :: DkM a -> DkM b -> DkM a onException x y = do conf <- configuration- io $ runDkM conf x `E.onException` runDkM conf y+ io $ runDkM x conf `E.onException` runDkM y conf
Dedukti/Driver/Batch.hs view
@@ -4,6 +4,7 @@ -- -- The batch driver. It compiles all given targets and all their dependencies, -- also invoking the Haskell compiler on the generated source code.+ module Dedukti.Driver.Batch (make) where import Dedukti.Driver.Compile@@ -14,12 +15,10 @@ import qualified Dedukti.Config as Config import qualified Control.Hmk.IO as IO import Control.Hmk-import qualified Data.Text.Lazy.Encoding as T-import qualified Data.ByteString.Lazy as B+import qualified Data.ByteString.Lazy.Char8 as B import qualified Data.Map as Map import Control.Monad.State import Control.Applicative-import Data.Typeable (Typeable) import System.Directory (copyFile) import Data.Char (toUpper) @@ -47,7 +46,8 @@ Nothing -> do lift $ say Verbose $ text "Parsing" <+> text (show mod) <+> text "..." let path = srcPathFromModule mod- src <- lift (parse path <$> io (liftM T.decodeUtf8 (B.readFile path)))+ config <- lift configuration+ src <- lift (parse config path <$> io (B.readFile path)) let dependencies = collectDependencies src rs = g mod dependencies (task_compile mod src) -- Recursively construct rules for dependent modules.@@ -72,23 +72,23 @@ , Rule hi (dko:dki:dephis) (Just $ task_hscomp dko) cmp , Rule o (dko:dki:dephis) (Just $ task_hscomp dko) cmp , Rule chi [hi] (Just $ task_himv hi chi) cmp ]- task_hscomp dko _ = do+ task_hscomp dko _ = abortOnError $ do hscomp <- parameter Config.hsCompiler io . IO.testExitCode =<< command hscomp [ "-c", "-w", "-x", "hs", dko , "-XOverloadedStrings" , "-XPatternGuards" ] -- GHC won't find the interface files if their names don't start with a -- capital letter. So alias the interface file with a capitalized name.- task_himv hi chi _ = do+ task_himv hi chi _ = abortOnError $ do io $ copyFile hi chi return TaskSuccess- task_compile mod src _ = do+ task_compile mod src _ = abortOnError $ do compileAST mod src `onException` (say Quiet $ text "In module" <+> pretty mod <> text ":") return TaskSuccess data CommandError = CommandError- deriving Typeable+ deriving Typeable instance Show CommandError where show CommandError = "Command returned non-zero exit status."@@ -97,19 +97,30 @@ -- | Perform each system action, aborting if an action returns -- non-zero exit code.-abortOnError :: [DkM Result] -> DkM ()-abortOnError = mapM_ f where- f cmd = do code <- cmd- case code of- TaskSuccess -> return ()- TaskFailure -> throw CommandError+abortOnError :: DkM Result -> DkM Result+abortOnError cmd = do+ code <- cmd+ case code of+ TaskFailure -> throw CommandError+ x -> return x -- | Compile each of the modules given as input and all of their -- dependencies, if necessary. make :: [MName] -> DkM () make modules = do+ config <- configuration let targets = map (pathFromModule ".o") modules+ run :: Rule DkM a -> Rule IO a+ run Rule{..} = Rule{ recipe = fmap (\f x -> runDkM (f x) config) recipe+ , isStale = \x y -> runDkM (isStale x y) config+ , .. } rs <- process cmp <$> rules modules- schedule <- mk rs targets- say Debug $ text "Tasks to execute:" <+> int (length schedule)- abortOnError schedule+ -- Depending on whether we have several cores or not, we either call+ -- mkConcurrent to perform all the tasks concurrently, or call mk to create+ -- a schedule and execute that.+ n <- parameter Config.jobs+ if n > 1 then+ do io $ mkConcurrent n (map run rs) targets else+ do schedule <- mk rs targets+ say Verbose $ text "Tasks to execute:" <+> int (length schedule)+ sequence_ schedule
Dedukti/Driver/Compile.hs view
@@ -8,29 +8,26 @@ import Dedukti.Module import Dedukti.Parser+import qualified Dedukti.Parser.Interface as Interface import Dedukti.DkM import Dedukti.Core import Dedukti.Analysis.Dependency import Dedukti.Analysis.Scope+import Control.Applicative import qualified Dedukti.CodeGen.Exts as CG import qualified Dedukti.Rule as Rule import qualified Dedukti.Analysis.Rule as Rule-import qualified Data.Text.Lazy as T-import qualified Data.Text.Lazy.Encoding as T-import qualified Data.ByteString.Lazy as B+import qualified Data.ByteString.Lazy.Char8 as B import qualified Data.Set as Set -readT = io . liftM T.decodeUtf8 . B.readFile-writeT path = io . B.writeFile path . T.encodeUtf8- -- | Qualify all occurrences of identifiers defined in current module. selfQualify :: MName -> [Pa RuleSet] -> [Pa RuleSet] selfQualify mod rsets = let defs = Set.fromList (map rs_name rsets) in map (descend (f defs))- (map (\RS{..} -> RS{rs_name = rs_name{qid_qualifier = mod}, ..}) rsets)+ (map (\RS{..} -> RS{rs_name = qualify mod rs_name, ..}) rsets) where f defs (Var x a) | Nothing <- provenance x- , x `Set.member` defs = Var x{qid_qualifier = mod} a+ , x `Set.member` defs = Var (qualify mod x) a f defs (Lam (x ::: ty) t a) = Lam (x ::: f defs ty) (f (Set.delete x defs) t) a f defs (Pi (x ::: ty) t a) =@@ -39,24 +36,24 @@ -- | Read the interface file of each module name to collect the declarations -- exported by the module.-populateInitialEnvironment :: [MName] -> DkM (Set.Set Qid)-populateInitialEnvironment =- liftM Set.unions .+populateInitialEnvironment :: [MName] -> DkM Context+populateInitialEnvironment deps =+ initContext . concat <$> mapM (\dep -> let path = ifacePathFromModule dep- in liftM (Set.fromList . map (qual dep) . parseIface path) $- readT path)- where qual mod qid = qid{qid_qualifier = mod}+ in map (qualify dep) . Interface.parse path <$>+ io (B.readFile path)) deps -- | Generate the content of an interface file.-interface :: Pa Module -> T.Text-interface (decls, _) = T.unlines (map (qid_stem . bind_name) decls)+interface :: Pa Module -> B.ByteString+interface (decls, _) = B.unlines (map (fromAtom . qid_stem . bind_name) decls) -- | Emit Haskell code for one module. compile :: MName -> DkM () compile mod = do say Verbose $ text "Parsing" <+> text (show mod) <+> text "..." let path = srcPathFromModule mod- compileAST mod =<< return (parse path) `ap` readT path+ config <- configuration+ compileAST mod =<< return (parse config path) `ap` io (B.readFile path) -- | Emit Haskell code for one module, starting from the AST. compileAST :: MName -> Pa Module -> DkM ()@@ -72,9 +69,10 @@ checkUniqueness src checkScopes extdecls src Rule.checkOrdering rules+ say Verbose $ text "Checking well formation of rule heads ..." mapM_ Rule.checkHead rules- say Debug $ pretty (concatMap rs_rules (Rule.ruleSets decls rules))+ say Debug $ pretty $ Rule.ruleSets decls rules say Verbose $ text "Compiling" <+> text (show mod) <+> text "..." let code = map CG.emit (selfQualify mod (Rule.ruleSets decls rules)) :: [CG.Code]- writeT (objPathFromModule mod) $ CG.serialize mod deps $ CG.coalesce code- writeT (ifacePathFromModule mod) $ interface src+ io $ B.writeFile (objPathFromModule mod) $ CG.serialize mod deps $ CG.coalesce code+ io $ B.writeFile (ifacePathFromModule mod) $ interface src
Dedukti/Module.hs view
@@ -5,6 +5,8 @@ -- A representation of module names and associated functions to map module -- names to source files and vice-versa. Qualified names, as required in the -- presence of modules, are also defined here.++{-# OPTIONS_GHC -funbox-strict-fields #-} module Dedukti.Module ( -- * Data types Hierarchy(..), MName@@ -14,18 +16,25 @@ , hierarchy, toList , pathFromModule, moduleFromPath , srcPathFromModule, objPathFromModule, ifacePathFromModule- -- * Qualified names.- , Qid(..), qid, (.$), provenance, unqualify+ -- * Qualified names+ , Qid, qid_qualifier, qid_stem, qid_suffix+ , qid, (.$), provenance, qualify, unqualify+ -- * Atoms+ , Atom+ , fromAtom, toAtom ) where import Dedukti.DkM import System.FilePath import Data.Char (isAlpha, isAlphaNum)-import qualified Data.Text.Lazy as T+import qualified Data.ByteString.Lazy.Char8 as B+import qualified Data.ByteString as BS (concat) import Text.PrettyPrint.Leijen+import qualified StringTable.Atom as Atom+import StringTable.Atom (Atom) -data Hierarchy = !Hierarchy :. !T.Text | Root+data Hierarchy = !Hierarchy :. !Atom | Root deriving (Eq, Ord, Show) type MName = Hierarchy@@ -39,31 +48,37 @@ instance Exception InvalidModuleName instance Pretty MName where- pretty (Root :. x) = text (T.unpack x)- pretty (xs :. x) = pretty xs <> char '.' <> text (T.unpack x)+ pretty (Root :. x) = text (B.unpack (fromAtom x))+ pretty (xs :. x) = pretty xs <> char '.' <> text (B.unpack (fromAtom x)) -hierarchy :: [T.Text] -> Hierarchy+fromAtom :: Atom -> B.ByteString+fromAtom = B.fromChunks . return . Atom.fromAtom++toAtom :: B.ByteString -> Atom+toAtom = Atom.toAtom . BS.concat . B.toChunks++hierarchy :: [B.ByteString] -> Hierarchy hierarchy = f . reverse where f [] = Root- f (x:xs) = f xs :. x+ f (x:xs) = f xs :. toAtom x -toList :: Hierarchy -> [T.Text]+toList :: Hierarchy -> [B.ByteString] toList = reverse . f where f Root = []- f (xs :. x) = x : f xs+ f (xs :. x) = fromAtom x : f xs -- | Raise an exception if module name component is a valid identifier. check :: String -> String-check cmpt@(x:xs) | isAlpha x, and (map isAlphaNum xs) = cmpt+check cmpt@(x:xs) | isAlpha x, and (map (\x -> isAlphaNum x || elem x "_-+~") xs) = cmpt | otherwise = throw $ InvalidModuleName cmpt pathFromModule :: String -> MName -> FilePath pathFromModule ext mod =- addExtension (joinPath $ map T.unpack $ toList mod) ext+ addExtension (joinPath $ map B.unpack $ toList mod) ext moduleFromPath :: FilePath -> MName moduleFromPath =- hierarchy . map (T.pack . check) . splitDirectories . dropExtension+ hierarchy . map (B.pack . check) . splitDirectories . dropExtension srcPathFromModule :: MName -> FilePath srcPathFromModule = pathFromModule ".dk"@@ -75,24 +90,30 @@ ifacePathFromModule = pathFromModule ".dki" -- | The datatype of qualified names.-data Qid = Qid { qid_qualifier :: !Hierarchy- , qid_stem :: !T.Text- , qid_suffix :: !Hierarchy }- deriving (Eq, Ord, Show)+data Qid = Qid !Hierarchy !Atom !Hierarchy+ deriving (Eq, Show, Ord) +qid_qualifier (Qid qual _ _) = qual+qid_stem (Qid _ stem _) = stem+qid_suffix (Qid _ _ suf) = suf+ -- | Shorthand qid introduction.-qid :: T.Text -> Qid-qid x = Qid Root x Root+qid :: B.ByteString -> Qid+qid x = Qid Root (toAtom x) Root -- | Append suffix.-(.$) :: Qid -> T.Text -> Qid-(Qid qual x sufs) .$ suf = Qid qual x (sufs :. suf)+(.$) :: Qid -> B.ByteString -> Qid+(Qid qual x sufs) .$ suf = Qid qual x (sufs :. (toAtom suf)) -- | Get the module where the qid is defined, based on its qualifier. provenance :: Qid -> Maybe MName provenance (Qid Root _ _) = Nothing provenance (Qid qual _ _) = Just qual +-- | Set the qualifier.+qualify :: Hierarchy -> Qid -> Qid+qualify qual (Qid _ stem suf) = Qid qual stem suf+ -- | Remove any qualifier. unqualify :: Qid -> Qid-unqualify qid = qid{qid_qualifier = Root}+unqualify (Qid _ stem suf) = Qid Root stem suf
Dedukti/Parser.hs view
@@ -1,181 +1,31 @@ -- | -- Copyright : © 2009 CNRS - École Polytechnique - INRIA -- License : GPL+--+-- Frontend to all the different parsers available. This module abstracts over+-- that fact that input can come in different formats, providing a single+-- point of entry to parsing instead. -{-# OPTIONS_GHC -fno-warn-unused-binds #-}-module Dedukti.Parser (Pa, Dedukti.Parser.parse, parseIface) where+module Dedukti.Parser where +import qualified Dedukti.Config as Config+import qualified Dedukti.Parser.External as External+import qualified Dedukti.Parser.Prefix as Prefix import Dedukti.Core import Dedukti.Module-import Text.Parsec hiding (ParseError, parse)-import qualified Text.Parsec.Token as Token-import Control.Applicative hiding ((<|>), many)-import Control.Monad.Identity-import qualified Control.Exception as Exception-import qualified Data.Text.Lazy as T-import Data.Typeable (Typeable)+import qualified Data.ByteString.Lazy.Char8 as B +type SourceName = String+ -- The AST type as returned by the Parser. type Pa t = t Qid Unannot --- The parsing monad.-type P = Parsec String [Pa TyRule]--newtype ParseError = ParseError String- deriving Typeable--instance Show ParseError where- show (ParseError e) = e--instance Exception.Exception ParseError--newtype IfaceError = IfaceError String- deriving Typeable--instance Show IfaceError where- show (IfaceError f) = "Broken interface file " ++ f ++ "."--instance Exception.Exception IfaceError--parse :: SourceName -> T.Text -> Pa Module-parse name input =- -- At the toplevel, a source file is a list of declarations and rule- -- definitions. Here rules are accumulated by side-effect, added to the- -- parser state as we encounter them.- case runParser ((,) <$> toplevel <*> allRules) [] name (T.unpack input) of- Left e -> Exception.throw (ParseError (show e))- Right x -> x---- | Parser for interface files.-parseIface :: SourceName -> T.Text -> [Qid]-parseIface _ = map qid . T.lines--addRule :: Pa TyRule -> P ()-addRule rule = modifyState (rule:)---- | Retrieve all rules encountered so far from the parser state.-allRules :: P [Pa TyRule]-allRules = liftM reverse getState--lexDef = Token.LanguageDef- { Token.commentStart = "(;"- , Token.commentEnd = ";)"- , Token.commentLine = ";"- , Token.nestedComments = False- , Token.identStart = alphaNum <|> char '_' <|> char '\''- , Token.identLetter = alphaNum <|> char '_' <|> char '\''- , Token.opStart = parserFail "No user defined operators yet."- , Token.opLetter = parserFail "No user defined operators yet."- , Token.reservedNames = ["Type", "Kind"]- , Token.reservedOpNames = [":", "=>", "->", "-->"]- , Token.caseSensitive = True- }--Token.LanguageDef{..} = lexDef-Token.TokenParser{..} = Token.makeTokenParser lexDef---- | Qualified or unqualified name.------ > qid ::= id.id | id-qident = ident <?> "qid" where- ident = do- c <- identStart- cs <- many identLetter- x <- (do let qualifier = T.pack (c:cs)- c <- try $ do char '.'; identStart- cs <- many identLetter- let name = T.pack (c:cs)- return $ Qid (Root :. qualifier) name Root)- <|> return (qid (T.pack (c:cs)))- whiteSpace- return (Var x nann)---- | Unqualified name.-ident = qid . T.pack <$> identifier---- | Root production rule of the grammar.------ > toplevel ::= declaration toplevel--- > | rule toplevel--- > | eof-toplevel =- whiteSpace *>- ( (rule *> toplevel) -- Rules are accumulated by side-effect.- <|> ((:) <$> declaration <*> toplevel)- <|> (eof *> return []))---- | Binding construct.------ > binding ::= id : term-binding = ((:::) <$> ident <* reservedOp ":" <*> term)- <?> "binding"---- | Top-level declarations.------ > declaration ::= id ":" term "."-declaration = (binding <* dot)- <?> "declaration"---- | Left hand side of an abstraction or a product.------ > domain ::= id ":" applicative--- > | applicative-domain = ( ((:::) <$> try (ident <* reservedOp ":") <*> applicative)- <|> (Hole <$> applicative))- <?> "domain"---- |--- > sort ::= Type-sort = Type <$ reserved "Type"---- | Terms and types.------ We first try to parse as the domain of a lambda or pi. If we--- later find out there was no arrow after the domain, then we take--- the domain to be an expression, and return that.------ > term ::= domain "->" term--- > | domain "=>" term--- > | applicative-term = do- d <- domain- choice [ pi d <?> "pi"- , lambda d <?> "lambda"- , return (bind_type d)]- where pi d = Pi <$> pure d <* reservedOp "->" <*> term <%%> nann- lambda d = Lam <$> pure d <* reservedOp "=>" <*> term <%%> nann---- | Constituents of an applicative form.------ > simple ::= sort--- > | qid--- > | "(" term ")"-simple = sort <|> qident <|> parens term---- | Expressions that are either a name or an application of a--- expression to one or more arguments.------ > applicative ::= simple--- > | applicative simple--- >-applicative = (\xs -> case xs of- [t] -> t- (f:ts) -> apply f ts (repeat nann))- <$> many1 simple- <?> "applicative"---- | A rule.------ > rule ::= env term "-->" term--- > env ::= "[]"--- > | "[" env2 "]"--- > env2 ::= binding--- > | binding "," env2-rule = ((\env lhs rhs -> foldr (&) emptyEnv env :@ lhs :--> rhs)- <$> brackets (sepBy binding comma)- <*> term- <* reservedOp "-->"- <*> term- <* dot) >>= addRule- <?> "rule"+parse :: Config.Config -> SourceName -> B.ByteString -> Pa Module+parse config name input =+ let magic = "(; # FORMAT prefix # ;)\n" in+ case (magic `B.isPrefixOf` input, Config.format config) of+ (True, _) -> Prefix.parse name (B.drop (B.length magic) input)+ (False, Just Config.Prefix) -> Prefix.parse name input+ (False, Just Config.External) -> External.parse name input+ (False, Nothing) -> External.parse name input
+ Dedukti/Parser.hs-boot view
@@ -0,0 +1,9 @@+module Dedukti.Parser where++import Dedukti.Core+import Dedukti.Module+++type SourceName = String+type Pa t = t Qid Unannot+
+ Dedukti/Parser/External.hs view
@@ -0,0 +1,175 @@+-- |+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA+-- License : GPL++{-# OPTIONS_GHC -fno-warn-unused-binds #-}+module Dedukti.Parser.External (Pa, parse) where++import {-# SOURCE #-} Dedukti.Parser+import Dedukti.Core+import Dedukti.Module+import Text.Parsec hiding (SourceName, ParseError, parse)+import qualified Text.Parsec.Token as Token+import Control.Applicative hiding ((<|>), many)+import Control.Monad.Identity+import qualified Data.ByteString.Lazy.Char8 as B+import qualified Control.Exception as Exception+import Data.Typeable (Typeable)+++-- The parsing monad.+type P = Parsec B.ByteString [Pa TyRule]++newtype ParseError = ParseError String+ deriving Typeable++instance Show ParseError where+ show (ParseError e) = e++instance Exception.Exception ParseError++newtype IfaceError = IfaceError String+ deriving Typeable++instance Show IfaceError where+ show (IfaceError f) = "Broken interface file " ++ f ++ "."++instance Exception.Exception IfaceError++parse :: SourceName -> B.ByteString -> Pa Module+parse name input =+ -- At the toplevel, a source file is a list of declarations and rule+ -- definitions. Here rules are accumulated by side-effect, added to the+ -- parser state as we encounter them.+ case runParser ((,) <$> toplevel <*> allRules) [] name input of+ Left e -> Exception.throw (ParseError (show e))+ Right x -> x++addRule :: Pa TyRule -> P ()+addRule rule = modifyState (rule:)++-- | Retrieve all rules encountered so far from the parser state.+allRules :: P [Pa TyRule]+allRules = liftM reverse getState++lexDef = Token.LanguageDef+ { Token.commentStart = "(;"+ , Token.commentEnd = ";)"+ , Token.commentLine = ";"+ , Token.nestedComments = False+ , Token.identStart = alphaNum <|> char '_' <|> char '\''+ , Token.identLetter = alphaNum <|> char '_' <|> char '\''+ , Token.opStart = parserFail "No user defined operators yet."+ , Token.opLetter = parserFail "No user defined operators yet."+ , Token.reservedNames = ["Type", "Kind"]+ , Token.reservedOpNames = [":", "=>", "->", "-->"]+ , Token.caseSensitive = True+ }++Token.LanguageDef{..} = lexDef+Token.TokenParser{..} = Token.makeTokenParser lexDef++-- | Qualified or unqualified name.+--+-- > qid ::= id.id | id+qident = ident <?> "qid" where+ ident = do+ c <- identStart+ cs <- many identLetter+ x <- (do let qualifier = B.pack (c:cs)+ c <- try $ do char '.'; identStart+ cs <- many identLetter+ let name = B.pack (c:cs)+ return $ qualify (hierarchy [qualifier]) (qid name))+ <|> return (qid (B.pack (c:cs)))+ whiteSpace+ return (Var x nann)++-- | Unqualified name.+ident = qid . B.pack <$> identifier++-- | Root production rule of the grammar.+--+-- > toplevel ::= declaration toplevel+-- > | rule toplevel+-- > | eof+toplevel =+ whiteSpace *>+ ( (rule *> toplevel) -- Rules are accumulated by side-effect.+ <|> ((:) <$> declaration <*> toplevel)+ <|> (eof *> return []))++-- | Binding construct.+--+-- > binding ::= id ":" term+binding = ((:::) <$> ident <* reservedOp ":" <*> term)+ <?> "binding"++-- | Top-level declarations.+--+-- > declaration ::= binding "."+declaration = (binding <* dot)+ <?> "declaration"++-- | Left hand side of an abstraction or a product.+--+-- > domain ::= id ":" applicative+-- > | applicative+domain = ( ((:::) <$> try (ident <* reservedOp ":") <*> applicative)+ <|> (Hole <$> applicative))+ <?> "domain"++-- |+-- > sort ::= "Type"+sort = Type <$ reserved "Type"++-- | Terms and types.+--+-- We first try to parse as the domain of a lambda or pi. If we+-- later find out there was no arrow after the domain, then we take+-- the domain to be an expression, and return that.+--+-- > term ::= domain "->" term+-- > | domain "=>" term+-- > | applicative+term = do+ d <- domain+ choice [ pi d <?> "pi"+ , lambda d <?> "lambda"+ , return (bind_type d)]+ where pi d = Pi <$> pure d <* reservedOp "->" <*> term <%%> nann+ lambda d = Lam <$> pure d <* reservedOp "=>" <*> term <%%> nann++-- | Constituents of an applicative form.+--+-- > simple ::= sort+-- > | qid+-- > | "(" term ")"+simple = sort <|> qident <|> parens term++-- | Expressions that are either a name or an application of a+-- expression to one or more arguments.+--+-- > applicative ::= simple+-- > | applicative simple+-- >+applicative = (\xs -> case xs of+ [t] -> t+ (f:ts) -> apply f ts (repeat nann))+ <$> many1 simple+ <?> "applicative"++-- | A rule.+--+-- > rule ::= env term "-->" term "."+-- > env ::= "[]"+-- > | "[" env2 "]"+-- > env2 ::= binding+-- > | binding "," env2+rule = ((\env lhs rhs -> foldr (&) emptyEnv env :@ lhs :--> rhs)+ <$> brackets (sepBy binding comma)+ <*> term+ <* reservedOp "-->"+ <*> term+ <* dot) >>= addRule+ <?> "rule"
+ Dedukti/Parser/Prefix.hs view
@@ -0,0 +1,57 @@+-- |+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA+-- License : GPL+--+-- Parser for an alternative format for Dedukti source files using reverse+-- polish notation. This format has the advantage of being very easy to parse+-- efficiently.++{-# OPTIONS_GHC -funbox-strict-fields #-}+module Dedukti.Parser.Prefix (Pa, parse) where++import {-# SOURCE #-} Dedukti.Parser+import Dedukti.Core+import Dedukti.Module+import qualified Data.ByteString.Lazy.Char8 as B+import Data.Either (partitionEithers)+import Data.Char (isSpace)+++type Token = B.ByteString+data Frame = Expr !(Pa Expr)+ | Binding !(Pa Binding)+ | Env [Pa Binding]+ | TyRule !(Pa TyRule)++type Stack = [Frame]+++parse :: SourceName -> B.ByteString -> Pa Module+parse name = partitionEithers . map classify . foldr step [] . tokens+ where classify (Binding x) = Left x+ classify (TyRule x) = Right x+ classify _ = error $ "Parse error in " ++ name++tokens :: B.ByteString -> [Token]+tokens = filter (not . B.null) . B.splitWith isSpace++step :: Token -> Stack -> Stack++-- bindings+step ":" (Expr (Var x _) : Expr y : xs) = Binding (x ::: y) : xs++-- rules+step "-->" (Env x : Expr y : Expr z : xs) = TyRule (fromBindings x :@ y :--> z) : xs++-- environments+step "," (Binding x : Env y : xs) = Env (x:y) : xs+step "[]" xs = Env [] : xs++-- expressions+step "=>" (Binding x : Expr y : xs) = Expr (Lam x y %% nann) : xs+step "->" (Binding x : Expr y : xs) = Expr (Pi x y %% nann) : xs+step "@" (Expr x : Expr y : xs) = Expr (App x y %% nann) : xs+step "Type" xs = Expr Type : xs+step v xs = case reverse (B.split '.' v) of+ var : quals -> let mod = hierarchy (reverse quals)+ in Expr (Var (qualify mod (qid var)) %% nann) : xs
Dedukti/Pretty.hs view
@@ -12,15 +12,33 @@ import Dedukti.Core import Dedukti.Module import Text.PrettyPrint.Leijen-import qualified Data.Text.Lazy as T+import qualified Data.ByteString.Lazy.Char8 as B -textT = text . T.unpack+textB = text . B.unpack +-- | For purposes of pretty-printing, need to distinguish a top-level binding+-- from a binding representing the domain of a dependent product or+-- abstraction.+newtype Domain id a = Domain (Binding id a)++instance Pretty id => Pretty (Binding id a) where+ pretty (x ::: ty) = pretty x <+> char ':' <+> pretty ty+ pretty (Hole ty) = pretty ty++ prettyList = vcat . map (\x -> pretty x <> dot)++instance Pretty id => Pretty (Domain id a) where+ pretty (Domain dom) =+ let pty | Pi _ _ _ <- bind_type dom = parens (pretty (bind_type dom))+ | otherwise = pretty (bind_type dom)+ in case dom of+ x ::: _ -> pretty x <+> char ':' <+> pty+ Hole _ -> pty+ instance Pretty id => Pretty (Expr id a) where- pretty (Lam x t _) = pretty x <+> text "=>" <+> pretty t- pretty (Pi x t _) | Pi _ _ _ <- bind_type x = parens (pretty x) <+> text "->" <+> pretty t- | otherwise = pretty x <+> text "->" <+> pretty t+ pretty (Lam dom ran _) = pretty dom <+> text "=>" <+> pretty ran+ pretty (Pi dom ran _) = pretty (Domain dom) <+> text "->" <+> pretty ran pretty (App t1 t2 _) = let f = if isApplicative t1 then id else parens g = if isAtomic t2 then id else parens@@ -29,12 +47,6 @@ pretty Type = text "Type" pretty Kind = text "Kind" -instance Pretty id => Pretty (Binding id a) where- pretty (x ::: ty) = pretty x <+> char ':' <+> pretty ty- pretty (Hole ty) = pretty ty-- prettyList = vcat . map (\x -> pretty x <> dot)- instance Pretty id => Pretty (Rule id a) where pretty (lhs :--> rhs) = pretty lhs <+> text "-->" <+> pretty rhs @@ -48,11 +60,15 @@ prettyList = vcat . map (\x -> pretty x <> dot) +instance (Eq a, Ord id, Pretty id) => Pretty (RuleSet id a) where+ pretty RS{..} = vcat (pretty (rs_name ::: rs_type) : map pretty rs_rules)+ prettyList = vcat . punctuate line . map pretty+ instance Pretty Qid where pretty qid = joinQ (qid_qualifier qid) <>- textT (qid_stem qid) <>+ textB (fromAtom (qid_stem qid)) <> joinS (qid_suffix qid) where joinQ Root = empty- joinQ (h :. x) = joinQ h <> textT x <> dot+ joinQ (h :. x) = joinQ h <> textB (fromAtom x) <> dot joinS Root = empty- joinS (h :. x) = joinS h <> char '_' <> textT x+ joinS (h :. x) = joinS h <> char '_' <> textB (fromAtom x)
Dedukti/Rule.hs view
@@ -36,9 +36,9 @@ -- | Combine declarations with their associated rules, if any. ruleSets :: (Show id, Show a, Ord id) => [Binding id a] -> [TyRule id a] -> [RuleSet id a]-ruleSets ds rs = snd $ foldl aux (sortBy cmp (group rs), []) ds where- aux ([], rsets) (x ::: ty) = ([], RS x ty [] : rsets)- aux (rs : rss, rsets) (x ::: ty)+ruleSets ds rs = snd $ foldr aux (sortBy cmp (group rs), []) ds where+ aux (x ::: ty) ([], rsets) = ([], RS x ty [] : rsets)+ aux (x ::: ty) (rs : rss, rsets) | x == headConstant (Prelude.head rs) = (rss, RS x ty rs : rsets) | otherwise = (rs : rss, RS x ty [] : rsets) -- We cannot change the order of the declarations, but we need rules to be@@ -46,7 +46,7 @@ ordering = Map.fromList (zip (map bind_name ds) [0..]) cmp x y = let xi = ordering Map.! headConstant (Prelude.head x) yi = ordering Map.! headConstant (Prelude.head y)- in compare xi yi+ in compare yi xi -- | Make the rule left-linear and return collected unification constraints. -- This function must be provided with an infinite supply of fresh variable@@ -62,7 +62,7 @@ (xs, seen, constraints) <- get if x `Set.member` seen then do let Stream.Cons x' xs' = xs- put (xs', Set.insert x seen, (x, x'):constraints)+ put (xs', Set.insert x' seen, (x, x'):constraints) return $ Var x' a else do put (xs, Set.insert x seen, constraints) return t
Dedukti/Runtime.hs view
@@ -29,8 +29,8 @@ import Text.Show.Functions () import Data.Typeable hiding (typeOf) import Prelude hiding (pi, catch)-import System.IO import Data.Time.Clock+import Text.PrettyPrint.Leijen -- Exceptions@@ -41,7 +41,7 @@ data TypeError = TypeError deriving (Show, Typeable) -data RuleError = RuleError+data RuleError = RuleError Doc Doc deriving (Show, Typeable) instance Exception SortError@@ -106,25 +106,25 @@ typeOf :: Int -> Term -> Code typeOf n (Box ty _) = ty-typeOf n (TLam bx@(Box Type a) f) = Pi a (\x -> typeOf n (f (Box a x)))-typeOf n (TPi bx@(Box Type a) f) = typeOf (n + 1) (f (Box a (Var n)))-typeOf n (TApp t1 bx@(Box ty2 t2))+typeOf n (TLam (Box Type a) f) = Pi a (\x -> typeOf n (f (Box a x)))+typeOf n (TPi (Box Type a) f) = typeOf (n + 1) (f (Box a (Var n)))+typeOf n (TApp t1 (Box ty2 t2)) | Pi tya f <- typeOf n t1, convertible n tya ty2 = f t2-typeOf n (TApp t1 bx@(UBox tty2 t2))+typeOf n (TApp t1 (UBox tty2 t2)) | Pi tya f <- typeOf n t1, ty2 <- typeOf n tty2, convertible n tya ty2 = f t2 typeOf n TType = Kind typeOf n t = throw TypeError checkDeclaration :: String -> Term -> IO ()-checkDeclaration x t = catch (evaluate t >> putStrLn "Check") handler+checkDeclaration x t = catch (evaluate t >> putStrLn ("Checked " ++ x ++ ".")) handler where handler (SomeException e) = do- putStrLn $ "Error during checking of " ++ x+ putStrLn $ "Error during checking of " ++ x ++ "." throw e checkRule :: Term -> Term -> Term checkRule lhs rhs | convertible 0 (typeOf 0 lhs) (typeOf 0 rhs) = emptyBox- | otherwise = throw RuleError+ | otherwise = throw $ RuleError (pretty (typeOf 0 lhs)) (pretty (typeOf 0 rhs)) start :: IO UTCTime start = do@@ -137,3 +137,15 @@ t' <- getCurrentTime let total = diffUTCTime t' t putStrLn $ "Stop. Runtime: " ++ show total++-- Pretty printing.++instance Pretty Code where+ pretty = p 0 where+ p n (Var x) = text (show x)+ p n (Con c) = text (show c)+ p n (Lam f) = parens (int n <+> text "=>" <+> p (n + 1) (f (Var n)))+ p n (Pi ty1 ty2) = parens (int n <+> colon <+> p n ty1 <+> text "->" <+> p (n + 1) (ty2 (Var n)))+ p n (App t1 t2) = parens (p n t1 <+> p n t2)+ p n Type = text "Type"+ p n Kind = text "Kind"
Setup.lhs view
@@ -1,3 +1,14 @@ #!/usr/bin/env runhaskell-> import Distribution.Simple-> main = defaultMain++> import Distribution.Simple as Simple+> import Distribution.Simple.LocalBuildInfo+> import Distribution.PackageDescription+> import System.FilePath+> import System.Process+>+> main = defaultMainWithHooks hooks+> where hooks = simpleUserHooks { Simple.runTests = Main.runTests }+>+> runTests :: Args -> Bool -> PackageDescription -> LocalBuildInfo -> IO ()+> runTests _ _ _ lbi = system testprog >> return ()+> where testprog = (buildDir lbi) </> "dedukti-tests" </> "dedukti-tests"
+ Test.hs view
@@ -0,0 +1,90 @@+module Main where++import Test.Framework (defaultMain)+import Test.Framework.Providers.API+import System.FilePath+import System.Directory+import System.Process+import System.Exit+import Control.Exception+import Data.Typeable+import Prelude hiding (catch)++data CheckResult = CheckOk+ -- ^ The property is true as far as we could check it+ | CheckFailed String+ -- ^ The property was not true. The string is the reason.+ | CheckNoExpectedFailure+ -- ^ We expected that a property would fail but it didn't+ | CheckTimedOut+ -- ^ The property timed out during execution+ | CheckException String+ -- ^ The property raised an exception during execution+ deriving Typeable++instance Show CheckResult where+ show CheckOk = "Ok, passed."+ show (CheckFailed err) = "Failed: " ++ err+ show CheckNoExpectedFailure = "No expected failure."+ show CheckTimedOut = "Timed out."+ show (CheckException err) = "Exception: " ++ err++instance Exception CheckResult++data CheckRunning = CheckRunning+ deriving Show++instance TestResultlike CheckRunning CheckResult where+ testSucceeded CheckOk = True+ testSucceeded _ = False++data Expectation = ExpectSuccess | ExpectFailure++data Check = Check { chk_test :: String+ , chk_deps :: [String]+ , chk_expect :: Expectation }++instance Testlike CheckRunning CheckResult Check where+ runTest topts Check{..} = runImprovingIO $ do+ yieldImprovement CheckRunning+ result <- maybeTimeoutImprovingIO (unK $ topt_timeout topts) $+ liftIO (dkrun chk_test chk_deps chk_expect)+ return (result `orElse` CheckTimedOut)++ testTypeName _ = "Type Checking Runs"++dkrun :: FilePath -> [FilePath] -> Expectation -> IO CheckResult+dkrun dk deps exp = do+ cwd <- getCurrentDirectory+ setCurrentDirectory $ cwd </> "t"+ result <- catch (do+ let compile = rawSystem "../dist/build/dedukti/dedukti" [dk <.> "dk"]+ run = rawSystem "../scripts/dkrun" $ (dk <.> "dko") : map (<.> "dko") deps+ test (return ()) fail compile+ case exp of+ ExpectSuccess -> test (return CheckOk) fail run+ ExpectFailure -> test (return CheckNoExpectedFailure) (const $ return CheckOk) run)+ (\e -> return (e :: CheckResult))+ setCurrentDirectory cwd+ return result+ where test s f m = m >>= \code -> case code of+ ExitSuccess -> s+ ExitFailure x -> f x+ fail x = throw $ CheckFailed $ "exit status " ++ show x++check :: TestName -> [String] -> Test+check name deps = Test name (Check name deps ExpectSuccess)++checkFailure :: TestName -> [String] -> Test+checkFailure name deps = Test name (Check name deps ExpectFailure)++-- * Actual tests.++main = defaultMain tests++tests = [ testGroup "Smoke tests"+ [ check "nat" []+ , check "logic" []+ , check "coc" []+ , check "peano" ["logic", "coc"]+ , checkFailure "bug" [] ] ]
dedukti.cabal view
@@ -1,9 +1,9 @@ name: dedukti-version: 1.0.3+version: 1.1.0 author: Mathieu Boespflug maintainer: Mathieu Boespflug <mboes@lix.polytechnique.fr> copyright: © 2009 CNRS - École Polytechnique - INRIA-homepage: http://www.lix.polytechnique.fr/~mboes/src/dedukti.git+homepage: http://www.lix.polytechnique.fr/dedukti synopsis: A type-checker for the λΠ-modulo calculus. description: Dedukti is a proof checker for the λΠ-modulo calculus, a@@ -16,7 +16,7 @@ license: GPL license-file: COPYING cabal-version: >= 1.6.0-build-type: Simple+build-type: Custom tested-with: GHC ==6.10 data-files: t/bug.dk t/coc.dk@@ -36,11 +36,22 @@ doc/fdl.texi doc/references.texi +flag test+ description: Compile test harness (requires test-framework).+ default: False +library+ exposed-modules: Dedukti.Runtime+ build-depends: time >= 1.1+ extensions: DeriveDataTypeable, PatternGuards, FlexibleInstances+ ghc-options: -fwarn-unused-binds -fwarn-unused-imports+ executable dedukti main-is: Dedukti.hs other-modules: Dedukti.Core, Dedukti.Parser,+ Dedukti.Parser.External,+ Dedukti.Parser.Prefix, Dedukti.Pretty, Dedukti.Driver.Interactive, Dedukti.Driver.Batch,@@ -57,18 +68,32 @@ build-depends: base >= 4 && < 5, mtl >= 1.1, containers >= 0.2, directory, filepath, process,- parsec >= 3.0.0, wl-pprint >= 1.0, bytestring >= 0.9.1.0,- haskell-src-exts >= 1.1.0, Stream >= 0.3, text >= 0.3,- hmk >= 0.9- extensions: EmptyDataDecls, PatternGuards, GeneralizedNewtypeDeriving- DeriveDataTypeable, TypeFamilies, LiberalTypeSynonyms,+ bytestring >= 0.9.1.0,+ parsec >= 3.1.0,+ wl-pprint >= 1.0,+ haskell-src-exts >= 1.1.0,+ haskell-src-exts-qq >= 0.1,+ Stream >= 0.3 && < 0.3.2,+ hmk >= 0.9.7,+ stringtable-atom >= 0.0.6+ extensions: EmptyDataDecls, PatternGuards,+ GeneralizedNewtypeDeriving, DeriveDataTypeable,+ TypeFamilies, LiberalTypeSynonyms, FlexibleInstances, FlexibleContexts, OverloadedStrings, RecordWildCards, TypeSynonymInstances, ScopedTypeVariables- MultiParamTypeClasses+ MultiParamTypeClasses,+ TemplateHaskell, QuasiQuotes ghc-options: -fwarn-unused-binds -fwarn-unused-imports -library- exposed-modules: Dedukti.Runtime- build-depends: time >= 1.1- extensions: DeriveDataTypeable, PatternGuards, FlexibleInstances- ghc-options: -fwarn-unused-binds -fwarn-unused-imports++executable dedukti-tests+ main-is: Test.hs+ if !flag(test)+ buildable: False+ else+ buildable: True+ build-depends: directory, filepath, process,+ test-framework >= 0.2 && < 0.3+ extensions: DeriveDataTypeable, MultiParamTypeClasses,+ RecordWildCards+ ghc-options: -fwarn-unused-binds -fwarn-unused-imports
doc/manual.texi.in view
@@ -66,8 +66,8 @@ @menu * Overview:: The general architecture. * Installation:: How to install the Dedukti system.-* Dedukti syntax:: The input language for Dedukti.-* Invoking dedukti:: The compiler.+* Dedukti syntax:: The input language for Dedukti.+* Invoking dedukti:: The compiler. * Invoking dkrun:: Executing the proof checks. * References:: Bibliographic references. * Copying this manual:: How you can copy and share this manual.@@ -113,14 +113,32 @@ @cindex Cabal @cindex Hackage Dedukti uses the Cabal architecture for building and packaging-applications and libraries.+applications and libraries. Regardless of the method of installation+chosen, one needs to satisfy manually dependency on system libraries,+such as the PCRE library. It might also be necessary to install+development version of these packages, depending on your distribution. @menu+* Requirements:: Required versions for compiler and libraries. * Local install:: Installing in your home directory. * Global install:: Installing in the system directories. * Building the documentation:: How to build the documentation. @end menu +@node Requirements+@section Requirements+@cindex system libaries+@cindex Haskell compiler++Dedukti requires the Glorious Haskell Compiler (GHC) versions 6.10 and+above to compile. Note that GHC 6.12.1 has a bug preventing a dependency+of Dedukti to compile properly, so ulterior revisions in the 6.12 series+are recommended.++The PCRE library 7.0 or above, including the header files, must be+present on the system before proceeding to @ref{Local install} or+@ref{Global install}.+ @node Local install @section Installing Dedukti locally @@ -208,9 +226,11 @@ @chapter Dedukti syntax @menu-* Syntax overview:: An informal description of input files.-* Scoping rules:: The scope of declarations and rules.-* Grammar:: A formal specification of the syntax.+* Syntax overview:: An informal description of input files.+* Pragmas:: Use source pragmas for compiler hints.+* Scoping rules:: The scope of declarations and rules.+* Grammar:: A formal specification of the syntax.+* Prefix notation grammar:: A formal specification of an alternative syntax. @end menu @node Syntax overview@@ -349,6 +369,30 @@ @end example @end quotation +@node Pragmas+@section Pragmas+@cindex pragmas++Multi-line comments whose first non-blank character following the+comment delimiter is a hash ``@verb{.#.}'' symbol are treated specially+by Dedukti. These comments are considered @dfn{pragmas}, providing hints+to the compilation process. The syntax of pragmas is as follows.+Following the hash sign is the name of the pragma, in upper case. All+remaining tokens until the closing comment delimiter are arguments to+the pragma.++Currently, the only supported pragma is the @code{FORMAT} pragma,+expliciting the syntax of the source file in which it occurs. This+pragma may only appear on the first line of the source file, as in the+following:++@example+(; # FORMAT prefix ;)+@end example++This line says that the source file is in prefix notation (@pxref{Prefix+syntax}).+ @node Scoping rules @section Scoping rules @cindex scoping@@ -379,11 +423,11 @@ toplevel ::= declaration toplevel | rule toplevel | eof-binding ::= id : term-declaration ::= id ":" term "."+binding ::= id ":" term+declaration ::= binding "." domain ::= id ":" applicative | applicative-sort ::= Type+sort ::= "Type" term ::= domain "->" term | domain "=>" term | applicative@@ -392,19 +436,54 @@ | "(" term ")" applicative ::= simple | applicative simple-rule ::= env term "-->" term+rule ::= env term "-->" term "." env ::= "[]" | "[" env2 "]" env2 ::= binding | binding "," env2 @end example +@node Prefix notation grammar+@section Axioms and rules in prefix notation+@cindex grammar+@cindex syntax+@cindex prefix notation+@cindex polish notation++For the rationale behind prefix notation, see @ref{Prefix syntax}++Source files in prefix notation consist in a string of whitespace+delimited tokens, as is the case for the human-readable format defined+above. Unlike that format, however, there is no syntax for comments,+though a @code{FORMAT} pragma may appear on the first line. Any token+that is not one of the literals appearing in the grammar below is+considered an identifier. Identifiers are period separated lists of+characters, everything before the last period specifying the module+qualifier for an identifier.++@example+qid ::= id.id | id+toplevel ::= binding toplevel+ | rule toplevel+ | eof+binding ::= ":" id term+sort ::= "Type"+term ::= "->" binding term+ | "=>" binding term+ | "@@" term term+ | qid+rule ::= "-->" env term term+env ::= "[]"+ | "," binding env+@end example+ @node Invoking dedukti @chapter Invoking @command{dedukti} @menu * One-shot mode:: Compiling one source file at a time. * Batch mode:: Let Dedukti figure out what needs to be compiled.+* Prefix syntax:: Input source files to Dedukti in alternative syntax. @end menu @node One-shot mode@@ -441,7 +520,7 @@ @node Batch mode @section Batch mode -Compile in batch mode by passing the @code{--make} flag to+Compile in batch mode by passing the @code{--make} option to @command{dedukti}. In this mode, dependencies of the file given in argument will be compiled first, though after the dependencies of the dependencies have been compiled, etc. Those dependencies that do not@@ -453,6 +532,45 @@ for the module given as argument and its dependencies. Compiling to native code often yields much better performance during checking. @xref{Invoking dkrun}.++@node Prefix syntax+@section Prefix syntax+@cindex prefix notation+@cindex polish notation+@cindex syntax+@cindex source files+@cindex parsing++Because Dedukti may be used as the backend proof checker for a number of+frontend mechanized translators, proof assistants and other interactive+environments, in many cases the input to Dedukti is not human crafted+but mechanically generated. Dedukti therefore accepts source files in an+alternative syntax that can be parsed much more efficiently, inspired by+Jan Łukasiewicz' polish notation for sentential+logic@footnote{@uref{http://en.wikipedia.org/wiki/Polish_notation}}. The+syntax uses prefix notation for operators, much like Lisp, but unlike+Lisp, arities for all the operators are fixed and known in advance,+therefore no parentheses are need around subterms.++This syntax for Dedukti axioms and rules is the preferred target syntax+for automated tools that produce Dedukti code. Parsing time is at least+an order of magnitude smaller for source files in prefix notation.+Dedukti can automatically recognize the syntax of the source file if the+first line of the source file is a @code{FORMAT} pragma+(@pxref{Pragmas}). It is also possible to force a particular format+using the following command line options:++@table @option+@item -fexternal+Force recognizing input as (human-readable) external format.++@item -fprefix-notation+Force recognizing input as (fast) prefix format.++@end table++See @ref{Prefix notation grammar} for the lexical and grammatical+structure of this syntax. @node Invoking dkrun @chapter Invoking @command{dkrun}
doc/mkfile view
@@ -9,7 +9,7 @@ m4 $prereq | makeinfo - default:QV:- echo 'Please specify one of "html" or "pdf" as targets.'+ echo 'Please specify one of "html", "pdf" or "info" as targets.' exit 1 pdf:V: manual.pdf
scripts/dkrun view
@@ -2,7 +2,7 @@ if [ -z $* ] then- echo "Usage: dkrun module.euo [DEPENDENCY]..." 1>&2+ echo "Usage: dkrun module.dko [DEPENDENCY]..." 1>&2 echo " Where all dependent modules must be listed explicitly," 1>&2 echo " after the module to typecheck." 1>&2 exit 1