Make translator aware of substring primitive

CakeML · Oct 18, 2017 · fdcbb7d · fdcbb7d
1 parent 657a661
commit fdcbb7d
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 0 deletions.
diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
@@ -2322,6 +2322,12 @@ fun mutual_to_single_line_def def = let
   val (def,ind) = single_line_def def
   in ([def],ind) end
 
+val builtin_terops =
+  [Eval_substring]
+  |> map SPEC_ALL
+  |> map (fn th =>
+      (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator |> rator, th))
+
 val builtin_binops =
   [Eval_NUM_ADD,
    Eval_NUM_SUB,
@@ -2372,6 +2378,7 @@ val builtin_monops =
 
 val AUTO_ETA_EXPAND_CONV = let (* K ($=) --> K (\x y. x = y) *)
   val must_eta_expand_ops =
+    map fst builtin_terops @
     map fst builtin_binops @
     map fst builtin_monops
   fun must_eta_expand tm =
@@ -2443,6 +2450,15 @@ fun preprocess_def def = let
 
 (* definition of the main work horse: hol2deep: term -> thm *)
 
+fun dest_builtin_terop tm = let
+  val (pxx,r3) = dest_comb tm
+  val (px,r2) = dest_comb pxx
+  val (p,r1) = dest_comb px
+  val (x,th) = first (fn (x,_) => can (match_term x) p) builtin_terops
+  val (ss,ii) = match_term x p
+  val th = INST ss (INST_TYPE ii th)
+  in (p,r1,r2,r3,th) end handle HOL_ERR _ => failwith("Not a builtin operator")
+
 fun dest_builtin_binop tm = let
   val (px,r2) = dest_comb tm
   val (p,r1) = dest_comb px
@@ -2794,6 +2810,14 @@ fun hol2deep tm =
     val (ss,ii) = match_term pat inv
     val result = INST ss (INST_TYPE ii th)
     in check_inv "lookup_eval_thm" tm result end else
+  (* built-in ternary operations *)
+  if can dest_builtin_terop tm then let
+    val (p,x1,x2,x3,lemma) = dest_builtin_terop tm
+    val th1 = hol2deep x1
+    val th2 = hol2deep x2
+    val th3 = hol2deep x3
+    val result = MATCH_MP (MATCH_MP (MATCH_MP lemma th1) (UNDISCH_ALL th2)) (UNDISCH_ALL th3) |> UNDISCH_ALL
+    in check_inv "terop" tm result end else
   (* built-in binary operations *)
   if can dest_builtin_binop tm then let
     val (p,x1,x2,lemma) = dest_builtin_binop tm

diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml
@@ -1392,6 +1392,32 @@ val Eval_concat = Q.store_thm("Eval_concat",
   \\ rw[vs_to_string_def]
   \\ fs[concat_def,STRING_TYPE_def]);
 
+val Eval_substring = Q.store_thm("Eval_substring",
+  `∀env x1 x2 x3 len off st.
+    Eval env x1 (STRING_TYPE st) ==>
+    Eval env x2 (NUM off) ==>
+    Eval env x3 (NUM len) ==>
+      off + len <= strlen st ==>
+    Eval env (App CopyStrStr [x1; x2; x3]) (STRING_TYPE (substring st off len))`,
+  rw[Eval_def]
+  \\ rw[Once evaluate_cases,PULL_EXISTS,empty_state_with_refs_eq]
+  \\ rw[Once evaluate_cases,PULL_EXISTS,empty_state_with_refs_eq]
+  \\ first_x_assum(qspec_then`refs`strip_assume_tac)
+  \\ asm_exists_tac \\ rw[]
+  \\ rw[Once evaluate_cases,PULL_EXISTS,empty_state_with_refs_eq]
+  \\ first_x_assum(qspec_then`refs++refs'`strip_assume_tac)
+  \\ asm_exists_tac \\ rw[]
+  \\ rw[Once evaluate_cases,PULL_EXISTS,empty_state_with_refs_eq]
+  \\ first_x_assum(qspec_then`refs++refs'++refs''`strip_assume_tac)
+  \\ asm_exists_tac \\ rw[]
+  \\ rw[Once evaluate_cases,PULL_EXISTS,empty_state_with_refs_eq]
+  \\ rw[state_component_equality]
+  \\ rw[do_app_def]
+  \\ Cases_on`st` \\ fs[STRING_TYPE_def]
+  \\ fs[NUM_def,INT_def,IMPLODE_EXPLODE_I]
+  \\ rw[copy_array_def,INT_ABS_NUM,INT_ADD,
+        substring_def,SEG_TAKE_BUTFISTN,STRING_TYPE_def]);
+
 (* vectors *)
 
 val VECTOR_TYPE_def = Define `