Fixes stack overflow in sail caused by list append in type_internal.ml.

Also makes the check function in type_check tail recursive.

2 files changed, 8 insertions, 7 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index c4119281..f090ef58 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2521,9 +2521,10 @@ let check_def envs def =
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)
-let rec check envs (Defs defs) = 
- match defs with
-   | [] -> (Defs []),envs
-   | def::defs -> let (def, envs) = check_def envs def in
-                  let (Defs defs, envs) = check envs (Defs defs) in
-                  (Defs (def::defs)), envs
+let check envs (Defs defs) =
+  let rec check' envs (Defs defs) k =
+    match defs with
+    | [] -> k ((Defs []), envs)
+    | def::defs -> let (def, envs) = check_def envs def in
+                   check' envs (Defs defs) (fun (Defs defs, envs) -> Defs (def::defs), envs) in
+  check' envs (Defs defs) (fun x -> x)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index ad7a772e..2eaef407 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -3264,7 +3264,7 @@ let merge_bounds b1 b2 =
                   if nexp_eq n1 n2 then b1 else VR_range(v,[Eq((Patt Parse_ast.Unknown),n1,n2)])
                 | VR_eq(v,n),VR_range(_,ranges) | 
                   VR_range(v,ranges),VR_eq(_,n) -> VR_range(v,(Eq((Patt Parse_ast.Unknown),n,n))::ranges)
-                | VR_range(v,ranges1),VR_range(_,ranges2) -> VR_range(v,ranges1@ranges2)
+                | VR_range(v,ranges1),VR_range(_,ranges2) -> VR_range(v, List.rev_append (List.rev ranges1) ranges2)
                 | VR_vec_eq(v,n1),VR_vec_eq(_,n2) ->
                   if nexp_eq n1 n2 then b1 else VR_vec_r(v,[Eq((Patt Parse_ast.Unknown),n1,n2)])
                 | VR_vec_eq(v,n),VR_vec_r(_,ranges) |