***
***	This examples show how to implement maps using AC rewriting.
***	Insertion and lookup are O(log n) because of the new
***	AC/ACU term representation and matching/renormalization
***	algorithms.
***

fmod MAP is
  sort Domain Range Pair Map .
  subsort Pair < Map .

  op _|->_ : Domain Range -> Pair .
  op empty : -> Map .
  op _,_ : Map Map -> Map [assoc comm id: empty] .
  op undefined : -> [Range] .

  var D : Domain .
  vars R R' : Range .
  var M : Map .

  op _[_] : Map Domain -> [Range] .
  eq (M, D |-> R)[D] = R .
  eq M[D] = undefined [owise] .

  op insert : Domain Range Map -> Map .
  eq insert(D, R, (M, D |-> R')) = (M, D |-> R) .
  eq insert(D, R, M) = (M, D |-> R) [owise] .
endfm

***
***	We use the map for explicit memoization in calculating
***	Fibonacci modulo 100 (real Fibonacci grows to fast).
***

fmod MAP-TEST is
  pr MAP .
  pr NAT .
  subsort Nat < Domain Range .
  subsort Nat < Range .

  op f : Nat -> Map .

var N : Nat .

  eq f(0) = insert(0, 1, empty) .
  eq f(1) = insert(1, 1, f(0)) .
  eq f(s s N) = insert(s s N,
                       ((f(s N)[s N]) + (f(s N)[N])) rem 100,
                       f(s N)) .
endfm

red f(100)[50] .
red f(1000)[500] .
red f(10000)[5000] .
red f(100000)[50000] .