Skip to content

Commit f1e2059

Browse files
loutrloutr
committed
style: use regular datatype for ty_body
1 parent 48a21c3 commit f1e2059

File tree

11 files changed

+102
-99
lines changed

11 files changed

+102
-99
lines changed

‎src/ecDecl.ml‎

Lines changed: 18 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -15,36 +15,37 @@ 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 ty_dtype = {
19+
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
20+
tydt_schelim : EcCoreFol.form;
21+
tydt_schcase : EcCoreFol.form;
22+
}
23+
24+
type ty_body =
25+
| Concrete of EcTypes.ty
26+
| Abstract of Sp.t
27+
| Datatype of ty_dtype
28+
| Record of EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
29+
30+
1831
type tydecl = {
1932
tyd_params : ty_params;
2033
tyd_type : ty_body;
2134
tyd_loca : locality;
2235
}
2336

24-
and ty_body = [
25-
| `Concrete of EcTypes.ty
26-
| `Abstract of Sp.t
27-
| `Datatype of ty_dtype
28-
| `Record of EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
29-
]
30-
31-
and ty_dtype = {
32-
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
33-
tydt_schelim : EcCoreFol.form;
34-
tydt_schcase : EcCoreFol.form;
35-
}
3637

3738
let tydecl_as_concrete (td : tydecl) =
38-
match td.tyd_type with `Concrete x -> Some x | _ -> None
39+
match td.tyd_type with Concrete x -> Some x | _ -> None
3940

4041
let tydecl_as_abstract (td : tydecl) =
41-
match td.tyd_type with `Abstract x -> Some x | _ -> None
42+
match td.tyd_type with Abstract x -> Some x | _ -> None
4243

4344
let tydecl_as_datatype (td : tydecl) =
44-
match td.tyd_type with `Datatype x -> Some x | _ -> None
45+
match td.tyd_type with Datatype x -> Some x | _ -> None
4546

4647
let tydecl_as_record (td : tydecl) =
47-
match td.tyd_type with `Record x -> Some x | _ -> None
48+
match td.tyd_type with Record (x, y) -> Some (x, y) | _ -> None
4849

4950
(* -------------------------------------------------------------------- *)
5051
let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
@@ -59,7 +60,7 @@ let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
5960
(EcUid.NameGen.bulk ~fmt n)
6061
in
6162

62-
{ tyd_params = params; tyd_type = `Abstract tc; tyd_loca = lc; }
63+
{ tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; }
6364

6465
(* -------------------------------------------------------------------- *)
6566
let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =

‎src/ecDecl.mli‎

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -11,25 +11,26 @@ 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 ty_dtype = {
15+
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
16+
tydt_schelim : EcCoreFol.form;
17+
tydt_schcase : EcCoreFol.form;
18+
}
19+
20+
type ty_body =
21+
| Concrete of EcTypes.ty
22+
| Abstract of Sp.t
23+
| Datatype of ty_dtype
24+
| Record of EcCoreFol.form * (EcSymbols.symbol * EcTypes.ty) list
25+
26+
1427
type tydecl = {
1528
tyd_params : ty_params;
29+
(* tyd_positivity : bool list; *)
1630
tyd_type : ty_body;
1731
tyd_loca : locality;
1832
}
1933

20-
and ty_body = [
21-
| `Concrete of EcTypes.ty
22-
| `Abstract of Sp.t
23-
| `Datatype of ty_dtype
24-
| `Record of form * (EcSymbols.symbol * EcTypes.ty) list
25-
]
26-
27-
and ty_dtype = {
28-
tydt_ctors : (EcSymbols.symbol * EcTypes.ty list) list;
29-
tydt_schelim : form;
30-
tydt_schcase : form;
31-
}
32-
3334
val tydecl_as_concrete : tydecl -> EcTypes.ty option
3435
val tydecl_as_abstract : tydecl -> Sp.t option
3536
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
@@ -776,10 +776,10 @@ module MC = struct
776776
let loca = tyd.tyd_loca in
777777

778778
match tyd.tyd_type with
779-
| `Concrete _ -> mc
780-
| `Abstract _ -> mc
779+
| Concrete _ -> mc
780+
| Abstract _ -> mc
781781

782-
| `Datatype dtype ->
782+
| Datatype dtype ->
783783
let cs = dtype.tydt_ctors in
784784
let schelim = dtype.tydt_schelim in
785785
let schcase = dtype.tydt_schcase in
@@ -823,7 +823,7 @@ module MC = struct
823823
_up_operator candup mc name (ipath name, op)
824824
) mc projs
825825

