<commit_before>/// Types and backend for emitting Horn clauses for HSF consumption.
module Starling.Horn

open Chessie.ErrorHandling
open Starling.Collections
open Starling.Utils
open Starling.Var
open Starling.Expr
open Starling.Model
open Starling.Reifier
open Starling.Errors.Horn

/// A literal in a Datalog-style Horn clause.
/// We model Datalog terms as Starling expressions, refusing those
/// expressions not modellable in Datalog at output time.
/// Only arithmetic expressions can be modelled in HSF, so we disallow
/// Booleans.
type Literal = 
    /// A predicate.
    | Pred of Func<ArithExpr>
    | And of Literal list
    | Or of Literal list
    | True
    | False
    | ITE of Literal * Literal * Literal
    | Eq of ArithExpr * ArithExpr
    | Neq of ArithExpr * ArithExpr
    | Gt of ArithExpr * ArithExpr
    | Ge of ArithExpr * ArithExpr
    | Le of ArithExpr * ArithExpr
    | Lt of ArithExpr * ArithExpr

/// A Horn clause, in Datalog/HSF form.
type Horn = 
    /// A normal Horn clause.
    | Clause of head: Literal * body: (Literal list)
    /// A comment.
    | Comment of string
    /// A query-naming call.
    | QueryNaming of Func<string>


(*
 * Expression generation
 *)

/// Checks whether an ArithExpr is useable by HSF.
let checkArith =
    function
    | AAdd [] -> EmptyCompoundExpr "addition" |> fail
    | ASub [] -> EmptyCompoundExpr "subtraction" |> fail
    | AMul [] -> EmptyCompoundExpr "multiplication" |> fail
    | x -> ok x

/// Converts a BoolExpr to a HSF literal.
let rec boolExpr =
    function
    // TODO(CaptainHayashi): are these allowed?
    | BAnd xs -> List.map boolExpr xs |> collect |> lift And
    | BOr xs -> List.map boolExpr xs |> collect |> lift Or
    | BTrue -> ok <| True
    | BFalse -> ok <| False
    | BEq(AExpr x, AExpr y) -> lift2 (curry Eq) (checkArith x) (checkArith y)
    | BNot(BEq(AExpr x, AExpr y)) -> lift2 (curry Neq) (checkArith x) (checkArith y)
    | BGt(x, y) -> lift2 (curry Gt) (checkArith x) (checkArith y)
    | BGe(x, y) -> lift2 (curry Ge) (checkArith x) (checkArith y)
    | BLe(x, y) -> lift2 (curry Le) (checkArith x) (checkArith y)
    | BLt(x, y) -> lift2 (curry Lt) (checkArith x) (checkArith y)
    | x -> fail <| UnsupportedExpr(BExpr x)

(*
 * Func sanitisation
 *)

/// Extracts an ArithExpr from an Expr, if it is indeed arithmetic.
/// Fails with UnsupportedExpr if the expresson is Boolean.
let tryArithExpr =
    function
    | AExpr x -> x |> ok
    | e -> e |> UnsupportedExpr |> fail

/// Ensures a param in a viewdef multiset is arithmetic.
let ensureArith =
   function
   | (Type.Int, x) -> ok (aUnmarked x)
   | x -> fail <| NonArithParam x

/// Constructs a pred from a Func, given a set of active globals,
/// and some validator on the parameters.
let predOfFunc gs parT { Name = n; Params = pars } =
    lift (fun parR -> Pred { Name = n; Params = parR })
         (pars |> Seq.map parT |> collect)
(*
 * View definitions
 *)

/// Generates a query_naming clause for a viewdef.
let queryNaming { Name = n; Params = ps } =
    QueryNaming {Name = n; Params = ps |> List.map snd}

/// Constructs a full constraint in HSF.
/// The map of active globals should be passed as gs.
/// Some is returned if the constraint is definite; None otherwise.
let hsfViewDef gs { View = vs; Def = ex } =
    Option.map (fun dex ->
        lift2 (fun hd bd -> [ queryNaming vs
                              Clause (hd, [bd]) ])
              (boolExpr dex)
              (predOfFunc gs ensureArith vs)) ex

/// Constructs a set of Horn clauses for all definite viewdefs in a model.
let hsfModelViewDefs gs =
    Seq.choose (hsfViewDef gs)
    >> collect
    >> lift (List.concat >> Set.ofSeq)

(*
 * Variables
 *)

