Add @property, @property-test-with, @property-bootstrap

CleanTypeUnifier @ e696b7fe

-Subproject commit 73708b8b9a65ffc51219347ecf19d4b2e99bc077
+Subproject commit e696b7feca939c4ee74acbe8c8edbedcd061e975

CloogleDB.icl

@@ -62,12 +62,14 @@ derive JSONEncode ClassDoc, ClassEntry, ClassMemberDoc, CloogleEntry,
 	Constructor, ConstructorDoc, DeriveEntry, FunctionDoc, FunctionEntry,
 	InstanceEntry, Location, ModuleDoc, ModuleEntry, Priority, RecordField,
 	SyntaxEntry, Type, TypeDef, TypeDefEntry, TypeDefRhs, TypeDoc,
-	TypeRestriction, ABCInstructionEntry
+	TypeRestriction, ABCInstructionEntry, Property, PropertyVarInstantiation,
+	MultiLineString
 derive JSONDecode ClassDoc, ClassEntry, ClassMemberDoc, CloogleEntry,
 	Constructor, ConstructorDoc, DeriveEntry, FunctionDoc, FunctionEntry,
 	InstanceEntry, Location, ModuleDoc, ModuleEntry, Priority, RecordField,
 	SyntaxEntry, Type, TypeDef, TypeDefEntry, TypeDefRhs, TypeDoc,
-	TypeRestriction, ABCInstructionEntry
+	TypeRestriction, ABCInstructionEntry, Property, PropertyVarInstantiation,
+	MultiLineString
 
 printersperse :: Bool a [b] -> [String] | print a & print b
 printersperse ia a bs = intercalate (print False a) (map (print ia) bs)

CloogleDBFactory.icl

@@ -90,8 +90,8 @@ from CloogleDB import
 	instance == Location,
 	location
 from Cloogle import instance == FunctionKind
-from Doc import :: ModuleDoc, :: FunctionDoc{..}, :: ClassDoc, :: TypeDoc{..},
-	:: ConstructorDoc, :: ClassMemberDoc, :: Description,
+from Doc import :: ModuleDoc, :: FunctionDoc{vars,description}, :: ClassDoc,
+	:: TypeDoc{..}, :: ConstructorDoc, :: ClassMemberDoc, :: Description,
 	:: ParseWarning(UsedReturn,IllegalField), :: ParseError,
 	generic docBlockToDoc, parseDoc, parseSingleLineDoc, :: DocBlock,
 	class docType(..), instance docType FunctionDoc,

Doc.dcl

@@ -12,6 +12,14 @@ from Data.Maybe import :: Maybe
 
 from TypeDef import :: Type
 
+/**
+ * A wrapper around the {{`String`}} type which makes sure that multi-line
+ * documentation blocks get trimmed w.r.t. whitespace.
+ */
+:: MultiLineString = MultiLine !String
+
+fromMultiLine :: !MultiLineString -> String
+
 class docDescription    d :: !d -> Maybe Description
 class docParams         d :: !d -> [Description]
 class docVars           d :: !d -> [Description]
@@ -27,7 +35,8 @@ class docRepresentation d :: !d -> Maybe (Maybe Description)
  * Documentation of a Clean module.
  */
 :: ModuleDoc =
