<commit_before>module Starling.Tests.Modeller

open Chessie.ErrorHandling  // ok
open Fuchu                  // general test framework
open Microsoft.Z3           // anything involving ctx
open Starling
open Starling.AST

/// Assertion that converting the arithmetic expression `expr` to Z3
/// yields the given AST.
let assertZ3ArithExpr ctx expr z3 =
    Assert.Equal ( Starling.Pretty.AST.printExpression expr
                   + " -Z3-> " + z3.ToString ()
                 , Starling.Modeller.arithExprToZ3 ctx expr
                 , ok z3
                 )

/// Assertion that converting the Boolean expression `expr` to Z3
/// yields the given AST.
let assertZ3BoolExpr ctx expr z3 =
    Assert.Equal ( Starling.Pretty.AST.printExpression expr
                   + " -Z3-> " + z3.ToString ()
                 , Starling.Modeller.boolExprToZ3 ctx expr
                 , ok z3
                 )

let testExprToZ3 ctx =
    testList "Test translation of expressions" [
        testList "Test translation of arithmetic expressions" [
            testCase "Test arithmetic-only expressions" <|
                fun _ -> assertZ3ArithExpr ctx
                                    ( AddExp ( MulExp ( IntExp 1L
                                                    , IntExp 2L
                                                    )
                                            , IntExp 3L
                                            )
                                    )
                                    ( ctx.MkAdd [| ctx.MkMul [| ctx.MkInt 1 :> ArithExpr
                                                            ; ctx.MkInt 2 :> ArithExpr
                                                            |]
                                                ; ctx.MkInt 3 :> ArithExpr
                                                |]
                                    )
        ]
        testList "Test translation of Boolean expressions" [
            testCase "Test Boolean-only expressions" <|
                fun _ -> assertZ3BoolExpr ctx
                                    ( AndExp ( OrExp ( TrueExp
                                                    , TrueExp
                                                    )
                                            , FalseExp
                                            )
                                    )
                                    ( ctx.MkAnd [| ctx.MkOr [| ctx.MkTrue ()
                                                            ; ctx.MkTrue ()
                                                            |]
                                                ; ctx.MkFalse ()
                                                |])
        ]
    ]

let testModelVarListNoDuplicates ctx =
    testList "Test modelling of variables forbids duplicates"
        [ testCase "Forbid duplicate with same type"
          <| fun _ -> Assert.Equal ("bool foo; bool foo -> error",
                                    Starling.Modeller.modelVarList ctx [ (Bool, "foo")
                                                                         (Bool, "foo") ],
                                    fail <| Starling.Errors.Modeller.VEDuplicate "foo")
          testCase "Forbid duplicate with different type"
          <| fun _ -> Assert.Equal ("bool foo; int foo -> error",
                                    Starling.Modeller.modelVarList ctx [ (Bool, "foo")
                                                                         (Int, "foo") ],
                                    fail <| Starling.Errors.Modeller.VEDuplicate "foo")
        ]

let testModelVars ctx =
    testList "Test modelling of variables"
        [ testModelVarListNoDuplicates ctx ]

[<Tests>]
let testZ3 =
    let ctx = new Context ()
    let t = testList "Test the Z3 translation"
                     [ testExprToZ3 ctx
                       testModelVars ctx ]
    ctx.Dispose ()
    t
<commit_msg>Get some abortive test stuff out of the way.<commit_after>module Starling.Tests.Modeller

open Chessie.ErrorHandling  // ok
open Fuchu                  // general test framework
open Microsoft.Z3           // anything involving ctx
open Starling
open Starling.AST

/// Assertion that converting the arithmetic expression `expr` to Z3
/// yields the given AST.
let assertZ3ArithExpr ctx expr z3 =
    Assert.Equal (Starling.Pretty.AST.printExpression expr
                   + " -Z3-> " + z3.ToString (),
                  Starling.Modeller.arithExprToZ3 ctx expr,
                  ok z3)

/// Assertion that converting the Boolean expression `expr` to Z3
/// yields the given AST.
let assertZ3BoolExpr ctx expr z3 =
    Assert.Equal (Starling.Pretty.AST.printExpression expr
                   + " -Z3-> " + z3.ToString (),
                  Starling.Modeller.boolExprToZ3 ctx expr,
                  ok z3)

let testExprToZ3 ctx =
    testList "Test translation of expressions" [
        testList "Test translation of arithmetic expressions" [
            testCase "Test arithmetic-only expressions" <|
                fun _ ->
                    assertZ3ArithExpr ctx
                                      (AddExp (MulExp (IntExp 1L,
                                                       IntExp 2L),
                                               IntExp 3L))
                                      (ctx.MkAdd [| ctx.MkMul [| ctx.MkInt 1 :> ArithExpr
                                                                 ctx.MkInt 2 :> ArithExpr |]
                                                    ctx.MkInt 3 :> ArithExpr |]) ]
        testList "Test translation of Boolean expressions" [
            testCase "Test Boolean-only expressions" <|
                fun _ ->
                    assertZ3BoolExpr ctx
                                     (AndExp (OrExp (TrueExp,
                                                     TrueExp),
                                             FalseExp))
                                     (ctx.MkAnd [| ctx.MkOr [| ctx.MkTrue ()
                                                               ctx.MkTrue () |]
                                                   ctx.MkFalse () |]) ]]

let testModelVarListNoDuplicates ctx =
    testList "Test modelling of variables forbids duplicates"
        [ testCase "Forbid duplicate with same type"
          <| fun _ -> Assert.Equal ("bool foo; bool foo -> error",
                                    fail <| Starling.Errors.Modeller.VEDuplicate "foo",
                                    Starling.Modeller.modelVarList ctx [ (Bool, "foo")
                                                                         (Bool, "foo") ])
          testCase "Forbid duplicate with different type"
          <| fun _ -> Assert.Equal ("bool foo; int foo -> error",
                                    fail <| Starling.Errors.Modeller.VEDuplicate "foo",
                                    Starling.Modeller.modelVarList ctx [ (Bool, "foo")
                                                                         (Int, "foo") ])
        ]

let testModelVars ctx =
    testList "Test modelling of variables"
        [ testModelVarListNoDuplicates ctx ]

        (*
let testTicketedLock =
    testCase "Test that the ticketed lock produces the correct model" <|
    fun _ ->
        Assert.Equal
            "ticketed lock collation -> ticketed lock model"
            {
            }
            (Starling.Modeller.model
            *)


[<Tests>]
let testModeller =
    let ctx = new Context ()
    let t = testList "Test the modeller"
                     [ testExprToZ3 ctx
                       testModelVars ctx
                       (*testTicketedLock*) ]
    ctx.Dispose ()
    t

{'fraction_non_alphanumeric': 0.07126137841352406, 'fraction_numerical': 0.006762028608582575, 'mean_word_length': 0.9505452700989094, 'pattern_counts': {'":': 0, '<': 18, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 83, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6563850', 'n_tokens_mistral': 1750, 'n_tokens_neox': 1668, 'n_words': 473}