Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Dec 4, 2023
1 parent 1fc9043 commit 2dbe485
Showing 1 changed file with 34 additions and 32 deletions.
66 changes: 34 additions & 32 deletions structures.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,9 @@ pred docstring o:loc, o:string.

(* This database is used by the parsing phase only *)
#[synterp] Elpi Db export.db lp:{{

Check warning on line 238 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.16) 

This command does not support this attribute: synterp.

Check warning on line 238 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.17) 

This command does not support this attribute: synterp.

Check warning on line 238 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.18) 

This command does not support this attribute: synterp.
pred module-to-export o:string, o:modpath.
% 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.

}}.

Expand Down Expand Up @@ -451,9 +453,9 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".

Check warning on line 456 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.16) 

This command does not support this attribute: synterp.

Check warning on line 456 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.17) 

This command does not support this attribute: synterp.

Check warning on line 456 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.18) 

This command does not support this attribute: synterp.
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.

Check warning on line 457 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.16) 

This command does not support this attribute: synterp.

Check warning on line 457 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.17) 

This command does not support this attribute: synterp.

Check warning on line 457 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.18) 

This command does not support this attribute: synterp.
#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{

Check warning on line 458 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.16) 

This command does not support this attribute: synterp.

Check warning on line 458 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.17) 

This command does not support this attribute: synterp.

Check warning on line 458 in structures.v

View workflow job for this annotation

GitHub Actions / opam (8.18) 

This command does not support this attribute: synterp.

pred record-decl->id i:indt-decl, o:id.
record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N.
Expand All @@ -471,7 +473,7 @@ actions N :-
end-module _,
export-module E,
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 "" E)).

main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).

Expand Down Expand Up @@ -645,9 +647,9 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{

shorten coq.env.{ begin-module, end-module, begin-section, end-section, import-module, export-module }.

Expand All @@ -663,8 +665,8 @@ actions N :-
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)),
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.
Expand All @@ -676,7 +678,7 @@ actions-compat ModuleName :-
end-module O,
export-module O,
coq.env.current-library File,
coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File O)).
coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" O)).

main [const-decl N _ _] :- !, with-attributes (actions N).

Expand Down Expand Up @@ -768,7 +770,7 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{

shorten coq.env.{ begin-section, end-section }.

Expand Down Expand Up @@ -813,9 +815,9 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
#[synterp,skip="8.1[67]"] 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.
Expand All @@ -833,7 +835,7 @@ actions N :-
end-module _,
export-module E,
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 "" E)).

main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
main [const-decl N _ _] :- with-attributes (actions N).
Expand Down Expand Up @@ -901,8 +903,8 @@ Elpi Accumulate File "HB/context.elpi".
Elpi Accumulate File "HB/export.elpi".
Elpi Accumulate File "HB/factory.elpi".
Elpi Accumulate File "HB/builders.elpi".
#[synterp] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp] Elpi Accumulate lp:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{

shorten coq.env.{ begin-module, end-module, begin-section }.

Expand Down Expand Up @@ -940,9 +942,9 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
#[synterp,skip="8.1[67]"] Elpi Accumulate lp:{{

shorten coq.env.{ end-module, end-section, begin-module, end-module, export-module }.

Expand All @@ -954,7 +956,7 @@ actions :-
end-module _,
export-module M,
coq.env.current-library File,
coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File M)).
coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" M)).

main [] :- !, with-attributes actions.
main _ :- coq.error "Usage: HB.end.".
Expand Down Expand Up @@ -1011,17 +1013,17 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
#[synterp,skip="8.1[67]"] 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)).
coq.elpi.accumulate current "export.db" (clause _ _ (module-to-export File "" MP)).
actions [].

main [str M] :- !, with-attributes (actions {coq.locate-all M}).
Expand Down Expand Up @@ -1057,24 +1059,24 @@ 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:{{
#[synterp,skip="8.1[67]"] Elpi Accumulate File "HB/common/utils-synterp.elpi".
#[synterp,skip="8.1[67]"] Elpi Accumulate Db export.db.
#[synterp,skip="8.1[67]"] 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) :-
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.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).
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)).
Expand Down

0 comments on commit 2dbe485

Please sign in to comment.