val free_vars_expr (genv: global_env) (env out: env_t) (e: T.expr) : ML env_t
val free_vars_expr (genv: global_env) (env out: env_t) (e: T.expr) : ML env_t
let rec free_vars_expr (genv:global_env)
                       (env:env_t)
                       (out:env_t)
                       (e:T.expr)
  : ML env_t
  = let open T in
    match fst e with
    | Constant _ -> out
    | Identifier i ->
      if Some? (type_in_local_env i out) then out
      else begin
        match type_in_local_env i env with
        | None ->
          check_in_global_env genv i;
          out
        | Some t -> (i, t) :: out
      end
    | App hd args ->
      List.fold_left (free_vars_expr genv env) out args
    | Record _ fields ->
      List.fold_left (fun out (_, e) -> free_vars_expr genv env out e) out fields
(*
   Copyright 2019 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 TranslateForInterpreter
(* This module translates type definitions from the source Ast
   to types, parsers and validators in the Target language *)
open Ast
module A = Ast
module B = Binding
module T = Target
module H = Hashtable
module TS = TypeSizes
open FStar.All
open FStar.Pervasives
open FStar.List.Tot

noeq
type global_env = {
  benv:B.global_env;
  size_env: TS.env_t;
  has_reader: H.t ident' bool;
  parser_kind_nz: H.t ident' bool;
  parser_weak_kind: H.t ident' A.weak_kind;
  parser_kind_is_constant_size: H.t ident' bool;
}

let has_reader (env:global_env) (id:A.ident) : ML bool =
  if B.has_reader env.benv id
  then true
  else Some? (H.try_find env.has_reader id.v)

let add_reader (env:global_env) (id:A.ident) : ML unit =
  H.insert env.has_reader id.v true

let parser_kind_nz (env:global_env) (id:A.ident) : ML bool =
  match H.try_find env.parser_kind_nz id.v with
  | Some b -> b
  | None ->
    match B.parser_kind_nz env.benv id with
    | Some b -> b
    | None ->
      failwith (Printf.sprintf "Type %s has an unknown parser kind" (ident_to_string id))

let parser_weak_kind (env:global_env) (id:A.ident) : ML A.weak_kind =
  match H.try_find env.parser_weak_kind id.v with
  | Some b -> b
  | None ->
    match B.parser_weak_kind env.benv id with
    | Some b -> b
    | None ->
      failwith (Printf.sprintf "Type %s has an unknown weak kind" (ident_to_string id))

let parser_kind_is_constant_size
  (env: global_env) (id: A.ident)
: ML bool
= 
  match H.try_find env.parser_kind_is_constant_size id.v with
  | Some b -> b
  | None ->
    match TS.size_of_typename env.size_env id with
    | TS.Fixed _ -> true
    | _ -> false

let add_parser_kind_is_constant_size (genv:global_env) (id:A.ident) (is_constant_size:bool) =
  H.insert genv.parser_kind_is_constant_size id.v is_constant_size

/// gensym (top-level effect, safe to ignore)
#push-options "--warn_error -272"
let gen_ident : option string -> St ident =
  let open FStar.ST in
  let ctr : ref int = alloc 0 in
  let next base_name_opt =
    let v = !ctr in
    ctr := v + 1;
    let id =
      match base_name_opt with
      | None -> Printf.sprintf "_x_%d" v
      | Some n -> Printf.sprintf "_%s_%d" n v
    in
    with_dummy_range (to_ident' id)
  in
  next
#pop-options

let underscore_ident = with_dummy_range (to_ident' "_")

(** Some utilities **)
let mk_lam (f:(A.ident -> ML 'a)) : ML (T.lam 'a) =
  let x = gen_ident None in
  Some x, f x

let map_lam (x:T.lam 'a) (g: 'a -> ML 'b) : ML (T.lam 'b) =
  fst x, g (snd x)

let mk_parser k t typename fieldname p = T.({
  p_kind = k;
  p_typ = t;
  p_parser = p;
  p_typename = typename;
  p_fieldname = fieldname
})

// Kind constructors
let pk_return = T.({
  pk_kind = PK_return;
  pk_nz = false;
  pk_weak_kind = WeakKindStrongPrefix;
})
let pk_impos = T.({
  pk_kind = PK_impos;
  pk_nz = true;
  pk_weak_kind = WeakKindStrongPrefix;
})
let pk_base id nz wk = T.({
  pk_kind = PK_base id;
  pk_weak_kind = wk;
  pk_nz = nz
})
let pk_list = T.({
  pk_kind = PK_list;
  pk_weak_kind = WeakKindStrongPrefix;
  pk_nz = false
})
let pk_t_at_most = T.({
  pk_kind = PK_t_at_most;
  pk_weak_kind = WeakKindStrongPrefix;
  pk_nz = false
})
let pk_t_exact = T.({
  pk_kind = PK_t_exact;
  pk_weak_kind = WeakKindStrongPrefix;
  pk_nz = false
})
let pk_string = T.({
  pk_kind = PK_string;
  pk_weak_kind = WeakKindStrongPrefix;
  pk_nz = true
})
let pk_filter k = T.({
  pk_kind = PK_filter k;
  pk_weak_kind = k.pk_weak_kind;
  pk_nz = k.pk_nz
})
let pk_and_then k1 k2 = T.({
  pk_kind = PK_and_then k1 k2;
  pk_weak_kind = k2.pk_weak_kind;
  pk_nz = k1.pk_nz || k2.pk_nz
})
let pk_glb k1 k2 = T.({
  pk_kind = PK_glb k1 k2;
  pk_weak_kind = weak_kind_glb k1.pk_weak_kind k2.pk_weak_kind;
  pk_nz = k1.pk_nz && k2.pk_nz
})

let false_typ = T.T_false
let unit_typ =
    T.T_app (with_dummy_range (to_ident' "unit")) KindSpec []
let unit_val =
    T.(mk_expr (App (Ext "()") []))
let unit_parser =
    let unit_id = with_dummy_range (to_ident' "unit") in
    mk_parser pk_return unit_typ unit_id "none" (T.Parse_return unit_val)
let pair_typ t1 t2 =
    T.T_app (with_dummy_range (to_ident' "tuple2")) KindSpec [Inl t1; Inl t2]
let pair_value x y =
    T.Record (with_dummy_range (to_ident' "tuple2"))
             [(with_dummy_range (to_ident' "fst"), T.mk_expr (T.Identifier x));
              (with_dummy_range (to_ident' "snd"), T.mk_expr (T.Identifier y))]
let pair_parser n1 p1 p2 =
    let open T in
    let pt = pair_typ p1.p_typ p2.p_typ in
    let t_id = with_dummy_range (to_ident' "tuple2") in
    mk_parser (pk_and_then p1.p_kind p2.p_kind)
              pt
              t_id
              (ident_to_string n1)
              (Parse_pair n1 p1 p2)
let dep_pair_typ t1 (t2:(A.ident & T.typ)) : T.typ =
    T.T_dep_pair t1 t2
let dep_pair_value x y : T.expr =
    T.mk_expr
      (T.Record (with_dummy_range (to_ident' "dtuple2"))
                [(with_dummy_range (to_ident' "fst"), T.mk_expr (T.Identifier x));
                 (with_dummy_range (to_ident' "snd"), T.mk_expr (T.Identifier y))])
let dep_pair_parser n1 p1 (p2:A.ident & T.parser) =
  let open T in
  let t = T_dep_pair p1.p_typ (fst p2, (snd p2).p_typ) in
  let t_id = with_dummy_range (to_ident' "dtuple2") in
  mk_parser
      (pk_and_then p1.p_kind (snd p2).p_kind) 
      t
      t_id
      (ident_to_string n1)
      (Parse_dep_pair n1 p1 (Some (fst p2), snd p2))
let dep_pair_with_refinement_parser n1 p1 (e:T.lam T.expr) (p2:A.ident & T.parser) =
  let open T in
  let t1 = T_refine p1.p_typ e in
  let t = T_dep_pair t1 (fst p2, (snd p2).p_typ) in
  let k1 = pk_filter p1.p_kind in
  let t_id = with_dummy_range (to_ident' "dtuple2") in
  mk_parser
      (pk_and_then k1 (snd p2).p_kind)
      t
      t_id
      (ident_to_string n1)
      (Parse_dep_pair_with_refinement n1 p1 e (Some (fst p2), snd p2))
let dep_pair_with_refinement_and_action_parser n1 p1 (e:T.lam T.expr) (a:T.lam T.action) (p2:A.ident & T.parser) =
  let open T in
  let t1 = T_refine p1.p_typ e in
  let t = T_dep_pair t1 (fst p2, (snd p2).p_typ) in
  let k1 = pk_filter p1.p_kind in
  let t_id = with_dummy_range (to_ident' "dtuple2") in  
  mk_parser
      (pk_and_then k1 (snd p2).p_kind)
      t
      t_id
      (ident_to_string n1)
      (Parse_dep_pair_with_refinement_and_action n1 p1 e a (Some (fst p2), snd p2))
let dep_pair_with_action_parser p1 (a:T.lam T.action) (p2:A.ident & T.parser) =
  let open T in
  let t1 = p1.p_typ in
  let t = T_dep_pair t1 (fst p2, (snd p2).p_typ) in
  let k1 = p1.p_kind in
  let t_id = with_dummy_range (to_ident' "dtuple2") in
  mk_parser
      (pk_and_then k1 (snd p2).p_kind)
      t
      t_id
      "none"
      (Parse_dep_pair_with_action p1 a (Some (fst p2), snd p2))
let extend_fieldname fieldname e = Printf.sprintf "%s.%s" fieldname e
let ite_parser typename fieldname (e:T.expr) (then_:T.parser) (else_:T.parser) : ML T.parser =      
    let k, p1, p2 =
      if T.parser_kind_eq then_.p_kind else_.p_kind
      then then_.p_kind, then_, else_
      else let k = pk_glb then_.p_kind else_.p_kind in
           k,
           mk_parser k then_.p_typ typename (extend_fieldname fieldname "case_left") (T.Parse_weaken_right then_ else_.p_kind),
           mk_parser k else_.p_typ typename (extend_fieldname fieldname "case_right") (T.Parse_weaken_left else_ then_.p_kind)
    in
    let t = T.T_if_else e then_.p_typ else_.p_typ in
    mk_parser k t typename fieldname (T.Parse_if_else e p1 p2)

let translate_op : A.op -> ML T.op = 
  let force_topt (o:option A.integer_type) 
    : ML integer_type
    = match o with
      | None -> failwith (Printf.sprintf "Unelaborated integer operator")
      | Some t -> t
  in
  fun op ->
  match op with
  | Eq -> T.Eq
  | Neq -> T.Neq
  | And -> T.And
  | Or -> T.Or
  | Not -> T.Not
  | Plus topt -> T.Plus (force_topt topt)
  | Minus topt -> T.Minus (force_topt topt)
  | Mul topt -> T.Mul (force_topt topt)
  | Division topt -> T.Division (force_topt topt)
  | Remainder topt -> T.Remainder (force_topt topt)
  | BitwiseAnd topt -> T.BitwiseAnd (force_topt topt)
  | BitwiseXor topt -> T.BitwiseXor (force_topt topt)
  | BitwiseOr topt -> T.BitwiseOr (force_topt topt)
  | BitwiseNot topt -> T.BitwiseNot (force_topt topt)
  | ShiftRight topt -> T.ShiftRight (force_topt topt)
  | ShiftLeft topt -> T.ShiftLeft (force_topt topt)
  | LT topt -> T.LT (force_topt topt)
  | GT topt -> T.GT (force_topt topt)
  | LE topt -> T.LE (force_topt topt)
  | GE topt -> T.GE (force_topt topt)
  | IfThenElse -> T.IfThenElse
  | BitFieldOf i order -> T.BitFieldOf i order
  | Cast (Some from) to -> T.Cast from to
  | Ext s -> T.Ext s
  | Cast None _
  | SizeOf -> failwith (Printf.sprintf "Operator `%s` should have been eliminated already"
                                  (Ast.print_op op))


let rec translate_expr (e:A.expr) : ML T.expr =
  (match e.v with
   | Constant c -> T.Constant c
   | Identifier i -> T.Identifier i
   | App op exprs -> T.App (translate_op op) (List.map translate_expr exprs)
   | Static _ -> failwith "`static` should have been eliminated already"
   | This -> failwith "`this` should have been eliminated already"),
  e.A.range

(*
 * Straightforward 1-1 translation
 *)

let rec translate_output_type (t:A.typ) : ML T.typ =
  match t.v with
  | Pointer t -> T.T_pointer (translate_output_type t)
  | Type_app id b [] -> T.T_app id b []
  | _ -> failwith "Impossible, translate_output_type did not get an output type!"

let rec translate_out_expr_node (oe:with_meta_t out_expr')
  : ML T.output_expr' =
  match oe.v with
  | OE_id id -> T.T_OE_id id
  | OE_star oe -> T.T_OE_star (translate_out_expr oe)
  | OE_addrof oe -> T.T_OE_addrof (translate_out_expr oe)
  | OE_deref oe id -> T.T_OE_deref (translate_out_expr oe) id
  | OE_dot oe id -> T.T_OE_dot (translate_out_expr oe) id

and translate_out_expr (oe:out_expr) : ML T.output_expr =
  let oe' = translate_out_expr_node oe.out_expr_node in
  match oe.out_expr_meta with
  | Some ({ out_expr_base_t = bt; out_expr_t = t; out_expr_bit_width = n }) ->
    { T.oe_expr = oe';
      T.oe_bt = translate_output_type bt;
      T.oe_t = translate_output_type t;
      T.oe_bitwidth = n}
  | None -> failwith "Impossible, translate_out_expr got an output expression node without metadata!"

(*
 * We create the Output_type_expr decl with these attributes,
 *   they are not used for output types
 *)

let output_types_attributes = {
  T.is_hoisted = false;
  T.is_if_def = false;
  T.is_exported = false;
  T.should_inline = false;
  T.comments = [] 
}

(*
 * An output expression type parameter is translated to
 *   an external function call
 *
 * In addition we emit a top-level Output_type_expr decl
 *)

let translate_out_expr_typ_param (oe:out_expr) : ML (T.expr & T.decls) =
  let t_oe = translate_out_expr oe in
  let fn_name = T.output_getter_name t_oe in
  let base_var = T.output_base_var t_oe in
  let te =
    (T.App (T.Ext fn_name)
      [(T.Identifier base_var, oe.A.out_expr_node.A.range)]), oe.A.out_expr_node.A.range in
  te, [T.Output_type_expr t_oe true, output_types_attributes]
  
let translate_typ_param (p:typ_param) : ML (T.expr & T.decls) =
  match p with
  | A.Inl e  -> translate_expr e, []
  | A.Inr oe -> translate_out_expr_typ_param oe

let rec translate_typ (t:A.typ) : ML (T.typ & T.decls) =
  match t.v with
  | Pointer t ->
    let t', decls = translate_typ t in
    T.T_pointer t', decls
  | Type_app hd b args ->
    let args, decls = args |> List.map translate_typ_param |> List.split in
    T.T_app hd b (List.map Inr args), List.flatten decls

let has_entrypoint (l:list A.attribute) =
  List.tryFind (function A.Entrypoint -> true | _ -> false) l
  |> Some?

let translate_typedef_name (tdn:A.typedef_names) (params:list Ast.param)
  : ML (T.typedef_name & T.decls) =

  let params, ds = params |> List.map (fun (t, id, _) ->  //TODO: ignores qualifier
    let t, ds = translate_typ t in
    (id, t), ds) |> List.split in

  let open T in
  { td_name = tdn.typedef_name;
    td_params = params;
    td_entrypoint = has_entrypoint tdn.typedef_attributes }, List.flatten ds

let make_enum_typ (t:T.typ) (ids:list ident) =
  let refinement i =
    let x = T.Identifier i in
    List.fold_right
      (fun y e -> T.mk_expr (T.App T.Or [T.mk_expr (T.App T.Eq [T.mk_expr x; T.mk_expr (T.Identifier y);]); e]))
      ids
      (T.mk_expr (T.Constant (Bool false)))
  in
  T.T_refine t (mk_lam refinement)

let rec has_refinement_and_action (t:T.typ)
  : ML (option (T.typ &
                option (T.lam T.expr) &
                option (either T.action (T.lam T.action)) &
                option comments))
  = let open T in
    match t with
    | T_refine t e -> Some (t, Some e, None, None)
    | T_with_action t a ->
      begin
      match has_refinement_and_action t with
      | None ->
        Some(t, None, Some (Inl a), None)
      | Some (t, e, None, c) ->
        Some (t, e, Some (Inl a), c)
      | Some (_, _, Some _, _) ->
        failwith "Nested actions: impossible"
      end
    | T_with_dep_action t a ->
      begin
      match has_refinement_and_action t with
      | None ->
        Some (t, None, Some (Inr a), None)
      | Some (t, e, None, c) ->
        Some (t, e, Some (Inr a), c)
      | Some (_, _, Some _, _) ->
        failwith "Nested actions: impossible"
      end
    | T_with_comment t c ->
      begin
      match has_refinement_and_action t with
      | None -> None
      | Some (t, e, a, None) -> 
        Some (t, e, a, Some c)
      | Some (t, e, a, Some c') ->
        Some (t, e, a, Some (c @ c'))
      end
    | _ -> None

let maybe_add_comment t copt =
    match copt with
    | None -> t
    | Some c -> T.T_with_comment t c

let rec parse_typ (env:global_env)
                  (typename: A.ident) 
                  (fieldname:string)
                  (t:T.typ) : ML T.parser =
  let open T in
  let extend_fieldname e = Printf.sprintf "%s.%s" fieldname e in
  match t with
  | T_false ->
    mk_parser pk_impos T_false typename fieldname Parse_impos

  | T.T_app _ A.KindOutput _
  | T.T_app _ A.KindExtern _ ->
    failwith "Impossible, did not expect parse_typ to be called with an output/extern type!"

  | T.T_app {v={name="nlist"}} KindSpec [Inr e; Inl t] ->
    let pt = parse_typ env typename (extend_fieldname "element") t in
    mk_parser pk_list
              t
              typename
              fieldname
              (T.Parse_nlist e pt)

  | T.T_app {v={name="t_at_most"}} KindSpec [Inr e; Inl t] ->
    let pt = parse_typ env typename (extend_fieldname "element") t in
    mk_parser pk_t_at_most
              t
              typename
              fieldname
              (T.Parse_t_at_most e pt)

  | T.T_app {v={name="t_exact"}} KindSpec [Inr e; Inl t] ->
    let pt = parse_typ env typename (extend_fieldname "element") t in
    mk_parser pk_t_exact
              t
              typename
              fieldname
              (T.Parse_t_exact e pt)

  | T.T_app {v={name="cstring"}} KindSpec [Inl t; Inr e] ->
    let pt = parse_typ env typename (extend_fieldname "element") t in
    mk_parser pk_string
              t
              typename
              fieldname
              (T.Parse_string pt e)

  | T.T_app hd KindSpec args ->
    mk_parser (pk_base hd (parser_kind_nz env hd) (parser_weak_kind env hd))
              t
              typename
              fieldname
              (T.Parse_app hd args)

  | T.T_refine t_base refinement ->
    let base = parse_typ env typename fieldname t_base in
    let refined = T.Parse_refinement typename base refinement in
    mk_parser (pk_filter base.p_kind) t typename (extend_fieldname "refinement") refined

  | T.T_if_else e t1 t2 ->
    let p1 = parse_typ env typename fieldname t1 in
    let p2 = parse_typ env typename fieldname t2 in
    ite_parser typename fieldname e p1 p2

  | T.T_dep_pair t1 (x, t2) ->
    dep_pair_parser typename (parse_typ env typename (extend_fieldname "first") t1) 
                             (x, parse_typ env typename (extend_fieldname "second") t2)

  | T.T_with_action _ _
  | T.T_with_dep_action _ _ ->
    let ref_action = has_refinement_and_action t in
    begin
    match ref_action with
    | None
    | Some (_, _, None, _) ->
      failwith "Impossible"
    | Some (t, None, Some (Inl a), copt) ->
      let t = maybe_add_comment t copt in
      let p = parse_typ env typename (extend_fieldname "base") t in
      mk_parser p.p_kind t typename fieldname (T.Parse_with_action typename p a)
    | Some (t, None, Some (Inr a), copt) ->
      let t = maybe_add_comment t copt in    
      let p = parse_typ env typename (extend_fieldname "base") t in
      mk_parser p.p_kind t typename fieldname (T.Parse_with_dep_action typename p a)
    | Some (t, Some r, Some (Inl a), copt) ->
      let t = maybe_add_comment t copt in        
      let p = parse_typ env typename (extend_fieldname "base") t in
      mk_parser (pk_filter p.p_kind)
                (T.T_refine t r)
                typename
                fieldname
                (T.Parse_refinement_with_action typename p r (Some underscore_ident, a))
    | Some (t, Some r, Some (Inr a), copt) ->
      let t = maybe_add_comment t copt in            
      let p = parse_typ env typename (extend_fieldname "base") t in
      mk_parser (pk_filter p.p_kind)
                (T.T_refine t r)
                typename
                fieldname
                (T.Parse_refinement_with_action typename p r a)
    end
  | T.T_with_comment t c ->
    let p = parse_typ env typename fieldname t in
    { p with p_parser = T.Parse_with_comment p c }

  | T.T_pointer _ ->
    failwith "No parsers for pointer types"

  | T.T_with_probe content_type probe len dest -> 
    let p = parse_typ env typename fieldname content_type in
    let q = T.Parse_with_probe p probe len dest in
    let u64_t, _ = translate_typ A.tuint64 in
    let u64_parser = parse_typ env typename fieldname u64_t in
    { p_kind = u64_parser.p_kind;
      p_typ = t;
      p_parser = q;
      p_typename = typename;
      p_fieldname = fieldname }


let rec read_typ (env:global_env) (t:T.typ) : ML (option T.reader) =
  let open T in
  match t with
  | T_app ({v={name="UINT8"}}) _ [] -> Some Read_u8
  | T_app ({v={name="UINT16"}}) _ [] -> Some Read_u16
  | T_app ({v={name="UINT32"}}) _ [] -> Some Read_u32
  | T.T_app hd KindSpec args ->
    if has_reader env hd
    then Some (T.Read_app hd args)
    else None
  | T.T_with_comment t _
  | T.T_with_action t _ ->
    read_typ env t
  | _ -> None

let make_reader (env:global_env) (t:T.typ) : ML T.reader =
  match read_typ env t with
  | None ->
    failwith (Printf.sprintf "Unsupported reader type: %s\n" (T.print_typ "" t))  //AR: TODO: needs a module name
  | Some r ->
    r

/// To translate an assignment action, a star is translated as before
///
/// Other output expressions are translated to setters applied to the base variable and rhs
///
/// In addition a top-level Output_type_expr decl is emitted

let translate_action_assignment (lhs:A.out_expr) (rhs:A.expr)
  : ML (T.atomic_action & T.decls) =

  let open A in
  match lhs.out_expr_node.v with
  | OE_star ({out_expr_node={v=OE_id i}}) ->
    T.Action_assignment i (translate_expr rhs), []
  | _ ->
    let t_lhs = translate_out_expr lhs in
    let fn_name = T.output_setter_name t_lhs in
    let base_var = T.output_base_var t_lhs in
    let v = translate_expr rhs in
    let act = T.Action_call (Ast.with_dummy_range (Ast.to_ident' fn_name))
      [(T.Identifier base_var, rhs.A.range); v] in
    act, [T.Output_type_expr t_lhs false, output_types_attributes]

let translate_action_field_ptr_after (write_to:A.out_expr) (sz:A.expr)
  : ML (T.atomic_action & T.decls)
=
  let open A in
  match write_to.out_expr_node.v with
  | OE_star ({out_expr_node={v=OE_id i}}) ->
    T.Action_field_ptr_after (translate_expr sz) i, []
  | _ ->
    let t_write_to = translate_out_expr write_to in
    let fn_name = T.output_setter_name t_write_to in
    let base_var = T.output_base_var t_write_to in
    let v = translate_expr sz in
    let act = T.Action_field_ptr_after_with_setter v
      (Ast.with_dummy_range (Ast.to_ident' fn_name))
      (T.Identifier base_var, sz.A.range)
    in
    act, [T.Output_type_expr t_write_to false, output_types_attributes]

let rec translate_action (a:A.action) : ML (T.action & T.decls) =
  let translate_atomic_action (a:A.atomic_action)
    : ML (T.atomic_action & T.decls)
    = match a with
      | Action_return e ->
        T.Action_return (translate_expr e), []
      | Action_abort ->
        T.Action_abort, []
      | Action_field_pos_64 ->
        T.Action_field_pos_64, []
      | Action_field_pos_32 ->
        T.Action_field_pos_32, []
      | Action_field_ptr ->
        T.Action_field_ptr, []
      | Action_field_ptr_after sz write_to ->
        translate_action_field_ptr_after write_to sz
      | Action_deref i ->
        T.Action_deref i, []
      | Action_assignment lhs rhs ->
        translate_action_assignment lhs rhs
      | Action_call f args ->
        T.Action_call f (List.map translate_expr args), []
  in
  match a.v with
  | Atomic_action a ->
    let act, ds = translate_atomic_action a in
    T.Atomic_action act, ds

  | Action_seq hd tl ->
    let hd, ds1 = translate_atomic_action hd in
    let tl, ds2 = translate_action tl in
    T.Action_seq hd tl, ds1@ds2

  | Action_ite hd then_ (Some else_) ->
    let then_, ds_then = translate_action then_ in
    let else_, ds_else = translate_action else_ in
    T.Action_ite (translate_expr hd) then_ else_, ds_then @ ds_else

  | Action_ite hd then_ None ->
    let then_, ds_then = translate_action then_ in
    T.Action_ite (translate_expr hd)
                 then_
                 (T.Atomic_action (T.Action_return (T.mk_expr (T.Constant A.Unit)))),
    ds_then

  | Action_let i a k ->
    let a, ds1 = translate_atomic_action a in
    let k, ds2 = translate_action k in
    T.Action_let i a k, ds1 @ ds2

  | Action_act a ->
    let a, ds = translate_action a in
    T.Action_act a, ds

let rec parser_is_constant_size_without_actions
  (env: global_env)
  (p: T.parser)
: ML bool
= match p.T.p_parser with
  | T.Parse_return _
  | T.Parse_impos
    -> true
  | T.Parse_app hd _
    -> parser_kind_is_constant_size env hd
  | T.Parse_nlist array_size parse_elem
    -> begin match fst array_size with
      | T.Constant (A.Int _ array_size) -> parser_is_constant_size_without_actions env parse_elem
      | _ -> false
      end
  | T.Parse_pair _ hd tl
    -> if parser_is_constant_size_without_actions env hd
      then parser_is_constant_size_without_actions env tl
      else false
  | T.Parse_dep_pair _ parse_key (_, parse_value)
  | T.Parse_dep_pair_with_refinement _ parse_key _ (_, parse_value)
    -> (* the lambda identifier is not global, because the 3d syntax does not allow higher-order types *)
      if parser_is_constant_size_without_actions env parse_key
      then parser_is_constant_size_without_actions env parse_value
      else false
  | T.Parse_t_at_most _ _
  | T.Parse_t_exact _ _  
  | T.Parse_dep_pair_with_action _ _ _
  | T.Parse_dep_pair_with_refinement_and_action _ _ _ _ _
  | T.Parse_refinement_with_action _ _ _ _
  | T.Parse_with_dep_action _ _ _
  | T.Parse_with_action _ _ _
  | T.Parse_if_else _ _ _
  | T.Parse_string _ _
  | T.Parse_with_probe _ _ _ _
    -> false
  | T.Parse_map p _
  | T.Parse_refinement _ p _
  | T.Parse_weaken_left p _
  | T.Parse_weaken_right p _  
  | T.Parse_with_comment p _
    -> parser_is_constant_size_without_actions env p

let unknown_type_ident = 
  let open Ast in
  let id = {
    modul_name = None;
    name = "<unknown>"
  } in
  with_range id dummy_range

let make_zero (r: range) (t: typ) : ML T.expr =
  let it = typ_as_integer_type t in
  (T.Constant (Int it 0), r)

#push-options "--z3rlimit_factor 4"
let translate_atomic_field (f:A.atomic_field) : ML (T.struct_field & T.decls) =
  let sf = f.v in
  match f.v.field_probe with
  | Some probe_call -> (
    match f.v.field_type.v, probe_call.probe_fn with
    | Pointer t, Some probe_fn ->
      let t, ds1 = translate_typ t in
      let len = translate_expr probe_call.probe_length in
      let dest = probe_call.probe_dest in
      let sf_typ = T.T_with_probe t probe_fn len dest in
      T.({ sf_dependence=sf.field_dependence;
           sf_ident=sf.field_ident;
           sf_typ=sf_typ }), 
      ds1
      
    | _ -> 
      failwith "Impossible: probed fields must be pointers and the probe function must be resolved"
  )
  
  | _ -> 
    let t, ds1 = translate_typ sf.field_type in
    let t =
        let mk_at_most t e : ML T.typ =
          let e = translate_expr e in
          T.T_app (with_range (to_ident' "t_at_most") sf.field_type.range) KindSpec [Inr e; Inl t]
        in
        match sf.field_array_opt with
        | FieldScalar -> t
        | FieldArrayQualified (e, ByteArrayByteSize)
        | FieldArrayQualified (e, ArrayByteSize) ->
          let e = translate_expr e in
          T.T_app (with_range (to_ident' "nlist") sf.field_type.range) KindSpec [Inr e; Inl t]
        | FieldArrayQualified (e, ArrayByteSizeAtMost) ->
          mk_at_most t e
        | FieldArrayQualified (e, ArrayByteSizeSingleElementArray) ->
          let e = translate_expr e in
          T.T_app (with_range (to_ident' "t_exact") sf.field_type.range) KindSpec [Inr e; Inl t]
        | FieldString sz ->
          let r = sf.field_type.range in
          let str = T.T_app (with_range (to_ident' "cstring") r) KindSpec [Inl t; Inr (make_zero r sf.field_type)] in
          begin match sz with
          | None -> str
          | Some e -> mk_at_most str e
          end
        | FieldConsumeAll -> T.T_app (with_range (to_ident' "all_bytes") sf.field_type.range) KindSpec []
    in
    let t =
      match sf.field_constraint with
      | None -> t
      | Some e ->
        T.T_refine t (Some sf.field_ident, translate_expr e)
    in
    let t, ds2 =
      match sf.field_action with
      | None -> t, []
      | Some (a, false) ->
        let a, ds2 = translate_action a in
        T.T_with_action t a, ds2
      | Some (a, _) ->
        let a, ds2 = translate_action a in
        T.T_with_dep_action t (Some sf.field_ident, a), ds2
    in
    let t : T.typ =
      match f.comments with
      | [] ->
        let c =
          Printf.sprintf "Validating field %s"
            (print_ident sf.field_ident)
        in
        T.T_with_comment t [c]
      | c -> T.T_with_comment t c
    in
    if T.T_pointer? t
    then failwith "Type-checking should have forbidden fields with pointer types"
    else
      T.({sf_dependence=sf.field_dependence;
          sf_ident=sf.field_ident;
          sf_typ=t}), ds1@ds2
#pop-options

noeq
type grouped_fields =
  // | Empty_grouped_field
  | DependentField    : hd:T.field -> tl:grouped_fields -> grouped_fields
  | NonDependentField : hd:T.field -> tl:option grouped_fields -> grouped_fields
  | ITEGroup          : e:T.expr -> then_:grouped_fields -> else_:grouped_fields -> grouped_fields
  | GroupThen         : id:A.ident -> struct:grouped_fields -> rest:option grouped_fields -> grouped_fields

let parse_grouped_fields (env:global_env) (typename:A.ident) (gfs:grouped_fields)
  : ML T.parser
  = let open T in
    let parse_typ (fieldname:A.ident) = parse_typ env typename Ast.(fieldname.v.name) in
    let rec aux (gfs:grouped_fields) : ML parser =
      match gfs with
      // | Empty_grouped_field ->
      //   failwith "Unexpected empty list of fields"
      | DependentField sf gfs ->
        //This a dependent pair, gfs cannot be empty
        let get_action = function
          | Inl a -> (Some sf.sf_ident, a)
          | Inr a -> a
        in
        begin
        match has_refinement_and_action sf.sf_typ with
        | None ->
          dep_pair_parser
            sf.sf_ident
            (parse_typ sf.sf_ident sf.sf_typ)
            (sf.sf_ident, aux gfs)
            
        | Some (_, None, None, copt) ->
          dep_pair_parser
            sf.sf_ident
            (parse_typ sf.sf_ident (maybe_add_comment sf.sf_typ copt))
            (sf.sf_ident, aux gfs)

        | Some (t, Some e, None, copt) ->
          dep_pair_with_refinement_parser
            sf.sf_ident
            (parse_typ sf.sf_ident (maybe_add_comment t copt))
            e
            (sf.sf_ident, aux gfs)

        | Some (t, Some e, Some a, copt) ->
          dep_pair_with_refinement_and_action_parser
            sf.sf_ident
            (parse_typ sf.sf_ident (maybe_add_comment t copt))
            e
            (get_action a)
            (sf.sf_ident, aux gfs)

        | Some (t, None, Some a, copt) ->
          dep_pair_with_action_parser
            (parse_typ sf.sf_ident (maybe_add_comment t copt))
            (get_action a)
            (sf.sf_ident, aux gfs)
        end

      | NonDependentField sf rest -> (
        match rest with
        | None ->
          parse_typ sf.sf_ident sf.sf_typ

        | Some rest -> 
          pair_parser sf.sf_ident
            (parse_typ sf.sf_ident sf.sf_typ)
            (aux rest)
        )
        
      | ITEGroup e then_ else_ ->
        let id = gen_ident None in
        let then_ = aux then_ in
        let else_ = aux else_ in
        ite_parser typename id.v.name e then_ else_

      | GroupThen id gfs rest -> (
        match rest with
        | None ->
          aux gfs

        | Some rest -> 
          pair_parser id
            (aux gfs)
            (aux rest)
        )

    in
    aux gfs


let make_tdn (i:A.ident) =
  {
    typedef_name = i;
    typedef_abbrev = with_dummy_range (to_ident' "");
    typedef_ptr_abbrev = with_dummy_range (to_ident' "");
    typedef_attributes = []
  }

let env_t = list (A.ident * T.typ)

let check_in_global_env (env:global_env) (i:A.ident) =
  let _ = B.lookup_expr_name (B.mk_env env.benv) i in ()

let maybe_gen_ident (env:global_env) (s:string) : A.ident =
  with_dummy_range (to_ident' s)

let type_in_local_env (i:A.ident) (env:env_t)
  : ML (option T.typ) =
    match List.tryFind (fun (i', _) -> A.(i.v = i'.v)) env with
    | None -> None
    | Some (_, t) -> Some t
/
TypeSizes.fsti.checked Target.fsti.checked prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.ST.fst.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 Desugar.fst.checked Binding.fsti.checked Ast.fst.checked
TranslateForInterpreter.fst

    genv: TranslateForInterpreter.global_env ->
    env: TranslateForInterpreter.env_t ->
    out: TranslateForInterpreter.env_t ->
    e: Target.expr
  -> FStar.All.ML TranslateForInterpreter.env_t
TranslateForInterpreter.global_env TranslateForInterpreter.env_t Target.expr FStar.Pervasives.Native.fst Target.expr' Ast.range Ast.constant Ast.ident Prims.bool Prims.unit TranslateForInterpreter.check_in_global_env Target.typ Prims.Cons FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option TranslateForInterpreter.type_in_local_env FStar.Pervasives.Native.uu___is_Some Target.op Prims.list FStar.List.fold_left TranslateForInterpreter.free_vars_expr
let rec free_vars_expr (genv: global_env) (env out: env_t) (e: T.expr) : ML env_t =
  
let open T in
match fst e with
| Constant _ -> out
| Identifier i ->
  if Some? (type_in_local_env i out)
  then out
  else
    (match type_in_local_env i env with
      | None ->
        check_in_global_env genv i;
        out
      | Some t -> (i, t) :: out)
| App hd args -> List.fold_left (free_vars_expr genv env) out args
| Record _ fields -> List.fold_left (fun out (_, e) -> free_vars_expr genv env out e) out fields