Skip to content

GitLab

Commit 81b34e7b authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Use sub-sorts *up to* a size instead of simply of that size

parent 6270b79c
Hide whitespace changes
Inline Side-by-side
Tool/Variable/DeBruijn.hs
View file @ 81b34e7b
......@@ -248,10 +248,15 @@ generatorFunctions (nsd, sd, _, _) =
where
generators :: SortDef -> [Function]
generators s@(MkDefSort sname ctxs ctors rewrite) =
[Fn ("gen" ++ sname) -- Function that returns a datastructure representing every term of some size.
[(VarParam "env" : replaceParam s (IntParam 0) params, FnCall "empty" []),
(VarParam "env" : replaceParam s (IntParam 1) params, alternatives $ map genFromCtor $ filter ((== 0) . ctorSize) ctors),
(VarParam "env" : params , alternatives $ map genFromCtor $ filter ((/= 0) . ctorSize) ctors)],
[Fn (sname ++ "OfSize") -- Function that returns a datastructure representing every term of some size.
[(VarParam "env" : replaceParam (IntParam 0) params, FnCall "empty" []),
(VarParam "env" : replaceParam (IntParam 1) params, alternatives $ map genFromCtor $ filter ((== 0) . ctorSize) ctors),
(VarParam "env" : params , alternatives $ map genFromCtor $ filter ((/= 0) . ctorSize) ctors)],
Fn (sname ++ "UpToSize") -- Combines all constructors up to a certain size
[(VarParam "env" : replaceParam (IntParam 0) params, FnCall "empty" []),
(VarParam "env" : params, AltExpr (FnCall (sname ++ "UpToSize") (VarExpr "env" : replaceArg (Minus (VarExpr ("n" ++ sname)) (IntExpr 1)) args))
(FnCall (sname ++ "OfSize") (VarExpr "env" : args)))],
Fn (sname ++ "Env") -- Function to 'cast' the contexts of one sort to another by discarding variables not in the target sort's contexts
([([ConstrParam ("S" ++ nsname) [VarParam "next"]],
......@@ -263,7 +268,7 @@ generatorFunctions (nsd, sd, _, _) =
Fn ("for" ++ sname ++ "WithSize") -- Wrapper for QuickCheck's forAll
[(VarParam "env" : params ++ [VarParam "prop"],
LetExpr [(VarParam "c", FnCall ("gen" ++ sname) $ VarExpr "env" : (argsOf sname)),
LetExpr [(VarParam "c", FnCall (sname ++ "OfSize") $ VarExpr "env" : args),
(VarParam "n", FnCall "card" [VarExpr "c"]),
(VarParam "g", AppFnCall "(!)" [FnCall "pure" [VarExpr "c"],
FnCall "chooseInteger" [TupleExpr [IntExpr 0, Minus (VarExpr "n") (IntExpr 1)]]])]
......@@ -271,12 +276,15 @@ generatorFunctions (nsd, sd, _, _) =
]
where
params = paramsOf sname
args = argsOf sname
-- Turn a constructor into an expression that defines a single alternative
genFromCtor :: ConstructorDef -> Expression
genFromCtor c@(MkVarConstructor cname cinst) = AppConstrInst cname [FnCall ("get" ++ getNsByInst ctxs cinst) [VarExpr "env", ConstrInst "Z" []]]
genFromCtor c@(MkDefConstructor cname _ csorts _ cattrs natives) = makeRecursiveCtor cname csorts cattrs "" natives
genFromCtor c@(MkBindConstructor cname _ csorts _ (_, ns) cattrs natives) = makeRecursiveCtor cname csorts cattrs ns natives
-- Def and Bind constructors share a similar expression, which this function returns.
makeRecursiveCtor :: ConstructorName -> [(IdenName, SortName)] -> [AttributeDef] -> NamespaceName -> [HaskellTypeName] -> Expression
makeRecursiveCtor cname csorts cattrs ns natives =
if countSorts csorts s > 1
......@@ -285,22 +293,23 @@ generatorFunctions (nsd, sd, _, _) =
[LambdaExpr [VarParam "l"] $ AppConstrInst cname (ctorArgs 0 ns cattrs csorts ++ nativeArgs),
FnCall "splitn" [IntExpr $ countSorts csorts s, Minus (VarExpr $ "n" ++ sname) (IntExpr 1)]]]
else
AppConstrInst cname ([FnCall ("gen" ++ aname) $
(envFor ns arg cattrs):(replaceArg s (Minus (VarExpr $ "n" ++ sname) (IntExpr 1)) $ argsOf aname) | arg@(_, aname) <- csorts]
AppConstrInst cname ([FnCall (aname ++ "OfSize") $
(envFor ns arg cattrs):(replaceArg (Minus (VarExpr $ "n" ++ sname) (IntExpr 1)) $ argsOf aname) | arg@(_, aname) <- csorts]
++ nativeArgs)
where
nativeArgs = [FnCall ("gen" ++ tname) [] | tname <- natives]
-- Generate the arguments of a comble with the correct variables and expressions as its arguments
ctorArgs :: Int -> NamespaceName -> [AttributeDef] -> [(IdenName, SortName)] -> [Expression]
ctorArgs _ _ _ [] = []
ctorArgs n ns attrs (arg@(_, aname):as) =
if aname == sname
then (FnCall ("gen" ++ aname) $ env:(replaceArg s (FnCall "(!!)" [VarExpr "l", IntExpr n]) args)) : ctorArgs (n+1) ns attrs as
else (FnCall ("gen" ++ aname) $ env:args) : ctorArgs n ns attrs as
then (FnCall (aname ++ "OfSize") $ env:(replaceArg (FnCall "(!!)" [VarExpr "l", IntExpr n]) args)) : ctorArgs (n+1) ns attrs as
else (FnCall (aname ++ "UpToSize") $ env:(argsOf aname)) : ctorArgs n ns attrs as
where
env = envFor ns arg attrs
args = argsOf aname
-- Use the binder and the attributes of a ctor to determine the environment to be passed to subcombles
envFor :: NamespaceName -> (IdenName, SortName) -> [AttributeDef] -> Expression
envFor binder (iden, name) allAttrs = FnCall (name ++ "Env") [envexpr attrs]
where
......@@ -314,6 +323,19 @@ generatorFunctions (nsd, sd, _, _) =
ctorSize MkDefConstructor{csorts=sorts} = countSorts sorts s
ctorSize MkBindConstructor{csorts=sorts} = countSorts sorts s
-- Replace the argument or parameter corresponding to the current sort with the given expression or parameter
replaceParam :: Parameter -> [Parameter] -> [Parameter]
replaceParam replacewith = map $ \p -> case p of (VarParam var) -> if var == "n" ++ sname
then replacewith
else p
_ -> p
replaceArg :: Expression -> [Expression] -> [Expression]
replaceArg replacewith = map $ \a -> case a of (VarExpr var) -> if var == "n" ++ sname
then replacewith
else a
_ -> a
getNsByInst :: [Context] -> NamespaceName -> NamespaceName
getNsByInst (ctx:ctxs) inst = if inst == xinst ctx
then xnamespace ctx
......@@ -340,18 +362,6 @@ generatorFunctions (nsd, sd, _, _) =
argsOf :: SortName -> [Expression]
argsOf = map (\(MkDefSort sname _ _ _) -> VarExpr ("n" ++ sname)) . accessibleSorts . getSortByName sd
replaceParam :: SortDef -> Parameter -> [Parameter] -> [Parameter]
replaceParam (MkDefSort sname _ _ _) replacewith = map $ \p -> case p of (VarParam var) -> if var == "n" ++ sname
then replacewith
else p
_ -> p
replaceArg :: SortDef -> Expression -> [Expression] -> [Expression]
replaceArg (MkDefSort sname _ _ _) replacewith = map $ \a -> case a of (VarExpr var) -> if var == "n" ++ sname
then replacewith
else a
_ -> a
countSorts [] _ = 0
countSorts ((_, name):sorts) s@(MkDefSort sname _ _ _) = (if name == sname
then 1
......
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