more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
authorwenzelm
Fri Mar 26 20:28:15 2010 +0100 (2010-03-26)
changeset 35975cef3c78ace0a
parent 35974 3a588b344749
child 35976 ea3d4691a8c6
more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Fri Mar 26 17:59:11 2010 +0100
     1.2 +++ b/src/Pure/sorts.ML	Fri Mar 26 20:28:15 2010 +0100
     1.3 @@ -254,18 +254,21 @@
     1.4            (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
     1.5        else err_conflict pp t NONE (c, Ss) (c, Ss'));
     1.6  
     1.7 -fun insert_ars pp algebra (t, ars) arities =
     1.8 +in
     1.9 +
    1.10 +fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
    1.11 +
    1.12 +fun insert_complete_ars pp algebra (t, ars) arities =
    1.13    let val ars' =
    1.14      Symtab.lookup_list arities t
    1.15 -    |> fold_rev (fold_rev (insert pp algebra t)) (map (complete algebra) ars)
    1.16 +    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
    1.17    in Symtab.update (t, ars') arities end;
    1.18  
    1.19 -in
    1.20 -
    1.21 -fun add_arities pp arg algebra = algebra |> map_arities (insert_ars pp algebra arg);
    1.22 +fun add_arities pp arg algebra =
    1.23 +  algebra |> map_arities (insert_complete_ars pp algebra arg);
    1.24  
    1.25  fun add_arities_table pp algebra =
    1.26 -  Symtab.fold (fn (t, ars) => insert_ars pp algebra (t, map snd ars));
    1.27 +  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
    1.28  
    1.29  end;
    1.30  
    1.31 @@ -291,11 +294,22 @@
    1.32    let
    1.33      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
    1.34        handle Graph.DUP c => err_dup_class c
    1.35 -          | Graph.CYCLES css => err_cyclic_classes pp css;
    1.36 +        | Graph.CYCLES css => err_cyclic_classes pp css;
    1.37      val algebra0 = make_algebra (classes', Symtab.empty);
    1.38 -    val arities' = Symtab.empty
    1.39 -      |> add_arities_table pp algebra0 arities1
    1.40 -      |> add_arities_table pp algebra0 arities2;
    1.41 +    val arities' =
    1.42 +      (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
    1.43 +        (true, true) => arities1
    1.44 +      | (true, false) =>  (*no completion*)
    1.45 +          (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
    1.46 +            if pointer_eq (ars1, ars2) then raise Symtab.SAME
    1.47 +            else insert_ars pp algebra0 t ars2 ars1)
    1.48 +      | (false, true) =>  (*unary completion*)
    1.49 +          Symtab.empty
    1.50 +          |> add_arities_table pp algebra0 arities1
    1.51 +      | (false, false) => (*binary completion*)
    1.52 +          Symtab.empty
    1.53 +          |> add_arities_table pp algebra0 arities1
    1.54 +          |> add_arities_table pp algebra0 arities2);
    1.55    in make_algebra (classes', arities') end;
    1.56  
    1.57