fix base type checking around structs and struct members

backend/cn/check.ml

@@ -9,6 +9,7 @@ module RT = ReturnTypes
 module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
 module TE = TypeErrors
+module IdSet = Set.Make(Id)
 module SymSet = Set.Make(Sym)
 module SymMap = Map.Make(Sym)
 module S = Solver
@@ -201,26 +202,18 @@ let rec check_mem_value (loc : loc) ~(expect:BT.t) (mem : mem_value) : (lvt) m =
 
 and check_struct (loc : loc) (tag : Sym.t) 
                  (member_values : (Id.t * mem_value) list) : (lvt) m =
-  (* might have to make sure the fields are ordered in the same way as
-     in the struct declaration *)
   let@ layout = get_struct_decl loc tag in
-  let rec check fields spec =
-    match fields, spec with
-    | ((member, mv) :: fields), ((smember, sct) :: spec) 
-         when Id.equal member smember ->
-       let@ member_lvt = check_mem_value loc ~expect:(BT.of_sct sct) mv in
-       let@ member_its = check fields spec in
-       return ((member, member_lvt) :: member_its)
-    | [], [] -> 
-       return []
-    | ((id, mv) :: fields), ((smember, sbt) :: spec) ->
-       Cerb_debug.error "mismatch in fields in infer_struct"
-    | [], ((member, _) :: _) ->
-       fail (fun _ -> {loc; msg = Generic (!^"field" ^/^ Id.pp member ^^^ !^"missing")})
-    | ((member,_) :: _), [] ->
-       fail (fun _ -> {loc; msg = Generic (!^"supplying unexpected field" ^^^ Id.pp member)})
+  let@ () = 
+    WellTyped.correct_and_no_duplicate_members loc tag 
+      (List.map fst member_values)
+  in
+  let@ member_its = 
+    ListM.mapM (fun (member, mv) ->
+        let@ sct = get_member_type loc tag member layout in
+        let@ member_lvt = check_mem_value loc ~expect:(BT.of_sct sct) mv in
+        return (member, member_lvt)
+      ) member_values
   in
-  let@ member_its = check member_values (Memory.member_types layout) in
   return (IT.struct_ (tag, member_its))
 
 and check_union (loc : loc) (tag : Sym.t) (id : Id.t) 
@@ -688,6 +681,8 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t)
      )
   | M_PEstruct (tag, xs) ->
      let@ layout = get_struct_decl loc tag in
+     let@ () = WellTyped.correct_and_no_duplicate_members loc tag
+                 (List.map fst xs) in
      let@ xs_with_expects = ListM.mapM (fun (nm, expr) ->
        let@ ty = get_member_type loc tag nm layout in
        return (expr, BT.of_sct ty)) xs in
@@ -1667,11 +1662,19 @@ let check_tagdefs tagDefs =
     | M_UnionDef _ -> 
        unsupported Loc.unknown !^"todo: union types"
     | M_StructDef layout -> 
-       ListM.iterM (fun piece ->
-           match piece.member_or_padding with
-           | Some (name, ct) -> WellTyped.WCT.is_ct Loc.unknown ct
-           | None -> return ()
-         ) layout
+       let@ _ = 
+         ListM.fold_rightM (fun piece have ->
+             match piece.member_or_padding with
+             | Some (name, _) when IdSet.mem name have ->
+                fail (fun _ -> {loc = Loc.unknown; msg = Duplicate_member name})
+             | Some (name, ct) -> 
+                let@ () = WellTyped.WCT.is_ct Loc.unknown ct in
+                return (IdSet.add name have)
+             | None -> 
+                return have
+           ) layout IdSet.empty
+       in
+       return ()
   ) tagDefs
 
 

backend/cn/typeErrors.ml

@@ -83,9 +83,6 @@ type sym_or_string =
   | String of string
 
 
-
-
-
 type message =
   | Unknown_variable of Sym.t
   | Unknown_function of Sym.t
@@ -102,6 +99,8 @@ type message =
   | First_iarg_missing
   | First_iarg_not_pointer of { pname : ResourceTypes.predicate_name; found_bty: BaseTypes.t }
 
+  | Missing_member of Id.t
+  | Duplicate_member of Id.t
 
   | Missing_resource of {orequest : RET.t option; situation : situation; oinfo : info option; ctxt : Context.t; model: Solver.model_with_q; trace: Trace.t }
   | Merging_multiple_arrays of {orequest : RET.t option; situation : situation; oinfo : info option; ctxt : Context.t; model: Solver.model_with_q }
