equal
deleted
inserted
replaced
475 gen_code - flag if an abstract type given by quot_thm should be registred |
475 gen_code - flag if an abstract type given by quot_thm should be registred |
476 as an abstract type in the code generator |
476 as an abstract type in the code generator |
477 quot_thm - a quotient theorem (Quotient R Abs Rep T) |
477 quot_thm - a quotient theorem (Quotient R Abs Rep T) |
478 opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive |
478 opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive |
479 (in the form "reflp R") |
479 (in the form "reflp R") |
|
480 opt_par_thm - a parametricity theorem for R |
480 *) |
481 *) |
481 |
482 |
482 fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy = |
483 fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy = |
483 let |
484 let |
484 (**) |
485 (**) |
850 end |
851 end |
851 handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] |
852 handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] |
852 @ (map (Pretty.string_of o Pretty.item o single) errs))) |
853 @ (map (Pretty.string_of o Pretty.item o single) errs))) |
853 end |
854 end |
854 |
855 |
|
856 (* |
|
857 Registers the data in qinfo in the Lifting infrastructure. |
|
858 *) |
|
859 |
855 fun lifting_restore qinfo ctxt = |
860 fun lifting_restore qinfo ctxt = |
856 let |
861 let |
857 val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo |
862 val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo |
858 val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) |
863 val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) |
859 val qty_full_name = (fst o dest_Type) qty |
864 val qty_full_name = (fst o dest_Type) qty |