Skip to content

Commit 75935d7

Browse files
loutrloutr
committed
style: use regular datatype for ty_body
1 parent a12b3e8 commit 75935d7

11 files changed

Lines changed: 107 additions & 106 deletions

File tree

‎src/ecDecl.ml‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -15,42 +15,42 @@ type ty_param = EcIdent.t * EcPath.Sp.t
1515
type ty_params = ty_param list
1616
type ty_pctor = [ `Int of int | `Named of ty_params ]
1717

18-
type tydecl = {
19-
tyd_params : ty_params;
20-
tyd_type : ty_body;
21-
tyd_loca : locality;
22-
}
23-
24-
and ty_body = [
25-
| `Concrete of EcTypes.ty
26-
| `Abstract of Sp.t
27-
| `Datatype of ty_dtype
28-
| `Record of ty_record
29-
]
30-
31-
and ty_record =
18+
type ty_record =
3219
EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
3320

34-
and ty_dtype_ctor =
21+
type ty_dtype_ctor =
3522
EcSymbols.symbol * EcTypes.ty list
3623

37-
and ty_dtype = {
24+
type ty_dtype = {
3825
tydt_ctors : ty_dtype_ctor list;
3926
tydt_schelim : EcCoreFol.form;
4027
tydt_schcase : EcCoreFol.form;
4128
}
4229

30+
type ty_body =
31+
| Concrete of EcTypes.ty
32+
| Abstract of Sp.t
33+
| Datatype of ty_dtype
34+
| Record of ty_record
35+
36+
37+
type tydecl = {
38+
tyd_params : ty_params;
39+
tyd_type : ty_body;
40+
tyd_loca : locality;
41+
}
42+
4343
let tydecl_as_concrete (td : tydecl) =
44-
match td.tyd_type with `Concrete x -> Some x | _ -> None
44+
match td.tyd_type with Concrete x -> Some x | _ -> None
4545

4646
let tydecl_as_abstract (td : tydecl) =
47-
match td.tyd_type with `Abstract x -> Some x | _ -> None
47+
match td.tyd_type with Abstract x -> Some x | _ -> None
4848

4949
let tydecl_as_datatype (td : tydecl) =
50-
match td.tyd_type with `Datatype x -> Some x | _ -> None
50+
match td.tyd_type with Datatype x -> Some x | _ -> None
5151

5252
let tydecl_as_record (td : tydecl) =
53-
match td.tyd_type with `Record x -> Some x | _ -> None
53+
match td.tyd_type with Record (x, y) -> Some (x, y) | _ -> None
5454

5555
(* -------------------------------------------------------------------- *)
5656
let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
@@ -65,7 +65,7 @@ let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
6565
(EcUid.NameGen.bulk ~fmt n)
6666
in
6767

68-
{ tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }
68+
{ tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; }
6969

7070
(* -------------------------------------------------------------------- *)
7171
let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =

‎src/ecDecl.mli‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -11,31 +11,31 @@ type ty_param = EcIdent.t * EcPath.Sp.t
1111
type ty_params = ty_param list
1212
type ty_pctor = [ `Int of int | `Named of ty_params ]
1313

14-
type tydecl = {
15-
tyd_params : ty_params;
16-
tyd_type : ty_body;
17-
tyd_loca : locality;
18-
}
19-
20-
and ty_body = [
21-
| `Concrete of EcTypes.ty
22-
| `Abstract of Sp.t
23-
| `Datatype of ty_dtype
24-
| `Record of ty_record
25-
]
26-
27-
and ty_record =
14+
type ty_record =
2815
EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
2916

30-
and ty_dtype_ctor =
17+
type ty_dtype_ctor =
3118
EcSymbols.symbol * EcTypes.ty list
3219

33-
and ty_dtype = {
20+
type ty_dtype = {
3421
tydt_ctors : ty_dtype_ctor list;
3522
tydt_schelim : EcCoreFol.form;
3623
tydt_schcase : EcCoreFol.form;
3724
}
3825

26+
type ty_body =
27+
| Concrete of EcTypes.ty
28+
| Abstract of Sp.t
29+
| Datatype of ty_dtype
30+
| Record of ty_record
31+
32+
33+
type tydecl = {
34+
tyd_params : ty_params;
35+
tyd_type : ty_body;
36+
tyd_loca : locality;
37+
}
38+
3939
val tydecl_as_concrete : tydecl -> EcTypes.ty option
4040
val tydecl_as_abstract : tydecl -> Sp.t option
4141
val tydecl_as_datatype : tydecl -> ty_dtype option

‎src/ecEnv.ml‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -781,10 +781,10 @@ module MC = struct
781781
let loca = tyd.tyd_loca in
782782

783783
match tyd.tyd_type with
784-
| `Concrete _ -> mc
785-
| `Abstract _ -> mc
784+
| Concrete _ -> mc
785+
| Abstract _ -> mc
786786

787-
| `Datatype dtype ->
787+
| Datatype dtype ->
788788
let cs = dtype.tydt_ctors in
789789
let schelim = dtype.tydt_schelim in
790790
let schcase = dtype.tydt_schcase in
@@ -828,7 +828,7 @@ module MC = struct
828828
_up_operator candup mc name (ipath name, op)
829829
) mc projs
830830

831-
| `Record (scheme, fields) ->
831+
| Record (scheme, fields) ->
832832
let params = List.map (fun (x, _) -> tvar x) tyd.tyd_params in
833833
let nfields = List.length fields in
834834
let cfields =
@@ -2541,12 +2541,12 @@ module Ty = struct
25412541
25422542
let defined (name : EcPath.path) (env : env) =
25432543
match by_path_opt name env with
2544-
| Some { tyd_type = `Concrete _ } -> true
2544+
| Some { tyd_type = Concrete _ } -> true
25452545
| _ -> false
25462546
25472547
let unfold (name : EcPath.path) (args : EcTypes.ty list) (env : env) =
25482548
match by_path_opt name env with
2549-
| Some ({ tyd_type = `Concrete body } as tyd) ->
2549+
| Some ({ tyd_type = Concrete body } as tyd) ->
25502550
Tvar.subst
25512551
(Tvar.init (List.map fst tyd.tyd_params) args)
25522552
body
@@ -2582,14 +2582,15 @@ module Ty = struct
25822582
match ty.ty_node with
25832583
| Tconstr (p, tys) -> begin
25842584
match by_path_opt p env with
2585-
| Some ({ tyd_type = (`Datatype _ | `Record _) as body }) ->
2585+
| Some ({ tyd_type = (Datatype _ | Record _) as body }) ->
25862586
let prefix = EcPath.prefix p in
25872587
let basename = EcPath.basename p in
25882588
let basename =
25892589
match body, mode with
2590-
| `Record _, (`Ind | `Case) -> basename ^ "_ind"
2591-
| `Datatype _, `Ind -> basename ^ "_ind"
2592-
| `Datatype _, `Case -> basename ^ "_case"
2590+
| Record _, (`Ind | `Case) -> basename ^ "_ind"
2591+
| Datatype _, `Ind -> basename ^ "_ind"
2592+
| Datatype _, `Case -> basename ^ "_case"
2593+
| _, _ -> assert false
25932594
in
25942595
Some (EcPath.pqoname prefix basename, tys)
25952596
| _ -> None
@@ -2605,7 +2606,7 @@ module Ty = struct
26052606
let env = MC.bind_tydecl name ty env in
26062607
26072608
match ty.tyd_type with
2608-
| `Abstract tc ->
2609+
| Abstract tc ->
26092610
let myty =
26102611
let myp = EcPath.pqname (root env) name in
26112612
let typ = List.map (fst_map EcIdent.fresh) ty.tyd_params in
@@ -2931,7 +2932,7 @@ module Theory = struct
29312932
29322933
| Th_type (x, tyd) -> begin
29332934
match tyd.tyd_type with
2934-
| `Abstract tc ->
2935+
| Abstract tc ->
29352936
let myty =
29362937
let typ = List.map (fst_map EcIdent.fresh) tyd.tyd_params in
29372938
(typ, EcTypes.tconstr (xpath x) (List.map (tvar |- fst) typ))

‎src/ecHiInductive.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
8484
let env0 =
8585
let myself = {
8686
tyd_params = EcUnify.UniEnv.tparams ue;
87-
tyd_type = `Abstract EcPath.Sp.empty;
87+
tyd_type = Abstract EcPath.Sp.empty;
8888
tyd_loca = lc;
8989
} in
9090
EcEnv.Ty.bind (unloc name) myself env
@@ -135,16 +135,16 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
135135
fun ty -> ty_instanciate tdecl.tyd_params targs ty in
136136

