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/comFixpoint.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0a70954dd2..4e5b1d7205 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -279,12 +279,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fiximps = List.map (fun (n,r,p) -> r) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in + let univs = Evd.check_univ_decl ~poly evd pl in let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - List.map4 (fun name body types impargs -> - let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in - DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce) + DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind fixnames fixdecls fixtypes fiximps in Declare.recursive_message (not cofix) gidx fixnames; -- 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/comFixpoint.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 4e5b1d7205..55ef0f67d6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -264,7 +264,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, gidx = + let vars, fixdecls, indexes = if not cofix then let env = Global.env() in let indexes = Pretyping.search_guard env indexes fixdecls in @@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let univs = Evd.check_univ_decl ~poly evd pl in let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind + DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind fixnames fixdecls fixtypes fiximps in - Declare.recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () -- 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/comFixpoint.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 55ef0f67d6..ced9656218 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -282,10 +282,9 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let univs = Evd.check_univ_decl ~poly evd pl in let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind + DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps in - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; () let extract_decreasing_argument ~structonly { CAst.v = v; _ } = -- 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/comFixpoint.ml | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index ced9656218..6e6be4fe3a 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -256,26 +256,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs lemma let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let indexes, cofix, fix_kind = + let possible_indexes, cofix, fix_kind = match indexes with - | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint) - | None -> [], true, Decls.(IsDefinition CoFixpoint) + | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint) + | None -> None, true, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, indexes = - if not cofix then - let env = Global.env() in - let indexes = Pretyping.search_guard env indexes fixdecls in - let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in - let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in - vars, fixdecls, Some indexes - else (* cofix *) - let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None - in + let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in -- 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/comFixpoint.ml | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6e6be4fe3a..0e2d8c1453 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,24 +255,20 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let possible_indexes, cofix, fix_kind = +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = + let possible_indexes, fix_kind = match indexes with - | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint) - | None -> None, true, Decls.(IsDefinition CoFixpoint) + | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint) + | None -> None, Decls.(IsDefinition CoFixpoint) in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let univs = Evd.check_univ_decl ~poly evd pl in - let ubind = Evd.universe_binders evd in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~indexes ~cofix ~scope ~opaque:false ~univs ~kind:fix_kind ~ubind ~ntns - fixnames fixdecls fixtypes fiximps + DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + fixnames fixtypes fiximps in () -- 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/comFixpoint.ml | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0e2d8c1453..6580495295 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -236,16 +236,22 @@ let interp_fixpoint ~cofix l = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = - let fix_kind, cofix, indexes = match indexes with - | Some indexes -> Decls.Fixpoint, false, indexes - | None -> Decls.CoFixpoint, true, [] +let build_recthms ~indexes fixnames fixtypes fiximps = + let fix_kind, cofix = match indexes with + | Some indexes -> Decls.Fixpoint, false + | None -> Decls.CoFixpoint, true in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { Lemmas.Recthm.name; typ + { DeclareDef.Recthm.name; typ ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) - fixnames fixtypes fiximps in + fixnames fixtypes fiximps + in + fix_kind, cofix, thms + +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = + let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in + let indexes = Option.default [] indexes in let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = @@ -256,19 +262,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs lemma let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = - let possible_indexes, fix_kind = - match indexes with - | Some indexes -> Some indexes, Decls.(IsDefinition Fixpoint) - | None -> None, Decls.(IsDefinition CoFixpoint) - in (* We shortcut the proof process *) + let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in + let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration - fixnames fixtypes fiximps + ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + fixitems in () -- cgit v1.2.3