diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 16 | ||||
| -rw-r--r-- | src/tac2expr.mli | 11 | ||||
| -rw-r--r-- | src/tac2intern.ml | 33 | ||||
| -rw-r--r-- | src/tac2print.ml | 4 |
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 |