Convert process_topdecs patterns to Quote syntax

candle/overloading/ml_checker/ml_cyclicityCheckerProgScript.sml

@@ -69,24 +69,24 @@ val _ = Q.prove(
 
 val _ = translate parse_strlit_def
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_string cs =
     case parse_strlit cs of
       None => None
     | Some (str, cs) => Some (String.implode str, cs)
-  ’
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_skip_space l =
     case l of
       [] => []
     | (x::cs) =>
       if Char.isSpace x then
         parse_skip_space cs
       else (x::cs);
-  ’
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_token token cs =
     case cs of
       (c::cs) =>
@@ -97,9 +97,9 @@ val _ = (append_prog o process_topdecs) ‘
         else
           None
     | [] => None
-  ’
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_list_innards is_ordered parse_elem cs one_more_elem acc =
     case cs of
       c::cs =>
@@ -133,9 +133,10 @@ val _ = (append_prog o process_topdecs) ‘
         if one_more_elem then None
         else if is_ordered then
           Some(List.rev acc, [])
-        else Some (acc, [])’
+        else Some (acc, [])
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_list is_ordered parse_elem cs =
     case cs of
       c::cs =>
@@ -144,9 +145,10 @@ val _ = (append_prog o process_topdecs) ‘
         else if c = #"[" then
           parse_list_innards is_ordered parse_elem cs False []
         else None
-    | [] => None’
+    | [] => None
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_type cs =
     case cs of
     (#"T" :: #"y" :: #"v" :: #"a" :: #"r" :: #" " :: cs) =>
@@ -160,9 +162,10 @@ val _ = (append_prog o process_topdecs) ‘
            (case parse_list True parse_type cs of
               None => None
             | Some (tylist, cs) => Some (Kernel.Tyapp name tylist, cs)))
-  | _ => None’
+  | _ => None
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_pair parse_fst parse_snd cs =
     case parse_token #"(" cs of
       None => None
@@ -178,9 +181,10 @@ val _ = (append_prog o process_topdecs) ‘
           | Some (second, cs) =>
             (case parse_token #")" cs of
               None => None
-            | Some cs => Some ((first, second), cs)))))’
+            | Some cs => Some ((first, second), cs)))))
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun parse_sum parse_inl parse_inr cs =
     let val cs = parse_skip_space cs in
     case parse_inr cs of
@@ -189,21 +193,25 @@ val _ = (append_prog o process_topdecs) ‘
           None => None
         | Some (inl, cs) => Some (Inl inl, cs))
     | Some (inr, cs) => Some (Inr inr, cs)
-    end’
+    end
+End
 
-val _ = (append_prog o process_topdecs)
-  ‘fun parse_sum_hol_type x = parse_sum parse_type (parse_pair parse_string parse_type) x’
+Quote add_cakeml:
+  fun parse_sum_hol_type x = parse_sum parse_type (parse_pair parse_string parse_type) x
+End
 
-val _ = (append_prog o process_topdecs)
-  ‘fun hol_type_sum_pairs x = parse_pair parse_sum_hol_type parse_sum_hol_type x’
+Quote add_cakeml:
+  fun hol_type_sum_pairs x = parse_pair parse_sum_hol_type parse_sum_hol_type x
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun intersperse_commas l =
       case l of [] => []
              | [e] => [e]
-             | e::l => e:: "," :: intersperse_commas l’
+             | e::l => e:: "," :: intersperse_commas l
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun present_type ty =
       case ty of (Kernel.Tyvar s) => "'" ^ s
               | (Kernel.Tyapp s []) => s
@@ -213,15 +221,17 @@ val _ = (append_prog o process_topdecs) ‘
                     val ps = String.concat(intersperse_commas(List.map present_type l))
                   in
                     "(" ^ ps ^ ") " ^ s
-                  end’
+                  end
+End
 
-val _ = (append_prog o process_topdecs) ‘
+Quote add_cakeml:
   fun present_tot ty =
     case ty of (Inl ty) => present_type ty
-            | (Inr(Kernel.Const name ty)) => name ^ " : " ^ present_type ty’
+            | (Inr(Kernel.Const name ty)) => name ^ " : " ^ present_type ty
+End
 