826-
| `Record (scheme, fields) ->
826+
| Record (scheme, fields) ->
827827
let params = List.map (fun (x, _) -> tvar x) tyd.tyd_params in
828828
let nfields = List.length fields in
829829
let cfields =
@@ -2513,12 +2513,12 @@ module Ty = struct
25132513
25142514
let defined (name : EcPath.path) (env : env) =
25152515
match by_path_opt name env with
2516-
| Some { tyd_type = `Concrete _ } -> true
2516+
| Some { tyd_type = Concrete _ } -> true
25172517
| _ -> false
25182518
25192519
let unfold (name : EcPath.path) (args : EcTypes.ty list) (env : env) =
25202520
match by_path_opt name env with
2521-
| Some ({ tyd_type = `Concrete body } as tyd) ->
2521+
| Some ({ tyd_type = Concrete body } as tyd) ->
25222522
Tvar.subst
25232523
(Tvar.init (List.map fst tyd.tyd_params) args)
25242524
body
@@ -2554,14 +2554,15 @@ module Ty = struct
25542554
match ty.ty_node with
25552555
| Tconstr (p, tys) -> begin
25562556
match by_path_opt p env with
2557-
| Some ({ tyd_type = (`Datatype _ | `Record _) as body }) ->
2557+
| Some ({ tyd_type = (Datatype _ | Record _) as body }) ->
25582558
let prefix = EcPath.prefix p in
25592559
let basename = EcPath.basename p in
25602560
let basename =
25612561
match body, mode with
2562-
| `Record _, (`Ind | `Case) -> basename ^ "_ind"
2563-
| `Datatype _, `Ind -> basename ^ "_ind"
2564-
| `Datatype _, `Case -> basename ^ "_case"
2562+
| Record _, (`Ind | `Case) -> basename ^ "_ind"
2563+
| Datatype _, `Ind -> basename ^ "_ind"
2564+
| Datatype _, `Case -> basename ^ "_case"
2565+
| _, _ -> assert false
25652566
in
25662567
Some (EcPath.pqoname prefix basename, tys)
25672568
| _ -> None
@@ -2577,7 +2578,7 @@ module Ty = struct
25772578
let env = MC.bind_tydecl name ty env in
25782579
25792580
match ty.tyd_type with
2580-
| `Abstract tc ->
2581+
| Abstract tc ->
25812582
let myty =
25822583
let myp = EcPath.pqname (root env) name in
25832584
let typ = List.map (fst_map EcIdent.fresh) ty.tyd_params in
@@ -2903,7 +2904,7 @@ module Theory = struct
29032904
29042905
| Th_type (x, tyd) -> begin
29052906
match tyd.tyd_type with
2906-
| `Abstract tc ->
2907+
| Abstract tc ->
29072908
let myty =
29082909
let typ = List.map (fst_map EcIdent.fresh) tyd.tyd_params in
29092910
(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
@@ -1272,7 +1272,7 @@ let pp_opapp
12721272
let recp = EcDecl.operator_as_rcrd op in
12731273

12741274
match EcEnv.Ty.by_path_opt recp env with
1275-
| Some { tyd_type = `Record (_, fields) }
1275+
| Some { tyd_type = Record (_, fields) }
12761276
when List.length fields = List.length es
12771277
-> begin
12781278
let wmap =
@@ -2242,12 +2242,12 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) =
22422242

22432243
and pp_body fmt =
22442244
match tyd.tyd_type with
2245-
| `Abstract _ -> () (* FIXME: TC HOOK *)
2245+
| Abstract _ -> () (* FIXME: TC HOOK *)
22462246

2247-
| `Concrete ty ->
2247+
| Concrete ty ->
22482248
Format.fprintf fmt " =@ %a" (pp_type ppe) ty
22492249

2250-
| `Datatype { tydt_ctors = cs } ->
2250+
| Datatype { tydt_ctors = cs } ->
22512251
let pp_ctor fmt (c, cty) =
22522252
match cty with
22532253
| [] ->
@@ -2258,7 +2258,7 @@ let pp_typedecl (ppe : PPEnv.t) fmt (x, tyd) =
22582258
in
22592259
Format.fprintf fmt " =@ [@[<hov 2>%a@]]" (pp_list " |@ " pp_ctor) cs
22602260

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

‎src/ecScope.ml‎

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

19511951
| PTYD_Alias bd ->
19521952
let ue = TT.transtyvars env (loc, Some args) in
19531953
let body = transty tp_tydecl env ue bd in
1954-
EcUnify.UniEnv.tparams ue, `Concrete body
1954+
EcUnify.UniEnv.tparams ue, Concrete body
19551955

19561956
| PTYD_Datatype dt ->
19571957
let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
19581958
let tparams, tydt =
19591959
try ELI.datatype_as_ty_dtype datatype
19601960
with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
19611961
in
1962-
tparams, `Datatype tydt
1962+
tparams, Datatype tydt
19631963

19641964
| PTYD_Record rt ->
19651965
let record = EHI.trans_record env (mk_loc loc (args,name)) rt in
19661966
let scheme = ELI.indsc_of_record record in
1967-
record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
1967+
record.ELI.rc_tparams, Record (scheme, record.ELI.rc_fields)
19681968
in
19691969

19701970
bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; })
@@ -1977,7 +1977,7 @@ module Ty = struct
19771977
let scope =
19781978
let decl = EcDecl.{
19791979
tyd_params = [];
1980-
tyd_type = `Abstract Sp.empty;
1980+
tyd_type = Abstract Sp.empty;
19811981
tyd_loca = `Global; (* FIXME:SUBTYPE *)
19821982
} in bind scope (unloc subtype.pst_name, decl) in
19831983

@@ -2072,7 +2072,7 @@ module Ty = struct
20722072
let asty =
20732073
let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
20742074
{ tyd_params = [];
2075-
tyd_type = `Abstract body;
2075+
tyd_type = Abstract body;
20762076
tyd_loca = (lc :> locality); } in
20772077
let scenv = EcEnv.Ty.bind name asty scenv in
20782078

‎src/ecSection.ml‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -362,12 +362,12 @@ let on_typarams cb typarams =
362362
let on_tydecl (cb : cb) (tyd : tydecl) =
363363
on_typarams cb tyd.tyd_params;
364364
match tyd.tyd_type with
365-
| `Concrete ty -> on_ty cb ty
366-
| `Abstract s -> on_typeclasses cb s
367-
| `Record (f, fds) ->
365+
| Concrete ty -> on_ty cb ty
366+
| Abstract s -> on_typeclasses cb s
367+
| Record (f, fds) ->
368368
on_form cb f;
369369
List.iter (on_ty cb |- snd) fds
370-
| `Datatype dt ->
370+
| Datatype dt ->
371371
List.iter (List.iter (on_ty cb) |- snd) dt.tydt_ctors;
372372
List.iter (on_form cb) [dt.tydt_schelim; dt.tydt_schcase]
373373

@@ -574,7 +574,7 @@ let add_declared_ty to_gen path tydecl =
574574
assert (tydecl.tyd_params = []);
575575
let s =
576576
match tydecl.tyd_type with
577-
| `Abstract s -> s
577+
| Abstract s -> s
578578
| _ -> assert false in
579579

580580
let name = "'" ^ basename path in
@@ -643,14 +643,14 @@ and fv_and_tvar_f f =
643643
let tydecl_fv tyd =
644644
let fv =
645645
match tyd.tyd_type with
646-
| `Concrete ty -> ty_fv_and_tvar ty
647-
| `Abstract _ -> Mid.empty
648-
| `Datatype tydt ->
646+
| Concrete ty -> ty_fv_and_tvar ty
647+
| Abstract _ -> Mid.empty
648+
| Datatype tydt ->
649649
List.fold_left (fun fv (_, l) ->
650650
List.fold_left (fun fv ty ->
651651
EcIdent.fv_union fv (ty_fv_and_tvar ty)) fv l)
652652
Mid.empty tydt.tydt_ctors
653-
| `Record (_f, l) ->
653+
| Record (_f, l) ->
654654
List.fold_left (fun fv (_, ty) ->
655655
EcIdent.fv_union fv (ty_fv_and_tvar ty)) Mid.empty l in
656656
List.fold_left (fun fv (id, _) -> Mid.remove id fv) fv tyd.tyd_params
@@ -739,9 +739,9 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
739739
let tosubst = fst_params, tconstr path args in
740740
let tg_subst, tyd_type =
741741
match tydecl.tyd_type with
742-
| `Concrete _ | `Abstract _ ->
742+
| Concrete _ | Abstract _ ->
743743
EcSubst.add_tydef to_gen.tg_subst path tosubst, tydecl.tyd_type
744-
| `Record (f, prs) ->
744+
| Record (f, prs) ->
745745
let subst = EcSubst.empty in
746746
let tg_subst = to_gen.tg_subst in
747747
let subst = EcSubst.add_tydef subst path tosubst in
@@ -758,8 +758,8 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
758758
in
759759
let prs = List.map add_op prs in
760760
let f = EcSubst.subst_form !rsubst f in
761-
!rtg_subst, `Record (f, prs)
762-
| `Datatype dt ->
761+
!rtg_subst, Record (f, prs)
762+
| Datatype dt ->
763763
let subst = EcSubst.empty in
764764
let tg_subst = to_gen.tg_subst in
765765
let subst = EcSubst.add_tydef subst path tosubst in
@@ -779,7 +779,7 @@ let generalize_tydecl to_gen prefix (name, tydecl) =
779779
let tydt_ctors = List.map add_op dt.tydt_ctors in
780780
let tydt_schelim = EcSubst.subst_form !rsubst dt.tydt_schelim in
781781
let tydt_schcase = EcSubst.subst_form !rsubst dt.tydt_schcase in
782-
!rtg_subst, `Datatype {tydt_ctors; tydt_schelim; tydt_schcase }
782+
!rtg_subst, Datatype {tydt_ctors; tydt_schelim; tydt_schcase }
783783

784784
in
785785

@@ -1066,7 +1066,7 @@ let sc_decl_mod (id,mt) = SC_decl_mod (id,mt)
10661066
(* ---------------------------------------------------------------- *)
10671067

10681068
let is_abstract_ty = function
1069-
| `Abstract _ -> true
1069+
| Abstract _ -> true
10701070
| _ -> false
10711071

10721072
(*

0 commit comments

Comments
 (0)