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();