struct/record type checking

3 files changed, 171 insertions, 9 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 623158c9..9be7a323 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -218,7 +218,7 @@ let rec check_pattern envs (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap)
 	| Some(Some((params,t),tag,constraints,eft)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a constructor"))
     | P_record(fpats,_) -> 
       (match (fields_to_rec fpats d_env.rec_env) with
-	| None -> typ_error l ("No record exists with the listed fields")
+	| None -> typ_error l ("No struct exists with the listed fields")
 	| Some(id,typ_pats) ->
 	  let pat_checks = 
 	    List.map (fun (tan,id,l,pat) -> 
@@ -640,9 +640,123 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let (i', ti, _,cs_i,ef_i) = check_exp envs item_t i in
       let (t',cs',e') = type_coerce l d_env lt (E_aux(E_cons(ls',i'),(l,Some(([],lt),Emp,cs@cs_i,(union_effects ef ef_i))))) expect_t in
       (e',t',t_env,cs@cs'@cs_i,(union_effects ef ef_i))
-    | E_record(fexps) -> (E_aux(e,(l,annot)),expect_t,t_env,[],pure_e)
-    | E_record_update(exp,fexps) -> (E_aux(e,(l,annot)),expect_t,t_env,[],pure_e)
-    | E_field(exp,id) -> (E_aux(e,(l,annot)),expect_t,t_env,[],pure_e)
+    | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> 
+      let u = match (get_abbrev d_env expect_t) with
+	| Some(t,cs,ef) -> t
+	| None -> expect_t in
+      (match u.t with
+	| Tid(n) ->
+	  (match lookup_record_typ n d_env.rec_env with 
+	    | None -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct")
+	    | Some(((i,Record,fields) as r)) -> 
+	      if (List.length fexps = List.length fields) 
+	      then let fexps,cons,ef =
+		     List.fold_right 
+		       (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
+			 let i = id_to_string id in
+			 match lookup_field_type i r with
+			   | None -> 
+			     typ_error l ("Expected a struct of type " ^ n ^ ", which should not have a field " ^ i)
+			   | Some((params,et),tag,cs,ef) ->
+			     let (e,t',_,c,ef) = check_exp envs et exp in
+			     (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+		       fexps ([],[],pure_e) in
+		   E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,cons,ef))),expect_t,t_env,cons,ef
+	      else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields")
+	    | Some(i,Register,fields) -> typ_error l ("Expected a value with register type, found a struct"))
+	| Tuvar _ ->
+	  let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
+	  (match lookup_record_fields field_names d_env.rec_env with
+	    | None -> typ_error l "No struct type matches the set of fields given"
+	    | Some(((i,Record,fields) as r)) ->
+	      let fexps,cons,ef =
+		List.fold_right 
+		  (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
+		    let i = id_to_string id in
+		    match lookup_field_type i r with
+		      | None -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+		      | Some((params,et),tag,cs,ef) ->
+			let (e,t',_,c,ef) = check_exp envs et exp in
+			(FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+		  fexps ([],[],pure_e) in
+	      expect_t.t <- Tid i;
+	      E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,cons,ef))),expect_t,t_env,cons,ef
+	    | Some(i,Register,fields) -> typ_error l "Expected a value with register type, found a struct")
+	| _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct"))
+    | E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) -> 
+      let (e',t',_,c,ef) = check_exp envs expect_t exp in
+      (match t'.t with
+	| Tid i ->
+	  (match lookup_record_typ i d_env.rec_env with
+	    | None -> typ_error l ("Expected a struct for this update, instead found an expression with type " ^ i)
+	    | Some((i,Register,fields)) ->
+	      typ_error l "Expected a struct for this update, instead found a register"
+	    | Some(((i,Record,fields) as r)) ->
+	      if (List.length fexps <= List.length fields) 
+	      then let fexps,cons,ef =
+		     List.fold_right 
+		       (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
+			 let fi = id_to_string id in
+			 match lookup_field_type fi r with
+			   | None -> 
+			     typ_error l ("Expected a struct with type " ^ i ^ ", which does not have a field " ^ fi)
+			   | Some((params,et),tag,cs,ef) ->
+			     let (e,t',_,c,ef) = check_exp envs et exp in
+			     (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+		       fexps ([],[],pure_e) in
+		   E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,cons,ef))),expect_t,t_env,cons,ef
+	      else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes"))
+	| Tuvar _ ->
+	  let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
+	  (match lookup_possible_records field_names d_env.rec_env with
+	    | [] -> typ_error l "No struct matches the set of fields given for this struct update"
+	    | [(((i,Record,fields) as r))] ->
+	      let fexps,cons,ef =
+		List.fold_right 
+		  (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) (fexps,cons,ef') ->
+		    let i = id_to_string id in
+		    match lookup_field_type i r with
+		      | None -> raise (Reporting_basic.err_unreachable l "field_match didn't have a full match")
+		      | Some((params,et),tag,cs,ef) ->
+			let (e,t',_,c,ef) = check_exp envs et exp in
+			(FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef'))
+		  fexps ([],[],pure_e) in
+	      expect_t.t <- Tid i;
+	      E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,cons,ef))),expect_t,t_env,cons,ef
+	    | [(i,Register,fields)] -> typ_error l "Expected a value with register type, found a struct"
+	    | records -> typ_error l "Multiple structs contain this set of fields, try adding a cast to disambiguate")
+	| _ -> typ_error l ("Expected a struct to update but found an expression of type " ^ t_to_string expect_t))
+    | E_field(exp,id) ->
+      let (e',t',_,c,ef) = check_exp envs (new_t()) exp in
+      (match t'.t with
+	| Tid i ->
+	  (match lookup_record_typ i d_env.rec_env with
+	    | None -> typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)
+	    | Some(((i,rec_kind,fields) as r)) ->
+	      let fi = id_to_string id in
+	      (match lookup_field_type fi r with
+		| None -> 
+		  typ_error l ("Type " ^ i ^ " does not have a field " ^ fi)
+		| Some((params,et),tag,cs,ef) ->
+		  let et,cs,ef = subst params et cs ef in
+		  let (et',c',acc) = type_coerce l d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+		  (acc,et',t_env,cs@c',ef)))
+	| Tuvar _ ->
+	  let fi = id_to_string id in
+	  (match lookup_possible_records [fi] d_env.rec_env with
+	    | [] -> typ_error l ("No struct has a field " ^ fi)
+	    | [(((i,rkind,fields) as r))] ->
+	      let fi = id_to_string id in
+	      (match lookup_field_type fi r with
+		| None -> 
+		  raise (Reporting_basic.err_unreachable l "lookup_possible_records returned a record that didn't include the field")
+		| Some((params,et),tag,cs,ef) ->
+		  let et,cs,ef = subst params et cs ef in
+		  let (et',c',acc) = type_coerce l d_env et (E_aux(E_field(e',id),(l,Some(([],et),tag,cs,ef)))) expect_t in
+		  t'.t <- Tid i;
+		  (acc,et',t_env,cs@c',ef))
+	    | records -> typ_error l ("Multiple structs contain field " ^ fi ^ ", try adding a cast to disambiguate"))
+	| _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t'))
     | E_case(exp,pexps) ->
       let check_t = new_t() in
       let (e',t',_,cs,ef) = check_exp envs check_t exp in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 6c0b3e9d..bb9801a3 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -78,20 +78,28 @@ type tannot = ((t_params * t) * tag * nexp_range list * effect) option
 type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
+type rec_env = (string * rec_kind * ((string * tannot) list))
 type def_envs = { 
   k_env: kind emap; 
   abbrevs: tannot emap; 
   namesch : tannot emap; 
   enum_env : (string list) emap; 
-  rec_env : (string * rec_kind * ((string * tannot) list)) list;
+  rec_env : rec_env list;
  }  
 
 type exp = tannot Ast.exp
 
+let rec effect_remove_dups = function
+  | [] -> []
+  | (BE_aux(be,l))::es -> 
+    if (List.exists (fun (BE_aux(be',_)) -> be = be') es)
+    then effect_remove_dups es
+    else (BE_aux(be,l))::(effect_remove_dups es)
+      
 let add_effect e ef =
   match ef.effect with
   | Evar s -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "add_effect given var instead of uvar")
-  | Eset bases -> ef.effect <- Eset (e::bases); ef
+  | Eset bases -> {effect = Eset (effect_remove_dups (e::bases))}
   | Euvar _ -> ef.effect <- Eset [e]; ef
 
 let union_effects e1 e2 =
@@ -99,7 +107,41 @@ let union_effects e1 e2 =
   | Evar s,_ | _,Evar s -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "union_effects given var(s) instead of uvar(s)")
   | Euvar _,_ -> e1.effect <- e2.effect; e2
   | _,Euvar _ -> e2.effect <- e1.effect; e2
-  | Eset b1, Eset b2 -> e1.effect <- Eset (b1@b2); e2.effect <- e1.effect; e2  
+  | Eset b1, Eset b2 -> {effect= Eset (effect_remove_dups (b1@b2))}  
+
+let rec lookup_record_typ (typ : string) (env : rec_env list) : rec_env option =
+  match env with
+    | [] -> None
+    | ((id,_,_) as r)::env -> 
+      if typ = id then Some(r) else lookup_record_typ typ env
+
+let rec fields_match f1 f2 =
+  match f1 with
+    | [] -> true
+    | f::fs -> (List.mem_assoc f f2) && fields_match fs f2
+
+let rec lookup_record_fields (fields : string list) (env : rec_env list) : rec_env option =
+  match env with
+    | [] -> None
+    | ((id,r,fs) as re)::env ->
+      if ((List.length fields) = (List.length fs)) &&
+	 (fields_match fields fs) then
+	Some re
+      else lookup_record_fields fields env
+
+let rec lookup_possible_records (fields : string list) (env : rec_env list) : rec_env list =
+  match env with
+    | [] -> []
+    | ((id,r,fs) as re)::env ->
+      if (((List.length fields) <= (List.length fs)) &&
+	  (fields_match fields fs))
+      then re::(lookup_possible_records fields env)
+      else lookup_possible_records fields env
+
+let lookup_field_type (field: string) ((id,r_kind,fields) : rec_env) : tannot =
+  if List.mem_assoc field fields
+  then List.assoc field fields
+  else None
 
 let v_count = ref 0
 let t_count = ref 0
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 161a0d74..13cb56ea 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -73,16 +73,22 @@ type tannot = ((t_params * t) * tag * nexp_range list * effect) option
 type 'a emap = 'a Envmap.t
 
 type rec_kind = Record | Register
+type rec_env = (string * rec_kind * ((string * tannot) list))
 type def_envs = { 
   k_env: kind emap; 
   abbrevs: tannot emap; 
   namesch : tannot emap; 
   enum_env : (string list) emap; 
-  rec_env : (string * rec_kind * ((string * tannot) list)) list;
+  rec_env : rec_env list;
  }
 
 type exp = tannot Ast.exp
 
+val lookup_record_typ : string -> rec_env list -> rec_env option
+val lookup_record_fields : string list -> rec_env list -> rec_env option
+val lookup_possible_records : string list -> rec_env list -> rec_env list
+val lookup_field_type : string -> rec_env -> tannot
+
 val add_effect : Ast.base_effect -> effect -> effect
 val union_effects : effect -> effect -> effect
 
@@ -104,7 +110,7 @@ val new_o : unit -> order
 val new_e : unit -> effect
 
 val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect
-
+val get_abbrev : def_envs -> t -> (t * nexp_range list * effect) option
 
 (* 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.