src/Tools/Code/code_runtime.ML
changeset 64940 19ca3644ec46
parent 64928 18a6b96f8b00
child 64943 c5618df67c2a
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Jan 23 17:35:37 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Jan 22 21:39:16 2017 +0100
     1.3 @@ -28,18 +28,10 @@
     1.4      -> Proof.context -> term -> 'a Exn.result
     1.5    val dynamic_holds_conv: Proof.context -> conv
     1.6    val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     1.7 -  val fully_static_value: (Proof.context -> term -> 'a) cookie
     1.8 -    -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
     1.9 -           consts: (string * typ) list, T: typ }
    1.10 -    -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*)
    1.11 -  val fully_static_value_strict: (Proof.context -> term -> 'a) cookie
    1.12 +  val experimental_computation: (Proof.context -> term -> 'a) cookie
    1.13      -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.14 -           consts: (string * typ) list, T: typ }
    1.15 +           terms: term list, T: typ }
    1.16      -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
    1.17 -  val fully_static_value_exn: (Proof.context -> term -> 'a) cookie
    1.18 -    -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
    1.19 -           consts: (string * typ) list, T: typ }
    1.20 -    -> Proof.context -> term -> 'a Exn.result (*EXPERIMENTAL!*)
    1.21    val code_reflect: (string * string list option) list -> string list -> string
    1.22      -> string option -> theory -> theory
    1.23    datatype truth = Holds
    1.24 @@ -62,7 +54,6 @@
    1.25  val s_Holds = Long_Name.append this "Holds";
    1.26  
    1.27  val target = "Eval";
    1.28 -val structure_generated = "Generated_Code";
    1.29  
    1.30  datatype truth = Holds;
    1.31  
    1.32 @@ -203,7 +194,156 @@
    1.33  end; (*local*)
    1.34  
    1.35  
    1.36 -(** fully static evaluation -- still with limited coverage! **)
    1.37 +(** computations -- experimental! **)
    1.38 +
    1.39 +fun typ_signatures_for T =
    1.40 +  let
    1.41 +    val (Ts, T') = strip_type T;
    1.42 +  in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end;
    1.43 +
    1.44 +fun typ_signatures cTs =
    1.45 +  let
    1.46 +    fun add (c, T) =
    1.47 +      fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts)))
    1.48 +        (typ_signatures_for T);
    1.49 +  in
    1.50 +    Typtab.empty
    1.51 +    |> fold add cTs
    1.52 +    |> Typtab.lookup_list
    1.53 +  end;
    1.54 +
    1.55 +fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
    1.56 +  let
    1.57 +    val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
    1.58 +    fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
    1.59 +      |> fold (fn x => fn s => s ^ " $ " ^ x) xs
    1.60 +      |> enclose "(" ")"
    1.61 +      |> prefix "ctxt ";
    1.62 +    fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T)
    1.63 +      |> fold2 (fn T' => fn x => fn s =>
    1.64 +         s ^ (" (" ^ of_term_for_typ T' ^ " ctxt " ^ x ^ ")")) Ts xs
    1.65 +    fun print_eq T (c, Ts) =
    1.66 +      let
    1.67 +        val xs = var_names (length Ts);
    1.68 +      in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end;
    1.69 +    val err_eq =
    1.70 +      "ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)";
    1.71 +    fun print_eqs T =
    1.72 +      let
    1.73 +        val typ_signs = typ_sign_for T;
    1.74 +        val name = of_term_for_typ T;
    1.75 +      in
    1.76 +        (map (print_eq T) typ_signs @ [err_eq])
    1.77 +        |> map (prefix (name ^ " "))
    1.78 +        |> space_implode "\n  | "
    1.79 +      end;
    1.80 +  in
    1.81 +    map print_eqs Ts
    1.82 +    |> space_implode "\nand "
    1.83 +    |> prefix "fun "
    1.84 +  end;
    1.85 +
    1.86 +local
    1.87 +
    1.88 +fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
    1.89 +  | tycos_of _ = [];
    1.90 +
    1.91 +val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
    1.92 +
    1.93 +in
    1.94 +
    1.95 +fun of_term_for_typ Ts =
    1.96 +  let
    1.97 +    val names = Ts
    1.98 +      |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
    1.99 +      |> Name.variant_list [];
   1.100 +  in the o AList.lookup (op =) (Ts ~~ names) end;
   1.101 +
   1.102 +fun eval_for_const ctxt cTs =
   1.103 +  let
   1.104 +    fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
   1.105 +    val names = cTs
   1.106 +      |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
   1.107 +      |> Name.variant_list [];
   1.108 +  in the o AList.lookup (op =) (cTs ~~ names) end;
   1.109 +
   1.110 +end;
   1.111 +
   1.112 +val generated_computationN = "Generated_Computation";
   1.113 +
   1.114 +fun print_computation_code ctxt compiled_value T cTs =
   1.115 +  let
   1.116 +    val typ_sign_for = typ_signatures cTs;
   1.117 +    fun add_typ T Ts =
   1.118 +      if member (op =) Ts T
   1.119 +      then Ts
   1.120 +      else Ts
   1.121 +        |> cons T
   1.122 +        |> fold (fold add_typ o snd) (typ_sign_for T);
   1.123 +    val Ts = add_typ T [];
   1.124 +    val of_term_for_typ' = of_term_for_typ Ts;
   1.125 +    val of_terms = map of_term_for_typ' Ts;
   1.126 +    val eval_for_const' = eval_for_const ctxt cTs;
   1.127 +    val evals = map eval_for_const' cTs;
   1.128 +    val eval_tuple = enclose "(" ")" (commas evals);
   1.129 +    val eval_abs = space_implode "" (map (fn s => "fn " ^ s ^ " => ") evals);
   1.130 +    val of_term_code = print_of_term_funs {
   1.131 +      typ_sign_for = typ_sign_for,
   1.132 +      eval_for_const = eval_for_const',
   1.133 +      of_term_for_typ = of_term_for_typ' } Ts;
   1.134 +  in
   1.135 +    (cat_lines [
   1.136 +      "structure " ^ generated_computationN ^ " =",
   1.137 +      "struct",
   1.138 +      "",
   1.139 +      "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()",
   1.140 +      "  (" ^ eval_abs,
   1.141 +      "    " ^ eval_tuple ^ ");",
   1.142 +      "",
   1.143 +      of_term_code,
   1.144 +      "",
   1.145 +      "end"
   1.146 +    ], map (prefix (generated_computationN ^ ".")) of_terms)
   1.147 +  end;
   1.148 +
   1.149 +fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
   1.150 +  let
   1.151 +    val raw_cTs = case evals of
   1.152 +        Abs (_, _, t) => (snd o strip_comb) t
   1.153 +      | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
   1.154 +    val cTs = map (fn Const cT => cT
   1.155 +      | t => error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)) raw_cTs;
   1.156 +    fun comp' vs_ty_evals =
   1.157 +      let
   1.158 +        val (generated_code, compiled_value) =
   1.159 +          build_computation_text ctxt NONE program deps vs_ty_evals;
   1.160 +        val (of_term_code, of_terms) = print_computation_code ctxt compiled_value T cTs;
   1.161 +      in
   1.162 +        (generated_code ^ "\n" ^ of_term_code,
   1.163 +          enclose "(" ")" ("fn () => " ^ List.last of_terms))
   1.164 +      end;
   1.165 +    val compiled_computation =
   1.166 +      Exn.release (run_computation_text cookie ctxt comp' vs_ty_evals []);
   1.167 +  in fn ctxt' =>
   1.168 +    compiled_computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
   1.169 +  end;
   1.170 +
   1.171 +fun experimental_computation cookie { ctxt, lift_postproc, terms = ts, T } =
   1.172 +  let
   1.173 +    val cTs = (fold o fold_aterms) (fn Const cT => insert (op =) cT | _ => I) ts [];
   1.174 +    val vT = TFree (singleton (Name.variant_list
   1.175 +      (fold (fn (_, T) => fold_atyps (fn TFree (v, _) => insert (op =) v | _ => I)
   1.176 +        T) cTs [])) Name.aT, []);
   1.177 +    val evals = Abs ("eval", map snd cTs ---> vT, list_comb (Bound 0, map Const cTs));
   1.178 +    val computation = Code_Thingol.dynamic_value ctxt
   1.179 +      (K I) (compile_computation cookie ctxt T) evals;
   1.180 +  in
   1.181 +    Code_Preproc.static_value { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
   1.182 +      (K computation)
   1.183 +  end;
   1.184 +
   1.185 +
   1.186 +(** code antiquotation **)
   1.187  
   1.188  fun evaluation_code ctxt module_name program tycos consts =
   1.189    let
   1.190 @@ -225,107 +365,6 @@
   1.191          | SOME tyco' => (tyco, tyco')) tycos tycos';
   1.192    in (ml_code, (tycos_map, consts_map)) end;
   1.193  
   1.194 -fun typ_signatures_for T =
   1.195 -  let
   1.196 -    val (Ts, T') = strip_type T;
   1.197 -  in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end;
   1.198 -
   1.199 -fun typ_signatures cTs =
   1.200 -  let
   1.201 -    fun add (c, T) =
   1.202 -      fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts)))
   1.203 -        (typ_signatures_for T);
   1.204 -  in
   1.205 -    Typtab.empty
   1.206 -    |> fold add cTs
   1.207 -    |> Typtab.lookup_list
   1.208 -  end;
   1.209 -
   1.210 -fun print_of_term_funs { typ_sign_for, ml_name_for_const, ml_name_for_typ } Ts =
   1.211 -  let
   1.212 -    val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
   1.213 -    fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
   1.214 -      |> fold (fn x => fn s => s ^ " $ " ^ x) xs
   1.215 -      |> enclose "(" ")"
   1.216 -      |> prefix "ctxt ";
   1.217 -    fun print_rhs c Ts xs = ml_name_for_const c
   1.218 -      |> fold2 (fn T => fn x => fn s =>
   1.219 -         s ^ (" (" ^ ml_name_for_typ T ^ " ctxt " ^ x ^ ")")) Ts xs
   1.220 -    fun print_eq (c, Ts) =
   1.221 -      let
   1.222 -        val xs = var_names (length Ts);
   1.223 -      in print_lhs c xs ^ " = " ^ print_rhs c Ts xs end;
   1.224 -    val err_eq =
   1.225 -      "ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)";
   1.226 -    fun print_eqs T =
   1.227 -      let
   1.228 -        val typ_signs = typ_sign_for T;
   1.229 -        val name = ml_name_for_typ T;
   1.230 -      in
   1.231 -        (map print_eq typ_signs @ [err_eq])
   1.232 -        |> map (prefix (name ^ " "))
   1.233 -        |> space_implode "\n  | "
   1.234 -      end;
   1.235 -  in
   1.236 -    map print_eqs Ts
   1.237 -    |> space_implode "\nand "
   1.238 -    |> prefix "fun "
   1.239 -    |> pair (map ml_name_for_typ Ts)
   1.240 -  end;
   1.241 -
   1.242 -fun print_of_term ctxt ml_name_for_const T cTs =
   1.243 -  let
   1.244 -    val typ_sign_for = typ_signatures cTs;
   1.245 -    fun add_typ T Ts =
   1.246 -      if member (op =) Ts T
   1.247 -      then Ts
   1.248 -      else Ts
   1.249 -        |> cons T
   1.250 -        |> fold (fold add_typ o snd) (typ_sign_for T);
   1.251 -    val Ts = add_typ T [];
   1.252 -    fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   1.253 -      | tycos_of _ = [];
   1.254 -    val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
   1.255 -    val ml_names = map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) Ts
   1.256 -      |> Name.variant_list [];
   1.257 -    val ml_name_for_typ = the o AList.lookup (op =) (Ts ~~ ml_names);
   1.258 -  in
   1.259 -    print_of_term_funs { typ_sign_for = typ_sign_for,
   1.260 -      ml_name_for_const = ml_name_for_const,
   1.261 -      ml_name_for_typ = ml_name_for_typ } Ts
   1.262 -  end;
   1.263 -
   1.264 -fun compile_computation cookie ctxt cs_code cTs T { program, deps } =
   1.265 -  let
   1.266 -    val (context_code, (_, const_map)) =
   1.267 -      evaluation_code ctxt structure_generated program [] cs_code;
   1.268 -    val ml_name_for_const = the o AList.lookup (op =) const_map;
   1.269 -    val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs
   1.270 -    val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
   1.271 -  in
   1.272 -    Code_Preproc.timed_value "computing" 
   1.273 -      (fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t)
   1.274 -  end;
   1.275 -
   1.276 -fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
   1.277 -  let
   1.278 -    val thy = Proof_Context.theory_of ctxt;
   1.279 -    val cs_code = map (Axclass.unoverload_const thy) consts;
   1.280 -    val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
   1.281 -    val computation = Code_Thingol.static_value { ctxt = ctxt,
   1.282 -      lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
   1.283 -      (compile_computation cookie ctxt cs_code cTs T);
   1.284 -  in fn ctxt' =>
   1.285 -    computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
   1.286 -  end;
   1.287 -
   1.288 -fun fully_static_value_strict cookie x = Exn.release oo fully_static_value_exn cookie x;
   1.289 -
   1.290 -fun fully_static_value cookie x = partiality_as_none oo fully_static_value_exn cookie x;
   1.291 -
   1.292 -
   1.293 -(** code antiquotation **)
   1.294 -
   1.295  local
   1.296  
   1.297  structure Code_Antiq_Data = Proof_Data
   1.298 @@ -345,7 +384,7 @@
   1.299      val consts' = fold (insert (op =)) new_consts consts;
   1.300      val program = Code_Thingol.consts_program ctxt consts';
   1.301      val acc_code = Lazy.lazy (fn () =>
   1.302 -      evaluation_code ctxt structure_generated program tycos' consts'
   1.303 +      evaluation_code ctxt Code_Target.generatedN program tycos' consts'
   1.304        |> apsnd snd);
   1.305    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
   1.306  
   1.307 @@ -553,7 +592,7 @@
   1.308    |-> (fn ([Const (const, _)], _) =>
   1.309      Code_Target.set_printings (Constant (const,
   1.310        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   1.311 -  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE structure_generated []));
   1.312 +  #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target NONE Code_Target.generatedN []));
   1.313  
   1.314  fun process_file filepath (definienda, thy) =
   1.315    let