@@ -130,7 +129,7 @@ type message =
 
   | Empty_pattern
   | Missing_pattern of Pp.document
-  | Duplicate_pattern of Loc.t
+  | Duplicate_pattern
 
 
 type type_error = {
@@ -226,6 +225,12 @@ let pp_message te =
         Pp.squotes (BaseTypes.(pp found_bty))
      in
      { short; descr = Some descr; state = None; trace = None }
+  | Missing_member m ->
+     let short = !^"Missing member" ^^^ Id.pp m in
+     { short; descr = None; state = None; trace = None }
+  | Duplicate_member m ->
+     let short = !^"Duplicate member" ^^^ Id.pp m in
+     { short; descr = None; state = None; trace = None }
   | Missing_resource {orequest; situation; oinfo; ctxt; model; trace} ->
      let short = !^"Missing resource" ^^^ for_situation situation in
      let descr = missing_or_bad_request_description oinfo orequest in
@@ -387,8 +392,8 @@ let pp_message te =
   | Missing_pattern p' ->
      let short = !^"Missing pattern" ^^^ squotes p' ^^ dot in
      { short; descr = None; state = None; trace = None }
-  | Duplicate_pattern loc ->
-     let short = !^"Duplicate pattern (already matched at" ^^^ Loc.pp loc ^^ !^")" in
+  | Duplicate_pattern ->
+     let short = !^"Duplicate pattern" in
      { short; descr = None; state = None; trace = None }
 
 

backend/cn/wellTyped.ml

@@ -8,6 +8,7 @@ module LRT = LogicalReturnTypes
 module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
 module Mu = Mucore
+module IdSet = Set.Make(Id)
 
 open Global
 open TE
@@ -26,6 +27,26 @@ open Effectful.Make(Typing)
 let ensure_base_type = Typing.ensure_base_type
 
 
+let correct_and_no_duplicate_members loc tag members =
+  let@ layout = get_struct_decl loc tag in
+  let member_types = Memory.member_types layout in
+  let@ _, needed = 
+    ListM.fold_rightM (fun member (have, needed) ->
+        if IdSet.mem member have then
+          fail (fun _ -> {loc; msg = Duplicate_member member})
+        else if not (IdSet.mem member needed) then
+          fail (fun _ -> {loc; msg = Unknown_member (tag, member)})
+        else
+          return (IdSet.add member have, IdSet.remove member needed)
+      ) members (IdSet.empty, IdSet.of_list (List.map fst member_types))
+  in
+  match IdSet.elements needed with
+  | [] -> return ()
+  | member :: _ -> fail (fun _ -> {loc; msg = Missing_member member})
+
+
+
+
 
 (* let check_bound_l loc s =  *)
 (*   let@ is_bound = bound_l s in *)
@@ -132,14 +153,25 @@ module WIT = struct
   let eval = Simplify.IndexTerms.eval
 
   let check_and_bind_pattern loc (Pat (pat_, _)) bt =
-    match pat_ with
-    | PSym s -> 
-       let@ () = add_l s bt (loc, lazy (Sym.pp s)) in
-       return (Pat (PSym s, bt))
-    | PWild ->
-       return (Pat (PWild, bt))
-    | PConstructor (s, args) ->
-       failwith "asd"
+    let@ pat_ = match pat_ with
+      | PSym s -> 
+         let@ () = add_l s bt (loc, lazy (Sym.pp s)) in
+         return (PSym s)
+      | PWild ->
+         return (PWild)
+      | PConstructor (s, args) ->
+         let@ constr_info = get_datatype_constr loc s in
+         let@ () = ensure_base_type loc (Datatype constr_info.c_datatype_tag) ~expect:bt in
+         let@ args = 
+           ListM.mapM (fun (id, apat) ->
+               failwith "asd"
+             ) args
+         in
+         return (PConstructor (s, args))
+    in
+    return (Pat (pat_, bt))
+
+
 
   let rec infer =
       fun loc (IT (it, _)) ->
@@ -381,13 +413,8 @@ module WIT = struct
          return (IT (NthTuple (n, t'),item_bt))
       | Struct (tag, members) ->
          let@ layout = get_struct_decl loc tag in
+         let@ () = correct_and_no_duplicate_members loc tag (List.map fst members) in
          let decl_members = Memory.member_types layout in
-         let@ () = 
-           let has = List.length members in
-           let expect = List.length decl_members in
-           if has = expect then return ()
-           else fail (fun _ -> {loc; msg = Number_members {has; expect}})
-         in
          let@ members = 
            ListM.mapM (fun (member,t) ->
                let@ bt = match List.assoc_opt Id.equal member decl_members with