From ff469898d5f4e1c9b3cd6692f99dd1e1f2e700bc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 11 Aug 2017 10:54:15 +0100
Subject: Make type checking just clever enough to solve 8*n = constant

---
 src/type_check.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index bd2db570..c4f700b0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1320,6 +1320,13 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
            match nexp_aux2 with
            | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1a, n2a), Parse_ast.Unknown)) ->
               unify_nexps l env goals n1b n2b
+           | Nexp_constant c2 ->
+              begin
+                match n1a with
+                | Nexp_aux (Nexp_constant c1,_) when c2 mod c1 = 0 ->
+                   unify_nexps l env goals n1b (mk_nexp (Nexp_constant (c2 / c1)))
+                | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
+              end
            | _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
          end
        else if KidSet.is_empty (nexp_frees n1b)
-- 
cgit v1.2.3