include "basics/types.ma".

include "ASM/BitVectorTrie.ma".
include "common/Identifiers.ma".
include "common/AST.ma".

axiom LabelTag : String.

definition label ≝ identifier LabelTag.

(* o'caml compiler doesn't make distinction between idents and labels *)
definition label_to_ident: label → ident ≝
  λl.
  match l with
  [ an_identifier l ⇒ an_identifier SymbolTag l
  ].

definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.

definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.

definition graph_fold ≝
  λA, B: Type[0].
  λf.
  λgraph: graph A.
  λseed: B.
  match graph with
  [ an_id_map map ⇒ fold A B f map seed
  ].

axiom graph_add:
  ∀A: Type[0].
  ∀g: graph A.
  ∀l: label.
  ∀s: A.
    lookup ? ? (add ? ? g l s) l ≠ None ?.

axiom graph_add_lookup:
  ∀A: Type[0].
  ∀g: graph A.
  ∀l: label.
  ∀s: A.
  ∀to_insert: label.
    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.

axiom graph_num_nodes:
  ∀A: Type[0].
  ∀g: graph A.
    nat.