Merge pull request kind2-mc#1031 from daniel-larraz/fix-enum-types

Do not transform enum types to abstract types

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'))

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

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