src/Pure/sign.ML
changeset 949 83c588d6fee9
parent 926 9d1348498c36
child 952 9e10962866b0
equal deleted inserted replaced
948:3647161d15d3 949:83c588d6fee9
    37     val pprint_typ: sg -> typ -> pprint_args -> unit
    37     val pprint_typ: sg -> typ -> pprint_args -> unit
    38     val certify_typ: sg -> typ -> typ
    38     val certify_typ: sg -> typ -> typ
    39     val certify_term: sg -> term -> term * typ * int
    39     val certify_term: sg -> term -> term * typ * int
    40     val read_typ: sg * (indexname -> sort option) -> string -> typ
    40     val read_typ: sg * (indexname -> sort option) -> string -> typ
    41     val infer_types: sg -> (indexname -> typ option) ->
    41     val infer_types: sg -> (indexname -> typ option) ->
    42       (indexname -> sort option) -> bool -> term list * typ ->
    42       (indexname -> sort option) -> string list -> bool -> bool
    43       int * term * (indexname * typ) list
    43       -> term list * typ -> int * term * (indexname * typ) list
    44     val add_classes: (class * class list) list -> sg -> sg
    44     val add_classes: (class * class list) list -> sg -> sg
    45     val add_classrel: (class * class) list -> sg -> sg
    45     val add_classrel: (class * class) list -> sg -> sg
    46     val add_defsort: sort -> sg -> sg
    46     val add_defsort: sort -> sg -> sg
    47     val add_types: (string * int * mixfix) list -> sg -> sg
    47     val add_types: (string * int * mixfix) list -> sg -> sg
    48     val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    48     val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
   250 
   250 
   251 
   251 
   252 
   252 
   253 (** infer_types **)         (*exception ERROR*)
   253 (** infer_types **)         (*exception ERROR*)
   254 
   254 
   255 fun infer_types sg types sorts print_msg (ts, T) =
   255 fun infer_types sg types sorts used freeze print_msg (ts, T) =
   256   let
   256   let
   257     val Sg {tsig, ...} = sg;
   257     val Sg {tsig, ...} = sg;
   258     val show_typ = string_of_typ sg;
   258     val show_typ = string_of_typ sg;
   259     val show_term = string_of_term sg;
   259     val show_term = string_of_term sg;
   260 
   260 
   266     fun exn_type_msg (msg, Ts, ts) =
   266     fun exn_type_msg (msg, Ts, ts) =
   267 	"\nType checking error: " ^ msg ^ "\n" ^
   267 	"\nType checking error: " ^ msg ^ "\n" ^
   268 	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
   268 	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
   269 
   269 
   270     val T' = certify_typ sg T
   270     val T' = certify_typ sg T
   271       handle TYPE arg => error (exn_type_msg arg);
   271              handle TYPE arg => error (exn_type_msg arg);
   272 
   272 
   273     val ct = const_type sg;
   273     val ct = const_type sg;
   274 
   274 
   275     fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
   275     fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
   276          let fun mk_some (x, y) = (Some x, Some y);
   276          let val (infrd_t', tye', msg') = 
   277 
   277               let val (T,tye) =
   278              val ((infrd_t', tye'), msg') = 
   278                     Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
   279               (mk_some (Type.infer_types (tsig, ct, types, sorts, T', t)), msg)
   279               in (Some T, Some tye, msg) end
   280               handle TYPE arg => ((None, None), exn_type_msg arg)
   280               handle TYPE arg => (None, None, exn_type_msg arg)
   281 
   281 
   282              val old_show_brackets = !show_brackets;
   282              val old_show_brackets = !show_brackets;
   283 
   283 
   284              val _ = (show_brackets := true);
   284              val _ = (show_brackets := true);
   285 
   285 
   289                else (if msg' = "" then 
   289                else (if msg' = "" then 
   290                 "Error: More than one term is type correct:\n" ^
   290                 "Error: More than one term is type correct:\n" ^
   291                 (show_term (the infrd_t)) else msg') ^ "\n" ^ 
   291                 (show_term (the infrd_t)) else msg') ^ "\n" ^ 
   292                 (show_term (the infrd_t')) ^ "\n";
   292                 (show_term (the infrd_t')) ^ "\n";
   293 
   293 
   294              val _ = (show_brackets := old_show_brackets);
   294          in show_brackets := old_show_brackets;
   295          in if is_none infrd_t' then
   295             if is_none infrd_t' then
   296               process_terms ts (idx, infrd_t, tye) msg'' (n+1)
   296               process_terms ts (idx, infrd_t, tye) msg'' (n+1)
   297             else
   297             else
   298               process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
   298               process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
   299          end
   299          end
   300       | process_terms [] (idx, infrd_t, tye) msg _ = 
   300       | process_terms [] (idx, infrd_t, tye) msg _ =