Merge remote-tracking branch 'origin/sail_new_tc' into experiments

5 files changed, 53 insertions, 9 deletions

diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 4f2c3ab0..66252d94 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -237,7 +237,7 @@ let doc_exp_ocaml, doc_let_ocaml =
           doc_op coloneq (doc_lexp_ocaml true le) (exp e)
         | LEXP_vector _ ->
           doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e)
-        | LEXP_vector_range _ ->
+        | LEXP_vector_range _ | LEXP_field _ ->
           doc_lexp_rwrite le e)
       else
        (match le_act with
diff --git a/src/type_check.ml b/src/type_check.ml
index 4507ec41..e37c2141 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1713,13 +1713,15 @@ let rec add_constraints constrs env =
    impossible, but we should be careful to never rule out a possible
    cast - match_typ and filter_casts implement this logic. It must be
    the case that if two types unify, then they match. *)
-let rec match_typ (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) =
-  match typ1, typ2 with
+let rec match_typ env typ1 typ2 =
+  let Typ_aux (typ1_aux, _) = Env.expand_synonyms env typ1 in
+  let Typ_aux (typ2_aux, _) = Env.expand_synonyms env typ2 in
+  match typ1_aux, typ2_aux with
   | Typ_wild, Typ_wild -> true
   | _, Typ_var kid2 -> true
   | Typ_id v1, Typ_id v2 when Id.compare v1 v2 = 0 -> true
   | Typ_id v1, Typ_id v2 when string_of_id v1 = "int" && string_of_id v2 = "nat" -> true
-  | Typ_tup typs1, Typ_tup typs2 -> List.for_all2 match_typ typs1 typs2
+  | Typ_tup typs1, Typ_tup typs2 -> List.for_all2 (match_typ env) typs1 typs2
   | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" && string_of_id f = "atom" -> true
   | Typ_id v, Typ_app (f, _) when string_of_id v = "int" &&  string_of_id f = "atom" -> true
   | Typ_id v, Typ_app (f, _) when string_of_id v = "nat" &&  string_of_id f = "range" -> true
@@ -1738,7 +1740,7 @@ let rec filter_casts env from_typ to_typ casts =
        let (quant, cast_typ) = Env.get_val_spec cast env in
        match cast_typ with
        | Typ_aux (Typ_fn (cast_from_typ, cast_to_typ, _), _)
-            when match_typ from_typ cast_from_typ && match_typ to_typ cast_to_typ ->
+            when match_typ env from_typ cast_from_typ && match_typ env to_typ cast_to_typ ->
           typ_print ("Considering cast " ^ string_of_typ cast_typ ^ " for " ^ string_of_typ from_typ ^ " to " ^ string_of_typ to_typ);
           cast :: filter_casts env from_typ to_typ casts
        | _ -> filter_casts env from_typ to_typ casts
@@ -2100,7 +2102,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
      annot_pat (P_vector_concat (inferred_pat :: inferred_pats)) (lvector_typ env len vtyp), env
   | P_as (pat, id) ->
      let (typed_pat, env) = infer_pat env pat in
-     annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), env
+     annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env
   | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat)
 
 and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) =
@@ -2368,6 +2370,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        match is_range (typ_of inferred_f), is_range (typ_of inferred_t) with
        | None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range")
        | _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range")
+       (* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) ->
+          let loop_vtyp = exist_typ (fun e -> nc_and (nc_lteq l1 (nvar e)) (nc_lteq (nvar e) u2)) (fun e -> atom_typ (nvar e)) in
+          let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in
+          annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *)
        | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) ->
           let kid = mk_kid ("loop_" ^ string_of_id v) in
           if KBindings.mem kid (Env.get_typ_vars env)
diff --git a/test/typecheck/pass/as_pattern.sail b/test/typecheck/pass/as_pattern.sail
new file mode 100644
index 00000000..a1cd9461
--- /dev/null
+++ b/test/typecheck/pass/as_pattern.sail
@@ -0,0 +1,7 @@
+
+val int -> int effect pure test
+
+function test ((int) _ as x) =
+{
+  x
+}
diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail
new file mode 100644
index 00000000..72a7e9d0
--- /dev/null
+++ b/test/typecheck/pass/vector_synonym_cast.sail
@@ -0,0 +1,8 @@
+
+typedef vecsyn = vector<0,1,dec,bit>
+
+val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure test_cast
+
+val vector<1,1,dec,bit> -> vecsyn effect pure test
+
+function test x = x
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index c4faad7e..8659e60e 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -101,17 +101,20 @@ function test_lem {
     do
 	if $SAILDIR/sail -lem $DIR/$1/$i 2> /dev/null
 	then
+	    green "generated lem for $1/$i" "pass"
+
 	    mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/
 	    mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/
 	    if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null
 	    then
-		green "generated lem for $1/$i" "pass"
+		green "typechecking lem for $1/$i" "pass"
 	    else
-		red "generated lem for $1/$i" "failed to typecheck lem"
+		red "typechecking lem for $1/$i" "fail"
 	    fi
 	else
-	    red "generated lem for $1/$i" "failed to generate lem"
+	    red "generated lem for $1/$i" "fail"
+	    red "typechecking lem for $1/$i" "fail"
 	fi
     done
 }
@@ -124,4 +127,24 @@ test_lem rtpass
 
 finish_suite "Lem generation 2"
 
+function test_ocaml {
+    for i in `ls $DIR/pass/`;
+    do
+	if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null
+	then
+	    green "generated ocaml for $1/$i" "pass"
+	else
+	    red "generated ocaml for $1/$i" "fail"
+	fi
+    done
+}
+
+test_ocaml pass
+
+finish_suite "Ocaml generation 1"
+
+test_ocaml rtpass
+
+finish_suite "Ocaml generation 2"
+
 printf "</testsuites>\n" >> $DIR/tests.xml