Get semantics dir to build #79

compiler/backend/backend_commonScript.sml

@@ -43,4 +43,27 @@ val bvl_num_stubs_def = Define`
   bvl_num_stubs = data_num_stubs + 5
 `;
 
+val _ = Datatype `
+  fp_cmp =
+    | FP_Less
+    | FP_LessEqual
+    | FP_Greater
+    | FP_GreaterEqual
+    | FP_Equal`
+
+val _ = Datatype `
+  fp_uop =
+ (* | FP_ToInt *)
+    | FP_FromInt
+    | FP_Abs
+    | FP_Neg
+    | FP_Sqrt`
+
+val _ = Datatype `
+  fp_bop =
+    | FP_Add
+    | FP_Sub
+    | FP_Mul
+    | FP_Div`
+
 val _ = export_theory();

compiler/backend/closLangScript.sml

@@ -1,4 +1,4 @@
-open preamble;
+open preamble backend_commonTheory;
 
 val _ = new_theory "closLang";
 
@@ -50,7 +50,10 @@ val _ = Datatype `
      | WordOp word_size opw
      | WordShift word_size shift num
      | WordFromInt
-     | WordToInt`
+     | WordToInt
+     | FP_cmp fp_cmp
+     | FP_uop fp_uop
+     | FP_bop fp_bop`
 
 val _ = Datatype `
   exp = Var num

compiler/backend/proofs/bvi_to_dataProofScript.sml

@@ -5,6 +5,7 @@ open preamble
      data_simpProofTheory
      data_liveProofTheory
      data_spaceProofTheory;
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory"bvi_to_dataProof";
 

compiler/backend/proofs/bvl_to_bviProofScript.sml

@@ -8,6 +8,7 @@ local open
   bvi_letProofTheory
   bvl_inlineProofTheory
 in end;
+val _ = Parse.hide "exp";
 
 val _ = new_theory"bvl_to_bviProof";
 
