namespace.lem

(*
  Defines a datatype for nested namespaces where names can be either
  short (e.g. foo) or long (e.g. ModuleA.InnerB.bar).
*)
open import Pervasives
open import Set_extra

type alist 'k 'v = list ('k * 'v)

(* Identifiers *)
type id 'm 'n =
  | Short of 'n
  | Long of 'm * id 'm 'n

val mk_id : forall 'n 'm. list 'm -> 'n -> id 'm 'n
let rec mk_id [] n = Short n
    and mk_id (mn::mns) n = Long mn (mk_id mns n)
declare termination_argument mk_id = automatic

val id_to_n : forall 'n 'm. id 'm 'n -> 'n
let rec id_to_n (Short n) = n
    and id_to_n (Long _ id) = id_to_n id
declare termination_argument id_to_n = automatic

val id_to_mods : forall 'n 'm. id 'm 'n -> list 'm
let rec id_to_mods (Short _) = []
    and id_to_mods (Long mn id) = mn :: id_to_mods id
declare termination_argument id_to_mods = automatic

type namespace 'm 'n 'v =
  Bind of alist 'n 'v * alist 'm (namespace 'm 'n 'v)

val nsLookup : forall 'v 'm 'n. Eq 'n, Eq 'm => namespace 'm 'n 'v -> id 'm 'n -> maybe 'v
let rec nsLookup (Bind v m) (Short n) = List.lookup n v
    and nsLookup (Bind v m) (Long mn id) =
      match List.lookup mn m with
      | Nothing -> Nothing
      | Just env -> nsLookup env id
      end
declare termination_argument nsLookup = automatic

val nsLookupMod : forall 'm 'n 'v. Eq 'n, Eq 'm => namespace 'm 'n 'v -> list 'm -> maybe (namespace 'm 'n 'v)
let rec nsLookupMod e [] = Just e
    and nsLookupMod (Bind v m) (mn::path) =
      match List.lookup mn m with
      | Nothing -> Nothing
      | Just env -> nsLookupMod env path
      end
declare termination_argument nsLookupMod = automatic

val nsEmpty : forall 'v 'm 'n. namespace 'm 'n 'v
let nsEmpty = Bind [] []

val nsAppend : forall 'v 'm 'n. namespace 'm 'n 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v
let nsAppend (Bind v1 m1) (Bind v2 m2) = Bind (v1 ++ v2) (m1 ++ m2)

val nsLift : forall 'v 'm 'n. 'm -> namespace 'm 'n 'v -> namespace 'm 'n 'v
let nsLift mn env = Bind [] [(mn, env)]

val alist_to_ns : forall 'v 'm 'n. alist 'n 'v -> namespace 'm 'n 'v
let alist_to_ns a = Bind a []

val nsBind : forall 'v 'm 'n. 'n -> 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v
let nsBind k x (Bind v m) = Bind ((k,x)::v) m

val nsBindList : forall 'v 'm 'n. list ('n * 'v) -> namespace 'm 'n 'v -> namespace 'm 'n 'v
let nsBindList l e = List.foldr (fun (x,v) e -> nsBind x v e) e l

val nsOptBind : forall 'v 'm 'n. maybe 'n -> 'v -> namespace 'm 'n 'v -> namespace 'm 'n 'v
let nsOptBind n x env =
  match n with
  | Nothing -> env
  | Just n' -> nsBind n' x env
  end

val nsSing : forall 'v 'm 'n. 'n -> 'v -> namespace 'm 'n 'v
let nsSing n x = Bind ([(n,x)]) []

val nsSub : forall 'v1 'v2 'm 'n. Eq 'm, Eq 'n, Eq 'v1, Eq 'v2 =>
  (id 'm 'n -> 'v1 -> 'v2 -> bool) -> namespace 'm 'n 'v1 -> namespace 'm 'n 'v2 -> bool
let nsSub r env1 env2 =
  (forall id v1.
    nsLookup env1 id = Just v1
    -->
    exists v2. nsLookup env2 id = Just v2 && r id v1 v2)
  &&
  (forall path.
    nsLookupMod env2 path = Nothing --> nsLookupMod env1 path = Nothing)

val nsAll : forall 'v 'm 'n. Eq 'm, Eq 'n, Eq 'v => (id 'm 'n -> 'v -> bool) -> namespace 'm 'n 'v -> bool
let rec nsAll f env =
  (forall id v.
     nsLookup env id = Just v
     -->
     f id v)

val eAll2 : forall 'v1 'v2 'm 'n. Eq 'm, Eq 'n, Eq 'v1, Eq 'v2 =>
   (id 'm 'n -> 'v1 -> 'v2 -> bool) -> namespace 'm 'n 'v1 -> namespace 'm 'n 'v2 -> bool
let nsAll2 r env1 env2 =
  nsSub r env1 env2 &&
  nsSub (fun x y z -> r x z y) env2 env1

val nsDom : forall 'v 'm 'n. Eq 'm, Eq 'n, Eq 'v, SetType 'v => namespace 'm 'n 'v -> set (id 'm 'n)
let nsDom env = { n | forall (v IN universal) (n IN universal) | nsLookup env n = Just v }

val nsDomMod : forall 'v 'm 'n. SetType 'm, Eq 'm, Eq 'n, Eq 'v => namespace 'm 'n 'v -> set (list 'm)
let nsDomMod env = { n | forall (v IN universal) (n IN universal) | nsLookupMod env n = Just v }

val nsMap : forall 'v 'w 'm 'n. ('v -> 'w) -> namespace 'm 'n 'v -> namespace 'm 'n 'w
let rec nsMap f (Bind v m) =
  Bind (List.map (fun (n,x) -> (n, f x)) v)
       (List.map (fun (mn,e) -> (mn, nsMap f e)) m)