114 |
114 |
115 |
115 |
116 (** certificate theorems **) |
116 (** certificate theorems **) |
117 |
117 |
118 fun string_of_lthms r = case Susp.peek r |
118 fun string_of_lthms r = case Susp.peek r |
119 of SOME thms => (map string_of_thm o rev) thms |
119 of SOME thms => (map Display.string_of_thm o rev) thms |
120 | NONE => ["[...]"]; |
120 | NONE => ["[...]"]; |
121 |
121 |
122 fun pretty_lthms ctxt r = case Susp.peek r |
122 fun pretty_lthms ctxt r = case Susp.peek r |
123 of SOME thms => map (ProofContext.pretty_thm ctxt) thms |
123 of SOME thms => map (ProofContext.pretty_thm ctxt) thms |
124 | NONE => [Pretty.str "[...]"]; |
124 | NONE => [Pretty.str "[...]"]; |
145 fun matches [] _ = true |
145 fun matches [] _ = true |
146 | matches (Var _ :: xs) [] = matches xs [] |
146 | matches (Var _ :: xs) [] = matches xs [] |
147 | matches (_ :: _) [] = false |
147 | matches (_ :: _) [] = false |
148 | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; |
148 | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; |
149 fun drop thm' = not (matches args (args_of thm')) |
149 fun drop thm' = not (matches args (args_of thm')) |
150 orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false); |
150 orelse (warning ("code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false); |
151 val (keeps, drops) = List.partition drop sels; |
151 val (keeps, drops) = List.partition drop sels; |
152 in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end; |
152 in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end; |
153 |
153 |
154 fun add_thm thm (sels, dels) = |
154 fun add_thm thm (sels, dels) = |
155 apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels)); |
155 apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels)); |
535 |
535 |
536 fun certify_const thy const thms = |
536 fun certify_const thy const thms = |
537 let |
537 let |
538 fun cert thm = if const = const_of_func thy thm |
538 fun cert thm = if const = const_of_func thy thm |
539 then thm else error ("Wrong head of defining equation,\nexpected constant " |
539 then thm else error ("Wrong head of defining equation,\nexpected constant " |
540 ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm) |
540 ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm) |
541 in map cert thms end; |
541 in map cert thms end; |
542 |
542 |
543 |
543 |
544 |
544 |
545 (** operational sort algebra and class discipline **) |
545 (** operational sort algebra and class discipline **) |
653 in if Sign.typ_instance thy (ty_strongest, ty) |
653 in if Sign.typ_instance thy (ty_strongest, ty) |
654 then if Sign.typ_instance thy (ty, ty_decl) |
654 then if Sign.typ_instance thy (ty, ty_decl) |
655 then thm |
655 then thm |
656 else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty |
656 else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty |
657 ^ "\nof defining equation\n" |
657 ^ "\nof defining equation\n" |
658 ^ string_of_thm thm |
658 ^ Display.string_of_thm thm |
659 ^ "\nto permitted most general type\n" |
659 ^ "\nto permitted most general type\n" |
660 ^ CodeUnit.string_of_typ thy ty_decl); |
660 ^ CodeUnit.string_of_typ thy ty_decl); |
661 constrain thm) |
661 constrain thm) |
662 else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty |
662 else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty |
663 ^ "\nof defining equation\n" |
663 ^ "\nof defining equation\n" |
664 ^ string_of_thm thm |
664 ^ Display.string_of_thm thm |
665 ^ "\nis incompatible with permitted least general type\n" |
665 ^ "\nis incompatible with permitted least general type\n" |
666 ^ CodeUnit.string_of_typ thy ty_strongest) |
666 ^ CodeUnit.string_of_typ thy ty_strongest) |
667 end; |
667 end; |
668 fun check_typ_fun (c, thm) = |
668 fun check_typ_fun (c, thm) = |
669 let |
669 let |
671 val ty_decl = Sign.the_const_type thy c; |
671 val ty_decl = Sign.the_const_type thy c; |
672 in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) |
672 in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) |
673 then thm |
673 then thm |
674 else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty |
674 else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty |
675 ^ "\nof defining equation\n" |
675 ^ "\nof defining equation\n" |
676 ^ string_of_thm thm |
676 ^ Display.string_of_thm thm |
677 ^ "\nis incompatible with declared function type\n" |
677 ^ "\nis incompatible with declared function type\n" |
678 ^ CodeUnit.string_of_typ thy ty_decl) |
678 ^ CodeUnit.string_of_typ thy ty_decl) |
679 end; |
679 end; |
680 fun check_typ (c, thm) = |
680 fun check_typ (c, thm) = |
681 case AxClass.inst_of_param thy c |
681 case AxClass.inst_of_param thy c |
729 let |
729 let |
730 val func = mk_func thm; |
730 val func = mk_func thm; |
731 val c = const_of_func thy func; |
731 val c = const_of_func thy func; |
732 val _ = if (is_some o AxClass.class_of_param thy) c |
732 val _ = if (is_some o AxClass.class_of_param thy) c |
733 then error ("Rejected polymorphic equation for overloaded constant:\n" |
733 then error ("Rejected polymorphic equation for overloaded constant:\n" |
734 ^ string_of_thm thm) |
734 ^ Display.string_of_thm thm) |
735 else (); |
735 else (); |
736 val _ = if (is_some o get_datatype_of_constr thy) c |
736 val _ = if (is_some o get_datatype_of_constr thy) c |
737 then error ("Rejected equation for datatype constructor:\n" |
737 then error ("Rejected equation for datatype constructor:\n" |
738 ^ string_of_thm func) |
738 ^ Display.string_of_thm func) |
739 else (); |
739 else (); |
740 in |
740 in |
741 (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default |
741 (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default |
742 (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy |
742 (c, (false, (Susp.value [], []))) (apsnd (add_thm func))) thy |
743 end; |
743 end; |