src/Tools/Code/code_runtime.ML
changeset 64957 3faa9b31ff78
parent 64956 de7ce0fad5bc
child 64958 85b87da722ab
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:19 2017 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  open Basic_Code_Symbol;
     1.6  
     1.7 -(** computation **)
     1.8 +(** ML compiler as evaluation environment **)
     1.9  
    1.10  (* technical prerequisites *)
    1.11  
    1.12 @@ -82,24 +82,24 @@
    1.13        prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
    1.14        put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
    1.15      val ctxt' = ctxt
    1.16 -      |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    1.17 +      |> put (fn () => error ("Bad compilation for " ^ quote put_ml))
    1.18        |> Context.proof_map (compile_ML false code);
    1.19      val computator = get ctxt';
    1.20    in Code_Preproc.timed_exec "running ML" computator ctxt' end;
    1.21  
    1.22  
    1.23 -(* computation as evaluation into ML language values *)
    1.24 +(* evaluation into ML language values *)
    1.25  
    1.26  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
    1.27  
    1.28  fun reject_vars ctxt t =
    1.29    ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
    1.30  
    1.31 -fun build_computation_text ctxt some_target program consts =
    1.32 -  Code_Target.computation_text ctxt (the_default target some_target) program consts false
    1.33 +fun build_compilation_text ctxt some_target program consts =
    1.34 +  Code_Target.compilation_text ctxt (the_default target some_target) program consts false
    1.35    #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    1.36  
    1.37 -fun run_computation_text cookie ctxt comp vs_t args =
    1.38 +fun run_compilation_text cookie ctxt comp vs_t args =
    1.39    let
    1.40      val (program_code, value_name) = comp vs_t;
    1.41      val value_code = space_implode " "
    1.42 @@ -118,7 +118,7 @@
    1.43        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
    1.44        else ()
    1.45      fun comp program _ vs_ty_t deps =
    1.46 -      run_computation_text cookie ctxt (build_computation_text ctxt some_target program deps) vs_ty_t args;
    1.47 +      run_compilation_text cookie ctxt (build_compilation_text ctxt some_target program deps) vs_ty_t args;
    1.48    in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
    1.49  
    1.50  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    1.51 @@ -129,15 +129,15 @@
    1.52  
    1.53  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    1.54    let
    1.55 -    fun computation' { program, deps } =
    1.56 +    fun compilation' { program, deps } =
    1.57        let
    1.58 -        val computation'' = run_computation_text cookie ctxt
    1.59 -          (build_computation_text ctxt target program (map Constant deps));
    1.60 -      in fn _ => fn _ => fn vs_ty_t => fn _ => computation'' vs_ty_t [] end;
    1.61 -    val computation = Code_Thingol.static_value { ctxt = ctxt,
    1.62 +        val compilation'' = run_compilation_text cookie ctxt
    1.63 +          (build_compilation_text ctxt target program (map Constant deps));
    1.64 +      in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end;
    1.65 +    val compilation = Code_Thingol.static_value { ctxt = ctxt,
    1.66        lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    1.67 -      computation';
    1.68 -  in fn ctxt' => computation ctxt' o reject_vars ctxt' end;
    1.69 +      compilation';
    1.70 +  in fn ctxt' => compilation ctxt' o reject_vars ctxt' end;
    1.71  
    1.72  fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x;
    1.73  
    1.74 @@ -166,7 +166,7 @@
    1.75        then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    1.76        else ();
    1.77      val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    1.78 -    val result = case partiality_as_none (run_computation_text truth_cookie ctxt evaluator vs_t [])
    1.79 +    val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t [])
    1.80       of SOME Holds => true
    1.81        | _ => false;
    1.82    in
    1.83 @@ -184,19 +184,24 @@
    1.84  
    1.85  fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
    1.86    (fn program => fn vs_t => fn deps =>
    1.87 -    check_holds_oracle ctxt (build_computation_text ctxt NONE program deps) vs_t)
    1.88 +    check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
    1.89        o reject_vars ctxt;
    1.90  
    1.91  fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
    1.92    Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
    1.93 -    K (check_holds_oracle ctxt' (build_computation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    1.94 +    K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    1.95  
    1.96  end; (*local*)
    1.97  
    1.98  
    1.99 -(** computations -- experimental! **)
   1.100 +(** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **)
   1.101 +
   1.102 +(* auxiliary *)
   1.103  
   1.104 -fun monomorphic T = fold_atyps ((K o K) false) T true;
   1.105 +val generated_computationN = "Generated_Computation";
   1.106 +
   1.107 +
   1.108 +(* possible type signatures of constants *)
   1.109  
   1.110  fun typ_signatures_for T =
   1.111    let
   1.112 @@ -214,6 +219,64 @@
   1.113      |> Typtab.lookup_list
   1.114    end;
   1.115  
   1.116 +
   1.117 +(* name mangling *)
   1.118 +
   1.119 +local
   1.120 +
   1.121 +fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   1.122 +  | tycos_of _ = [];
   1.123 +
   1.124 +val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
   1.125 +
   1.126 +in
   1.127 +
   1.128 +fun of_term_for_typ Ts =
   1.129 +  let
   1.130 +    val names = Ts
   1.131 +      |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
   1.132 +      |> Name.variant_list [];
   1.133 +  in the o AList.lookup (op =) (Ts ~~ names) end;
   1.134 +
   1.135 +fun eval_for_const ctxt cTs =
   1.136 +  let
   1.137 +    fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
   1.138 +    val names = cTs
   1.139 +      |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
   1.140 +      |> Name.variant_list [];
   1.141 +  in the o AList.lookup (op =) (cTs ~~ names) end;
   1.142 +
   1.143 +end;
   1.144 +
   1.145 +
   1.146 +(* checks for input terms *)
   1.147 +
   1.148 +fun monomorphic T = fold_atyps ((K o K) false) T true;
   1.149 +
   1.150 +fun check_typ ctxt T t =
   1.151 +  Syntax.check_term ctxt (Type.constraint T t);
   1.152 +
   1.153 +fun check_computation_input ctxt cTs t =
   1.154 +  let
   1.155 +    fun check t = check_comb (strip_comb t)
   1.156 +    and check_comb (t as Abs _, _) =
   1.157 +          error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
   1.158 +      | check_comb (t as Const (cT as (c, T)), ts) =
   1.159 +          let
   1.160 +            val _ = if not (member (op =) cTs cT)
   1.161 +              then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
   1.162 +              else ();
   1.163 +            val _ = if not (monomorphic T)
   1.164 +              then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
   1.165 +              else ();
   1.166 +            val _ = map check ts;
   1.167 +          in () end;
   1.168 +    val _ = check t;
   1.169 +  in t end;
   1.170 +
   1.171 +
   1.172 +(* code generation for of the universal morphism *)
   1.173 +
   1.174  fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
   1.175    let
   1.176      val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
   1.177 @@ -242,34 +305,6 @@
   1.178      |> prefix "fun "
   1.179    end;
   1.180  
   1.181 -local
   1.182 -
   1.183 -fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   1.184 -  | tycos_of _ = [];
   1.185 -
   1.186 -val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
   1.187 -
   1.188 -in
   1.189 -
   1.190 -fun of_term_for_typ Ts =
   1.191 -  let
   1.192 -    val names = Ts
   1.193 -      |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
   1.194 -      |> Name.variant_list [];
   1.195 -  in the o AList.lookup (op =) (Ts ~~ names) end;
   1.196 -
   1.197 -fun eval_for_const ctxt cTs =
   1.198 -  let
   1.199 -    fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
   1.200 -    val names = cTs
   1.201 -      |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
   1.202 -      |> Name.variant_list [];
   1.203 -  in the o AList.lookup (op =) (cTs ~~ names) end;
   1.204 -
   1.205 -end;
   1.206 -
   1.207 -val generated_computationN = "Generated_Computation";
   1.208 -
   1.209  fun print_computation_code ctxt compiled_value requested_Ts cTs =
   1.210    let
   1.211      val proper_cTs = map_filter I cTs;
   1.212 @@ -307,26 +342,13 @@
   1.213      ], map (prefix (generated_computationN ^ ".") o of_term_for_typ') requested_Ts)
   1.214    end;
   1.215  
   1.216 -fun check_typ ctxt T t =
   1.217 -  Syntax.check_term ctxt (Type.constraint T t);
   1.218 -
   1.219 -fun check_computation_input ctxt cTs t =
   1.220 -  let
   1.221 -    fun check t = check_comb (strip_comb t)
   1.222 -    and check_comb (t as Abs _, _) =
   1.223 -          error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
   1.224 -      | check_comb (t as Const (cT as (c, T)), ts) =
   1.225 -          let
   1.226 -            val _ = if not (member (op =) cTs cT)
   1.227 -              then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
   1.228 -              else ();
   1.229 -            val _ = if not (monomorphic T)
   1.230 -              then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
   1.231 -              else ();
   1.232 -            val _ = map check ts;
   1.233 -          in () end;
   1.234 -    val _ = check t;
   1.235 -  in t end;
   1.236 +fun mount_computation ctxt cTs T raw_computation lift_postproc =
   1.237 +  Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
   1.238 +    (fn _ => fn ctxt' =>
   1.239 +      check_typ ctxt' T
   1.240 +      #> reject_vars ctxt'
   1.241 +      #> check_computation_input ctxt' cTs
   1.242 +      #> raw_computation);
   1.243  
   1.244  fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
   1.245    let
   1.246 @@ -340,20 +362,15 @@
   1.247      fun comp' vs_ty_evals =
   1.248        let
   1.249          val (generated_code, compiled_value) =
   1.250 -          build_computation_text ctxt NONE program deps vs_ty_evals;
   1.251 +          build_compilation_text ctxt NONE program deps vs_ty_evals;
   1.252          val (of_term_code, [of_term]) = print_computation_code ctxt compiled_value [T] cTs;
   1.253        in
   1.254          (generated_code ^ "\n" ^ of_term_code,
   1.255            enclose "(" ")" ("fn () => " ^ of_term))
   1.256        end;
   1.257      val compiled_computation =
   1.258 -      Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []);
   1.259 -  in fn ctxt' =>
   1.260 -    check_typ ctxt' T
   1.261 -    #> reject_vars ctxt'
   1.262 -    #> check_computation_input ctxt (map_filter I cTs)
   1.263 -    #> compiled_computation
   1.264 -  end;
   1.265 +      Exn.release (run_compilation_text cookie ctxt comp' vs_ty_evals []);
   1.266 +  in (map_filter I cTs, compiled_computation) end;
   1.267  
   1.268  fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
   1.269    let
   1.270 @@ -365,17 +382,16 @@
   1.271          if not (monomorphic T) then error ("Polymorphic constant:" ^ Syntax.string_of_term ctxt t)
   1.272          else insert (op =) cT | _ => I) ts [];
   1.273      val evals = Abs ("eval", map snd cTs ---> TFree (Name.aT, []), list_comb (Bound 0, map Const cTs));
   1.274 -    val computation = Code_Thingol.dynamic_value ctxt
   1.275 +    val (cTs, raw_computation) = Code_Thingol.dynamic_value ctxt
   1.276        (K I) (compile_computation cookie ctxt T) evals;
   1.277    in
   1.278 -    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
   1.279 -      (K computation)
   1.280 +    mount_computation ctxt cTs T raw_computation lift_postproc
   1.281    end;
   1.282  
   1.283  
   1.284  (** code antiquotation **)
   1.285  
   1.286 -fun evaluation_code ctxt module_name program tycos consts =
   1.287 +fun runtime_code ctxt module_name program tycos consts =
   1.288    let
   1.289      val thy = Proof_Context.theory_of ctxt;
   1.290      val (ml_modules, target_names) =
   1.291 @@ -422,7 +438,7 @@
   1.292    let
   1.293      val program = Code_Thingol.consts_program ctxt consts;
   1.294      val (code, (_, consts_map)) =
   1.295 -      evaluation_code ctxt Code_Target.generatedN program [] consts
   1.296 +      runtime_code ctxt Code_Target.generatedN program [] consts
   1.297    in { code = code, consts_map = consts_map } end);
   1.298  
   1.299  fun register_const const ctxt =
   1.300 @@ -532,7 +548,7 @@
   1.301      val functions = map (prep_const thy) raw_functions;
   1.302      val consts = constrs @ functions;
   1.303      val program = Code_Thingol.consts_program ctxt consts;
   1.304 -    val result = evaluation_code ctxt module_name program tycos consts
   1.305 +    val result = runtime_code ctxt module_name program tycos consts
   1.306        |> (apsnd o apsnd) (chop (length constrs));
   1.307    in
   1.308      thy