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(-) (limited to 'src') 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') 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) = -- 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 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'src') 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 -- 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(-) (limited to 'src') 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