1.1 --- a/src/Tools/Code/code_thingol.ML Fri Jul 02 16:15:49 2010 +0200
1.2 +++ b/src/Tools/Code/code_thingol.ML Fri Jul 02 16:20:56 2010 +0200
1.3 @@ -86,7 +86,6 @@
1.4 val is_case: stmt -> bool
1.5 val contr_classparam_typs: program -> string -> itype option list
1.6 val labelled_name: theory -> program -> string -> string
1.7 - val labelled_traceback: theory -> program -> string -> string
1.8 val group_stmts: theory -> program
1.9 -> ((string * stmt) list * (string * stmt) list
1.10 * ((string * stmt) list * (string * stmt) list)) list
1.11 @@ -490,15 +489,6 @@
1.12 val Datatype (tyco, _) = Graph.get_node program tyco
1.13 in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
1.14
1.15 -fun labelled_traceback thy program name =
1.16 - let
1.17 - val minimals = Graph.minimals program;
1.18 - val traceback = these (get_first
1.19 - (fn minimal => case Graph.irreducible_paths program (minimal, name)
1.20 - of [] => NONE
1.21 - | p :: ps => SOME p) minimals);
1.22 - in space_implode " -> " (map (labelled_name thy program) traceback) end;
1.23 -
1.24 fun linear_stmts program =
1.25 rev (Graph.strong_conn program)
1.26 |> map (AList.make (Graph.get_node program));
1.27 @@ -557,19 +547,21 @@
1.28
1.29 exception PERMISSIVE of unit;
1.30
1.31 -fun translation_error thy permissive some_thm msg sub_msg (dep, (_, program)) =
1.32 +fun translation_error thy permissive some_thm msg sub_msg =
1.33 if permissive
1.34 then raise PERMISSIVE ()
1.35 else let
1.36 val err_thm = case some_thm
1.37 of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
1.38 | NONE => "";
1.39 - val traceback = case dep
1.40 - of SOME name => labelled_traceback thy program name
1.41 - | NONE => "";
1.42 - val err_traceback = if traceback = ""
1.43 - then "" else "\n(dependencies " ^ traceback ^ ")";
1.44 - in error (msg ^ err_thm ^ err_traceback ^ ":\n" ^ sub_msg) end;
1.45 + in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
1.46 +
1.47 +fun not_wellsorted thy permissive some_thm ty sort e =
1.48 + let
1.49 + val err_class = Sorts.class_error (Syntax.pp_global thy) e;
1.50 + val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
1.51 + ^ Syntax.string_of_sort_global thy sort;
1.52 + in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
1.53
1.54
1.55 (* translation *)
1.56 @@ -706,15 +698,16 @@
1.57 handle PERMISSIVE () => ([], prgrm)
1.58 and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
1.59 let
1.60 - val abstraction_violation = (case some_abs of NONE => true | SOME abs => not (c = abs))
1.61 + val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
1.62 andalso Code.is_abstr thy c
1.63 + then translation_error thy permissive some_thm
1.64 + "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
1.65 + else ()
1.66 val arg_typs = Sign.const_typargs thy (c, ty);
1.67 val sorts = Code_Preproc.sortargs eqngr c;
1.68 val function_typs = (fst o Term.strip_type) ty;
1.69 in
1.70 - abstraction_violation ? translation_error thy permissive some_thm
1.71 - "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
1.72 - #> ensure_const thy algbr eqngr permissive c
1.73 + ensure_const thy algbr eqngr permissive c
1.74 ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
1.75 ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
1.76 ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
1.77 @@ -803,12 +796,6 @@
1.78 #>> (fn sort => (unprefix "'" v, sort))
1.79 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
1.80 let
1.81 - fun format_class_error e =
1.82 - let
1.83 - val err_class = Sorts.class_error (Syntax.pp_global thy) e;
1.84 - val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
1.85 - ^ Syntax.string_of_sort_global thy sort;
1.86 - in err_typ ^ "\n" ^ err_class end;
1.87 datatype typarg =
1.88 Global of (class * string) * typarg list list
1.89 | Local of (class * class) list * (string * (int * sort));
1.90 @@ -822,11 +809,11 @@
1.91 let
1.92 val sort' = proj_sort sort;
1.93 in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
1.94 - val (class_error, typargs) = ("", Sorts.of_sort_derivation algebra
1.95 + val typargs = Sorts.of_sort_derivation algebra
1.96 {class_relation = K (Sorts.classrel_derivation algebra class_relation),
1.97 type_constructor = type_constructor,
1.98 - type_variable = type_variable} (ty, proj_sort sort))
1.99 - handle Sorts.CLASS_ERROR e => (format_class_error e, []);
1.100 + type_variable = type_variable} (ty, proj_sort sort)
1.101 + handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
1.102 fun mk_dict (Global (inst, yss)) =
1.103 ensure_inst thy algbr eqngr permissive inst
1.104 ##>> (fold_map o fold_map) mk_dict yss
1.105 @@ -834,11 +821,7 @@
1.106 | mk_dict (Local (classrels, (v, (n, sort)))) =
1.107 fold_map (ensure_classrel thy algbr eqngr permissive) classrels
1.108 #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
1.109 - in
1.110 - not (class_error = "")
1.111 - ? translation_error thy permissive some_thm "Wellsortedness error" class_error
1.112 - #> fold_map mk_dict typargs
1.113 - end;
1.114 + in fold_map mk_dict typargs end;
1.115
1.116
1.117 (* store *)