From 4f81cc44e5af01f40ad972a7285edd2c40c178c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Mar 2020 01:04:46 -0500 Subject: [proof] Start of mutual definition save refactoring. First commit of a series that will unify (and enforce) the handling of mutual constants. We will split this in several commits as to easy debugging / bisect in case of problems. In this first commit, we move the actual declare logic to a common place. --- vernac/declareDef.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 09582f4ef2..edf7ed9dc3 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,6 +69,13 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref +let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = + CList.map4 + (fun name body types impargs -> + let ce = Declare.definition_entry ~opaque ~types ~univs body in + declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + fixnames fixdecls fixtypes fiximps + let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ -- cgit v1.2.3 From a0296d51711cdd42f201b9d0e937266984a20944 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 01:49:07 -0400 Subject: [proof] Factorize call info message in mutual declarations --- vernac/declareDef.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index edf7ed9dc3..9708f43e53 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,12 +69,15 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref -let declare_mutually_recursive ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = - CList.map4 - (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque ~types ~univs body in - declare_definition ~name ~scope ~kind ~ubind ~impargs ce) - fixnames fixdecls fixtypes fiximps +let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = + let csts = CList.map4 + (fun name body types impargs -> + let ce = Declare.definition_entry ~opaque ~types ~univs body in + declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + fixnames fixdecls fixtypes fiximps + in + Declare.recursive_message (not cofix) indexes fixnames; + csts let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" -- cgit v1.2.3 From 09d6197bd11ed4a323b335118ae749d7caefeb55 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 01:51:37 -0400 Subject: [proof] [mutual] Factorize notation declaration. --- vernac/declareDef.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 9708f43e53..b3bcf58b4a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,7 +69,7 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref -let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind fixnames fixdecls fixtypes fiximps = +let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps = let csts = CList.map4 (fun name body types impargs -> let ce = Declare.definition_entry ~opaque ~types ~univs body in @@ -77,6 +77,7 @@ let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubin fixnames fixdecls fixtypes fiximps in Declare.recursive_message (not cofix) indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts let warn_let_as_axiom = -- cgit v1.2.3 From affb6ac843380e8e134fd89380746f2f6f8c11de Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 02:09:03 -0400 Subject: [proof] [mutual] Factorize mutual body construction. --- vernac/declareDef.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index b3bcf58b4a..ba84734360 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,6 +69,19 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref +let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes = + match possible_indexes with + | Some possible_indexes -> + let env = Global.env() in + let indexes = Pretyping.search_guard env possible_indexes rec_declaration in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in + vars, fixdecls, Some indexes + | None -> + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps = let csts = CList.map4 (fun name body types impargs -> -- cgit v1.2.3 From a15e584571a4e153e98a11c93d12759c45ea2dcd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 02:22:59 -0400 Subject: [proof] [mutual] Factorize universe handling. Note that we had to introduce a `restrict_ucontext` parameter to be faithful to the implementation in obligations, however this looks like a bug. --- vernac/declareDef.ml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index ba84734360..de7223ae62 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -82,14 +82,29 @@ let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes = let vars = Vars.universes_of_constr (List.hd fixdecls) in vars, fixdecls, None -let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps = +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps = + let vars, fixdecls, indexes = + mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in + let ubind, univs = + (* XXX: Note that obligations don't do this, is that a bug? *) + if restrict_ucontext + then + let evd = Evd.from_ctx uctx in + let evd = Evd.restrict_universe_context evd vars in + let univs = Evd.check_univ_decl ~poly evd udecl in + Evd.universe_binders evd, univs + else + let univs = UState.univ_entry ~poly uctx in + UnivNames.empty_binders, univs + in let csts = CList.map4 (fun name body types impargs -> let ce = Declare.definition_entry ~opaque ~types ~univs body in declare_definition ~name ~scope ~kind ~ubind ~impargs ce) fixnames fixdecls fixtypes fiximps in - Declare.recursive_message (not cofix) indexes fixnames; + let isfix = Option.is_empty possible_indexes in + Declare.recursive_message isfix indexes fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts -- cgit v1.2.3 From 8129fb2abce6ba2e5ddd1f384618bb2fb8f817b5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 02:47:01 -0400 Subject: [proof] [mutual] Factorize mutual per-entry information We move `Recthm` to `DeclareDef` so it is shared by interactive and direct fixpoint declaration. This is the last step before unifying both paths. --- vernac/declareDef.ml | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index de7223ae62..6e19cf97b0 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -69,22 +69,35 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = end; dref -let mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes = +let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> let env = Global.env() in let indexes = Pretyping.search_guard env possible_indexes rec_declaration in let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in - let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixnames in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in vars, fixdecls, Some indexes | None -> - let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in let vars = Vars.universes_of_constr (List.hd fixdecls) in vars, fixdecls, None -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixnames fixtypes fiximps = +module Recthm = struct + type t = + { name : Names.Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Names.Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixitems = let vars, fixdecls, indexes = - mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in + mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in let ubind, univs = (* XXX: Note that obligations don't do this, is that a bug? *) if restrict_ucontext @@ -97,13 +110,14 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re let univs = UState.univ_entry ~poly uctx in UnivNames.empty_binders, univs in - let csts = CList.map4 - (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque ~types ~univs body in + let csts = CList.map2 + (fun Recthm.{ name; typ; impargs } body -> + let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in declare_definition ~name ~scope ~kind ~ubind ~impargs ce) - fixnames fixdecls fixtypes fiximps + fixitems fixdecls in let isfix = Option.is_empty possible_indexes in + let fixnames = List.map (fun { Recthm.name } -> name) fixitems in Declare.recursive_message isfix indexes fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts -- cgit v1.2.3 From b623017fea475b7b91c99f462b0fe2458bfe91e7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Mar 2020 23:52:31 -0400 Subject: [declare] make restrict_ucontext an optional parameter. The current API does just exist as a workaround for a bug. --- vernac/declareDef.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/declareDef.ml') diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 6e19cf97b0..fc53abdcea 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -95,11 +95,11 @@ module Recthm = struct } end -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ~restrict_ucontext fixitems = +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in let ubind, univs = - (* XXX: Note that obligations don't do this, is that a bug? *) + (* XXX: Obligations don't do this, this seems like a bug? *) if restrict_ucontext then let evd = Evd.from_ctx uctx in -- cgit v1.2.3