src/Tools/Code/code_thingol.ML
changeset 37697 db7b5f2e19cd
parent 37640 fc27be4c6b1c
child 37698 e38abf437c20
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Jul 02 16:10:59 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Jul 02 16:15:49 2010 +0200
     1.3 @@ -86,6 +86,7 @@
     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 @@ -489,6 +490,15 @@
    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 @@ -547,21 +557,19 @@
    1.28  
    1.29  exception PERMISSIVE of unit;
    1.30  
    1.31 -fun translation_error thy permissive some_thm msg sub_msg =
    1.32 +fun translation_error thy permissive some_thm msg sub_msg (dep, (_, program)) =
    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 -  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
    1.40 -
    1.41 -fun not_wellsorted thy permissive some_thm ty sort e =
    1.42 -  let
    1.43 -    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    1.44 -    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
    1.45 -      ^ Syntax.string_of_sort_global thy sort;
    1.46 -  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
    1.47 +    val traceback = case dep
    1.48 +     of SOME name => labelled_traceback thy program name
    1.49 +      | NONE => "";
    1.50 +    val err_traceback = if traceback = ""
    1.51 +      then "" else "\n(dependencies " ^ traceback ^ ")";
    1.52 +  in error (msg ^ err_thm ^ err_traceback ^ ":\n" ^ sub_msg) end;
    1.53  
    1.54  
    1.55  (* translation *)
    1.56 @@ -698,16 +706,15 @@
    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 _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
    1.61 +    val abstraction_violation = (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 -    ensure_const thy algbr eqngr permissive c
    1.71 +    abstraction_violation ? translation_error thy permissive some_thm
    1.72 +      "Abstraction violation" ("constant " ^ Code.string_of_const thy 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 @@ -796,6 +803,12 @@
    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 @@ -809,11 +822,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 typargs = Sorts.of_sort_derivation algebra
    1.95 +    val (class_error, 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 => not_wellsorted thy permissive some_thm ty sort e;
   1.100 +       type_variable = type_variable} (ty, proj_sort sort))
   1.101 +      handle Sorts.CLASS_ERROR e => (format_class_error 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 @@ -821,7 +834,11 @@
   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 fold_map mk_dict typargs end;
   1.110 +  in
   1.111 +    not (class_error = "")
   1.112 +      ? translation_error thy permissive some_thm "Wellsortedness error" class_error
   1.113 +    #> fold_map mk_dict typargs
   1.114 +  end;
   1.115  
   1.116  
   1.117  (* store *)