Merge remote-tracking branch 'origin/master' into issue797

basis/CharProgScript.sml

@@ -27,16 +27,60 @@ val _ = trans ">=" stringSyntax.char_ge_tm;
 val _ = next_ml_names := ["isSpace"];
 val res = translate stringTheory.isSpace_def;
 
-val sigs = module_signatures [
-  "ord",
-  "chr",
-  "<",
-  ">",
-  "<=",
-  ">=",
-  "isSpace"
-];
-
-val _ = ml_prog_update (close_module (SOME sigs));
+Definition fromByte_def:
+  fromByte (w:word8) = CHR (w2n w)
+End
+
+val _ = next_ml_names := ["fromByte"];
+val res = translate fromByte_def;
+
+Triviality frombyte_side_thm:
+  frombyte_side v = T
+Proof
+  fs [fetch "-" "frombyte_side_def"]
+  \\ qspec_then ‘v’ assume_tac w2n_lt
+  \\ fs [dimword_def]
+QED
+
+val _ = update_precondition frombyte_side_thm;
+
+Definition some_chars_vector_def:
+  some_chars_vector = Vector (GENLIST (λn. SOME (CHR n)) 256)
+End
+
+Definition some_char_def:
+  some_char c = regexp_compiler$sub some_chars_vector (ORD c)
+End
+
+Theorem some_char_thm:
+  some_char c = SOME c
+Proof
+  Cases_on ‘c’
+  \\ rewrite_tac [some_chars_vector_def,some_char_def,regexp_compilerTheory.sub_def]
+  \\ full_simp_tac std_ss [ORD_CHR]
+  \\ full_simp_tac std_ss [GSYM ORD_CHR]
+  \\ full_simp_tac std_ss [EL_GENLIST]
+QED
+
+val _ = ml_prog_update open_local_block;
+
+val res = translate (EVAL “some_chars_vector”);
+
+val _ = ml_prog_update open_local_in_block;
+
+val _ = next_ml_names := ["some"];
+val res = translate some_char_def;
+
+Triviality some_char_side_thm:
+  some_char_side v = T
+Proof
+  fs [fetch "-" "some_char_side_def"] \\ EVAL_TAC \\ fs [ORD_BOUND]
+QED
+
+val _ = update_precondition some_char_side_thm;
+
+val _ = ml_prog_update close_local_blocks;
+
+val _ = ml_prog_update (close_module NONE);
 
 val _ = export_theory()

basis/TextIOProgScript.sml

@@ -251,7 +251,7 @@ in input0 off len 0 end
 val _ = ml_prog_update open_local_in_block;
 
 val _ = (append_prog o process_topdecs)`
-  fun input1 fd = Some (Char.chr(Word8.toInt(read_byte (get_in fd)))) handle EndOfFile => None`
+  fun input1 fd = Char.some(Char.fromByte(read_byte (get_in fd))) handle EndOfFile => None`
 
 val _ = ml_prog_update open_local_block;
 
@@ -498,7 +498,7 @@ val _ = (append_prog o process_topdecs)`
           else
             let val readat = (!rref) in
               rref := (!rref) + 1;