137137
match tdecl.tyd_type with
138-
| `Abstract _ ->
138+
| Abstract _ ->
139139
List.exists isempty (targs)
140140

141-
| `Concrete ty ->
141+
| Concrete ty ->
142142
isempty_1 [tyinst () ty]
143143

144-
| `Record (_, fields) ->
144+
| Record (_, fields) ->
145145
isempty_1 (List.map (tyinst () |- snd) fields)
146146

147-
| `Datatype dt ->
147+
| Datatype dt ->
148148
isempty_n (List.map (List.map (tyinst ()) |- snd) dt.tydt_ctors)
149149

150150
in

‎src/ecPrinting.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1281,7 +1281,7 @@ let pp_opapp
12811281
let recp = EcDecl.operator_as_rcrd op in
12821282

12831283
match EcEnv.Ty.by_path_opt recp env with
1284-
| Some { tyd_type = `Record (_, fields) }
1284+
| Some { tyd_type = Record (_, fields) }
12851285
when List.length fields = List.length es
12861286
-> begin
12871287
let wmap =
@@ -2280,12 +2280,12 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) =
22802280

22812281
and pp_body fmt =
22822282
match tyd.tyd_type with
2283-
| `Abstract _ -> () (* FIXME: TC HOOK *)
2283+
| Abstract _ -> () (* FIXME: TC HOOK *)
22842284

2285-
| `Concrete ty ->
2285+
| Concrete ty ->
22862286
Format.fprintf fmt " =@ %a" (pp_type ppe) ty
22872287

2288-
| `Datatype { tydt_ctors = cs } ->
2288+
| Datatype { tydt_ctors = cs } ->
22892289
let pp_ctor fmt (c, cty) =
22902290
match cty with
22912291
| [] ->
@@ -2296,7 +2296,7 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) =
22962296
in
22972297
Format.fprintf fmt " =@ [@[<hov 2>%a@]]" (pp_list " |@ " pp_ctor) cs
22982298

