<commit_before>﻿#light "off"
module FStar.Tactics.Basic
open FStar
open FStar.ST
open FStar.All
open FStar.Syntax.Syntax
open FStar.Util
open FStar.Ident
open FStar.TypeChecker.Env

module SP = FStar.Syntax.Print
module S = FStar.Syntax.Syntax
module SS = FStar.Syntax.Subst
module SF = FStar.Syntax.Free
module PC = FStar.Parser.Const
module U = FStar.Syntax.Util
module BU = FStar.Util
module Env = FStar.TypeChecker.Env
module Rel = FStar.TypeChecker.Rel
module Print = FStar.Syntax.Print
module TcUtil = FStar.TypeChecker.Util
module TcTerm = FStar.TypeChecker.TcTerm
module N = FStar.TypeChecker.Normalize
module RD = FStar.Reflection.Data
module UF = FStar.Syntax.Unionfind

type name = bv
type env = Env.env
type implicits = Env.implicits

// Beta reduce
let bnorm e t = N.normalize [] e t

(*
   f: x:int -> P
   ==================
      P
 *)
//A goal is typically of the form
//    G |- ?u : t
// where context = G
//       witness = ?u, although, more generally, witness is a partial solution and can be any term
//       goal_ty = t
type goal = {
    context : env;
    witness : term;
    goal_ty : typ;
    opts    : FStar.Options.optionstate; // option state for this particular goal
}

type proofstate = {
    main_context : env;          //the shared top-level context for all goals
    main_goal    : goal;         //this is read only; it helps keep track of the goal we started working on initially
    all_implicits: implicits ;   //all the implicits currently open, partially resolved (unclear why we really need this)
    goals        : list<goal>;   //all the goals remaining to be solved
    smt_goals    : list<goal>;   //goals that have been deferred to SMT
}

type result<'a> =
    | Success of 'a * proofstate
    | Failed  of string    //error message
              * proofstate //the proofstate at time of failure

(* An exception, typically used only to simplify local data flow,
                 although, when not handled, it signifies a fatal error
                           in the tactic engine
*)
exception TacFailure of string

(* The main monad for tactics.
 * A record, so we can keep it somewhat encapsulated and
 * can more easily add things to it if need be.
 *)
type tac<'a> = {
    tac_f : proofstate -> result<'a>;
}

let mk_tac (f : proofstate -> result<'a>) : tac<'a> =
    { tac_f = f }

let run t p = t.tac_f p

(* monadic return *)
let ret (x:'a) : tac<'a> =
    mk_tac (fun p -> Success (x, p))

(* monadic bind *)
let bind (t1:tac<'a>) (t2:'a -> tac<'b>) : tac<'b> =
    mk_tac (fun p ->
            match run t1 p with
            | Success (a, q)  -> run (t2 a) q
            | Failed (msg, q) -> Failed (msg, q))

let idtac : tac<unit> = ret ()

let goal_to_string (g:goal) =
    let g_binders = Env.all_binders g.context |> Print.binders_to_string ", " in
    Util.format3 "%s |- %s : %s" g_binders (Print.term_to_string g.witness) (Print.term_to_string g.goal_ty)

let tacprint  (s:string)       = BU.print1 "TAC>> %s\n" s
let tacprint1 (s:string) x     = BU.print1 "TAC>> %s\n" (BU.format1 s x)
let tacprint2 (s:string) x y   = BU.print1 "TAC>> %s\n" (BU.format2 s x y)
let tacprint3 (s:string) x y z = BU.print1 "TAC>> %s\n" (BU.format3 s x y z)

(* TODO: If I define this as *)
(*     (U.comp_to_comp_typ c).result_typ *)
(*     then I get  *)
(*     Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. *)
(*     Assertion failed: Computation type without universe *)
let comp_to_typ (c:comp) : typ =
    match c.n with
    | Total (t, _)
    | GTotal (t, _) -> t
    | Comp ct -> ct.result_typ

let is_irrelevant (g:goal) : bool =
    match U.un_squash (N.unfold_whnf g.context g.goal_ty) with
    | Some t -> true
    | _ -> false

let dump_goal ps goal =
    tacprint (goal_to_string goal);
    ()

let dump_cur ps msg =
    match ps.goals with
    | [] ->
        tacprint1 "No more goals (%s)" msg
    | h::_ ->
        begin
        tacprint1 "Current goal (%s):" msg;
        dump_goal ps (List.hd ps.goals)
        end

let dump_proofstate ps msg =
    tacprint "";
    tacprint1 "State dump (%s):" msg;
    tacprint1 "ACTIVE goals (%s):" (string_of_int (List.length ps.goals));
    List.iter (dump_goal ps) ps.goals;
    tacprint1 "SMT goals (%s):" (string_of_int (List.length ps.smt_goals));
    List.iter (dump_goal ps) ps.smt_goals;
    ()

let print_proof_state1 (msg:string) : tac<unit> =
    mk_tac (fun p -> dump_cur p msg;
                     Success ((), p))

let print_proof_state (msg:string) : tac<unit> =
    mk_tac (fun p -> dump_proofstate p msg;
                     Success ((), p))

(* get : get the current proof state *)
let get : tac<proofstate> =
    mk_tac (fun p -> Success (p, p))

let tac_verb_dbg : ref<option<bool>> = BU.mk_ref None
let rec log ps f : unit =
    match !tac_verb_dbg with
    | None -> (tac_verb_dbg := Some (Env.debug ps.main_context (Options.Other "TacVerbose"));
               log ps f)
    | Some true -> f ()
    | Some false -> ()

let mlog f : tac<unit> =
    bind get (fun ps -> log ps f; ret ())

//val fail : string -> tac<'a>
let fail msg =
    mk_tac (fun ps ->
        if Env.debug ps.main_context (Options.Other "TacFail")
        then dump_proofstate ps ("TACTING FAILING: " ^ msg);
        Failed (msg, ps)
    )

let fail1 msg x     = fail (BU.format1 msg x)
let fail2 msg x y   = fail (BU.format2 msg x y)
let fail3 msg x y z = fail (BU.format3 msg x y z)

let trytac (t : tac<'a>) : tac<option<'a>> =
    mk_tac (fun ps ->
            let tx = UF.new_transaction () in
            match run t ps with
            | Success (a, q) ->
                UF.commit tx;
                Success (Some a, q)
            | Failed (_, _) ->
                UF.rollback tx;
                Success (None, ps)
           )

////////////////////////////////////////////////////////////////////
(* Some TRUSTED internal utilities *)

(* set : set the current proof state; shouldn't be exposed externally *)
let set (p:proofstate) : tac<unit> =
    mk_tac (fun _ -> Success ((), p))

let solve goal solution =
    if Rel.teq_nosmt goal.context goal.witness solution
    then ()
    else raise (TacFailure(BU.format3 "%s does not solve %s : %s"
                          (Print.term_to_string solution)
                          (Print.term_to_string goal.witness)
                          (Print.term_to_string goal.goal_ty)))

let dismiss : tac<unit> =
    bind get (fun p ->
    set ({p with goals=List.tl p.goals}))

let dismiss_all : tac<unit> =
    bind get (fun p ->
    set ({p with goals=[]}))

let add_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with goals=gs@p.goals}))

let add_smt_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with smt_goals=gs@p.smt_goals}))