-              Some (Char.chr (Word8.toInt (Word8Array.sub surplus readat)))
+              Char.some (Char.fromByte (Word8Array.sub surplus readat))
             end`;
 
 val _ = ml_prog_update open_local_in_block;

basis/TextIOProofScript.sml

@@ -1848,9 +1848,9 @@ Proof
     \\ xlet_auto_spec(SOME read_byte_STDIO_spec)
     \\ xsimpl \\ simp[bumpFD_0,FD_def] \\ xsimpl
     \\ xlet_auto \\ xsimpl
-    \\ xlet_auto \\ xsimpl
-    \\ xcon \\ xsimpl
-    \\ fs[ORD_BOUND,CHR_ORD,std_preludeTheory.OPTION_TYPE_def] )
+    \\ xapp \\ xsimpl
+    \\ asm_exists_tac \\ fs [CharProgTheory.some_char_thm]
+    \\ fs[ORD_BOUND,CHR_ORD,std_preludeTheory.OPTION_TYPE_def,CharProgTheory.fromByte_def])
   >- xsimpl
   \\ xsimpl
   \\ xcases
@@ -2355,16 +2355,16 @@ Proof
     \\ rveq \\ xlet_auto >- xsimpl
     \\ xlet_auto >- xsimpl
     \\ xlet_auto >- (xsimpl \\ fs[instream_buffered_inv_def])
-    \\ xlet_auto >- xsimpl
-    \\ xlet_auto >- (xsimpl \\ simp[w2n_lt_256])
-    \\ xcon \\ `bactive <> []`
-                by (fs[instream_buffered_inv_def]
-                    \\ fs[DROP_NIL])
+    \\ xlet_auto >- xsimpl \\ fs [CharProgTheory.fromByte_def]
+    \\ xapp
+    \\ `bactive <> []` by (fs[instream_buffered_inv_def] \\ fs[DROP_NIL])
     \\ xsimpl
+    \\ asm_exists_tac \\ fs [CharProgTheory.some_char_thm]
     \\ CASE_TAC
     >-(fs[])
     >-(xsimpl
       \\ fs[instream_buffered_inv_def, std_preludeTheory.OPTION_TYPE_def] \\ xsimpl
+      \\ ntac 2 strip_tac \\ fs []
       \\ reverse conj_tac
       >-(`h::t = (TAKE (w − r) (DROP r bcontent))` by fs[]
         \\ `t = DROP 1 (TAKE (w − r) (DROP r bcontent))`

compiler/backend/flat_to_closScript.sml

@@ -10,11 +10,21 @@ val _ = new_theory"flat_to_clos"
 
 val _ = set_grammar_ancestry ["flatLang","closLang","backend_common"];
 
+val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
+
 Definition dest_pat_def:
   dest_pat [(Pvar v, h)] = SOME (v:string,h) /\
   dest_pat _ = NONE
 End
 
+Theorem dest_pat_pmatch:
+  dest_pat x =
+    case x of [(Pvar v, h)] => SOME (v:string,h) | _ => NONE
+Proof
+  CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV)
+  \\ every_case_tac \\ fs [dest_pat_def]
+QED
+
 Theorem dest_pat_thm:
   dest_pat pes = SOME (p_1,p_2) <=> pes = [(Pvar p_1, p_2)]
 Proof
@@ -35,14 +45,30 @@ End
 
 Definition arg1_def:
   arg1 xs f =
-    case xs of [x] => f x | _ => closLang$Let None xs (Var None 0)
+    dtcase xs of [x] => f x | _ => closLang$Let None xs (Var None 0)
 End
 
+Theorem arg1_pmatch:
+  arg1 xs f =
+    case xs of [x] => f x | _ => closLang$Let None xs (Var None 0)
+Proof
+  CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV)
+  \\ every_case_tac \\ fs [arg1_def]
+QED
+
 Definition arg2_def:
   arg2 xs f =
-    case xs of [x; y] => f x y | _ => closLang$Let None xs (Var None 0)
+    dtcase xs of [x; y] => f x y | _ => closLang$Let None xs (Var None 0)
 End
 
+Theorem arg2_pmatch:
+  arg2 xs f =
+    case xs of [x; y] => f x y | _ => closLang$Let None xs (Var None 0)
+Proof
+  CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV)
+  \\ every_case_tac \\ fs [arg2_def]
+QED
+
 Definition AllocGlobals_def:
   AllocGlobals t n =
     if n = 0 then Op t (Cons 0) [] else
@@ -77,7 +103,7 @@ End
 
 Definition compile_op_def:
   compile_op t op xs =
-    case op of
+    dtcase op of
     | Opapp => arg2 xs (\x f. closLang$App t NONE f [x])
     | TagLenEq tag n => closLang$Op t (TagLenEq tag n) xs
     | LenEq n => closLang$Op t (LenEq n) xs
@@ -88,15 +114,15 @@ Definition compile_op_def:
                         (If t (Op t Less [Var t 0; Op None (Const 255) []])
                           (Raise t (Op t (Cons chr_tag) []))
                           (Var t 0)))
-    | Chopb chop => Op t (case chop of
+    | Chopb chop => Op t (dtcase chop of
                           | Lt => Less
                           | Gt => Greater
                           | Leq => LessEq
                           | Geq => GreaterEq) xs
     | Opassign => arg2 xs (\x y. Op t Update [x; Op None (Const 0) []; y])
     | Opref => Op t Ref xs
     | ConfigGC => Op t ConfigGC xs
-    | Opb l => Op t (case l of
+    | Opb l => Op t (dtcase l of
                      | Lt => Less
                      | Gt => Greater
                      | Leq => LessEq
@@ -175,17 +201,37 @@ Definition join_strings_def:
     else mlstring$concat [x; mlstring$strlit "_"; y]
 End
 
+Definition dest_nop_def:
+  dest_nop op e =
+    dtcase op of
+    | WordFromInt W8 => (dtcase e of [App _ Ord [x]] => SOME x | _ => NONE)
+    | Chr => (dtcase e of [App _ (WordToInt W8) [x]] => SOME x | _ => NONE)
+    | _ => NONE
+End
+
+Theorem dest_nop_thm:
+  dest_nop op es = SOME x ⇔
+    (∃t. op = WordFromInt W8 ∧ es = [App t Ord [x]]) ∨
+    (∃t. op = Chr ∧ es = [App t (WordToInt W8) [x]])
+Proof
+  Cases_on ‘op’ \\ fs [dest_nop_def] \\ every_case_tac \\ fs []
+QED
+
 Definition compile_def:
   (compile m [] = []) /\
   (compile m (x::y::xs) = compile m [x] ++ compile m (y::xs)) /\
   (compile m [flatLang$Raise t e] = [closLang$Raise t (HD (compile m [e]))]) /\
   (compile m [Lit t l] = [compile_lit t l]) /\
   (compile m [Var_local t v] = [Var t (findi (SOME v) m)]) /\
   (compile m [Con t n es] =
-     let tag = (case n of SOME (t,_) => t | _ => 0) in
+     let tag = (dtcase n of SOME (t,_) => t | _ => 0) in
        [Op t (Cons tag) (compile m (REVERSE es))]) /\
-  (compile m [App t op es] = [compile_op t op (compile m (REVERSE es))]) /\
-  (compile m [Fun t v e] = [Fn (mlstring$implode t) NONE NONE 1 (HD (compile (SOME v::m) [e]))]) /\
+  (compile m [App t op es] =
+     dtcase dest_nop op es of
+     | SOME e => compile m [e]
+     | NONE => [compile_op t op (compile m (REVERSE es))]) /\
+  (compile m [Fun t v e] =
+     [Fn (mlstring$implode t) NONE NONE 1 (HD (compile (SOME v::m) [e]))]) /\
   (compile m [If t x1 x2 x3] =
      [If t (HD (compile m [x1]))
            (HD (compile m [x2]))
@@ -194,7 +240,7 @@ Definition compile_def:
      [Let t (compile m [e1]) (HD (compile (vo::m) [e2]))]) /\
   (compile m [Mat t e pes] = [Op t (Const 0) []]) /\
   (compile m [Handle t e pes] =
-     case dest_pat pes of
+     dtcase dest_pat pes of
      | SOME (v,h) => [Handle t (HD (compile m [e])) (HD (compile (SOME v::m) [h]))]
      | _ => compile m [e]) /\
   (compile m [Letrec t funs e] =
@@ -207,6 +253,7 @@ Termination
   \\ `!funs f v x. MEM (f,v,x) funs ==> exp_size x < flatLang$exp1_size funs` by
     (Induct \\ fs [] \\ rw [] \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs [])
   \\ res_tac \\ fs [dest_pat_thm] \\ fs [flatLangTheory.exp_size_def]
+  \\ gvs [dest_nop_thm] \\ fs [flatLangTheory.exp_size_def]
 End
 
 Definition compile_decs_def: