From bad63e3aabcec04a8796ad177b5c4ca8046bd042 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Dec 2023 16:03:42 +0100 Subject: [PATCH] separate synterp phase --- HB/builders.elpi | 17 ++- HB/common/stdpp.elpi | 5 - HB/common/utils-synterp.elpi | 70 +++++++++ HB/common/utils.elpi | 54 +------ HB/instance.elpi | 2 +- HB/lock.elpi | 44 ------ HB/structure.elpi | 2 +- examples/hulk.v | 2 +- structures.v | 267 ++++++++++++++++++++++++++--------- tests/exports.v | 1 + tests/hnf.v.out | 2 +- 11 files changed, 287 insertions(+), 179 deletions(-) create mode 100644 HB/common/utils-synterp.elpi delete mode 100644 HB/lock.elpi diff --git a/HB/builders.elpi b/HB/builders.elpi index f32a31ed1..37493db36 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -5,21 +5,21 @@ namespace builders { pred begin i:context-decl. begin CtxSkel :- std.do! [ - Name is "Builders_" ^ {std.any->string {new_int}}, % TODO? + std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module", if-verbose (coq.say {header} "begin module for builders"), log.coq.env.begin-module Name none, builders.private.factory CtxSkel IDF GRF, % the Super module to access operations/axioms shadowed by the ones in the factory + if-verbose (coq.say {header} "begin module Super"), + log.coq.env.begin-module "Super" none, if (GRF = indt FRecord) (std.do! [ - if-verbose (coq.say {header} "begin module Super"), - log.coq.env.begin-module "Super" none, std.forall {coq.env.projections FRecord} builders.private.declare-shadowed-constant, - log.coq.env.end-module-name "Super" _, - if-verbose (coq.say {header} "ended module Super") - ]) (true), + ]) true, + if-verbose (coq.say {header} "ended module Super"), + log.coq.env.end-module-name "Super" _, log.coq.env.begin-section Name, if-verbose (coq.say {header} "postulating factories"), @@ -31,7 +31,7 @@ begin CtxSkel :- std.do! [ % "end" is a keyword, be put it in the namespace by hand pred builders.end. builders.end :- std.do! [ - current-mode (builder-from _ _ GR ModName), + current-mode (builder-from _ _ _ ModName), log.coq.env.end-section-name ModName, @@ -48,8 +48,7 @@ builders.end :- std.do! [ std.filter ExportClauses (export.private.abbrev-in-module CurModPath) ExportClausesFiltered, % TODO: Do we need this module? - gref->modname GR 1 "" M, - Name is M ^ "_Exports", + std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module", log.coq.env.begin-module Name none, acc-clauses current Clauses, diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index fac753e44..5a5b85e10 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -118,11 +118,6 @@ constraint print-ctx mixin-src { %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% approximation, it should be logical path, not the file name -pred coq.env.current-library o:string. -coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. -coq.env.current-library "dummy.v". - pred coq.term-is-gref? i:term, o:gref. coq.term-is-gref? (global GR) GR :- !. coq.term-is-gref? (pglobal GR _) GR :- !. diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi new file mode 100644 index 000000000..39fb91867 --- /dev/null +++ b/HB/common/utils-synterp.elpi @@ -0,0 +1,70 @@ +/* Hierarchy Builder: algebraic hierarchies made easy + This software is released under the terms of the MIT license */ + +% runs P in a context where Coq #[attributes] are parsed +pred with-attributes i:prop. +with-attributes P :- + attributes A, + coq.parse-attributes A [ + att "verbose" bool, + att "mathcomp" bool, + att "mathcomp.axiom" string, + att "short.type" string, + att "short.pack" string, + att "key" string, + att "arg_sort" bool, + att "log" bool, + att "log.raw" bool, + att "compress_coercions" bool, + att "export" bool, + att "skip" string, + att "local" bool, + att "fail" bool, + att "doc" string, + att "primitive" bool, + att "non_forgetful_inheritance" bool, + att "hnf" bool, + ] Opts, !, + Opts => (save-docstring, P). + +pred if-verbose i:prop. +if-verbose P :- get-option "verbose" tt, !, P. +if-verbose _. + +% header of if-verbose messages +pred header o:string. +header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ". + +% approximation, it should be logical path, not the file name +pred coq.env.current-library o:string. +coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. +coq.env.current-library "dummy.v". + +% this is only declared in hb.db, this declaration is only to avoid a warning +pred docstring o:loc, o:string. + +pred save-docstring. +save-docstring :- + if (get-option "elpi.loc" Loc, get-option "elpi.phase" "interp", get-option "doc" Txt) + (coq.elpi.accumulate _ "hb.db" (clause _ _ (docstring Loc Txt))) + true. + +pred compute-filter i:option string, o:list string. +compute-filter none []. +compute-filter (some S) MFilter :- % S is a component of the current modpath + coq.env.current-path P, + rex_split "\\." S L, + compute-filter.aux P L MFilter, !. +compute-filter (some S) MFilter :- + coq.locate-module S M, + coq.modpath->path M MFilter. +compute-filter.aux [S|_] [S] [S] :- !. +compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS. +compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS. + +pred list-uniq i:list A, o:list A. +pred list-uniq.seen i:A. +list-uniq [] []. +list-uniq [X|XS] YS :- list-uniq.seen X, !, list-uniq XS YS. +list-uniq [X|XS] [X|YS] :- list-uniq.seen X => list-uniq XS YS. + diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index b205154b7..de87dc33f 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -3,56 +3,10 @@ % This file contains some HB specific utilities +accumulate HB/common/utils-synterp. shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }. -% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2 -type attmap attribute-type. - -% runs P in a context where Coq #[attributes] are parsed -pred with-attributes i:prop. -with-attributes P :- - attributes A, - -% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2 -(pi S L AS Prefix R R1 Map PS\ - parse-attributes.aux [attribute S (node L)|AS] Prefix R :- - if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !, - parse-attributes.aux AS Prefix R1, - (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map, - std.append R1 [get-option PS Map] R -) => - - coq.parse-attributes A [ - att "verbose" bool, - att "mathcomp" bool, - att "mathcomp.axiom" string, - att "short.type" string, - att "short.pack" string, - att "key" string, - att "arg_sort" bool, - att "log" bool, - att "log.raw" bool, - att "compress_coercions" bool, - att "export" bool, - att "skip" string, - att "local" bool, - att "fail" bool, - att "doc" string, - att "primitive" bool, - att "non_forgetful_inheritance" bool, - att "hnf" bool, - ] Opts, !, - Opts => (save-docstring, P). - -pred if-verbose i:prop. -if-verbose P :- get-option "verbose" tt, !, P. -if-verbose _. - -% header of if-verbose messages -pred header o:string. -header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ". - pred if-arg-sort i:prop. if-arg-sort P :- get-option "arg_sort" tt, !, P. if-arg-sort _. @@ -78,12 +32,6 @@ pred acc-clauses i:scope, i:list prop. acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}. */ -pred save-docstring. -save-docstring :- - if (get-option "elpi.loc" Loc, get-option "doc" Txt) - (acc-clause _ (docstring Loc Txt)) - true. - % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?) % Should we make this an HO predicate, eg "located->gref S L is-factory? GR" % TODO: rename since this is HB specific and is expected to return a factory diff --git a/HB/instance.elpi b/HB/instance.elpi index 7e931d49b..2eec1d08b 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -35,7 +35,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [ if-verbose (coq.say "HB: skipping section opening"), SectionBody = Body ) ( - SectionName is "hb_instance_" ^ {std.any->string {new_int}}, + std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section", log.coq.env.begin-section SectionName, private.postulate-arity TyWP [] Body SectionBody SectionTy ), diff --git a/HB/lock.elpi b/HB/lock.elpi deleted file mode 100644 index 65d6c0361..000000000 --- a/HB/lock.elpi +++ /dev/null @@ -1,44 +0,0 @@ -/* Hierarchy Builder: algebraic hierarchies made easy - This software is released under the terms of the MIT license */ - - -namespace lock { - -pred lock-def i:id, i:arity, i:term. -lock-def Name AritySkel BoSkel :- std.do! [ - std.assert-ok! (coq.elaborate-arity-skeleton AritySkel _ Arity) "HB: type illtyped", - coq.arity->term Arity Ty, - std.assert-ok! (coq.elaborate-skeleton BoSkel Ty Bo) "HB: body illtyped", - - NameTy is Name ^ "Locked", - private.lock-module-type NameTy Ty Bo Signature, - private.lock-module-body Signature NameTy Name Ty Bo C, - - @global! => log.coq.notation.add-abbreviation Name 0 (global (const C)) ff _, -]. - -namespace private { - -pred lock-module-type i:id, i:term, i:term, o:modtypath. -lock-module-type Name Ty Bo M :- std.do! [ - log.coq.env.begin-module-type Name, - log.coq.env.add-parameter "body" Ty C, B = global (const C), - PTY = {{ lib:@hb.eq _ lp:B lp:Bo }}, - std.assert-ok! (coq.typecheck-ty PTY _) "HB unlock statement illtyped", - log.coq.env.add-parameter "unlock" PTY _, - log.coq.env.end-module-type-name Name M, -]. - -pred lock-module-body o:modtypath, i:id, i:id, i:term, i:term, o:constant. -lock-module-body Signature SignatureName Name Ty Bo C:- std.do! [ - log.coq.env.begin-module Name (some (pr Signature SignatureName)), - log.coq.env.add-const "body" Bo Ty @transparent! C, B = global (const C), - P = {{ lib:@hb.erefl lp:Ty lp:B }}, - std.assert-ok! (coq.typecheck P _) "HB unlock proof illtyped", - PTY = {{ lib:@hb.eq _ lp:B lp:Bo }}, - std.assert-ok! (coq.typecheck-ty PTY _) "HB unlock statement illtyped", - log.coq.env.add-const "unlock" P PTY @opaque! _, - log.coq.env.end-module-name Name _, -]. - -}} \ No newline at end of file diff --git a/HB/structure.elpi b/HB/structure.elpi index 1c715656e..be549496a 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -170,7 +170,7 @@ declare Module BSkel Sort :- std.do! [ if-verbose (coq.say {header} "operations meta-data module: ElpiOperations"), - ElpiOperationModName is "ElpiOperations" ^ {std.any->string {new_int}}, + ElpiOperationModName is {calc (Module ^ "ElpiOperations")}, log.coq.env.begin-module ElpiOperationModName none, acc-clauses current {std.append EX MixinFirstClass}, log.coq.env.end-module-name ElpiOperationModName ElpiOperations, diff --git a/examples/hulk.v b/examples/hulk.v index 60b68c530..d2b802218 100644 --- a/examples/hulk.v +++ b/examples/hulk.v @@ -269,7 +269,7 @@ rewrite new_concept.unlock. Time Fail reflexivity. (* takes 7s, the original body is restored *) Abort. -Print Module Type new_conceptLocked. +Print Module Type new_concept_Locked. Print Module new_concept. (* Module Type new_conceptLocked = Sig diff --git a/structures.v b/structures.v index 9326c4fc1..c1669a5c0 100644 --- a/structures.v +++ b/structures.v @@ -55,9 +55,9 @@ Global Open Scope HB_scope. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (** This data represents the hierarchy and some other piece of state to - implement the commands above *) + implement the commands of this file *) -Elpi Db hb.db lp:{{ +#[interp] Elpi Db hb.db lp:{{ typeabbrev mixinname gref. typeabbrev classname gref. @@ -234,6 +234,15 @@ pred docstring o:loc, o:string. }}. +(* This database is used by the parsing phase only *) +#[synterp] Elpi Db export.db lp:{{ + % the middle argument [id] is useless, but to preserve compat with < 8.18 + % we keep the same signature found in hb.db + pred module-to-export o:string, o:id, o:modpath. + +}}. + + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -444,14 +453,38 @@ Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/export.elpi". Elpi Accumulate File "HB/factory.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +pred record-decl->id i:indt-decl, o:id. +record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N. +record-decl->id (record N _ _ _) N. + +shorten coq.env.{ begin-module, end-module, begin-section, end-section, export-module }. + +pred actions i:id. +actions N :- + begin-module N none, + begin-section N, + end-section, + begin-module "Exports" none, + end-module E, + end-module _, + export-module E, + coq.env.current-library File, + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)). + +main [indt-decl D] :- record-decl->id D N, with-attributes (actions N). + +main _ :- + coq.error "Usage: HB.mixin Record T of F A & … := { … }.". +}}. Elpi Accumulate lp:{{ :name "start" -main [A] :- A = indt-decl _, !, - with-attributes (with-logging (factory.declare-mixin A)). +main [A] :- with-attributes (with-logging (factory.declare-mixin A)). -main _ :- - coq.error "Usage: HB.mixin Record T of F A & … := { … }.". }}. Elpi Typecheck. Elpi Export HB.mixin. @@ -606,16 +639,54 @@ Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/factory.elpi". Elpi Accumulate File "HB/structure.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +shorten coq.env.{ begin-module, end-module, begin-section, end-section, import-module, export-module }. + +pred actions i:id. +actions N :- + begin-module N none, + begin-module "Exports" none, + end-module E, + import-module E, + end-module _, + export-module E, + begin-module {calc (N ^ "ElpiOperations")} none, + end-module O, + export-module O, + coq.env.current-library File, + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)), + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)), + if (get-option "mathcomp" tt ; get-option "mathcomp.axiom" _) (actions-compat N) true. + +pred actions-compat i:id. +actions-compat ModuleName :- + CompatModuleName is "MathCompCompat" ^ ModuleName, + begin-module CompatModuleName none, + begin-module ModuleName none, + end-module _, + end-module O, + export-module O, + % is this a bug? + % coq.env.current-library File, + % coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)). + true. + +main [const-decl N _ _] :- !, with-attributes (actions N). + +main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". +}}. Elpi Accumulate lp:{{ :name "start" -main [const-decl N (some B) Arity] :- !, std.do! [ +main [const-decl N (some B) Arity] :- std.do! [ % compute the universe for the structure (default ) prod-last {coq.arity->term Arity} Ty, if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, with-attributes (with-logging (structure.declare N B Univ)), ]. -main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". }}. Elpi Typecheck. @@ -693,6 +764,18 @@ Elpi Accumulate File "HB/common/log.elpi". Elpi Accumulate File "HB/common/synthesis.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/instance.elpi". +#[synterp] Elpi Accumulate lp:{{ + +shorten coq.env.{ begin-section, end-section }. + +main [const-decl _ _ (arity _)] :- !. +main [const-decl _ _ (parameter _ _ _ _)] :- !, + SectionName is "hb_instance_" ^ {std.any->string {new_int} }, + begin-section SectionName, end-section. +main [_, _] :- !. + +main _ :- coq.error "Usage: HB.instance Definition := T ...". +}}. Elpi Accumulate lp:{{ :name "start" @@ -702,8 +785,6 @@ main [T0, F0] :- !, coq.warning "HB" "HB.deprecated" "The syntax \"HB.instance Key FactoryInstance\" is deprecated, use \"HB.instance Definition\" instead", with-attributes (with-logging (instance.declare-existing T0 F0)). -main _ :- coq.error "Usage: HB.instance Definition := T ...". - }}. Elpi Typecheck. Elpi Export HB.instance. @@ -728,14 +809,39 @@ Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/export.elpi". Elpi Accumulate File "HB/factory.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +pred record-decl->id i:indt-decl, o:id. +record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N. +record-decl->id (record N _ _ _) N. + +shorten coq.env.{ begin-module, end-module, begin-section, end-section, export-module }. + +pred actions i:id. +actions N :- + begin-module N none, + begin-section N, + end-section, + begin-module "Exports" none, + end-module E, + end-module _, + export-module E, + coq.env.current-library File, + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" E)). + +main [indt-decl D] :- record-decl->id D N, with-attributes (actions N). +main [const-decl N _ _] :- with-attributes (actions N). + +main _ :- + coq.error "Usage: HB.factory Record T of F A & … := { … }.\nUsage: HB.factory Definition T of F A := t.". +}}. Elpi Accumulate lp:{{ :name "start" -main [A] :- (A = indt-decl _ ; A = const-decl _ _ _), !, - with-attributes (with-logging (factory.declare A)). +main [A] :- with-attributes (with-logging (factory.declare A)). -main _ :- - coq.error "Usage: HB.factory Record T of F A & … := { … }.\nUsage: HB.factory Definition T of F A := t.". }}. Elpi Typecheck. Elpi Export HB.factory. @@ -791,12 +897,26 @@ Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/export.elpi". Elpi Accumulate File "HB/factory.elpi". Elpi Accumulate File "HB/builders.elpi". -Elpi Accumulate lp:{{ +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate lp:{{ -:name "start" -main [ctx-decl C] :- !, with-attributes (with-logging (builders.begin C)). +shorten coq.env.{ begin-module, end-module, begin-section }. + +pred actions i:id. +actions N :- + begin-module N none, + begin-module "Super" none, + end-module _, + begin-section N. +main [ctx-decl _] :- !, with-attributes (actions {calc ("Builders_" ^ {std.any->string {new_int} })}). + main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).". +}}. +Elpi Accumulate lp:{{ + +:name "start" +main [ctx-decl C] :- with-attributes (with-logging (builders.begin C)). }}. Elpi Typecheck. @@ -816,11 +936,31 @@ Elpi Accumulate File "HB/instance.elpi". Elpi Accumulate File "HB/context.elpi". Elpi Accumulate File "HB/export.elpi". Elpi Accumulate File "HB/builders.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +shorten coq.env.{ end-module, end-section, begin-module, end-module, export-module }. + +pred actions. +actions :- + end-section, + begin-module {calc ("Builders_Export_" ^ {std.any->string {new_int} })} none, + end-module M, + end-module _, + export-module M, + coq.env.current-library File, + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" M)). + +main [] :- !, with-attributes actions. +main _ :- coq.error "Usage: HB.end.". + +}}. + Elpi Accumulate lp:{{ :name "start" -main [] :- !, with-attributes (with-logging builders.end). -main _ :- coq.error "Usage: HB.end.". +main [] :- with-attributes (with-logging builders.end). }}. Elpi Typecheck. @@ -867,6 +1007,23 @@ Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/utils.elpi". Elpi Accumulate File "HB/common/log.elpi". Elpi Accumulate File "HB/export.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +shorten coq.env.{ export-module }. + +pred actions i:list located. +actions [loc-modpath MP] :- !, + export-module MP, + coq.env.current-library File, + coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" MP)). +actions []. + +main [str M] :- !, with-attributes (actions {coq.locate-all M}). +main _ :- coq.error "Usage: HB.export M.". + +}}. Elpi Accumulate lp:{{ :name "start" @@ -896,6 +1053,31 @@ Elpi Accumulate File "HB/common/database.elpi". Elpi Accumulate File "HB/common/utils.elpi". Elpi Accumulate File "HB/common/log.elpi". Elpi Accumulate File "HB/export.elpi". +#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi". +#[synterp] Elpi Accumulate Db export.db. +#[synterp] Elpi Accumulate lp:{{ + +shorten coq.env.{ export-module }. + +pred module-in-module i:list string, i:prop. +module-in-module PM (module-to-export _ _ M) :- + coq.modpath->path M PC, + std.appendR PM _ PC. % sublist + +pred actions i:option id. +actions Filter :- + coq.env.current-library File, + compute-filter Filter MFilter, + std.findall (module-to-export File _ Module_) ModsCL, + std.filter {list-uniq ModsCL} (module-in-module MFilter) ModsCLFiltered, + std.forall ModsCLFiltered (x\sigma mp\x = module-to-export _ _ mp, export-module mp). + +main [] :- !, with-attributes (actions none). +main [str M] :- !, with-attributes (actions (some M)). +main _ :- coq.error "Usage: HB.reexport.". + + +}}. Elpi Accumulate lp:{{ :name "start" @@ -911,51 +1093,9 @@ Elpi Export HB.reexport. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(** [HB.lock] hides the body of a definition behind a sealed module. - - Syntax to lock: - -[[ -HB.lock Definition foo : ty := t. -]] - - Pseudocode: - -[[ -Module Type fooLocked. -Parameter body : ty. -Parameter unlock : body = t. -End fooLocked. - -Module foo : fooLocked. -Definition body : ty := t. -Lemma unlock : body = t. Proof. by []. Qed. -End foo. - -Notation foo := foo.body. -]] -*) - -#[arguments(raw)] Elpi Command HB.lock. -Elpi Accumulate Db hb.db. -Elpi Accumulate File "HB/common/stdpp.elpi". -Elpi Accumulate File "HB/common/database.elpi". -#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi". -#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi". -Elpi Accumulate File "HB/common/utils.elpi". -Elpi Accumulate File "HB/common/log.elpi". -Elpi Accumulate File "HB/lock.elpi". -Elpi Accumulate lp:{{ - -:name "start" -main [const-decl Name (some BoSkel) TySkel] :- !, - with-attributes (with-logging (lock.lock-def Name TySkel BoSkel)). -main _ :- coq.error "Usage: HB.lock Definition name : ty := t.". - -}}. -Elpi Typecheck. -Elpi Export HB.lock. +From elpi.apps Require Import locker. +Elpi Export mlock As HB.lock. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -1056,7 +1196,6 @@ check-or-not Skel :- Elpi Typecheck. Elpi Export HB.check. - (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) diff --git a/tests/exports.v b/tests/exports.v index b92d7de15..687e70289 100644 --- a/tests/exports.v +++ b/tests/exports.v @@ -22,6 +22,7 @@ HB.mixin Record Ring_of_TYPE A := { mulrDl : left_distributive mul add; mulrDr : right_distributive mul add; }. +#[mathcomp] HB.structure Definition Ring := { A of Ring_of_TYPE A }. (* Notations *) diff --git a/tests/hnf.v.out b/tests/hnf.v.out index 16a06c026..b35edbc76 100644 --- a/tests/hnf.v.out +++ b/tests/hnf.v.out @@ -8,5 +8,5 @@ Datatypes_bool__canonical__hnf_S = {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} : S.type HB_unnamed_mixin_12 = -Builders_2.HB_unnamed_factory_4 bool HB_unnamed_factory_9 +Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9 : M.axioms_ bool