NES in HB

NES.v

@@ -0,0 +1,78 @@
+From elpi Require Import elpi.
+
+Elpi Db NES.db lp:{{
+
+pred open-ns o:string, o:list string.
+:name "open-ns:begin"
+open-ns _ _ :- fail.
+
+typeabbrev path (list string).
+
+:index (2)
+pred ns o:path, o:modpath.
+
+}}.
+
+Elpi Command NES.Status.
+Elpi Accumulate Db NES.db.
+Elpi Accumulate File "nes.elpi".
+Elpi Accumulate lp:{{
+
+main _ :-
+  std.map {std.findall (open-ns X_ P_)} nes.open-ns->string Stack,
+  coq.say "NES: current namespace" {nes.join "." {std.rev Stack} },
+  std.findall (ns Y_ Z_) NS,
+  coq.say "NES: registered namespaces" NS.
+
+}}.
+Elpi Typecheck.
+Elpi Export NES.Status.
+
+Elpi Command NES.Begin.
+Elpi Accumulate File "nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- nes.begin-path {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Begin <DotSeparatedPath>".
+
+}}.
+Elpi Accumulate Db NES.db.
+Elpi Typecheck.
+Elpi Export NES.Begin.
+
+Elpi Command NES.End.
+Elpi Accumulate File "nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- nes.end-path {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.End <DotSeparatedPath>".
+
+}}.
+Elpi Accumulate Db NES.db.
+Elpi Typecheck.
+Elpi Export NES.End.
+
+
+Elpi Command NES.Open.
+Elpi Accumulate Db NES.db.
+Elpi Accumulate File "nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- nes.open-path {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Open <DotSeparatedPath>".
+
+}}.
+Elpi Typecheck.
+Elpi Export NES.Open.
+
+Elpi Command NES.Export.
+Elpi Accumulate Db NES.db.
+Elpi Accumulate File "nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- !, nes.export {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Export <DotSeparatedPath>".
+
+}}.
+Elpi Typecheck.
+Elpi Export NES.Export.

_CoqProject

@@ -1,4 +1,5 @@
 structures.v
+NES.v
 
 readme.v
 

nes.elpi

@@ -0,0 +1,128 @@
+namespace nes {
+
+pred ns->modpath i:prop, o:modpath.
+ns->modpath (ns _ M) M.
+
+pred open-ns->string i:prop, o:string.
+open-ns->string (open-ns S _) S.
+
+pred begin-ns i:string, i:list string.
+begin-ns NS Path :-
+  if (Path = [])
+     (Fresh is NS ^ "_aux_" ^ {std.any->string {new_int} }, coq.env.begin-module Fresh none)
+     true,
+  coq.env.begin-module NS none,
+  coq.env.current-path CP,
+  @local! => coq.elpi.accumulate current "NES.db"
+               (clause _ (after "open-ns:begin") (open-ns NS CP)).
+
+pred subpath i:list string, i:prop.
+subpath Path (ns Sub _) :- std.appendR _Prefix Path Sub.
+
+pred submod i:modpath, i:prop.
+submod Mod (ns _ SubMod) :-
+  coq.modpath->path SubMod SubPath,
+  coq.modpath->path Mod ModPath,
+  std.appendR ModPath _Suffix SubPath.
+
+pred undup i:list A, i:list A, o:list A.
+undup [] _ [].
+undup [X|XS] Seen YS :- std.mem! Seen X, !, undup XS Seen YS.
+undup [X|XS] Seen [X|YS] :- undup XS [X|Seen] YS.
+
+% end-ns ID Stack ClauseIn ClauseOut
+pred end-ns i:string, i:list string, i:list prop, o:list prop.
+end-ns NS Stack In Out :- In => std.do! [
+  std.rev Stack Path,
+  std.append Path [NS|END_] PathNoEnd,
+  std.findall (ns PathNoEnd M_) AllNS,
+  coq.env.end-module M,
+  % stuff inside M
+  std.filter AllNS (submod M) SubmodNS,
+  % since the current program still sees the clauses that will be dropped
+  % after closing M
+  undup SubmodNS [] SubmodNSNodup,
+
+  coq.locate-module NS M,
+  if (Path = [])
+     (std.do! [coq.env.end-module M_aux, coq.env.export-module M_aux, Local = @global!])
+     (Local = @local!),
+  % NES.Open can put clauses in scope
+  std.append Path [NS] NewPath,
+  New = [ns NewPath M | SubmodNSNodup],
+  std.append In New Out,
+  std.forall New (c\ Local => coq.elpi.accumulate current "NES.db" (clause _ _ c)),
+].
+
+pred iter-> i:list A, i:list A, i:(A -> list A -> list prop -> list prop -> prop), i:list prop, o:list prop.
+iter-> _ [] _ O O :- coq.error "No elements".
+iter-> INIT [X] F In Out :- !, F X INIT In Out.
+iter-> INIT [X|XS] F In Out :- F X {std.append XS INIT} In Mid, iter-> INIT XS F Mid Out.
+
+pred iter<- i:list A, i:list A, i:(A -> list A -> prop).
+iter<- _ [] _ :- coq.error "No elements".
+iter<- INIT [X] F :- !, F X INIT.
+iter<- INIT [X|XS] F :- iter<- INIT XS F, F X {std.append XS INIT}.
+
+pred string->ns i:string, o:list string.
+string->ns S L :- rex_split "\\." S L.
+
+:index (_ 1)
+pred join i:string, i:list string,  o:string.
+join _ [] "".
+join _ [X] X :- !.
+join Sep [X|XS] S :- join Sep XS S0, S is X ^ Sep ^ S0.
+
+pred begin-path i:list string.
+begin-path Path :- std.do! [
+  coq.env.current-path CP,
+  if (open-ns _ NSCP) (std.assert! (NSCP = CP) "NS: cannot begin a namespace inside a module that is inside a namespace") true,
+  std.map {std.findall (open-ns Y_ P_)} open-ns->string Stack,
+  coq.locate-all {join "." Path} L,
+  if (std.do! [
+     std.mem L (loc-modpath M),
+     coq.modpath->path M MP,
+     MP = {std.append CP Path}
+  ])
+    (iter-> [] Stack end-ns [] _, iter<- [] Stack begin-ns)
+    true,
+  iter<- Stack {std.rev Path} begin-ns,
+
+  open-super-path Path [],
+
+].
+
+pred std.time-do! i:list prop.
+std.time-do! [].
+std.time-do! [P|PS] :-
+  std.time P T, coq.say P "\ntakes" T "\n",
+  !,
+  std.time-do! PS.
+
+pred end-path i:list string.
+end-path Path :- std.do! [
+  std.map {std.findall (open-ns X_ P_)} nes.open-ns->string Stack,
+  std.assert! (std.appendR {std.rev Path} Bottom Stack) "NES: Ending a namespace that is not begun",
+  nes.iter-> Bottom {std.rev Path} nes.end-ns [] _,
+].
+
+
+pred open-path i:list string.
+open-path Path :- std.do! [
+  std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
+  std.forall Mods coq.env.import-module
+].
+
+pred open-super-path i:list string, i:list string.
+open-super-path [] _.
+open-super-path [P|PS] ACC :-
+  std.append ACC [P] Cur,
+  open-path Cur,
+  open-super-path PS Cur.
+
+pred export i:list string.
+export Path :- std.do! [
+  std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
+  std.forall Mods coq.env.export-module
+].
+}

structures.v

@@ -1,5 +1,6 @@
 From Coq Require Import String ssreflect ssrfun.
 From elpi Require Import elpi.
+From HB Require Export NES.
 Export String.StringSyntax.
 
 (** Technical definition from /Canonical Structures for the working Coq user/ *)
@@ -499,6 +500,7 @@ main _ :- coq.error "Usage: hb.context <CarrierTerm> <FactoryGR>".
 
 }}.
 Elpi Typecheck.
+Elpi Export HB.context.
 
 *)