38 val unfold_abs: iexpr -> (vname * itype) list * iexpr; |
38 val unfold_abs: iexpr -> (vname * itype) list * iexpr; |
39 val unfold_let: iexpr -> (ipat * iexpr) list * iexpr; |
39 val unfold_let: iexpr -> (ipat * iexpr) list * iexpr; |
40 val itype_of_iexpr: iexpr -> itype; |
40 val itype_of_iexpr: iexpr -> itype; |
41 val itype_of_ipat: ipat -> itype; |
41 val itype_of_ipat: ipat -> itype; |
42 val ipat_of_iexpr: iexpr -> ipat; |
42 val ipat_of_iexpr: iexpr -> ipat; |
|
43 val iexpr_of_ipat: ipat -> iexpr; |
43 val eq_itype: itype * itype -> bool; |
44 val eq_itype: itype * itype -> bool; |
44 val tvars_of_itypes: itype list -> string list; |
45 val tvars_of_itypes: itype list -> string list; |
45 val vars_of_ipats: ipat list -> string list; |
46 val vars_of_ipats: ipat list -> string list; |
46 val vars_of_iexprs: iexpr list -> string list; |
47 val vars_of_iexprs: iexpr list -> string list; |
47 |
48 |
|
49 type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); |
48 datatype def = |
50 datatype def = |
49 Nop |
51 Undef |
50 | Prim of (string * Pretty.T) list |
52 | Prim of (string * Pretty.T option) list |
51 | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype) |
53 | Fun of funn |
52 | Typesyn of (vname * string list) list * itype |
54 | Typesyn of (vname * string list) list * itype |
53 | Datatype of (vname * string list) list * (string * itype list) list * string list |
55 | Datatype of ((vname * string list) list * (string * itype list) list) * string list |
54 | Datatypecons of string |
56 | Datatypecons of string |
55 | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list |
57 | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list |
56 | Classmember of class |
58 | Classmember of class |
57 | Classinst of (class * (string * (vname * sort) list)) |
59 | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; |
58 * ((string * (string * ClassPackage.sortlookup list list)) list |
|
59 * (string * (string * ClassPackage.sortlookup list list)) list); |
|
60 type module; |
60 type module; |
61 type transact; |
61 type transact; |
62 type 'dst transact_fin; |
62 type 'dst transact_fin; |
63 type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin; |
63 type gen_defgen = string -> transact -> def transact_fin; |
64 type gen_defgen = string -> transact -> (def * string list) transact_fin; |
|
65 val pretty_def: def -> Pretty.T; |
64 val pretty_def: def -> Pretty.T; |
66 val pretty_module: module -> Pretty.T; |
65 val pretty_module: module -> Pretty.T; |
67 val pretty_deps: module -> Pretty.T; |
66 val pretty_deps: module -> Pretty.T; |
68 val empty_module: module; |
67 val empty_module: module; |
69 val add_prim: string -> string list -> (string * Pretty.T) -> module -> module; |
68 val add_prim: string -> string list -> (string * Pretty.T) -> module -> module; |
70 val ensure_prim: string -> module -> module; |
69 val ensure_prim: string -> string -> module -> module; |
71 val get_def: module -> string -> def; |
70 val get_def: module -> string -> def; |
72 val merge_module: module * module -> module; |
71 val merge_module: module * module -> module; |
73 val partof: string list -> module -> module; |
72 val partof: string list -> module -> module; |
74 val has_nsp: string -> string -> bool; |
73 val has_nsp: string -> string -> bool; |
75 val succeed: 'a -> transact -> 'a transact_fin; |
74 val succeed: 'a -> transact -> 'a transact_fin; |
76 val fail: string -> transact -> 'a transact_fin; |
75 val fail: string -> transact -> 'a transact_fin; |
77 val gen_invoke: (string * ('src, 'dst) gen_exprgen) list -> string |
|
78 -> 'src -> transact -> 'dst * transact; |
|
79 val gen_ensure_def: (string * gen_defgen) list -> string |
76 val gen_ensure_def: (string * gen_defgen) list -> string |
80 -> string -> transact -> transact; |
77 -> string -> transact -> transact; |
81 val start_transact: (transact -> 'a * transact) -> module -> 'a * module; |
78 val start_transact: (transact -> 'a * transact) -> module -> 'a * module; |
82 |
79 |
83 val class_eq: string; |
|
84 val type_bool: string; |
|
85 val type_pair: string; |
|
86 val type_list: string; |
|
87 val type_integer: string; |
|
88 val cons_pair: string; |
|
89 val fun_eq: string; |
|
90 val fun_fst: string; |
|
91 val fun_snd: string; |
|
92 val Type_integer: itype; |
|
93 val Cons_true: iexpr; |
|
94 val Cons_false: iexpr; |
|
95 val Cons_pair: iexpr; |
|
96 val Cons_nil: iexpr; |
|
97 val Cons_cons: iexpr; |
|
98 val Fun_eq: iexpr; |
|
99 val Fun_not: iexpr; |
|
100 val Fun_and: iexpr; |
|
101 val Fun_or: iexpr; |
|
102 val Fun_if: iexpr; |
|
103 val Fun_fst: iexpr; |
|
104 val Fun_snd: iexpr; |
|
105 val Fun_0: iexpr; |
|
106 val Fun_1: iexpr; |
|
107 val Fun_add: iexpr; |
|
108 val Fun_mult: iexpr; |
|
109 val Fun_minus: iexpr; |
|
110 val Fun_lt: iexpr; |
|
111 val Fun_le: iexpr; |
|
112 val Fun_wfrec: iexpr; |
|
113 |
|
114 val prims: string list; |
|
115 val invoke_eq: ('a -> transact -> itype * transact) |
|
116 -> (string * (def * (string * sort) list) -> transact -> transact) |
|
117 -> 'a -> transact -> bool * transact; |
|
118 val extract_defs: iexpr -> string list; |
80 val extract_defs: iexpr -> string list; |
119 val eta_expand: (string -> int) -> module -> module; |
81 val eta_expand: (string -> int) -> module -> module; |
120 val eta_expand_poly: module -> module; |
82 val eta_expand_poly: module -> module; |
121 val tupelize_cons: module -> module; |
|
122 val eliminate_classes: module -> module; |
83 val eliminate_classes: module -> module; |
123 |
84 |
124 val debug_level : int ref; |
85 val debug_level: int ref; |
125 val debug : int -> ('a -> string) -> 'a -> 'a; |
86 val debug: int -> ('a -> string) -> 'a -> 'a; |
126 val soft_exc: bool ref; |
87 val soft_exc: bool ref; |
127 |
88 |
128 val serialize: |
89 val serialize: |
129 ((string -> string) -> (string * def) list -> Pretty.T option) |
90 ((string -> string) -> (string * def) list -> 'a option) |
130 -> (string * Pretty.T list -> Pretty.T) |
91 -> (string list -> string * 'a list -> 'b -> 'a * 'b) |
131 -> (string -> string option) |
92 -> (string -> string option) |
132 -> string list list -> string -> module -> Pretty.T |
93 -> string list list -> string -> module -> 'b -> 'a * 'b; |
133 |
|
134 val get_prefix: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * ('a list * 'a list) |
|
135 end; |
94 end; |
136 |
95 |
137 signature CODEGEN_THINGOL_OP = |
96 signature CODEGEN_THINGOL_OP = |
138 sig |
97 sig |
139 include CODEGEN_THINGOL; |
98 include CODEGEN_THINGOL; |
798 Module modl |
774 Module modl |
799 |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) |
775 |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) |
800 |> dest_modl |
776 |> dest_modl |
801 end; |
777 end; |
802 |
778 |
803 fun (*add_check_transform (name, (Datatypecons dtname)) = |
779 fun imports_of modl name_root name = |
804 (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name |
780 let |
805 ^ " of datatype " ^ quote dtname) (); |
781 fun imports prfx [] modl = |
806 ([([dtname], |
782 [] |
807 fn [Datatype (_, _, [])] => NONE |
783 | imports prfx (m::ms) modl = |
808 | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], |
784 map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m)) |
809 [(dtname, |
785 @ map single (Graph.imm_preds modl m); |
810 fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts) |
786 in |
811 | def => "attempted to add datatype constructor to non-datatype: " |
787 map (cons name_root) (imports [] name modl) |
812 ^ (Pretty.output o pretty_def) def |> error)]) |
788 |> map NameSpace.pack |
|
789 end; |
|
790 |
|
791 fun check_samemodule names = |
|
792 fold (fn name => |
|
793 let |
|
794 val modn = (fst o dest_name) name |
|
795 in |
|
796 fn NONE => SOME modn |
|
797 | SOME mod' => if modn = mod' then SOME modn else error "inconsistent name prefix for simultanous names" |
|
798 end |
|
799 ) names NONE; |
|
800 |
|
801 fun check_funeqs eqs = |
|
802 (fold (fn (pats, _) => |
|
803 let |
|
804 val l = length pats |
|
805 in |
|
806 fn NONE => SOME l |
|
807 | SOME l' => if l = l' then SOME l else error "function definition with different number of arguments" |
|
808 end |
|
809 ) eqs NONE; eqs); |
|
810 |
|
811 fun check_prep_def modl Undef = |
|
812 Undef |
|
813 | check_prep_def modl (d as Prim _) = |
|
814 d |
|
815 | check_prep_def modl (Fun (eqs, d)) = |
|
816 Fun (check_funeqs eqs, d) |
|
817 | check_prep_def modl (d as Typesyn _) = |
|
818 d |
|
819 | check_prep_def modl (d as Datatype (_, insts)) = |
|
820 if null insts |
|
821 then d |
|
822 else error "attempted to add datatype with bare instances" |
|
823 | check_prep_def modl (Datatypecons dtco) = |
|
824 error "attempted to add bare datatype constructor" |
|
825 | check_prep_def modl (d as Class ((_, (v, membrs)), insts)) = |
|
826 if null insts |
|
827 then |
|
828 if member (op =) (map fst (Library.flat (map (fst o snd) membrs))) v |
|
829 then error "incorrectly abstracted class type variable" |
|
830 else d |
|
831 else error "attempted to add class with bare instances" |
|
832 | check_prep_def modl (Classmember _) = |
|
833 error "attempted to add bare class member" |
|
834 | check_prep_def modl (Classinst ((d as (class, (tyco, arity)), memdefs))) = |
|
835 let |
|
836 val Class ((_, (v, membrs)), _) = get_def modl class; |
|
837 val _ = if length memdefs > length memdefs |
|
838 then error "too many member definitions given" |
|
839 else (); |
|
840 fun mk_memdef (m, (ctxt, ty)) = |
|
841 case AList.lookup (op =) memdefs m |
|
842 of NONE => error ("missing definition for member " ^ quote m) |
|
843 | SOME (eqs, (ctxt', ty')) => |
|
844 if eq_itype (ty |> instant_itype (v, tyco `%% map IVarT arity), ty') |
|
845 then (m, (check_funeqs eqs, (ctxt', ty'))) |
|
846 else error ("inconsistent type for member definition " ^ quote m) |
|
847 in Classinst (d, map mk_memdef membrs) end; |
|
848 |
|
849 fun postprocess_def (name, Datatype ((_, constrs), _)) = |
|
850 (check_samemodule (name :: map fst constrs); |
|
851 fold (fn (co, _) => |
|
852 ensure_def (co, Datatypecons name) |
|
853 #> add_dep (co, name) |
|
854 #> add_dep (name, co) |
|
855 ) constrs |
813 ) |
856 ) |
814 | add_check_transform (name, Classmember (clsname, v, ty)) = |
857 | postprocess_def (name, Class ((_, (_, membrs)), _)) = |
815 let |
858 (check_samemodule (name :: map fst membrs); |
816 val _ = debug 7 (fn _ => "transformation for class member " ^ quote name |
859 fold (fn (m, _) => |
817 ^ " of class " ^ quote clsname) (); |
860 ensure_def (m, Classmember name) |
818 fun check_var (IType (tyco, tys)) s = |
861 #> add_dep (m, name) |
819 fold check_var tys s |
862 #> add_dep (name, m) |
820 | check_var (IFun (ty1, ty2)) s = |
863 ) membrs |
821 s |
864 ) |
822 |> check_var ty1 |
865 | postprocess_def (name, Classinst ((class, (tyco, _)), _)) = |
823 |> check_var ty2 |
866 map_def class (fn Datatype (d, insts) => Datatype (d, name::insts) |
824 | check_var (IVarT (w, sort)) s = |
867 | d => d) |
825 if v = w |
868 #> map_def class (fn Class (d, insts) => Class (d, name::insts)) |
826 andalso member (op =) sort clsname |
869 | postprocess_def _ = |
827 then "additional class appears at type variable" |> SOME |
870 I; |
828 else NONE |
871 |
829 in |
872 fun succeed some (_, modl) = (Succeed some, modl); |
830 ([([], fn [] => check_var ty NONE), |
873 fun fail msg (_, modl) = (Fail ([msg], NONE), modl); |
831 ([clsname], |
|
832 fn [Class (_, _, _, [])] => NONE |
|
833 | _ => "attempted to add class member to witnessed class" |> SOME)], |
|
834 [(clsname, |
|
835 fn Class (supcs, v, mems, insts) => Class (supcs, v, name::mems, insts) |
|
836 | def => "attempted to add class member to non-class" |
|
837 ^ (Pretty.output o pretty_def) def |> error)]) |
|
838 end |
|
839 | *) add_check_transform (name, Classinst ((clsname, (tyco, arity)), (_, memdefs))) = |
|
840 let |
|
841 val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco |
|
842 ^ " of class " ^ quote clsname) (); |
|
843 (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = |
|
844 let |
|
845 val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c; |
|
846 in if eq_itype (mtyp_i', mtyp_i) |
|
847 then NONE |
|
848 else "wrong type signature for class member: " |
|
849 ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected, " |
|
850 ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME |
|
851 end |
|
852 | check defs = |
|
853 "non-well-formed definitions encountered for classmembers: " |
|
854 ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME *) |
|
855 in |
|
856 ((* map (fn (memname, memprim) => ([memname, memprim], check)) memdefs*) [], |
|
857 [(clsname, |
|
858 fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts) |
|
859 | def => "attempted to add class instance to non-class" |
|
860 ^ (Pretty.output o pretty_def) def |> error), |
|
861 (tyco, |
|
862 fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts) |
|
863 | Nop => Nop |
|
864 | def => "attempted to instantiate non-type to class instance" |
|
865 ^ (Pretty.output o pretty_def) def |> error)]) |
|
866 end |
|
867 | add_check_transform _ = ([], []); |
|
868 |
|
869 (* checks to be implemented here lateron: |
|
870 - well-formedness of function equations |
|
871 - only possible to add defined constructors and class members |
|
872 - right type abstraction with class members |
|
873 - correct typing of instance definitions |
|
874 *) |
|
875 |
|
876 fun succeed some = pair (Succeed some); |
|
877 fun fail msg = pair (Fail ([msg], NONE)); |
|
878 |
874 |
879 fun check_fail _ (Succeed dst, trns) = (dst, trns) |
875 fun check_fail _ (Succeed dst, trns) = (dst, trns) |
880 | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); |
876 | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); |
881 |
877 |
882 fun select_generator _ _ [] modl = |
878 fun select_generator _ src [] modl = |
883 ([], modl) |> fail ("no code generator available") |
879 (SOME src, modl) |> fail ("no code generator available") |
884 | select_generator mk_msg src gens modl = |
880 | select_generator mk_msg src gens modl = |
885 let |
881 let |
886 fun handle_fail msgs f = |
882 fun handle_fail msgs f = |
887 let |
883 let |
888 in |
884 in |
889 if ! soft_exc |
885 if ! soft_exc |
890 then |
886 then |
891 ([], modl) |> f |
887 (SOME src, modl) |> f |
892 handle FAIL exc => (Fail exc, ([], modl)) |
888 handle FAIL exc => (Fail exc, modl) |
893 | e => (Fail (msgs, SOME e), ([], modl)) |
889 | e => (Fail (msgs, SOME e), modl) |
894 else |
890 else |
895 ([], modl) |> f |
891 (SOME src, modl) |> f |
896 handle FAIL exc => (Fail exc, ([], modl)) |
892 handle FAIL exc => (Fail exc, modl) |
897 end; |
893 end; |
898 fun select msgs [(gname, gen)] = |
894 fun select msgs [(gname, gen)] = |
899 handle_fail (msgs @ [mk_msg gname]) (gen src) |
895 handle_fail (msgs @ [mk_msg gname]) (gen src) |
900 fun select msgs ((gname, gen)::gens) = |
896 | select msgs ((gname, gen)::gens) = |
901 let |
897 let |
902 val msgs' = msgs @ [mk_msg gname] |
898 val msgs' = msgs @ [mk_msg gname] |
903 in case handle_fail msgs' (gen src) |
899 in case handle_fail msgs' (gen src) |
904 of (Fail (_, NONE), _) => |
900 of (Fail (_, NONE), _) => |
905 select msgs' gens |
901 select msgs' gens |
906 | result => |
902 | result => result |
907 result |
|
908 end; |
903 end; |
909 in select [] gens end; |
904 in select [] gens end; |
910 |
905 |
911 fun gen_invoke codegens msg src (deps, modl) = |
906 fun gen_ensure_def defgens msg name (dep, modl) = |
912 modl |
907 let |
913 |> select_generator (fn gname => "trying code generator " ^ gname ^ " for source " ^ quote msg) |
908 val msg' = case dep |
914 src codegens |
909 of NONE => msg |
915 |> check_fail msg |
910 | SOME dep => msg ^ ", with dependency " ^ quote dep; |
916 ||> (fn (deps', modl') => (append deps' deps, modl')); |
911 fun add_dp NONE = I |
917 |
912 | add_dp (SOME dep) = |
918 fun gen_ensure_def defgens msg name (deps, modl) = |
913 debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) |
919 let |
914 #> add_dep (dep, name); |
920 fun add (name, def) (deps, modl) = |
915 fun prep_def def modl = |
921 let |
916 (check_prep_def modl def, modl); |
922 val (checks, trans) = add_check_transform (name, def); |
|
923 fun check (check_defs, checker) modl = |
|
924 let |
|
925 fun get_def' s = |
|
926 if NameSpace.is_qualified s |
|
927 then get_def modl s |
|
928 else Nop |
|
929 val defs = |
|
930 check_defs |
|
931 |> map get_def'; |
|
932 in |
|
933 case checker defs |
|
934 of NONE => modl |
|
935 | SOME msg => raise FAIL ([msg], NONE) |
|
936 end; |
|
937 fun transform (name, f) modl = |
|
938 modl |
|
939 |> debug 9 (fn _ => "transforming node " ^ name) |
|
940 |> (if NameSpace.is_qualified name then map_def name f else I); |
|
941 in |
|
942 modl |
|
943 |> debug 10 (fn _ => "considering addition of " ^ name |
|
944 ^ " := " ^ (Pretty.output o pretty_def) def) |
|
945 |> debug 10 (fn _ => "consistency checks") |
|
946 |> fold check checks |
|
947 |> debug 10 (fn _ => "dependencies") |
|
948 |> fold (curry add_dep name) deps |
|
949 |> debug 10 (fn _ => "adding") |
|
950 |> map_def name (fn _ => def) |
|
951 |> debug 10 (fn _ => "transforming") |
|
952 |> fold transform trans |
|
953 |> debug 10 (fn _ => "adding done") |
|
954 end; |
|
955 fun ensure_node name modl = |
|
956 (debug 9 (fn _ => "testing node " ^ quote name) (); |
|
957 if can (get_def modl) name |
|
958 then |
|
959 modl |
|
960 |> debug 9 (fn _ => "asserting node " ^ quote name) |
|
961 |> pair [name] |
|
962 else |
|
963 modl |
|
964 |> debug 9 (fn _ => "allocating node " ^ quote name) |
|
965 |> add_def (name, Nop) |
|
966 |> debug 9 (fn _ => "creating node " ^ quote name) |
|
967 |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) |
|
968 name defgens |
|
969 |> debug 9 (fn _ => "checking creation of node " ^ quote name) |
|
970 |> check_fail msg |
|
971 |-> (fn (def, names') => |
|
972 add (name, def) |
|
973 #> fold_map ensure_node names') |
|
974 |-> (fn names' => pair (name :: Library.flat names')) |
|
975 ) |
|
976 in |
917 in |
977 modl |
918 modl |
978 |> ensure_node name |
919 |> (if can (get_def modl) name |
979 |-> (fn names => pair (names@deps)) |
920 then |
|
921 debug 9 (fn _ => "asserting node " ^ quote name) |
|
922 #> add_dp dep |
|
923 else |
|
924 debug 9 (fn _ => "allocating node " ^ quote name) |
|
925 #> add_def (name, Undef) |
|
926 #> add_dp dep |
|
927 #> debug 9 (fn _ => "creating node " ^ quote name) |
|
928 #> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) |
|
929 name defgens |
|
930 #> debug 9 (fn _ => "checking creation of node " ^ quote name) |
|
931 #> check_fail msg' |
|
932 #-> (fn def => prep_def def) |
|
933 #-> (fn def => |
|
934 debug 10 (fn _ => "addition of " ^ name |
|
935 ^ " := " ^ (Pretty.output o pretty_def) def) |
|
936 #> debug 10 (fn _ => "adding") |
|
937 #> ensure_def (name, def) |
|
938 #> debug 10 (fn _ => "postprocessing") |
|
939 #> postprocess_def (name, def) |
|
940 #> debug 10 (fn _ => "adding done") |
|
941 )) |
|
942 |> pair dep |
980 end; |
943 end; |
981 |
944 |
982 fun start_transact f modl = |
945 fun start_transact f modl = |
983 let |
946 let |
984 fun handle_fail f modl = |
947 fun handle_fail f modl = |
985 ((([], modl) |> f) |
948 (((NONE, modl) |> f) |
986 handle FAIL (msgs, NONE) => |
949 handle FAIL (msgs, NONE) => |
987 (error o cat_lines) ("code generation failed, while:" :: msgs)) |
950 (error o cat_lines) ("code generation failed, while:" :: msgs)) |
988 handle FAIL (msgs, SOME e) => |
951 handle FAIL (msgs, SOME e) => |
989 ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
952 ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
990 in |
953 in |
991 modl |
954 modl |
992 |> handle_fail f |
955 |> handle_fail f |
993 |-> (fn x => fn (_, module) => (x, module)) |
956 |-> (fn x => fn (_, module) => (x, module)) |
994 end; |
957 end; |
995 |
958 |
996 |
|
997 (** primitive language constructs **) |
|
998 |
|
999 val class_eq = "Eq"; (*defined for all primitve types and extensionally for all datatypes*) |
|
1000 val type_bool = "Bool"; |
|
1001 val type_integer = "Integer"; (*infinite!*) |
|
1002 val type_float = "Float"; |
|
1003 val type_pair = "Pair"; |
|
1004 val type_list = "List"; |
|
1005 val cons_true = "True"; |
|
1006 val cons_false = "False"; |
|
1007 val cons_not = "not"; |
|
1008 val cons_pair = "Pair"; |
|
1009 val cons_nil = "Nil"; |
|
1010 val cons_cons = "Cons"; |
|
1011 val fun_eq = "eq"; (*to class eq*) |
|
1012 val fun_not = "not"; |
|
1013 val fun_and = "and"; |
|
1014 val fun_or = "or"; |
|
1015 val fun_if = "if"; |
|
1016 val fun_fst = "fst"; |
|
1017 val fun_snd = "snd"; |
|
1018 val fun_add = "add"; |
|
1019 val fun_mult = "mult"; |
|
1020 val fun_minus = "minus"; |
|
1021 val fun_lt = "lt"; |
|
1022 val fun_le = "le"; |
|
1023 val fun_wfrec = "wfrec"; |
|
1024 |
|
1025 local |
|
1026 |
|
1027 val A = IVarT ("a", []); |
|
1028 val B = IVarT ("b", []); |
|
1029 val E = IVarT ("e", [class_eq]); |
|
1030 |
|
1031 in |
|
1032 |
|
1033 val Type_bool = type_bool `%% []; |
|
1034 val Type_integer = type_integer `%% []; |
|
1035 val Type_float = type_float `%% []; |
|
1036 fun Type_pair a b = type_pair `%% [a, b]; |
|
1037 fun Type_list a = type_list `%% [a]; |
|
1038 val Cons_true = IConst (cons_true, Type_bool); |
|
1039 val Cons_false = IConst (cons_false, Type_bool); |
|
1040 val Cons_pair = IConst (cons_pair, A `-> B `-> Type_pair A B); |
|
1041 val Cons_nil = IConst (cons_nil, Type_list A); |
|
1042 val Cons_cons = IConst (cons_cons, A `-> Type_list A `-> Type_list A); |
|
1043 val Fun_eq = IConst (fun_eq, E `-> E `-> Type_bool); |
|
1044 val Fun_not = IConst (fun_not, Type_bool `-> Type_bool); |
|
1045 val Fun_and = IConst (fun_and, Type_bool `-> Type_bool `-> Type_bool); |
|
1046 val Fun_or = IConst (fun_or, Type_bool `-> Type_bool `-> Type_bool); |
|
1047 val Fun_if = IConst (fun_if, Type_bool `-> A `-> A `-> A); |
|
1048 val Fun_fst = IConst (fun_fst, Type_pair A B `-> A); |
|
1049 val Fun_snd = IConst (fun_snd, Type_pair A B `-> B); |
|
1050 val Fun_0 = IConst ("0", Type_integer); |
|
1051 val Fun_1 = IConst ("1", Type_integer); |
|
1052 val Fun_add = IConst (fun_add, Type_integer `-> Type_integer `-> Type_integer); |
|
1053 val Fun_mult = IConst (fun_mult, Type_integer `-> Type_integer `-> Type_integer); |
|
1054 val Fun_minus = IConst (fun_minus, Type_integer `-> Type_integer); |
|
1055 val Fun_lt = IConst (fun_lt, Type_integer `-> Type_integer `-> Type_bool); |
|
1056 val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool); |
|
1057 val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B); |
|
1058 |
|
1059 fun foldl1 f (x::xs) = |
|
1060 Library.foldl f (x, xs); |
|
1061 val ** = foldl1 (uncurry Type_pair); |
|
1062 val XXp = foldl1 (fn (a, b) => |
|
1063 let |
|
1064 val ty_a = itype_of_ipat a; |
|
1065 val ty_b = itype_of_ipat b; |
|
1066 in ICons ((cons_pair, [a, b]), Type_pair ty_a ty_b) end); |
|
1067 val XXe = foldl1 (fn (a, b) => |
|
1068 let |
|
1069 val ty_a = itype_of_iexpr a; |
|
1070 val ty_b = itype_of_iexpr b; |
|
1071 in IConst (cons_pair, ty_a `-> ty_b `-> Type_pair ty_a ty_b) `$ a `$ b end); |
|
1072 |
|
1073 end; (* local *) |
|
1074 |
|
1075 val prims = [class_eq, type_bool, type_integer, type_float, type_pair, type_list, |
|
1076 cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_eq, fun_not, fun_and, |
|
1077 fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec]; |
|
1078 |
|
1079 |
|
1080 (** equality handling **) |
|
1081 |
|
1082 fun invoke_eq gen_ty gen_eq x (trns as (_ , modl)) = |
|
1083 let |
|
1084 fun mk_eqpred dtname = |
|
1085 let |
|
1086 val (vs, cons, _) = case get_def modl dtname of Datatype info => info; |
|
1087 val arity = map (rpair [class_eq] o fst) vs |
|
1088 val ty = IType (dtname, map IVarT arity); |
|
1089 fun mk_eq (c, []) = |
|
1090 ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true) |
|
1091 | mk_eq (c, tys) = |
|
1092 let |
|
1093 val vars1 = Term.invent_names [] "a" (length tys); |
|
1094 val vars2 = Term.invent_names vars1 "b" (length tys); |
|
1095 fun mk_eq_cons ty' (v1, v2) = |
|
1096 IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty) |
|
1097 fun mk_conj (e1, e2) = |
|
1098 Fun_and `$ e1 `$ e2; |
|
1099 in |
|
1100 ([ICons ((c, map2 (curry IVarP) vars1 tys), ty), |
|
1101 ICons ((c, map2 (curry IVarP) vars2 tys), ty)], |
|
1102 foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2))) |
|
1103 end; |
|
1104 val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)]; |
|
1105 in |
|
1106 (Fun (eqs, (arity, ty `-> ty `-> Type_bool)), arity) |
|
1107 end; |
|
1108 fun invoke' (IType (tyco, tys)) trns = |
|
1109 trns |
|
1110 |> fold_map invoke' tys |
|
1111 |-> (fn is_eq => |
|
1112 if forall I is_eq |
|
1113 then if NameSpace.is_qualified tyco |
|
1114 then |
|
1115 gen_eq (tyco, mk_eqpred tyco) |
|
1116 #> pair true |
|
1117 else |
|
1118 pair true |
|
1119 else |
|
1120 pair false) |
|
1121 | invoke' (IFun _) trns = |
|
1122 trns |
|
1123 |> pair false |
|
1124 | invoke' (IVarT (_, sort)) trns = |
|
1125 trns |
|
1126 |> pair (member (op =) sort class_eq) |
|
1127 in |
|
1128 trns |
|
1129 |> gen_ty x |
|
1130 |-> (fn ty => invoke' ty) |
|
1131 end; |
|
1132 |
959 |
1133 |
960 |
1134 (** generic transformation **) |
961 (** generic transformation **) |
1135 |
962 |
1136 fun extract_defs e = |
963 fun extract_defs e = |