Commit b7522247 authored by Jente Hidskes's avatar Jente Hidskes

Fix soundness tests for sort semantics

parent 7c73e677
......@@ -375,23 +375,18 @@ convertToList [] ctx = Term (List Bottom) ctx
convertToList ts ctx = Term (List (sort $ lub ts)) ctx
termToSort :: C.Term -> Sort
termToSort (C.Cons _ _) = Sort "Exp"
termToSort (C.Cons (Constructor c) _) = Sort (SortId c)
termToSort (C.StringLiteral _) = Lexical
termToSort (C.NumberLiteral _) = Numerical
sortContext :: C.Term -> SortContext
sortContext term = SortContext
{ signatures = case term of
C.Cons c ts -> unionsWith (++) tss where
tss = M.singleton c [(map termToSort ts, termToSort term)]
: map (signatures . sortContext) ts
C.Cons c ts -> unionsWith (\s1 s2 -> nub (s1 ++ s2)) (M.singleton c [(map termToSort ts, termToSort term)] : map (signatures . sortContext) ts)
_ -> M.empty
, lexicals = Set.empty
-- Top can be formed from any sort.
, injectionClosure = M.insertWith Set.union Top (Set.fromList [termToSort term,Numerical,Lexical]) $ case term of
C.Cons _ ts ->
unionsWith Set.union $ M.singleton (termToSort term) (Set.fromList (map termToSort ts))
: map (injectionClosure . sortContext) ts
, injectionClosure = case term of
C.Cons _ ts -> unionsWith Set.union $ M.singleton (termToSort term) (Set.fromList (map termToSort ts)) : map (injectionClosure . sortContext) ts
_ -> M.empty
}
......
......@@ -5,6 +5,7 @@ module SortSemanticsSpec(main, spec) where
import qualified ConcreteSemantics as C
import SharedSemantics hiding (cons)
import Soundness
import Sort (SortId(..))
import Syntax hiding (Fail)
import SortSemantics hiding (sortContext)
......@@ -12,6 +13,7 @@ import Control.Arrow
import Data.Abstract.FreeCompletion (fromCompletion)
import Data.Abstract.HandleError
import qualified Data.Abstract.Maybe as M
import qualified Data.Abstract.PreciseStore as S
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (fromTerminating)
......@@ -315,17 +317,29 @@ spec = do
sound'' :: Strat -> [(C.Term,[(TermVar,C.Term)])] -> TermPattern -> Property
sound'' s xs pat = sound (M.empty,ctx) (C.fromFoldable $ fmap (second termEnv') xs) (eval' s) (eval' s :: Interp (SW.Categories (Strat,StratEnv) (TermEnv,Term) SW.Stack) Term Term) where
ctx = (alpha::C.Pow C.Term -> SortContext) (C.fromFoldable (map fst xs)) `union` patContext pat
ctx = (alpha::C.Pow C.Term -> SortContext) (C.fromFoldable (map fst xs)) `union` patContext tenv pat
tenv = (termEnv [ (v,(alpha::C.Pow C.Term -> Term) (C.singleton t)) | (_,xs') <- xs, (v,t) <- xs'])
patContext :: TermPattern -> SortContext
patContext pat = case pat of
patContext :: TermEnv -> TermPattern -> SortContext
patContext tenv pat = case pat of
Cons c pats -> SortContext
{ signatures = unionsWith (++) (M.singleton c [(replicate (length pats) "Exp", "Exp")]:map (signatures . patContext) pats)
{ signatures = unionsWith (++) (M.singleton c [(map (patToSort tenv) pats, patToSort tenv pat)]:map (signatures . (patContext tenv)) pats)
, lexicals = Set.empty
, injectionClosure = M.empty -- Since we're taking the union, we can just leave this empty. It's Exp->Exp anyway.
, injectionClosure = M.empty -- Since we're taking the union, we can just leave this empty.
}
_ -> SortContext { signatures = M.empty, lexicals = Set.empty, injectionClosure = M.empty }
patToSort :: TermEnv -> TermPattern -> Sort
patToSort _ (Cons (Constructor c) _) = Sort (SortId c)
patToSort _ (StringLiteral _) = Lexical
patToSort _ (NumberLiteral _) = Numerical
patToSort _ (As _ _) = error "no such sort: as"
patToSort _ (Explode _ _) = error "no such sort: explode"
patToSort tenv (Var x) = case S.lookup x tenv of
M.Just (Term s _) -> s
M.JustNothing (Term s _) -> s
M.Nothing -> Bottom
termEnv' = C.TermEnv . M.fromList
termEnv :: [(TermVar, Term)] -> TermEnv
termEnv = S.fromList
......
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