src/Tools/Code/code_runtime.ML

 val generated_computationN = "Generated_Computation";
 
 
 (* possible type signatures of constants *)
 
-fun typ_signatures_for T =
+fun typ_signatures' T =
   let
     val (Ts, T') = strip_type T;
   in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end;
 
 fun typ_signatures cTs =
   let
     fun add (c, T) =
       fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts)))
-        (typ_signatures_for T);
+        (typ_signatures' T);
   in
     Typtab.empty
     |> fold add cTs
     |> Typtab.lookup_list
   end;

 
 (* code generation for of the universal morphism *)
 
 val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ;
 
-fun print_of_term_funs { typ_sign_for, eval_for_const, of_term_for_typ } Ts =
+fun print_of_term_funs { typ_signatures_for, eval_for_const, of_term_for_typ } Ts =
   let
     val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
     fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
       |> fold (fn x => fn s => s ^ " $ " ^ x) xs
       |> enclose "(" ")";

       let
         val xs = var_names (length Ts);
       in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end;
     fun print_eqs T =
       let
-        val typ_signs = typ_sign_for T;
+        val typ_signs = typ_signatures_for T;
         val name = of_term_for_typ T;
       in
         map (print_eq T) typ_signs
         |> map (prefix (name ^ " "))
         |> space_implode "\n  | "

     map print_eqs Ts
     |> space_implode "\nand "
     |> prefix "fun "
   end;
 
-fun print_computation_code ctxt compiled_value [] requested_Ts = ("", [])
+fun print_computation_code ctxt compiled_value [] requested_Ts =
+      if null requested_Ts then ("", [])
+      else error ("No equation available for requested type "
+        ^ Syntax.string_of_typ ctxt (hd requested_Ts))
   | print_computation_code ctxt compiled_value cTs requested_Ts =
       let
         val proper_cTs = map_filter I cTs;
-        val typ_sign_for = typ_signatures proper_cTs;
+        val typ_signatures_for = typ_signatures proper_cTs;
         fun add_typ T Ts =
           if member (op =) Ts T
           then Ts
-          else Ts
-            |> cons T
-            |> fold (fold add_typ o snd) (typ_sign_for T);
+          else case typ_signatures_for T of
+            [] => error ("No equation available for requested type "
+              ^ Syntax.string_of_typ ctxt T)
+          | typ_signs =>
+              Ts
+              |> cons T
+              |> fold (fold add_typ o snd) typ_signs;
         val required_Ts = fold add_typ requested_Ts [];
         val of_term_for_typ' = of_term_for_typ required_Ts;
         val eval_for_const' = eval_for_const ctxt proper_cTs;
         val eval_for_const'' = the_default "_" o Option.map eval_for_const';
         val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
         fun mk_abs s = "fn " ^ s ^ " => ";
         val eval_abs = space_implode ""
           (map (mk_abs o eval_for_const'') cTs);
         val of_term_code = print_of_term_funs {
-          typ_sign_for = typ_sign_for,
+          typ_signatures_for = typ_signatures_for,
           eval_for_const = eval_for_const',
           of_term_for_typ = of_term_for_typ' } required_Ts;
         val of_term_names = map (Long_Name.append generated_computationN
           o of_term_for_typ') requested_Ts;
       in