From c6793857058d4e902edb890fb1c8c58386e7c306 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Jan 2021 18:43:14 +0100 Subject: [PATCH] logging: ability to print vernacular commands Attributes #[log] and #[elpi.log_hb] to get the text in the console or the disk. Utility hb to patch/reset files (replacing calls to HB by their equivalent). --- .github/workflows/main.yml | 21 +- .gitignore | 3 + Makefile.common | 8 + Makefile.coq.local | 16 ++ README.md | 64 +++++ coq-hierarchy-builder.opam | 2 +- demo2/stage10.v | 2 - demo2/stage11.v | 2 - demo5/hierarchy_0.v | 2 - hb.elpi | 462 +++++++++++++++++++++++++++++-------- hb.ml | 186 +++++++++++++++ structures.v | 62 +++-- 12 files changed, 709 insertions(+), 121 deletions(-) create mode 100644 hb.ml diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 728fb9db2..f0425da21 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -29,8 +29,6 @@ jobs: strategy: matrix: coq_version: - - '8.11' - - '8.12' - '8.13' ocaml_version: - 'minimal' @@ -41,3 +39,22 @@ jobs: opam_file: './coq-hierarchy-builder.opam' coq_version: ${{ matrix.coq_version }} ocaml_version: ${{ matrix.ocaml_version }} + + hb-plan-B: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: './coq-hierarchy-builder.opam' + coq_version: '8.13' + ocaml_version: 'minimal' + script: | + mkdir /home/coq/workspace + cp -ra . /home/coq/workspace + cd /home/coq/workspace + COQ_ELPI_ATTRIBUTES=log_hb make -j2 + make patch + make -j2 + make reset + git diff --exit-code diff --git a/.gitignore b/.gitignore index 21e65d20f..94f350cef 100644 --- a/.gitignore +++ b/.gitignore @@ -34,6 +34,9 @@ nra.cache Makefile.coq Makefile.coq.conf .coqdeps.d +*.v.hb +*.v.hb.old +hb _minted-* *.aux diff --git a/Makefile.common b/Makefile.common index 857ddef27..18a26b43c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -128,6 +128,14 @@ endif %.vo: __always__ Makefile.coq +$(COQMAKE) $@ +hb: __always__ Makefile.coq + +$(COQMAKE) $@ + +reset: hb + ./hb reset `find . -name \*.v` +patch: hb + ./hb patch `find . -name \*.v` + doc: __always__ Makefile.coq mkdir -p _build_doc/ cp -r $(COQFILES) -t _build_doc/ --parents diff --git a/Makefile.coq.local b/Makefile.coq.local index 2e73623e1..c0b965f59 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -14,3 +14,19 @@ structures.vo : hb.elpi # $(foreach M,$(shell seq 0 10),\ # $(foreach K,$(shell seq 0 10),\ # $(eval $(call MKRULE,$(N),$(M),$(K)))))) + +pre-all:: hb + +hb: hb.ml + $(SHOW)'OCAMLC hb.ml -o hb' + $(HIDE) ocamlc unix.cma str.cma hb.ml -o hb + +install-extra:: + $(SHOW)'install hb $(dir $(shell which $(COQBIN)coqc))' + $(HIDE) install -m 0755 hb $(dir $(shell which $(COQBIN)coqc)) + +clean:: + $(SHOW)'CLEAN *.hb *.hb.old ./hb' + $(HIDE) find . -name \*.hb -delete + $(HIDE) find . -name \*.hb.old -delete + $(HIDE) rm -f hb \ No newline at end of file diff --git a/README.md b/README.md index ea1cf5612..0a0587159 100644 --- a/README.md +++ b/README.md @@ -143,3 +143,67 @@ prefixed with the attribute `#[verbose]` to get an idea of what they are doing. this seamingly mutual dependency using HB.

+ +#### Plan B + +Scared of making your project depend on HB? This section is for you. + +HB is based on a thick layer of software which we plan to maintain, but we +also understand it can look scary. Hence this insurance plan. By passing +the attribute `#[log]` each command prints Coq commands which are equivalent to +its effect. By replacing each HB command by its equivalent Coq commands, you +can eliminate the dependency on HB from your project. + +This is a "plan B", by looking at the output of`#[log]` you will realize that +HB commands are much nicer (and shorter) than the equivalent Coq code. The +point of a "plan B" is to avoid nightmares, not to be nicer than plan A ;-) + +How can you be ensure plan B works? We provide tools to check that, see +the details below. + +
(click to expand)

+ + +Hierarchy Builder commands can log their equivalent vernacular commands +to "patch" file (extension `.hb`). In order to do so, one has to +compile the project with the `COQ_ELPI_ATTRIBUTES=log_hb` variable set. Eg + +```shell +COQ_ELPI_ATTRIBUTES=log_hb make +``` + +The `hb` command line utility, provided by the `coq-hierarchy-builder` package, +is able to apply the generated patches: it comments out HB commands and +inserts their equivalent Coq commands. + +```shell +hb apply file1.v file2.v ... +``` + +The converse operation can be performed using the following command: + +```shell +hb reset file1.v file2.v ... +``` + +We recommend to setup a CI job testing plan B. If you are using +`docker-coq-action` the following snippet is a good start: + +```yaml + hb-plan-B: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: './your-project.opam' # depends on coq-hierarchy-builder + script: | + COQ_ELPI_ATTRIBUTES=log_hb make -j2 + hb patch `find . -name \*.v` + rm -rf `coqc -where`/user-constribs/HB + make -j2 + hb reset `find . -name \*.v` + git diff --exit-code +``` + +

diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 3a31049a3..981a85254 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -10,7 +10,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make ] install: [ make "install" "VFILES=structures.v" ] -depends: [ "coq-elpi" {>= "1.6" & < "1.9~"} ] +depends: [ "coq-elpi" {>= "1.6" & < "1.10~"} ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """ Hierarchy Builder is a high level language to build hierarchies of algebraic structures and make these diff --git a/demo2/stage10.v b/demo2/stage10.v index 95932c8f0..fc8905a4c 100644 --- a/demo2/stage10.v +++ b/demo2/stage10.v @@ -10,8 +10,6 @@ Local Open Scope hb_scope. Module Stage10. -HB.structure Definition TYPE := { A of True }. - HB.mixin Record AddAG_of_TYPE A := { zero : A; add : A -> A -> A; diff --git a/demo2/stage11.v b/demo2/stage11.v index dc2269986..86568e670 100644 --- a/demo2/stage11.v +++ b/demo2/stage11.v @@ -10,8 +10,6 @@ Local Open Scope hb_scope. Module Stage11. -HB.structure Definition TYPE := { A of True }. - HB.mixin Record AddAG_of_TYPE A := { zero : A; add : A -> A -> A; diff --git a/demo5/hierarchy_0.v b/demo5/hierarchy_0.v index 8bd66c73a..65f54c00e 100644 --- a/demo5/hierarchy_0.v +++ b/demo5/hierarchy_0.v @@ -1,8 +1,6 @@ From Coq Require Import ssreflect ssrfun. From HB Require Import structures. -HB.structure Definition TYPE := { A of True }. - HB.mixin Record AddComoid_of_TYPE A := { zero : A; add : A -> A -> A; diff --git a/hb.elpi b/hb.elpi index dc687dfd9..a42d31e4d 100644 --- a/hb.elpi +++ b/hb.elpi @@ -80,6 +80,195 @@ list-eq-set L1 L2 :- list-diff L1 L2 [], list-diff L2 L1 []. pred under.do! i:((A -> Prop) -> A -> prop), i:list prop. under.do! Then LP :- Then (_\ std.do! LP) _. +%%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pred logger o:list coq.pp, o:bool. + +pred logger-extend i:list coq.pp, i:coq.pp. +logger-extend [] _ :- coq.error "HB: logger was closed". +logger-extend (uvar as X) V :- X = [V|FRESH_]. +logger-extend [_|XS] V :- logger-extend XS V. + +pred logger-close i:list coq.pp. +logger-close (uvar as X) :- X = []. +logger-close [_|XS] :- logger-close XS. + +pred log-vernac i:coq.vernac. +log-vernac V :- logger L Nice, !, + if (Nice = tt) (PPALL = []) (PPALL = [@ppmost!]), + logger-extend L {PPALL => coq.vernac->pp [V]}. +log-vernac _. + +pred with-logging i:prop. +with-logging P :- get-option "log" tt, + logger L tt => P, + logger-close L, + std.intersperse coq.pp.spc L PP, + coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S, + coq.say "(* \n" S "\n*)". +with-logging P :- get-option "elpi.log_hb" _, % env variable + logger L ff => P, + logger-close L, + std.intersperse coq.pp.spc L PP, + coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S, + get-option "elpi.loc" Loc, + rex_split "," Loc [FILE|_], + FILENAME is FILE ^ ".hb", + open_append FILENAME OC, + std.string.concat "\n" ["","HIERARCHY BUILDER PATCH",Loc,S] PATCH, + output OC PATCH, + close_out OC. +with-logging P :- P. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Coq document + +% This is a very minimalistic AST to represent a Coq document equipped with +% pretty printing facilities. +% +% When "complete enough" this should be moved to coq-elpi proper. + +kind coq.vernac type. +type coq.vernac.begin-module string -> option string -> coq.vernac. +type coq.vernac.end-module string -> coq.vernac. +type coq.vernac.begin-section string -> coq.vernac. +type coq.vernac.end-section string -> coq.vernac. +type coq.vernac.import-module string -> coq.vernac. +type coq.vernac.export-module string -> coq.vernac. +type coq.vernac.definition string -> option term -> term -> coq.vernac. +type coq.vernac.variable string -> term -> coq.vernac. +type coq.vernac.inductive indt-decl -> coq.vernac. +type coq.vernac.abbreviation string -> int -> term -> coq.vernac. +type coq.vernac.coercion string -> gref -> class -> coq.vernac. +type coq.vernac.canonical string -> coq.vernac. +type coq.vernac.implicit string -> list implicit_kind -> coq.vernac. +type coq.vernac.comment A -> coq.vernac. + +% The main entry point to print vernacular commands is coq.vernac->pp + +{ +shorten coq.vernac.{ begin-module , end-module , begin-section, end-section }. +shorten coq.vernac.{ import-module , export-module }. +shorten coq.vernac.{ definition , variable , comment }. +shorten coq.{ vernac.inductive , vernac.implicit }. +shorten coq.vernac.{ canonical , abbreviation , coercion }. +shorten coq.pp.{ box , h , spc , v , str , hv , hov, glue, brk }. + +pred coq.vernac->pp i:list coq.vernac, o:coq.pp. +coq.vernac->pp L (box (v 0) L2) :- + std.map L coq.vernac->pp1 L1, + std.intersperse spc L1 L2. + +pred coq.vernac->pp1 i:coq.vernac, o:coq.pp. +coq.vernac->pp1 (begin-module Name none) PP :- + PP = box h [str "Module ", str Name, str "."]. +coq.vernac->pp1 (begin-module Name (some TyName)) PP :- + PP = box h [str "Module ", str Name, str " : ", str TyName, str "."]. +coq.vernac->pp1 (end-module Name) PP :- + PP = box h [str "End ", str Name, str "."]. +coq.vernac->pp1 (begin-section Name) PP :- + PP = box h [str "Section ", str Name, str "."]. +coq.vernac->pp1 (end-section Name) PP :- + PP = box h [str "End ", str Name, str "."]. +coq.vernac->pp1 (definition Name none Body) PP :- + PP = box (hv 2) [str "Definition ", str Name, str " :=", spc, B, str "."], + coq.term->pp Body B. +coq.vernac->pp1 (definition Name (some Ty) Body) PP :- + PP = box (hv 2) [str "Definition ", str Name, str " : ", T, str " :=", spc, B, str "."], + coq.term->pp Ty T, + coq.term->pp Body B. +coq.vernac->pp1 (variable Name Ty) (box (hv 2) [box h [str "Variable ", str Name, str " :"], spc, TY, str "."]) :- + coq.term->pp Ty TY. +coq.vernac->pp1 (import-module Name) (box h [str "Import ", str Name, str "."]). +coq.vernac->pp1 (export-module Name) (box h [str "Export ", str Name, str "."]). +coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notation ",str Name|StrParams], str " :=", spc, B, str "."]) :- + coq.vernac->ppabbrterm NParams Term StrParams B. +coq.vernac->pp1 (canonical Name) (box h [str "Canonical ", str Name, str "."]). +coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :- + coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S, + if2 (TGT = sortclass) (T = "Sortclass") + (TGT = funclass) (T = "Funclass") + (TGT = grefclass GR, coq.gref->path GR GRP, std.string.concat "." {std.take-last 2 GRP} T). +coq.vernac->pp1 (vernac.inductive I) PP :- + coq.vernac->ppinductive I [] PP. +coq.vernac->pp1 (vernac.implicit Name []) (box h [str "Arguments ", str Name, str " : clear implicits."]). +coq.vernac->pp1 (vernac.implicit Name L) (box h [str "Arguments ", str Name, spc, glue PP, str "."]) :- + std.map L coq.vernac->ppimparg PP1, + std.intersperse spc PP1 PP. +coq.vernac->pp1 (comment A) (box (hov 2) [str"(*", str S, str"*)"]) :- + std.any->string A S. + + +pred coq.vernac->ppimparg i:implicit_kind, o:coq.pp. +coq.vernac->ppimparg explicit (str "_"). +coq.vernac->ppimparg maximal (str "{_}"). +coq.vernac->ppimparg implicit (str "[_]"). + +pred coq.vernac->ppinductive i:indt-decl, i:list (pair implicit_kind term), o:coq.pp. +coq.vernac->ppinductive (parameter ID IMPL TY I) Acc R :- + @pi-parameter ID TY p\ coq.vernac->ppinductive (I p) [pr IMPL p|Acc] R. +coq.vernac->ppinductive (record ID SORT KID RD) ParamsRev PP :- + PP = (box (hov 0) [ + box (hov 0) [str "Record", spc, str ID, brk 1 4, glue ParamsPP, + str " : ", SortPP, brk 1 2, str":= ", str KID], + brk 1 2, + box (hv 2) [str"{", spc, glue FieldsPP, str"}"], + str"."]), + std.rev ParamsRev Params, + coq.vernac->ppinductiveparams Params ParamsPP, + coq.term->pp SORT SortPP, + coq.vernac->pprecordfields RD FieldsPP. +coq.vernac->ppinductive (inductive ID IsInd Arity Ks) ParamsRev PP :- + PP = (box (hov 0) [ + str CO,str "Inductive", spc, + box (hov 0) [ + str ID, brk 1 4, glue ParamsPP, ArityPP, str " :="], + brk 0 2, + box (hv 2) [str" ", glue KsPp], + str "."]), + std.rev ParamsRev Params, + coq.vernac->ppinductiveparams Params ParamsPP, + std.map Params snd ParamsAsArgs, + if (IsInd = tt) (CO = "") (CO = "Co"), + coq.arity->pp Arity ArityPP, + @pi-inductive ID Arity x\ + coq.mk-app x ParamsAsArgs (X x), + coq.vernac->ppinductiveconstructor (Ks (X x)) KsPp. + +pred coq.vernac->ppinductiveconstructor i:list indc-decl, o:list coq.pp. +coq.vernac->ppinductiveconstructor [] []. +coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :- + PP = [str ID,{coq.arity->pp Arity},SEP|Rest], + if (Ks = []) (SEP = str"") (SEP = glue [brk 1 0, str "| "]), + coq.vernac->ppinductiveconstructor Ks Rest. + +pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp. +coq.vernac->ppinductiveparams [] []. +coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :- + PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest], + decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY, + if2 (Imp = explicit) (A = "(", B = ")") + (Imp = maximal) (A = "{", B = "}") + (A = "[", B = "]"), + coq.vernac->ppinductiveparams Rest PPRest. + +pred coq.vernac->pprecordfields i:record-decl, o:list coq.pp. +coq.vernac->pprecordfields end-record []. +coq.vernac->pprecordfields (field _ ID TY F) [ str ID, str " : ", TYPP, str ";", spc|FPP] :- % TODO attributes + coq.term->pp TY TYPP, + @pi-parameter ID TY p\ coq.vernac->pprecordfields (F p) FPP. + +pred coq.vernac->ppabbrterm i:int, i:term, o:list coq.pp, o:coq.pp. +coq.vernac->ppabbrterm 0 T [] B :- !, @holes! => coq.term->pp T B. +coq.vernac->ppabbrterm N (fun _ _ F) [spc,str ID|StrParams] B :- + ID is "X" ^ {std.any->string N}, + coq.id->name ID Name, + M is N - 1, + @pi-decl Name (sort prop) x\ coq.vernac->ppabbrterm M (F x) StrParams B. + +} + %%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % runs P in a context where Coq #[attributes] are parsed @@ -90,6 +279,7 @@ with-attributes P :- att "verbose" bool, att "mathcomp" bool, att "mathcomp.axiom" string, + att "log" bool, ] Opts, !, Opts => P. @@ -344,23 +534,98 @@ distribute-w-params (w-params.nil N T F) L :- pred w-params_1 i:one-w-params A, o:A. w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y. -% no implicit arguments + +pred hb-set-implicit i:gref, i:list implicit_kind. +hb-set-implicit GR I :- std.do! [ + coq.arguments.set-implicit GR [I], + log-vernac (coq.vernac.implicit {coq.gref->id GR} I), +]. + + pred hb-add-const i:id, i:term, i:term, i:opaque?, o:constant. hb-add-const Name Bo Ty Opaque C :- std.do! [ coq.env.add-const Name Bo Ty Opaque C, - coq.arguments.set-implicit (const C) [[]] + if (var Ty) (Ty? = none) (Ty? = some Ty), + log-vernac (coq.vernac.definition Name Ty? Bo), + hb-set-implicit (const C) [], +]. + +pred hb-add-variable i:id, i:term, o:constant. +hb-add-variable Name Ty C :- std.do! [ + if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name), + @local! => coq.env.add-const ID _ Ty @opaque! C, + log-vernac (coq.vernac.variable ID Ty), + hb-set-implicit (const C) [], ]. pred hb-add-indt i:indt-decl, o:inductive. hb-add-indt Decl I :- std.do! [ coq.env.add-indt Decl I, + log-vernac (coq.vernac.inductive Decl), +]. + +pred hb-begin-module i:id. +hb-begin-module Name :- std.do! [ + coq.env.begin-module Name none, + log-vernac (coq.vernac.begin-module Name none), +]. + +pred hb-end-module i:id, o:modpath. +hb-end-module Name M :- std.do! [ + coq.env.end-module M, + log-vernac (coq.vernac.end-module Name), +]. + +pred hb-begin-section i:id. +hb-begin-section Name :- std.do! [ + coq.env.begin-section Name, + log-vernac (coq.vernac.begin-section Name), +]. + +pred hb-end-section i:id. +hb-end-section Name :- std.do! [ + coq.env.end-section, + log-vernac (coq.vernac.end-section Name), +]. + +pred hb-declare-instance i:gref. +hb-declare-instance GR :- std.do! [ + coq.CS.declare-instance GR, + coq.gref->id GR Name, + log-vernac (coq.vernac.canonical Name), +]. + +pred hb-add-abbreviation i:id, i:int, i:term, i:bool, o:abbreviation. +hb-add-abbreviation Name NArgs Body OnlyParsing O :- std.do! [ + coq.notation.add-abbreviation Name NArgs Body OnlyParsing O, + log-vernac (coq.vernac.abbreviation Name NArgs Body), +]. + + +pred hb-export-module i:modpath. +hb-export-module M :- std.do! [ + coq.env.export-module M, + coq.modpath->path M MP, + std.take-last 2 MP MPNice, + log-vernac (coq.vernac.export-module {std.string.concat "." MPNice}), +]. + +pred hb-coercion-declare i:coercion. +hb-coercion-declare C :- std.do! [ + coq.coercion.declare C, + C = coercion GR _ SRCGR TGTCL, + coq.gref->id GR Name, + log-vernac (coq.vernac.coercion Name SRCGR TGTCL), ]. %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %Specialize coq.elpi.accumulate to "hiearchy.db" -pred acc i:scope, i:clause. -acc S CL :- coq.elpi.accumulate S "hb.db" CL. +pred hb-accumulate i:scope, i:clause. +hb-accumulate S CL :- std.do! [ + coq.elpi.accumulate S "hb.db" CL, + if-verbose (log-vernac (coq.vernac.comment CL)), +]. pred from_mixin i:prop, o:mixinname. from_mixin (from _ X _) X. @@ -462,14 +727,14 @@ toposort-mixins In Out :- std.do! [ ]. pred toposort-proj i:(A -> B -> prop), i:list (pair B B), i:list A, o:list A. -toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out. +toposort-proj Proj ES In Out :- !, toposort-proj.hb-accumulate Proj ES [] In Out. pred topo-find i:B, o:A. -pred toposort-proj.acc i:(A -> B -> prop), i:list (pair B B), i:list B, i:list A, o:list A. -toposort-proj.acc _ ES Acc [] Out :- !, +pred toposort-proj.hb-accumulate i:(A -> B -> prop), i:list (pair B B), i:list B, i:list A, o:list A. +toposort-proj.hb-accumulate _ ES Acc [] Out :- !, std.map {toposort ES Acc} topo-find Out. -toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![ +toposort-proj.hb-accumulate Proj ES Acc [A|In] Out :- std.do![ Proj A B, - topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out + topo-find B A => toposort-proj.hb-accumulate Proj ES [B|Acc] In Out ]. % Classes can be topologically sorted according to the subclass relation @@ -931,12 +1196,12 @@ mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [ std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped", hb-add-const NC T TTy @transparent! C, mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT, - @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev, + @global! => hb-add-abbreviation N NParams AbbrevT tt Abbrev, ]. -% [acc-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F -pred acc-phant-abbrev i:string, i:gref, o:gref, o:abbreviation. -acc-phant-abbrev Str GR (const PhC) Abbrev :- !, std.do! [ +% [hb-accumulate-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F +pred hb-accumulate-phant-abbrev i:string, i:gref, o:gref, o:abbreviation. +hb-accumulate-phant-abbrev Str GR (const PhC) Abbrev :- !, std.do! [ mk-phant-term (global GR) PhGR, mk-phant-abbrev Str PhGR PhC Abbrev ]. @@ -1134,7 +1399,7 @@ declare-instances T [class Class Struct MLwP|Rest] :- std.assert-ok! (coq.typecheck S STy) "declare-instances: S illtyped", hb-add-const Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let - coq.CS.declare-instance (const CS), % Bug coq/coq#11155, should be local + hb-declare-instance (const CS), % Bug coq/coq#11155, should be local declare-instances T Rest. declare-instances T [_|Rest] :- declare-instances T Rest. declare-instances _ []. @@ -1146,10 +1411,10 @@ type factory-by-phantabbrev abbreviation -> factory-abbrev. pred declare-factory-abbrev i:id, i:factory-abbrev. declare-factory-abbrev Name (factory-by-classname GR) :- % looks fishy (the parameters are not taken into account) - @global! => coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _. + @global! => hb-add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt _. declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :- coq.notation.abbreviation-body Abbr Nargs AbbrTrm, - @global! => coq.notation.add-abbreviation Name Nargs AbbrTrm tt _. + @global! => hb-add-abbreviation Name Nargs AbbrTrm tt _. % [mk-factory-requires-clause-and-abbrev Str GR FL CL FactAbbrev] % computes the list of mixins ML provided by FL, @@ -1163,7 +1428,7 @@ mk-factory-requires-clause-and-abbrev Str GR GRFS [FactoryRequires|Aliases] Fact if (factory-alias->gref GR _) (Aliases = [], FactAbbrev = factory-by-classname GR) - (acc-phant-abbrev Str GR PhGR Abbrv, + (hb-accumulate-phant-abbrev Str GR PhGR Abbrv, Aliases = [phant-abbrev GR PhGR Abbrv], FactAbbrev = factory-by-phantabbrev Abbrv), ]. @@ -1190,7 +1455,7 @@ postulate-arity (parameter ID _ S A) Acc T T1 Ty :- std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped", if-verbose (coq.say "HB: postulating" ID), if (var S) (coq.fresh-type S) true, - @local! => hb-add-const ID _ S @opaque! C, + hb-add-variable ID S C, Var = global (const C), postulate-arity (A Var) [Var|Acc] T T1 Ty. postulate-arity (arity Ty) ArgsRev X T Ty :- @@ -1209,7 +1474,7 @@ postulate-mixin (triple M Ps T) MSL [mixin-src T M (global (const C))|MSL] :- MS mgref->term Ps T M Ty, std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped", - @local! => hb-add-const Name _ Ty @opaque! C % no body, local -> a variable + hb-add-variable Name Ty C ]. % [main-declare-context TheType Parameters Factories Clauses] postulates a @@ -1222,7 +1487,7 @@ main-declare-context TheType TheParams GRFSwP MSL :- std.do! [ apply-w-params MLwP TheParams TheType MLwAllArgs, std.fold MLwAllArgs [] postulate-mixin MSL, MSL => declare-instances TheType {findall-classes}, - std.forall MSL (ms\ acc current (clause _ _ ms)), + std.forall MSL (ms\ hb-accumulate current (clause _ _ ms)), ]. % [main-declare-builder (builder _ F M B) From MoreFrom] Given B of type FB, it @@ -1245,8 +1510,8 @@ main-declare-builder (builder _ SrcFactory TgtMixin B) FromClauses MoreFromClaus pred to-export o:modpath. pred export i:modpath. export Module :- !, - coq.env.export-module Module, - acc current (clause _ _ (to-export Module)). + hb-export-module Module, + hb-accumulate current (clause _ _ (to-export Module)). pred mk-mixin-fun i:list-w-params mixinname, i:term, o:term. mk-mixin-fun ML X MLX :- mk-mixin-fun.then ML (p\ t\ body\ body = X) MLX. @@ -1306,7 +1571,7 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std w-params.nparams MwP NP, NImplicits is NP + 1, std.map {std.iota NImplicits} (_\r\ r = maximal) Implicits, - @global! => coq.arguments.set-implicit (const C) [Implicits], + @global! => hb-set-implicit (const C) Implicits, EXO = [exported-op M Poperation C|EXI] ]. @@ -1387,7 +1652,7 @@ pred declare-coercion i:term, i:term, i:class, i:class. declare-coercion SortProjection ClassProjection (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [ - acc current (clause _ _ (sub-class FC TC)), + hb-accumulate current (clause _ _ (sub-class FC TC)), gref->modname StructureF ModNameF, gref->modname StructureT ModNameT, @@ -1404,7 +1669,7 @@ declare-coercion SortProjection ClassProjection if-verbose (coq.say "HB: declare coercion hint" CName), hb-add-const CName CoeBody Ty @transparent! C, - @global! => coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)), + @global! => hb-coercion-declare (coercion (const C) 1 FC (grefclass TC)), Coercion = global (const C), w-params.then FMLwP mk-fun ignore @@ -1416,8 +1681,8 @@ declare-coercion SortProjection ClassProjection if-verbose (coq.say "HB: declare unification hint" SName), hb-add-const SName SCoeBody STy @transparent! SC, - @global! => coq.coercion.declare (coercion (const SC) 0 StructureF (grefclass StructureT)), - coq.CS.declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref + @global! => hb-coercion-declare (coercion (const SC) 0 StructureF (grefclass StructureT)), + hb-declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref ]. pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term, @@ -1455,7 +1720,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C (global S2_Pack) S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody, std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped", hb-add-const Name JoinBody Ty @transparent! J, - coq.CS.declare-instance (const J). + hb-declare-instance (const J). % TODO: this works under the invariant: we never have two classes that % contain exactly the same mixins. hb.structure should enforce this @@ -1537,7 +1802,7 @@ declare-sort-coercion StructureName (global Proj) :- if-verbose (coq.say "HB: declare sort coercion"), - @global! => coq.coercion.declare (coercion Proj 0 StructureName sortclass). + @global! => hb-coercion-declare (coercion Proj 0 StructureName sortclass). pred if-class-already-exists-error i:id, i:list class, i:list mixinname. if-class-already-exists-error _ [] _. @@ -1554,27 +1819,27 @@ export-mixin-coercion ClassName (some C) :- head-gref-under-prods CTy MixinGR, if-verbose (coq.say "HB: export class to mixin coercion for mixin" {nice-gref->string MixinGR}), @global! => - coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)). + hb-coercion-declare (coercion (const C) _ ClassName (grefclass MixinGR)). pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:classname, i:term, i:option gref. mc-compat-structure ModuleName _Module NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [ CompatModuleName is "MathCompCompat" ^ ModuleName, - coq.env.begin-module CompatModuleName none, % to avoid collisions - coq.env.begin-module ModuleName none, + hb-begin-module CompatModuleName, % to avoid collisions + hb-begin-module ModuleName, if (Axioms = some GR) - (@global! => coq.notation.add-abbreviation "axiom" 0 (global GR) ff _) + (@global! => hb-add-abbreviation "axiom" 0 (global GR) ff _) true, if (NewMixins = [NewMixin]) (std.do! [ if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"), MArgs is {factory-nparams NewMixin} + 1, mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin, - @global! => coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _, - @global! => coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _, + @global! => hb-add-abbreviation "axioms" MArgs EtaNewMixin ff _, + @global! => hb-add-abbreviation "mixin_of" MArgs EtaNewMixin ff _, std.assert! (factory-constructor NewMixin FK) "BUG: Factory constructor missing", std.assert! (phant-abbrev FK _ PhAbb) "BUG: missing phant-abbrev", - @global! => coq.notation.add-abbreviation "Mixin" 0 + @global! => hb-add-abbreviation "Mixin" 0 {coq.notation.abbreviation PhAbb {coq.mk-n-holes MArgs}} ff _, if-verbose (coq.say "mc-compat-structure: declaring pack abbreviation"), class-def (class ClassName _ ClassMixins), @@ -1587,11 +1852,11 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassName ClassProject std.assert-ok! (coq.typecheck ClassProjection ClassProjectionTy) "wtf", CArgs is CNParams + 1, mk-eta CArgs ClassProjectionTy ClassProjection EtaClassProjection, - @global! => coq.notation.add-abbreviation "class_of" CArgs EtaClassProjection ff _, + @global! => hb-add-abbreviation "class_of" CArgs EtaClassProjection ff _, - coq.env.end-module _, - coq.env.end-module MCCompat, - coq.env.export-module MCCompat, + hb-end-module ModuleName _, + hb-end-module CompatModuleName MCCompat, + hb-export-module MCCompat, %coq.env.import-module Module, ]. @@ -1652,7 +1917,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [ if-verbose (coq.say "HB: start module" Module), - coq.env.begin-module Module none, + hb-begin-module Module, declare-class+structure MLwP ClassName Structure SortProjection ClassProjection Factories, @@ -1671,7 +1936,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [ if-verbose (coq.say "HB: start module Exports"), - coq.env.begin-module "Exports" none, + hb-begin-module "Exports", declare-sort-coercion Structure SortProjection, if-verbose (coq.say "HB: exporting operations"), ClassAlias => ClassRequires => Factories => @@ -1683,7 +1948,7 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [ ClassAlias => ClassRequires => Factories => declare-unification-hints SortProjection ClassProjection CurrentClass NewJoins, % Register in Elpi's DB the new structure - % NOT TODO: All these acc are correctly locaed in an Export Module + % NOT TODO: All these hb-accumulate are correctly locaed in an Export Module if (ClassName = indt ClassInd) (std.do![ if-verbose (coq.say "HB: exporting coercions from class to mixins"), @@ -1700,12 +1965,12 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [ NewJoins, [class-def CurrentClass] ] NewClauses, - std.forall NewClauses (c\ acc current (clause _ _ c)), + std.forall NewClauses (c\ hb-accumulate current (clause _ _ c)), if-verbose (coq.say "HB: stop module Exports"), - coq.env.end-module Exports, + hb-end-module "Exports" Exports, - coq.env.end-module ModulePath, + hb-end-module Module ModulePath, if-verbose (coq.say "HB: end modules; export" Exports), @@ -1723,23 +1988,23 @@ main-begin-declare Module TName GRFS Decl :- std.do! [ if-verbose (coq.say "HB: start module and section" Module), - coq.env.begin-module Module none, - coq.env.begin-section Module, + hb-begin-module Module none, + hb-begin-section Module, if-verbose (coq.say "HB: postulate type" TName), coq.fresh-type Ty, @local! => hb-add-const TName _ Ty @opaque! T, % no body, local -> a variable main-declare-context (global (const T)) [] GRFS _, % TODO params - acc current (clause _ _ (current-mode Decl)) + hb-accumulate current (clause _ _ (current-mode Decl)) ]. */ pred main-end-declare-builders. main-end-declare-builders :- std.do! [ - current-mode (builder-from _ GR), + current-mode (builder-from _ GR ModName), - coq.env.end-section, + hb-end-section ModName, findall-builders LFIL, @@ -1752,11 +2017,11 @@ main-end-declare-builders :- std.do! [ % TODO: Do we need this module? gref->modname GR M, Name is M ^ "_Exports", - coq.env.begin-module Name none, - (std.forall Clauses c\ acc current (clause _ _ c)), + hb-begin-module Name, + (std.forall Clauses c\ hb-accumulate current (clause _ _ c)), - coq.env.end-module Exports, - coq.env.end-module _, + hb-end-module Name Exports, + hb-end-module ModName _, export Exports, ]. @@ -1780,7 +2045,7 @@ add-mixin T FGR MakeCanon MissinMixin Bo [MixinSrcCl, BuiderDeclCl] :- hb-add-const Name Bo Ty @transparent! C), if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _) (if-verbose (coq.say "HB: declare canonical mixin instance" C), - coq.CS.declare-instance (const C)) + hb-declare-instance (const C)) true. pred mixin-for_mixin-builder i:prop, o:term. @@ -1830,19 +2095,19 @@ declare-canonical-instances-from-factory T F :- % entry point for HB.instance pred main-declare-instance i:term, i:term, o:list prop. -main-declare-instance T F Clauses :- current-mode (builder-from TheFactory FGR), !, +main-declare-instance T F Clauses :- current-mode (builder-from TheFactory FGR _), !, declare-canonical-instances-from-factory-and-local-builders T F TheFactory FGR Clauses. main-declare-instance T F [] :- declare-canonical-instances-from-factory T F. pred declare-old-located i:string, i:located. declare-old-located Id (loc-gref GR) :- - @global! => coq.notation.add-abbreviation Id 0 (global GR) ff _. + @global! => hb-add-abbreviation Id 0 (global GR) ff _. declare-old-located Id (loc-abbreviation Abbrev) :- coq.notation.abbreviation Abbrev [] T, % FIXME: this assumes the abbreviation has no arg % we should fix it. - @global! => coq.notation.add-abbreviation Id 0 T ff _. + @global! => hb-add-abbreviation Id 0 T ff _. pred declare-old-constant i:option constant. declare-old-constant none. @@ -1876,14 +2141,25 @@ purge-id T T1 :- pred main-begin-declare-builders i:context-decl. main-begin-declare-builders CtxSkel :- std.do! [ Name is "Builders_" ^ {term_to_string {new_int}}, % TODO? +<<<<<<< HEAD std.assert-ok! (elaborate-context-skel->factory CtxSkel Ctx GRF) "Context illtyped", coq.env.begin-module Name none, +======= + context->factory CtxSkel GRF, + hb-begin-module Name, +>>>>>>> logging: ability to print vernacular commands if (GRF = indt FRecord) (std.do! [ - coq.env.begin-module "Super" none, + hb-begin-module "Super", std.forall {coq.CS.canonical-projections FRecord} declare-old-constant, +<<<<<<< HEAD coq.env.end-module _]) (true), coq.env.begin-section Name, builders-postulate-factories Ctx, +======= + hb-end-module "Super" _]) (true), + hb-begin-section Name, + builders-postulate-factories Name CtxSkel, +>>>>>>> logging: ability to print vernacular commands ]. pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term. @@ -1893,7 +2169,7 @@ postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [ coq.notation.abbreviation Fabv {std.append Params [TheType]} Package, Msg is "Unable to declare factory " ^ Name, std.assert-ok! (coq.typecheck-ty Package _) Msg, - @local! => hb-add-const Name _ Package @opaque! C, + hb-add-variable Name Package C, TheFactory = global (const C), ]. @@ -1914,21 +2190,21 @@ define-factory-operation TheType TheFactory NHoles (some P) :- T = app[global (const P), TheType|Holes_Factory], std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation", coq.gref->id (const P) Name, - @local! => coq.notation.add-abbreviation Name 0 T ff _. + @local! => hb-add-abbreviation Name 0 T ff _. pred fresh-indexed-type o:term. fresh-indexed-type Ty :- Ty = {{lib:hb.indexed Type}}, std.assert-ok! (coq.typecheck-ty Ty _) "impossible". -pred builders-postulate-factories i:context-decl. -builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [ +pred builders-postulate-factories i:id, i:context-decl. +builders-postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [ % TODO we should allow T to be anything. std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "builders-postulate-factory: illtyped context", if (var Ty) (fresh-indexed-type Ty) (std.assert-ok! (coq.unify-eq Ty {{Type}}) "The last context item before the factory must be a type variable"), if-verbose (coq.say "HB: postulating type" IDT), - @local! => hb-add-const IDT _ Ty @opaque! C, % no body, local -> a variable + hb-add-variable IDT Ty C, TheType = global (const C), std.assert! (factory? (TF TheType) (triple GRF Params TheType)) @@ -1937,19 +2213,19 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF main-declare-context TheType Params GRFMLwP _, postulate-factory-abbrev TheType Params IDF GRF TheFactory, define-factory-operations TheType TheFactory GRF, - acc current (clause _ _ (current-mode (builder-from TheFactory GRF))), + hb-accumulate current (clause _ _ (current-mode (builder-from TheFactory GRF ModName))), ]. -builders-postulate-factories (context-item ID _ TSkel none Factories) :- std.do! [ +builders-postulate-factories ModName (context-item ID _ TSkel none Factories) :- std.do! [ if-verbose (coq.say "HB: postulating" ID), std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factories: illtyped context", if (var T) (coq.fresh-type T) true, - @local! => hb-add-const ID _ T @opaque! P, % no body, local -> a variable + hb-add-variable ID T P, TheParam = global (const P), - builders-postulate-factories (Factories TheParam), + builders-postulate-factories ModName (Factories TheParam), ]. -builders-postulate-factories (context-item ID _ _ (some _) _) :- +builders-postulate-factories _ (context-item ID _ _ (some _) _) :- coq.error "context item cannot be given a body:" ID. % In an asset like HB.mixing Recoord P1 .. PN A of F1 .. & FK .. @@ -1968,8 +2244,8 @@ main-declare-asset Asset AssetKind :- std.do! [ if-verbose (coq.say "HB: start module and section" Module), - coq.env.begin-module Module none, - coq.env.begin-section Module, + hb-begin-module Module, + hb-begin-section Module, % We start by postulating the parameters process-asset-named-parameters Asset AssetKind Module [], @@ -1981,7 +2257,7 @@ process-asset-named-parameters (asset-parameter Name T Rest as R) D Module Param if-verbose (coq.say "HB: postulate type" Name), if (var T) (fresh-indexed-type Ty) (Ty = T), - @local! => hb-add-const Name _ Ty @opaque! C, % no body, local -> a variable + hb-add-variable Name Ty C, TheType = global (const C), % We postulate the dependencies @@ -1992,7 +2268,7 @@ process-asset-named-parameters (asset-parameter Name T Rest) D Module Params :- std.assert-ok! (coq.typecheck-ty T _) "Illtyped parameter", if-verbose (coq.say "HB: postulate " Name), if (var T) (coq.fresh-type T) true, - @local! => hb-add-const Name _ T @opaque! C, % no body, local -> a variable + hb-add-variable Name T C, TheParam = global (const C), process-asset-named-parameters (Rest TheParam) D Module [pr TheParam T|Params], ]. @@ -2037,7 +2313,7 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [ hb-add-const "Axioms_" MFK MFKTyC @transparent! CK, GRK = const CK, - coq.env.end-section, + hb-end-section Module, mk-phant-term (global GRK) PhGRK0, if (mixin-first-class F _) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK), @@ -2049,16 +2325,16 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [ if-verbose (coq.say "HB: start module Exports"), - coq.env.begin-module "Exports" none, - std.forall Clauses (c\ acc current (clause _ _ c)), + hb-begin-module "Exports", + std.forall Clauses (c\ hb-accumulate current (clause _ _ c)), % std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits, - % coq.arguments.set-implicit GRK [[maximal|Implicits]] tt, + % hb-set-implicit GRK [maximal|Implicits], w-params.nparams MLwP NParams, - acc current (clause _ _ (factory-nparams (const C) NParams)), - acc current (clause _ _ (factory-constructor (const C) GRK)), - acc current (clause _ _ (factory-builder-nparams BuildConst NParams)), - coq.env.end-module Exports, - coq.env.end-module _Module, + hb-accumulate current (clause _ _ (factory-nparams (const C) NParams)), + hb-accumulate current (clause _ _ (factory-constructor (const C) GRK)), + hb-accumulate current (clause _ _ (factory-builder-nparams BuildConst NParams)), + hb-end-module "Exports" Exports, + hb-end-module Module _, if-verbose (coq.say "HB: end modules and sections; export" Exports), @@ -2096,7 +2372,7 @@ declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std. RDeclSkel = record "axioms_" Sort1 Kname Fields1, std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped", hb-add-indt RDecl R, - coq.env.end-section, + hb-end-section Module, coq.env.indt R tt _ _ _ [K] _, GRK = indc K, @@ -2122,17 +2398,17 @@ declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std. if-verbose (coq.say "HB: start module Exports"), - coq.env.begin-module "Exports" none, - std.forall Clauses (c\ acc current (clause _ _ c)), + hb-begin-module "Exports", + std.forall Clauses (c\ hb-accumulate current (clause _ _ c)), w-params.nparams MLwP NParams, - acc current (clause _ _ (factory-nparams (indt R) NParams)), + hb-accumulate current (clause _ _ (factory-nparams (indt R) NParams)), std.map {list-w-params_list {gr-deps GRK}} (_\ r\ r = maximal) Implicits, - @global! => coq.arguments.set-implicit GRK [[maximal|Implicits]], - acc current (clause _ _ (factory-constructor (indt R) GRK)), - acc current (clause _ _ (factory-builder-nparams BuildConst NParams)), - acc current (clause _ _ (phant-abbrev GRK (const BuildConst) BuildAbbrev)), - coq.env.end-module Exports, - coq.env.end-module _Module, + @global! => hb-set-implicit GRK [maximal|Implicits], + hb-accumulate current (clause _ _ (factory-constructor (indt R) GRK)), + hb-accumulate current (clause _ _ (factory-builder-nparams BuildConst NParams)), + hb-accumulate current (clause _ _ (phant-abbrev GRK (const BuildConst) BuildAbbrev)), + hb-end-module "Exports" Exports, + hb-end-module Module _, if-verbose (coq.say "HB: end modules and sections; export" Exports), diff --git a/hb.ml b/hb.ml new file mode 100644 index 000000000..46f775102 --- /dev/null +++ b/hb.ml @@ -0,0 +1,186 @@ + +(* ----------- aux -------------------------------------------------------- *) +let int_of_string s = + try int_of_string s + with Failure _ -> Printf.eprintf "ERROR: not a number \n"; exit 1 + +let unix_read ic len = + let all = Bytes.create len in + let rec loop cur len = + if cur >= len then () + else + let n = Unix.read ic all cur (len-cur) in + loop (cur+n) len in + loop 0 len; + Bytes.to_string all + +let unix_open_file file = + let ic = Unix.openfile file [Unix.O_RDONLY] 0 in + let len = Unix.lseek ic 0 Unix.SEEK_END in + let _ = Unix.lseek ic 0 Unix.SEEK_SET in + ic, len + +let unix_read_whole_file file = + let ic, len = unix_open_file file in + let data = unix_read ic len in + Unix.close ic; + data + +(* ----------- patches ----------------------------------------------------- *) + +type patch = { + start : int; + stop : int; + text : string; +} + +let parse_one_patch text = + let r = Str.regexp "[^,]+, characters \\([0-9]+\\)-\\([0-9]+\\).*" in + let beginning = String.index text '\n' in + let header = String.sub text 0 beginning in + let start = int_of_string @@ Str.replace_first r "\\1" header in + let stop = int_of_string @@ Str.replace_first r "\\2" header in + let text = String.sub text (beginning+1) (String.length text - beginning -1) in + { start; stop; text } + +let delim_start = "(* ------------ generator ----------------" +let delim_mid = "------------ generated ---------------- *)" +let delim_end = "(* ----------------- end ----------------- *)" + +let parse_patch_file file = + let text = unix_read_whole_file file in + let patches = Str.split (Str.regexp_string "\nHIERARCHY BUILDER PATCH\n") text in + let patches = List.map parse_one_patch patches in + patches + +let patch_file file patches = + let ic, len = unix_open_file file in + + let out = Buffer.create 1024 in + + let apply_one_hunk cur { start; stop; text } = + let before = unix_read ic (start - cur) in + let before, extra = + (* HACK since the locs don't include #[attrs], to be removed in Coq 8.14 https://github.com/coq/coq/pull/13844 *) + match String.rindex_opt before '\n' with + | Some i when before.[i+1] = '#' -> + String.sub before 0 (i+1), + String.sub before (i+1) (String.length before - i-1) + | _ -> before, "" + in + let current = unix_read ic (stop - start) in + Printf.bprintf out "%s\n%s\n%s%s\n%s\n%s\n%s\n" + before + delim_start + extra + current + delim_mid + text + delim_end; + stop + in + + Printf.printf "Patching %s ..." file; + let cur = List.fold_left apply_one_hunk 0 patches in + let rest = unix_read ic (len - cur) in + Printf.bprintf out "%s" rest; + Unix.close ic; + let oc = open_out file in + Buffer.output_buffer oc out; + close_out oc; + Printf.printf "done.\n" +;; + +let reset_file file = + let ic, len = unix_open_file file in + let text = unix_read ic len in + let lines = String.split_on_char '\n' text in + let rec copy = function + | x :: xs when x = delim_start -> `Glue :: copy xs + | x :: xs when x = delim_mid -> erase xs + | x :: xs -> `Keep x :: copy xs + | [] -> [] + and erase = function + | x :: xs when x = delim_end -> `Glue :: copy xs + | _ :: xs -> erase xs + | [] -> assert false + in + let new_lines = copy lines in + let rec glue = function + | [] -> [] + | `Keep x :: `Glue :: `Keep y :: rest -> glue (`Keep(x^y) :: rest) + | `Keep x :: xs -> x :: glue xs + | `Glue :: xs -> glue xs + in + Unix.close ic; + let new_text = String.concat "\n" (glue new_lines) in + if new_text = text then + Printf.printf "Skip %s since it contains no generated code\n" file + else + let oc = open_out file in + Printf.fprintf oc "%s" new_text; + close_out oc; + try + Sys.rename (file ^ ".hb") (file ^ ".hb.old"); + Printf.printf "Reset %s (patch file renamed to %s.hb.old)\n" file file + with Sys_error _ -> Printf.printf "Reset %s\n" file + + +(* ----------- CLI ----------------------------------------------------- *) + +let usage () = + Printf.printf {| +Command line utility to apply patches generated by HB. + +After building your project with logging enabled, eg + + COQ_ELPI_ATTRIBUTES=log_hb make + +each file.v file contanining calls to HB is paired with a file.v.hb patch +file which can be applied by this utility. + +usage: + hb patch [-f] .. Applies the patches in to . + -f forces patch application even if the soure file + is newer than the patch. + hb reset .. Erases all generated code from source file. It does + nothing if the file is not patched. If a patch file + exists it is renamed to . + + hb show .. Lists all the patches contained in (debugging). + +|}; + exit 1 + +let apply_patches ~force file = + let pfile = file ^ ".hb" in + if Sys.file_exists pfile then + let patches = parse_patch_file pfile in + let { Unix.st_mtime = time_patch } = Unix.stat pfile in + let { Unix.st_mtime = time_orig } = Unix.stat file in + if time_orig > time_patch && not force then + Printf.eprintf "Skip %s since it is more recent than %s.\n" file pfile + else + patch_file (Filename.chop_extension pfile) patches + else + Printf.printf "Skip %s since it has no patch\n" file + + +let list_patches pfile = + let patches = parse_patch_file pfile in + List.iter (fun { start; stop; text } -> + Printf.printf "Replace %d-%d with\n%s\n\n" start stop text) + patches + +let reset_patches file = + reset_file file + +let () = + let args = Array.to_list Sys.argv in + match args with + | _ :: "patch" :: "-f" :: (_ :: _ as args) -> List.iter (apply_patches ~force:true) args + | _ :: "patch" :: (_ :: _ as args) -> List.iter (apply_patches ~force:false) args + | _ :: "reset" :: (_ :: _ as args) -> List.iter reset_patches args + | _ :: "show" :: (_ :: _ as args) -> List.iter list_patches args + | _ -> usage () + diff --git a/structures.v b/structures.v index c7fa67d85..909d70302 100644 --- a/structures.v +++ b/structures.v @@ -126,7 +126,8 @@ pred mixin-first-class o:mixinname, o:classname. % To tell HB.end what we are doing kind declaration type. -type builder-from term -> factoryname -> declaration. % TheFactory and it's name +% TheFactory and it's name and the name of the module encloding all that +type builder-from term -> factoryname -> id -> declaration. pred current-mode o:declaration. pred exported-op o:mixinname, o:constant, o:constant. % memory of exported operations @@ -242,8 +243,11 @@ Elpi Accumulate File "hb.elpi". Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ -main [A] :- A = indt-decl _, !, - with-attributes (main-declare-asset {argument->asset A} asset-mixin). +main [A] :- A = indt-decl _, !, std.do! [ + with-attributes (with-logging ( + main-declare-asset {argument->asset A} asset-mixin + )), +]. main _ :- coq.error "Usage: HB.mixin Record T of F A & … := { … }.". @@ -294,7 +298,9 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :- main [const-decl Module (some B) _] :- !, std.do! [ purge-id B B1, std.assert-ok! (coq.elaborate-skeleton B1 _ B2) "illtyped structure definition", sigT->list-w-params B2 GRFS ClosureCheck, !, - with-attributes (main-declare-structure Module GRFS ClosureCheck), + with-attributes (with-logging ( + main-declare-structure Module GRFS ClosureCheck + )), ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". }}. @@ -327,12 +333,13 @@ Elpi Accumulate lp:{{ % If you don't mention the factory in a builder, then Coq won't make % a lambda for it at section closing time. pred hack-section-discharging i:term, o:term. -hack-section-discharging B B1 :- current-mode (builder-from TheFactory _), !, +hack-section-discharging B B1 :- current-mode (builder-from TheFactory _ _), !, std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)", B1 = {{ let _ : lp:TheFactoryTy := lp:TheFactory in lp:B }}. hack-section-discharging B B. -main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [ +pred main-const-decl i:id, i:term, i:arity. +main-const-decl Name BodySkel TyWPSkel :- std.do! [ std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped", coq.arity->term TyWP Ty, std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped", @@ -340,11 +347,11 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [ % Do not open a section when it is not necessary (no parameters) % A side effect of opening a section is loosing meta data associated % with instances, in particular builder tags are lost - with-attributes (if-verbose (coq.say "HB: skipping section opening")), + if-verbose (coq.say "HB: skipping section opening"), SectionBody = Body ) ( SectionName is "hb_instance_" ^ {term_to_string {new_int} }, - coq.env.begin-section SectionName, + hb-begin-section SectionName, postulate-arity TyWP [] Body SectionBody SectionTy ), @@ -357,21 +364,30 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [ (hb-add-const Name SectionBodyHack _ @transparent! C, TheFactory = (global (const C))), std.appendR {coq.mk-n-holes NParams} [TheType|_] Args, - with-attributes (main-declare-instance TheType TheFactory Clauses), + main-declare-instance TheType TheFactory Clauses, if (TyWP = arity _) true ( if-verbose (coq.say "HB: closing instance section"), - coq.env.end-section + hb-end-section SectionName ), % we accumulate clauses here since the section ends - std.forall Clauses (x\acc current (clause _ _ x)), + std.forall Clauses (x\hb-accumulate current (clause _ _ x)), +]. + +main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [ + with-attributes (with-logging ( + main-const-decl Name BodySkel TyWPSkel + )), +]. +main [T0, F0] :- std.do! [ + argument->ty T0 T, % TODO: change this when supporting morphism hierarchies + argument->term F0 F, + with-attributes (with-logging ( + main-declare-instance T F Clauses, + std.forall Clauses (x\hb-accumulate current (clause _ _ x)) + )), ]. -main [T0, F0] :- - argument->ty T0 T, !, % TODO: change this when supporting morphism hierarchies - argument->term F0 F, !, - with-attributes (main-declare-instance T F Clauses), !, - std.forall Clauses (x\acc current (clause _ _ x)). main _ :- coq.error "Usage: HB.instance *\nUsage: HB.instance Definition := T ...". @@ -390,7 +406,9 @@ Elpi Accumulate File "hb.elpi". Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ main [A] :- !, - with-attributes (main-declare-asset {argument->asset A} asset-factory). + with-attributes (with-logging ( + main-declare-asset {argument->asset A} asset-factory + )). main _ :- coq.error "Usage: HB.factory Record T of F A & … := { … }.\nUsage: HB.factory Definition T of F A := t.". @@ -436,7 +454,10 @@ Elpi Command HB.builders. Elpi Accumulate File "hb.elpi". Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ -main [ctx-decl C] :- !, with-attributes (main-begin-declare-builders C). +main [ctx-decl C] :- !, + with-attributes (with-logging ( + main-begin-declare-builders C + )). main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).". }}. @@ -448,7 +469,10 @@ Elpi Command HB.end. Elpi Accumulate File "hb.elpi". Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ -main [] :- !, with-attributes main-end-declare-builders. +main [] :- !, + with-attributes (with-logging ( + main-end-declare-builders + )). main _ :- coq.error "Usage: HB.end.". }}. Elpi Typecheck.