<commit_before>open Starling

open System
open CommandLine
open CommandLine.Text

open Fuchu
open FParsec // TODO: push fparsec references out of Main.

type Options = {
    [<Option('t',
             HelpText = "Ignore input and run regression tests.")>]
    test: bool;
    [<Option('p',
             HelpText = "Pretty-prints the input instead of attempting to verify it.")>]
    pprint: bool;
    [<Value(0,
            MetaName = "input",
            HelpText = "The file to load (omit, or supply -, for standard input).")>]
    input: string option;
}

let parseFile name pprint =
    let (stream, streamName) =
        match name with
            | Some("-") -> (Console.OpenStandardInput(),        "(stdin)")
            | None      -> (Console.OpenStandardInput(),        "(stdin)")
            | Some(nam) -> (IO.File.OpenRead(nam) :> IO.Stream, nam      )
    let pres = runParserOnStream Starling.Parser.parseScript () streamName stream Text.Encoding.UTF8
    match pres with
        | Success(result, _, _)   -> if pprint
                                     then printfn "%s" ( Starling.Pretty.printScript result )
                                     else printfn "Success: %A" result
        | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg

    0

let mainWithOptions opts argv =
    if opts.test
    then defaultMainThisAssembly argv
    else parseFile opts.input opts.pprint

[<EntryPoint>]
let main argv =
    let result = CommandLine.Parser.Default.ParseArguments<Options>(argv)
    match result with
        | :? Parsed<Options> as parsed -> mainWithOptions parsed.Value argv
        | :? NotParsed<Options> as notParsed -> printfn "failure: %A" notParsed.Errors
                                                2
        | _ -> printfn "parse result of unknown type"
               3<commit_msg>Hook up Z3 conversion demo to main.<commit_after>open Starling

open System
open CommandLine
open CommandLine.Text

open Fuchu
open FParsec // TODO: push fparsec references out of Main.
open Microsoft.Z3 // TODO: this too.

type Options = {
    [<Option('t',
             HelpText = "Ignore input and run regression tests.")>]
    test: bool;
    [<Option('p',
             HelpText = "Pretty-prints the input instead of attempting to verify it.")>]
    pprint: bool;
    [<Value(0,
            MetaName = "input",
            HelpText = "The file to load (omit, or supply -, for standard input).")>]
    input: string option;
}

/// Pretty-prints a Z3 conversion result.
let printCR cr =
    // TODO(CaptainHayashi): does this belong in the Z3 module?
    match cr with
        | Starling.Z3.Bool  b -> b.ToString ()
        | Starling.Z3.Arith a -> a.ToString ()
        | Starling.Z3.Fail  e -> "ERROR: " + e

/// Runs Starling on the given parsed script.
let runStarlingOnScript result =
    // TODO(CaptainHayashi): eventually this will run the actual prover
    printfn "AST: \n%A" result
    printfn "---"
    printfn "Constraints: \n"
    let ctx = new Context ()
    List.iter (
        fun vc ->
            printfn "  View: %s" <| Starling.Pretty.printView ( fst vc )
            printfn "    Z3: %s" <| printCR ( snd vc )
    ) <| Starling.Z3.scriptViewConstraintsZ3 ctx result
    printfn "---"

let parseFile name pprint =
    let (stream, streamName) =
        match name with
            | Some("-") -> (Console.OpenStandardInput(),        "(stdin)")
            | None      -> (Console.OpenStandardInput(),        "(stdin)")
            | Some(nam) -> (IO.File.OpenRead(nam) :> IO.Stream, nam      )
    let pres = runParserOnStream Starling.Parser.parseScript () streamName stream Text.Encoding.UTF8
    match pres with
        | Success(result, _, _)   -> if pprint
                                     then printfn "%s" ( Starling.Pretty.printScript result )
                                     else runStarlingOnScript result
        | Failure(errorMsg, _, _) -> printfn "Failure: %s" errorMsg

    0

let mainWithOptions opts argv =
    if opts.test
    then defaultMainThisAssembly argv
    else parseFile opts.input opts.pprint

[<EntryPoint>]
let main argv =
    let result = CommandLine.Parser.Default.ParseArguments<Options>(argv)
    match result with
        | :? Parsed<Options> as parsed -> mainWithOptions parsed.Value argv
        | :? NotParsed<Options> as notParsed -> printfn "failure: %A" notParsed.Errors
                                                2
        | _ -> printfn "parse result of unknown type"
               3
{'fraction_non_alphanumeric': 0.10774710596616206, 'fraction_numerical': 0.004452359750667854, 'mean_word_length': 2.073187414500684, 'pattern_counts': {'":': 0, '<': 20, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '147822', 'n_tokens_mistral': 1297, 'n_tokens_neox': 1271, 'n_words': 394}