val free_vars_of_eloc (e: eloc) : ML (list A.ident)
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
val free_vars_of_eloc (e: eloc) : ML (list A.ident)
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
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
InterpreterTarget.eloc Prims.Nil Ast.ident Prims.list FStar.List.Tot.Base.op_At InterpreterTarget.free_vars_of_eloc Prims.Cons InterpreterTarget.expr FStar.List.collect InterpreterTarget.free_vars_of_expr
(*
   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)
val free_vars_of_eloc (e: eloc) : ML (list A.ident)
e: InterpreterTarget.eloc -> FStar.All.ML (Prims.list Ast.ident)