equal
deleted
inserted
replaced
300 |
300 |
301 fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) = |
301 fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) = |
302 let |
302 let |
303 exception NO_MATCH; |
303 exception NO_MATCH; |
304 fun eq_sctxt subs sctxt1 sctxt2 = |
304 fun eq_sctxt subs sctxt1 sctxt2 = |
305 map (fn (v, sort) => case AList.lookup (op =) subs v |
305 map (fn (v : string, sort : string list) => case AList.lookup (op =) subs v |
306 of NONE => raise NO_MATCH |
306 of NONE => raise NO_MATCH |
307 | SOME v' => case AList.lookup (op =) sctxt2 v' |
307 | SOME (v' : string) => case AList.lookup (op =) sctxt2 v' |
308 of NONE => raise NO_MATCH |
308 of NONE => raise NO_MATCH |
309 | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1 |
309 | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1 |
310 fun eq (ITyVar v1) (ITyVar v2) subs = |
310 fun eq (ITyVar v1) (ITyVar v2) subs = |
311 (case AList.lookup (op =) subs v1 |
311 (case AList.lookup (op =) subs v1 |
312 of NONE => subs |> AList.update (op =) (v1, v2) |
312 of NONE => subs |> AList.update (op =) (v1, v2) |
428 type transact = Graph.key option * module; |
428 type transact = Graph.key option * module; |
429 datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option; |
429 datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option; |
430 type 'dst transact_fin = 'dst transact_res * module; |
430 type 'dst transact_fin = 'dst transact_res * module; |
431 exception FAIL of string list * exn option; |
431 exception FAIL of string list * exn option; |
432 |
432 |
433 val eq_def = (op =); |
433 val eq_def = (op =) : def * def -> bool; |
434 |
434 |
435 (* simple diagnosis *) |
435 (* simple diagnosis *) |
436 |
436 |
437 fun pretty_def Undef = |
437 fun pretty_def Undef = |
438 Pretty.str "<UNDEF>" |
438 Pretty.str "<UNDEF>" |
695 fun merge_module modl12 = |
695 fun merge_module modl12 = |
696 let |
696 let |
697 fun join_module _ (Module m1, Module m2) = |
697 fun join_module _ (Module m1, Module m2) = |
698 Module (merge_module (m1, m2)) |
698 Module (merge_module (m1, m2)) |
699 | join_module name (Def d1, Def d2) = |
699 | join_module name (Def d1, Def d2) = |
700 if eq_def (d1, d2) then Def d1 else raise Graph.DUP name |
700 if eq_def (d1, d2) then Def d1 else Def d1 (*raise Graph.DUP name*) |
701 | join_module name _ = raise Graph.DUP name |
701 | join_module name _ = raise Graph.DUP name |
702 in Graph.join join_module modl12 end; |
702 in Graph.join join_module modl12 end; |
703 |
703 |
704 fun diff_module modl12 = |
704 fun diff_module modl12 = |
705 let |
705 let |
947 fun handle_fail f x = |
947 fun handle_fail f x = |
948 (f x |
948 (f x |
949 handle FAIL (msgs, NONE) => |
949 handle FAIL (msgs, NONE) => |
950 (error o cat_lines) ("code generation failed, while:" :: msgs)) |
950 (error o cat_lines) ("code generation failed, while:" :: msgs)) |
951 handle FAIL (msgs, SOME e) => |
951 handle FAIL (msgs, SOME e) => |
952 ((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
952 ((Output.error_msg o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
953 in |
953 in |
954 (init, modl) |
954 (init, modl) |
955 |> handle_fail f |
955 |> handle_fail f |
956 |-> (fn x => fn (_, module) => (x, module)) |
956 |-> (fn x => fn (_, module) => (x, module)) |
957 end; |
957 end; |