src/Tools/Code/code_runtime.ML
changeset 64990 c6a7de505796
parent 64989 40c36a4aee1f
child 64991 d2c79b16e133
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:33 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Feb 06 20:56:34 2017 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4  
     1.5  (* possible type signatures of constants *)
     1.6  
     1.7 -fun typ_signatures_for T =
     1.8 +fun typ_signatures' T =
     1.9    let
    1.10      val (Ts, T') = strip_type T;
    1.11    in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end;
    1.12 @@ -215,7 +215,7 @@
    1.13    let
    1.14      fun add (c, T) =
    1.15        fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts)))
    1.16 -        (typ_signatures_for T);
    1.17 +        (typ_signatures' T);
    1.18    in
    1.19      Typtab.empty
    1.20      |> fold add cTs
    1.21 @@ -284,7 +284,7 @@
    1.22  
    1.23  val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ;
    1.24  
    1.25 -fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
    1.26 +fun print_of_term_funs { typ_signatures_for, eval_for_const, of_term_for_typ } Ts =
    1.27    let
    1.28      val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
    1.29      fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
    1.30 @@ -299,7 +299,7 @@
    1.31        in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end;
    1.32      fun print_eqs T =
    1.33        let
    1.34 -        val typ_signs = typ_sign_for T;
    1.35 +        val typ_signs = typ_signatures_for T;
    1.36          val name = of_term_for_typ T;
    1.37        in
    1.38          map (print_eq T) typ_signs
    1.39 @@ -312,17 +312,24 @@
    1.40      |> prefix "fun "
    1.41    end;
    1.42  
    1.43 -fun print_computation_code ctxt compiled_value [] requested_Ts = ("", [])
    1.44 +fun print_computation_code ctxt compiled_value [] requested_Ts =
    1.45 +      if null requested_Ts then ("", [])
    1.46 +      else error ("No equation available for requested type "
    1.47 +        ^ Syntax.string_of_typ ctxt (hd requested_Ts))
    1.48    | print_computation_code ctxt compiled_value cTs requested_Ts =
    1.49        let
    1.50          val proper_cTs = map_filter I cTs;
    1.51 -        val typ_sign_for = typ_signatures proper_cTs;
    1.52 +        val typ_signatures_for = typ_signatures proper_cTs;
    1.53          fun add_typ T Ts =
    1.54            if member (op =) Ts T
    1.55            then Ts
    1.56 -          else Ts
    1.57 -            |> cons T
    1.58 -            |> fold (fold add_typ o snd) (typ_sign_for T);
    1.59 +          else case typ_signatures_for T of
    1.60 +            [] => error ("No equation available for requested type "
    1.61 +              ^ Syntax.string_of_typ ctxt T)
    1.62 +          | typ_signs =>
    1.63 +              Ts
    1.64 +              |> cons T
    1.65 +              |> fold (fold add_typ o snd) typ_signs;
    1.66          val required_Ts = fold add_typ requested_Ts [];
    1.67          val of_term_for_typ' = of_term_for_typ required_Ts;
    1.68          val eval_for_const' = eval_for_const ctxt proper_cTs;
    1.69 @@ -332,7 +339,7 @@
    1.70          val eval_abs = space_implode ""
    1.71            (map (mk_abs o eval_for_const'') cTs);
    1.72          val of_term_code = print_of_term_funs {
    1.73 -          typ_sign_for = typ_sign_for,
    1.74 +          typ_signatures_for = typ_signatures_for,
    1.75            eval_for_const = eval_for_const',
    1.76            of_term_for_typ = of_term_for_typ' } required_Ts;
    1.77          val of_term_names = map (Long_Name.append generated_computationN