dedukti 1.1.0 → 1.1.1
raw patch · 5 files changed
+72/−32 lines, 5 files
Files
- Dedukti/CodeGen/Exts.hs +27/−27
- Dedukti/Parser/Interface.hs +14/−0
- Test.hs +1/−1
- dedukti.cabal +6/−1
- doc/manual.texi.in +24/−3
Dedukti/CodeGen/Exts.hs view
@@ -45,32 +45,32 @@ emit rs@(RS x ty rules) = Rec x (length rules) (function rs : def_ty : def_box : zipWith defs_rule [0..] rules) 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) |]+ 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 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) |]]+ 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 |]+ body = Hs.letE decls [$hs| main |]+ in [$dec| ((rule)) = $body |] coalesce records = Bundle $ concatMap rec_code records ++ [main]- where main = [dec| main = $checks |]+ where main = [$dec| main = $checks |] checks = Hs.Do (concatMap rules records ++ map declaration records) declaration r = let desc = Hs.strE $ show $ pretty $ unqualify $ rec_name r- in Hs.qualStmt [hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |]+ in Hs.qualStmt [$hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |] rules (Rec _ 0 _) = [] rules (Rec x nr _) = 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 |]]+ 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 |]]+ ++ [Hs.qualStmt [$hs| putStrLn $finishmsg |]] serialize mod deps (Bundle decls) = B.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $@@ -105,7 +105,7 @@ where n = Rule.arity (head rs) 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+ 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) @@ -118,15 +118,15 @@ 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') |])+ [$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.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+ (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) |]+constant c = [$hs| Con $(Hs.strE $ show $ pretty c) |] pattern :: Em Env -> Em Expr -> Hs.Pat pattern env (Var x _) | x `isin` env = Hs.pvar (varName x)@@ -141,30 +141,30 @@ -- | Turn an expression into object code with types erased. code :: Em Expr -> Hs.Exp code (Var x _) = var x-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 |]+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 _) = 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 |]+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 |] typedAbstraction c b t = case b of- x ::: ty -> [hs| $c $(dom ty) (\((box)) -> $ran) |]+ 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) |]+ 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) |]+ then term ty else [$hs| sbox $(term ty) Type $(code ty) |] varName :: Id Record -> Hs.Name varName = Hs.name . xencode . unqualify
+ Dedukti/Parser/Interface.hs view
@@ -0,0 +1,14 @@+-- |+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA+-- License : GPL+--+-- Parser for interface files.++module Dedukti.Parser.Interface (parse) where++import Dedukti.Module+import qualified Data.ByteString.Lazy.Char8 as B++parse :: FilePath -> B.ByteString -> [Qid]+parse _ = map qid . B.lines+
Test.hs view
@@ -84,7 +84,7 @@ tests = [ testGroup "Smoke tests" [ check "nat" []- , check "logic" [] , check "coc" []+ , check "logic" ["coc"] , check "peano" ["logic", "coc"] , checkFailure "bug" [] ] ]
dedukti.cabal view
@@ -1,5 +1,5 @@ name: dedukti-version: 1.1.0+version: 1.1.1 author: Mathieu Boespflug maintainer: Mathieu Boespflug <mboes@lix.polytechnique.fr> copyright: © 2009 CNRS - École Polytechnique - INRIA@@ -40,6 +40,10 @@ description: Compile test harness (requires test-framework). default: False +source-repository head+ type: git+ location: git://github.com/mboes/dedukti+ library exposed-modules: Dedukti.Runtime build-depends: time >= 1.1@@ -52,6 +56,7 @@ Dedukti.Parser, Dedukti.Parser.External, Dedukti.Parser.Prefix,+ Dedukti.Parser.Interface, Dedukti.Pretty, Dedukti.Driver.Interactive, Dedukti.Driver.Batch,
doc/manual.texi.in view
@@ -123,6 +123,7 @@ * Local install:: Installing in your home directory. * Global install:: Installing in the system directories. * Building the documentation:: How to build the documentation.+* Smoke tests:: Running smoke tests (for developers) @end menu @node Requirements@@ -135,9 +136,11 @@ 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}.+The PCRE library version 7.0 or above, including the header files, must+be present on the system before proceeding to @ref{Local install} or+@ref{Global install}. Dedukti has an indirect dependency on @code{happy+>= 1.17}. You should ensure that the @command{happy} command is in a+location mentioned in your @env{PATH}. @node Local install @section Installing Dedukti locally@@ -221,6 +224,24 @@ folder, depending on the type of installation. You will also need a POSIX compatible environment to build the documentation, including the @command{m4} command to preprocess the texinfo source.++@node Smoke tests+@section Smoke tests++The package description file for Dedukti declares a @code{test} flag.+Enabling this flag instructs Cabal to build the test harness as well.+The test harness currently contains a handful of smoke tests useful for+sanity checking of new patches to Dedukti, for instance.++In a Dedukti source directory, one can perform smoke tests as follows:++@example+$ cabal configure -f test+$ cabal build+$ cabal test+@end example++New changesets should not be submitted unless all tests pass. @node Dedukti syntax @chapter Dedukti syntax