Commit 60e8d5d5 authored by André Pacak's avatar André Pacak
Browse files

define small dsl to construct terms (extendedTLC)

parent 137c3ccd
......@@ -30,14 +30,6 @@ data Term =
InL Term Parent |
InR Term Parent |
Case Term Name Term Name Term Parent
-- flip 1/2, flip 3/4, flip 2/3
swap_1_2 = flip
swap_2_3 = (.) flip
swap_3_4 = ((.).(.)) flip
flipForCase :: (Term -> Name -> Term -> Name -> Term -> Term) -> (Name -> Name -> Term -> Term -> Term -> Term)
flipForCase = swap_2_3 . swap_3_4 . swap_1_2
instance Eq Term where
(Var n1 _) == (Var n2 _) = n1 == n2
......@@ -80,25 +72,47 @@ parent (InL _ p) = p
parent (InR _ p) = p
parent (Case _ _ _ _ _ p) = p
-- DSL for constructing terms
type TermBuild = Parent -> Term
cons0 :: (Parent -> Term) -> TermBuild
cons0 cons parent = let res = cons parent in res
cons1 :: (Term -> Parent -> Term) -> TermBuild -> TermBuild
cons1 cons e parent = let res = cons (e (Just res)) parent in res
cons2 :: (Term -> Term -> Parent -> Term) -> TermBuild -> TermBuild -> TermBuild
cons2 cons e1 e2 parent = let res = cons (e1 (Just res)) (e2 (Just res)) parent in res
cons3 :: (Term -> Term -> Term -> Parent -> Term) -> TermBuild -> TermBuild -> TermBuild -> TermBuild
cons3 cons e1 e2 e3 parent = let res = cons (e1 (Just res)) (e2 (Just res)) (e3 (Just res)) parent in res
root :: TermBuild -> Term
root t = t Nothing
infixr 6 *
(*) :: (Term -> TermBuild) -> TermBuild -> TermBuild
parent * kid1 = \parentParent ->
let iparent = parent (kid1 $ Just iparent) parentParent in iparent
var n = cons0 (Var n)
app = cons2 App
lam n = cons1 (Lam n)
anno ty = cons1 (flip Anno ty)
zero = cons0 Zero
succ = cons1 Succ
add = cons2 Add
mult = cons2 Mult
pair = cons2 Pair
fst' = cons1 Fst
snd' = cons1 Snd
let' n = cons2 (Let n)
infixr 6 **
(**) :: (Term -> Term -> TermBuild) -> (TermBuild, TermBuild) -> TermBuild
parent ** (kid1, kid2) = \parentParent ->
let iparent = parent (kid1 $ Just iparent) (kid2 $ Just iparent) parentParent in iparent
sel n = cons1 (Sel n)
inl = cons1 InL
inr = cons1 InR
-- case' :: (Term -> Name -> Term -> Name -> Term -> Parent -> Term) -> TermBuild -> TermBuild -> TermBuild -> TermBuild
-- case' cons e n1 t1 n2 t2 parent = let res = cons (e (Just res)) n1 (t1 (Just res)) n2 (t2 (Just res)) parent in res
infixr 6 ***
(***) :: (Term -> Term -> Term -> TermBuild) -> (TermBuild, TermBuild, TermBuild) -> TermBuild
parent *** (kid1, kid2, kid3) = \parentParent ->
let iparent = parent (kid1 $ Just iparent) (kid2 $ Just iparent) (kid3 $ Just iparent) parentParent in iparent
instance Show Term where
showsPrec _ (Var x _) = showString x
......
......@@ -51,6 +51,8 @@ sharedSpec inferType = do
-- let res = convert $ inferType tOkRecord in res `shouldBe` B.Inferred (Fun (Fun Nat Nat))
it "should infer left injection " $ do
let res = convert $ inferType tOkInL in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
it "should infer right injection " $ do
let res = convert $ inferType tOkInR in res `shouldBe` B.Inferred (Sum Nat (Prod Nat (Fun Nat Nat)))
it "should fail while inferring an arithmetic expression with an unapplied lambda expression" $ do
let res = isInferred $ convert $ inferType tFailArithmetic in res `shouldBe` False
it "should fail while inferring an application of a lambda expression without type annotation" $ do
......@@ -67,3 +69,7 @@ sharedSpec inferType = do
let res = isInferred $ convert $ inferType tFailLetInPairFst in res `shouldBe` False
it "should fail while infering let binding in pair(snd)" $ do
let res = isInferred $ convert $ inferType tFailLetInPairSnd in res `shouldBe` False
it "should fail while infering left injection" $ do
let res = isInferred $ convert $ inferType tFailInL in res `shouldBe` False
it "should fail while infering right injection" $ do
let res = isInferred $ convert $ inferType tFailInR in res `shouldBe` False
module ExtendedTLC.TestCases where
import Prelude hiding (lookup,(*), (**))
import Prelude hiding (lookup,(*), (**), succ, fst, snd)
import ExtendedTLC.Language
tOkZero = root Zero
tOkSucc = root $ Succ * Succ * Succ * Succ * Zero
tOkArithmetic = root $ Add ** (Succ * Succ * Zero, Mult ** (Zero, Succ * Succ * Succ * Succ * Zero))
tOkLetBindingWithArith = root $ Let "x" ** (Add ** (Zero, Succ * Zero), Mult ** (Var "x", Succ * Succ * Zero))
tOkProd = root $ flip Anno (Prod Nat (Prod Nat Nat)) *
Pair ** (Succ * Succ * Zero, Pair ** (Zero, Succ * Zero))
tOkProjection1 = root $ Fst * flip Anno (Prod Nat Nat) *
Pair ** (Mult ** (Zero, Zero), Add ** (Succ * Zero, Zero))
tOkProjection2 = root $ Snd * flip Anno (Prod Nat (Prod Nat Nat)) *
Pair ** (Succ * Succ * Zero, Pair ** (Zero, Succ * Zero))
tOkAnno = root $ flip Anno (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat))) *
Lam "f" * Lam "g" * Lam "b" * App ** (Var "g", App ** (Var "f", Var "b"))
tOkLambdaAnno = root $ flip Anno (Fun Nat Nat) * Lam "a" * Add ** (Var "a", Zero)
tOkAppLambdaAnno = root $ App ** (flip Anno (Fun Nat Nat) * Lam "b" * (Add ** (Var "b", Zero)), Succ * Succ * Zero)
tOkAnnoInBindingLet = root $ Let "e" ** (flip Anno Nat * Add ** (Zero, Succ * Zero), Mult ** (Var "e", Succ * Zero))
tOkLetInPairFst = root $ flip Anno (Prod Nat (Fun Nat Nat)) * Pair ** (Let "e" ** (Zero, Succ * Succ * Var "e"), Lam "a" * Succ * Var "a")
tOkLetInPairSnd = root $ flip Anno (Prod (Fun Nat Nat) Nat) * Pair ** (Lam "n" * Var "n", Let "e" ** (Zero, Succ * Succ * Var "e"))
tFailArithmetic = root $ Add ** (Succ * Succ * Zero, Mult ** (flip Anno (Fun Nat Nat) * Lam "f" * Var "f", Succ * Succ * Succ * Succ * Zero))
tFailLambdaNoAnno = root $ flip Anno Nat *
App ** (Lam "b" * (Add ** (Var "b", Zero)), Succ * Succ * Zero)
tFailProdInAdd = root $ flip Anno Nat *
Add ** (flip Anno (Prod Nat Nat) * Pair ** (Zero, Zero), Zero)
tFailLambdaInProd = root $ flip Anno Nat *
Snd * flip Anno (Prod Nat Nat) * Pair ** (flip Anno (Fun Nat Nat) * Lam "a" * Var "a", Zero)
tFailProjectionOnNat = root $ Snd * Succ * Succ * Zero
tFailLambdaNotAnnoInBindingLet = root $ Let "e" ** (Lam "n" * Add ** (Var "n", Succ * Zero), Mult ** (App ** (Var "e", Zero), Succ * Zero))
tFailLetInPairFst = root $ flip Anno (Prod (Fun Nat Nat) (Fun Nat Nat)) * Pair ** (Let "e" ** (Zero, Succ * Succ * Var "e"), Lam "a" * Succ * Var "a")
tFailLetInPairSnd = root $ flip Anno (Prod Nat (Fun Nat Nat)) * Pair ** (Lam "n" * Var "n", Let "e" ** (Zero, Succ * Succ * Var "e"))
-- tFailExperiment = root $ flip App ** (flip Anno (Fun Nat (Fun Nat Nat)) * Lam "x" * Let "y" ** (flip Anno (Fun Nat Nat) * Lam "x" * Var "x", Zero), Zero)
tFailExperiment2 = root $ flip Anno (Fun Nat Nat) * Lam "x" * Let "y" ** (flip Anno (Fun (Fun Nat Nat) Nat) * Lam "z" * App ** (Var "z", Zero), App ** (Var "y", Lam "x" * Zero))
tFailExperiment3 = root $ Let "y" ** (Zero, Let "y" ** (flip Anno (Fun Nat Nat) * Lam "n" * Var "n", App ** (Var "y", Zero)))
tFailExperiment = root $ flip Anno (Fun Nat (Fun (Fun (Prod Nat Nat) Nat) Nat)) * Lam "x" * Lam "y" * Lam "y" * Zero
tOkInL = root $ flip Anno (Sum Nat (Fun Nat Nat)) * InL * Succ * Zero
-- tOkRecord = root $ Sel "b" * Rec ([("a", Zero)]) -- , ("b", Lam "x" * Lam "y" * Zero), ("c", Pair ** (Zero, Succ * Zero))])
tOkZero = root zero
tOkSucc = root $ succ $ succ zero
tOkArithmetic = root $ (add (succ $ succ zero) (mult zero (succ $ succ $ succ $ succ zero)))
tOkLetBindingWithArith = root $ (let' "x" (add zero (succ zero)) (mult (var "x") (succ $ succ zero)))
tOkProd = root $ (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (succ zero))))
tOkProjection1 = root $ fst' (anno (Prod Nat Nat) (pair (mult zero zero) (add (succ zero) zero)))
tOkProjection2 = root $ snd' (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (succ zero))))
tOkAnno = root $ (anno (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat))) (lam "f" $ lam "g" $ lam "b" (app (var "g") (app (var "f") (var "b")))))
tOkLambdaAnno = root $ (anno (Fun Nat Nat) (lam "a" (add (var "a") zero)))
tOkAppLambdaAnno = root $ (app (anno (Fun Nat Nat) (lam "b" (add (var "b") zero))) (succ $ succ zero))
tOkAnnoInBindingLet = root $ (let' "e" (anno Nat (add zero (succ zero))) (mult (var "e") (succ zero)))
tOkLetInPairFst = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (let' "e" zero (succ $ succ (var "e"))) (lam "a" (succ (var "a")))))
tOkLetInPairSnd = root $ (anno (Prod (Fun Nat Nat) Nat) (pair (lam "n" (var "n")) (let' "e" zero (succ $ succ (var "e")))))
tOkInL = root $ (anno (Sum Nat (Fun Nat Nat)) (inl $ succ zero))
tOkInR = root $ (anno (Sum Nat (Prod Nat (Fun Nat Nat))) (inr (pair (succ $ succ zero) (anno (Fun Nat Nat) (lam "b" zero)))))
tFailArithmetic = root $ (add (succ $ succ zero) (mult (anno (Fun Nat Nat) (lam "f" (var "f"))) (succ $ succ $ succ $ succ zero)))
tFailLambdaNoAnno = root $ (anno Nat (app (lam "b" (add (var "b") zero)) (succ $ succ zero)))
tFailProdInAdd = root $ (anno Nat (add (anno (Prod Nat Nat) (pair zero zero)) zero))
tFailLambdaInProd = root $ (anno Nat (snd' (anno (Prod Nat Nat) (pair (anno (Fun Nat Nat) (lam "a" (var "a"))) zero))))
tFailProjectionOnNat = root $ snd' $ succ $ succ zero
tFailLambdaNotAnnoInBindingLet = root $ (let' "e" (lam "n" (add (var "n") (succ zero))) (mult (app (var "e") zero) (succ zero)))
tFailLetInPairFst = root $ (anno (Prod (Fun Nat Nat) (Fun Nat Nat)) (pair (let' "e" zero $ succ $ succ $ var "e") (lam "a" $ succ $ var "a")))
tFailLetInPairSnd = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (lam "n" $ var "n") (let' "e" zero $ succ $ succ $ var "e")))
tFailInL = root $ (anno (Sum Nat Nat) (inl (pair zero zero)))
tFailInR = root $ (anno (Sum Nat Nat) (inr (lam "x" $ var "x")))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment