Restoring typechecker

OCamlPro · May 24, 2024 · 8d4eb8c · 8d4eb8c
1 parent cf97bc7
commit 8d4eb8c
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 14 deletions.
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
@@ -69,10 +69,14 @@ module Types = struct
     match ty with
     | Ty.Text (lty', s)
     | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty',_) ->
+    | Ty.Tadt (s,lty',false) ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
+    | Ty.Tadt (s,lty',true) ->
+      if List.length lty <> 0 || List.length lty' <> 0 then
+        Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
+      []
     | _ -> assert false
 
   let equal_pp_vars lpp lvars =
@@ -162,7 +166,7 @@ module Types = struct
                 (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs }
     | Enum l ->
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
-      let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
+      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Algebraic l ->
       let l = (* convert ppure_type to Ty.t in l *)
@@ -269,8 +273,8 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tadt (name, params, _) ->
-      let Adt cases = Ty.type_body name params in
+    | Ty.Tadt (name, [], true) ->
+      let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
         (fun m c ->
@@ -295,11 +299,12 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tadt (name, params, _) ->
-      let Adt cases = Ty.type_body name params in
+    | Ty.Tadt (name, [], true) ->
+      let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.find (fun c -> String.equal n @@ Uid.show c) cstrs
-    | _ -> assert false
+    | _ ->
+      assert false
 
   let add_fpa_builtins env =
     let (->.) args result = { args; result } in
@@ -999,9 +1004,8 @@ let rec type_term ?(call_from_type_form=false) env f =
       let ty = Ty.shorten e.c.tt_ty in
       let ty_body = match ty with
         | Ty.Tadt (name, params, _) ->
-          begin match Ty.type_body name params with
-            | Ty.Adt cases -> cases
-          end
+          let Ty.Adt cases = Ty.type_body name params in
+          cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr; destrs = lbs}]
         | _ -> Errors.typing_error (ShouldBeADT ty) loc
@@ -1408,9 +1412,8 @@ and type_form ?(in_theory=false) env f =
       let ty = e.c.tt_ty in
       let ty_body = match ty with
         | Ty.Tadt (name, params, _) ->
-          begin match Ty.type_body name params with
-            | Ty.Adt cases -> cases
-          end
+          let Ty.Adt cases = Ty.type_body name params in
+          cases
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr ; destrs = lbs}]
 

diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
@@ -96,7 +96,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let body =
     List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
   in
-  let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =