Skip to content

Commit 4d63793

Browse files
yannl35133yannl35133
committed
Cleanup around DefAttributes
1 parent c08bb75 commit 4d63793

File tree

2 files changed

+37
-53
lines changed

2 files changed

+37
-53
lines changed

‎plugins/derive/derive.ml‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,11 @@ let rec fill_assumptions env sigma = function
4343
and [lemma] as the proof. *)
4444
let start_deriving ~atts bl suchthat name : Declare.Proof.t =
4545

46-
let scope, _local, poly, program_mode, user_warns, typing_flags, using, clearbody =
47-
atts.scope, atts.locality, atts.poly, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
46+
let {
47+
scope; poly; program=program_mode;
48+
user_warns; typing_flags; using; clearbody;
49+
} = atts
50+
in
4851
if program_mode then CErrors.user_err (Pp.str "Program mode not supported.");
4952

5053
let env = Global.env () in

‎vernac/vernacentries.ml‎

Lines changed: 32 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -829,8 +829,7 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
829829
then
830830
user_err ?loc (Id.print id ++ str " already exists.")
831831

832-
let vernac_definition_hook ~atts ~canonical_instance ~local ~poly ~reversible kind =
833-
let hooks = atts.DefAttributes.hooks in
832+
let vernac_definition_hook ~hooks ~canonical_instance ~local ~poly ~reversible kind =
834833
let hooks =
835834
let open Decls in
836835
let open Declare.Hook in
@@ -872,40 +871,37 @@ let vernac_definition_name lid local =
872871
lid.v
873872

874873
let vernac_definition_interactive ~atts (discharge, kind) (lid, udecl) bl t =
875-
let open DefAttributes in
876-
let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
877-
atts.scope, atts.locality, atts.poly, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
878-
let hook =
879-
let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
880-
vernac_definition_hook ~atts ~canonical_instance ~local ~poly ~reversible kind
874+
let DefAttributes.{
875+
scope; locality=local; poly; program=program_mode; hooks;
876+
user_warns; typing_flags; using; clearbody; canonical_instance; reversible;
877+
} = atts
881878
in
879+
let hook = vernac_definition_hook ~hooks ~canonical_instance ~local ~poly ~reversible kind in
882880
let name = vernac_definition_name lid scope in
883-
ComDefinition.do_definition_interactive ?loc:lid.loc ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody:atts.clearbody
884-
~kind:(Decls.IsDefinition kind) ?user_warns ?using:atts.using ?hook udecl bl t
881+
ComDefinition.do_definition_interactive ?loc:lid.loc ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody
882+
~kind:(Decls.IsDefinition kind) ?user_warns ?using ?hook udecl bl t
885883

886884
let vernac_definition_refine ~atts (discharge, kind) (lid, udecl) bl red_option c typ_opt =
887885
if Option.has_some red_option then
888886
CErrors.user_err ?loc:c.loc Pp.(str "Cannot use Eval with #[refine].");
889-
let open DefAttributes in
890-
let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
891-
atts.scope, atts.locality, atts.poly, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
892-
let hook =
893-
let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
894-
vernac_definition_hook ~atts ~canonical_instance ~local ~poly kind ~reversible
887+
let DefAttributes.{
888+
scope; locality=local; poly; program=program_mode; hooks;
889+
user_warns; typing_flags; using; clearbody; canonical_instance; reversible;
890+
} = atts
895891
in
892+
let hook = vernac_definition_hook ~hooks ~canonical_instance ~local ~poly kind ~reversible in
896893
let name = vernac_definition_name lid scope in
897894
ComDefinition.do_definition_refine ~name ?loc:lid.loc
898895
?clearbody ~poly ~typing_flags ~scope ~kind:(Decls.IsDefinition kind)
899896
?user_warns ?using udecl bl c typ_opt ?hook
900897

901898
let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c typ_opt =
902-
let open DefAttributes in
903-
let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
904-
atts.scope, atts.locality, atts.poly, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
905-
let hook =
906-
let canonical_instance, reversible = atts.canonical_instance, atts.reversible in
907-
vernac_definition_hook ~atts ~canonical_instance ~local ~poly kind ~reversible
899+
let DefAttributes.{
900+
scope; locality=local; poly; program=program_mode; hooks;
901+
user_warns; typing_flags; using; clearbody; canonical_instance; reversible;
902+
} = atts
908903
in
904+
let hook = vernac_definition_hook ~hooks ~canonical_instance ~local ~poly kind ~reversible in
909905
let name = vernac_definition_name lid scope in
910906
let red_option = match red_option with
911907
| None -> None
@@ -927,12 +923,13 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c t
927923

