val print_lam (#a: Type) (f: (a -> ML string)) (x: lam a) : ML string
let print_lam (#a:Type) (f:a -> ML string) (x:lam a) : ML string =
  match x with
  | Some x, y ->
    Printf.sprintf ("(fun %s -> %s)")
      (print_ident x)
      (f y)
  | None, y -> f y
val print_lam (#a: Type) (f: (a -> ML string)) (x: lam a) : ML string
let print_lam (#a: Type) (f: (a -> ML string)) (x: lam a) : ML string =
match x with
| Some x, y -> Printf.sprintf ("(fun %s -> %s)") (print_ident x) (f y)
| None, y -> f y
Target.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked HashingOptions.fst.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.Char.fsti.checked FStar.All.fst.checked Binding.fsti.checked Ast.fst.checked
Target.fst
Prims.string Target.lam Ast.ident FStar.Printf.sprintf Target.print_ident
(*
   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 Target
(* The abstract syntax for the code produced by 3d *)
open FStar.All
module A = Ast
open Binding

let rec expr_eq e1 e2 =
  match fst e1, fst e2 with
  | Constant c1, Constant c2 -> c1=c2
  | Identifier i1, Identifier i2 -> A.(i1.v = i2.v)
  | App hd1 args1, App hd2 args2 -> hd1 = hd2 && exprs_eq args1 args2
  | Record t1 fields1, Record t2 fields2 -> A.(t1.v = t2.v) && fields_eq fields1 fields2
  | _ -> false
and exprs_eq es1 es2 =
  match es1, es2 with
  | [], [] -> true
  | e1::es1, e2::es2 -> expr_eq e1 e2 && exprs_eq es1 es2
  | _ -> false
and fields_eq fs1 fs2 =
  match fs1, fs2 with
  | [], [] -> true
  | (i1, e1)::fs1, (i2, e2)::fs2 ->
    A.(i1.v = i2.v)
    && fields_eq fs1 fs2
  | _ -> false
let rec parser_kind_eq k k' =
  match k.pk_kind, k'.pk_kind with
  | PK_return, PK_return -> true
  | PK_impos, PK_impos -> true
  | PK_list,  PK_list -> true
  | PK_t_at_most,  PK_t_at_most -> true
  | PK_t_exact,  PK_t_exact -> true
  | PK_base hd1, PK_base hd2 -> A.(hd1.v = hd2.v)
  | PK_filter k, PK_filter k' -> parser_kind_eq k k'
  | PK_and_then k1 k2, PK_and_then k1' k2'
  | PK_glb k1 k2, PK_glb k1' k2' ->
    parser_kind_eq k1 k1'
    && parser_kind_eq k2 k2'
  | _ -> false

// Some constants

let default_attrs = {
    is_hoisted = false;
    is_if_def = false;
    is_exported = false;
    should_inline = false;
    comments = []
}

let error_handler_name =
  let open A in
  let id' = {
    modul_name = None;
    name = "handle_error";
  } in
  let id = with_range id' dummy_range in
  id
  
let error_handler_decl =
  let open A in
  let error_handler_id' = {
    modul_name = Some "EverParse3d.Actions.Base";
    name = "error_handler"
  } in
  let error_handler_id = with_range error_handler_id' dummy_range in
  let typ = T_app error_handler_id KindSpec [] in
  let a = Assumption (error_handler_name, typ) in
  a, default_attrs

////////////////////////////////////////////////////////////////////////////////
// Printing the target AST in F* concrete syntax
////////////////////////////////////////////////////////////////////////////////

let maybe_mname_prefix (mname:string) (i:A.ident) =
  let open A in
  match i.v.modul_name with
  | None -> ""
  | Some s -> if s = mname then "" else Printf.sprintf "%s." s

let print_ident (i:A.ident) =
  let open A in
  match String.list_of_string i.v.name with
  | [] -> i.v.name
  | c0::_ ->
    if FStar.Char.lowercase c0 = c0
    then i.v.name
    else Ast.reserved_prefix^i.v.name

let print_maybe_qualified_ident (mname:string) (i:A.ident) =
  Printf.sprintf "%s%s" (maybe_mname_prefix mname i) (print_ident i)

let print_field_id_name (i:A.ident) =
  let open A in
  match i.v.modul_name with
  | None -> failwith "Unexpected: module name missing from the field id"
  | Some m -> Printf.sprintf "%s_%s" (String.lowercase m) i.v.name

let print_integer_type =
  let open A in
  function
   | UInt8 -> "uint8"
   | UInt16 -> "uint16"
   | UInt32 -> "uint32"
   | UInt64 -> "uint64"

let namespace_of_integer_type =
  let open A in
  function
   | UInt8 -> "UInt8"
   | UInt16 -> "UInt16"
   | UInt32 -> "UInt32"
   | UInt64 -> "UInt64"

let print_range (r:A.range) : string =
  let open A in
  Printf.sprintf "(FStar.Range.mk_range \"%s\" %d %d %d %d)"
    (fst r).filename
    (fst r).line
    (fst r).col
    (snd r).line
    (snd r).col

let arith_op (o:op) =
  match o with
  | Plus _
  | Minus _
  | Mul _
  | Division _
  | Remainder _
  | ShiftLeft _
  | ShiftRight _
  | BitwiseAnd _
  | BitwiseOr _
  | BitwiseXor _
  | BitwiseNot _ -> true
  | _ -> false

let integer_type_of_arith_op (o:op{arith_op o}) =
  match o with
  | Plus t
  | Minus t
  | Mul t
  | Division t
  | Remainder t
  | ShiftLeft t
  | ShiftRight t
  | BitwiseAnd t
  | BitwiseOr t
  | BitwiseXor t
  | BitwiseNot t -> t

let print_arith_op_range () : ML bool =
  List.length (Options.get_equate_types_list ()) = 0

let print_arith_op
  (o:op{arith_op o})
  (r:option A.range) : ML string
  = let fn =
      match o with
      | Plus _ -> "add"
      | Minus _ -> "sub"
      | Mul _ -> "mul"
      | Division _ -> "div"
      | Remainder _ -> "rem"
      | ShiftLeft _ -> "shift_left"
      | ShiftRight _ -> "shift_right"
      | BitwiseAnd _ -> "logand"
      | BitwiseOr _ -> "logor"
      | BitwiseXor _ -> "logxor"
      | BitwiseNot _ -> "lognot"
    in

    if print_arith_op_range ()
    then
      let t =
        match integer_type_of_arith_op o with
        | A.UInt8 -> "u8"
        | A.UInt16 -> "u16"
        | A.UInt32 -> "u32"
        | A.UInt64 -> "u64"
      in
      let r = match r with | Some r -> r | None -> A.dummy_range in
      Printf.sprintf "EverParse3d.Prelude.%s_%s %s"
        t fn (print_range r)
    else
      let m =
        match integer_type_of_arith_op o with
        | A.UInt8 -> "FStar.UInt8"
        | A.UInt16 -> "FStar.UInt16"
        | A.UInt32 -> "FStar.UInt32"
        | A.UInt64 -> "FStar.UInt64"
      in
      Printf.sprintf "%s.%s" m fn

let is_infix =
  function
  | Eq
  | Neq
  | And
  | Or -> true
  | _ -> false

// Bitfield operators from EverParse3d.Prelude.StaticHeader are least
// significant bit first by default, following MSVC
// (https://learn.microsoft.com/en-us/cpp/c-language/c-bit-fields)
let print_bitfield_bit_order = function
  | A.LSBFirst -> ""
  | A.MSBFirst -> "_msb_first"

let print_op_with_range ropt o =
  match o with
  | Eq -> "="
  | Neq -> "<>"
  | And -> "&&"
  | Or -> "||"
  | Not -> "not"
  | Plus _
  | Minus _
  | Mul _
  | Division _
  | Remainder _
  | ShiftLeft _
  | ShiftRight _
  | BitwiseAnd _
  | BitwiseOr _
  | BitwiseXor _
  | BitwiseNot _ -> print_arith_op o ropt
  | LT t -> Printf.sprintf "FStar.%s.lt" (namespace_of_integer_type t)
  | GT t -> Printf.sprintf "FStar.%s.gt" (namespace_of_integer_type t)
  | LE t -> Printf.sprintf "FStar.%s.lte" (namespace_of_integer_type t)
  | GE t -> Printf.sprintf "FStar.%s.gte" (namespace_of_integer_type t)
  | IfThenElse -> "ite"
  | BitFieldOf i order -> Printf.sprintf "get_bitfield%d%s" i (print_bitfield_bit_order order)
  | Cast from to ->
    let tfrom = print_integer_type from in
    let tto = print_integer_type to in
    if tfrom = tto
    then "EverParse3d.Prelude.id"
    else Printf.sprintf "EverParse3d.Prelude.%s_to_%s" tfrom tto
  | Ext s -> s

let print_op = print_op_with_range None

let rec print_expr (mname:string) (e:expr) : ML string =
  match fst e with
  | Constant c ->
    A.print_constant c
  | Identifier i -> print_maybe_qualified_ident mname i
  | Record nm fields ->
    Printf.sprintf "{ %s }" (String.concat "; " (print_fields mname fields))
  | App op [e1;e2] ->
    if is_infix op
    then
      Printf.sprintf "(%s %s %s)"
                   (print_expr mname e1)
                   (print_op_with_range (Some (snd e)) (App?.hd (fst e)))
                   (print_expr mname e2)
    else
      Printf.sprintf "(%s %s %s)"
                   (print_op_with_range (Some (snd e)) (App?.hd (fst e)))
                   (print_expr mname e1)
                   (print_expr mname e2)
  | App Not [e1]
  | App (BitwiseNot _) [e1] ->
    Printf.sprintf "(%s %s)" (print_op (App?.hd (fst e))) (print_expr mname e1)
  | App IfThenElse [e1;e2;e3] ->
    Printf.sprintf
      "(if %s then %s else %s)"
      (print_expr mname e1) (print_expr mname e2) (print_expr mname e3)
  | App (BitFieldOf i order) [e1;e2;e3] ->
    Printf.sprintf
      "(%s %s %s %s)"
      (print_op (BitFieldOf i order))
      (print_expr mname e1) (print_expr mname e2) (print_expr mname e3)
  | App op [] ->
    print_op op
  | App op es ->
    Printf.sprintf "(%s %s)" (print_op op) (String.concat " " (print_exprs mname es))

and print_exprs (mname:string) (es:list expr) : ML (list string) =
  match es with
  | [] -> []
  | hd::tl -> print_expr mname hd :: print_exprs mname tl

and print_fields (mname:string) (fs:_) : ML (list string) =
  match fs with
  | [] -> []
  | (x, e)::tl ->
    Printf.sprintf "%s = %s" (print_ident x) (print_expr mname e)
    :: print_fields mname tl
val print_lam (#a: Type) (f: (a -> ML string)) (x: lam a) : ML string
f: (_: a -> FStar.All.ML Prims.string) -> x: Target.lam a -> FStar.All.ML Prims.string