Added basic support for pure record definitions and functional record

updates to the new typechecker

2 files changed, 66 insertions, 0 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 28169c41..9797ac25 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1918,6 +1918,37 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           annot_exp (E_list checked_xs) typ
        | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
      end
+  | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ ->
+     (* TODO: this could also infer exp - also fix code duplication with E_record below *)
+     let checked_exp = crule check_exp env exp typ in
+     let rectyp_id = match Env.expand_synonyms env typ with
+       | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
+          rectyp_id
+       | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
+     in
+     let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
+       let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+       let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+       let field_typ' = subst_unifiers unifiers field_typ in
+       let checked_exp = crule check_exp env exp field_typ' in
+       FE_aux (FE_Fexp (field, checked_exp), (l, None))
+     in
+     annot_exp (E_record_update (checked_exp, FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ
+  | E_record (FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ ->
+     (* TODO: check record fields are total *)
+     let rectyp_id = match Env.expand_synonyms env typ with
+       | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
+          rectyp_id
+       | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
+     in
+     let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
+       let (typq, Typ_aux (Typ_fn (rectyp_q, field_typ, _), _)) = Env.get_accessor rectyp_id field env in
+       let unifiers, _, _ (* FIXME *) = try unify l env rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+       let field_typ' = subst_unifiers unifiers field_typ in
+       let checked_exp = crule check_exp env exp field_typ' in
+       FE_aux (FE_Fexp (field, checked_exp), (l, None))
+     in
+     annot_exp (E_record (FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
@@ -2773,6 +2804,15 @@ and propagate_exp_effect_aux = function
      let p_cases = List.map propagate_pexp_effect cases in
      let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
      E_case (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
+  | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, _))) ->
+     let p_exp = propagate_exp_effect exp in
+     let p_fexps = List.map propagate_fexp_effect fexps in
+     E_record_update (p_exp, FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))),
+     List.fold_left union_effects no_effect (effect_of p_exp :: List.map snd p_fexps)
+  | E_record (FES_aux (FES_Fexps (fexps, flag), (l, _))) ->
+     let p_fexps = List.map propagate_fexp_effect fexps in
+     E_record (FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))),
+     List.fold_left union_effects no_effect (List.map snd p_fexps)
   | E_try (exp, cases) ->
      let p_exp = propagate_exp_effect exp in
      let p_cases = List.map propagate_pexp_effect cases in
@@ -2821,6 +2861,10 @@ and propagate_exp_effect_aux = function
   | exp_aux -> typ_error Parse_ast.Unknown ("Unimplemented: Cannot propagate effect in expression "
                                             ^ string_of_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))))
 
+and propagate_fexp_effect (FE_aux (FE_Fexp (id, exp), (l, _))) =
+  let p_exp = propagate_exp_effect exp in
+  FE_aux (FE_Fexp (id, p_exp), (l, None)), effect_of p_exp
+
 and propagate_pexp_effect = function
   | Pat_aux (Pat_exp (pat, exp), (l, annot)) ->
      begin
diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail
new file mode 100644
index 00000000..c7bc373a
--- /dev/null
+++ b/test/typecheck/pass/pure_record.sail
@@ -0,0 +1,22 @@
+default Order dec
+
+typedef State = const struct forall Type 'a. {
+  vector<0, 1, dec, 'a> N;
+  vector<0, 1, dec, bit> Z;
+}
+
+let (State<bit>) myStateM = {
+  (State<bit>) r := undefined;
+  r.N := 0b1;
+  r.Z := 0b1;
+  r
+}
+
+let (State<bit>) myState = { N = 0b1; Z = 0b1 }
+
+val unit -> unit effect {undef} test
+
+function test () = {
+  (State<bit>) myState2 := { N = undefined; Z = 0b1 };
+  (State<bit>) myState3 := { myState2 with N = 0b0 }
+}