Skip to content

Commit

Permalink
Do not transform enum types to abstract types
Browse files Browse the repository at this point in the history
Commit 5439c29 introduced this transformation (I do not know why),
but it was the source of several bugs (see 54ded7a, c2d6105).
This commit removes the transformation.
  • Loading branch information
daniel-larraz committed Nov 9, 2023
1 parent cff33d5 commit c20339d
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 27 deletions.
12 changes: 2 additions & 10 deletions src/lustre/lustreAstInlineConstants.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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'))
Expand Down
15 changes: 2 additions & 13 deletions src/lustre/lustreNodeGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/lustre/lustreTypeChecker.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit c20339d

Please sign in to comment.