Cleaning up code in internalization.

4 files changed, 45 insertions, 19 deletions

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 6fce739d30..5490f9d57f 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -78,7 +78,7 @@ let change_sp_label sp id =
 let push_typedef visibility sp kn (_, def) = match def with
 | GTydDef _ ->
   Tac2env.push_type visibility sp kn
-| GTydAlg cstrs ->
+| GTydAlg { galg_constructors = cstrs } ->
   (** Register constructors *)
   let iter (c, _) =
     let spc = change_sp_label sp c in
@@ -107,7 +107,7 @@ let next i =
 let define_typedef kn (params, def as qdef) = match def with
 | GTydDef _ ->
   Tac2env.define_type kn qdef
-| GTydAlg cstrs ->
+| GTydAlg { galg_constructors = cstrs } ->
   (** Define constructors *)
   let constant = ref 0 in
   let nonconstant = ref 0 in
@@ -665,7 +665,17 @@ let call ~default e =
 let register_prim_alg name params def =
   let id = Id.of_string name in
   let def = List.map (fun (cstr, tpe) -> (Id.of_string_soft cstr, tpe)) def in
-  let def = (params, GTydAlg def) in
+  let getn (const, nonconst) (c, args) = match args with
+  | [] -> (succ const, nonconst)
+  | _ :: _ -> (const, succ nonconst)
+  in
+  let nconst, nnonconst = List.fold_left getn (0, 0) def in
+  let alg = {
+    galg_constructors = def;
+    galg_nconst = nconst;
+    galg_nnonconst = nnonconst;
+  } in
+  let def = (params, GTydAlg alg) in
   let def = { typdef_local = false; typdef_expr = def } in
   ignore (Lib.add_leaf id (inTypDef def))
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index b268e70cb3..e564dbde78 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -53,9 +53,18 @@ type 'a glb_typexpr =
 | GTypTuple of 'a glb_typexpr list
 | GTypRef of type_constant * 'a glb_typexpr list
 
+type glb_alg_type = {
+  galg_constructors : (uid * int glb_typexpr list) list;
+  (** Constructors of the algebraic type *)
+  galg_nconst : int;
+  (** Number of constant constructors *)
+  galg_nnonconst : int;
+  (** Number of non-constant constructors *)
+}
+
 type glb_typedef =
 | GTydDef of int glb_typexpr option
-| GTydAlg of (uid * int glb_typexpr list) list
+| GTydAlg of glb_alg_type
 | GTydRec of (lid * mutable_flag * int glb_typexpr) list
 | GTydOpn
 
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 431b551191..86db803ea7 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -482,7 +482,7 @@ let check_elt_empty loc env t = match kind env t with
 | GTypRef (kn, _) ->
   let def = Tac2env.interp_type kn in
   match def with
-  | _, GTydAlg [] -> kn
+  | _, GTydAlg { galg_constructors = [] } -> kn
   | _ ->
     let name = env_name env in
     user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type")
@@ -856,17 +856,13 @@ and intern_case env loc e pl =
     let subst, tc = fresh_reftype env kn in
     let () = unify ~loc:(loc_of_tacexpr e) env t tc in
     let (params, def) = Tac2env.interp_type kn in
-    let cstrs = match def with
+    let galg = match def with
     | GTydAlg c -> c
     | _ -> assert false
     in
-    let count (const, nonconst) (c, args) = match args with
-    | [] -> (succ const, nonconst)
-    | _ :: _ -> (const, succ nonconst)
-    in
-    let nconst, nnonconst = List.fold_left count (0, 0) cstrs in
-    let const = Array.make nconst None in
-    let nonconst = Array.make nnonconst None in
+    let cstrs = galg.galg_constructors in
+    let const = Array.make galg.galg_nconst None in
+    let nonconst = Array.make galg.galg_nnonconst None in
     let ret = GTypVar (fresh_id env) in
     let rec intern_branch = function
     | [] -> ()
@@ -1114,7 +1110,17 @@ let intern_typedef self (ids, t) : glb_quant_typedef =
   | CTydAlg constrs ->
     let map (c, t) = (c, List.map intern t) in
     let constrs = List.map map constrs in
-    (count, GTydAlg constrs)
+    let getn (const, nonconst) (c, args) = match args with
+    | [] -> (succ const, nonconst)
+    | _ :: _ -> (const, succ nonconst)
+    in
+    let nconst, nnonconst = List.fold_left getn (0, 0) constrs in
+    let galg = {
+      galg_constructors = constrs;
+      galg_nconst = nconst;
+      galg_nnonconst = nnonconst;
+    } in
+    (count, GTydAlg galg)
   | CTydRec fields ->
     let map (c, mut, t) = (c, mut, intern t) in
     let fields = List.map map fields in
@@ -1324,13 +1330,14 @@ let subst_typedef subst e = match e with
 | GTydDef t ->
   let t' = Option.smartmap (fun t -> subst_type subst t) t in
   if t' == t then e else GTydDef t'
-| GTydAlg constrs ->
+| GTydAlg galg ->
   let map (c, tl as p) =
     let tl' = List.smartmap (fun t -> subst_type subst t) tl in
     if tl' == tl then p else (c, tl')
   in
-  let constrs' = List.smartmap map constrs in
-  if constrs' == constrs then e else GTydAlg constrs'
+  let constrs' = List.smartmap map galg.galg_constructors in
+  if constrs' == galg.galg_constructors then e
+  else GTydAlg { galg with galg_constructors = constrs' }
 | GTydRec fields ->
   let map (c, mut, t as p) =
     let t' = subst_type subst t in
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 2afcfb4a6e..aa8e1e98d5 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -175,7 +175,7 @@ let pr_glbexpr_gen lvl c =
     mt () (** FIXME when implemented *)
   | GTacCst (GCaseAlg tpe, n, cl) ->
     begin match Tac2env.interp_type tpe with
-    | _, GTydAlg def ->
+    | _, GTydAlg { galg_constructors = def } ->
       let paren = match lvl with
       | E0 -> paren
       | E1 | E2 | E3 | E4 | E5 -> fun x -> x
@@ -202,7 +202,7 @@ let pr_glbexpr_gen lvl c =
     let br = match info with
     | GCaseAlg kn ->
       let def = match Tac2env.interp_type kn with
-      | _, GTydAlg def -> def
+      | _, GTydAlg { galg_constructors = def } -> def
       | _, GTydDef _ | _, GTydRec _ | _, GTydOpn -> assert false
       in
       let br = order_branches cst_br ncst_br def in