include "basics/types.ma".
include "ASM/String.ma".
include "ASM/Arithmetic.ma".
include "common/Errors.ma".

(* identifiers and their generators are tagged to differentiate them, and to
   provide extra type checking. *)

(* in common/PreIdentifiers.ma, via Errors.ma.
inductive identifier (tag:String) : Type[0] ≝
  an_identifier : Word → identifier tag.
*)

record universe (tag:String) : Type[0] ≝
  { next_identifier : Word }.


definition new_universe : ∀tag:String. universe tag ≝
  λtag. mk_universe tag (zero ?).

axiom OutOfIdentifiers : String.

definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
λtag,g.
  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
    if get_index_v ?? carries 0 ? then Error ? (msg OutOfIdentifiers) else
      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
// qed.

definition eq_identifier ≝
  λt.
  λl, r: identifier t.
  match l with
  [ an_identifier l' ⇒
    match r with
    [ an_identifier r' ⇒
      eq_bv ? l' r'
    ]
  ].
    
    
definition word_of_identifier ≝
  λt.
  λl: identifier t.
  match l with    
  [ an_identifier l' ⇒ l'
  ].

definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
#E [ % | %2 ]
lapply E @eq_bv_elim
[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
qed.

definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
  λtag,n. an_identifier tag (bitvector_of_nat ? n).


(* Maps from identifiers to arbitrary types. *)

include "ASM/BitVectorTrie.ma".

inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
  
definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
  λtag,A. an_id_map tag A (Stub A 16).

definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
                              (match m with [ an_id_map m' ⇒ m' ]).

(* Always adds the identifier to the map. *)
definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
                                           (match m with [ an_id_map m' ⇒ m' ])).

axiom MissingId : String.

(* Only updates an existing entry; fails with an error otherwise. *)
definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
λtag,A,m,l,a.
  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
                    (match m with [ an_id_map m' ⇒ m' ]) with
  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
  | Some m' ⇒ OK ? (an_id_map tag A m')
  ].

(* Sets *)

inductive identifier_set (tag:String) : Type[0] ≝
  an_id_set : BitVectorTrie unit 16 → identifier_set tag.

definition empty_set : ∀tag:String. identifier_set tag ≝
λtag. an_id_set tag (Stub unit 16).

definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
                                     it (match s with [ an_id_set s' ⇒ s' ])).

definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
λtag,i. add_set tag (empty_set tag) i.

definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
                                (match s with [ an_id_set s' ⇒ s' ]) with
          [ None ⇒ false
          | Some _ ⇒ true
          ].

definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
                                        (match s' with [ an_id_set s1 ⇒ s1 ])).

interpretation "identifier set union" 'union a b = (union_set ? a b).
notation "∅" non associative with precedence 90 for @{ 'empty }.
interpretation "empty identifier set" 'empty = (empty_set ?).
interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).