<commit_before>/// <summary>
///     Part of the Starling tool that flattens terms, adding in globals.
/// </summary>
module Starling.Flattener

open Starling.Collections
open Starling.Core.TypeSystem
open Starling.Core.Expr
open Starling.Core.View
open Starling.Core.Symbolic
open Starling.Core.Model
open Starling.Core.Command
open Starling.Core.Var
open Starling.Core.GuardedView


(*
 * View-to-func flattening.
 *)

/// Extracts a sequence of all of the parameters in a view in order.
let paramsOfView ms =
    ms
    |> Seq.map (fun v -> v.Params)
    |> Seq.concat

/// Constructs a (hopefully) unique name for a func encompassing a view.
let funcNameOfView : Func<'a> seq ->  string =
    fun ms ->
    ms
    // These two steps are to ensure we don't capture an existing name.
    |> Seq.map (fun { Name = n } -> n.Replace("_", "__"))
    |> scons "v"
    |> String.concat "_"
    |> (fun s -> if s = "v" then "emp" else s)

/// Constructs a Func from a View, given a set of active globals in the
/// appropriate format for appending into the func's parameter list.
/// and some transformer from the parameters to expressions.
let funcOfView globals view =
    { Name = view |> funcNameOfView
      Params = view |> paramsOfView |> Seq.append globals |> List.ofSeq }

(*
 * View usages
 *)

/// Adds the globals in gs to the argument lists of a view assertion.
let addGlobalsToViewSet gs =
   Seq.map (mapItem (funcOfView gs)) >> Multiset.ofFlatSeq

/// Adds the globals in gs to the argument list of the assertions in a term.
let addGlobalsToTerm gs _ =
    mapTerm id
            (addGlobalsToViewSet (gs Before))
            (funcOfView (gs After))

(*
 * View definitions
 *)

/// Adds the globals in gs to a defining view.
let addGlobalsToViewDef gs =
    function
    | Definite (v, d) -> Definite (funcOfView gs v, d)
    | Indefinite v -> Indefinite (funcOfView gs v)

(*
 * Whole models
 *)

/// Adds globals to the arguments of all views in a model.
let flatten (mdl: UVModel<Term<'cmd, Set<GuardedSubview>, OView>>) =
    /// Build a function making a list of global arguments, for view assertions.
    let gargs marker = varMapToExprs (marker >> Reg) mdl.Globals

    /// Build a list of global parameters, for view definitions.
    let gpars =
        mdl.Globals
        |> Map.toSeq
        |> Seq.map (fun (name, ty) -> withType ty name)
        |> List.ofSeq

    {Globals = mdl.Globals
     Locals = mdl.Locals
     Axioms = Map.map (addGlobalsToTerm gargs) mdl.Axioms
     ViewDefs = List.map (addGlobalsToViewDef gpars) mdl.ViewDefs
     Semantics = mdl.Semantics}


/// <summary>
///     Tests for <c>Flattener</c>.
/// </summary>
module Tests =
    open NUnit.Framework
    open Chessie.ErrorHandling
    open Starling.Utils.Testing


    /// <summary>
    ///     NUnit tests for <c>Flattener</c>.
    /// </summary>
    type NUnit () =
        /// The globals environment used in the tests.
        static member Globals : VarMap =
            returnOrFail <| makeVarMap
                [ TypedVar.Int "serving"
                  TypedVar.Int "ticket" ]

        /// Test cases for the view func renamer.
        static member ViewFuncNamings =
            let ms : SMVFunc list -> OView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "foo"; Params = [] }
                                { Name = "bar_baz"; Params = [] } ])
                .Returns("v_bar__baz_foo") // Remember, multisets sort!
                .SetName("Encode func name of view 'foo() * bar_baz()' as 'v_bar__baz_foo'")
              TestCaseData(ms []).Returns("emp")
                .SetName("Encode func name of view '' as 'emp'") ]

        /// Tests the view predicate name generator.
        [<TestCaseSource("ViewFuncNamings")>]
        member x.``the flattened view name generator generates names correctly`` v =
            let pn : OView -> string = funcNameOfView
            pn v

        /// Test cases for the full defining-view func converter.
        /// These all use the Globals environment above.
        static member DViewFuncs =
            let ms : DFunc list -> DView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "holdLock"; Params = [] }
                                { Name = "holdTick"; Params = [ Int "t" ] } ])
                 .Returns({ Name = "v_holdLock_holdTick"
                            Params =
                                [ Int "serving"
                                  Int "ticket"
                                  Int "t" ] } : DFunc)
                .SetName("Convert defining view 'holdLock() * holdTick(t)' to defining func") ]

        /// Tests the viewdef LHS translator.
        [<TestCaseSource("DViewFuncs")>]
        member x.``the defining view func translator works correctly`` (v: DView) =
            v |> funcOfView (NUnit.Globals
                             |> Map.toSeq
                             |> Seq.map (fun (n, t) -> withType t n))

        /// Test cases for the full view func converter.
        /// These all use the Globals environment above.
        static member ViewFuncs =
            let ms : SMVFunc list -> OView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "holdLock"; Params = [] }
                                { Name = "holdTick"; Params = [ Expr.Int (siBefore "t") ] } ])
                 .Returns({ Name = "v_holdLock_holdTick"
                            Params =
                                [ Expr.Int (siBefore "serving")
                                  Expr.Int (siBefore "ticket")
                                  Expr.Int (siBefore "t") ] })
                .SetName("Convert 'holdLock() * holdTick(t)' to func") ]

        /// Tests the viewdef LHS translator.
        [<TestCaseSource("ViewFuncs")>]
        member x.``the view func translator works correctly`` (v: OView) =
            v |> funcOfView (NUnit.Globals
                             |> Map.toSeq
                             |> Seq.map (function
                                         | (x, Type.Int ()) -> x |> siBefore |> Expr.Int
                                         | (x, Type.Bool ()) -> x |> sbBefore |> Expr.Bool))
