open preamble
open MachineTypeTheory ExpressionAbbrevsTheory

val _ = new_theory "DaisyMap";

val _ = Datatype `
  cmp = Lt | Eq | Gt`;

val expCompare_def = Define `
  expCompare (e1:real exp) e2 =
    case e1, e2 of
      |(Var (n1:num)), (Var n2) =>
                 if (n1 < n2)
                 then Lt
                 else
                     if (n1 = n2) then Eq else Gt
      | (Var n), _ => Lt
      | (Const _ _), Var _ => Gt
      | Const m1 v1, Const m2 v2 =>
          if m1 = m2
          then
              (if (v1 < v2)
               then Lt
               else if (v1 = v2)
               then Eq
               else Gt)
          else (if morePrecise m1 m2 then Lt else Gt)
      | Const _ _, _ => Lt
      | Unop u1 e1, Unop u2 e2 =>
        if u1 = u2
        then expCompare e1 e2
        else (if u1 = Neg then Lt else Gt)
      | Unop _ _, Binop _ _ _ => Lt
      | Unop _ _, Downcast _ _ => Lt
      | Unop _ _, _ => Gt
      | Downcast m1 e1, Downcast m2 e2 =>
          if m1 = m2
          then expCompare e1 e2
          else (if morePrecise m1 m2 then Lt else Gt)
      | Downcast _ _, Binop _ _ _ => Lt
      | Downcast _ _, _ => Gt
      | Binop b1 e11 e12, Binop b2 e21 e22 =>
        let res = case b1, b2 of
                 | Plus, Plus => Eq
                 | Plus, _ => Lt
                 | Sub, Sub => Eq
                 | Sub, Plus => Gt
                 | Sub, _ => Lt
                 | Mult, Mult => Eq
                 | Mult, Div => Lt
                 | Mult, _ => Gt
                 | Div, Div => Eq
                 | Div, _ => Gt
        in
          (case res of
             | Eq =>
               (case expCompare e11 e21  of
                  | Eq => expCompare e12 e22
                  | Lt => Lt
                  | Gt => Gt)
             | _ => res)
     |_ , _ => Gt`;

val DaisyMapList_insert_def = Define `
  (DaisyMapList_insert e k NIL = [(e,k)]) /\
  (DaisyMapList_insert e k ((e1,l1) :: el) =
   case expCompare e e1 of
     | Lt => (e,k)::(e1,l1)::el
     | Eq  => (e1,l1) :: el
     | Gt => (e1,l1):: DaisyMapList_insert e k el)`;

val DaisyMapList_find_def = Define `
  (DaisyMapList_find e NIL = NONE) /\
  (DaisyMapList_find e ((e1,k)::el) = if expCompare e e1 = Eq then SOME k else DaisyMapList_find e el)`;

val _ = Datatype `
  binTree = Node 'a binTree binTree | Leaf 'a | LeafN`;

val DaisyMapTree_insert_def = Define `
  (DaisyMapTree_insert e k LeafN = Leaf (e,k)) /\
  (DaisyMapTree_insert e k (Leaf (e1,k1)) =
     case (expCompare e e1) of
            | Lt => Node (e1,k1) (Leaf (e,k)) (LeafN)
            | Eq => Leaf (e1,k1)
            | Gt => Node (e1,k1) (LeafN) (Leaf (e,k))) /\
  (DaisyMapTree_insert e k (Node (e1,k1) tl tr) =
     case (expCompare e e1) of
            | Lt => Node (e1,k1) (DaisyMapTree_insert e k tl) tr
            | Eq => (Node (e1, k1) tl tr)
            | Gt => Node (e1,k1) tl (DaisyMapTree_insert e k tr))`;

val DaisyMapTree_find_def = Define `
  (DaisyMapTree_find e (LeafN) = NONE) /\
  (DaisyMapTree_find e (Leaf (e1,k1)) =
     if expCompare e e1 = Eq then SOME k1 else NONE) /\
  (DaisyMapTree_find e (Node (e1,k1) tl tr) =
    case (expCompare e e1) of
      | Lt => DaisyMapTree_find e tl
      | Eq => SOME k1
      | Gt => DaisyMapTree_find e tr)`;

val DaisyMapTree_mem_def = Define `
  DaisyMapTree_mem e tMap =
    case (DaisyMapTree_find e tMap) of
      | SOME _ => T
      | _ => F`;

val DaisyMapTree_empty_def = Define `
  DaisyMapTree_empty = LeafN `;

val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``);
val _ = type_abbrev ("DaisyMap", ``:(real exp # ((real # real) # error) binTree``);

val _ = export_theory();