362 |
362 |
363 fun string_for_assign_clause [] = "\<bot>" |
363 fun string_for_assign_clause [] = "\<bot>" |
364 | string_for_assign_clause asgs = |
364 | string_for_assign_clause asgs = |
365 space_implode " \<or> " (map string_for_assign asgs) |
365 space_implode " \<or> " (map string_for_assign asgs) |
366 |
366 |
367 fun do_assign _ NONE = NONE |
367 fun add_assign_conjunct _ NONE = NONE |
368 | do_assign (x, a) (SOME asgs) = |
368 | add_assign_conjunct (x, a) (SOME asgs) = |
369 case AList.lookup (op =) asgs x of |
369 case AList.lookup (op =) asgs x of |
370 SOME a' => if a = a' then SOME asgs else NONE |
370 SOME a' => if a = a' then SOME asgs else NONE |
371 | NONE => SOME ((x, a) :: asgs) |
371 | NONE => SOME ((x, a) :: asgs) |
372 |
372 |
373 fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) = |
373 fun add_assign_disjunct _ NONE = NONE |
|
374 | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs) |
|
375 |
|
376 fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) = |
374 (case (aa1, aa2) of |
377 (case (aa1, aa2) of |
375 (A a1, A a2) => if a1 = a2 then SOME accum else NONE |
378 (A a1, A a2) => if a1 = a2 then SOME accum else NONE |
376 | (V x1, A a2) => |
379 | (V x1, A a2) => |
377 SOME asgs |> do_assign (x1, a2) |> Option.map (rpair comps) |
380 SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps) |
378 | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps) |
381 | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps) |
379 | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum) |
382 | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum) |
380 | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) = |
383 | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) = |
381 (case (aa1, aa2) of |
384 (case (aa1, aa2) of |
382 (_, A Gen) => SOME accum |
385 (_, A Gen) => SOME accum |
383 | (A Gen, A _) => NONE |
386 | (A Gen, A _) => NONE |
384 | (A a1, A a2) => if a1 = a2 then SOME accum else NONE |
387 | (A a1, A a2) => if a1 = a2 then SOME accum else NONE |
385 | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps)) |
388 | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps)) |
386 | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) = |
389 | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) = |
387 SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps) |
390 SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps) |
388 |
391 |
389 fun do_mtype_comp _ _ _ _ NONE = NONE |
392 fun do_mtype_comp _ _ _ _ NONE = NONE |
390 | do_mtype_comp _ _ MAlpha MAlpha accum = accum |
393 | do_mtype_comp _ _ MAlpha MAlpha accum = accum |
391 | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22)) |
394 | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22)) |
392 (SOME accum) = |
395 (SOME accum) = |
393 accum |> do_annotation_atom_comp Eq xs aa1 aa2 |
396 accum |> add_annotation_atom_comp Eq xs aa1 aa2 |
394 |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22 |
397 |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22 |
395 | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22)) |
398 | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22)) |
396 (SOME accum) = |
399 (SOME accum) = |
397 (if exists_alpha_sub_mtype M11 then |
400 (if exists_alpha_sub_mtype M11 then |
398 accum |> do_annotation_atom_comp Leq xs aa1 aa2 |
401 accum |> add_annotation_atom_comp Leq xs aa1 aa2 |
399 |> do_mtype_comp Leq xs M21 M11 |
402 |> do_mtype_comp Leq xs M21 M11 |
400 |> (case aa2 of |
403 |> (case aa2 of |
401 A Gen => I |
404 A Gen => I |
402 | A _ => do_mtype_comp Leq xs M11 M21 |
405 | A _ => do_mtype_comp Leq xs M11 M21 |
403 | V x => do_mtype_comp Leq (x :: xs) M11 M21) |
406 | V x => do_mtype_comp Leq (x :: xs) M11 M21) |
414 | do_mtype_comp cmp _ M1 M2 _ = |
417 | do_mtype_comp cmp _ M1 M2 _ = |
415 raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")", |
418 raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")", |
416 [M1, M2], []) |
419 [M1, M2], []) |
417 |
420 |
418 fun add_mtype_comp cmp M1 M2 ((asgs, comps, clauses) : constraint_set) = |
421 fun add_mtype_comp cmp M1 M2 ((asgs, comps, clauses) : constraint_set) = |
419 (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^ |
422 (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^ |
420 string_for_comp_op cmp ^ " " ^ string_for_mtype M2); |
423 string_for_comp_op cmp ^ " " ^ string_for_mtype M2); |
421 case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of |
424 case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of |
422 NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) |
425 NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) |
423 | SOME (asgs, comps) => (asgs, comps, clauses)) |
426 | SOME (asgs, comps) => (asgs, comps, clauses)) |
424 |
427 |
425 val add_mtypes_equal = add_mtype_comp Eq |
428 val add_mtypes_equal = add_mtype_comp Eq |
426 val add_is_sub_mtype = add_mtype_comp Leq |
429 val add_is_sub_mtype = add_mtype_comp Leq |
427 |
430 |
428 fun do_notin_mtype_fv _ _ _ NONE = NONE |
431 fun do_notin_mtype_fv _ _ _ NONE = NONE |
429 | do_notin_mtype_fv Minus _ MAlpha accum = accum |
432 | do_notin_mtype_fv Minus _ MAlpha accum = accum |
430 | do_notin_mtype_fv Plus [] MAlpha _ = NONE |
433 | do_notin_mtype_fv Plus [] MAlpha _ = NONE |
431 | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, clauses)) = |
434 | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, clauses)) = |
432 SOME asgs |> do_assign (x, a) |> Option.map (rpair clauses) |
435 SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses) |
433 | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) = |
436 | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) = |
434 SOME (asgs, insert (op =) clause clauses) |
437 SOME (asgs, insert (op =) clause clauses) |
435 | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum = |
438 | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum = |
436 accum |> (if aa <> Gen andalso sn = Plus then |
439 accum |> (if aa <> Gen andalso sn = Plus then |
437 do_notin_mtype_fv Plus clause M1 |
440 do_notin_mtype_fv Plus clause M1 |
441 do_notin_mtype_fv Minus clause M1 |
444 do_notin_mtype_fv Minus clause M1 |
442 else |
445 else |
443 I) |
446 I) |
444 |> do_notin_mtype_fv sn clause M2 |
447 |> do_notin_mtype_fv sn clause M2 |
445 | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) accum = |
448 | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) accum = |
446 accum |> (case do_assign (x, Gen) (SOME clause) of |
449 accum |> (case add_assign_disjunct (x, Gen) (SOME clause) of |
447 NONE => I |
450 NONE => I |
448 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
451 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
449 |> do_notin_mtype_fv Minus clause M1 |
452 |> do_notin_mtype_fv Minus clause M1 |
450 |> do_notin_mtype_fv Plus clause M2 |
453 |> do_notin_mtype_fv Plus clause M2 |
451 | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum = |
454 | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum = |
452 accum |> (case fold (fn a => do_assign (x, a)) (* [New, Fls, Tru] FIXME *) [Fls] |
455 accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru] |
453 (SOME clause) of |
456 (SOME clause) of |
454 NONE => I |
457 NONE => I |
455 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
458 | SOME clause' => do_notin_mtype_fv Plus clause' M1) |
456 |> do_notin_mtype_fv Minus clause M2 |
459 |> do_notin_mtype_fv Minus clause M2 |
457 | do_notin_mtype_fv sn clause (MPair (M1, M2)) accum = |
460 | do_notin_mtype_fv sn clause (MPair (M1, M2)) accum = |