diff --git a/src/lustre/lustreAstInlineConstants.ml b/src/lustre/lustreAstInlineConstants.ml index 09b6548ba..98a382c55 100644 --- a/src/lustre/lustreAstInlineConstants.ml +++ b/src/lustre/lustreAstInlineConstants.ml @@ -488,16 +488,8 @@ let rec inline_constants_of_contract: TC.tc_context -> LA.contract -> LA.contrac let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declaration) = fun ctx -> function | TypeDecl (span, AliasType (pos, i, t)) -> - let ctx', t' = - match t with - | LA.EnumType _ -> - (* Special handling is applied to enum types (see type_check_infer_globals) *) - ctx, t - | _ -> - let t' = inline_constants_of_lustre_type ctx t in - TC.add_ty_syn ctx i t', t' - in - ctx', LA.TypeDecl (span, AliasType (pos, i, t')) + let t' = inline_constants_of_lustre_type ctx t in + TC.add_ty_syn ctx i t', LA.TypeDecl (span, AliasType (pos, i, t')) | ConstDecl (span, FreeConst (pos, id, ty)) -> let ty' = inline_constants_of_lustre_type ctx ty in ctx, ConstDecl (span, FreeConst (pos, id, ty')) diff --git a/src/lustre/lustreNodeGen.ml b/src/lustre/lustreNodeGen.ml index c41b01c97..b11f5ec3f 100644 --- a/src/lustre/lustreNodeGen.ml +++ b/src/lustre/lustreNodeGen.ml @@ -623,19 +623,8 @@ and compile_ast_type | A.UserType (_, ident) -> StringMap.find ident cstate.type_alias | A.AbstractType (_, ident) -> - (match StringMap.find_opt ident cstate.type_alias with - | Some candidate -> - (* The typechecker transforms enum types to abstract types (not sure why) - here we check if the ident in fact names an enum type *) - let ident = HString.string_of_hstring ident in - let bindings = X.bindings candidate in - let (head_index, ty) = List.hd bindings in - if List.length bindings = 1 && head_index = X.empty_index && Type.is_enum ty then - candidate - else X.singleton [X.AbstractTypeIndex ident] Type.t_int - | None -> - let ident = HString.string_of_hstring ident in - X.singleton [X.AbstractTypeIndex ident] Type.t_int) + let ident = HString.string_of_hstring ident in + X.singleton [X.AbstractTypeIndex ident] Type.t_int | A.RecordType (_, _, record_fields) -> let over_fields = fun a (_, i, t) -> let i = HString.string_of_hstring i in diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index d296b1f4e..5d5660a3c 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -212,14 +212,14 @@ let type_error pos kind = Error (`LustreTypeCheckerError (pos, kind)) let check_merge_clock: LA.expr -> LA.lustre_type -> (unit, [> error]) result = fun e ty -> match ty with - | AbstractType (_, _) -> LSC.no_mismatched_clock false e + | EnumType _ -> LSC.no_mismatched_clock false e | Bool _ -> LSC.no_mismatched_clock true e | _ -> Ok () let check_merge_exhaustive: tc_context -> Lib.position -> LA.lustre_type -> HString.t list -> (unit, [> error]) result = fun ctx pos ty cases -> match ty with - | AbstractType (_, enum_id) -> (match lookup_variants ctx enum_id with + | EnumType (_, enum_id, _) -> (match lookup_variants ctx enum_id with | Some variants -> let check_cases_containment = R.seq_ (List.map (fun i -> @@ -248,7 +248,7 @@ let check_merge_exhaustive: tc_context -> Lib.position -> LA.lustre_type -> HStr ^ " is not an enumeration identifier"))) | Bool _ -> Ok () (* TODO: What checks should we do for a boolean merge? *) | _ -> type_error pos (Impossible ("Type " ^ string_of_tc_type ty ^ - " must be an abstract type")) + " must be a bool or an enum type")) let rec infer_const_attr ctx exp = let r = infer_const_attr ctx in @@ -1360,7 +1360,7 @@ and tc_ctx_of_ty_decl: tc_context -> LA.type_decl -> (tc_context, [> error]) res (* 1. add the enum type and variants to the enum context *) let ctx' = add_enum_variants ctx ename econsts in (* 2. add the enum type as a valid type in context*) - let ctx'' = add_ty_syn ctx' ename (LA.AbstractType (pos, ename)) in + let ctx'' = add_ty_syn ctx' i ty in R.ok (List.fold_left union (add_ty_decl ctx'' ename) (* 3. Lift all enum constants (terms) with associated user type of enum name *) (enum_type_bindings