928924
(* NB: pstate argument to use combinators easily *)
929925
let vernac_start_proof ~atts kind l =
930-
let open DefAttributes in
931926
if Dumpglob.dump () then
932927
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
933-
let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody =
934-
atts.scope, atts.locality, atts.poly,
935-
atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in
928+
let DefAttributes.{
929+
scope; locality=local; poly; program=program_mode;
930+
user_warns; typing_flags; using; clearbody;
931+
} = atts
932+
in
936933
List.iter (fun ((id, _), _) -> check_name_freshness scope id) l;
937934
match l with
938935
| [] -> assert false
@@ -972,9 +969,7 @@ let vernac_exact_proof ~lemma ~pm c =
972969
pm
973970

974971
let vernac_assumption ~atts kind l inline =
975-
let open DefAttributes in
976-
let scope, poly, program_mode, using, user_warns =
977-
atts.scope, atts.poly, atts.program, atts.using, atts.user_warns in
972+
let DefAttributes.{ scope; poly; program=program_mode; using; user_warns; } = atts in
978973
if Option.has_some using then
979974
Attributes.unsupported_attributes [CAst.make ("using",VernacFlagEmpty)];
980975
ComAssumption.do_assumptions ~poly ~program_mode ~scope ~kind ?user_warns ~inline l
@@ -1329,13 +1324,6 @@ let vernac_inductive ~atts kind indl =
13291324
let preprocess_inductive_decl ~atts kind indl =
13301325
snd @@ preprocess_inductive_decl ~atts kind indl
13311326

1332-
let vernac_fixpoint_common ~atts l =
1333-
if Dumpglob.dump () then
1334-
List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
1335-
let scope = atts.DefAttributes.scope in
1336-
List.iter (fun { fname } -> check_name_freshness scope fname) l;
1337-
scope
1338-
13391327
let with_obligations program_mode f pm =
13401328
if program_mode then
13411329
f pm ~program_mode:true
@@ -1345,10 +1333,10 @@ let with_obligations program_mode f pm =
13451333
pm, proof
13461334

13471335
let vernac_fixpoint ~atts ~refine ~pm (rec_order,fixl) =
1348-
let open DefAttributes in
1349-
let scope = vernac_fixpoint_common ~atts fixl in
1350-
let poly, typing_flags, program_mode, clearbody, using, user_warns =
1351-
atts.poly, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in
1336+
let DefAttributes.{ scope; poly; typing_flags; program=program_mode; clearbody; using; user_warns; } = atts in
1337+
if Dumpglob.dump () then
1338+
List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") fixl;
1339+
List.iter (fun { fname } -> check_name_freshness scope fname) fixl;
13521340
let () =
13531341
if program_mode then
13541342
(* XXX: Switch to the attribute system and match on ~atts *)
@@ -1358,18 +1346,11 @@ let vernac_fixpoint ~atts ~refine ~pm (rec_order,fixl) =
13581346
(fun pm -> ComFixpoint.do_mutually_recursive ?pm ~refine ~scope ?clearbody ~kind:(IsDefinition Fixpoint) ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl))
13591347
pm
13601348

1361-
let vernac_cofixpoint_common ~atts l =
1362-
if Dumpglob.dump () then
1363-
List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
1364-
let scope = atts.DefAttributes.scope in
1365-
List.iter (fun { fname } -> check_name_freshness scope fname) l;
1366-
scope
1367-
13681349
let vernac_cofixpoint ~pm ~refine ~atts cofixl =
1369-
let open DefAttributes in
1370-
let scope = vernac_cofixpoint_common ~atts cofixl in
1371-
let poly, typing_flags, program_mode, clearbody, using, user_warns =
1372-
atts.poly, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in
1350+
let DefAttributes.{ scope; poly; typing_flags; program=program_mode; clearbody; using; user_warns; } = atts in
1351+
if Dumpglob.dump () then
1352+
List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") cofixl;
1353+
List.iter (fun { fname } -> check_name_freshness scope fname) cofixl;
13731354
let () =
13741355
if program_mode then
13751356
let opens = List.exists (fun { body_def } -> Option.is_empty body_def) cofixl in

0 commit comments

Comments
 (0)