val filter_args_for_inv (args: list expr) (td: type_decl) : ML (list expr)
let filter_args_for_inv (args:list expr)
                        (td:type_decl)
  : ML (list expr)
  = let fvs = free_vars_of_inv_eloc td.inv_eloc in
    let args =
      List.map2
        (fun (b, _) a ->
          if Some? (List.tryFind (fun j -> A.ident_name b = A.ident_name j) fvs)
          then [a]
          else [])
        td.name.td_params
        args
    in
    List.flatten args
val filter_args_for_inv (args: list expr) (td: type_decl) : ML (list expr)
let filter_args_for_inv (args: list expr) (td: type_decl) : ML (list expr) =
let fvs = free_vars_of_inv_eloc td.inv_eloc in
let args =
  List.map2 (fun (b, _) a ->
        if Some? (List.tryFind (fun j -> A.ident_name b = A.ident_name j) fvs) then [a] else [])
    td.name.td_params
    args
in
List.flatten args
InterpreterTarget.fst.checked
Target.fsti.checked prims.fst.checked Hashtable.fsti.checked FStar.String.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.All.fst.checked Ast.fst.checked
InterpreterTarget.fst
Prims.list InterpreterTarget.expr InterpreterTarget.type_decl FStar.List.Tot.Base.flatten FStar.List.map2 FStar.Pervasives.Native.tuple2 Ast.with_meta_t Ast.ident' Target.typ Prims.Cons Prims.Nil Prims.bool FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.option FStar.List.tryFind Prims.op_Equality Prims.string Ast.ident_name Target.__proj__Mktypedef_name__item__td_params InterpreterTarget.__proj__Mktype_decl__item__name Ast.ident InterpreterTarget.free_vars_of_inv_eloc InterpreterTarget.__proj__Mktype_decl__item__inv_eloc
(*
   Copyright 2021 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module InterpreterTarget
(* The abstract syntax for the code produced by 3d, targeting prelude/Interpreter.fst *)
open FStar.All
open FStar.List.Tot
module A = Ast
module T = Target
module H = Hashtable

noeq
type inv =
  | Inv_true : inv
  | Inv_conj : inv -> inv -> inv
  | Inv_ptr  : A.ident -> inv
  | Inv_name : A.ident -> list expr -> inv

noeq
type eloc =
  | Eloc_none   : eloc
  | Eloc_output : eloc
  | Eloc_union  : eloc -> eloc -> eloc
  | Eloc_ptr    : A.ident -> eloc
  | Eloc_name   : A.ident -> list expr -> eloc

noeq
type on_success =
  | On_success : bool -> on_success
  | On_success_named : A.ident -> list expr -> on_success
  | On_success_union : on_success -> on_success -> on_success

let inv_eloc = inv & eloc & on_success
let inv_eloc_nil = Inv_true, Eloc_none, On_success false
let inv_eloc_union (i, e, b) (i', e', b') = Inv_conj i i', Eloc_union e e', On_success_union b b'
let inv_eloc_name hd args = Inv_name hd args, Eloc_name hd args, On_success_named hd args

let env = H.t A.ident' type_decl
let create_env (_:unit) : ML env = H.create 100

let rec free_vars_of_expr (e:T.expr)
  : ML (list A.ident)
  = let open T in
    match fst e with
    | Constant _ -> []
    | Identifier i -> [i]
    | App _ args -> List.collect free_vars_of_expr args
    | Record _ args -> List.collect (fun (_, e) -> free_vars_of_expr e) args

let rec free_vars_of_inv (i:inv)
  : ML (list A.ident)
  = match i with
    | Inv_true -> []
    | Inv_conj i j -> free_vars_of_inv i @ free_vars_of_inv j
    | Inv_ptr x -> [x]
    | Inv_name _ args -> List.collect free_vars_of_expr args

let rec free_vars_of_eloc (e:eloc)
  : ML (list A.ident)
  = match e with
    | Eloc_none
    | Eloc_output -> []
    | Eloc_union i j -> free_vars_of_eloc i @ free_vars_of_eloc j
    | Eloc_ptr x -> [x]
    | Eloc_name _ args -> List.collect free_vars_of_expr args

let free_vars_of_inv_eloc (i:inv_eloc) =
  let i, j, _ = i in
  free_vars_of_inv i @ free_vars_of_eloc j

let filter_args_for_inv (args:list expr)
                        (td:type_decl)
val filter_args_for_inv (args: list expr) (td: type_decl) : ML (list expr)
args: Prims.list InterpreterTarget.expr -> td: InterpreterTarget.type_decl
  -> FStar.All.ML (Prims.list InterpreterTarget.expr)