WIP state

hol4/DaisyMapScript.sml

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

hol4/Infra/DaisyTactics.sml

@@ -112,4 +112,34 @@ fun daisy_eval_tac t :tactic=
     \\ fs[sptreeTheory.lookup_def]
 end;
 
+fun case_destruct_tac thm =
+let
+  val conclusion = concl thm;
+  val caseTerm = find_term TypeBase.is_case conclusion;
+  val (_, caseOn, _) = TypeBase.dest_case caseTerm
+  val _ = print ("Case analysis on ")
+  val _ = print_term caseOn in
+    BasicProvers.Cases_on `^caseOn`
+end;
+
+fun case_compute_tac pat =
+  qpat_x_assum pat
+               (fn thm => REPEAT (case_destruct_tac thm \\ fs[]));
+
+fun const_type_length cst =
+let
+    val holObj = dest_thy_const cst;
+    val t = #Ty holObj;
+    val (_, typeParamsList) = dest_type t in
+    length typeParamsList
+end
+
+fun foo t =
+  let
+      val as_str = term_to_string t in
+      map const_type_length (decls as_str)
+end;
+mk_comb (``typeCheck``,``_:real exp``)
+dest_term ``typeCheck _``
+
 end

hol4/Infra/MachineTypeScript.sml

@@ -41,6 +41,41 @@ val mTypeToQ_pos = store_thm("mTypeToQ_pos",
 val isMorePrecise_def = Define `
   isMorePrecise (m1:mType) (m2:mType) = (mTypeToQ (m1) <= mTypeToQ (m2))`;
 
+val morePrecise_def = Define `
+  (morePrecise M0 _ = T) /\
+  (morePrecise M16 M16 = T) /\
+  (morePrecise M32 M32 = T) /\
+  (morePrecise M32 M16 = T) /\
+  (morePrecise M64 M0 = F) /\
+  (morePrecise M64 _ = T) /\
+  (morePrecise _ _ = F) `;
+
+val morePrecise_antisym = store_thm (
+  "morePrecise_antisym",
+  ``!m1 m2.
+      morePrecise m1 m2 /\
+      morePrecise m2 m1 ==>
+      m1 = m2``,
+ rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]);
+
+val morePrecise_trans = store_thm (
+  "morePrecise_trans",
+  ``!m1 m2 m3.
+      morePrecise m1 m2 /\
+      morePrecise m2 m3 ==>
+      morePrecise m1 m3``,
+  rpt strip_tac
+  \\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
+  \\ fs[morePrecise_def]);
+
+val isMorePrecise_morePrecise = store_thm (
+  "isMorePrecise_morePrecise",
+  ``!m1 m2.
+    isMorePrecise m1 m2 = morePrecise m1 m2``,
+  rpt strip_tac
+  \\ Cases_on `m1` \\ Cases_on `m2`
+  \\ fs[morePrecise_def, isMorePrecise_def, mTypeToQ_def]);
+
 val M0_least_precision = store_thm ("M0_least_precision",
   ``!(m:mType).
       isMorePrecise m M0 ==>

hol4/TypingScript.sml

 open preamble miscTheory
 open DaisyTactics
-open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory CommandsTheory
-open IntervalValidationTheory
+open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
+     CommandsTheory IntervalValidationTheory DaisyMapTheory
 
 val _ = new_theory "Typing";
 
@@ -23,19 +23,52 @@ val typeExpression_def = Define `
         | SOME m1 => if (isMorePrecise m1 m) then SOME m else NONE
         | NONE => NONE`
 
+(* val typeMap_def = Define ` *)
+(*   typeMap (Gamma: num -> mType option) (e: real exp) (e': real exp) : mType option = *)
+(*     case e of *)
+(*       | Var v => (if (e = e') then Gamma v else NONE) *)
+(*       | Const m n => if e = e' then SOME m else NONE *)
+(*       | Unop u e1 => if e = e' then typeExpression Gamma e else typeMap Gamma e1 e' *)
+(*       | Binop b e1 e2 => if e = e' then typeExpression Gamma e *)
+(*                          else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e') of *)
+(*                                 | SOME m1, SOME m2 => (if (m1 = m2) then SOME m1 else NONE) *)
+(*                                 | SOME m1, NONE => SOME m1 *)
+(*                                 | NONE, SOME m2 => SOME m2 *)
+(*                                 | NONE, NONE => NONE) *)
+(*       | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'` *)
+
 val typeMap_def = Define `
-  typeMap (Gamma: num -> mType option) (e: real exp) (e': real exp) : mType option =
-    case e of
-      | Var v => (if (e = e') then Gamma v else NONE)
-      | Const m n => if e = e' then SOME m else NONE
-      | Unop u e1 => if e = e' then typeExpression Gamma e else typeMap Gamma e1 e'
-      | Binop b e1 e2 => if e = e' then typeExpression Gamma e
-                         else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e') of
-                                | SOME m1, SOME m2 => (if (m1 = m2) then SOME m1 else NONE)
-                                | SOME m1, NONE => SOME m1
-                                | NONE, SOME m2 => SOME m2
-                                | NONE, NONE => NONE)
-      | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'`
+  typeMap (Gamma:num -> mType option) (e:real exp) (tMap:typeMap) =
+    if (DaisyMapTree_mem e tMap)
+    then tMap
+    else
+      case e of
+        | Var v => (case (Gamma v) of
+                     | SOME m => DaisyMapTree_insert e m tMap
+                     | NONE => DaisyMapTree_empty)
+        | Const m n => DaisyMapTree_insert e m tMap
+        | Unop u e1 =>
+          let tMap_new = typeMap Gamma e1 tMap in
+          (case DaisyMapTree_find e1 tMap_new of
+          | SOME m_e1 => DaisyMapTree_insert e m_e1 tMap
+          | NONE => DaisyMapTree_empty)
+        | Binop b e1 e2 =>
+          let tMap1 = typeMap Gamma e1 tMap in
+          let tMap2 = typeMap Gamma e2 tMap1 in
+          let m1 = DaisyMapTree_find e1 tMap2 in
+          let m2 = DaisyMapTree_find e2 tMap2 in
+          (case m1, m2 of
+           | SOME t1, SOME t2 => DaisyMapTree_insert e (join t1 t2) tMap2
+           | _ , _ => DaisyMapTree_empty)
+        | Downcast m e1 =>
+          let tMap_new = typeMap Gamma e1 tMap in
+          let m1 = DaisyMapTree_find e1 tMap in
+          (case m1 of
+             | SOME t1 =>
+               (if morePrecise t1 m
+                then DaisyMapTree_insert e m tMap_new
+                else DaisyMapTree_empty)
+             | _ =>  DaisyMapTree_empty)`;
 
 val typeCmd_def = Define `
   typeCmd (Gamma: num -> mType option) (f: real cmd) : mType option =
@@ -45,23 +78,37 @@ val typeCmd_def = Define `
                           | NONE => NONE)
       | Ret e => typeExpression Gamma e`
 
+(* val typeMapCmd_def = Define ` *)
+(*   typeMapCmd (Gamma: num -> mType option) (f: real cmd) (f': real exp) : mType option = *)
+(*     case f of *)
+(*       | Let m n e c => if f' = (Var n) then (*FIXME: This may fail because n not in Gamma... *) *)
+(*                            (case Gamma n of *)
+(*                               | SOME m' => if isMorePrecise m m' then SOME m else NONE *)
+(*                               | NONE => NONE) *)
+(*                        else *)
+(*                            let te = typeMap Gamma e in *)
+(*                            let tc = typeMapCmd Gamma c in *)
+(*                            (case (te f', tc f') of *)
+(*                              | SOME m1, SOME m2 => if (m1 = m2) then SOME m1 else NONE *)
+(*                              | SOME m1, NONE => SOME m1 *)
+(*                              | NONE, SOME m2 => SOME m2 *)
+(*                              | NONE, NONE => NONE) *)
+(*      | Ret e => typeMap Gamma e f'` *)
+
 val typeMapCmd_def = Define `
-  typeMapCmd (Gamma: num -> mType option) (f: real cmd) (f': real exp) : mType option =
+  typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) =
     case f of
-      | Let m n e c => if f' = (Var n) then (*FIXME: This may fail because n not in Gamma... *)
-                           (case Gamma n of
-                              | SOME m' => if isMorePrecise m m' then SOME m else NONE
-                              | NONE => NONE)
-                       else
-                           let te = typeMap Gamma e in
-                           let tc = typeMapCmd Gamma c in
-                           (case (te f', tc f') of
-                             | SOME m1, SOME m2 => if (m1 = m2) then SOME m1 else NONE
-                             | SOME m1, NONE => SOME m1
-                             | NONE, SOME m2 => SOME m2
-                             | NONE, NONE => NONE)
-     | Ret e => typeMap Gamma e f'`
-
+      | Let m n e c =>
+          let tMap_new = typeMap Gamma e tMap in
+          let tc = typeMapCmd Gamma c tMap_new in
+          let mN = Gamma n in
+          (case mN of
+             | SOME m_n =>
+               if morePrecise m m_n
+               then DaisyMapTree_insert (Var n) m tc
+               else DaisyMapTree_empty
+             | _ => DaisyMapTree_empty)
+      | Ret e => typeMap Gamma e tMap`;
 
 val typeCheck_def = Define `
   typeCheck (e:real exp) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
@@ -105,7 +152,14 @@ val typingSoundnessExp = store_thm("typingSoundnessExp",
     typeCheck e Gamma expTypes /\
     eval_exp E Gamma e v m ==>
     (expTypes e = SOME m)``,
-  Induct_on `e` \\ rpt strip_tac \\ fs []
+rpt strip_tac
+
+    \\ qpat_x_assum `typeCheck` kall_tac
+  Induct_on `e` \\ rpt strip_tac
+  \\ qpat_x_assum `typeCheck _ _ _`
+       (fn thm => assume_tac (computeLib.RESTR_EVAL_RULE (decls "typeCheck") (ONCE_REWRITE_RULE [Once typeCheck_def] thm)) )
+  \\ fs [] \\ rveq
+  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
   >- (inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
      \\ fs [typeCheck_def]
      \\ Cases_on `expTypes (Var n)` \\ fs [])