open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

(** val graph_to_lin_statement :
    Joint.uns_params -> AST.ident List.list -> 'a1 Identifiers.identifier_map
    -> Joint.joint_statement -> Joint.joint_statement **)
let graph_to_lin_statement p globals visited = function
| Joint.Sequential (c, nxt) ->
  (match c with
   | Joint.COST_LABEL x -> Joint.Sequential (c, (Obj.magic Types.It))
   | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
   | Joint.COND (a, ltrue) ->
     (match Identifiers.member PreIdentifiers.LabelTag visited
              (Obj.magic nxt) with
      | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
      | Bool.False -> Joint.Sequential (c, (Obj.magic Types.It)))
   | Joint.Step_seq x -> Joint.Sequential (c, (Obj.magic Types.It)))
| Joint.Final c -> Joint.Final c
| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)

(** val chop :
    ('a1 -> Bool.bool) -> 'a1 List.list -> ('a1, 'a1 List.list) Types.prod
    Types.option **)
let rec chop test = function
| List.Nil -> Types.None
| List.Cons (x, l') ->
  (match test x with
   | Bool.True -> chop test l'
   | Bool.False ->
     Obj.magic
       (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
         Types.snd = l' }))

type graph_visit_ret_type =
  ((Nat.nat Identifiers.identifier_map, Identifiers.identifier_set)
  Types.prod, __) Types.prod Types.sig0

(** val graph_visit :
    Joint.uns_params -> AST.ident List.list -> __ ->
    Identifiers.identifier_set -> Nat.nat Identifiers.identifier_map -> __ ->
    Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
    graph_visit_ret_type **)
let rec graph_visit p globals g required visited generated visiting gen_length n entry =
  (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
           visiting with
   | Types.None ->
     (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
       Types.snd = generated })
   | Types.Some pr ->
     (fun _ ->
       let vis_hd = pr.Types.fst in
       let vis_tl = pr.Types.snd in
       (match n with
        | Nat.O -> (fun _ -> assert false (* absurd case *))
        | Nat.S n' ->
          (fun _ ->
            let visited' =
              Identifiers.add PreIdentifiers.LabelTag visited vis_hd
                gen_length
            in
            let statement =
              Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
                vis_hd
            in
            let translated_statement =
              graph_to_lin_statement p globals visited' statement
            in
            let generated' = List.Cons ({ Types.fst = (Types.Some vis_hd);
              Types.snd = translated_statement }, (Obj.magic generated))
            in
            let required' =
              Identifiers.union_set PreIdentifiers.LabelTag
                (Identifiers.set_from_list PreIdentifiers.LabelTag
                  (Joint.stmt_explicit_labels (Joint.lp_to_p__o__stmt_pars p)
                    globals translated_statement)) required
            in
            let visiting' =
              List.append
                (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars p);
                  Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
                  Joint.has_fcond = Bool.False } globals statement) vis_tl
            in
            let add_req_gen =
              match statement with
              | Joint.Sequential (s, nxt) ->
                (match s with
                 | Joint.COST_LABEL x ->
                   (match Identifiers.member PreIdentifiers.LabelTag visited'
                            (Obj.magic nxt) with
                    | Bool.True ->
                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
                        (Identifiers.add_set PreIdentifiers.LabelTag
                          (Identifiers.empty_set PreIdentifiers.LabelTag)
                          (Obj.magic nxt)) }; Types.snd = (List.Cons
                        ({ Types.fst = Types.None; Types.snd =
                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
                        x0) }, List.Nil)) }
                    | Bool.False ->
                      { Types.fst = { Types.fst = Nat.O; Types.snd =
                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
                        Types.snd = List.Nil })
                 | Joint.CALL (x, x0, x1) ->
                   (match Identifiers.member PreIdentifiers.LabelTag visited'
                            (Obj.magic nxt) with
                    | Bool.True ->
                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
                        (Identifiers.add_set PreIdentifiers.LabelTag
                          (Identifiers.empty_set PreIdentifiers.LabelTag)
                          (Obj.magic nxt)) }; Types.snd = (List.Cons
                        ({ Types.fst = Types.None; Types.snd =
                        (let x2 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
                        x2) }, List.Nil)) }
                    | Bool.False ->
                      { Types.fst = { Types.fst = Nat.O; Types.snd =
                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
                        Types.snd = List.Nil })
                 | Joint.COND (x, x0) ->
                   { Types.fst = { Types.fst = Nat.O; Types.snd =
                     (Identifiers.empty_set PreIdentifiers.LabelTag) };
                     Types.snd = List.Nil }
                 | Joint.Step_seq x ->
                   (match Identifiers.member PreIdentifiers.LabelTag visited'
                            (Obj.magic nxt) with
                    | Bool.True ->
                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
                        (Identifiers.add_set PreIdentifiers.LabelTag
                          (Identifiers.empty_set PreIdentifiers.LabelTag)
                          (Obj.magic nxt)) }; Types.snd = (List.Cons
                        ({ Types.fst = Types.None; Types.snd =
                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
                        x0) }, List.Nil)) }
                    | Bool.False ->
                      { Types.fst = { Types.fst = Nat.O; Types.snd =
                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
                        Types.snd = List.Nil }))
              | Joint.Final x ->
                { Types.fst = { Types.fst = Nat.O; Types.snd =
                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
                  Types.snd = List.Nil }
              | Joint.FCOND (x0, x1, x2) ->
                { Types.fst = { Types.fst = Nat.O; Types.snd =
                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
                  Types.snd = List.Nil }
            in
            graph_visit p globals g
              (Identifiers.union_set PreIdentifiers.LabelTag
                add_req_gen.Types.fst.Types.snd required') visited'
              (Obj.magic (List.append add_req_gen.Types.snd generated'))
              visiting'
              (Nat.plus add_req_gen.Types.fst.Types.fst (Nat.S gen_length))
              n' entry)) __)) __

(** val branch_compress :
    Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
    Types.sig0 -> __ **)
let branch_compress p globals g entry =
  g

(** val filter_labels :
    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> Bool.bool)
    -> 'a1 LabelledObjects.labelled_obj List.list -> (__, 'a1) Types.prod
    List.list **)
let filter_labels tag test c =
  List.map (fun s ->
    let { Types.fst = l_opt; Types.snd = x } = s in
    { Types.fst =
    (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
      match test l with
      | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
      | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)

(** val linearise_code :
    Joint.uns_params -> AST.ident List.list -> __ -> Graphs.label Types.sig0
    -> (__, Graphs.label -> Nat.nat Types.option) Types.prod Types.sig0 **)
let linearise_code p globals g entry_sig =
  let g0 = branch_compress p globals g entry_sig in
  let triple =
    graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
      (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
      (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
      (Types.pi1 entry_sig)
  in
  let sigma = triple.Types.fst.Types.fst in
  let required = triple.Types.fst.Types.snd in
  let crev = triple.Types.snd in
  let lbld_code = Util.rev (Obj.magic crev) in
  { Types.fst =
  (Obj.magic
    (filter_labels PreIdentifiers.LabelTag (fun l ->
      Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
  Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }

(** val linearise_int_fun :
    Joint.uns_params -> AST.ident List.list ->
    Joint.joint_closed_internal_function ->
    (Joint.joint_closed_internal_function, Graphs.label -> Nat.nat
    Types.option) Types.prod Types.sig0 **)
let linearise_int_fun p globals f_sig =
  let code_sigma =
    linearise_code p globals (Types.pi1 f_sig).Joint.joint_if_code
      (Obj.magic (Types.pi1 f_sig).Joint.joint_if_entry)
  in
  let code = (Types.pi1 code_sigma).Types.fst in
  let sigma = (Types.pi1 code_sigma).Types.snd in
  { Types.fst = { Joint.joint_if_luniverse =
  (Types.pi1 f_sig).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
  (Types.pi1 f_sig).Joint.joint_if_runiverse; Joint.joint_if_result =
  (Types.pi1 f_sig).Joint.joint_if_result; Joint.joint_if_params =
  (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
  (Types.pi1 f_sig).Joint.joint_if_stacksize;
  Joint.joint_if_local_stacksize =
  (Types.pi1 f_sig).Joint.joint_if_local_stacksize; Joint.joint_if_code =
  code; Joint.joint_if_entry = (Obj.magic Nat.O) }; Types.snd = sigma }

(** val linearise :
    Joint.uns_params -> Joint.joint_program -> Joint.joint_program **)
let linearise p pr =
  Joint.transform_joint_program (Joint.graph_params_to_params p)
    (Joint.lin_params_to_params p) (fun globals f_in ->
    (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst) pr