<commit_msg>Annotate, inner-rename, and clear up Flattener.<commit_after>/// <summary>
///     Part of the Starling tool that flattens terms, adding in globals.
/// </summary>
module Starling.Flattener

open Starling.Collections
open Starling.Core.TypeSystem
open Starling.Core.Expr
open Starling.Core.View
open Starling.Core.Symbolic
open Starling.Core.Model
open Starling.Core.Command
open Starling.Core.Var
open Starling.Core.GuardedView


/// <summary>
///     Extracts a sequence of all of the parameters in an func sequence
///     (OView or DView) in order.
/// </summary>
let paramsOfFuncSeq (funcs : Func<'var> seq) : 'var seq =
    funcs |> Seq.map (fun v -> v.Params) |> Seq.concat

/// <summary>
///     Constructs a (hopefully) unique name for a Func resulting from
///     the flattening of a func sequence (OView or DView).
/// </summary>
let genFlatFuncSeqName (funcs : Func<'var> seq) : string =
    funcs
    // These two steps are to ensure we don't capture an existing name.
    |> Seq.map (fun { Name = n } -> n.Replace("_", "__"))
    |> scons "v"
    |> String.concat "_"
    // This step ensures that the empty view is named 'emp', not 'v'.
    |> fun s -> if s = "v" then "emp" else s

/// <summary>
///     Constructs a Func from a func sequence, appending global variables.
/// </summary>
/// <param name="globals">
///     The set of active globals, in expression form, which will be appended
///     into the Func's parameter list.
/// </param>
/// <param name="funcs">
///     The Func sequence to flatten.
/// </param>
/// <returns>
///     A new SMVFunc containing all of the parameters of the constituent
///     funcs, as well as the globals list, and a new unique name.
/// </returns>
let flattenFuncSeq
  (globals : 'var seq)
  (oview : Func<'var> seq)
  : Func<'var> =
    { Name = genFlatFuncSeqName oview
      Params = oview |> paramsOfFuncSeq |> Seq.append globals |> List.ofSeq }

/// <summary>
///     Flattens a term by converting all of its OViews into single funcs.
/// </summary>
/// <param name="globalsF">
///     A function that takes a marker (Before, After, etc.) and returns
///     a sequence of all global variables converted into symbolic marked
///     expressions with said marker.
/// </param>
/// <returns>
///     A function mapping terms over OViews to terms over SMVFuncs.
/// </returns>
let flattenTerm
  (globalsF : (Var -> MarkedVar) -> SMExpr seq)
  : Term<_, Set<GuardedSubview>, OView> -> Term<_, SMGView, SMVFunc> =
    mapTerm id
            (Seq.map (mapItem (flattenFuncSeq (globalsF Before)))
             >> Multiset.ofFlatSeq)
            (flattenFuncSeq (globalsF After))

/// <summary>
///     Flattens a view definition by converting its DViews into single funcs.
/// </summary>
/// <param name="globalsP">
///     A sequence of formal parameters, representing each global variable in
///     the model, to append to the argument list of the flattened funcs.
/// </param>
/// <returns>
///     A function mapping view definitions over DViews to definitions over
///     SMVFuncs.
/// </returns>
let flattenViewDef
  (globalsP : TypedVar seq)
  : ViewDef<DView, _> -> ViewDef<DFunc, _> =
    function
    | Definite (v, d) -> Definite (flattenFuncSeq globalsP v, d)
    | Indefinite v -> Indefinite (flattenFuncSeq globalsP v)

/// <summary>
///    Flattens all func sequences in a model, turning them into funcs.
///    <para>
///        This allows each combination of views coming out of reification
///        to be represented by a single uninterpreted function, which can
///        then either be interpreted using the corresponding ViewDefs,
///        or inferred by using a solver like HSF.
///    </para>
/// </summary>
/// <param name="model">
///     The model to flatten.
/// </param>
/// <returns>
///     The flattened model.
/// </returns>
let flatten
  (model : UVModel<Term<_, Set<GuardedSubview>, OView>>)
  : UFModel<Term<_, SMGView, SMVFunc>> =
    /// Build a function making a list of global arguments, for view assertions.
    let globalsF marker = varMapToExprs (marker >> Reg) model.Globals

    /// Build a list of global parameters, for view definitions.
    let globalsP =
        model.Globals
        |> Map.toSeq
        |> Seq.map (fun (name, ty) -> withType ty name)
        |> List.ofSeq

    { Globals = model.Globals
      Locals = model.Locals
      Axioms = Map.map (fun _ x -> flattenTerm globalsF x) model.Axioms
      ViewDefs = List.map (flattenViewDef globalsP) model.ViewDefs
      Semantics = model.Semantics }


/// <summary>
///     Tests for <c>Flattener</c>.
/// </summary>
module Tests =
    open NUnit.Framework
    open Chessie.ErrorHandling
    open Starling.Utils.Testing


    /// <summary>
    ///     NUnit tests for <c>Flattener</c>.
    /// </summary>
    type NUnit () =
        /// The globals environment used in the tests.
        static member Globals : VarMap =
            returnOrFail <| makeVarMap
                [ TypedVar.Int "serving"
                  TypedVar.Int "ticket" ]

        /// Test cases for the view func renamer.
        static member ViewFuncNamings =
            let ms : SMVFunc list -> OView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "foo"; Params = [] }
                                { Name = "bar_baz"; Params = [] } ])
                .Returns("v_bar__baz_foo") // Remember, multisets sort!
                .SetName("Encode func name of view 'foo() * bar_baz()' as 'v_bar__baz_foo'")
              TestCaseData(ms []).Returns("emp")
                .SetName("Encode func name of view '' as 'emp'") ]

        /// Tests the view predicate name generator.
        [<TestCaseSource("ViewFuncNamings")>]
        member x.``the flattened view name generator generates names correctly`` v =
            (genFlatFuncSeqName : OView -> string) v

        /// Test cases for the full defining-view func converter.
        /// These all use the Globals environment above.
        static member DViewFuncs =
            let ms : DFunc list -> DView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "holdLock"; Params = [] }
                                { Name = "holdTick"; Params = [ Int "t" ] } ])
                 .Returns({ Name = "v_holdLock_holdTick"
                            Params =
                                [ Int "serving"
                                  Int "ticket"
                                  Int "t" ] } : DFunc)
                .SetName("Convert defining view 'holdLock() * holdTick(t)' to defining func") ]

        /// Tests the viewdef LHS translator.
        [<TestCaseSource("DViewFuncs")>]
        member x.``the defining view func translator works correctly`` (v : DView) =
            v
            |> flattenFuncSeq
                   (NUnit.Globals
                    |> Map.toSeq
                    |> Seq.map (fun (n, t) -> withType t n))

        /// Test cases for the full view func converter.
        /// These all use the Globals environment above.
        static member ViewFuncs =
            let ms : SMVFunc list -> OView = Multiset.ofFlatList >> Multiset.toFlatList
            [ TestCaseData(ms [ { Name = "holdLock"; Params = [] }
                                { Name = "holdTick"; Params = [ Expr.Int (siBefore "t") ] } ])
                 .Returns({ Name = "v_holdLock_holdTick"
                            Params =
                                [ Expr.Int (siBefore "serving")
                                  Expr.Int (siBefore "ticket")
                                  Expr.Int (siBefore "t") ] })
                .SetName("Convert 'holdLock() * holdTick(t)' to func") ]

        /// Tests the viewdef LHS translator.
        [<TestCaseSource("ViewFuncs")>]
        member x.``the view func translator works correctly`` (v : OView) =
            v
            |> flattenFuncSeq
                   (NUnit.Globals
                    |> Map.toSeq
                    |> Seq.map
                           (function
                            | (x, Type.Int ()) -> x |> siBefore |> Expr.Int
                            | (x, Type.Bool ()) -> x |> sbBefore |> Expr.Bool))

{'fraction_non_alphanumeric': 0.11897329171002428, 'fraction_numerical': 0.0, 'mean_word_length': 1.864295648718458, 'pattern_counts': {'":': 0, '<': 81, '<?xml version=': 0, '>': 177, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2789923', 'n_tokens_mistral': 4356, 'n_tokens_neox': 4165, 'n_words': 1349}