]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/listAvs.ml
an optimization was inserted
[helm.git] / helm / ocaml / mathql / listAvs.ml
index e25fc61c730975236bd11137672a97def63308d5..591dc3fe296c41dd06054220357ef9d51afecbc8 100644 (file)
@@ -133,8 +133,13 @@ let rec union s1 s2 =
 let grp_union = union
 
 let prod g1 g2 =
-   let aux a = set_iter (fun h -> [union a h]) g2 in
-   set_iter aux g1      
+   match g1, g2 with
+      | [], [] -> []
+      | _, []  -> g1
+      | [], _  -> g2
+      | _, _   ->
+         let aux a = set_iter (fun h -> [union a h]) g2 in
+         set_iter aux g1      
 
 let rec d_union s1 s2 =
    match s1, s2 with
@@ -177,13 +182,13 @@ let rec diff s1 s2 =
       | (r1, _) :: _, (r2, _) :: t2 when r1 > r2  -> diff s1 t2
       | _ :: t1, _ :: t2                          -> diff t1 t2
 
-(* concatenation ************************************************************)
-
-let append v1 v2 = v1 @ v2
-
 (* peeking ******************************************************************)
 
 let peek = function
    | []           -> Empty
    | [s, gl]      -> Single (s, gl)
    | (s, gl) :: _ -> Many (s, gl)
+
+(* optimization *************************************************************)
+
+let optimize = List.rev