Full power.sail now type checking and generating Lem.

2 files changed, 12 insertions, 10 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 714112ad..b55bf4b9 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -31,6 +31,7 @@ let pp_format_id (Id_aux(i,_)) =
 let pp_format_var (Kid_aux(Var v,_)) = v
 
 let rec pp_format_l_lem = function
+  | _ -> "Unknown" 
   | Parse_ast.Unknown -> "Unknown"
   | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)"
   | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
@@ -258,7 +259,7 @@ let pp_format_tag = function
 
 let rec pp_format_nes nes = 
   "[" ^ 
-  (list_format "; "
+  (*(list_format "; "
      (fun ne -> match ne with
        | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
        | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
@@ -272,7 +273,7 @@ let rec pp_format_nes nes =
        | BranchCons(_,nes_b) ->
          "(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"
      )
-     nes) ^ "]"
+     nes) ^*) "]"
 
 let pp_format_annot = function
   | NoTyp -> "Nothing"
diff --git a/src/type_check.ml b/src/type_check.ml
index 7c6ad921..8bdede1d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1375,19 +1375,20 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	    | (Tapp("range",[TA_nexp base_e1;TA_nexp range_e1]),
 	       Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])) -> base_e1,range_e1,base_e2,range_e2
 	    | _ -> base_e1,range_e1,base_e2,range_e2 in
+          let len = new_n() in
 	  let cs_t,res_t = match ord.order with
 	    | Oinc ->  ([LtEq((Expr l),base,base_e1);
 			 LtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)});
-			 LtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,rise)})],
-			{t=Tapp("vector",[TA_nexp base_e1;
-					  TA_nexp {nexp = Nadd({nexp = Nadd({nexp=Nadd(base_e2,range_e2)},{nexp = Nconst one})},
-							       {nexp=Nneg base_e1})};TA_ord ord;TA_typ t])})
+			 LtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,rise)});
+                         LtEq((Expr l),len, {nexp =Nadd({nexp= Nadd({nexp= Nadd(base_e2,range_e2)},{nexp= Nconst one})},
+                                                        {nexp = Nneg({nexp = Nadd(base_e1,range_e1)})})});],
+			{t=Tapp("vector",[TA_nexp base_e1;TA_nexp len;TA_ord ord;TA_typ t])})
 	    | Odec -> ([GtEq((Expr l),base,base_e1);
 			GtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)});
-			GtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,{nexp=Nneg rise})})],
-		       {t=Tapp("vector",[TA_nexp {nexp=Nadd(base_e1,range_e1)};
-					 TA_nexp {nexp=Nadd({nexp=Nadd(base_e1,range_e1)},{nexp=Nneg{nexp=Nadd(base_e2,range_e2)}})};
-					 TA_ord ord; TA_typ t])})
+			GtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,{nexp=Nneg rise})});                         
+                        LtEq((Expr l),len, {nexp =Nadd({nexp= Nadd({nexp= Nadd(base_e2,range_e2)},{nexp= Nconst one})},
+                                                        {nexp = Nneg({nexp = Nadd(base_e1,range_e1)})})});],
+                       {t=Tapp("vector",[TA_nexp {nexp=Nadd(base_e1,range_e1)};TA_nexp len;TA_ord ord; TA_typ t])})
 	    | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order")
 	  in
 	  let cs = cs_t@cs@cs1@cs2 in