|
definition:
|
attachProperties2Funcs :: [CFuncDecl] -> [(SourceLine,String)]
-> [(String,[(FuncAttachment,String,[BaseHtml])])]
attachProperties2Funcs _ [] = []
attachProperties2Funcs props ((sourceline,_) : slines) =
case sourceline of
FuncDef fn -> let (fprops,rslines) = span isPropFuncDef slines
in (fn, showContracts fn ++ concatMap showProp fprops) :
attachProperties2Funcs props rslines
_ -> attachProperties2Funcs props slines
where
propNames = map (snd . funcName) props
showProp (FuncDef fn,_) =
let propdecl = fromJust (find (\fd -> snd (funcName fd) == fn) props)
in if isProperty propdecl
then map (\rhs -> (Property, fn,
[code [htxt $ prettyWith (ppCRhs empty) rhs]]))
(map ruleRHS (funcRules propdecl))
else []
showContracts fn =
showContract (fn++"'pre") showPreCond ++
showContract (fn++"'post") showPostCond ++
showContract (fn++"'spec") showSpec
showContract fnsuff formatrule =
maybe []
(\contractdecl -> showRulesWith formatrule fnsuff contractdecl)
(find (\fd -> snd (funcName fd) == fnsuff) props)
showRulesWith formatrule fnsuff (CFunc qn@(mn,fn) ar _ ftype rules) =
let stripSuffix = reverse . tail . dropWhile (/='\'') . reverse
in map (formatrule fnsuff qn (mn,stripSuffix fn)
. etaExpand ar (length (argTypes (typeOfQualType ftype)))) rules
-- eta expand simple rules for more reasonable documentation
etaExpand arity tarity rule = case rule of
CRule ps (CSimpleRhs exp ldecls) ->
if arity == tarity
then rule
else let evars = map (\i -> (i,"x"++show i)) [(arity+1) .. tarity]
in CRule (ps ++ map CPVar evars)
(CSimpleRhs (foldl CApply exp (map CVar evars)) ldecls)
_ -> rule -- don't do it for complex rules
showPreCond fnpre qp qn rule = case rule of
CRule _ (CSimpleRhs _ _) ->
let (lhs,rhs) = break (=='=') (prettyRule qn rule)
in (PreCond, fnpre, [code [htxt $ "(" ++ stripSpaces lhs ++ ")"],
italic [htxt " requires "],
code [htxt (safeTail rhs)]])
_ -> -- we don't put must effort to format complex preconditions:
(PreCond, fnpre, [code [htxt $ prettyRule qp rule]])
showPostCond fnpost qp qn rule = case rule of
CRule ps (CSimpleRhs _ _) ->
let (_,rhs) = break (=='=') (prettyRule qn rule)
in (PostCond, fnpost,
[code [htxt $ prettyWith ppCPattern (last ps) ++ " = " ++
prettyWith ppCPattern
(CPComb qn (take (length ps - 1) ps)) ],
italic [htxt " satisfies "],
code [htxt (safeTail rhs)]])
_ -> -- we don't put must effort to format complex postconditions:
(PostCond, fnpost, [code [htxt $ prettyRule qp rule]])
showSpec fnspec qp qn rule = case rule of
CRule _ (CSimpleRhs _ _) ->
let (lhs,rhs) = break (=='=') (prettyRule qn rule)
in (SpecFun, fnspec, [code [htxt $ "(" ++ stripSpaces lhs ++ ")"],
italic [htxt " is equivalent to "],
code [htxt (safeTail rhs)]])
_ -> -- we don't put must effort to format complex specifications:
(SpecFun, fnspec, [code [htxt $ prettyRule qp rule]])
prettyWith ppfun = showWidth 78 . ppfun prettyOpts
prettyRule qn rl = showWidth 78 (ppCRule prettyOpts qn rl)
prettyOpts = setNoQualification defaultOptions
safeTail xs = if null xs then xs else tail xs
isPropFuncDef (sline,_) =
case sline of FuncDef fn -> fn `elem` propNames
_ -> False
|