src/Tools/Code/code_runtime.ML
changeset 69593 3dda49e08b9d
parent 67649 1e1782c1aedf
child 69597 ff784d5a5bfb
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -52,15 +52,15 @@
     1.4  
     1.5  val _ = Theory.setup
     1.6    (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
     1.7 -  #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
     1.8 +  #> Code_Target.set_printings (Type_Constructor (\<^type_name>\<open>prop\<close>,
     1.9      [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))]))
    1.10 -  #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
    1.11 +  #> Code_Target.set_printings (Constant (\<^const_name>\<open>Code_Generator.holds\<close>,
    1.12      [(target, SOME (Code_Printer.plain_const_syntax HoldsN))]))
    1.13    #> Code_Target.add_reserved target thisN
    1.14    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
    1.15         (*avoid further pervasive infix names*)
    1.16  
    1.17 -val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    1.18 +val trace = Attrib.setup_config_bool \<^binding>\<open>code_runtime_trace\<close> (K false);
    1.19  
    1.20  fun compile_ML verbose code context =
    1.21   (if Config.get_generic context trace then tracing code else ();
    1.22 @@ -142,16 +142,16 @@
    1.23      val _ = if fastype_of t <> propT
    1.24        then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    1.25        else ();
    1.26 -    val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    1.27 +    val iff = Thm.cterm_of ctxt (Term.Const (\<^const_name>\<open>Pure.eq\<close>, propT --> propT --> propT));
    1.28      val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t [])
    1.29       of SOME Holds => true
    1.30        | _ => false;
    1.31    in
    1.32 -    Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)
    1.33 +    Thm.mk_binop iff ct (if result then \<^cprop>\<open>PROP Code_Generator.holds\<close> else ct)
    1.34    end;
    1.35  
    1.36  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
    1.37 -  (Thm.add_oracle (@{binding holds_by_evaluation},
    1.38 +  (Thm.add_oracle (\<^binding>\<open>holds_by_evaluation\<close>,
    1.39    fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
    1.40  
    1.41  fun check_holds_oracle ctxt evaluator vs_ty_t ct =
    1.42 @@ -369,7 +369,7 @@
    1.43    in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end;
    1.44  
    1.45  val _ = Theory.setup
    1.46 -  (Attrib.setup @{binding code_computation_unfold}
    1.47 +  (Attrib.setup \<^binding>\<open>code_computation_unfold\<close>
    1.48      (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I)))
    1.49      "preprocessing equations for computation");
    1.50  
    1.51 @@ -413,16 +413,16 @@
    1.52  
    1.53  local
    1.54  
    1.55 -fun holds ct = Thm.mk_binop @{cterm "Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop"}
    1.56 -  ct @{cprop "PROP Code_Generator.holds"};
    1.57 +fun holds ct = Thm.mk_binop \<^cterm>\<open>Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop\<close>
    1.58 +  ct \<^cprop>\<open>PROP Code_Generator.holds\<close>;
    1.59  
    1.60  val (_, holds_oracle) = Context.>>> (Context.map_theory_result
    1.61 -  (Thm.add_oracle (@{binding holds}, holds)));
    1.62 +  (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds)));
    1.63  
    1.64  in
    1.65  
    1.66  fun mount_computation_check ctxt cTs raw_computation =
    1.67 -  mount_computation_conv ctxt cTs @{typ prop} raw_computation
    1.68 +  mount_computation_conv ctxt cTs \<^typ>\<open>prop\<close> raw_computation
    1.69      ((K o K) holds_oracle);
    1.70  
    1.71  end;
    1.72 @@ -595,7 +595,7 @@
    1.73        mount_computation_checkN,
    1.74        "(Context.proof_of (Context.the_generic_context ()))",
    1.75        Long_Name.implode [prfx, generated_computationN, covered_constsN],
    1.76 -      Long_Name.append prfx (of_term_for_typ @{typ prop})
    1.77 +      Long_Name.append prfx (of_term_for_typ \<^typ>\<open>prop\<close>)
    1.78      ]) ctxt;
    1.79  
    1.80  
    1.81 @@ -652,7 +652,7 @@
    1.82  fun ml_computation_check_antiq raw_spec ctxt =
    1.83    let
    1.84      val cTs = insert (op =) (dest_Const @{const holds}) (prep_spec ctxt raw_spec);
    1.85 -  in (print_computation_check ctxt, register_computation cTs @{typ prop} ctxt) end;
    1.86 +  in (print_computation_check ctxt, register_computation cTs \<^typ>\<open>prop\<close> ctxt) end;
    1.87  
    1.88  end; (*local*)
    1.89  
    1.90 @@ -755,13 +755,13 @@
    1.91  in
    1.92  
    1.93  val _ = Theory.setup
    1.94 -  (ML_Antiquotation.declaration @{binding code}
    1.95 +  (ML_Antiquotation.declaration \<^binding>\<open>code\<close>
    1.96      Args.term (K ml_code_antiq)
    1.97 -  #> ML_Antiquotation.declaration @{binding computation}
    1.98 +  #> ML_Antiquotation.declaration \<^binding>\<open>computation\<close>
    1.99      (Args.typ -- parse_consts_spec) (K ml_computation_antiq)
   1.100 -  #> ML_Antiquotation.declaration @{binding computation_conv}
   1.101 +  #> ML_Antiquotation.declaration \<^binding>\<open>computation_conv\<close>
   1.102      (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq)
   1.103 -  #> ML_Antiquotation.declaration @{binding computation_check}
   1.104 +  #> ML_Antiquotation.declaration \<^binding>\<open>computation_check\<close>
   1.105      parse_consts_spec (K ml_computation_check_antiq));
   1.106  
   1.107  end;
   1.108 @@ -769,19 +769,19 @@
   1.109  local
   1.110  
   1.111  val parse_datatype =
   1.112 -  Parse.name -- Scan.optional (@{keyword "="} |--
   1.113 +  Parse.name -- Scan.optional (\<^keyword>\<open>=\<close> |--
   1.114      (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
   1.115 -    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
   1.116 +    || ((Parse.term ::: (Scan.repeat (\<^keyword>\<open>|\<close> |-- Parse.term))) >> SOME))) (SOME []);
   1.117  
   1.118  in
   1.119  
   1.120  val _ =
   1.121 -  Outer_Syntax.command @{command_keyword code_reflect}
   1.122 +  Outer_Syntax.command \<^command_keyword>\<open>code_reflect\<close>
   1.123      "enrich runtime environment with generated code"
   1.124 -    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
   1.125 -      ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
   1.126 -    -- Scan.optional (@{keyword "functions"} |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
   1.127 -    -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)
   1.128 +    (Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
   1.129 +      ::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
   1.130 +    -- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
   1.131 +    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.name)
   1.132      >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
   1.133        (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
   1.134