/// Constructs a Horn clause for initialising an integer variable.
/// Returns an error if the variable is not an integer.
/// Returns no clause if the variable is not initialised.
/// Takes the environment of active global variables.
let hsfModelVariables gs =
    let vpars =
        gs
        |> Map.toSeq
        |> Seq.map
            (fun (name, ty) -><commit_msg>Emit query_naming for indefinite viewdefs.<commit_after>/// Types and backend for emitting Horn clauses for HSF consumption.
module Starling.Horn

open Chessie.ErrorHandling
open Starling.Collections
open Starling.Utils
open Starling.Var
open Starling.Expr
open Starling.Model
open Starling.Reifier
open Starling.Errors.Horn

/// A literal in a Datalog-style Horn clause.
/// We model Datalog terms as Starling expressions, refusing those
/// expressions not modellable in Datalog at output time.
/// Only arithmetic expressions can be modelled in HSF, so we disallow
/// Booleans.
type Literal = 
    /// A predicate.
    | Pred of Func<ArithExpr>
    | And of Literal list
    | Or of Literal list
    | True
    | False
    | ITE of Literal * Literal * Literal
    | Eq of ArithExpr * ArithExpr
    | Neq of ArithExpr * ArithExpr
    | Gt of ArithExpr * ArithExpr
    | Ge of ArithExpr * ArithExpr
    | Le of ArithExpr * ArithExpr
    | Lt of ArithExpr * ArithExpr

/// A Horn clause, in Datalog/HSF form.
type Horn = 
    /// A normal Horn clause.
    | Clause of head: Literal * body: (Literal list)
    /// A comment.
    | Comment of string
    /// A query-naming call.
    | QueryNaming of Func<string>


(*
 * Expression generation
 *)

/// Checks whether an ArithExpr is useable by HSF.
let checkArith =
    function
    | AAdd [] -> EmptyCompoundExpr "addition" |> fail
    | ASub [] -> EmptyCompoundExpr "subtraction" |> fail
    | AMul [] -> EmptyCompoundExpr "multiplication" |> fail
    | x -> ok x

/// Converts a BoolExpr to a HSF literal.
let rec boolExpr =
    function
    // TODO(CaptainHayashi): are these allowed?
    | BAnd xs -> List.map boolExpr xs |> collect |> lift And
    | BOr xs -> List.map boolExpr xs |> collect |> lift Or
    | BTrue -> ok <| True
    | BFalse -> ok <| False
    | BEq(AExpr x, AExpr y) -> lift2 (curry Eq) (checkArith x) (checkArith y)
    | BNot(BEq(AExpr x, AExpr y)) -> lift2 (curry Neq) (checkArith x) (checkArith y)
    | BGt(x, y) -> lift2 (curry Gt) (checkArith x) (checkArith y)
    | BGe(x, y) -> lift2 (curry Ge) (checkArith x) (checkArith y)
    | BLe(x, y) -> lift2 (curry Le) (checkArith x) (checkArith y)
    | BLt(x, y) -> lift2 (curry Lt) (checkArith x) (checkArith y)
    | x -> fail <| UnsupportedExpr(BExpr x)

(*
 * Func sanitisation
 *)

/// Extracts an ArithExpr from an Expr, if it is indeed arithmetic.
/// Fails with UnsupportedExpr if the expresson is Boolean.
let tryArithExpr =
    function
    | AExpr x -> x |> ok
    | e -> e |> UnsupportedExpr |> fail

/// Ensures a param in a viewdef multiset is arithmetic.
let ensureArith =
   function
   | (Type.Int, x) -> ok (aUnmarked x)
   | x -> fail <| NonArithParam x

/// Constructs a pred from a Func, given a set of active globals,
/// and some validator on the parameters.
let predOfFunc gs parT { Name = n; Params = pars } =
    lift (fun parR -> Pred { Name = n; Params = parR })
         (pars |> Seq.map parT |> collect)
(*
 * View definitions
 *)

/// Generates a query_naming clause for a viewdef.
let queryNaming { Name = n; Params = ps } =
    QueryNaming {Name = n; Params = ps |> List.map snd}

/// Constructs a full constraint in HSF.
/// The map of active globals should be passed as gs.
/// Some is returned if the constraint is definite; None otherwise.
let hsfViewDef gs { View = vs; Def = ex } =
    let clause =
        Option.map (fun dex ->
            lift2 (fun hd bd -> Clause (hd, [bd]))
                  (boolExpr dex)
                  (predOfFunc gs ensureArith vs)) ex
    match clause with
    | Some cl -> lift (fun c -> [ queryNaming vs; c ]) cl
    | None -> ok [ queryNaming vs ]

/// Constructs a set of Horn clauses for all definite viewdefs in a model.
let hsfModelViewDefs gs =
    Seq.map (hsfViewDef gs)
    >> collect
    >> lift (List.concat >> Set.ofSeq)

(*
 * Variables
 *)

/// Constructs a Horn clause for initialising an integer variable.
/// Returns an error if the variable is not an integer.
/// Returns no clause if the variable is not initialised.
/// Takes the environment of active global variables.
let hsfModelVariables gs =
    let vpars =
        gs
        |> Map.toSeq
        |> Seq.map
            (fun (name, ty) ->
{'fraction_non_alphanumeric': 0.10903614457831326, 'fraction_numerical': 0.0016867469879518072, 'mean_word_length': 2.5489525438221463, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 98, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4830459', 'n_tokens_mistral': 2793, 'n_tokens_neox': 2704, 'n_words': 1026}