val parser_kind_nz (env: global_env) (id: A.ident) : ML bool
val parser_kind_nz (env: global_env) (id: A.ident) : ML bool
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))
(*
   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
/
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
env: TranslateForInterpreter.global_env -> id: Ast.ident -> FStar.All.ML Prims.bool
TranslateForInterpreter.global_env Ast.ident Prims.bool FStar.All.failwith FStar.Printf.sprintf Ast.ident_to_string FStar.Pervasives.Native.option Binding.parser_kind_nz TranslateForInterpreter.__proj__Mkglobal_env__item__benv Hashtable.try_find Ast.ident' TranslateForInterpreter.__proj__Mkglobal_env__item__parser_kind_nz Ast.__proj__Mkwith_meta_t__item__v
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))