Commit ae19a325 authored by Sven Keidel's avatar Sven Keidel

fix sort semantics for tuples

parent 3120362e
......@@ -176,14 +176,29 @@ instance IsTerm Term (Interp s) where
("Cons",_,_) -> throw -< ()
("Nil",[],_) -> (returnA -< Term (List Bottom) ctx) (throw -< ())
("Nil",_,_) -> throw -< ()
(_,_,Top) -> (lubA (proc (Signature ss _) -> if eqLength ss ps
then do
ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
cons -< (c,ss')
else throw -< ()) -<< Ctx.lookupCons ctx c)
("",_,Tuple ss)
| eqLength ss ps -> do
ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
cons -< (c,ss')
| otherwise -> throw -< ()
(_,_,Top) ->
(let sorts = Ctx.lookupCons ctx c
in if null sorts
then fail -< printf "Constructor %s is not in context" (show c)
else
(lubA (proc (Signature ss _) ->
if eqLength ss ps
then do
ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
cons -< (c,ss')
else throw -< ()) -<< Ctx.lookupCons ctx c))
(throw -< ())
_ ->
lubA (proc (c',Signature ss _) -> if c == c' && eqLength ss ps
_ -> do
let sorts = Ctx.lookupSort ctx s
if null sorts
then fail -< printf "Sort %s is not in context" (show s)
else lubA (proc (c',Signature ss _) ->
if c == c' && eqLength ss ps
then do
ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
cons -< (c',ss')
......@@ -235,7 +250,7 @@ instance IsTerm Term (Interp s) where
"Nil" -> case ss of
[] -> Term (List Bottom) ctx
_ -> Term Top ctx
"Tuple" -> Term (Tuple (map sort ss)) ctx
"" -> Term (Tuple (map sort ss)) ctx
_ -> glb (Term Top ctx : [ Term s ctx | Signature ss' s <- Ctx.lookupCons ctx c, ss sortsToTerms ss' ctx ])
numberLiteral = proc _ -> do
......
......@@ -246,7 +246,7 @@ spec = do
describe "Let" $ do
it "should apply a single function call" $
let ?ctx = Ctx.empty in
let t = term "Exp"
let t = term (Tuple ["Exp","Exp"])
tenv = termEnv [("x",t)]
in seval 2 (Let [("swap", swap)] (Match "x" `Seq` Call "swap" [] ["x"])) t `shouldBe` success (tenv, t)
......@@ -261,7 +261,7 @@ spec = do
it "should apply a single function call" $
let ?ctx = Ctx.empty in
let senv = M.singleton "swap" (Closure swap M.empty)
t = term "Exp"
t = term (Tuple ["Exp","Exp"])
tenv = termEnv [("x",t)]
in seval'' 1 10 (Match "x" `Seq` Call "swap" [] []) senv emptyEnv t `shouldBe` success (tenv, t)
......@@ -348,7 +348,7 @@ spec = do
-- showLub :: C.Term -> C.Term -> String
-- showLub t1 t2 = show (alpha (C.fromFoldable [t1,t2] :: C.Pow C.Term) :: Term)
swap = Strategy [] [] (Scope ["x","y"] (Match (Cons "Tuple" ["x","y"]) `Seq` Build (Cons "Tuple" ["y","x"])))
swap = Strategy [] [] (Scope ["x","y"] (Match (Cons "" ["x","y"]) `Seq` Build (Cons "" ["y","x"])))
map' = Strategy ["f"] ["l"] (Scope ["x","xs","x'","xs'"] (
Build "l" `Seq`
......
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