open DNList
open DPow
open DProd
open DSum
open DUnit
open Datatypes
open Fold
open Global
open InterNode
open IntraNode
open TStr

type __ = Obj.t

module Proc = DStr.DStr

module PowProc = Pow(Proc)

module GVar = DStr.DStr

module LVar = ProdKey2(Proc)(DStr.DStr)

module Var = SumKey2(GVar)(LVar)

module Field = DStr.DStr

module Fields = NListKey(Field)

module ExtAllocsite = SumKey2(Unit)(Proc)

module Allocsite = SumKey2(InterNode)(ExtAllocsite)

module VarAllocsite = SumKey2(Var)(Allocsite)

module FldLoc = ProdKey2(VarAllocsite)(Fields)

module Loc = SumKey2(FldLoc)(Proc)

module PowLoc = Pow(Loc)

(** val var_of_gvar : GVar.t -> Var.t **)

let var_of_gvar x =
  Var.Inl x

(** val var_of_lvar : LVar.t -> Var.t **)

let var_of_lvar x =
  Var.Inr x

(** val approx_one_loc : G.t -> Loc.t -> bool **)

let approx_one_loc g = function
| Loc.Inl a ->
  let (t0, t1) = a in
  (match t0 with
   | VarAllocsite.Inl a0 ->
     (match a0 with
      | Var.Inl _ ->
        (match t1 with
         | Fields.Coq_nil -> true
         | Fields.Coq_cons (_, _) -> false)
      | Var.Inr b ->
        let (f, _) = b in
        (match t1 with
         | Fields.Coq_nil -> negb (G.is_rec f g)
         | Fields.Coq_cons (_, _) -> false))
   | VarAllocsite.Inr _ -> false)
| Loc.Inr _ -> false

(** val is_local_of : DStr.DStr.t -> Loc.t' -> bool **)

let is_local_of f = function
| Loc.Inl a ->
  let (t0, _) = a in
  (match t0 with
   | VarAllocsite.Inl a0 ->
     (match a0 with
      | Var.Inl _ -> false
      | Var.Inr b ->
        let (g, _) = b in if DStr.DStr.eq_dec f g then true else false)
   | VarAllocsite.Inr _ -> false)
| Loc.Inr _ -> false

(** val loc_of_var : Var.t -> Loc.t **)

let loc_of_var x =
  Loc.Inl ((VarAllocsite.Inl x), Fields.Coq_nil)

(** val loc_of_allocsite : Allocsite.t -> Loc.t **)

let loc_of_allocsite x =
  Loc.Inl ((VarAllocsite.Inr x), Fields.Coq_nil)

(** val loc_of_proc : Proc.t -> Loc.t **)

let loc_of_proc x =
  Loc.Inr x

(** val append_field : Loc.t -> Field.t -> Loc.t **)

let append_field l f =
  match l with
  | Loc.Inl va -> Loc.Inl ((fst va), (Fields.app (snd va) f))
  | Loc.Inr _ -> l

module SMLocLoc = SetMap(Loc)(PowLoc)(Loc)(PowLoc)

(** val pow_loc_append_field : PowLoc.t -> Field.t -> PowLoc.t **)

let pow_loc_append_field ls f =
  SMLocLoc.map (fun l -> append_field l f) ls

(** val allocsite_of_node : InterNode.t -> Allocsite.t **)

let allocsite_of_node node =
  Allocsite.Inl node

(** val allocsite_of_ext : Proc.t option -> Allocsite.t **)

let allocsite_of_ext = function
| Some fid -> Allocsite.Inr (ExtAllocsite.Inr fid)
| None -> Allocsite.Inr (ExtAllocsite.Inl ())