val as_lam (x: T.lam 'a) : lam 'a
let as_lam (x:T.lam 'a)
  : lam 'a
  = let i =
      match fst x with
      | None -> A.(with_dummy_range (to_ident' "_"))
      | Some i -> i
    in
    i, snd x
val as_lam (x: T.lam 'a) : lam 'a
let as_lam (x: T.lam 'a) : lam 'a =
let i =
  match fst x with
  | None -> let open A in with_dummy_range (to_ident' "_")
  | Some i -> i
in
i, snd x
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
Target.lam FStar.Pervasives.Native.Mktuple2 Ast.ident FStar.Pervasives.Native.snd FStar.Pervasives.Native.option FStar.Pervasives.Native.fst Ast.with_dummy_range Ast.ident' Ast.to_ident' InterpreterTarget.lam
(*
   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)
  : 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

let itype_of_ident (hd:A.ident)
  : option itype
  = match hd.v.name with
    | "UINT8" -> Some UInt8
    | "UINT16" -> Some UInt16
    | "UINT32" -> Some UInt32
    | "UINT64" -> Some UInt64
    | "UINT8BE" -> Some UInt8BE
    | "UINT16BE" -> Some UInt16BE
    | "UINT32BE" -> Some UInt32BE
    | "UINT64BE" -> Some UInt64BE
    | "unit" -> Some Unit
    | "all_bytes" -> Some AllBytes
    | "all_zeros" -> Some AllZeros
    | _ -> None

let dtyp_of_app (en: env) (hd:A.ident) (args:list T.index)
  : ML dtyp
  = match itype_of_ident hd, args with
    | Some i, [] ->
      DT_IType i

    | _ ->
      let readable = match H.try_find en hd.v with
      | None -> failwith "type not found"
      | Some td -> td.allow_reading
      in
      DT_App readable hd
        (List.map
          (function Inl _ -> failwith "Unexpected type application"
                  | Inr e -> e)
          args)

let tag_of_parser p
  = let open T in
    match p.p_parser with
    | Parse_return _ -> "Parse_return"
    | Parse_app _ _ -> "Parse_app"
    | Parse_nlist _ _ -> "Parse_nlist"
    | Parse_t_at_most _ _ -> "Parse_t_at_most"
    | Parse_t_exact _ _ -> "Parse_t_exact"
    | Parse_pair _ _ _ -> "Parse_pair"
    | Parse_dep_pair _ _ _ -> "Parse_dep_pair"
    | Parse_dep_pair_with_refinement _ _ _ _ -> "Parse_dep_pair_with_refinement"
    | Parse_dep_pair_with_action _ _ _ -> "Parse_dep_pair_with_action"
    | Parse_dep_pair_with_refinement_and_action _ _ _ _ _ -> "Parse_dep_pair_with_refinement_and_action"
    | Parse_map _ _ -> "Parse_map"
    | Parse_refinement _ _ _ -> "Parse_refinement"
    | Parse_refinement_with_action _ _ _ _ -> "Parse_refinement_with_action"
    | Parse_with_dep_action _ _ _ -> "Parse_with_dep_action"
    | Parse_with_action _ _ _ -> "Parse_with_action"
    | Parse_weaken_left _ _ -> "Parse_weaken_left"
    | Parse_weaken_right _ _ -> "Parse_weaken_right"
    | Parse_if_else _ _ _ -> "Parse_if_else"
    | Parse_impos -> "Parse_impos"
    | Parse_with_comment _ _ -> "Parse_with_comment"
    | Parse_string _ _ -> "Parse_string"

let as_lam (x:T.lam 'a)
val as_lam (x: T.lam 'a) : lam 'a
x: Target.lam 'a -> InterpreterTarget.lam 'a