src/Tools/Code/code_runtime.ML
changeset 64955 25281bee02ac
parent 64954 e5f535f90d61
child 64956 de7ce0fad5bc
     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:18 2017 +0100
     1.3 @@ -399,31 +399,50 @@
     1.4  
     1.5  structure Code_Antiq_Data = Proof_Data
     1.6  (
     1.7 -  type T = string list * (bool
     1.8 -    * (string * (string * string) list) lazy);
     1.9 -  val empty: T = ([], (true, (Lazy.value ("", []))));
    1.10 +  type T = { named_consts: string list,
    1.11 +    first_occurrence: bool,
    1.12 +    generated_code: {
    1.13 +      code: string,
    1.14 +      consts_map: (string * string) list
    1.15 +    } lazy
    1.16 +  };
    1.17 +  val empty: T = { named_consts = [],
    1.18 +    first_occurrence = true,
    1.19 +    generated_code = Lazy.value {
    1.20 +      code = "",
    1.21 +      consts_map = []
    1.22 +    }
    1.23 +  };
    1.24    fun init _ = empty;
    1.25  );
    1.26  
    1.27 -val is_first_occ = fst o snd o Code_Antiq_Data.get;
    1.28 +val is_first_occurrence = #first_occurrence o Code_Antiq_Data.get;
    1.29 +
    1.30 +fun lazy_code ctxt program consts = Lazy.lazy (fn () =>
    1.31 +  let
    1.32 +    val (code, (_, consts_map)) =
    1.33 +      evaluation_code ctxt Code_Target.generatedN program [] consts
    1.34 +  in { code = code, consts_map = consts_map } end);
    1.35  
    1.36  fun register_const const ctxt =
    1.37    let
    1.38 -    val (consts, _) = Code_Antiq_Data.get ctxt;
    1.39 -    val consts' = insert (op =) const consts;
    1.40 -    val program = Code_Thingol.consts_program ctxt consts';
    1.41 -    val acc_code = Lazy.lazy (fn () =>
    1.42 -      evaluation_code ctxt Code_Target.generatedN program [] consts'
    1.43 -      |> apsnd snd);
    1.44 -  in Code_Antiq_Data.put (consts', (false, acc_code)) ctxt end;
    1.45 +    val consts = insert (op =) const ((#named_consts o Code_Antiq_Data.get) ctxt);
    1.46 +    val program = Code_Thingol.consts_program ctxt consts;
    1.47 +  in
    1.48 +    ctxt
    1.49 +    |> Code_Antiq_Data.put { 
    1.50 +        named_consts = consts,
    1.51 +        first_occurrence = false,
    1.52 +        generated_code = lazy_code ctxt program consts
    1.53 +      }
    1.54 +  end;
    1.55  
    1.56 -fun print_code is_first const ctxt =
    1.57 +fun print_code is_first_occ const ctxt =
    1.58    let
    1.59 -    val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
    1.60 -    val (ml_code, consts_map) = Lazy.force acc_code;
    1.61 -    val ml_code = if is_first then ml_code else "";
    1.62 +    val { code, consts_map } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
    1.63 +    val effective_code = if is_first_occ then code else "";
    1.64      val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const);
    1.65 -  in (ml_code, body) end;
    1.66 +  in (effective_code, body) end;
    1.67  
    1.68  in
    1.69  
    1.70 @@ -431,7 +450,7 @@
    1.71    let
    1.72      val thy = Proof_Context.theory_of ctxt;
    1.73      val const = Code.check_const thy raw_const;
    1.74 -    val is_first = is_first_occ ctxt;
    1.75 +    val is_first = is_first_occurrence ctxt;
    1.76    in (print_code is_first const, register_const const ctxt) end;
    1.77  
    1.78  end; (*local*)