Commit a5137ecd authored by Camil Staps's avatar Camil Staps 🚀

Generate preconditions (#16)

parent 44b57b7e
Subproject commit 23b05936be80efc2d30df8c09d347bc04754655d Subproject commit 393afb033911087478d932ab02236203a77849ed
...@@ -5,8 +5,9 @@ CLMFLAGS:=-nr -nt -h 100m -nortsopts\ ...@@ -5,8 +5,9 @@ CLMFLAGS:=-nr -nt -h 100m -nortsopts\
-IL Platform\ -IL Platform\
-I Cloogle\ -I Cloogle\
-I Cloogle/libcloogle\ -I Cloogle/libcloogle\
-I Cloogle/CleanTypes\
-I Cloogle/CleanPrettyPrint\ -I Cloogle/CleanPrettyPrint\
-I Cloogle/CleanRegex\
-I Cloogle/CleanTypes\
-I Cloogle/clean-compiler/frontend\ -I Cloogle/clean-compiler/frontend\
-I Cloogle/clean-compiler/backend\ -I Cloogle/clean-compiler/backend\
-I Cloogle/clean-compiler/main\ -I Cloogle/clean-compiler/main\
......
...@@ -302,7 +302,7 @@ where ...@@ -302,7 +302,7 @@ where
generateProperties :: ![PropertyVarInstantiation] ![NamedTestGenerator] generateProperties :: ![PropertyVarInstantiation] ![NamedTestGenerator]
!LocationInModule !FunctionEntry -> [GeneratedProperty] !LocationInModule !FunctionEntry -> [GeneratedProperty]
generateProperties pvis generators loc fe=:{fe_documentation=Just doc} = generateProperties pvis generators loc fe=:{fe_documentation=Just doc} =
[gen i (fromJust loc.LocationInModule.name) p config [gen i (fromJust loc.LocationInModule.name) doc.preconditions p config
\\ p <- doc.properties \\ p <- doc.properties
, config <- configurations $ groupInstantiations $ pvis ++ docPropertyTestWith doc , config <- configurations $ groupInstantiations $ pvis ++ docPropertyTestWith doc
& i <- [1..]] & i <- [1..]]
...@@ -314,8 +314,8 @@ where ...@@ -314,8 +314,8 @@ where
configurations [vis:viss] = [[vi`:vis`] \\ vi` <- vis, vis` <- configurations viss] configurations [vis:viss] = [[vi`:vis`] \\ vi` <- vis, vis` <- configurations viss]
configurations [] = [[]] configurations [] = [[]]
gen :: !Int !String !Property ![(String,Type)] -> GeneratedProperty gen :: !Int !String ![String] !Property ![(String,Type)] -> GeneratedProperty
gen i fname (ForAll name ts imp) vis = gen i fname preconditions (ForAll name ts imp) vis =
{ gp_name = tname { gp_name = tname
, gp_implementation = join "\n" , gp_implementation = join "\n"
[ tname +++ " :: Property" [ tname +++ " :: Property"
...@@ -323,7 +323,11 @@ where ...@@ -323,7 +323,11 @@ where
, "\t(" +++ lambda +++ join " " [name`` +++ "`":map snd3 ts`] +++ ")" , "\t(" +++ lambda +++ join " " [name`` +++ "`":map snd3 ts`] +++ ")"
, "where" , "where"
, "\t" +++ name`` +++ "` :: " +++ toString type` , "\t" +++ name`` +++ "` :: " +++ toString type`
, "\t" +++ join " " [name`` +++ "`":map fst3 ts`] +++ " = prop _p\n\twhere\n\t\t_p = " +++ replaceSubString "\n" "\n\t\t\t" imp , "\t" +++ join " " [name`` +++ "`":map fst3 ts`] +++ " = prop _p"
, "\twhere"
, "\t\t_p = (True" +++ concat [" /\\ _pre" <+ i \\ i <- [1..] & pre <- preconditions] +++ ") ==> _p`"
, "\t\t_p` = " +++ replaceSubString "\n" "\n\t\t\t" imp
: ["\t\t_pre" <+ i <+ " = " +++ s \\ s <- preconditions & i <- [1..]]
] ]
} }
where where
......
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