465 Pretty.block [ |
467 Pretty.block [ |
466 Pretty.str "cons ", |
468 Pretty.str "cons ", |
467 Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname]) |
469 Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname]) |
468 ] |
470 ] |
469 | pretty_def (Class (supcls, mems, insts)) = |
471 | pretty_def (Class (supcls, mems, insts)) = |
470 Pretty.str "Class ..." |
472 Pretty.block [ |
|
473 Pretty.str "class extending", |
|
474 Pretty.gen_list "," "[" "]" (map Pretty.str supcls), |
|
475 Pretty.str "with ", |
|
476 Pretty.gen_list "," "[" "]" (map Pretty.str mems), |
|
477 Pretty.str "instances ", |
|
478 Pretty.gen_list "," "[" "]" (map Pretty.str insts) |
|
479 ] |
471 | pretty_def (Classmember (cls, v, ty)) = |
480 | pretty_def (Classmember (cls, v, ty)) = |
472 Pretty.str "Classmember ..." |
481 Pretty.block [ |
473 | pretty_def (Classinst (cls, insts, mems)) = |
482 Pretty.str "class member belonging to ", |
474 Pretty.str "Classinst ..." |
483 Pretty.str cls |
|
484 ] |
|
485 | pretty_def (Classinst (cls, (tyco, arity), mems)) = |
|
486 Pretty.block [ |
|
487 Pretty.str "class instance (", |
|
488 Pretty.str cls, |
|
489 Pretty.str ", (", |
|
490 Pretty.str tyco, |
|
491 Pretty.str ", ", |
|
492 Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str) arity), |
|
493 Pretty.str "))" |
|
494 ]; |
475 |
495 |
476 fun pretty_module modl = |
496 fun pretty_module modl = |
477 let |
497 let |
478 fun pretty (name, Module modl) = |
498 fun pretty (name, Module modl) = |
479 Pretty.block ( |
499 Pretty.block ( |
625 |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) |
645 |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) |
626 |> dest_modl |
646 |> dest_modl |
627 end; |
647 end; |
628 |
648 |
629 fun add_check_transform (name, (Datatypecons (dtname, _))) = |
649 fun add_check_transform (name, (Datatypecons (dtname, _))) = |
|
650 (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name |
|
651 ^ " of datatype " ^ quote dtname) (); |
630 ([([dtname], |
652 ([([dtname], |
631 fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], |
653 fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], |
632 [(dtname, |
654 [(dtname, |
633 fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss) |
655 fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss) |
634 | def => "attempted to add datatype constructor to non-datatype: " |
656 | def => "attempted to add datatype constructor to non-datatype: " |
635 ^ (Pretty.output o pretty_def) def |> error)]) |
657 ^ (Pretty.output o pretty_def) def |> error)]) |
|
658 ) |
636 | add_check_transform (name, Classmember (clsname, v, ty)) = |
659 | add_check_transform (name, Classmember (clsname, v, ty)) = |
637 let |
660 let |
|
661 val _ = debug 7 (fn _ => "transformation for class member " ^ quote name |
|
662 ^ " of class " ^ quote clsname) (); |
638 fun check_var (IType (tyco, tys)) s = |
663 fun check_var (IType (tyco, tys)) s = |
639 fold check_var tys s |
664 fold check_var tys s |
640 | check_var (IFun (ty1, ty2)) s = |
665 | check_var (IFun (ty1, ty2)) s = |
641 s |
666 s |
642 |> check_var ty1 |
667 |> check_var ty1 |
656 | def => "attempted to add class member to non-class" |
681 | def => "attempted to add class member to non-class" |
657 ^ (Pretty.output o pretty_def) def |> error)]) |
682 ^ (Pretty.output o pretty_def) def |> error)]) |
658 end |
683 end |
659 | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) = |
684 | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) = |
660 let |
685 let |
|
686 val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco |
|
687 ^ " of class " ^ quote clsname) (); |
661 fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = |
688 fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = |
662 let |
689 let |
663 val mtyp_i' = instant_itype (v, tyco `%% |
690 val _ = writeln "CHECK RUNNING (1)"; |
664 map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c; |
691 val mtyp_i' = instant_itype (v, tyco `%% |
665 in if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*) |
692 map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c; |
666 then NONE |
693 val _ = writeln "CHECK RUNNING (2)"; |
667 else "wrong type signature for class member: " |
694 in let val XXX = ( |
668 ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected," |
695 if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*) |
669 ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME end |
696 then NONE |
|
697 else "wrong type signature for class member: " |
|
698 ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected," |
|
699 ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME |
|
700 ) in (writeln "CHECK RUNNING (3)"; XXX) end end |
|
701 | check defs = |
|
702 "non-well-formed definitions encountered for classmembers: " |
|
703 ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME |
670 in |
704 in |
671 (map (fn (memname, memprim) => ((writeln memname; writeln memprim; [memname, memprim]), check)) memdefs, |
705 (map (fn (memname, memprim) => ([memname, memprim], check)) memdefs, |
672 [(clsname, |
706 [(clsname, |
673 fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts) |
707 fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts) |
674 | def => "attempted to add class instance to non-class" |
708 | def => "attempted to add class instance to non-class" |
675 ^ (Pretty.output o pretty_def) def |> error), |
709 ^ (Pretty.output o pretty_def) def |> error), |
676 (tyco, |
710 (tyco, |
679 | def => "attempted to instantiate non-type to class instance" |
713 | def => "attempted to instantiate non-type to class instance" |
680 ^ (Pretty.output o pretty_def) def |> error)]) |
714 ^ (Pretty.output o pretty_def) def |> error)]) |
681 end |
715 end |
682 | add_check_transform _ = ([], []); |
716 | add_check_transform _ = ([], []); |
683 |
717 |
684 fun succeed some = (pair o Succeed) some; |
718 fun succeed some = pair (Succeed some); |
685 fun fail msg = (pair o Fail) msg; |
719 fun fail msg = pair (Fail ([msg], NONE)); |
686 |
720 |
687 fun check_fail msg' (Succeed dst, trns) = (dst, trns) |
721 fun check_fail _ (Succeed dst, trns) = (dst, trns) |
688 | check_fail msg' (Fail errmsg, _) = (tracing ("ROLLBACK CHECK: " ^ errmsg ^ "\n" ^ msg'); raise FAIL errmsg); |
722 | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); |
689 |
723 |
690 fun handle_fail msg f modl = |
724 fun select_generator _ _ [] modl = |
691 f modl handle FAIL msg' => ([], modl) |> fail (msg ^ "\n" ^ msg'); |
725 ([], modl) |> fail ("no code generator available") |
692 |
726 | select_generator mk_msg src gens modl = |
693 fun select_generator print_msg src [] trns = |
727 let |
694 fail ("no code generator available") trns |
728 fun handle_fail msgs f = |
695 | select_generator print_msg src [(gname, cgen)] trns = |
729 let |
696 (print_msg gname; cgen src trns) |
730 fun handl trns = |
697 | select_generator print_msg src ((gname, cgen)::cgens) trns = |
731 trns |> f |
698 case cgen src trns |
732 handle FAIL exc => (Fail exc, ([], modl)) |
699 of result as (Succeed _, _) => |
733 in |
700 (print_msg gname; result) |
734 if ! soft_exc |
701 | _ => select_generator print_msg src cgens trns |
735 then |
|
736 ([], modl) |> handl |
|
737 handle e => (Fail (msgs, SOME e), ([], modl)) |
|
738 else |
|
739 ([], modl) |> handl |
|
740 end; |
|
741 fun select msgs [(gname, gen)] = |
|
742 handle_fail (msgs @ [mk_msg gname]) (gen src) |
|
743 fun select msgs ((gname, gen)::gens) = |
|
744 let |
|
745 val msgs' = msgs @ [mk_msg gname] |
|
746 in case handle_fail msgs' (gen src) |
|
747 of (Fail (_, NONE), _) => |
|
748 select msgs' gens |
|
749 | result => |
|
750 result |
|
751 end; |
|
752 in select [] gens end; |
702 |
753 |
703 fun gen_invoke codegens msg src (deps, modl) = |
754 fun gen_invoke codegens msg src (deps, modl) = |
704 ([], modl) |
755 modl |
705 |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for source " ^ quote msg) |
756 |> select_generator (fn gname => "trying code generator " ^ gname ^ " for source " ^ quote msg) |
706 src codegens |
757 src codegens |
707 |> check_fail msg |
758 |> check_fail msg |
708 ||> (fn (deps', modl') => (append deps' deps, modl')); |
759 ||> (fn (deps', modl') => (append deps' deps, modl')); |
709 |
760 |
710 fun gen_ensure_def defgens msg name (deps, modl) = |
761 fun gen_ensure_def defgens msg name (deps, modl) = |
711 let |
762 let |
712 fun add (name, def) (deps, modl) = |
763 fun add (name, def) (deps, modl) = |
713 let |
764 let |
714 val (checks, trans) = add_check_transform (name, def); |
765 val (checks, trans) = add_check_transform (name, def); |
715 fun check (check_defs, checker) modl = |
766 fun check (check_defs, checker) modl = |
716 case checker (check_defs |> filter NameSpace.is_qualified |> map (get_def modl)) |
767 let |
717 of NONE => modl |
768 val _ = writeln ("CHECK (1): " ^ commas check_defs) |
718 | SOME e => raise FAIL e; |
769 fun get_def' s = |
|
770 if NameSpace.is_qualified s |
|
771 then get_def modl s |
|
772 else Nop |
|
773 val defs = |
|
774 check_defs |
|
775 |> map get_def'; |
|
776 val _ = writeln ("CHECK (2): " ^ commas check_defs) |
|
777 in |
|
778 let val XXX = case checker defs |
|
779 of NONE => modl |
|
780 | SOME e => raise FAIL ([e], NONE) |
|
781 in (writeln "CHECK (3)"; XXX) end |
|
782 end; |
719 fun transform (name, f) modl = |
783 fun transform (name, f) modl = |
720 modl |
784 modl |
721 |> K (NameSpace.is_qualified name) ? map_def name f; |
785 |> debug 9 (fn _ => "transforming node " ^ name) |
|
786 |> (if NameSpace.is_qualified name then map_def name f else I); |
722 in |
787 in |
723 modl |
788 modl |
|
789 |> debug 10 (fn _ => "considering addition of " ^ name |
|
790 ^ " := " ^ (Pretty.output o pretty_def) def) |
|
791 |> debug 10 (fn _ => "consistency checks") |
724 |> fold check checks |
792 |> fold check checks |
|
793 |> debug 10 (fn _ => "dependencies") |
725 |> fold (curry add_dep name) deps |
794 |> fold (curry add_dep name) deps |
|
795 |> debug 10 (fn _ => "adding") |
726 |> map_def name (fn _ => def) |
796 |> map_def name (fn _ => def) |
|
797 |> debug 10 (fn _ => "transforming") |
727 |> fold transform trans |
798 |> fold transform trans |
|
799 |> debug 10 (fn _ => "adding done") |
728 end; |
800 end; |
729 fun ensure_node name modl = |
801 fun ensure_node name modl = |
|
802 (debug 9 (fn _ => "testing node " ^ quote name) (); |
730 if can (get_def modl) name |
803 if can (get_def modl) name |
731 then ([name], modl) |
804 then |
|
805 modl |
|
806 |> debug 9 (fn _ => "asserting node " ^ quote name) |
|
807 |> pair [name] |
732 else |
808 else |
733 ([], modl |> add_def (name, Nop)) |
809 modl |
734 |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for definition of " ^ quote name) |
810 |> debug 9 (fn _ => "creating node " ^ quote name) |
|
811 |> add_def (name, Nop) |
|
812 |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) |
735 name defgens |
813 name defgens |
736 |> check_fail msg |
814 |> check_fail msg |
737 |-> (fn (def, names') => |
815 |-> (fn (def, names') => |
738 add (name, def) |
816 add (name, def) |
739 #> fold_map ensure_node names') |
817 #> fold_map ensure_node names') |
740 |-> (fn names' => pair (name :: Library.flat names')) |
818 |-> (fn names' => pair (name :: Library.flat names')) |
|
819 ) |
741 in |
820 in |
742 modl |
821 modl |
743 |> ensure_node name |
822 |> ensure_node name |
744 |-> (fn names => pair (names@deps)) |
823 |-> (fn names => pair (names@deps)) |
745 end; |
824 end; |
746 |
825 |
747 fun start_transact f module = |
826 fun start_transact f modl = |
748 ([], module) |
827 let |
749 |> f |
828 fun handle_fail f modl = |
750 |-> (fn x => fn (_, module) => (x, module)); |
829 ((([], modl) |> f) |
|
830 handle FAIL (msgs, NONE) => |
|
831 (error o cat_lines) ("code generation failed, while:" :: msgs)) |
|
832 handle FAIL (msgs, SOME e) => |
|
833 ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
|
834 in |
|
835 modl |
|
836 |> handle_fail f |
|
837 |-> (fn x => fn (_, module) => (x, module)) |
|
838 end; |
751 |
839 |
752 |
840 |
753 (** primitive language constructs **) |
841 (** primitive language constructs **) |
754 |
842 |
755 val class_eq = "Eqtype"; (*defined for all primitve types and extensionally for all datatypes*) |
843 val class_eq = "Eqtype"; (*defined for all primitve types and extensionally for all datatypes*) |