let print_derived_name (mname:string) (tag:string) (i:A.ident) =
  Printf.sprintf "%s%s_%s"
    (T.maybe_mname_prefix mname i)
    tag
    (T.print_ident i)
let print_derived_name (mname tag: string) (i: A.ident) =
Printf.sprintf "%s%s_%s" (T.maybe_mname_prefix mname i) tag (T.print_ident i)
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.string Ast.ident FStar.Printf.sprintf Target.maybe_mname_prefix Target.print_ident
(*
   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)
  : lam 'a
  = let i =
      match fst x with
      | None -> A.(with_dummy_range (to_ident' "_"))
      | Some i -> i
    in
    i, snd x

let rec inv_eloc_of_action (a:T.action)
  : ML inv_eloc
  = let open T in
    let of_atomic_action (a:T.atomic_action)
      : ML inv_eloc
      = match a with
        | Action_return _
        | Action_abort
        | Action_field_pos_32
        | Action_field_pos_64 -> inv_eloc_nil
        | Action_field_ptr_after _ write_to -> Inv_ptr write_to, Eloc_ptr write_to, On_success false
        | Action_field_ptr_after_with_setter _ _ _ -> Inv_true, Eloc_output, On_success false
        | Action_field_ptr -> Inv_true, Eloc_none, On_success true
        | Action_deref x -> Inv_ptr x, Eloc_none, On_success false
        | Action_assignment x _ -> Inv_ptr x, Eloc_ptr x, On_success false
        | Action_call f args -> Inv_true, Eloc_output, On_success false
    in
    match a with
    | Atomic_action aa -> of_atomic_action aa
    | Action_seq hd tl
    | Action_let _ hd tl ->
      inv_eloc_union (of_atomic_action hd) (inv_eloc_of_action tl)
    | Action_ite _ a0 a1 ->
      inv_eloc_union (inv_eloc_of_action a0) (inv_eloc_of_action a1)
    | Action_act a ->
      inv_eloc_of_action a

let rec inv_eloc_of_parser (en:env) (p:T.parser)
  : ML inv_eloc
  = let inv_eloc_of_parser = inv_eloc_of_parser en in
    match p.p_parser with
    | T.Parse_impos ->
      inv_eloc_nil

    | T.Parse_app hd args ->
      let dt = dtyp_of_app en hd args in
      begin
      match dt with
      | DT_IType _ ->
        inv_eloc_nil
      | DT_App _ hd args ->
        let td =
          match H.try_find en hd.v with
          | Some td -> td
          | _ -> failwith (Printf.sprintf "Type decl not found for %s" (A.ident_to_string hd))
        in
        inv_eloc_name hd (filter_args_for_inv args td)
      end

    | T.Parse_if_else _ p q
    | T.Parse_pair _ p q
    | T.Parse_dep_pair _ p (_, q)
    | T.Parse_dep_pair_with_refinement _ p _ (_, q) ->
      inv_eloc_union (inv_eloc_of_parser p) (inv_eloc_of_parser q)

    | T.Parse_weaken_left p _
    | T.Parse_weaken_right p _
    | T.Parse_refinement _ p _
    | T.Parse_with_comment p _
    | T.Parse_nlist _ p
    | T.Parse_t_at_most _ p
    | T.Parse_t_exact _ p ->
      inv_eloc_of_parser p

    | T.Parse_dep_pair_with_action p (_, a) (_, q)
    | T.Parse_dep_pair_with_refinement_and_action _ p _ (_, a) (_, q) ->
      inv_eloc_union (inv_eloc_of_parser p)
                     (inv_eloc_union (inv_eloc_of_action a) (inv_eloc_of_parser q))

    | T.Parse_with_action _ p a
    | T.Parse_with_dep_action _ p (_, a) ->
      inv_eloc_union (inv_eloc_of_parser p) (inv_eloc_of_action a)

    | T.Parse_string p _ ->
      inv_eloc_nil

    | T.Parse_refinement_with_action n p f (_, a) ->
      inv_eloc_union (inv_eloc_of_parser p) (inv_eloc_of_action a)

    | T.Parse_map _ _
    | T.Parse_return _ -> failwith "Unnecessary"

let typ_of_parser (en: env) : Tot (T.parser -> ML typ)
= let rec typ_of_parser (p:T.parser)
    : ML typ
  = let rec dtyp_of_parser (p:T.parser)
      : ML dtyp
      = match p.p_parser with
        | T.Parse_app hd args ->
          dtyp_of_app en hd args

        | T.Parse_weaken_left p _
        | T.Parse_weaken_right p _
        | T.Parse_with_comment p _ ->
          dtyp_of_parser p

        | _ ->
          failwith
            (Printf.sprintf "Expected a named type, got %s"
              (T.print_parser "" p))
    in
    let fn = nes p.p_fieldname in
    match p.p_parser with
    | T.Parse_impos ->
      T_false fn

    | T.Parse_app _ _ ->
      T_denoted fn (dtyp_of_parser p)

    | T.Parse_pair _ p q ->
      T_pair (nes p.p_fieldname) (typ_of_parser p) (typ_of_parser q)

    | T.Parse_with_comment p c ->
      T_with_comment fn (typ_of_parser p) (String.concat "; " c)

    | T.Parse_nlist n p ->
      T_nlist fn n (typ_of_parser p)

    | T.Parse_t_at_most n p ->
      T_at_most fn n (typ_of_parser p)

    | T.Parse_t_exact n p ->
      T_exact fn n (typ_of_parser p)

    | T.Parse_if_else e p1 p2 ->
      T_if_else e (typ_of_parser p1) (typ_of_parser p2)

    | T.Parse_dep_pair _ p k ->
      let i, k = as_lam k in
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_dep_pair (nes p.p_fieldname)
                   d
                   (i, typ_of_parser k)
      else
        failwith "typ_of_parser: Parse_dep_pair: tag not readable"

    | T.Parse_dep_pair_with_refinement _ p r k ->
      let i, r = as_lam r in
      let j, k = as_lam k in
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_dep_pair_with_refinement fn d (i, r) (j, typ_of_parser k)
      else
        failwith "typ_of_parser: Parse_dep_pair_with_refinement: tag not readable"

    | T.Parse_dep_pair_with_action p a k ->
      let (i, k) = as_lam k in
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_dep_pair_with_action fn d (i, typ_of_parser k) (as_lam a)
      else
        failwith "typ_of_parser: Parse_dep_pair_with_action: tag not readable"

    | T.Parse_dep_pair_with_refinement_and_action _ p r a k ->
      let a = as_lam a in
      let (i, k) = as_lam k in
      let r = as_lam r in
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_dep_pair_with_refinement_and_action fn d r (i, typ_of_parser k) a
      else
        failwith "typ_of_parser: Parse_dep_pair_with_refinement_and_action: tag not readable"

    | T.Parse_with_action _ p a ->
      T_with_action fn (typ_of_parser p) a

    | T.Parse_with_dep_action _ p a ->
      let a = as_lam a in
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_with_dep_action fn d a
      else
        failwith "typ_of_parser: Parse_with_dep_action: tag not readable"

    | T.Parse_string p z ->
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_string fn d z
      else
        failwith "typ_of_parser: Parse_string: element not readable"

    | T.Parse_refinement _ p f ->
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_refine fn d (as_lam f)
      else
        failwith "typ_of_parser: Parse_refinement: element not readable"

    | T.Parse_refinement_with_action _ p f a ->
      let d = dtyp_of_parser p in
      if allow_reader_of_dtyp d
      then
        T_refine_with_action fn d (as_lam f) (as_lam a)
      else
        failwith "typ_of_parser: Parse_refinement_with_action: element not readable"

    | T.Parse_weaken_left p _
    | T.Parse_weaken_right p _ ->
      typ_of_parser p

    | T.Parse_map _ _
    | T.Parse_return _ -> failwith "Unnecessary"

in typ_of_parser

let rec allow_reading_of_typ (t:typ)
  : Tot bool
  =
  match t with
  | T_with_comment _ t _ ->
    allow_reading_of_typ t

  | T_denoted _ dt ->
    begin
    match dt with
    | DT_IType i -> allow_reader_of_itype i
    | DT_App readable _ _ -> readable
    end

  | _ -> false

let translate_decls (en:env) (ds:T.decls)
  : ML (list decl)
  = List.map
        (fun d ->
          match d with
          | (T.Type_decl td, attrs) ->
            let t = typ_of_parser en td.decl_parser in
            let ar = allow_reading_of_typ t in
            let refined =
              if td.decl_is_enum
              then match td.decl_typ with
                   | T.TD_abbrev t ->
                     if T.T_refine? t
                     then Some t
                     else None
                   | _ -> None
              else None
            in
            let td =
              { name = td.decl_name;
                typ = typ_of_parser en td.decl_parser;
                kind = td.decl_parser.p_kind;
                inv_eloc = inv_eloc_of_parser en td.decl_parser;
                allow_reading = ar;
                attrs = attrs;
                enum_typ = refined
                }
            in
            H.insert en td.name.td_name.v td;
            Inr td
        | d ->
          Inl (d <: not_type_decl))
      ds

let print_ityp (i:itype) =
  match i with
  | UInt8 -> "UInt8"
  | UInt16 -> "UInt16"
  | UInt32 -> "UInt32"
  | UInt64 -> "UInt64"
  | UInt8BE -> "UInt8BE"
  | UInt16BE -> "UInt16BE"
  | UInt32BE -> "UInt32BE"
  | UInt64BE -> "UInt64BE"
  | Unit -> "Unit"
  | AllBytes -> "AllBytes"
  | AllZeros -> "AllZeros"

let print_ident (mname:string) (i:A.ident) =
  T.print_maybe_qualified_ident mname i
val print_derived_name : mname: Prims.string -> tag: Prims.string -> i: Ast.ident -> (Prims.string <: Type0)
mname: Prims.string -> tag: Prims.string -> i: Ast.ident -> (Prims.string <: Type0)