tuned structure and terminology
authorhaftmann
Thu Jan 26 16:06:19 2017 +0100 (2017-01-26)
changeset 649573faa9b31ff78
parent 64956 de7ce0fad5bc
child 64958 85b87da722ab
tuned structure and terminology
src/HOL/Library/code_test.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Thu Jan 26 16:06:18 2017 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Thu Jan 26 16:06:19 2017 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4      fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
     1.5      fun evaluator program _ vs_ty deps =
     1.6        Exn.interruptible_capture evaluate
     1.7 -        (Code_Target.computation_text ctxt target program deps true vs_ty)
     1.8 +        (Code_Target.compilation_text ctxt target program deps true vs_ty)
     1.9      fun postproc f = map (apsnd (Option.map (map f)))
    1.10    in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
    1.11  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 26 16:06:18 2017 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 26 16:06:19 2017 +0100
     2.3 @@ -311,7 +311,7 @@
     2.4    let
     2.5      fun evaluator program _ vs_ty_t deps =
     2.6        Exn.interruptible_capture (value opts ctxt cookie)
     2.7 -        (Code_Target.computation_text ctxt target program deps true vs_ty_t)
     2.8 +        (Code_Target.compilation_text ctxt target program deps true vs_ty_t)
     2.9    in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
    2.10  
    2.11  
     3.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
     3.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:19 2017 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4  
     3.5  open Basic_Code_Symbol;
     3.6  
     3.7 -(** computation **)
     3.8 +(** ML compiler as evaluation environment **)
     3.9  
    3.10  (* technical prerequisites *)
    3.11  
    3.12 @@ -82,24 +82,24 @@
    3.13        prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
    3.14        put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    3.15      val ctxt' = ctxt
    3.16 -      |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    3.17 +      |> put (fn () => error ("Bad compilation for " ^ quote put_ml))
    3.18        |> Context.proof_map (compile_ML false code);
    3.19      val computator = get ctxt';
    3.20    in Code_Preproc.timed_exec "running ML" computator ctxt' end;
    3.21  
    3.22  
    3.23 -(* computation as evaluation into ML language values *)
    3.24 +(* evaluation into ML language values *)
    3.25  
    3.26  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    3.27  
    3.28  fun reject_vars ctxt t =
    3.29    ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
    3.30  
    3.31 -fun build_computation_text ctxt some_target program consts =
    3.32 -  Code_Target.computation_text ctxt (the_default target some_target) program consts false
    3.33 +fun build_compilation_text ctxt some_target program consts =
    3.34 +  Code_Target.compilation_text ctxt (the_default target some_target) program consts false
    3.35    #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    3.36  
    3.37 -fun run_computation_text cookie ctxt comp vs_t args =
    3.38 +fun run_compilation_text cookie ctxt comp vs_t args =
    3.39    let
    3.40      val (program_code, value_name) = comp vs_t;
    3.41      val value_code = space_implode " "
    3.42 @@ -118,7 +118,7 @@
    3.43        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
    3.44        else ()
    3.45      fun comp program _ vs_ty_t deps =
    3.46 -      run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args;
    3.47 +      run_compilation_text cookie ctxt (build_compilation_text ctxt some_target program deps) vs_ty_t args;
    3.48    in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
    3.49  
    3.50  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    3.51 @@ -129,15 +129,15 @@
    3.52  
    3.53  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    3.54    let
    3.55 -    fun computation' { program, deps } =
    3.56 +    fun compilation' { program, deps } =
    3.57        let
    3.58 -        val computation'' = run_computation_text cookie ctxt
    3.59 -          (build_computation_text ctxt target program (map Constant deps));
    3.60 -      in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end;
    3.61 -    val computation = Code_Thingol.static_value { ctxt = ctxt,
    3.62 +        val compilation'' = run_compilation_text cookie ctxt
    3.63 +          (build_compilation_text ctxt target program (map Constant deps));
    3.64 +      in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end;
    3.65 +    val compilation = Code_Thingol.static_value { ctxt = ctxt,
    3.66        lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    3.67 -      computation';
    3.68 -  in fn ctxt' => computation ctxt' o reject_vars ctxt' end;
    3.69 +      compilation';
    3.70 +  in fn ctxt' => compilation ctxt' o reject_vars ctxt' end;
    3.71  
    3.72  fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x;
    3.73  
    3.74 @@ -166,7 +166,7 @@
    3.75        then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    3.76        else ();
    3.77      val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    3.78 -    val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t [])
    3.79 +    val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t [])
    3.80       of SOME Holds => true
    3.81        | _ => false;
    3.82    in
    3.83 @@ -184,19 +184,24 @@
    3.84  
    3.85  fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
    3.86    (fn program => fn vs_t => fn deps =>
    3.87 -    check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t)
    3.88 +    check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
    3.89        o reject_vars ctxt;
    3.90  
    3.91  fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
    3.92    Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
    3.93 -    K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    3.94 +    K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    3.95  
    3.96  end; (*local*)
    3.97  
    3.98  
    3.99 -(** computations -- experimental! **)
   3.100 +(** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **)
   3.101 +
   3.102 +(* auxiliary *)
   3.103  
   3.104 -fun monomorphic T = fold_atyps ((K o K) false) T true;
   3.105 +val generated_computationN = "Generated_Computation";
   3.106 +
   3.107 +
   3.108 +(* possible type signatures of constants *)
   3.109  
   3.110  fun typ_signatures_for T =
   3.111    let
   3.112 @@ -214,6 +219,64 @@
   3.113      |> Typtab.lookup_list
   3.114    end;
   3.115  
   3.116 +
   3.117 +(* name mangling *)
   3.118 +
   3.119 +local
   3.120 +
   3.121 +fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   3.122 +  | tycos_of _ = [];
   3.123 +
   3.124 +val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
   3.125 +
   3.126 +in
   3.127 +
   3.128 +fun of_term_for_typ Ts =
   3.129 +  let
   3.130 +    val names = Ts
   3.131 +      |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
   3.132 +      |> Name.variant_list [];
   3.133 +  in the o AList.lookup (op =) (Ts ~~ names) end;
   3.134 +
   3.135 +fun eval_for_const ctxt cTs =
   3.136 +  let
   3.137 +    fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
   3.138 +    val names = cTs
   3.139 +      |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
   3.140 +      |> Name.variant_list [];
   3.141 +  in the o AList.lookup (op =) (cTs ~~ names) end;
   3.142 +
   3.143 +end;
   3.144 +
   3.145 +
   3.146 +(* checks for input terms *)
   3.147 +
   3.148 +fun monomorphic T = fold_atyps ((K o K) false) T true;
   3.149 +
   3.150 +fun check_typ ctxt T t =
   3.151 +  Syntax.check_term ctxt (Type.constraint T t);
   3.152 +
   3.153 +fun check_computation_input ctxt cTs t =
   3.154 +  let
   3.155 +    fun check t = check_comb (strip_comb t)
   3.156 +    and check_comb (t as Abs _, _) =
   3.157 +          error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
   3.158 +      | check_comb (t as Const (cT as (c, T)), ts) =
   3.159 +          let
   3.160 +            val _ = if not (member (op =) cTs cT)
   3.161 +              then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
   3.162 +              else ();
   3.163 +            val _ = if not (monomorphic T)
   3.164 +              then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
   3.165 +              else ();
   3.166 +            val _ = map check ts;
   3.167 +          in () end;
   3.168 +    val _ = check t;
   3.169 +  in t end;
   3.170 +
   3.171 +
   3.172 +(* code generation for of the universal morphism *)
   3.173 +
   3.174  fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
   3.175    let
   3.176      val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
   3.177 @@ -242,34 +305,6 @@
   3.178      |> prefix "fun "
   3.179    end;
   3.180  
   3.181 -local
   3.182 -
   3.183 -fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   3.184 -  | tycos_of _ = [];
   3.185 -
   3.186 -val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
   3.187 -
   3.188 -in
   3.189 -
   3.190 -fun of_term_for_typ Ts =
   3.191 -  let
   3.192 -    val names = Ts
   3.193 -      |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
   3.194 -      |> Name.variant_list [];
   3.195 -  in the o AList.lookup (op =) (Ts ~~ names) end;
   3.196 -
   3.197 -fun eval_for_const ctxt cTs =
   3.198 -  let
   3.199 -    fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
   3.200 -    val names = cTs
   3.201 -      |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
   3.202 -      |> Name.variant_list [];
   3.203 -  in the o AList.lookup (op =) (cTs ~~ names) end;
   3.204 -
   3.205 -end;
   3.206 -
   3.207 -val generated_computationN = "Generated_Computation";
   3.208 -
   3.209  fun print_computation_code ctxt compiled_value requested_Ts cTs =
   3.210    let
   3.211      val proper_cTs = map_filter I cTs;
   3.212 @@ -307,26 +342,13 @@
   3.213      ], map (prefix (generated_computationN ^ ".") o of_term_for_typ') requested_Ts)
   3.214    end;
   3.215  
   3.216 -fun check_typ ctxt T t =
   3.217 -  Syntax.check_term ctxt (Type.constraint T t);
   3.218 -
   3.219 -fun check_computation_input ctxt cTs t =
   3.220 -  let
   3.221 -    fun check t = check_comb (strip_comb t)
   3.222 -    and check_comb (t as Abs _, _) =
   3.223 -          error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
   3.224 -      | check_comb (t as Const (cT as (c, T)), ts) =
   3.225 -          let
   3.226 -            val _ = if not (member (op =) cTs cT)
   3.227 -              then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
   3.228 -              else ();
   3.229 -            val _ = if not (monomorphic T)
   3.230 -              then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
   3.231 -              else ();
   3.232 -            val _ = map check ts;
   3.233 -          in () end;
   3.234 -    val _ = check t;
   3.235 -  in t end;
   3.236 +fun mount_computation ctxt cTs T raw_computation lift_postproc =
   3.237 +  Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
   3.238 +    (fn _ => fn ctxt' =>
   3.239 +      check_typ ctxt' T
   3.240 +      #> reject_vars ctxt'
   3.241 +      #> check_computation_input ctxt' cTs
   3.242 +      #> raw_computation);
   3.243  
   3.244  fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
   3.245    let
   3.246 @@ -340,20 +362,15 @@
   3.247      fun comp' vs_ty_evals =
   3.248        let
   3.249          val (generated_code, compiled_value) =
   3.250 -          build_computation_text ctxt NONE program deps vs_ty_evals;
   3.251 +          build_compilation_text ctxt NONE program deps vs_ty_evals;
   3.252          val (of_term_code, [of_term]) = print_computation_code ctxt compiled_value [T] cTs;
   3.253        in
   3.254          (generated_code ^ "\n" ^ of_term_code,
   3.255            enclose "(" ")" ("fn () => " ^ of_term))
   3.256        end;
   3.257      val compiled_computation =
   3.258 -      Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []);
   3.259 -  in fn ctxt' =>
   3.260 -    check_typ ctxt' T
   3.261 -    #> reject_vars ctxt'
   3.262 -    #> check_computation_input ctxt (map_filter I cTs)
   3.263 -    #> compiled_computation
   3.264 -  end;
   3.265 +      Exn.release (run_compilation_text cookie ctxt comp' vs_ty_evals []);
   3.266 +  in (map_filter I cTs, compiled_computation) end;
   3.267  
   3.268  fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
   3.269    let
   3.270 @@ -365,17 +382,16 @@
   3.271          if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t)
   3.272          else insert (op =) cT | _ => I) ts [];
   3.273      val evals = Abs ("eval", map snd cTs ---> TFree (Name.aT, []), list_comb (Bound 0, map Const cTs));
   3.274 -    val computation = Code_Thingol.dynamic_value ctxt
   3.275 +    val (cTs, raw_computation) = Code_Thingol.dynamic_value ctxt
   3.276        (K I) (compile_computation cookie ctxt T) evals;
   3.277    in
   3.278 -    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
   3.279 -      (K computation)
   3.280 +    mount_computation ctxt cTs T raw_computation lift_postproc
   3.281    end;
   3.282  
   3.283  
   3.284  (** code antiquotation **)
   3.285  
   3.286 -fun evaluation_code ctxt module_name program tycos consts =
   3.287 +fun runtime_code ctxt module_name program tycos consts =
   3.288    let
   3.289      val thy = Proof_Context.theory_of ctxt;
   3.290      val (ml_modules, target_names) =
   3.291 @@ -422,7 +438,7 @@
   3.292    let
   3.293      val program = Code_Thingol.consts_program ctxt consts;
   3.294      val (code, (_, consts_map)) =
   3.295 -      evaluation_code ctxt Code_Target.generatedN program [] consts
   3.296 +      runtime_code ctxt Code_Target.generatedN program [] consts
   3.297    in { code = code, consts_map = consts_map } end);
   3.298  
   3.299  fun register_const const ctxt =
   3.300 @@ -532,7 +548,7 @@
   3.301      val functions = map (prep_const thy) raw_functions;
   3.302      val consts = constrs @ functions;
   3.303      val program = Code_Thingol.consts_program ctxt consts;
   3.304 -    val result = evaluation_code ctxt module_name program tycos consts
   3.305 +    val result = runtime_code ctxt module_name program tycos consts
   3.306        |> (apsnd o apsnd) (chop (length constrs));
   3.307    in
   3.308      thy
     4.1 --- a/src/Tools/Code/code_target.ML	Thu Jan 26 16:06:18 2017 +0100
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu Jan 26 16:06:19 2017 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4      -> ((string * bool) * Token.T list) list -> unit
     4.5  
     4.6    val generatedN: string
     4.7 -  val computation_text: Proof.context -> string -> Code_Thingol.program
     4.8 +  val compilation_text: Proof.context -> string -> Code_Thingol.program
     4.9      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    4.10      -> (string * string) list * string
    4.11  
    4.12 @@ -399,7 +399,7 @@
    4.13      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
    4.14    end;
    4.15  
    4.16 -fun dynamic_computation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    4.17 +fun dynamic_compilation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    4.18    let
    4.19      val _ = if Code_Thingol.contains_dict_var t then
    4.20        error "Term to be evaluated contains free dictionaries" else ();
    4.21 @@ -416,13 +416,13 @@
    4.22      val value_name = the (deresolve Code_Symbol.value);
    4.23    in (program_code, value_name) end;
    4.24  
    4.25 -fun computation_text ctxt target_name program syms =
    4.26 +fun compilation_text ctxt target_name program syms =
    4.27    let
    4.28      val (mounted_serializer, (_, prepared_program)) =
    4.29        mount_serializer ctxt target_name NONE generatedN [] program syms;
    4.30    in
    4.31      Code_Preproc.timed_exec "serializing"
    4.32 -    (fn () => dynamic_computation_text mounted_serializer prepared_program syms) ctxt
    4.33 +    (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
    4.34    end;
    4.35  
    4.36  end; (* local *)
     5.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jan 26 16:06:18 2017 +0100
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jan 26 16:06:19 2017 +0100
     5.3 @@ -872,14 +872,14 @@
     5.4      #> term_value
     5.5    end;
     5.6  
     5.7 -fun dynamic_evaluation eval ctxt algebra eqngr t =
     5.8 +fun dynamic_evaluation comp ctxt algebra eqngr t =
     5.9    let
    5.10      val ((program, (vs_ty_t', deps)), _) =
    5.11        Code_Preproc.timed "translating term" #ctxt
    5.12        (fn { ctxt, algebra, eqngr, t } =>
    5.13          invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t)
    5.14          { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t };
    5.15 -  in eval program t vs_ty_t' deps end;
    5.16 +  in comp program t vs_ty_t' deps end;
    5.17  
    5.18  fun dynamic_conv ctxt conv =
    5.19    Code_Preproc.dynamic_conv ctxt