-val _ = (append_prog o process_topdecs)
-  ‘fun main u =
+Quote add_cakeml:
+  fun main u =
      let val cs = String.explode(TextIO.inputAll (TextIO.openStdIn ()));
      in
         (case parse_list False hol_type_sum_pairs cs of
@@ -263,7 +273,7 @@ val _ = (append_prog o process_topdecs)
             handle Kernel.Fail s => print s
                  | _ => print "Unhandled exception raised!\n"
      end
-  ’
+End
 
 val prog =
   “SNOC (Dlet unknown_loc (Pcon NONE []) (App Opapp [Var (Short "main"); Con NONE []]))

candle/overloading/ml_kernel/candle_kernelProgScript.sml

@@ -22,7 +22,7 @@ val _ = translate thm_to_string_def;
 
 val _ = ml_prog_update open_local_in_block;
 
-val _ = (append_prog o process_topdecs) `
+Quote add_cakeml:
   val print_thm = fn th => case th of Sequent tms c =>
     let
       val ctxt = !the_context
@@ -31,7 +31,7 @@ val _ = (append_prog o process_topdecs) `
     in
       #(kernel_ffi) str arr
     end;
-`
+End
 
 val _ = ml_prog_update close_local_blocks;
 val _ = ml_prog_update (close_module NONE);

candle/prover/candle_kernelProgScript.sml

@@ -24,7 +24,7 @@ val r = translate thm_to_string_def;
 
 val _ = ml_prog_update open_local_in_block;
 
-val _ = (append_prog o process_topdecs) `
+Quote add_cakeml:
   val print_thm = fn th => case th of Sequent tms c =>
     let
       val ctxt = !the_context
@@ -33,7 +33,7 @@ val _ = (append_prog o process_topdecs) `
     in
       #(kernel_ffi) str arr
     end;
-`
+End
 (* compute primitive *)
 
 val _ = ml_prog_update open_local_block;

characteristic/cfDivScript.sml

@@ -103,7 +103,7 @@ QED
 
 (* -- tailrec -- *)
 
-val tailrec_clos = cfTacticsLib.process_topdecs `
+val tailrec_clos = process_topdecs `
   fun tailrec f x =
     case f x of
       Inl x => tailrec f x
@@ -2250,7 +2250,7 @@ QED
 
 (* -- repeat -- *)
 
-val repeat_clos = cfTacticsLib.process_topdecs `
+val repeat_clos = process_topdecs `
   fun repeat f x = repeat f (f x);
   ` |> rator |> rand |> rand
 
@@ -3983,7 +3983,7 @@ QED
 
 (* -- old repeat approach -- *)
 
-val _ = (append_prog o cfTacticsLib.process_topdecs)
+val _ = (append_prog o process_topdecs)
   `fun repeat f x = repeat f (f x);`
 
 val st = ml_translatorLib.get_ml_prog_state ();

characteristic/examples/cf_examplesScript.sml

@@ -373,9 +373,9 @@ QED
 (* Quote add_cakeml: *)
 (*   fun strcat_foo r = r := !r ^ "foo" *)
 (* End *)
-(* TODO Try new syntax using Quote once #1313 on HOL has been resolved *)
-val strcat_foo = (append_prog o process_topdecs)
-  `fun strcat_foo r = r := !r ^ "foo"`
+Quote add_cakeml:
+  fun strcat_foo r = r := !r ^ "foo"
+End
 
 val xlet_auto = cfLetAutoLib.xlet_auto
 

characteristic/examples/cf_tutorialScript.sml

@@ -21,8 +21,8 @@ Libs
 val _ = translation_extends "basisProg"
 
 (* We use basisFunctionsLib for managing the state resulting from
-   the evaluation of several toplevel declarations, and the append_prog
-   function to add program definitions to the stored state
+   the evaluation of several toplevel declarations, and use the
+   Quote add_cakeml functionality to add program definitions to the stored state
 *)
 (* Then, write the code for the programs we want to specify.
 

compiler/backend/word_instScript.sml

@@ -290,7 +290,7 @@ Termination
    \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
    \\ fs[exp_size_def]
    \\ TRY (DECIDE_TAC)
-End ;
+End
 
 Theorem inst_select_exp_pmatch:
   !c tar temp exp.

compiler/bootstrap/translation/compiler32ProgScript.sml

@@ -375,7 +375,7 @@ val res = translate compile_pancake_32_def;
 
 val res = translate (has_pancake_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
 
-val main = process_topdecs`
+Quote add_cakeml:
   fun main u =
     let
       val cl = CommandLine.arguments ()
@@ -392,9 +392,8 @@ val main = process_topdecs`
         case compiler_compile_32 cl (TextIO.inputAll (TextIO.openStdIn ()))  of
           (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
                      compiler32prog_nonzero_exit_code_for_error_msg e)
-    end`;
-
-val res = append_prog main;
+    end
+End
 
 val main_v_def = fetch "-" "main_v_def";