2299-
| `Record (_, fields) ->
2299+
| Record (_, fields) ->
23002300
let pp_field fmt (f, fty) =
23012301
Format.fprintf fmt "%s: @[<hov 2>%a@]" f (pp_type ppe) fty
23022302
in

‎src/ecScope.ml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2239,25 +2239,25 @@ module Ty = struct
22392239
(fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env))
22402240
tcs in
22412241
let ue = TT.transtyvars env (loc, Some args) in
2242-
EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs)
2242+
EcUnify.UniEnv.tparams ue, Abstract (Sp.of_list tcs)
22432243

22442244
| PTYD_Alias bd ->
22452245
let ue = TT.transtyvars env (loc, Some args) in
22462246
let body = transty tp_tydecl env ue bd in
2247-
EcUnify.UniEnv.tparams ue, `Concrete body
2247+
EcUnify.UniEnv.tparams ue, Concrete body
22482248

22492249
| PTYD_Datatype dt ->
22502250
let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
22512251
let tparams, tydt =
22522252
try ELI.datatype_as_ty_dtype datatype
22532253
with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
22542254
in
2255-
tparams, `Datatype tydt
2255+
tparams, Datatype tydt
22562256

22572257
| PTYD_Record rt ->
22582258
let record = EHI.trans_record env (mk_loc loc (args,name)) rt in
22592259
let scheme = ELI.indsc_of_record record in
2260-
record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
2260+
record.ELI.rc_tparams, Record (scheme, record.ELI.rc_fields)
22612261
in
22622262

22632263
bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; })
@@ -2270,7 +2270,7 @@ module Ty = struct
22702270
let scope =
22712271
let decl = EcDecl.{
22722272
tyd_params = [];
2273-
tyd_type = `Abstract Sp.empty;
2273+
tyd_type = Abstract Sp.empty;
22742274
tyd_loca = `Global; (* FIXME:SUBTYPE *)
22752275
} in bind scope (unloc subtype.pst_name, decl) in
22762276

@@ -2365,7 +2365,7 @@ module Ty = struct
23652365
let asty =
23662366
let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
23672367
{ tyd_params = [];
2368-
tyd_type = `Abstract body;
2368+
tyd_type = Abstract body;
23692369
tyd_loca = (lc :> locality); } in
23702370
let scenv = EcEnv.Ty.bind name asty scenv in
23712371

