-
Notifications
You must be signed in to change notification settings - Fork 51
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
51 changed files
with
4,179 additions
and
1,798 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| namespace nes { | ||
|
|
||
| % Print a namespace | ||
| pred print-path i:list string, i:(gref -> coq.pp -> prop). | ||
| print-path Path PP :- std.do! [ | ||
| std.map {std.findall (ns Path _)} (p\ mp\ p = ns _ mp) MPs, | ||
| print.pp-list MPs (print.pp-module Path PP) Out, | ||
| coq.say {coq.pp->string Out}, | ||
| ]. | ||
|
|
||
| namespace print { | ||
|
|
||
| pred pp-list i:list A, i:(A -> coq.pp -> prop), o:coq.pp. | ||
| pp-list L F Out :- std.do! [ | ||
| std.map-filter L F PPs, | ||
| Out = coq.pp.box (coq.pp.v 0) {std.intersperse (coq.pp.brk 0 0) PPs}, | ||
| ]. | ||
|
|
||
| kind context type. | ||
| type context | ||
| list string -> % readable path | ||
| int -> % length of full path | ||
| (gref -> coq.pp -> prop) -> | ||
| context. | ||
|
|
||
| % Hides `aux` modules | ||
| pred readable-path i:context, i:list string, o:list string. | ||
| readable-path (context Prefix N _) FullPath Path :- std.do! [ | ||
| std.drop N FullPath RelPath, | ||
| std.append Prefix RelPath Path, | ||
| ]. | ||
|
|
||
| pred module-context i:list string, i:modpath, i:(gref -> coq.pp -> prop), o:context. | ||
| module-context Prefix MP PP Ctx :- std.do! [ | ||
| coq.modpath->path MP FullPath, | ||
| Ctx = context Prefix {std.length FullPath} PP, | ||
| ]. | ||
|
|
||
| pred submodule-context i:context, i:modpath, o:context. | ||
| submodule-context (context _ _ PP as Ctx) MP Ctx' :- std.do! [ | ||
| coq.modpath->path MP FullPath, | ||
| readable-path Ctx FullPath Path, | ||
| Ctx' = context Path {std.length FullPath} PP, | ||
| ]. | ||
|
|
||
| pred pp-module i:list string, i:(gref -> coq.pp -> prop), i:modpath, o:coq.pp. | ||
| pp-module Prefix PP MP Out :- std.do! [ | ||
| pp-module-items {module-context Prefix MP PP} {coq.env.module MP} Out, | ||
| ]. | ||
|
|
||
| pred pp-module-items i:context i:list module-item, o:coq.pp. | ||
| pp-module-items Ctx Items Out :- | ||
| pp-list Items (pp-module-item Ctx) Out. | ||
|
|
||
| pred pp-module-item i:context, i:module-item, o:coq.pp. | ||
| pp-module-item (context _ _ PP) (gref GR) Out :- PP GR Out, !. | ||
| pp-module-item Ctx (submodule MP Items) Out :- std.do! [ | ||
| pp-module-items {submodule-context Ctx MP} Items Out, | ||
| ]. | ||
| pp-module-item Ctx (module-type MTP) Out :- pp-modtypath Ctx MTP Out. | ||
| pp-module-item Ctx (module-type-functor MTP _) Out :- pp-modtypath Ctx MTP Out. | ||
| pp-module-item Ctx (module-functor MP _) Out :- pp-modpath Ctx MP Out. | ||
|
|
||
| pred pp-path i:context, i:string, i:list string, o:coq.pp. | ||
| pp-path Ctx What FullPath Out :- std.do! [ | ||
| readable-path Ctx FullPath Path, | ||
| Out = coq.pp.box coq.pp.h [ | ||
| coq.pp.str What, coq.pp.spc, | ||
| coq.pp.str {std.string.concat "." Path}, | ||
| ], | ||
| ]. | ||
|
|
||
| pred pp-modtypath i:context, i:modtypath, o:coq.pp. | ||
| pp-modtypath Ctx MTP Out :- std.do! [ | ||
| pp-path Ctx "Module Type" {coq.modtypath->path MTP} Out, | ||
| ]. | ||
|
|
||
| pred pp-modpath i:context, i:modpath, o:coq.pp. | ||
| pp-modpath Ctx MP Out :- std.do! [ | ||
| pp-path Ctx "Module" {coq.modpath->path MP} Out, | ||
| ]. | ||
| } | ||
|
|
||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,23 +1,29 @@ | ||
| From elpi.apps.NES Extra Dependency "nes.elpi" as nes. | ||
| From elpi.apps.NES Extra Dependency "nes_synterp.elpi" as nes_synterp. | ||
| From elpi.apps Require Import NES. | ||
|
|
||
| Elpi Command Make. | ||
| Elpi Accumulate Db NES.db. | ||
| Elpi Accumulate File nes. | ||
| Elpi Accumulate lp:{{ | ||
| #[synterp] Elpi Accumulate Db NES.db. | ||
| #[synterp] Elpi Accumulate File nes_synterp. | ||
| #[synterp] Elpi Accumulate lp:{{ | ||
|
|
||
| main [str Path] :- std.do! [ | ||
| main-synterp [str Path] ActionsToOpen :- std.do! [ | ||
| nes.string->ns Path NS, | ||
| nes.begin-path NS OpenNS, | ||
| OpenNS => std.do! [ | ||
| coq.env.add-const "x" {{ 42 }} _ @transparent! _C, | ||
| nes.end-path NS _NewNS, | ||
| ], | ||
| coq.synterp-actions ActionsToOpen, | ||
| OpenNS => nes.end-path NS _NewNS, | ||
| ]. | ||
| main _ :- coq.error "usage: Make <DotSeparatedPath>". | ||
|
|
||
| }}. | ||
| #[interp] Elpi Accumulate lp:{{ | ||
| main-interp [str _] ActionsBefore :- std.do! [ | ||
| std.forall ActionsBefore coq.replay-synterp-action, | ||
| coq.env.add-const "x" {{ 42 }} _ @transparent! _C, | ||
| coq.replay-all-missing-synterp-actions, | ||
| ]. | ||
| }}. | ||
| Elpi Typecheck. | ||
| Elpi Export Make. | ||
|
|
||
| Make Cats.And.Dogs. | ||
| Print Cats.And.Dogs.x. |
Oops, something went wrong.