187 Symtab.empty |
188 Symtab.empty |
188 |> Symtab.update ( |
189 |> Symtab.update ( |
189 #ml CodegenSerializer.serializers |
190 #ml CodegenSerializer.serializers |
190 |> apsnd (fn seri => seri |
191 |> apsnd (fn seri => seri |
191 (nsp_dtcon, nsp_class, K false) |
192 (nsp_dtcon, nsp_class, K false) |
192 [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]] |
193 [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]] |
193 ) |
194 ) |
194 ) |
195 ) |
195 |> Symtab.update ( |
196 |> Symtab.update ( |
196 #haskell CodegenSerializer.serializers |
197 #haskell CodegenSerializer.serializers |
197 |> apsnd (fn seri => seri |
198 |> apsnd (fn seri => seri |
198 nsp_dtcon |
199 nsp_dtcon |
199 [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]] |
200 [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]] |
200 ) |
201 ) |
201 ) |
202 ) |
202 ); |
203 ); |
203 |
204 |
204 |
205 |
563 trns |
564 trns |
564 |> ensure_def_tyco thy tabs tyco |
565 |> ensure_def_tyco thy tabs tyco |
565 ||>> fold_map (exprgen_type thy tabs) tys |
566 ||>> fold_map (exprgen_type thy tabs) tys |
566 |-> (fn (tyco, tys) => pair (tyco `%% tys)); |
567 |-> (fn (tyco, tys) => pair (tyco `%% tys)); |
567 |
568 |
568 fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns = |
569 fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns = |
569 trns |
570 trns |
570 |> ensure_def_class thy tabs cls |
571 |> ensure_def_inst thy tabs inst |
571 ||>> ensure_def_inst thy tabs inst |
572 ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls |
572 ||>> (fold_map o fold_map) (mk_lookup thy tabs) ls |
573 |-> (fn (inst, ls) => pair (Instance (inst, ls))) |
573 |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) |
574 | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = |
574 | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns = |
|
575 trns |
575 trns |
576 |> fold_map (ensure_def_class thy tabs) clss |
576 |> fold_map (ensure_def_class thy tabs) clss |
577 |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))) |
577 |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", i)))) |
578 and mk_fun thy tabs (c, ty) trns = |
578 and mk_fun thy tabs (c, ty) trns = |
579 case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) |
579 case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) |
580 of SOME (eq_thms, ty) => |
580 of SOME (eq_thms, ty) => |
581 let |
581 let |
582 val sortctxt = ClassPackage.extract_sortctxt thy ty; |
582 val sortctxt = ClassPackage.extract_sortctxt thy ty; |
595 |> fold_map (exprgen_term thy tabs o devarify_term) args |
595 |> fold_map (exprgen_term thy tabs o devarify_term) args |
596 ||>> (exprgen_term thy tabs o devarify_term) rhs |
596 ||>> (exprgen_term thy tabs o devarify_term) rhs |
597 |-> (fn (args, rhs) => pair (args, rhs)) |
597 |-> (fn (args, rhs) => pair (args, rhs)) |
598 in |
598 in |
599 trns |
599 trns |
600 |> debug 6 (fn _ => "(1) retrieved function equations for " ^ |
|
601 quote (c ^ "::" ^ Sign.string_of_typ thy ty)) |
|
602 |> fold_map (mk_eq o dest_eqthm) eq_thms |
600 |> fold_map (mk_eq o dest_eqthm) eq_thms |
603 |> debug 6 (fn _ => "(2) building equations") |
|
604 ||>> (exprgen_type thy tabs o devarify_type) ty |
601 ||>> (exprgen_type thy tabs o devarify_type) ty |
605 |> debug 6 (fn _ => "(3) building type") |
|
606 ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt |
602 ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt |
607 |> debug 6 (fn _ => "(4) building sort context") |
|
608 |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) |
603 |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) |
609 end |
604 end |
610 | NONE => (NONE, trns) |
605 | NONE => (NONE, trns) |
611 and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = |
606 and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = |
612 let |
607 let |
613 fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns = |
608 fun defgen_inst thy (tabs as (_, (insttab, _, _))) inst trns = |
614 case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) |
609 case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) |
615 of SOME (_, (cls, tyco)) => |
610 of SOME (_, (class, tyco)) => |
616 let |
611 let |
617 val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco); |
612 val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco); |
618 fun gen_suparity supclass trns = |
613 fun gen_suparity supclass trns = |
619 trns |
614 trns |
620 |> ensure_def_inst thy tabs (supclass, tyco) |
615 |> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
621 ||>> (fold_map o fold_map) (mk_lookup thy tabs) |
616 (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass) |
622 (ClassPackage.extract_sortlookup_inst thy (cls, tyco) supclass) |
617 ||>> ensure_def_inst thy tabs (supclass, tyco) |
623 |-> (fn (inst, ls) => pair (supclass, (inst, ls))); |
618 |-> (fn (ls, _) => pair (supclass, ls)); |
624 fun gen_membr (m, ty) trns = |
619 fun gen_membr (m, ty) trns = |
625 trns |
620 trns |
626 |> mk_fun thy tabs (m, ty) |
621 |> mk_fun thy tabs (m, ty) |
627 |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, funn) |
622 |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, funn) |
628 | NONE => error ("could not derive definition for member " ^ quote m)); |
623 | NONE => error ("could not derive definition for member " ^ quote m)); |
629 in |
624 in |
630 trns |
625 trns |
631 |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls |
626 |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls |
632 ^ ", " ^ quote tyco ^ ")") |
627 ^ ", " ^ quote tyco ^ ")") |
633 |> ensure_def_class thy tabs cls |
628 |> ensure_def_class thy tabs class |
634 |> debug 5 (fn _ => "(1) got class") |
|
635 ||>> ensure_def_tyco thy tabs tyco |
629 ||>> ensure_def_tyco thy tabs tyco |
636 |> debug 5 (fn _ => "(2) got type") |
|
637 ||>> fold_map (exprgen_tyvar_sort thy tabs) arity |
630 ||>> fold_map (exprgen_tyvar_sort thy tabs) arity |
638 |> debug 5 (fn _ => "(3) got arity") |
631 ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class) |
639 ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy cls) |
|
640 |> debug 5 (fn _ => "(4) got superarities") |
|
641 ||>> fold_map gen_membr memdefs |
632 ||>> fold_map gen_membr memdefs |
642 |> debug 5 (fn _ => "(5) got members") |
633 |-> (fn ((((class, tyco), arity), suparities), memdefs) => |
643 |-> (fn ((((cls, tyco), arity), suparities), memdefs) => |
634 succeed (Classinst (((class, (tyco, arity)), suparities), memdefs))) |
644 succeed (Classinst (((cls, (tyco, arity)), suparities), memdefs))) |
|
645 end |
635 end |
646 | _ => |
636 | _ => |
647 trns |> fail ("no class instance found for " ^ quote inst); |
637 trns |> fail ("no class instance found for " ^ quote inst); |
648 val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; |
638 val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; |
649 val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); |
639 val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); |
730 |-> (fn (e, es) => pair (e `$$ es)) |
720 |-> (fn (e, es) => pair (e `$$ es)) |
731 end |
721 end |
732 and appgen_default thy tabs ((c, ty), ts) trns = |
722 and appgen_default thy tabs ((c, ty), ts) trns = |
733 trns |
723 trns |
734 |> ensure_def_const thy tabs (c, ty) |
724 |> ensure_def_const thy tabs (c, ty) |
735 ||>> (fold_map o fold_map) (mk_lookup thy tabs) |
725 ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) |
736 (ClassPackage.extract_sortlookup thy (c, ty)) |
726 (ClassPackage.extract_classlookup thy (c, ty)) |
737 ||>> (exprgen_type thy tabs o devarify_type) ty |
727 ||>> (exprgen_type thy tabs o devarify_type) ty |
738 ||>> fold_map (exprgen_term thy tabs o devarify_term) ts |
728 ||>> fold_map (exprgen_term thy tabs o devarify_term) ts |
739 |-> (fn (((c, ls), ty), es) => |
729 |-> (fn (((c, ls), ty), es) => |
740 pair (IConst ((c, ty), ls) `$$ es)) |
730 pair (IConst ((c, ty), ls) `$$ es)) |
741 and appgen thy tabs ((f, ty), ts) trns = |
731 and appgen thy tabs ((f, ty), ts) trns = |