Skip to content

Commit

Permalink
Remove old implementation
Browse files Browse the repository at this point in the history
  • Loading branch information
SophieBosio committed May 7, 2024
1 parent 7bb4989 commit 1dcfa26
Showing 1 changed file with 0 additions and 36 deletions.
36 changes: 0 additions & 36 deletions src/Validation/Translator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -175,42 +175,6 @@ liftPropertyInputPatterns (Lambda p t _) =
liftPropertyInputPatterns t = return (id, t)


-- * Create symbolic variables for SBV to instantiate during solving
createSymbolic :: Pattern Type -> Formula SValue
createSymbolic (Variable _ Unit') = return SUnit
createSymbolic (Variable x Integer') =
do sx <- lift $ sInteger x
return $ SNumber sx
createSymbolic (Variable x Boolean') =
do sx <- lift $ sBool x
return $ SBoolean sx
createSymbolic (Variable x (Variable' _)) =
do sx <- lift $ free x
return $ SNumber sx
createSymbolic (Variable _ (TypeList [])) =
do return $ SArgs []
createSymbolic (Variable x (TypeList ts)) =
-- We should never be asked to create input for this type, since it's
-- internal and not exposed to the user. However, we are able to do so.
-- Fabricate new name for each variable by hashing <x><type-name>
-- and appending the index of the variable type in the TypeList.
do let names = zipWith (\tau i -> show (hash (x ++ show tau)) ++ show i)
ts
([0..] :: [Integer])
let ps = zipWith Variable names ts
sxs <- mapM createSymbolic ps
return $ SArgs sxs
createSymbolic (Variable x (ADT adt)) =
do env <- environment
si <- lift $ sInteger "selector"
upper <- cardinality env adt
lift $ constrain $ (si .>= 0) .&& (si .< literal upper)
return $ SADT adt si []
createSymbolic p = error $
"Unexpected request to create symbolic sub-pattern '"
++ show p ++ "' of type '" ++ show (annotation p) ++ "'"
++ "\nPlease note that generating arbitrary functions is not supported."

-- createSymbolic 0 (Variable x (ADT adt)) = error $
-- "Reached max. recursion depth while trying to generate symbolic ADT "
-- ++ adt ++ "' for variable '" ++ x ++ "'"
Expand Down

0 comments on commit 1dcfa26

Please sign in to comment.