<commit_before>﻿/// <summary>
///     Backend for emitting verification conditions in Grasshopper format
/// </summary>
module Starling.Backends.Grasshopper 

open Chessie.ErrorHandling

open Starling 
open Starling.Collections
open Starling.Utils
open Starling.Core.TypeSystem
open Starling.Core.Var
open Starling.Core.Expr
open Starling.Core.Model
open Starling.Core.Instantiate
open Starling.Core.GuardedView

[<AutoOpen>] 
module Types =
    type Grass = Backends.Z3.Types.ZModel  
    type Error = unit 

module Pretty = 
    let printQuery = 
        Backends.Z3.Pretty.printZTerm
        // failwith "not implemented yet" 

    let printGrassError e = 
        failwith "not implemented yet" 

let grassModel (i : Backends.Z3.Types.ZModel) : Result<Grass,Error>  = 
  ok i 
  // failwith "not implemented yet" <commit_msg>Hacked a pretty-printer for Grasshopper format<commit_after>﻿/// <summary>
///     Backend for emitting verification conditions in Grasshopper format
/// </summary>
module Starling.Backends.Grasshopper 

open Chessie.ErrorHandling

open Starling 
open Starling.Collections
open Starling.Utils
open Starling.Core.TypeSystem
open Starling.Core.Var
open Starling.Core.Expr
open Starling.Core.Model
open Starling.Core.Symbolic
open Starling.Core.Instantiate
open Starling.Core.GuardedView

[<AutoOpen>] 
module Types =
    type Grass = Backends.Z3.Types.ZModel // Just piggyback on Z3 for now.  
    type Error = unit 

module Pretty = 
    open Starling.Core.Pretty
    open Starling.Core.Model.Pretty
    open Starling.Core.Symbolic.Pretty

    let printMarkedVar =
        function
        | Before s -> String "before_" <-> String s 
        | After s -> String "after_" <-> String s
        | Intermediate (i, s) -> String "inter_" <-> String (sprintf "%A_" i) <-> String s 
        | Goal (i, s) -> String "goal_" <-> String (sprintf "%A_" i) <-> String s 

    // Print infix operator across multiple lines
    let infexprV (op : string) (pxs : 'x -> Doc) (xs : seq<'x>) : Doc = 
        let mapped = Seq.map pxs xs 
        let resseq = Seq.map (fun x -> vsep [(String op); Indent x]) (Seq.tail mapped) 
        hsep [Seq.head mapped; (hsep resseq)] 
        |> parened 

    // Print infix operator on one line
    let infexpr (op : string) (pxs : 'x -> Doc) (xs : seq<'x>) : Doc = 
        let mapped = Seq.map pxs xs 
        let resseq = Seq.map (fun x -> hsep [(String op); x]) (Seq.tail mapped) 
        hsep [Seq.head mapped; (hsep resseq)] 
        |> parened 

    /// Pretty-prints an arithmetic expression.
    let rec printIntExpr (pVar : 'Var -> Doc) : IntExpr<'Var> -> Doc =
        function
        | IVar c -> pVar c
        | _ -> failwith "Unimplemented" 

    /// Pretty-prints a Boolean expression.
    and printBoolExpr (pVar : 'Var -> Doc) : BoolExpr<'Var> -> Doc =
        function
        | BAnd xs -> infexprV "&&" (printBoolExpr pVar) xs
        | BOr xs -> infexprV "||" (printBoolExpr pVar) xs
        | BVar c -> pVar c
        | BImplies (x, y) -> infexprV "==>" (printBoolExpr pVar)  [x; y]
        | BNot (BEq (x, y)) -> infexpr "!=" (printExpr pVar) [x; y]
        | BEq (x, y) -> infexpr "==" (printExpr pVar) [x; y]
        | _ -> failwith "Unimplemented" 

    /// Pretty-prints an expression.
    and printExpr (pVar : 'Var -> Doc) : Expr<'Var> -> Doc =
        function
        | Int i -> printIntExpr pVar i
        | Bool b -> printBoolExpr pVar b
        | _ -> failwith "Unimplemented" 

    let rec printSym (pReg : 'Reg -> Doc) (sym : Sym<'Reg>) : Doc =
        match sym with
        | Reg r -> pReg r
        | Sym { Sentence = ws; Args = xs } ->
            let pArg = printExpr (printSym pReg)
            parened
                (printInterpolatedSymbolicSentence pArg ws xs)

    let printExprGrass a = 
        printBoolExpr (printSym printMarkedVar) a 

    let printQuery (zterm : Backends.Z3.Types.ZTerm) : Doc = 
        headed "Grasshopper terms" <| 
          [ printTerm
              (fun x -> String "Cmd printing not implemented yet.") 
              printExprGrass 
              printExprGrass 
              zterm.SymBool ]

    let printGrassError e = 
        failwith "not implemented yet" 

let grassModel (i : Backends.Z3.Types.ZModel) : Result<Grass,Error>  = 
  ok i 
{'fraction_non_alphanumeric': 0.11449309295247015, 'fraction_numerical': 0.001638960430812456, 'mean_word_length': 2.3219284603421464, 'pattern_counts': {'":': 0, '<': 24, '<?xml version=': 0, '>': 56, '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': '1622786', 'n_tokens_mistral': 1429, 'n_tokens_neox': 1367, 'n_words': 415}