ensure no duplicates after preprocessing
authorhaftmann
Tue Jan 24 22:29:43 2017 +0100 (2017-01-24)
changeset 649454db1aa362c8c
parent 64944 27b1ba3ef778
child 64946 03b5f4e7f4a6
ensure no duplicates after preprocessing
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Jan 24 22:29:42 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Jan 24 22:29:43 2017 +0100
     1.3 @@ -272,7 +272,8 @@
     1.4  
     1.5  fun print_computation_code ctxt compiled_value requested_Ts cTs =
     1.6    let
     1.7 -    val typ_sign_for = typ_signatures cTs;
     1.8 +    val proper_cTs = map_filter I cTs;
     1.9 +    val typ_sign_for = typ_signatures proper_cTs;
    1.10      fun add_typ T Ts =
    1.11        if member (op =) Ts T
    1.12        then Ts
    1.13 @@ -281,10 +282,12 @@
    1.14          |> fold (fold add_typ o snd) (typ_sign_for T);
    1.15      val required_Ts = fold add_typ requested_Ts [];
    1.16      val of_term_for_typ' = of_term_for_typ required_Ts;
    1.17 -    val eval_for_const' = eval_for_const ctxt cTs;
    1.18 -    val evals = map eval_for_const' cTs;
    1.19 -    val eval_tuple = enclose "(" ")" (commas evals);
    1.20 -    val eval_abs = space_implode "" (map (fn s => "fn " ^ s ^ " => ") evals);
    1.21 +    val eval_for_const' = eval_for_const ctxt proper_cTs;
    1.22 +    val eval_for_const'' = the_default "_" o Option.map eval_for_const';
    1.23 +    val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
    1.24 +    fun mk_abs s = "fn " ^ s ^ " => ";
    1.25 +    val eval_abs = space_implode ""
    1.26 +      (map (mk_abs o eval_for_const'') cTs);
    1.27      val of_term_code = print_of_term_funs {
    1.28        typ_sign_for = typ_sign_for,
    1.29        eval_for_const = eval_for_const',
    1.30 @@ -327,11 +330,13 @@
    1.31  
    1.32  fun compile_computation cookie ctxt T program evals vs_ty_evals deps =
    1.33    let
    1.34 +    fun the_const (Const cT) = cT
    1.35 +      | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)
    1.36      val raw_cTs = case evals of
    1.37 -        Abs (_, _, t) => (snd o strip_comb) t
    1.38 +        Abs (_, _, t) => (map the_const o snd o strip_comb) t
    1.39        | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
    1.40 -    val cTs = map (fn Const cT => cT
    1.41 -      | t => error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)) raw_cTs;
    1.42 +    val cTs = fold_rev (fn cT => fn cTs =>
    1.43 +      (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_cTs [];
    1.44      fun comp' vs_ty_evals =
    1.45        let
    1.46          val (generated_code, compiled_value) =
    1.47 @@ -346,7 +351,7 @@
    1.48    in fn ctxt' =>
    1.49      check_typ ctxt' T
    1.50      #> reject_vars ctxt'
    1.51 -    #> check_computation_input ctxt cTs
    1.52 +    #> check_computation_input ctxt (map_filter I cTs)
    1.53      #> compiled_computation
    1.54    end;
    1.55