val pair_typ : t1: Target.typ -> t2: Target.typ -> Target.typ
let pair_typ t1 t2 =
    T.T_app (with_dummy_range (to_ident' "tuple2")) KindSpec [Inl t1; Inl t2]
(*
   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
/
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
t1: Target.typ -> t2: Target.typ -> Target.typ
Target.typ Target.T_app Ast.with_dummy_range Ast.ident' Ast.to_ident' Ast.KindSpec Prims.Cons FStar.Pervasives.either Target.expr FStar.Pervasives.Inl Prims.Nil
let pair_typ t1 t2 =
  
T.T_app (with_dummy_range (to_ident' "tuple2")) KindSpec [Inl t1; Inl t2]