-	{ description :: Maybe Description
+	{ description        :: Maybe Description
+	, property_bootstrap :: Maybe MultiLineString //* For generating unit tests with clean-test
 	}
 
 instance docDescription ModuleDoc
@@ -37,12 +46,14 @@ derive gDefault ModuleDoc
  * Documentation of a Clean function.
  */
 :: FunctionDoc =
-	{ description :: Maybe Description
-	, params      :: [Description] //* Descriptions of the parameters
-	, vars        :: [Description] //* Descriptions of the type variables (for generics)
-	, results     :: [Description] //* Descriptions of the result(s, for tuples)
-	, type        :: Maybe Type    //* The type (for macros)
-	, throws      :: [Description] //* The exceptions it may throw (iTasks)
+	{ description        :: Maybe Description
+	, params             :: [Description] //* Descriptions of the parameters
+	, vars               :: [Description] //* Descriptions of the type variables (for generics)
+	, results            :: [Description] //* Descriptions of the result(s, for tuples)
+	, type               :: Maybe Type    //* The type (for macros)
+	, throws             :: [Description] //* The exceptions it may throw (iTasks)
+	, properties         :: [Property]    //* Properties of this function
+	, property_test_with :: [PropertyVarInstantiation] //* With which types to test the properties
 	}
 
 instance docDescription FunctionDoc
@@ -51,7 +62,13 @@ instance docVars FunctionDoc
 instance docResults FunctionDoc
 instance docType FunctionDoc
 instance docThrows FunctionDoc
-derive gDefault FunctionDoc
+
+:: Property
+	= ForAll String [(String,Type)] String
+
+:: PropertyVarInstantiation = PropertyVarInstantiation (String, Type)
+
+derive gDefault FunctionDoc, Property, PropertyVarInstantiation
 
 /**
  * Documentation of a Clean class member.
@@ -129,6 +146,7 @@ derive gDefault TypeDoc
 	= MissingAsterisk String //* At least one line did not start with a *
 	| MissingField String    //* A required field was missing
 	| UnknownError String    //* Another error
+	| InternalNoDataError
 
 /**
  * Parse warning while parsing Clean documentation; the parser has made a

Doc.icl

 implementation module Doc
 
+import _SystemArray
 import StdBool
 import StdChar
 import StdDebug
 from StdFunc import flip, o, twice
 import StdList
 import StdMisc
+import StdOrdList
 import StdString
 import StdTuple
 
 import Control.Applicative
-import Control.Monad
+import Control.Monad => qualified join
 import Data.Either
 from Data.Func import $
 import Data.Functor
@@ -18,13 +20,19 @@ import Data.GenDefault
 import Data.List
 import Data.Maybe
 import Data.Tuple
+from Text import class Text(join,split), instance Text String
+import qualified Text
 import Text.Language
+import Text.Parsers.Simple.ParserCombinators
 
 from TypeDef import :: Type, :: TypeRestriction
 import qualified TypeParse as T
 
 gDefault{|Maybe|} _ = Nothing
 
+fromMultiLine :: !MultiLineString -> String
+fromMultiLine (MultiLine s) = s
+
 instance docDescription ModuleDoc where docDescription d = d.ModuleDoc.description
 
 instance docDescription FunctionDoc where docDescription d = d.FunctionDoc.description
@@ -54,7 +62,8 @@ instance docConstructors   TypeDoc where docConstructors   d = d.TypeDoc.constru
 instance docRepresentation TypeDoc where docRepresentation d = d.TypeDoc.representation
 
 derive gDefault Type, TypeRestriction, ModuleDoc, FunctionDoc, ClassMemberDoc,
-	ConstructorDoc, ClassDoc, TypeDoc
+	ConstructorDoc, ClassDoc, TypeDoc, Property, PropertyVarInstantiation,
+	MultiLineString
 
 constructorToFunctionDoc :: !ConstructorDoc -> FunctionDoc
 constructorToFunctionDoc d =
@@ -84,7 +93,7 @@ parseDoc :: !String -> Either ParseError (d, [ParseWarning]) | docBlockToDoc{|*|
 parseDoc s = docBlockToDoc{|*|} (Left [s])
 
 generic docBlockToDoc d :: !(Either [String] DocBlock) -> Either ParseError (!d, ![ParseWarning])
-docBlockToDoc{|String|} (Left []) = Left (UnknownError "no string")
+docBlockToDoc{|String|} (Left []) = Left InternalNoDataError
 docBlockToDoc{|String|} (Left ss) = Right (toString $ trim $ fromString $ last ss, [])
 docBlockToDoc{|[]|} fx (Left ss) = (\vws -> (map fst vws, flatten (map snd vws)) ) <$> mapM fx (map (Left o pure) ss)
 docBlockToDoc{|Maybe|} fx (Left []) = Right (Nothing, [])
@@ -92,15 +101,18 @@ docBlockToDoc{|Maybe|} fx ss=:(Left _) = appFst Just <$> fx ss
 docBlockToDoc{|UNIT|} _ = Right (UNIT, [])
 docBlockToDoc{|PAIR|} fx fy db=:(Right _) = liftA2 (\(x,ws) (y,ws`) -> (PAIR x y, ws ++ ws`)) (fx db) (fy db)
 docBlockToDoc{|FIELD of d|} fx (Right db) = case fx (Left [v \\ (k,v) <- db | k matches d.gfd_name]) of
-	Right (f, ws) -> Right (FIELD f, ws)
-	Left _        -> Left (MissingField d.gfd_name)
+	Right (f, ws)            -> Right (FIELD f, ws)
+	Left InternalNoDataError -> Left (MissingField d.gfd_name)
+	Left e                   -> Left e
 where
 	(matches) infix 4 :: String String -> Bool
 	(matches) k name =
-		k == name ||
-		pluralise English k == name ||
-		k == "return" && name == "result" ||
-		k == "return" && name == "results"
+		k` == name ||
+		pluralise English k` == name ||
+		k` == "return" && name == "result" ||
+		k` == "return" && name == "results"
+	where
+		k` = {if (c == '-') '_' c \\ c <-: k}
 docBlockToDoc{|RECORD|} fx (Left [s]) = case parseDocBlock s of
 	Right (db, ws) -> case fx (Right db) of
 		Right (v, ws`) -> Right (RECORD v, ws ++ ws`)
@@ -115,14 +127,64 @@ docBlockToDoc{|EITHER|} fl fr doc = case fl doc of
 		Left _ -> Left e
 docBlockToDoc{|OBJECT|} fx doc = appFst OBJECT <$> fx doc
 
-docBlockToDoc{|Type|} (Left []) = Left (UnknownError "no type")
+docBlockToDoc{|MultiLineString|} (Left [s]) = Right (MultiLine $ trimMultiLine $ split "\n" s, [])
+
+docBlockToDoc{|Type|} (Left []) = Left InternalNoDataError
 docBlockToDoc{|Type|} (Left ss) = case [v \\ Just v <- map ('T'.parseType o fromString) ss] of
-	[] -> Left (UnknownError "no type")
+	[] -> Left (UnknownError "no parsable type")
 	vs -> Right (last vs, [])
 
+docBlockToDoc{|Property|} (Left [s]) = let [signature:property] = split "\n" s in
+		parseSignature signature >>= \(sig,ws1) ->
+		parseProperty property >>= \(prop,ws2) ->
+		Right (sig prop, ws1 ++ ws2)
+where
+	parseSignature :: !String -> Either ParseError (!String -> Property, ![ParseWarning])
+	parseSignature s = case parse parser (fromString s) of
+		Left es           -> Left (UnknownError "failed to parse property signature")
+		Right (name,args) -> Right (ForAll name args, [])
+	where
+		parser :: Parser Char (String, [(String, Type)])
+		parser = skipSpaces *>
+			pMany (pSatisfy \c -> c <> ':' && not (isSpace c)) >>= \name ->
+			skipSpaces *> pToken ':' *> skipSpaces *> pToken 'A' *> pToken '.' *>
+			pMany
+				(skipSpaces *>
+				(liftA2 tuple
+					(toString <$> pMany (pSatisfy (not o isSpace)))
+					(pList [skipSpaces,pToken ':',pToken ':',skipSpaces] *> pTypeWithColonOrSemicolon)
+				) <* skipSpaces) >>= \args ->
+			pure (toString name, args)
+
+		skipSpaces = pMany (pSatisfy isSpace) *> pYield undef
+		pTypeWithColonOrSemicolon = (pMany (pSatisfy \c -> c <> ':' && c <> ';') <* pOneOf [':;'])
+			>>= \t -> case 'T'.parseType t of
+				Nothing -> pError "type could not be parsed"
+				Just t  -> pure t
+
+	parseProperty :: ![String] -> Either ParseError (!String, ![ParseWarning])
+	parseProperty ss = Right (trimMultiLine ss, [])
+
+docBlockToDoc{|PropertyVarInstantiation|} (Left [s]) = case split "=" s of
+	[var:type:[]] -> case 'T'.parseType (fromString type) of
+		Just t -> Right (PropertyVarInstantiation ('Text'.trim var, t), [])
+		Nothing -> Left (UnknownError "type could not be parsed")
+	_ -> Left (UnknownError "property var instantiation could not be parsed")
+
 derive docBlockToDoc ModuleDoc, FunctionDoc, ClassMemberDoc, ConstructorDoc,
 	ClassDoc, TypeDoc
 
+trimMultiLine :: [String] -> String
+trimMultiLine ss = join "\n" [s % (trimn, size s - 1) \\ s <- ss]
+where
+	trimn = minList [i \\ Just i <- map (firstNonSpace 0) ss]
+
+	firstNonSpace :: !Int !String -> Maybe Int
+	firstNonSpace i s
+	| i >= size s   = Nothing
+	| isSpace s.[i] = firstNonSpace (i+1) s
+	| otherwise     = Just i
+
 :: DocBlock :== [(String, String)]
 
 parseDocBlock :: !String -> Either ParseError (DocBlock, [ParseWarning])
@@ -141,9 +203,9 @@ where
 		= parseFields rest` >>=
 			\(d,ws) -> appSnd ((++) ws) <$> parseFs field desc d
 	where
-		(field, [_:descline]) = span (not o isSpace) line
+		(field, descline) = span (not o isSpace) line
 		(restdesc, rest`) = span (\l -> isEmpty l || hd l <> '@') rest
-		desc = flatten $ intersperse ['\n'] [descline:restdesc]
+		desc = flatten $ intersperse ['\n'] $ if (isEmpty descline) restdesc [tl descline:restdesc]
 
 		parseFs :: [Char] [Char] DocBlock -> Either ParseError (DocBlock, [ParseWarning])
 		parseFs field val d = Right ([(toString field,toString val):d], [])

README.md

@@ -87,7 +87,8 @@ Some simple markup is allowed in documentation:
 ### Documentation fields
 
 The tables below describe which fields and documentation types can be used for
-different syntax elements, and what they should document.
+different syntax elements, and what they should document. An extension, to
+document test properties, is discussed below.
 
 |              | Description | `@param` | `@result` | `@type` | `@var` | `@representation` | `@throws`
 |--------------|-------------|----------|-----------|---------|--------|-------------------|----------
@@ -116,6 +117,24 @@ do), `CloogleDBFactory` can derive the type.</sup>
 | `@type`           | The type of a macro (without name and `::`)
 | `@var`            | Type variables of types, classes and generics
 
+### Property documentation
+
+With [clean-test][]'s `maketest` tool, [Gast][] test programs can be generated
+with properties from docblocks. For this, several additional fields can be
+used, which are further documented by [clean-test][]:
+
+- `@property` on functions describes the actual property to test. An example
+  is: `@property plus_commutative: A. x :: a; y :: a: x + y == y + x`. This
+  will test the property `\x y -> x + y == y + x` where `x` and `y` are of type
+  `a`.
+- `@property-test-with` indicates how to instantiate type variables (it is not
+  always required). For the above property, suitable doclines are
+  `@property-test-with a = Int` and `@property-test-with a = Real`. This
+  docfield has to be given on the same function as the corresponding
+  `@property`.
+- `@property-bootstrap` on a module can be used to add bootstrap code, like
+  imports, to the generated test program.
+
 ## Copyright &amp; License
 Copyright &copy; 2016-present Mart Lubbers and Camil Staps.
 Licensed under MIT; See the [LICENSE](/LICENSE) file.
@@ -123,5 +142,7 @@ Licensed under MIT; See the [LICENSE](/LICENSE) file.
 [Clean]: http://clean.cs.ru.nl
 [Cloogle]: https://cloogle.org
 [cocl]: https://svn.cs.ru.nl/repos/clean-compiler
+[clean-test]: https://gitlab.science.ru.nl/clean-and-itasks/clean-test
+[Gast]: https://gitlab.science.ru.nl/clean-and-itasks/gast
 
 [y]: http://i.stack.imgur.com/iro5J.png

TypeTree.icl

@@ -12,7 +12,7 @@ import Data.GenLexOrd
 import Data.Graphviz
 import Data.List
 import Data.Tuple
-from Text import class Text(concat), instance Text String
+from Text import class Text(concat), instance Text String, <+
 import Text.GenJSON
 
 import TypeDef
@@ -44,21 +44,20 @@ typeTreeDepth (Node _ _ cs) = maxList [0:map ((+) 1 o typeTreeDepth) cs]
 addType :: !Type !v !(TypeTree v) -> TypeTree v
 addType t v tree=:(Node n vs children)
 | t generalises n
-	| n generalises t = trace_n (t <+ " equivalent to " <+ n) Node n [v:vs] children
-	| otherwise       = trace_n (t <+ " generalises " <+ n) Node t [v] [tree]
+	| n generalises t = Node n [v:vs] children
+	| otherwise       = Node t [v] [tree]
 // A type may end up in different places when there are multiple types that
 // generalise it. We sort on the matching types here to avoid that as much as
 // is easily possible, because we want the tree to be as small as possible.
 | otherwise = case appFst sort $ partition (\(Node t` _ _) -> t` generalises t) children of
-	([],_) -> trace_n (t <+ " added to " <+ n) Node n vs [Node t [v] yes:no]
+	([],_) -> Node n vs [Node t [v] yes:no]
 		with (yes,no) = partition (\(Node c _ _) -> t generalises c) children
 	([g:gs],rest) -> Node n vs ([addType t v g:gs] ++ rest)
 
 findUnifying :: !Type !(TypeTree v) -> [(Type,Unifier,[v])]
 findUnifying t tree=:(Node n ls cs) = case unify t n of
-	Nothing -> trace_n ("NO\t" +++ toString n) []
-	Just tvas -> trace_n ("YES\t" +++ toString n)
-		[(n,finish_unification [] tvas,ls):concatMap (findUnifying t) cs]
+	Nothing -> []
+	Just tvas -> [(n,finish_unification [] tvas,ls):concatMap (findUnifying t) cs]
 
 allTypes :: (TypeTree v) -> [(Type,[v],[TypeTree v])]
 allTypes (Node t vs cs) = [(t,vs,cs):concatMap allTypes cs]
@@ -77,10 +76,3 @@ typeTreeToGraphviz tree = Digraph
 	Nothing
 where
 	nodes = [(t,cs) \\ (t,vs,cs) <- allTypes tree | length vs > 1 || length cs > 0]
-
-from Text import <+
-instance toString Type where toString t = concat $ print False t
-// Debugging:
-//import StdDebug
-// No debugging:
-trace_n _ x = x