Stop overzealously looking for constructors, only when the type suggests to

3 files changed, 88 insertions, 8 deletions

diff --git a/src/test/power.sail b/src/test/power.sail
index 4305c099..5f4783ce 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -427,6 +427,20 @@ function clause execute (Bclr (BO, BI, BH, LK)) =
     if LK then LR := CIA + 4 else ()
   }
 
+union ast member (bit[7]) Sc
+
+function clause decode (0b010001 :
+(bit[5]) _ :
+(bit[5]) _ :
+(bit[4]) _ :
+(bit[7]) LEV :
+(bit[3]) _ :
+0b1 :
+(bit[1]) _ as instr) =
+  Sc (LEV)
+
+function clause execute (Sc (LEV)) = ()
+
 union ast member (bit[5], bit[5], bit[16]) Lwz
 
 function clause decode (0b100000 :
@@ -538,9 +552,9 @@ function clause execute (Lswi (RT, RA, NB)) =
   {
     (bit[64]) EA := 0;
     if RA == 0 then EA := 0 else EA := GPR[RA];
-    (range<0, 32> ) r := 0;
+    ([|32|]) r := 0;
     r := RT - 1;
-    (range<0, 32> ) size := if NB == 0 then 32 else NB;
+    ([|32|]) size := if NB == 0 then 32 else NB;
     (bit[256]) membuffer := MEMr (EA,size);
     j := 0;
     i := 32;
@@ -548,7 +562,7 @@ function clause execute (Lswi (RT, RA, NB)) =
     {
       if i == 32
       then {
-        r := (range<0, 32> ) (r + 1) mod 32;
+        r := ([|32|]) (r + 1) mod 32;
         GPR[r] := 0
       }
       else ();
@@ -584,6 +598,24 @@ function clause execute (Addis (RT, RA, SI)) =
   then GPR[RT] := EXTS (SI : 0b0000000000000000)
   else GPR[RT] := GPR[RA] + EXTS (SI : 0b0000000000000000)
 
+union ast member (bit[5], bit[5], bit[5], bit, bit) Add
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[5]) RB :
+[OE] :
+0b100001010 :
+[Rc] as instr) =
+  Add (RT,RA,RB,OE,Rc)
+
+function clause execute (Add (RT, RA, RB, OE, Rc)) =
+  {
+    temp := GPR[RA] + GPR[RB];
+    GPR[RT] := temp;
+    if Rc then set_overflow_cr0 (temp) else ()
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit, bit) Subf
 
 function clause decode (0b011111 :
@@ -602,6 +634,26 @@ function clause execute (Subf (RT, RA, RB, OE, Rc)) =
     if Rc then set_overflow_cr0 (temp) else ()
   }
 
+union ast member (bit[5], bit[5], bit[16]) Addic
+
+function clause decode (0b001100 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[16]) SI as instr) =
+  Addic (RT,RA,SI)
+
+function clause execute (Addic (RT, RA, SI)) = GPR[RT] := GPR[RA] + EXTS (SI)
+
+union ast member (bit[5], bit[5], bit[16]) Addic
+
+function clause decode (0b001101 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[16]) SI as instr) =
+  Addic (RT,RA,SI)
+
+function clause execute (Addic (RT, RA, SI)) = GPR[RT] := GPR[RA] + EXTS (SI)
+
 union ast member (bit[5], bit[5], bit, bit) Neg
 
 function clause decode (0b011111 :
@@ -638,6 +690,26 @@ function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
     if Rc then set_overflow_cr0 (temp) else ()
   }
 
+union ast member (bit[3], bit, bit[5], bit[16]) Cmpi
+
+function clause decode (0b001011 :
+(bit[3]) BF :
+(bit[1]) _ :
+[L] :
+(bit[5]) RA :
+(bit[16]) SI as instr) =
+  Cmpi (BF,L,RA,SI)
+
+function clause execute (Cmpi (BF, L, RA, SI)) =
+  {
+    (bit[64]) a := 0;
+    if L == 0 then a := EXTS ((GPR[RA])[32 .. 63]) else a := GPR[RA];
+    if a < EXTS (SI)
+    then c := 0b100
+    else if a > EXTS (SI) then c := 0b010 else c := 0b001;
+    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
+  }
+
 union ast member (bit[3], bit, bit[5], bit[5]) Cmp
 
 function clause decode (0b011111 :
diff --git a/src/type_check.ml b/src/type_check.ml
index bfb59b3f..884e90c6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -237,18 +237,24 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
       (P_aux(P_typ(typ,pat'),(l,Base(([],t),Emp_local,[],pure_e))),env,cs@constraints,t)
     | P_id id -> 
       let i = id_to_string id in
+      let default = let tannot = Base(([],expect_t),emp_tag,cs,pure_e) in
+		    (P_aux(p,(l,tannot)),Envmap.from_list [(i,tannot)],cs,expect_t) in
       (match Envmap.apply t_env i with
 	| Some(Base((params,t),Constructor,cs,ef)) ->
 	  let t,cs,ef = subst params t cs ef in
           (match t.t with
             | Tfn({t = Tid "unit"},t',IP_none,ef) -> 
-	      let tp,cp = type_consistent (Expr l) d_env t' expect_t in
-	      (P_aux(P_app(id,[]),(l,(Base(([],t),Constructor,[],pure_e)))),Envmap.empty,cs@cp,tp)
+	      if conforms_to_t d_env false false t' expect_t 
+	      then
+		let tp,cp = type_consistent (Expr l) d_env t' expect_t in
+		(P_aux(P_app(id,[]),(l,(Base(([],t),Constructor,[],pure_e)))),Envmap.empty,cs@cp,tp)
+	      else default
             | Tfn(t1,t',IP_none,e) -> 
-              typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
+	      if conforms_to_t d_env false false t' expect_t
+	      then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
+	      else default
             | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
-	| _ -> let tannot = Base(([],expect_t),emp_tag,cs,pure_e) in
-	       (P_aux(p,(l,tannot)),Envmap.from_list [(id_to_string id,tannot)],cs,expect_t))
+	| _ -> default)
     | P_app(id,pats) -> 
       let i = id_to_string id in
       (match Envmap.apply t_env i with
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 63a18106..90eaea91 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -171,6 +171,8 @@ val check_tannot : Parse_ast.l -> tannot -> nexp_range list -> effect -> tannot
 
 val nexp_eq : nexp -> nexp -> bool
 
+val conforms_to_t : def_envs -> bool -> bool -> t -> t -> bool
+
 (* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where
    t1 and t2 are both enum types and t1 is contained within the range of t2: i.e.
    enum 2 5 is consistent with enum 0 10, but not vice versa.