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_eq:
  ∀A: Type[0].
  ∀g: graph A.
  ∀l: label.
  ∀s: A.
    lookup ? ? (add ? ? g l s) l = Some ? s.

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_add_preserve :
  ∀A: Type[0].
  ∀g: graph A.
  ∀l: label.
  ∀s: A.
  ∀to_insert: label.
  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.

definition graph_num_nodes:
  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
  
lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
#A#P#H#g
lapply (refl ? (|g|))
generalize in ⊢(???%→?);
#n lapply g -g
@(nat_elim1 … n)
#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
qed.