@@ -83,7 +83,8 @@ Module decltype.
8383 Section with_lang.
8484 Record ext_tu : Set :=
8585 { ext_symbols : name -> option decltype
86- ; ext_types : name -> option GlobDecl }.
86+ ; ext_types : name -> option GlobDecl
87+ ; ext_values : name -> option ObjValue }.
8788
8889 #[local] Definition M : Set -> Type :=
8990 readerT.M (ext_tu * decltype * option exprtype * list (localname * decltype)) (trace.M Error.t).
@@ -113,6 +114,20 @@ Module decltype.
113114 | None => throw ("failed to find global "%bs, n)
114115 end .
115116
117+ Definition value (n : name) : M ObjValue :=
118+ let * osym := readerT.asks (fun '(tu, _, _, _) => tu.(ext_values) n) in
119+ match osym with
120+ | Some ov => mret ov
121+ | None => throw ("failed to find global value "%bs, n)
122+ end .
123+
124+ Definition constructor_decl (n : name) : M Ctor :=
125+ let * ov := value n in
126+ match ov with
127+ | Oconstructor c => mret c
128+ | _ => throw ("global value is not a constructor "%bs, n, ov)
129+ end .
130+
116131 Definition type_of_constant (n : name) (id : ident) : M decltype :=
117132 let * osym := readerT.asks (fun '(tu, _, _, _) => tu.(ext_types) $ Nscoped n (Nid id)) in
118133 match osym with
@@ -529,6 +544,49 @@ Module decltype.
529544 | _ => throw "can not increment or decrement bool"%bs
530545 end .
531546
547+ Definition field_type (fld : field_name.t) (ms : list Member) : M type :=
548+ match List.find (fun m => bool_decide (m.(mem_name) = fld)) ms with
549+ | Some m => mret $ normalize_type m.(mem_type)
550+ | None => throw ("failed to find field "%bs, fld)
551+ end .
552+
553+ Definition type_of_global_or_field (n : name) : M decltype :=
554+ let * osym := readerT.asks (fun '(tu, _, _, _) => tu.(ext_symbols) n) in
555+ match osym with
556+ | Some sym => mret sym
557+ | None =>
558+ match n with
559+ | Nscoped cls fld =>
560+ let * gd := global cls in
561+ match gd with
562+ | Gstruct st => field_type fld st.(s_fields)
563+ | Gunion un => field_type fld un.(u_fields)
564+ | _ => throw ("global scope is not an aggregate "%bs, cls, gd)
565+ end
566+ | _ => throw ("failed to find global "%bs, n)
567+ end
568+ end .
569+
570+ Definition class_type (t : type) : M name :=
571+ match class_name t with
572+ | Some cls => mret cls
573+ | None => throw ("not a class type "%bs, t)
574+ end .
575+
576+ Definition constructed_class (t : type) : M name :=
577+ match class_name t with
578+ | Some cls => mret cls
579+ | None =>
580+ match array_type t with
581+ | Some ety => class_type ety
582+ | None => throw ("constructor result is not a class or class array "%bs, t)
583+ end
584+ end .
585+
586+ Definition check_constructor_result (c : Ctor) (t : type) : M unit :=
587+ let * cls := constructed_class t in
588+ require_eq cls c.(c_class).
589+
532590 Definition of_expr_body (e : Expr) : M decltype :=
533591 trace e $
534592 let * result :=
@@ -556,14 +614,9 @@ Module decltype.
556614 let * _ := require_eq (Tenum n) ct in
557615 mret $ Tenum n
558616 | Eglobal nm ty =>
559- (* TODO NAMES TYPING:
560- 1. fields are not included, these are necessary for <<sizeof()>> (see cxx/bitvector)
561- *)
562- (*
563- let* from_env := type_of_global nm in
564- trace ("from_env = ", from_env))%bs $
617+ let * from_env := type_of_global_or_field nm in
618+ trace ("from_env = "%bs, from_env) $
565619 let * _ := require_eq from_env (normalize_type ty) in
566- *)
567620 mret $ tref QM (normalize_type ty)
568621 | Eglobal_member nm ty =>
569622 match nm with
@@ -743,8 +796,10 @@ Module decltype.
743796 const Tsize_t <$> guard (t = Tsize_t)
744797 | Eoffsetof _ _ t => mret t
745798 | Econstructor f es t =>
746- (* TODO: check the type of the constructor [f] *)
799+ let * ctor := constructor_decl f in
747800 let * tes := traverse (T:=eta list) of_expr es in
801+ let * _ := check_args ctor.(c_arity) (snd <$> ctor.(c_params)) tes in
802+ let * _ := check_constructor_result ctor t in
748803 mret t
749804 | Elambda n es =>
750805 let * tes := traverse (T:=eta list) of_expr es in
@@ -1093,7 +1148,8 @@ Module decltype.
10931148
10941149 Definition tu_to_ext (tu : translation_unit) : internal.ext_tu :=
10951150 {| internal.ext_symbols nm := fmap (M:=fun t => option t) type_of_value $ tu.(symbols) !! nm
1096- ; internal.ext_types nm := types tu !! nm |}.
1151+ ; internal.ext_types nm := types tu !! nm
1152+ ; internal.ext_values nm := symbols tu !! nm |}.
10971153
10981154 Definition of_expr (tu : translation_unit) (e : Expr) : trace.M Error.t decltype :=
10991155 readerT.run (internal.of_expr e) (tu_to_ext tu, Tvoid, None, []).
0 commit comments