From a56ddf5b864c23be7c47dc84882b436b3a4f7473 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 1 Aug 2017 16:43:46 +0100 Subject: Added more patterns to ast_util and improved type checking of patterns --- src/ast_util.ml | 3 +++ src/type_check.ml | 15 +++++++++++---- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/ast_util.ml b/src/ast_util.ml index 6a97f6bf..ade13fe3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -311,6 +311,9 @@ and string_of_pat (P_aux (pat, l)) = | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")" | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2 | P_list pats -> "[||" ^ string_of_list "," string_of_pat pats ^ "||]" + | P_vector_concat pats -> string_of_list " : " string_of_pat pats + | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" + | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id | _ -> "PAT" and string_of_lexp (LEXP_aux (lexp, _)) = match lexp with diff --git a/src/type_check.ml b/src/type_check.ml index 90e1ad8c..0a2c0dcb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1943,13 +1943,13 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = annot_pat (P_lit lit) (infer_lit env lit), env | P_vector (pat :: pats) -> let fold_pats (pats, env) pat = - let inferred_pat, env = infer_pat env pat in - pats @ [inferred_pat], env + let typed_pat, env = bind_pat env pat bit_typ in + pats @ [typed_pat], env in - let ((inferred_pat :: inferred_pats) as pats), env = + let ((typed_pat :: typed_pats) as pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in let len = nexp_simp (nconstant (List.length pats)) in - let etyp = pat_typ_of inferred_pat in + let etyp = pat_typ_of typed_pat in List.map (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; annot_pat (P_vector pats) (lvector_typ env len etyp), env | P_vector_concat (pat :: pats) -> @@ -1966,6 +1966,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let len = nexp_simp (List.fold_left fold_len len inferred_pats) in 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 | _ -> 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) = @@ -2239,6 +2242,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 checked_body = crule check_exp (Env.add_local v (Immutable, range_typ l1 u2) env) body unit_typ in annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ -- cgit v1.2.3 From 3695b589eaf0bdf3cdb78cf0b26ba5f70f314dd3 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 1 Aug 2017 17:38:17 +0100 Subject: Fixed a bug where as patterns weren't binding their variable correctly --- src/type_check.ml | 2 +- test/typecheck/pass/as_pattern.sail | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 test/typecheck/pass/as_pattern.sail diff --git a/src/type_check.ml b/src/type_check.ml index 0a2c0dcb..87f65dcc 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1968,7 +1968,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) = 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 +} -- cgit v1.2.3 From ec9bfb950087c430ba96387c5b83dc88397e06b2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 1 Aug 2017 18:04:08 +0100 Subject: Fixed a bug where type_synonyms were not being expanded properly when considering possible casts --- src/type_check.ml | 10 ++++++---- test/typecheck/pass/vector_synonym_cast.sail | 8 ++++++++ 2 files changed, 14 insertions(+), 4 deletions(-) create mode 100644 test/typecheck/pass/vector_synonym_cast.sail diff --git a/src/type_check.ml b/src/type_check.ml index 87f65dcc..eb6eab09 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1587,13 +1587,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 @@ -1612,7 +1614,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 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 -- cgit v1.2.3 From 2dfc638ac88f869a3bf318914cd2060ea363d89a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 1 Aug 2017 18:15:21 +0100 Subject: Added ocaml generation to run_tests.sh --- test/typecheck/run_tests.sh | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) 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 "\n" >> $DIR/tests.xml -- cgit v1.2.3 From b63df3a5806c33401f03a8e9eb33fc3291872105 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 1 Aug 2017 18:41:34 +0100 Subject: Add missing lexp case to Ocaml pretty-printer --- src/pretty_print_ocaml.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3