‎src/ecSection.ml‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -437,12 +437,12 @@ and on_typarams (aenv : aenv) typarams =
437437
and on_tydecl (aenv : aenv) (tyd : tydecl) =
438438
on_typarams aenv tyd.tyd_params;
439439
match tyd.tyd_type with
440-
| `Concrete ty -> on_ty aenv ty
441-
| `Abstract s -> on_typeclasses aenv s
442-
| `Record (f, fds) ->
440+
| Concrete ty -> on_ty aenv ty
441+
| Abstract s -> on_typeclasses aenv s
442+
| Record (f, fds) ->
443443
on_form aenv f;
444444
List.iter (on_ty aenv |- snd) fds
445-
| `Datatype dt ->
445+
| Datatype dt ->
446446
List.iter (List.iter (on_ty aenv) |- snd) dt.tydt_ctors;
447447
List.iter (on_form aenv) [dt.tydt_schelim; dt.tydt_schcase]
448448

@@ -652,7 +652,7 @@ let add_declared_ty to_gen path tydecl =
652652
assert (tydecl.tyd_params = []);
653653
let s =
654654
match tydecl.tyd_type with
655-
| `Abstract s -> s
655+
| Abstract s -> s
656656
| _ -> assert false in
657657

658658
let name = "'" ^ basename path in
@@ -721,14 +721,14 @@ and fv_and_tvar_f f =
721721
let tydecl_fv tyd =
722722
let fv =
723723
match tyd.tyd_type with
724-
| `Concrete ty -> ty_fv_and_tvar ty
725-
| `Abstract _ -> Mid.empty
726-
| `Datatype tydt ->
724+
| Concrete ty -> ty_fv_and_tvar ty
725+
| Abstract _ -> Mid.empty
726+
| Datatype tydt ->
727727
List.fold_left (fun fv (_, l) ->
728728
List.fold_left (fun fv ty ->
729729
EcIdent.fv_union fv (ty_fv_and_tvar ty)) fv l)
730730
Mid.empty tydt.tydt_ctors
731-
| `Record (_f, l) ->
731+
| Record (_f, l) ->
732732
List.fold_left (fun fv (_, ty) ->
733733
EcIdent.fv_union fv (ty_fv_and_tvar ty)) Mid.empty l in
734734
List.fold_left (fun fv (id, _) -> Mid.remove id fv) fv tyd.tyd_params
@@ -817,9 +817,9 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
817817
let tosubst = fst_params, tconstr path args in
818818
let tg_subst, tyd_type =
819819
match tydecl.tyd_type with
820-
| `Concrete _ | `Abstract _ ->
820+
| Concrete _ | Abstract _ ->
821821
EcSubst.add_tydef to_gen.tg_subst path tosubst, tydecl.tyd_type
822-
| `Record (f, prs) ->
822+
| Record (f, prs) ->
823823
let subst = EcSubst.empty in
824824
let tg_subst = to_gen.tg_subst in
825825
let subst = EcSubst.add_tydef subst path tosubst in
@@ -836,8 +836,8 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
836836
in
837837
let prs = List.map add_op prs in
838838
let f = EcSubst.subst_form !rsubst f in
839-
!rtg_subst, `Record (f, prs)
840-
| `Datatype dt ->
839+
!rtg_subst, Record (f, prs)
840+
| Datatype dt ->
841841
let subst = EcSubst.empty in
842842
let tg_subst = to_gen.tg_subst in
843843
let subst = EcSubst.add_tydef subst path tosubst in
@@ -857,7 +857,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
857857
let tydt_ctors = List.map add_op dt.tydt_ctors in
858858
let tydt_schelim = EcSubst.subst_form !rsubst dt.tydt_schelim in
859859
let tydt_schcase = EcSubst.subst_form !rsubst dt.tydt_schcase in
860-
!rtg_subst, `Datatype {tydt_ctors; tydt_schelim; tydt_schcase }
860+
!rtg_subst, Datatype {tydt_ctors; tydt_schelim; tydt_schcase }
861861

862862
in
863863

@@ -1145,7 +1145,7 @@ let sc_decl_mod (id,mt) = SC_decl_mod (id,mt)
11451145
(* ---------------------------------------------------------------- *)
11461146

11471147
let is_abstract_ty = function
1148-
| `Abstract _ -> true
1148+
| Abstract _ -> true
11491149
| _ -> false
11501150

11511151
(*

0 commit comments

Comments
 (0)