let push_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with goals=p.goals@gs}))

let push_smt_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with smt_goals=p.smt_goals@gs}))

let replace_cur (g:goal) : tac<unit> =
    bind dismiss (fun _ ->
    add_goals [g])

let add_implicits (i:implicits) : tac<unit> =
    bind get (fun p ->
    set ({p with all_implicits=i@p.all_implicits}))

let new_uvar (env:env) (typ:typ) : tac<(term * guard_t)> =
    let u, _, g_u = TcUtil.new_implicit_var "tactics.new_uvar" typ.pos env typ in
    bind (add_implicits g_u.implicits) (fun _ ->
    ret (u, g_u))

//Any function that directly calls these utilities is also trusted
//End: Trusted utilities
////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////
(* Some utilities on goals *)
let is_true t =
    match U.un_squash t with
    | Some t' ->
        begin match (SS.compress t').n with
        | Tm_fvar fv -> S.fv_eq_lid fv PC.true_lid
        | _ -> false
        end
    | _ -> false

let is_false t =
    match U.un_squash t with
    | Some t' ->
        begin match (SS.compress t').n with
        | Tm_fvar fv -> S.fv_eq_lid fv PC.false_lid
        | _ -> false
        end
    | _ -> false
////////////////////////////////////////////////////////////////////


let cur_goal : tac<goal> =
    bind get (fun p ->
    match p.goals with
    | [] -> fail "No more goals (1)"
    | hd::tl -> ret hd)

let add_irrelevant_goal (env:env) (phi:typ) opts : tac<unit> =
    let typ = U.mk_squash phi in
    bind (new_uvar env typ) (fun (u, g_u) ->
    let goal = { context = env; witness = u; goal_ty = typ; opts = opts } in
    add_goals [goal])

let smt : tac<unit> =
    bind cur_goal (fun g ->
    if is_irrelevant g then
        bind dismiss (fun _ -> add_smt_goals [g])
    else
        fail1 "goal is not irrelevant: cannot dispatch to smt (%s)" (Print.term_to_string g.goal_ty)
    )

let divide (n:int) (l : tac<'a>) (r : tac<'b>) : tac<('a * 'b)> =
    bind get (fun p ->
    bind (try ret (List.splitAt n p.goals) with | _ -> fail "divide: not enough goals") (fun (lgs, rgs) ->
    let lp = {p with goals=lgs; smt_goals=[]} in
    let rp = {p with goals=rgs; smt_goals=[]} in
    bind (set lp) (fun _ ->
    bind l        (fun a ->
    bind get      (fun lp' ->
    bind (set rp) (fun _ ->
    bind r        (fun b ->
    bind get      (fun rp' ->
    let p' = {p with goals=lp'.goals@rp'.goals; smt_goals=lp'.smt_goals@rp'.smt_goals@p.smt_goals} in
    bind (set p') (fun _ ->
    ret (a, b))))))))))
    
(* focus: runs f on the current goal only, and then restores all the goals *)
(* There is a user defined version as well, we just use this one internally, but can't mark it as private *)
let focus (f:tac<'a>) : tac<'a> =
    bind (divide 1 f idtac) (fun (a, ()) -> ret a)

(* Applies t to each of the current goals
      fails if t fails on any of the goals
      collects each result in the output list *)
let rec map (tau:tac<'a>): tac<(list<'a>)> =
        bind get (fun p ->
        match p.goals with
        | [] -> ret []
        | _::_ ->
            bind (divide 1 tau (map tau)) (fun (h,t) -> ret (h :: t))
        )

(* Applies t1 to the current head goal
   And t2 to all the the sub-goals produced by t1

   Collects the resulting goals of t2 along with the initial auxiliary goals
 *)
let seq (t1:tac<unit>) (t2:tac<unit>) : tac<unit> =
    focus (
        bind t1 (fun _ ->
        bind (map t2) (fun _ -> ret ()))
    )

let intro : tac<binder> =
    bind cur_goal (fun goal ->
    match U.arrow_one goal.goal_ty with
    | Some (b, c) ->
        let bs, c = SS.open_comp [b] c in
        let b = match bs with
                | [b] -> b
                | _ -> failwith "impossible: open_comp returned different amount of binders"
        in
        if not (U.is_total_comp c)
        then fail "Codomain is effectful"
        else let env' = Env.push_binders goal.context [b] in
             let typ' = comp_to_typ c in
             bind (new_uvar env' typ') (fun (u, g) ->
             if Rel.teq_nosmt goal.context goal.witness (U.abs [b] u None)
             then bind (replace_cur ({ goal with context = env';
                                                 goal_ty = bnorm env' typ';
                                                 witness = bnorm env' u})) (fun _ ->
                  ret b)
             else fail "intro: unification failed"
             )
    | None ->
        fail1 "intro: goal is not an arrow (%s)" (Print.term_to_string goal.goal_ty)
    )

// TODO: missing: precedes clause, and somehow disabling fixpoints only as needed
let intro_rec : tac<(binder * binder)> =
    bind cur_goal (fun goal ->
    BU.print_string "WARNING (intro_rec): calling this is known to cause normalizer loops\n";
    BU.print_string "WARNING (intro_rec): proceed at your own risk...\n";
    match U.arrow_one goal.goal_ty with
    | Some (b, c) ->
        let bs, c = SS.open_comp [b] c in
        let b = match bs with
                | [b] -> b
                | _ -> failwith "impossible: open_comp returned different amount of binders"
        in
        if not (U.is_total_comp c)
        then fail "Codomain is effectful"
        else let bv = gen_bv "__recf" None goal.goal_ty in
             let bs = [S.mk_binder bv; b] in // recursively bound name and argument we're introducing
             let env' = Env.push_binders goal.context bs in
             bind (new_uvar env' (comp_to_typ c)) (fun (u, g) ->
             let lb = U.mk_letbinding (Inl bv) [] goal.goal_ty PC.effect_Tot_lid (U.abs [b] u None) in
             let body = S.bv_to_name bv in
             let lbs, body = SS.close_let_rec [lb] body in
             let tm = mk (Tm_let ((true, lbs), body)) None goal.witness.pos in
             BU.print_string "calling teq_nosmt\n";
             let res = Rel.teq_nosmt goal.context goal.witness tm in
             if res
             then bind (replace_cur ({ goal with context = env';
                                                 goal_ty = bnorm env' (comp_to_typ c);
                                                 witness = bnorm env' u})) (fun _ ->
                  ret (S.mk_binder bv, b))
             else fail "intro_rec: unification failed"
             )
    | None ->
        fail1 "intro_rec: goal is not an arrow (%s)" (Print.term_to_string goal.goal_ty)
    )

let norm (s : list<RD.norm_step>) : tac<unit> =
    bind cur_goal (fun goal ->
    // Translate to actual normalizer steps
    let tr s = match s with
        | RD.Simpl   -> [N.Simplify]
        | RD.WHNF    -> [N.WHNF]
        | RD.Primops -> [N.Primops]
        | RD.Delta   -> [N.UnfoldUntil Delta_constant]
    in
    let steps = [N.Reify; N.UnfoldTac]@(List.flatten (List.map tr s)) in
    let w = N.normalize steps goal.context goal.witness in
    let t = N.normalize steps goal.context goal.goal_ty in
    replace_cur ({goal with goal_ty = t; witness = w})
    )

let istrivial (e:env) (t:term) : bool =
    let steps = [N.Reify; N.UnfoldUntil Delta_constant; N.Primops; N.Simplify; N.UnfoldTac] in
    let t = N.normalize steps e t in
    is_true t

let trivial : tac<unit> =
    bind cur_goal (fun goal ->
    if istrivial goal.context goal.goal_ty
    then (solve goal U.exp_unit; dismiss)
    else fail1 "Not a trivial goal: %s" (Print.term_to_string goal.goal_ty)
    )

let exact (t:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (try ret (goal.context.type_of goal.context t)
          with e -> // printfn "Exception %A" e;
                    fail2 "exact: term is not typeable: %s (%s)" (Print.term_to_string t) (Print.tag_of_term t)) (fun (t, typ, guard) ->
    if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "exact: got non-trivial guard" else
    if Rel.teq_nosmt goal.context typ goal.goal_ty
    then let _ = solve goal t in dismiss
    else fail3 "%s : %s does not exactly solve the goal %s"
                    (Print.term_to_string t)
                    (Print.term_to_string (bnorm goal.context typ))
                    (Print.term_to_string goal.goal_ty)))

let exact_lemma (t:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (try ret (TcTerm.tc_term goal.context t)
          with e -> // printfn "Exception %A" e;
                    fail2 "exact_lemma: term is not typeable: %s (%s)" (Print.term_to_string t) (Print.tag_of_term t)) (fun (t, lcomp, guard) ->
    let comp = lcomp.comp () in
    if not (U.is_lemma_comp comp) then fail "exact_lemma: not a lemma" else
    if not (Rel.is_trivial guard) then fail "exact: got non-trivial guard" else
    let pre, post = match (U.comp_to_comp_typ comp).effect_args with
                    | pre::post::_ -> fst pre, fst post
                    | _ -> failwith "exact_lemma: impossible: not a lemma"
    in
    if Rel.teq_nosmt goal.context post goal.goal_ty
    then let _ = solve goal t in bind dismiss (fun _ -> add_irrelevant_goal goal.context pre goal.opts)
    else fail3 "%s : %s does not exactly solve the goal %s"
                    (Print.term_to_string t)
                    (Print.term_to_string post)
                    (Print.term_to_string goal.goal_ty)))

let uvar_free_in_goal (u:uvar) (g:goal) =
    let free_uvars = List.map fst (BU.set_elements (SF.uvars g.goal_ty)) in
    List.existsML (UF.equiv u) free_uvars

let uvar_free (u:uvar) (ps:proofstate) : bool =
    List.existsML (uvar_free_in_goal u) ps.goals

// uopt: Don't add goals for implicits that appear free in posterior goals.
// This is very handy for users, allowing to turn
//
// |- a = c
//
// by applying transivity to
//
// |- a = ?u
// |- ?u = c
//
// without asking for ?u first, which will most likely be instantiated when
// solving any of these two goals. In any case, if ?u is not solved, we fail afterwards.
let rec __apply (uopt:bool) (tm:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (trytac (exact tm)) (fun r ->
    match r with
    | Some r -> ret r // if tm is a solution, we're done
    | None ->
        // exact failed, try to instantiate more arguments
        let tm, typ, guard = goal.context.type_of goal.context tm in
        if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "apply: got non-trivial guard" else
        match U.arrow_one typ with
        | None -> fail1 "apply: cannot unify (%s)" (Print.term_to_string typ)
        | Some ((bv, aq), c) ->
            if not (U.is_total_comp c) then fail "apply: not total" else
            bind (new_uvar goal.context bv.sort) (fun (u, g_u) ->
            let tm' = mk_Tm_app tm [(u, aq)] None goal.context.range in
            bind (__apply uopt tm') (fun _ ->
            match (SS.compress (fst (U.head_and_args u))).n with
            | Tm_uvar (uvar, _) ->
                bind get (fun ps ->
                if uopt && uvar_free uvar ps
                then ret ()
                else add_goals [{context = goal.context;
                                 witness = bnorm goal.context u;
                                 goal_ty = bnorm goal.context bv.sort;
                                 opts    = goal.opts; }])
            | _ -> ret ()))))

let apply (tm:term) : tac<unit> =
    // Focus not really needed, but might help a bit for speed
    focus (__apply true tm)

let apply_lemma (tm:term) : tac<unit> =
    bind cur_goal (fun goal ->
    let tm, t, guard = goal.context.type_of goal.context tm in
    if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "apply_lemma: got non-trivial guard" else
    let bs, comp = U.arrow_formals_comp t in
    if not (U.is_lemma_comp comp) then fail "apply_lemma: not a lemma" else
    let uvs, implicits, subst =
       List.fold_left (fun (uvs, guard, subst) (b, aq) ->
               let b_t = SS.subst subst b.sort in
               let u, _, g_u = FStar.TypeChecker.Util.new_implicit_var "apply_lemma" goal.goal_ty.pos goal.context b_t in
               (u, aq)::uvs,
               FStar.TypeChecker.Rel.conj_guard guard g_u,
               S.NT(b, u)::subst)
       ([], guard, [])
       bs
    in
    let uvs = List.rev uvs in
    let comp = SS.subst_comp subst comp in
    let pre, post = match (U.comp_to_comp_typ comp).effect_args with
                    | pre::post::_ -> fst pre, fst post
                    | _ -> failwith "apply_lemma: impossible: not a lemma"
    in
    match Rel.try_teq false goal.context (U.mk_squash post) goal.goal_ty with
    | None -> fail2 "apply_lemma: does not unify with goal: %s vs %s"
                                 (Print.term_to_string (U.mk_squash post))
                                 (Print.term_to_string goal.goal_ty)
    | Some g ->
        let _ = Rel.discharge_guard_no_smt goal.context g in
        let solution = S.mk_Tm_app tm uvs None goal.context.range in
        let implicits = implicits.implicits |> List.filter (fun (_, _, _, tm, _, _) ->
             let hd, _ = U.head_and_args tm in
             match (SS.compress hd).n with
             | Tm_uvar _ -> true //still unresolved
             | _ -> false) in
        solve goal solution;
        bind dismiss (fun _ ->
        let is_free_uvar uv t =
            let free_uvars = List.map fst (BU.set_elements (SF.uvars t)) in
            List.existsML (fun u -> UF.equiv u uv) free_uvars
        in
        let appears uv goals = List.existsML (fun g' -> is_free_uvar uv g'.goal_ty) goals in
        let checkone t goals =
            let hd, _ = U.head_and_args t in
            begin match hd.n with
            | Tm_uvar (uv, _) -> appears uv goals
            | _ -> false
            end
        in
        let sub_goals =
             implicits |> List.map (fun (_msg, _env, _uvar, term, typ, _) ->
                     {context = goal.context;
                      witness = bnorm goal.context term;
                      goal_ty = bnorm goal.context typ;
                      opts    = goal.opts; })
        in
        // Optimization: if a uvar appears in a later goal, don't ask for it, since
        // it will be instantiated later. TODO: maybe keep and check later?
        let rec filter' (f : 'a -> list<'a> -> bool) (xs : list<'a>) : list<'a> =
             match xs with
             | [] -> []
             | x::xs -> if f x xs then x::(filter' f xs) else filter' f xs
        in
        let sub_goals = filter' (fun g goals -> not (checkone g.witness goals)) sub_goals in
        bind (add_irrelevant_goal goal.context pre goal.opts) (fun _ ->
        // Try to discharge the precondition, which is often trivial
        bind (trytac trivial) (fun _ ->
        bind (add_implicits g.implicits) (fun _ ->
        add_goals sub_goals)))))

let rewrite (h:binder) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (mlog <| (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (Print.bv_to_string (fst h)) (Print.term_to_string (fst h).sort))) (fun _ ->
    match U.destruct_typ_as_formula (fst <| Env.lookup_bv goal.context (fst h)) with
    | Some (U.BaseConn(l, [_; (x, _); (e, _)]))
              when Ident.lid_equals l PC.eq2_lid ->
      (match (SS.compress x).n with
       | Tm_name x ->
         let goal = {goal with goal_ty=SS.subst [NT(x, e)] goal.goal_ty; witness = SS.subst [NT(x, e)] goal.witness} in
         replace_cur goal
       | _ ->
         fail "Not an equality hypothesis with a variable on the LHS")
    | _ -> fail "Not an equality hypothesis"))

let clear : tac<unit> =
    bind cur_goal (fun goal ->
    match Env.pop_bv goal.context with
    | None -> fail "Cannot clear; empty context"
    | Some (x, env') ->
        let fns_ty = FStar.Syntax.Free.names goal.goal_ty in
        let fns_tm = FStar.Syntax.Free.names goal.witness in
        if Util.set_mem x fns_ty
        then fail "Cannot clear; variable appears in goal"
        else bind (new_uvar env' goal.goal_ty) (fun (u, g) ->
             if not (Rel.teq_nosmt goal.context goal.witness u)
             then fail "clear: unification failed"
             else let new_goal = {goal with context = env'; witness = bnorm env' u} in
                  bind dismiss (fun _ ->
                  add_goals [new_goal])))

let clear_hd (x:name) : tac<unit> =
    bind cur_goal (fun goal ->
    match Env.pop_bv goal.context with
    | None -> fail "Cannot clear_hd; empty context"
    | Some (y, env') ->
        if not (S.bv_eq x y)
        then fail "Cannot clear_hd; head variable mismatch"
        else clear)

let revert : tac<unit> =<commit_msg>***NO_CI*** removing a needless free name computation<commit_after>﻿#light "off"
module FStar.Tactics.Basic
open FStar
open FStar.ST
open FStar.All
open FStar.Syntax.Syntax
open FStar.Util
open FStar.Ident
open FStar.TypeChecker.Env

module SP = FStar.Syntax.Print
module S = FStar.Syntax.Syntax
module SS = FStar.Syntax.Subst
module SF = FStar.Syntax.Free
module PC = FStar.Parser.Const
module U = FStar.Syntax.Util
module BU = FStar.Util
module Env = FStar.TypeChecker.Env
module Rel = FStar.TypeChecker.Rel
module Print = FStar.Syntax.Print
module TcUtil = FStar.TypeChecker.Util
module TcTerm = FStar.TypeChecker.TcTerm
module N = FStar.TypeChecker.Normalize
module RD = FStar.Reflection.Data
module UF = FStar.Syntax.Unionfind

type name = bv
type env = Env.env
type implicits = Env.implicits

// Beta reduce
let bnorm e t = N.normalize [] e t

(*
   f: x:int -> P
   ==================
      P
 *)
//A goal is typically of the form
//    G |- ?u : t
// where context = G
//       witness = ?u, although, more generally, witness is a partial solution and can be any term
//       goal_ty = t
type goal = {
    context : env;
    witness : term;
    goal_ty : typ;
    opts    : FStar.Options.optionstate; // option state for this particular goal
}

type proofstate = {
    main_context : env;          //the shared top-level context for all goals
    main_goal    : goal;         //this is read only; it helps keep track of the goal we started working on initially
    all_implicits: implicits ;   //all the implicits currently open, partially resolved (unclear why we really need this)
    goals        : list<goal>;   //all the goals remaining to be solved
    smt_goals    : list<goal>;   //goals that have been deferred to SMT
}

type result<'a> =
    | Success of 'a * proofstate
    | Failed  of string    //error message
              * proofstate //the proofstate at time of failure

(* An exception, typically used only to simplify local data flow,
                 although, when not handled, it signifies a fatal error
                           in the tactic engine
*)
exception TacFailure of string

(* The main monad for tactics.
 * A record, so we can keep it somewhat encapsulated and
 * can more easily add things to it if need be.
 *)
type tac<'a> = {
    tac_f : proofstate -> result<'a>;
}

let mk_tac (f : proofstate -> result<'a>) : tac<'a> =
    { tac_f = f }

let run t p = t.tac_f p

(* monadic return *)
let ret (x:'a) : tac<'a> =
    mk_tac (fun p -> Success (x, p))

(* monadic bind *)
let bind (t1:tac<'a>) (t2:'a -> tac<'b>) : tac<'b> =
    mk_tac (fun p ->
            match run t1 p with
            | Success (a, q)  -> run (t2 a) q
            | Failed (msg, q) -> Failed (msg, q))

let idtac : tac<unit> = ret ()

let goal_to_string (g:goal) =
    let g_binders = Env.all_binders g.context |> Print.binders_to_string ", " in
    Util.format3 "%s |- %s : %s" g_binders (Print.term_to_string g.witness) (Print.term_to_string g.goal_ty)

let tacprint  (s:string)       = BU.print1 "TAC>> %s\n" s
let tacprint1 (s:string) x     = BU.print1 "TAC>> %s\n" (BU.format1 s x)
let tacprint2 (s:string) x y   = BU.print1 "TAC>> %s\n" (BU.format2 s x y)
let tacprint3 (s:string) x y z = BU.print1 "TAC>> %s\n" (BU.format3 s x y z)

(* TODO: If I define this as *)
(*     (U.comp_to_comp_typ c).result_typ *)
(*     then I get  *)
(*     Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. *)
(*     Assertion failed: Computation type without universe *)
let comp_to_typ (c:comp) : typ =
    match c.n with
    | Total (t, _)
    | GTotal (t, _) -> t
    | Comp ct -> ct.result_typ

let is_irrelevant (g:goal) : bool =
    match U.un_squash (N.unfold_whnf g.context g.goal_ty) with
    | Some t -> true
    | _ -> false

let dump_goal ps goal =
    tacprint (goal_to_string goal);
    ()

let dump_cur ps msg =
    match ps.goals with
    | [] ->
        tacprint1 "No more goals (%s)" msg
    | h::_ ->
        begin
        tacprint1 "Current goal (%s):" msg;
        dump_goal ps (List.hd ps.goals)
        end

let dump_proofstate ps msg =
    tacprint "";
    tacprint1 "State dump (%s):" msg;
    tacprint1 "ACTIVE goals (%s):" (string_of_int (List.length ps.goals));
    List.iter (dump_goal ps) ps.goals;
    tacprint1 "SMT goals (%s):" (string_of_int (List.length ps.smt_goals));
    List.iter (dump_goal ps) ps.smt_goals;
    ()

let print_proof_state1 (msg:string) : tac<unit> =
    mk_tac (fun p -> dump_cur p msg;
                     Success ((), p))

let print_proof_state (msg:string) : tac<unit> =
    mk_tac (fun p -> dump_proofstate p msg;
                     Success ((), p))

(* get : get the current proof state *)
let get : tac<proofstate> =
    mk_tac (fun p -> Success (p, p))

let tac_verb_dbg : ref<option<bool>> = BU.mk_ref None
let rec log ps f : unit =
    match !tac_verb_dbg with
    | None -> (tac_verb_dbg := Some (Env.debug ps.main_context (Options.Other "TacVerbose"));
               log ps f)
    | Some true -> f ()
    | Some false -> ()

let mlog f : tac<unit> =
    bind get (fun ps -> log ps f; ret ())

//val fail : string -> tac<'a>
let fail msg =
    mk_tac (fun ps ->
        if Env.debug ps.main_context (Options.Other "TacFail")
        then dump_proofstate ps ("TACTING FAILING: " ^ msg);
        Failed (msg, ps)
    )

let fail1 msg x     = fail (BU.format1 msg x)
let fail2 msg x y   = fail (BU.format2 msg x y)
let fail3 msg x y z = fail (BU.format3 msg x y z)

let trytac (t : tac<'a>) : tac<option<'a>> =
    mk_tac (fun ps ->
            let tx = UF.new_transaction () in
            match run t ps with
            | Success (a, q) ->
                UF.commit tx;
                Success (Some a, q)
            | Failed (_, _) ->
                UF.rollback tx;
                Success (None, ps)
           )

////////////////////////////////////////////////////////////////////
(* Some TRUSTED internal utilities *)

(* set : set the current proof state; shouldn't be exposed externally *)
let set (p:proofstate) : tac<unit> =
    mk_tac (fun _ -> Success ((), p))

let solve goal solution =
    if Rel.teq_nosmt goal.context goal.witness solution
    then ()
    else raise (TacFailure(BU.format3 "%s does not solve %s : %s"
                          (Print.term_to_string solution)
                          (Print.term_to_string goal.witness)
                          (Print.term_to_string goal.goal_ty)))

let dismiss : tac<unit> =
    bind get (fun p ->
    set ({p with goals=List.tl p.goals}))

let dismiss_all : tac<unit> =
    bind get (fun p ->
    set ({p with goals=[]}))

let add_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with goals=gs@p.goals}))

let add_smt_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with smt_goals=gs@p.smt_goals}))

let push_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with goals=p.goals@gs}))

let push_smt_goals (gs:list<goal>) : tac<unit> =
    bind get (fun p ->
    set ({p with smt_goals=p.smt_goals@gs}))

let replace_cur (g:goal) : tac<unit> =
    bind dismiss (fun _ ->
    add_goals [g])

let add_implicits (i:implicits) : tac<unit> =
    bind get (fun p ->
    set ({p with all_implicits=i@p.all_implicits}))

let new_uvar (env:env) (typ:typ) : tac<(term * guard_t)> =
    let u, _, g_u = TcUtil.new_implicit_var "tactics.new_uvar" typ.pos env typ in
    bind (add_implicits g_u.implicits) (fun _ ->
    ret (u, g_u))

//Any function that directly calls these utilities is also trusted
//End: Trusted utilities
////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////
(* Some utilities on goals *)
let is_true t =
    match U.un_squash t with
    | Some t' ->
        begin match (SS.compress t').n with
        | Tm_fvar fv -> S.fv_eq_lid fv PC.true_lid
        | _ -> false
        end
    | _ -> false

let is_false t =
    match U.un_squash t with
    | Some t' ->
        begin match (SS.compress t').n with
        | Tm_fvar fv -> S.fv_eq_lid fv PC.false_lid
        | _ -> false
        end
    | _ -> false
////////////////////////////////////////////////////////////////////


let cur_goal : tac<goal> =
    bind get (fun p ->
    match p.goals with
    | [] -> fail "No more goals (1)"
    | hd::tl -> ret hd)

let add_irrelevant_goal (env:env) (phi:typ) opts : tac<unit> =
    let typ = U.mk_squash phi in
    bind (new_uvar env typ) (fun (u, g_u) ->
    let goal = { context = env; witness = u; goal_ty = typ; opts = opts } in
    add_goals [goal])

let smt : tac<unit> =
    bind cur_goal (fun g ->
    if is_irrelevant g then
        bind dismiss (fun _ -> add_smt_goals [g])
    else
        fail1 "goal is not irrelevant: cannot dispatch to smt (%s)" (Print.term_to_string g.goal_ty)
    )

let divide (n:int) (l : tac<'a>) (r : tac<'b>) : tac<('a * 'b)> =
    bind get (fun p ->
    bind (try ret (List.splitAt n p.goals) with | _ -> fail "divide: not enough goals") (fun (lgs, rgs) ->
    let lp = {p with goals=lgs; smt_goals=[]} in
    let rp = {p with goals=rgs; smt_goals=[]} in
    bind (set lp) (fun _ ->
    bind l        (fun a ->
    bind get      (fun lp' ->
    bind (set rp) (fun _ ->
    bind r        (fun b ->
    bind get      (fun rp' ->
    let p' = {p with goals=lp'.goals@rp'.goals; smt_goals=lp'.smt_goals@rp'.smt_goals@p.smt_goals} in
    bind (set p') (fun _ ->
    ret (a, b))))))))))

(* focus: runs f on the current goal only, and then restores all the goals *)
(* There is a user defined version as well, we just use this one internally, but can't mark it as private *)
let focus (f:tac<'a>) : tac<'a> =
    bind (divide 1 f idtac) (fun (a, ()) -> ret a)

(* Applies t to each of the current goals
      fails if t fails on any of the goals
      collects each result in the output list *)
let rec map (tau:tac<'a>): tac<(list<'a>)> =
        bind get (fun p ->
        match p.goals with
        | [] -> ret []
        | _::_ ->
            bind (divide 1 tau (map tau)) (fun (h,t) -> ret (h :: t))
        )

(* Applies t1 to the current head goal
   And t2 to all the the sub-goals produced by t1

   Collects the resulting goals of t2 along with the initial auxiliary goals
 *)
let seq (t1:tac<unit>) (t2:tac<unit>) : tac<unit> =
    focus (
        bind t1 (fun _ ->
        bind (map t2) (fun _ -> ret ()))
    )

let intro : tac<binder> =
    bind cur_goal (fun goal ->
    match U.arrow_one goal.goal_ty with
    | Some (b, c) ->
        let bs, c = SS.open_comp [b] c in
        let b = match bs with
                | [b] -> b
                | _ -> failwith "impossible: open_comp returned different amount of binders"
        in
        if not (U.is_total_comp c)
        then fail "Codomain is effectful"
        else let env' = Env.push_binders goal.context [b] in
             let typ' = comp_to_typ c in
             bind (new_uvar env' typ') (fun (u, g) ->
             if Rel.teq_nosmt goal.context goal.witness (U.abs [b] u None)
             then bind (replace_cur ({ goal with context = env';
                                                 goal_ty = bnorm env' typ';
                                                 witness = bnorm env' u})) (fun _ ->
                  ret b)
             else fail "intro: unification failed"
             )
    | None ->
        fail1 "intro: goal is not an arrow (%s)" (Print.term_to_string goal.goal_ty)
    )

// TODO: missing: precedes clause, and somehow disabling fixpoints only as needed
let intro_rec : tac<(binder * binder)> =
    bind cur_goal (fun goal ->
    BU.print_string "WARNING (intro_rec): calling this is known to cause normalizer loops\n";
    BU.print_string "WARNING (intro_rec): proceed at your own risk...\n";
    match U.arrow_one goal.goal_ty with
    | Some (b, c) ->
        let bs, c = SS.open_comp [b] c in
        let b = match bs with
                | [b] -> b
                | _ -> failwith "impossible: open_comp returned different amount of binders"
        in
        if not (U.is_total_comp c)
        then fail "Codomain is effectful"
        else let bv = gen_bv "__recf" None goal.goal_ty in
             let bs = [S.mk_binder bv; b] in // recursively bound name and argument we're introducing
             let env' = Env.push_binders goal.context bs in
             bind (new_uvar env' (comp_to_typ c)) (fun (u, g) ->
             let lb = U.mk_letbinding (Inl bv) [] goal.goal_ty PC.effect_Tot_lid (U.abs [b] u None) in
             let body = S.bv_to_name bv in
             let lbs, body = SS.close_let_rec [lb] body in
             let tm = mk (Tm_let ((true, lbs), body)) None goal.witness.pos in
             BU.print_string "calling teq_nosmt\n";
             let res = Rel.teq_nosmt goal.context goal.witness tm in
             if res
             then bind (replace_cur ({ goal with context = env';
                                                 goal_ty = bnorm env' (comp_to_typ c);
                                                 witness = bnorm env' u})) (fun _ ->
                  ret (S.mk_binder bv, b))
             else fail "intro_rec: unification failed"
             )
    | None ->
        fail1 "intro_rec: goal is not an arrow (%s)" (Print.term_to_string goal.goal_ty)
    )

let norm (s : list<RD.norm_step>) : tac<unit> =
    bind cur_goal (fun goal ->
    // Translate to actual normalizer steps
    let tr s = match s with
        | RD.Simpl   -> [N.Simplify]
        | RD.WHNF    -> [N.WHNF]
        | RD.Primops -> [N.Primops]
        | RD.Delta   -> [N.UnfoldUntil Delta_constant]
    in
    let steps = [N.Reify; N.UnfoldTac]@(List.flatten (List.map tr s)) in
    let w = N.normalize steps goal.context goal.witness in
    let t = N.normalize steps goal.context goal.goal_ty in
    replace_cur ({goal with goal_ty = t; witness = w})
    )

let istrivial (e:env) (t:term) : bool =
    let steps = [N.Reify; N.UnfoldUntil Delta_constant; N.Primops; N.Simplify; N.UnfoldTac] in
    let t = N.normalize steps e t in
    is_true t

let trivial : tac<unit> =
    bind cur_goal (fun goal ->
    if istrivial goal.context goal.goal_ty
    then (solve goal U.exp_unit; dismiss)
    else fail1 "Not a trivial goal: %s" (Print.term_to_string goal.goal_ty)
    )

let exact (t:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (try ret (goal.context.type_of goal.context t)
          with e -> // printfn "Exception %A" e;
                    fail2 "exact: term is not typeable: %s (%s)" (Print.term_to_string t) (Print.tag_of_term t)) (fun (t, typ, guard) ->
    if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "exact: got non-trivial guard" else
    if Rel.teq_nosmt goal.context typ goal.goal_ty
    then let _ = solve goal t in dismiss
    else fail3 "%s : %s does not exactly solve the goal %s"
                    (Print.term_to_string t)
                    (Print.term_to_string (bnorm goal.context typ))
                    (Print.term_to_string goal.goal_ty)))

let exact_lemma (t:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (try ret (TcTerm.tc_term goal.context t)
          with e -> // printfn "Exception %A" e;
                    fail2 "exact_lemma: term is not typeable: %s (%s)" (Print.term_to_string t) (Print.tag_of_term t)) (fun (t, lcomp, guard) ->
    let comp = lcomp.comp () in
    if not (U.is_lemma_comp comp) then fail "exact_lemma: not a lemma" else
    if not (Rel.is_trivial guard) then fail "exact: got non-trivial guard" else
    let pre, post = match (U.comp_to_comp_typ comp).effect_args with
                    | pre::post::_ -> fst pre, fst post
                    | _ -> failwith "exact_lemma: impossible: not a lemma"
    in
    if Rel.teq_nosmt goal.context post goal.goal_ty
    then let _ = solve goal t in bind dismiss (fun _ -> add_irrelevant_goal goal.context pre goal.opts)
    else fail3 "%s : %s does not exactly solve the goal %s"
                    (Print.term_to_string t)
                    (Print.term_to_string post)
                    (Print.term_to_string goal.goal_ty)))

let uvar_free_in_goal (u:uvar) (g:goal) =
    let free_uvars = List.map fst (BU.set_elements (SF.uvars g.goal_ty)) in
    List.existsML (UF.equiv u) free_uvars

let uvar_free (u:uvar) (ps:proofstate) : bool =
    List.existsML (uvar_free_in_goal u) ps.goals

// uopt: Don't add goals for implicits that appear free in posterior goals.
// This is very handy for users, allowing to turn
//
// |- a = c
//
// by applying transivity to
//
// |- a = ?u
// |- ?u = c
//
// without asking for ?u first, which will most likely be instantiated when
// solving any of these two goals. In any case, if ?u is not solved, we fail afterwards.
let rec __apply (uopt:bool) (tm:term) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (trytac (exact tm)) (fun r ->
    match r with
    | Some r -> ret r // if tm is a solution, we're done
    | None ->
        // exact failed, try to instantiate more arguments
        let tm, typ, guard = goal.context.type_of goal.context tm in
        if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "apply: got non-trivial guard" else
        match U.arrow_one typ with
        | None -> fail1 "apply: cannot unify (%s)" (Print.term_to_string typ)
        | Some ((bv, aq), c) ->
            if not (U.is_total_comp c) then fail "apply: not total" else
            bind (new_uvar goal.context bv.sort) (fun (u, g_u) ->
            let tm' = mk_Tm_app tm [(u, aq)] None goal.context.range in
            bind (__apply uopt tm') (fun _ ->
            match (SS.compress (fst (U.head_and_args u))).n with
            | Tm_uvar (uvar, _) ->
                bind get (fun ps ->
                if uopt && uvar_free uvar ps
                then ret ()
                else add_goals [{context = goal.context;
                                 witness = bnorm goal.context u;
                                 goal_ty = bnorm goal.context bv.sort;
                                 opts    = goal.opts; }])
            | _ -> ret ()))))

let apply (tm:term) : tac<unit> =
    // Focus not really needed, but might help a bit for speed
    focus (__apply true tm)

let apply_lemma (tm:term) : tac<unit> =
    bind cur_goal (fun goal ->
    let tm, t, guard = goal.context.type_of goal.context tm in
    if not (Rel.is_trivial <| Rel.discharge_guard goal.context guard) then fail "apply_lemma: got non-trivial guard" else
    let bs, comp = U.arrow_formals_comp t in
    if not (U.is_lemma_comp comp) then fail "apply_lemma: not a lemma" else
    let uvs, implicits, subst =
       List.fold_left (fun (uvs, guard, subst) (b, aq) ->
               let b_t = SS.subst subst b.sort in
               let u, _, g_u = FStar.TypeChecker.Util.new_implicit_var "apply_lemma" goal.goal_ty.pos goal.context b_t in
               (u, aq)::uvs,
               FStar.TypeChecker.Rel.conj_guard guard g_u,
               S.NT(b, u)::subst)
       ([], guard, [])
       bs
    in
    let uvs = List.rev uvs in
    let comp = SS.subst_comp subst comp in
    let pre, post = match (U.comp_to_comp_typ comp).effect_args with
                    | pre::post::_ -> fst pre, fst post
                    | _ -> failwith "apply_lemma: impossible: not a lemma"
    in
    match Rel.try_teq false goal.context (U.mk_squash post) goal.goal_ty with
    | None -> fail2 "apply_lemma: does not unify with goal: %s vs %s"
                                 (Print.term_to_string (U.mk_squash post))
                                 (Print.term_to_string goal.goal_ty)
    | Some g ->
        let _ = Rel.discharge_guard_no_smt goal.context g in
        let solution = S.mk_Tm_app tm uvs None goal.context.range in
        let implicits = implicits.implicits |> List.filter (fun (_, _, _, tm, _, _) ->
             let hd, _ = U.head_and_args tm in
             match (SS.compress hd).n with
             | Tm_uvar _ -> true //still unresolved
             | _ -> false) in
        solve goal solution;
        bind dismiss (fun _ ->
        let is_free_uvar uv t =
            let free_uvars = List.map fst (BU.set_elements (SF.uvars t)) in
            List.existsML (fun u -> UF.equiv u uv) free_uvars
        in
        let appears uv goals = List.existsML (fun g' -> is_free_uvar uv g'.goal_ty) goals in
        let checkone t goals =
            let hd, _ = U.head_and_args t in
            begin match hd.n with
            | Tm_uvar (uv, _) -> appears uv goals
            | _ -> false
            end
        in
        let sub_goals =
             implicits |> List.map (fun (_msg, _env, _uvar, term, typ, _) ->
                     {context = goal.context;
                      witness = bnorm goal.context term;
                      goal_ty = bnorm goal.context typ;
                      opts    = goal.opts; })
        in
        // Optimization: if a uvar appears in a later goal, don't ask for it, since
        // it will be instantiated later. TODO: maybe keep and check later?
        let rec filter' (f : 'a -> list<'a> -> bool) (xs : list<'a>) : list<'a> =
             match xs with
             | [] -> []
             | x::xs -> if f x xs then x::(filter' f xs) else filter' f xs
        in
        let sub_goals = filter' (fun g goals -> not (checkone g.witness goals)) sub_goals in
        bind (add_irrelevant_goal goal.context pre goal.opts) (fun _ ->
        // Try to discharge the precondition, which is often trivial
        bind (trytac trivial) (fun _ ->
        bind (add_implicits g.implicits) (fun _ ->
        add_goals sub_goals)))))

let rewrite (h:binder) : tac<unit> =
    bind cur_goal (fun goal ->
    bind (mlog <| (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (Print.bv_to_string (fst h)) (Print.term_to_string (fst h).sort))) (fun _ ->
    match U.destruct_typ_as_formula (fst <| Env.lookup_bv goal.context (fst h)) with
    | Some (U.BaseConn(l, [_; (x, _); (e, _)]))
              when Ident.lid_equals l PC.eq2_lid ->
      (match (SS.compress x).n with
       | Tm_name x ->
         let goal = {goal with goal_ty=SS.subst [NT(x, e)] goal.goal_ty; witness = SS.subst [NT(x, e)] goal.witness} in
         replace_cur goal
       | _ ->
         fail "Not an equality hypothesis with a variable on the LHS")
    | _ -> fail "Not an equality hypothesis"))

let clear : tac<unit> =
    bind cur_goal (fun goal ->
    match Env.pop_bv goal.context with
    | None -> fail "Cannot clear; empty context"
    | Some (x, env') ->
        let fns_ty = FStar.Syntax.Free.names goal.goal_ty in
//        let fns_tm = FStar.Syntax.Free.names goal.witness in
        if Util.set_mem x fns_ty
        then fail "Cannot clear; variable appears in goal"
        else bind (new_uvar env' goal.goal_ty) (fun (u, g) ->
             if not (Rel.teq_nosmt goal.context goal.witness u)
             then fail "clear: unification failed"
             else let new_goal = {goal with context = env'; witness = bnorm env' u} in
                  bind dismiss (fun _ ->
                  add_goals [new_goal])))

let clear_hd (x:name) : tac<unit> =
    bind cur_goal (fun goal ->
    match Env.pop_bv goal.context with
    | None -> fail "Cannot clear_hd; empty context"
    | Some (y, env') ->
        if not (S.bv_eq x y)
        then fail "Cannot clear_hd; head variable mismatch"
        else clear)

let revert : tac<unit> =
{'fraction_non_alphanumeric': 0.1271552646215719, 'fraction_numerical': 0.002182004877422667, 'mean_word_length': 2.0188569583467872, 'pattern_counts': {'":': 0, '<': 147, '<?xml version=': 0, '>': 449, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 2, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4421438', 'n_tokens_mistral': 16008, 'n_tokens_neox': 15503, 'n_words': 5190}