@@ -139,7 +140,7 @@ val v_to_list_ok = Q.prove(
          EVERY (bv_ok refs) x`,
   ho_match_mp_tac v_to_list_ind >>
   simp[v_to_list_def,bv_ok_def] >> srw_tac[][] >>
-  every_case_tac >> full_simp_tac(srw_ss())[] >> srw_tac[][])
+  every_case_tac >> full_simp_tac(srw_ss())[] >> srw_tac[][]);
 
 val do_app_ok_lemma = Q.prove(
   `state_ok r /\ EVERY (bv_ok r.refs) a /\
@@ -403,7 +404,7 @@ val evaluate_CopyGlobals_code = Q.prove(
     simp[Abbr`ss`] >> EVAL_TAC >>
     simp[state_component_equality] ) >>
   simp[Abbr`ss`] >>
-  `&SUC n - 1 = &n` by (
+  `&SUC n - 1 = &n:int` by (
     simp[ADD1] >> intLib.COOPER_TAC ) >>
   simp[state_component_equality] >>
   simp[Abbr`rf`,fmap_eq_flookup,FLOOKUP_UPDATE] >>
@@ -462,7 +463,7 @@ val evaluate_AllocGlobal_code = Q.prove(
     simp[Abbr`ss`] >> EVAL_TAC >>
     simp[state_component_equality] ) >>
   simp[Abbr`ss`] >>
-  `&SUC n - 1 = &n` by (Cases_on`n`>>full_simp_tac(srw_ss())[]>>simp[ADD1]>>intLib.COOPER_TAC) >> full_simp_tac(srw_ss())[] >>
+  `&SUC n - 1 = &n:int` by (Cases_on`n`>>full_simp_tac(srw_ss())[]>>simp[ADD1]>>intLib.COOPER_TAC) >> full_simp_tac(srw_ss())[] >>
   simp[Abbr`rf`,fmap_eq_flookup,FLOOKUP_UPDATE,state_component_equality] >>
   srw_tac[][] >> simp[] >> TRY(intLib.COOPER_TAC) >>
   `n = LENGTH ls`by decide_tac >>
@@ -498,7 +499,7 @@ val evaluate_ListLength_code = Q.store_thm("evaluate_ListLength_code",
    (unabbrev_all_tac \\ fs [bviSemTheory.state_component_equality,
        bviSemTheory.dec_clock_def])
   \\ fs [] \\ pop_assum kall_tac
-  \\ `(1 + &n) = (&(n + 1))` by intLib.COOPER_TAC \\ fs []);
+  \\ `(1 + &n) = (&(n + 1)):int` by intLib.COOPER_TAC \\ fs []);
 
 val evaluate_FromListByte_code = Q.store_thm("evaluate_FromListByte_code",
   `∀lv vs n bs (s:'ffi bviSem$state).

compiler/backend/proofs/clos_annotateProofScript.sml

@@ -3,6 +3,7 @@ open preamble
      closSemTheory closPropsTheory
      clos_freeTheory clos_freeProofTheory
      clos_annotateTheory;
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory"clos_annotateProof";
 

compiler/backend/proofs/clos_numberProofScript.sml

@@ -1,4 +1,5 @@
 open preamble closLangTheory clos_numberTheory closSemTheory closPropsTheory;
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory"clos_numberProof";
 

compiler/backend/proofs/data_to_wordPropsScript.sml

@@ -2,6 +2,7 @@ open preamble bvlSemTheory dataSemTheory dataPropsTheory copying_gcTheory
      int_bitwiseTheory wordSemTheory data_to_wordTheory set_sepTheory
      labSemTheory whileTheory helperLib alignmentTheory multiwordTheory
 local open blastLib in end;
+val _ = map Parse.hide ["exp","max","pos"];
 
 val shift_def = wordLangTheory.shift_def;
 val good_dimindex_def = labPropsTheory.good_dimindex_def;
@@ -194,7 +195,7 @@ val v_size_LEMMA = Q.prove(
 
 val small_int_def = Define `
   small_int (:'a) i <=>
-    -&(dimword (:'a) DIV 8) <= i /\ i < &(dimword (:'a) DIV 8)`
+    -&(dimword (:'a) DIV 8) <= i /\ i < &(dimword (:'a) DIV 8):int`
 
 (*
   code pointers (i.e. Locs) will end in ...0
@@ -2729,7 +2730,7 @@ val memory_rel_El = Q.store_thm("memory_rel_El",
     \\ fs [word_heap_APPEND,word_heap_def,word_el_def,word_payload_def]
     \\ full_simp_tac (std_ss++sep_cond_ss) [cond_STAR]
     \\ `small_int (:α) (&index)` by
-     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k``]
+     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k:int``]
       \\ fs [labPropsTheory.good_dimindex_def,dimword_def] \\ rw [] \\ rfs [])
     \\ fs [] \\ clean_tac \\ fs [word_addr_def]
     \\ fs [Smallnum_def,GSYM word_mul_n2w,word_ml_inv_num_lemma] \\ NO_TAC)
@@ -2791,7 +2792,7 @@ val memory_rel_Deref = Q.store_thm("memory_rel_Deref",
     \\ fs [word_heap_APPEND,word_heap_def,word_el_def,word_payload_def]
     \\ full_simp_tac (std_ss++sep_cond_ss) [cond_STAR]
     \\ `small_int (:α) (&index)` by
-     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k``]
+     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k:int``]
       \\ fs [labPropsTheory.good_dimindex_def,dimword_def]
       \\ rw [] \\ rfs [] \\ fs [] \\ NO_TAC)
     \\ fs [] \\ clean_tac \\ fs [word_addr_def]
@@ -2874,7 +2875,7 @@ val memory_rel_Update = Q.store_thm("memory_rel_Update",
     \\ fs [word_heap_APPEND,word_heap_def,word_el_def,word_payload_def]
     \\ full_simp_tac (std_ss++sep_cond_ss) [cond_STAR]
     \\ `small_int (:α) (&index)` by
-     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k``]
+     (fs [small_int_def,intLib.COOPER_CONV ``-&n <= &k:int``]
       \\ fs [labPropsTheory.good_dimindex_def,dimword_def]
       \\ rw [] \\ rfs [] \\ fs [] \\ NO_TAC)
     \\ fs [] \\ clean_tac \\ fs [word_addr_def]

compiler/backend/proofs/word_allocProofScript.sml

@@ -1,6 +1,7 @@
 open preamble
      reg_allocTheory reg_allocProofTheory
      wordLangTheory wordSemTheory wordPropsTheory word_allocTheory
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory "word_allocProof";
 
