val translate_op: A.op -> ML T.op
val translate_op: A.op -> ML T.op
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))
(*
   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)
/
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
_: Ast.op -> FStar.All.ML Target.op
Ast.op Target.Eq Target.op Target.Neq Target.And Target.Or Target.Not FStar.Pervasives.Native.option Ast.integer_type Target.Plus Target.Minus Target.Mul Target.Division Target.Remainder Target.BitwiseAnd Target.BitwiseXor Target.BitwiseOr Target.BitwiseNot Target.ShiftRight Target.ShiftLeft Target.LT Target.GT Target.LE Target.GE Target.IfThenElse Prims.int Ast.bitfield_bit_order Target.BitFieldOf Target.Cast Prims.string Target.Ext FStar.All.failwith FStar.Printf.sprintf Ast.print_op
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
function
| 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))