diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index 2005e76e0..e919e7e05 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -157,17 +157,55 @@ let check_comptype (c : context) (ct : comptype) at = check_resulttype c ts1 at; check_resulttype c ts2 at -(* TODO: Make sure the describes and descriptor clauses match. *) let check_desctype (c : context) (dt : desctype) at = - match dt with - | DescT (ht1, ht2, ct) -> check_comptype c ct at + let DescT (_, _, ct) = dt in + check_comptype c ct at -let check_desctype_sub (c : context) (dt : desctype) (dti : desctype) x xi at = +let check_desctype_sub (c : context) (dt : desctype) (dt' : desctype) x x' at = (* TODO: check rules *) - let DescT (_, _, ct) = dt in - let DescT (_, _, cti) = dti in - require (match_comptype c.types ct cti) at ("sub type " ^ I32.to_string_u x ^ - " does not match super type " ^ I32.to_string_u xi) + let DescT (ut1, ut2, ct) = dt in + let DescT (ut1', ut2', ct') = dt' in + match ut1, ut1' with + | (Some ut1, Some ut1') -> + let dt1' = deftype_of_typeuse ut1' in + let x1 = idx_of_typeuse ut1 in + let SubT (_, uts, _) = unroll_deftype (type_ c (x1 @@ at)) in + (match uts with + | [] -> + require false at ("described type " ^ I32.to_string_u x1 ^ + " does not have required supertype") + | ut :: [] -> + let dt1'' = (type_ c ((idx_of_typeuse ut) @@ at)) in + require (dt1' = dt1'') at "oogabooga" + | _ -> assert false) + | (None, None) -> () + | _ -> require false at "blah"; + (* TODO: match ut2, ut2' *) + require (match_comptype c.types ct ct') at ("sub type " ^ I32.to_string_u x ^ + " does not match super type " ^ I32.to_string_u x') + +let check_descriptors (dts : deftype list) at = + List.iter (fun dt -> + let DefT ((RecT dts), x) = dt in + let SubT (_, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in + Option.iter (fun ut -> + match ut with + | Rec x' -> + let SubT (_, _, DescT (_, ut', _)) = Lib.List32.nth dts x' in + require (ut' = Some (Rec x)) at + "described type is not described by descriptor"; + require (x' < x) at "forward use of described type" + | _ -> require false at "described type is outside rec group" + ) ut1; + Option.iter (fun ut -> + match ut with + | Rec x' -> + let SubT (_, _, DescT (ut', _, _)) = Lib.List32.nth dts x' in + require (ut' = Some (Rec x)) at + "type is not described by its descriptor"; + | _ -> require false at "descriptor type is outside rec group" + ) ut2 + ) dts let check_subtype (c : context) (sut : subtype) at = let SubT (_fin, uts, dt) = sut in @@ -189,7 +227,9 @@ let check_subtype_sub (c : context) (sut : subtype) x at = let check_rectype (c : context) (rt : rectype) at : context = let RecT sts = rt in let x = Lib.List32.length c.types in - let c' = {c with types = c.types @ roll_deftypes x rt} in + let dts = roll_deftypes x rt in + check_descriptors dts at; + let c' = {c with types = c.types @ dts} in List.iter (fun st -> check_subtype c' st at) sts; Lib.List32.iteri (fun i st -> check_subtype_sub c' st (Int32.add x i) at) sts; diff --git a/test/core/custom-descriptors/descriptors.wast b/test/core/custom-descriptors/descriptors.wast index 4ba060487..78c47443a 100644 --- a/test/core/custom-descriptors/descriptors.wast +++ b/test/core/custom-descriptors/descriptors.wast @@ -72,3 +72,113 @@ ) "unexpected token" ) + +;; Type validation + +(assert_invalid + (module + (type (descriptor 1) (struct)) + ) + "descriptor type is outside rec group" +) + +(assert_invalid + (module + (type (describes 1) (struct)) + ) + "described type is outside rec group" +) + +(assert_invalid + (module + (type (descriptor 1) (struct)) + (type (struct)) + ) + "descriptor type is outside rec group" +) + +(assert_invalid + (module + (type (describes 1) (struct)) + (type (struct)) + ) + "described type is outside rec group" +) + +(assert_invalid + (module + (type (struct)) + (type (descriptor 0) (struct)) + ) + "descriptor type is outside rec group" +) + +(assert_invalid + (module + (type (struct)) + (type (describes 0) (struct)) + ) + "described type is outside rec group" +) + +(assert_invalid + (module + (rec + (type (descriptor 1) (struct)) + (type (struct)) + ) + ) + "type is not described by its descriptor" +) + +(assert_invalid + (module + (rec + (type (struct)) + (type (describes 0) (struct)) + ) + ) + "described type is not described by descriptor" +) + +(assert_invalid + (module + (rec + (type (describes 1) (struct)) + (type (descriptor 0) (struct)) + ) + ) + "forward use of described type" +) + +(assert_invalid + (module + (type (describes 0) (descriptor 0) (struct)) + ) + "forward use of described type" +) + +;; Subtyping + +(module + (rec + (type $A (sub (descriptor $A.desc) (struct))) + (type $A.desc (sub (describes $A) (struct))) + ) + (rec + (type $B (sub $A (descriptor $B.desc) (struct))) + (type $B.desc (sub $A.desc (describes $B) (struct))) + ) +) + +;; TODO: this fails! +(module + (rec + (type $A (sub (descriptor $A.desc) (struct))) + (type $A.desc (sub (describes $A) (struct))) + (type $B (sub $A (descriptor $B.desc) (struct))) + (type $B.desc (sub $A.desc (describes $B) (struct))) + ) +) + +;; TODO: structs only