@@ -5998,7 +5999,7 @@ val ssa_cc_trans_pre_alloc_conventions = Q.store_thm("ssa_cc_trans_pre_alloc_con
   imp_res_tac list_next_var_rename_lemma_2>>
   pop_assum(qspecl_then[`ssa`,`na+2`] assume_tac)>>rev_full_simp_tac(srw_ss())[LET_THM]>>
   qabbrev_tac `lss = MAP (λx. THE(lookup x ssa')) ls`>>
-  (qabbrev_tac `lss' = MAP (option_lookup ssa' o FST) (toAList s)`  
+  (qabbrev_tac `lss' = MAP (option_lookup ssa' o FST) (toAList s)`
    ORELSE
    qabbrev_tac `lss' = MAP (option_lookup ssa' o FST) (toAList s0)`)>>
   `∀x. MEM x lss' ⇒ MEM x lss` by

compiler/backend/semantics/bviSemScript.sml

@@ -1,5 +1,6 @@
 open preamble bviTheory;
 local open backend_commonTheory bvlSemTheory in end;
+val _ = map Parse.hide ["exp","max"];
 
 val _ = new_theory"bviSem";
 
@@ -34,7 +35,7 @@ val bvl_to_bvi_def = Define `
             ; ffi := s.ffi |>`;
 
 val small_enough_int_def = Define `
-  small_enough_int i <=> -268435457 <= i /\ i <= 268435457`;
+  small_enough_int i <=> -268435457 <= i /\ i <= 268435457:int`;
 
 val do_app_aux_def = Define `
   do_app_aux op (vs:bvlSem$v list) (s:'ffi bviSem$state) =

compiler/backend/semantics/bvlSemScript.sml

@@ -1,4 +1,5 @@
 open preamble bvlTheory closSemTheory
+val _ = Parse.hide "exp";
 
 val _ = new_theory"bvlSem"
 
@@ -230,6 +231,18 @@ val do_app_def = Define `
                       s with <| refs := s.refs |+ (ptr,ByteArray F ws')
                               ; ffi  := ffi'|>))
          | _ => Error)
+    | (FP_bop bop, ws) =>
+        (case ws of
+         | [Word64 w1; Word64 w2] => (Rval (Word64 (fp_bop bop w1 w2),s))
+         | _ => Error)
+    | (FP_uop uop, ws) =>
+        (case ws of
+         | [Word64 w] => (Rval (Word64 (fp_uop uop w),s))
+         | _ => Error)
+    | (FP_cmp cmp, ws) =>
+        (case ws of
+         | [Word64 w1; Word64 w2] => (Rval (Boolv (fp_cmp cmp w1 w2),s))
+         | _ => Error)
     | _ => Error`;
 
 val dec_clock_def = Define `

compiler/backend/semantics/closPropsScript.sml

@@ -1,4 +1,5 @@
 open preamble closLangTheory closSemTheory
+val _ = map Parse.hide ["exp","max"];
 
 val _ = new_theory"closProps"
 

compiler/backend/semantics/closSemScript.sml

@@ -1,4 +1,5 @@
-open preamble closLangTheory conLangTheory
+open preamble closLangTheory conLangTheory fpSemTheory
+val _ = Parse.hide "exp";
 
 val _ = new_theory"closSem"
 
@@ -241,6 +242,18 @@ val do_app_def = Define `
                       s with <| refs := s.refs |+ (ptr,ByteArray f ws')
                               ; ffi   := ffi'|>))
          | _ => Error)
+    | (FP_bop bop, ws) =>
+        (case ws of
+         | [Word64 w1; Word64 w2] => (Rval (Word64 (fp_bop bop w1 w2),s))
+         | _ => Error)
+    | (FP_uop uop, ws) =>
+        (case ws of
+         | [Word64 w] => (Rval (Word64 (fp_uop uop w),s))
+         | _ => Error)
+    | (FP_cmp cmp, ws) =>
+        (case ws of
+         | [Word64 w1; Word64 w2] => (Rval (Boolv (fp_cmp cmp w1 w2),s))
+         | _ => Error)
     | _ => Error`;
 
 val dec_clock_def = Define `

compiler/backend/semantics/conPropsScript.sml

@@ -1,4 +1,5 @@
 open preamble conSemTheory
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory"conProps"
 
@@ -340,7 +341,7 @@ val pmatch_any_match = Q.store_thm("pmatch_any_match",
   BasicProvers.CASE_TAC >>
   full_simp_tac(srw_ss())[] >> strip_tac >> full_simp_tac(srw_ss())[LET_THM] >>
   BasicProvers.CASE_TAC >> full_simp_tac(srw_ss())[] >>
-  TRY BasicProvers.CASE_TAC >> full_simp_tac(srw_ss())[] >> srw_tac[][] >> rev_full_simp_tac(srw_ss())[] >> full_simp_tac(srw_ss())[] >>
+  every_case_tac >> fs [] >>
   metis_tac[semanticPrimitivesTheory.match_result_distinct])
 
 val pmatch_any_no_match = Q.store_thm("pmatch_any_no_match",
@@ -355,7 +356,7 @@ val pmatch_any_no_match = Q.store_thm("pmatch_any_no_match",
   full_simp_tac(srw_ss())[] >> strip_tac >> full_simp_tac(srw_ss())[LET_THM] >>
   BasicProvers.CASE_TAC >> full_simp_tac(srw_ss())[] >>
   imp_res_tac pmatch_any_match >>
-  TRY BasicProvers.CASE_TAC >> full_simp_tac(srw_ss())[] >> srw_tac[][] >> rev_full_simp_tac(srw_ss())[] >> full_simp_tac(srw_ss())[] >>
+  every_case_tac >> fs [] >>
   metis_tac[semanticPrimitivesTheory.match_result_distinct]);
 
 val eval_decs_num_defs = Q.store_thm("eval_decs_num_defs",

compiler/backend/semantics/conSemScript.sml

@@ -1,4 +1,5 @@
 open preamble conLangTheory
+val _ = map Parse.hide ["exp","max"];
 
 val _ = new_theory"conSem"
 

compiler/backend/semantics/dataSemScript.sml

@@ -1,5 +1,6 @@
 open preamble dataLangTheory bvi_to_dataTheory;
 local open bvlSemTheory bvlPropsTheory bviSemTheory in end;
+val _ = Parse.hide "exp";
 
 val _ = new_theory"dataSem";
 

compiler/backend/semantics/decSemScript.sml

@@ -1,4 +1,5 @@
 open preamble conSemTheory
+val _ = Parse.hide "exp";
 
 val _ = new_theory"decSem"
 

compiler/backend/semantics/exhSemScript.sml

@@ -1,4 +1,5 @@
 open preamble exhLangTheory
+val _ = Parse.hide "exp";
 
 val _ = new_theory"exhSem"
 

compiler/backend/semantics/labSemScript.sml

@@ -1,5 +1,6 @@
 open preamble labLangTheory wordSemTheory;
 local open alignmentTheory targetSemTheory in end;
+val _ = map Parse.hide ["exp","max","pos"];
 
 val _ = new_theory"labSem";
 
@@ -183,7 +184,8 @@ val asm_inst_def = Define `
   (asm_inst Skip s = (s:('a,'ffi) labSem$state)) /\
   (asm_inst (Const r imm) s = upd_reg r (Word imm) s) /\
   (asm_inst (Arith x) s = arith_upd x s) /\
-  (asm_inst (Mem m r a) s = mem_op m r a s)`;
+  (asm_inst (Mem m r a) s = mem_op m r a s) /\
+  (asm_inst (FP f) s = assert F s)`;
 
 val _ = export_rewrites["mem_op_def","asm_inst_def","arith_upd_def"]
 
@@ -217,25 +219,25 @@ val lab_to_loc_def = Define `
 val loc_to_pc_def = Define `
   (loc_to_pc n1 n2 [] = NONE) /\
   (loc_to_pc n1 n2 ((Section k xs)::ys) =
-     if (k = n1) /\ (n2 = 0) then SOME (0:num) else
+     if (k = n1) /\ (n2 = 0n) then SOME (0:num) else
        case xs of
        | [] => loc_to_pc n1 n2 ys
        | (z::zs) =>
-         if (?k. z = Label n1 n2 k) /\ n2 <> 0 then SOME 0 else
+         if (?k. z = Label n1 n2 k) /\ n2 <> 0 then SOME 0n else
            if is_Label z then loc_to_pc n1 n2 ((Section k zs)::ys)
            else
              case loc_to_pc n1 n2 ((Section k zs)::ys) of
              | NONE => NONE
-             | SOME pos => SOME (pos + 1))`;
+             | SOME pos => SOME (pos + 1:num))`;
 
 val asm_inst_consts = Q.store_thm("asm_inst_consts",
   `((asm_inst i s).pc = s.pc) /\
-    ((asm_inst i s).code = s.code) /\
-    ((asm_inst i s).clock = s.clock) /\
-    ((asm_inst i s).ffi = s.ffi) ∧
-    ((asm_inst i s).ptr_reg = s.ptr_reg) ∧
-    ((asm_inst i s).len_reg = s.len_reg) ∧
-    ((asm_inst i s).link_reg = s.link_reg)`,
+   ((asm_inst i s).code = s.code) /\
+   ((asm_inst i s).clock = s.clock) /\
+   ((asm_inst i s).ffi = s.ffi) ∧
+   ((asm_inst i s).ptr_reg = s.ptr_reg) ∧
+   ((asm_inst i s).len_reg = s.len_reg) ∧
+   ((asm_inst i s).link_reg = s.link_reg)`,
   Cases_on `i` \\ fs [asm_inst_def,upd_reg_def,arith_upd_def]
   \\ TRY (Cases_on `a`)
   \\ fs [asm_inst_def,upd_reg_def,arith_upd_def]

compiler/backend/semantics/patSemScript.sml

@@ -1,4 +1,5 @@
 open preamble patLangTheory
+val _ = Parse.hide "exp";
 
 val _ = new_theory"patSem"