Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge branch 'master' of https://github.com/mpu/dedukti

Conflicts:
	Dedukti/Runtime.hs
  • Loading branch information...
commit cd91c35570775bd6be83c766d4c9640986a50fff 2 parents 0a3b2a9 + 55753a6
@mboes authored
View
2  .gitignore
@@ -0,0 +1,2 @@
+*.sw[po]
+dist
View
21 Dedukti/Analysis/Rule.hs
@@ -12,7 +12,8 @@ import Dedukti.DkM
import qualified Dedukti.Rule as Rule
import Dedukti.Pretty ()
import Text.PrettyPrint.Leijen hiding (group)
-import Data.List (group, sort)
+import Data.List (group, groupBy, sort)
+import Data.Function (on)
newtype NonContiguousRules = NonContiguousRules Qid
@@ -32,6 +33,24 @@ checkOrdering rules = do
mapM_ (\x -> when (length x > 1) (throw $ NonContiguousRules (head x))) $
group $ sort $ map head $ group $ map Rule.headConstant rules
+newtype BadArity = BadArity Qid
+ deriving (Eq, Ord, Typeable)
+
+instance Show BadArity where
+ show (BadArity id) =
+ show (text "Some rules for" <+> pretty id <+> text "have different arities.")
+
+instance Exception BadArity
+
+-- | All rules for one constant must have the same arity.
+checkArity :: [TyRule Qid a] -> DkM ()
+checkArity rules = do
+ say Verbose $ text "Checking arity of rules ..."
+ mapM_ (\(l:ls) -> chk (Rule.headConstant l) (napps (Rule.head l)) ls)
+ $ groupBy ((==) `on` Rule.headConstant) rules
+ where chk id n l = when (or (map ((/=) n . napps . Rule.head) l)) (throw $ BadArity id)
+ napps e = unapply e (\_ x _ -> length x)
+
newtype BadPattern = BadPattern [Qid]
deriving (Eq, Ord, Typeable)
View
8 Dedukti/Analysis/Scope.hs
@@ -14,6 +14,7 @@ import qualified Dedukti.Rule as Rule
import Dedukti.Pretty ()
import Dedukti.DkM
import Data.List (sort, group)
+import qualified Data.Traversable as T
import qualified Data.Map as Map
import qualified StringTable.AtomSet as AtomSet
@@ -71,7 +72,9 @@ checkScopes env (decls, rules) = do
(AtomSet.singleton (qid_stem qid)) env
notmem qid env = maybe False (AtomSet.notMember (qid_stem qid))
(Map.lookup (qid_qualifier qid) env)
- chkBinding env (L x) = return $ ins x env
+ chkBinding env (L x ty) = do
+ chkExpr env `T.mapM` ty
+ return $ ins x env
chkBinding env (x ::: ty) = do
chkExpr env ty
return $ ins x env
@@ -87,7 +90,8 @@ checkScopes env (decls, rules) = do
chkExpr env t@(V x _) = do
when (x `notmem` env) (throw $ ScopeError x)
return t
- chkExpr env (B (L x) t _) = do
+ chkExpr env (B (L x ty) t _) = do
+ chkExpr env `T.mapM` ty
chkExpr (ins x env) t
chkExpr env (B (x ::: ty) t _) = do
chkExpr env ty
View
56 Dedukti/CodeGen/Exts.hs
@@ -43,16 +43,16 @@ instance CodeGen Record where
data Bundle Record = Bundle [Hs.Decl]
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"))
+ Rec x (length rules) (def_ty : function rs : def_t : zipWith defs_rule [0..] rules)
+ where [tyname, tname, cname] = map (varName . (x .$)) ["ty", "t", "c"]
def_ty = [dec| ((tyname)) = $(code ty) |]
- def_box = [dec| ((boxname)) = bbox $(term ty) $(Hs.var tyname) $(var x) |]
+ def_t = [dec| ((tname)) = bbox $(term ty) $(Hs.var tyname) $(Hs.var cname) |]
-- 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")
+ ruleCheck = let rule_box = varName (qid "rule" .$ "t")
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))
@@ -63,7 +63,7 @@ instance CodeGen Record where
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 .$ "t")) |]
rules (Rec _ 0 _) = []
rules (Rec x nr _) =
let startmsg = Hs.strE $ "Starting rule " ++ show (pretty (unqualify x)) ++ "."
@@ -73,7 +73,7 @@ instance CodeGen Record where
++ [Hs.qualStmt [hs| putStrLn $finishmsg |]]
serialize mod deps (Bundle decls) =
- B.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $
+ B.pack $ prettyPrintWithMode defaultMode {layout = PPOffsideRule} $
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
@@ -100,8 +100,8 @@ xencode qid =
| otherwise = B.singleton x
function :: Em RuleSet -> Hs.Decl
-function (RS x _ []) = Hs.nameBind (*) (varName x) (constant x)
-function (RS x _ rs) = Hs.sfun (*) (varName x) [] (Hs.UnGuardedRhs rhs) (Hs.binds [f])
+function (RS x _ []) = Hs.nameBind (*) (varName (x .$ "c")) (constant x)
+function (RS x _ rs) = Hs.sfun (*) (varName (x .$ "c")) [] (Hs.UnGuardedRhs rhs) (Hs.binds [f])
where n = Rule.arity (head rs)
pats = Stream.take n variables
occs = map Hs.var pats
@@ -117,9 +117,9 @@ clause rule =
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| reflect (convertible 0 $(var x) $(var x')) |])
- qids = Stream.unfold (\i -> ((qid $ B.pack $ show i) .$ "fresh", i + 1)) 0
+ where guards = let tt = Hs.pApp (Hs.name "()") []
+ in map (\(x, x') -> Hs.Generator (*) tt [hs| convertible 0 $(var (x .$ "c")) $(var (x' .$ "c")) |])
+ qids = Stream.unfold (\i -> ((qid $ B.pack $ show i) .$ "fresh" .$ "c", i + 1)) 0
defaultClause :: Id Record -> Int -> Hs.Match
defaultClause x n =
@@ -129,7 +129,7 @@ defaultClause x n =
constant c = [hs| Con $(Hs.strE $ show $ pretty c) |]
pattern :: Em Env -> Em Expr -> Hs.Pat
-pattern env (V x _) | x `isin` env = Hs.pvar (varName x)
+pattern env (V x _) | x `isin` env = Hs.pvar (varName (x .$ "c"))
pattern env expr = unapply expr (\(V x _) xs _ -> primAppsP x (map (pattern env) xs))
-- | Build a pattern matching constant.
@@ -139,26 +139,32 @@ primAppsP c = foldl' primAppP (primConP c)
-- | Turn an expression into object code with types erased.
code :: Em Expr -> Hs.Exp
-code (B (L x) t _) | n <- varName x = [hs| Lam (\((n)) -> $(code t)) |]
-code (B (x ::: ty) t _) | n <- varName x = [hs| Pi $(code ty) (\((n)) -> $(code t)) |]
-code (B (x := t1) t2 _) | n <- varName x = [hs| let ((n)) = $(code t1) in $(code t2) |]
+code (V x _) = var (x .$ "c")
+code (B (L x _) t _) | n <- varName (x .$ "c") = [hs| Lam (\((n)) -> $(code t)) |]
+code (B (x ::: ty) t _) | n <- varName (x .$ "c") = [hs| Pi $(code ty) (\((n)) -> $(code t)) |]
+code (B (x := t1) t2 _) | n <- varName (x .$ "c") = [hs| let ((n)) = $(code t1) in $(code t2) |]
code (A t1 t2 _) = [hs| ap $(code t1) $(code t2) |]
-code (V x _) = var x
code Type = [hs| Type |]
-- | Turn a term into its Haskell representation, including all types.
term :: Em Expr -> Hs.Exp
-term (B (L x) t _) | n <- varName (x .$ "box") = [hs| TLam (\((n)) -> $(term t)) |]
-term (B (x ::: ty) t _) = typedAbstraction [hs| TPi |] x ty (term t)
-term (B (x := t1) t2 _) | n <- varName (x .$ "box") = [hs| TLet $(term t1) (\((n)) -> $(term t2)) |]
-term (A t1 t2 _) = [hs| TApp $(term t1) $(term t2) |]
-term (V x _) = var (x .$ "box")
+term (V x _) = var (x .$ "t")
+term (B (L x ty) t _) = lambdaAbstraction x ty (term t)
+term (B (x ::: ty) t _) = typedAbstraction x ty (term t)
+term (B (x := t1) t2 _) = letBinding x t1 (term t2)
+term (A t1 t2 _) = [hs| TApp $(term t1) (Pair $(term t2) $(code t2)) |]
term Type = [hs| TType |]
-typedAbstraction c x ty t = [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 |]
+letBinding x t1 t = [hs| TLet (Pair $(term t1) $(code t1)) (\(Pair ((xt)) ((xc))) -> $t) |]
+ where (xt, xc) = (varName (x .$ "t"), varName (x .$ "c"))
+
+lambdaAbstraction x ty t = [hs| TLam $tyterm (\(Pair ((xt)) ((xc))) -> $t) |]
+ where (xt, xc) = (varName (x .$ "t"), varName (x .$ "c"))
+ tyterm = case ty of Nothing -> [hs| Nothing |]
+ Just ty -> [hs| Just $ sbox $(term ty) Type $(code ty) |]
+
+typedAbstraction x ty t = [hs| TPi $(dom ty) (\(Pair ((xt)) ((xc))) -> $t) |]
+ where (xt, xc) = (varName (x .$ "t"), varName (x .$ "c"))
dom ty = if isVariable ty
then term ty else [hs| sbox $(term ty) Type $(code ty) |]
View
40 Dedukti/Core.hs
@@ -30,6 +30,7 @@ module Dedukti.Core
import Control.Applicative
import Control.Monad.Identity
import Control.Monad.State
+import qualified Data.Traversable as T
import qualified Data.Map as Map
@@ -44,9 +45,9 @@ infix 2 :::
-- | A type decorating a variable, a type on its own, or an expression
-- defining a variable
-data Binding id a = L id -- ^ Lambda binding
- | id ::: Expr id a -- ^ Pi binding
- | id := Expr id a -- ^ Let binding
+data Binding id a = L id (Maybe (Expr id a)) -- ^ Lambda binding
+ | id ::: Expr id a -- ^ Pi binding
+ | id := Expr id a -- ^ Let binding
deriving (Eq, Ord, Show)
-- | A rewrite rule.
@@ -82,6 +83,7 @@ type family Id t
type family A t
type instance Id [t] = Id t
+type instance Id (Maybe t) = Id t
type instance Id (Module id a) = id
type instance Id (Binding id a) = id
type instance Id (Rule id a) = id
@@ -90,6 +92,7 @@ type instance Id (RuleSet id a) = id
type instance Id (Expr id a) = id
type instance A [t] = A t
+type instance A (Maybe t) = A t
type instance A (Module id a) = a
type instance A (Binding id a) = a
type instance A (Rule id a) = a
@@ -98,13 +101,13 @@ type instance A (RuleSet id a) = a
type instance A (Expr id a) = a
bind_name :: Binding id a -> id
-bind_name (L x) = x
+bind_name (L x _) = x
bind_name (x ::: _) = x
bind_name (x := _) = x
-- | A lambda or Pi abstraction.
isAbstraction :: Expr id a -> Bool
-isAbstraction (B (L _) _ _) = True
+isAbstraction (B (L _ _) _ _) = True
isAbstraction (B (_ ::: _) _ _) = True
isAbstraction _ = False
@@ -186,7 +189,6 @@ abstract :: [Binding id a] -> Expr id a -> [a] -> Expr id a
abstract [] t _ = t
abstract (b:bs) t (a:annots) = B b (abstract bs t annots) %% a
abstract bs _ as = error $ "abstract: " ++ show (length bs) ++ " bindings but only "
- ++ show (length as) ++ " annotations."
unabstract :: Expr id a -> ([Binding id a] -> Expr id a -> [a] -> r) -> r
unabstract (B b t a) k = unabstract t (\bs t' as -> k (b:bs) t' (a:as))
@@ -205,7 +207,6 @@ unapply t k = go [] [] t where
go xs as (A t1 t2 a) = go (t2:xs) (a:as) t1
go xs as t = k t xs as
-
class Ord (Id t) => Transform t where
-- | Effectful bottom-up transformation on terms. A default for
-- 'transformM' in terms of 'descendM' for all instances other than
@@ -218,17 +219,17 @@ class Ord (Id t) => Transform t where
instance Ord id => Transform (Module id a) where
descendM f (decls, rules) =
- return (,) `ap` mapM (descendM f) decls `ap` mapM (descendM f) rules
+ return (,) `ap` descendM f decls `ap` descendM f rules
instance Ord id => Transform (Binding id a) where
- descendM f (L x) = return (L x)
+ descendM f (L x t) = return (L x) `ap` T.mapM f t
descendM f (x ::: ty) = return (x :::) `ap` f ty
descendM f (x := t) = return (x :=) `ap` f t
instance Ord id => Transform (TyRule id a) where
descendM f (env :@ rule) =
- return (:@) `ap` (return fromBindings `ap` mapM (descendM f) (env_bindings env)) `ap`
- descendM f rule
+ return (:@) `ap` (return fromBindings `ap` descendM f (env_bindings env))
+ `ap` descendM f rule
instance Ord id => Transform (Rule id a) where
descendM f (lhs :--> rhs) = return (:-->) `ap` f lhs `ap` f rhs
@@ -238,18 +239,17 @@ instance Ord id => Transform (RuleSet id a) where
return RS `ap` return rs_name `ap` f rs_type `ap` descendM f rs_rules
instance Ord id => Transform (Expr id a) where
- transformM f = f <=< descendM (transformM f)
-
- descendM f (B b t a) = do
- t' <- f t
- b' <- descendM f b
- return $ B b' t' a
- descendM f (A t1 t2 a) = do
- return A `ap` f t1 `ap` f t2 `ap` return a
+ transformM f = descendM (transformM f) >=> f
+
+ descendM f (B b t a) = return B `ap` descendM f b `ap` f t `ap` return a
+ descendM f (A t1 t2 a) = return A `ap` f t1 `ap` f t2 `ap` return a
descendM f t = return t
instance Transform t => Transform [t] where
- descendM f = mapM (descendM f)
+ descendM f = T.mapM (descendM f)
+
+instance Transform a => Transform (Maybe a) where
+ descendM f = T.mapM (descendM f)
-- | Pure bottom-up transformation on terms.
transform :: Transform t => (Expr (Id t) (A t) -> Expr (Id t) (A t)) -> t -> t
View
5 Dedukti/Driver/Compile.hs
@@ -36,8 +36,8 @@ selfQualify mod rsets = let defs = Set.fromList (map rs_name rsets)
(map (\RS{..} -> RS{rs_name = qualify mod rs_name, ..}) rsets)
where f defs (V x a) | Nothing <- provenance x
, x `Set.member` defs = V (qualify mod x) %% a
- f defs (B (L x) t a) =
- B (L x) (f (Set.delete x defs) t) %% a
+ f defs (B (L x ty) t a) =
+ B (L x (f defs `fmap` ty)) (f (Set.delete x defs) t) %% a
f defs (B (x ::: ty) t a) =
B (x ::: f defs ty) (f (Set.delete x defs) t) %% a
f defs t = descend (f defs) (t :: Pa Expr)
@@ -87,6 +87,7 @@ compileAST mod src@(decls, rules) = do
{-# SCC "check/uniqueness" #-} checkUniqueness src
{-# SCC "check/scopes" #-} checkScopes extdecls src
{-# SCC "check/ordering" #-} Rule.checkOrdering rules
+ {-# SCC "check/arity" #-} Rule.checkArity rules
say Verbose $ text "Checking well formation of rule heads ..."
{-# SCC "check/heads" #-} mapM_ Rule.checkHead rules
say Verbose $ text "Compiling" <+> text (show mod) <+> text "..."
View
35 Dedukti/Parser/External.hs
@@ -95,9 +95,9 @@ ident = qid . B.pack <$> identifier
-- > | eof
toplevel =
whiteSpace *>
- ( (rule *> toplevel) -- Rules are accumulated by side-effect.
- <|> ((:) <$> declaration <*> toplevel)
- <|> (eof *> return []))
+ choice [ rule *> toplevel -- Rules are accumulated by side effect.
+ , (:) <$> declaration <*> toplevel
+ , eof *> return [] ]
-- | Binding construct.
--
@@ -111,13 +111,14 @@ binding = ((:::) <$> ident <* reservedOp ":" <*> term)
declaration = (binding <* dot)
<?> "declaration"
--- | Left hand side of an abstraction or a product.
+-- | Left hand side of a product or a lambda.
--
--- > domain ::= id ":" applicative
--- > | applicative
-domain = ( ((:::) <$> try (ident <* reservedOp ":") <*> applicative)
- <|> ((qid "hole" .$ "parser" :::) <$> applicative))
- <?> "domain"
+-- > domain ::= [id ":"] applicative "->"
+-- > | id [":" applicative] "=>"
+domain = try (lambda <* reservedOp "=>") <|> try (pi <* reservedOp "->")
+ where lambda = L <$> ident <*> optionMaybe (reservedOp ":" *> applicative) <?> "lambda"
+ pi = (:::) <$> (try (ident <* reservedOp ":") <|> return (qid "hole" .$ "parser"))
+ <*> applicative <?> "pi"
-- |
-- > sort ::= "Type"
@@ -125,20 +126,12 @@ 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.
+-- We first try to parse the term as a pi or lambda binding. If it fails,
+-- we parse the rest as an applicative.
--
--- > term ::= domain "->" term
--- > | domain "=>" term
+-- > term ::= domain term
-- > | applicative
-term = do
- d@(x ::: ty) <- domain
- choice [ pi d <?> "pi"
- , lambda d <?> "lambda"
- , return ty ]
- where pi d = B d <$ reservedOp "->" <*> term <%%> nann
- lambda (x ::: _) = B (L x) <$ reservedOp "=>" <*> term <%%> nann
+term = (B <$> domain <*> term <%%> nann) <|> applicative
-- | Constituents of an applicative form.
--
View
6 Dedukti/Parser/Prefix.hs
@@ -47,10 +47,10 @@ step "," (Binding x : Env y : xs) = Env (x:y) : xs
step "[]" xs = Env [] : xs
-- expressions
-step "=>" (Binding (x ::: _) : Expr t : xs) = Expr (B (L x) t %% nann) : xs
+step "=>" (Binding (x ::: ty) : Expr t : xs) = Expr (B (L x (Just ty)) t %% nann) : xs
step "->" (Binding (x ::: ty) : Expr t : xs) = Expr (B (x ::: ty) t %% nann) : xs
-step "@" (Expr t1 : Expr t2 : xs) = Expr (A t1 t2 %% nann) : xs
-step "Type" xs = Expr Type : xs
+step "@" (Expr t1 : Expr t2 : xs) = Expr (A t1 t2 %% 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 (V (qualify mod (qid var)) %% nann) : xs
View
4 Dedukti/Pretty.hs
@@ -18,14 +18,14 @@ import qualified Data.ByteString.Lazy.Char8 as B
textB = text . B.unpack
instance Pretty id => Pretty (Binding id a) where
- pretty (L x) = pretty x
+ pretty (L x ty) = pretty x <+> char ':' <+> pretty ty
pretty (x ::: ty) = pretty x <+> char ':' <+> pretty ty
pretty (x := t) = pretty x <+> text ":=" <+> pretty t
prettyList = vcat . map (\x -> pretty x <> dot)
instance Pretty id => Pretty (Expr id a) where
- pretty (B (L x) t _) = pretty x <+> text "=>" <+> pretty t
+ pretty (B (L x ty) t _) = pretty x <> char ':' <> parens (pretty ty) <+> text "=>" <+> pretty t
pretty (B (x ::: dom@(B _ _ _)) ran _) =
pretty x <+> char ':' <+> parens (pretty dom) <+> text "->" <+> pretty ran
pretty (B (x ::: dom) ran _) =
View
94 Dedukti/Runtime.hs
@@ -18,10 +18,9 @@
-- inference function.
module Dedukti.Runtime
- ( Code(..), Term(..), ap
- , reflect
+ ( Code(..), Term(..), Pair(..), ap
, convertible
- , bbox, sbox, obj
+ , bbox, sbox
, start, stop
, checkDeclaration
, checkRule) where
@@ -71,34 +70,26 @@ data Code = Var !Int
| Kind
deriving (Eq, Show)
-data Term = TLam !(Term -> Term)
- | TPi !Term !(Term -> Term)
- | TLet !Term !(Term -> Term)
- | TApp !Term !Term
+instance Eq (Code -> Code)
+
+data Term = TLam !(Maybe Term) !(Pair -> Term)
+ | TLet !Pair !(Pair -> Term)
+ | TPi !Term !(Pair -> Term)
+ | TApp !Term !Pair
| TType
- | Box Code Code
+ | Box Code Code -- For typechecking purposes, not user generated.
deriving Show
-instance Eq (Code -> Code)
+data Pair = Pair Term Code
+ deriving Show
ap :: Code -> Code -> Code
ap (Lam f) t = f t
ap t1 t2 = App t1 t2
-obj :: Term -> Code
-obj (Box _ obj) = obj
-
--- | In the runtime, predicates are represented in half CPS, taking a success
--- continuation but throw an exception on failure.
-type Prop = forall r. r -> r
-
--- | Check that a predicate really evaluates to True.
-reflect :: Prop -> Bool
-reflect k | r <- k True = r
-
-convertible :: Int -> Code -> Code -> Prop
-convertible n t1 t2 k | conv n t1 t2 = k
- | otherwise = throw $ ConvError (prettyOpen n t1) (prettyOpen n t2)
+convertible :: Int -> Code -> Code -> ()
+convertible n t1 t2 | conv n t1 t2 = ()
+ | otherwise = throw $ ConvError (prettyCode n t1) (prettyCode n t2)
where conv n (Var x) (Var x') = x == x'
conv n (Con c) (Con c') = c == c'
conv n (Lam t) (Lam t') =
@@ -111,9 +102,6 @@ convertible n t1 t2 k | conv n t1 t2 = k
conv n Kind Kind = True
conv n _ _ = False
--- | A box in which we didn't put anything.
-emptyBox = Box undefined undefined
-
bbox, sbox :: Term -> Code -> Code -> Term
-- | A big box holds terms of sort Type or Kind
@@ -126,56 +114,58 @@ box sorts ty ty_code obj_code
| synth 0 ty `elem` sorts = Box ty_code obj_code
| otherwise = throw SortError
-check :: Int -> Term -> Code -> Prop
-check n (TLam f) (Pi a f') = check (n + 1) (f (Box a (Var n))) (f' (Var n))
-check n (TLet t1 f) ty | ty1 <- synth n t1 = check (n + 1) (f (Box ty1 (Var n))) ty
+mkpair n ty = Pair (Box ty (Var n)) (Var n)
+
+check :: Int -> Term -> Code -> ()
+check n (TLam _ f) (Pi a f') = check (n + 1) (f (mkpair n a)) (f' (Var n))
+check n (TLet (Pair t tc) f) ty
+ | tyt <- synth n t = check (n + 1) (f (Pair (Box tyt tc) tc)) ty
check n t ty = convertible n (synth n t) ty
synth :: Int -> Term -> Code
synth n (Box ty _) = ty
-synth n (TPi (Box Type tya) f) = synth (n + 1) (f (Box tya (Var n)))
-synth n (TApp t1 (Box ty2 t2))
- | Pi tya f <- synth n t1,
- reflect (convertible n tya ty2) = f t2
+synth n (TPi (Box Type tya) f) = synth (n + 1) (f (mkpair n tya))
+synth n (TApp t1 (Pair t2 c2))
+ | Pi tya f <- synth n t1
+ , () <- check n t2 tya = f c2
synth n TType = Kind
+synth n (TLam (Just (Box Type ty)) f) =
+ Pi ty (\xc -> synth (n + 1) (f (Pair (Box ty xc) xc)))
synth n t = throw SynthError
-checkDeclaration :: String -> Term -> IO ()
+checkDeclaration :: String -> a -> IO ()
checkDeclaration x t = catch (evaluate t >> putStrLn ("Checked " ++ x ++ ".")) handler
where handler (SomeException e) = do
putStrLn $ "Error during checking of " ++ x ++ "."
throw e
-checkRule :: Term -> Term -> Term
-checkRule lhs rhs | ty <- synth 0 lhs, reflect (check 0 rhs ty) = emptyBox
+checkRule :: Term -> Term -> ()
+checkRule lhs rhs | ty <- synth 0 lhs, () <- check 0 rhs ty = ()
| otherwise = throw $ RuleError
+-- Function utilites.
+
start :: IO UTCTime
start = do
putStrLn "Start."
getCurrentTime
-
stop :: UTCTime -> IO ()
stop t = do
t' <- getCurrentTime
let total = diffUTCTime t' t
putStrLn $ "Stop. Runtime: " ++ show total
- -- Use Posix exitImmediately rather than System.Exit to really exit GHCi.
- exitImmediately ExitSuccess
+ exitImmediately ExitSuccess -- Use Posix exitImmediately rather than System.Exit to really exit GHCi.
-- Pretty printing.
-instance Pretty Code where
- pretty = prettyOpen 0
-
-prettyOpen n (Var x) = text (show x)
-prettyOpen n (Con c) = text (show c)
-prettyOpen n (Lam f) =
- parens (int n <+> text "=>" <+> prettyOpen (n + 1) (f (Var n)))
-prettyOpen n (Pi ty1 ty2) =
- parens (int n <+> colon <+> prettyOpen n ty1 <+> text "->" <+> prettyOpen (n + 1) (ty2 (Var n)))
-prettyOpen n (App t1 t2) =
- parens (prettyOpen n t1 <+> prettyOpen n t2)
-prettyOpen n Type = text "Type"
-prettyOpen n Kind = text "Kind"
+prettyCode n (Var x) = text (show x)
+prettyCode n (Con c) = text (show c)
+prettyCode n (Lam f) =
+ parens (int n <+> text "=>" <+> prettyCode (n + 1) (f (Var n)))
+prettyCode n (Pi ty1 ty2) =
+ parens (int n <+> colon <+> prettyCode n ty1 <+> text "->" <+> prettyCode (n + 1) (ty2 (Var n)))
+prettyCode n (App t1 t2) =
+ parens (prettyCode n t1 <+> prettyCode n t2)
+prettyCode n Type = text "Type"
+prettyCode n Kind = text "Kind"
View
8 Dedukti/Synthesis/CC.hs
@@ -7,7 +7,6 @@
module Dedukti.Synthesis.CC where
import Dedukti.Core
-import Dedukti.Pretty
import Dedukti.Module
import Control.Applicative ((<*>))
import qualified Data.Set as Set
@@ -16,16 +15,13 @@ import qualified Data.ByteString.Lazy.Char8 as B
-- | Close all abstractions in a term.
closureConv :: Expr Qid Unannot -> Expr Qid Unannot
-closureConv t = unabstract t (go (closed abstract)) where
- -- Check that the given term is closed at toplevel.
- closed k fvs | Set.null fvs = k
- | otherwise = \ _ t _ -> error $ "Term not closed: \n" ++ show (pretty t)
+closureConv t = unabstract t (go (const abstract)) where
go k bs t | isAbstraction t = \as ->
let nas = repeat nann
k' fvs bs' t1' as' =
k (fvs Set.\\ Set.fromList (map bind_name bs)) bs
(apply (abstract bxs (abstract bs' t1' %%% as') %%% nas) xs %%% nas) as
- where lfvs = Set.toList fvs; bxs = map L lfvs; xs = map V lfvs <*> nas
+ where lfvs = Set.toList fvs; bxs = map (`L` Nothing) lfvs; xs = map V lfvs <*> nas
in unabstract t (go k')
go k bs (A t1 t2 a) = go (\fvs1 bs t1' ->
go (\fvs2 bs t2' ->
View
0  Test.hs 100755 → 100644
File mode changed
View
110 lua/dedukti.lua
@@ -0,0 +1,110 @@
+-- Dedukti LUA basic runtime.
+
+-- Terms can be of 6 kinds, either a lambda, a product, an
+-- application, type, a user created box, or a box.
+--
+-- In a term object, two fields must be present, 'tk',
+-- indicating the kind of the term, and a field with
+-- the name of the kind.
+
+-- Code can be of 7 kinds, either a lambda, a product, an
+-- application, type, kind, a variable, a constant.
+
+tlam, tpi, tapp, ttype, tubox, tbox = -- Possible tk
+ 'tlam', 'tpi', 'tapp', 'ttype', 'tubox', 'tbox';
+
+clam, cpi, capp, ctype, ckind, cvar, ccon = -- Possible ck
+ 'clam', 'cpi', 'capp', 'ctype', 'ckind', 'cvar', 'ccon';
+
+function mkcode(kind, ob) -- Building code.
+ assert(kind == clam or kind == cpi or kind == capp
+ or kind == ctype or kind == ckind or kind == cvar
+ or kind == ccon); -- I miss type safety.
+ return { ck = kind, [kind] = ob };
+end
+
+function ap(a, b)
+ assert(a.ck and b.ck);
+ if a.ck == clam then
+ return a.clam(b);
+ else
+ return mkcode(capp, { a, b });
+ end
+end
+
+function obj(t)
+ assert(t.tk and t.tk == tbox);
+ return t.tbox[2];
+end
+
+function convertible(a, b)
+ local function conv(n, a, b)
+ assert(a.ck and b.ck);
+ local v = mkcode(cvar, n);
+ if a.ck == cvar and b.ck == cvar then
+ return a.cvar == b.cvar;
+ elseif a.ck == ccon and b.ck == ccon then
+ return a.ccon == b.ccon;
+ elseif a.ck == clam and b.ck == clam then
+ return conv(n+1, a.clam(v), b.clam(v));
+ elseif a.ck == cpi and b.ck == cpi then
+ return conv(n, a.cpi[1], b.cpi[1])
+ and conv(n+1, a.cpi[2](v), b.cpi[2](v));
+ elseif a.ck == capp and b.ck == capp then
+ return conv(n, a.cpi[1], b.cpi[1])
+ and conv(n, a.cpi[2], b.cpi[2]);
+ elseif a.ck == ctype and b.ck == ctype then
+ return true;
+ elseif a.ck == ckind and b.ck == ckind then
+ return true;
+ else
+ return false;
+ end
+ end
+ return conv(0, a, b);
+end
+
+function box(cty, cv) -- Creates a Term box.
+ return { tk = tbox, tbox = { cty, cv } };
+end
+
+--[[ Typechecking functions. ]]
+
+function synth(n, t)
+ assert(t.tk);
+ if t.tk == tbox then
+ return t.tbox[1];
+ elseif t.tk == ttype then
+ return { ck = ckind };
+ elseif t.tk == tapp and t.tapp[2].tk == tbox then
+ local b = t.tapp[2].tbox;
+ local c = synth(n, t.tapp[1]);
+ assert(c.ck == cpi and convertible(c.cpi[1], b[1])); -- This is totally ugly.
+ return c.cpi[2](b[2]);
+ elseif t.tk == tapp and t.tapp[2].tk == tubox then
+ local b = t.tapp[2].tubox;
+ local ty = synth(n, b[1]);
+ local c = synth(n, t.tapp[1]);
+ assert(c.ck == cpi and convertible(c.cpi[1], ty));
+ return c.cpi[2](b[2]);
+ elseif t.tk == tpi and t.tpi[1].tk == tbox
+ and t.tpi[1].tbox[1].tk == ttype then
+ local v = mkcode(cvar, n);
+ return synth(n+1, t.tpi[2](v));
+ else
+ error("Type synthesis failed.");
+ end
+end
+
+function check(n, t, c) -- t is a term, c is a type.
+ assert(t.tk and c.ck);
+ local v = mkcode(cvar, n);
+ if t.tk == tlam and c.ck == cpi then
+ return check(n+1, t.tlam(box(c.cpi[1], v)), c.cpi[2](v))
+ else
+ return convertible(synth(n, t), c);
+ end
+end
+
+return 42;
+-- vi: expandtab
View
75 lua/tests.lua
@@ -0,0 +1,75 @@
+require "dedukti";
+
+function printc(n, c)
+ assert(c.ck);
+ local v = mkcode(cvar, n);
+ if c.ck == clam then
+ io.write("(Lam "..n..". ");
+ printc(n+1, c.clam(v));
+ io.write(")");
+ elseif c.ck == cpi then
+ io.write("(Pi "..n.." : ");
+ printc(n, c.cpi[1]);
+ io.write(". ");
+ printc(n+1, c.cpi[2](v));
+ io.write(")");
+ elseif c.ck == capp then
+ io.write("(");
+ printc(c.capp[1]);
+ io.write(" ");
+ printc(c.capp[2]);
+ io.write(")");
+ elseif c.ck == ctype then
+ io.write("Type");
+ elseif c.ck == ckind then
+ io.write("Kind");
+ elseif c.ck == cvar then
+ io.write("Var "..c.cvar);
+ elseif c.ck == ccon then
+ io.write("Con "..c.ccon);
+ else
+ error("Unknown code type.");
+ end
+end
+
+function mkarr(dom, codom)
+ return { ck = cpi; cpi = { dom, function (x) return codom; end } };
+end
+
+local aty = { ck = cvar; cvar = 'a' };
+local bty = { ck = cvar; cvar = 'b' };
+
+local idt = { tk = tlam, tlam = function (x_box) return x_box; end };
+local idty = mkarr(aty, aty);
+print("Checking identity: "..tostring(check(0, idt, idty)));
+
+local idty = mkarr(aty, bty);
+print("Checking identity (wrong type): "..tostring(check(0, idt, idty)));
+
+local two =
+ { tk = tlam
+ , tlam = function (f_box)
+ local f = obj(f_box);
+ return
+ { tk = tlam
+ , tlam = function (x_box)
+ local x = obj(x_box);
+ return
+ { tk = tapp
+ , tapp =
+ { f_box
+ , { tk = tubox
+ , tubox = { { tk = tapp, tapp = { f_box, x_box } }
+ , { ck = capp, capp = ap(f, x) }
+ }
+ }
+ }
+ };
+ end
+ };
+ end
+ };
+local twoty = mkarr(mkarr(aty, aty), mkarr(aty, aty));
+print("Checking Church's two: "..tostring(check(0, two, twoty)));
+
+-- vi: expandtab
View
1  setpath.sh
@@ -0,0 +1 @@
+export PATH=`pwd`/scripts:`pwd`/dist/build/dedukti:`pwd`/dist/build/smoke:$PATH
View
1  t/.gitignore
@@ -0,0 +1 @@
+*.dk[io]
View
49 t/fold/arithAnnot.dk
@@ -0,0 +1,49 @@
+prop : Type.
+eps : prop -> Type.
+
+implies : prop -> prop -> prop.
+
+nat : Type.
+nat_ : prop.
+
+bool : Type.
+bool_ : prop.
+
+true : bool.
+false : bool.
+
+isTrue : bool -> Type.
+trueisTrue : isTrue true.
+
+
+[] eps nat_ --> nat.
+[] eps bool_ --> bool.
+[a:prop,b:prop] eps (implies a b) --> eps a -> eps b.
+
+unfold : nat -> p:prop -> eps p -> (nat -> eps p -> eps p) -> eps p.
+fold : (p:prop -> eps p -> (nat -> eps p -> eps p) -> eps p) -> nat.
+
+[pi:p:prop -> eps p -> (nat -> eps p -> eps p) -> eps p] unfold (fold pi) --> pi.
+
+0 : nat.
+S : nat -> nat.
+
+[] 0 --> fold (p => u => v => u).
+[n:nat] S n --> fold (p => u => v => v n (unfold n p u v)).
+
+pred : nat -> nat.
+[n:nat] pred n --> unfold n nat_ 0 (m => _ => m).
+
+iszero : nat -> bool.
+[n:nat] iszero n --> unfold n bool_ true (_ => _ => false).
+
+eq : nat -> nat -> bool.
+[n:nat] eq n --> unfold n (implies nat_ bool_) iszero (_ => f => m => unfold m bool_ false (p => _ => f p)).
+
+
+test1 : nat.
+[] test1 --> S (S (S (S (S 0)))).
+
+test2 : isTrue (eq test1 test1).
+[] test2 --> trueisTrue.
+
View
2  t/peano.dk
@@ -53,7 +53,7 @@ eq_S2 : coc.etype (coc.dotpi1 nat_ (x : nat
pred : nat -> nat.
-[] pred --> nat_rec nat_ 0 (x:nat => nat => x).
+[] pred --> nat_rec nat_ 0 (x:nat => _:nat => x).
pred2 : nat -> nat.
Please sign in to comment.
Something went wrong with that request. Please try again.