-
Notifications
You must be signed in to change notification settings - Fork 37
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
42 changed files
with
3,483 additions
and
1,968 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
Large diffs are not rendered by default.
Oops, something went wrong.
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 |
---|---|---|
|
@@ -5,6 +5,7 @@ | |
(executable | ||
(name pp) | ||
(modules pp) | ||
(promote) | ||
(libraries elpi.ppx ppxlib)) | ||
|
||
(include dune.inc) | ||
|
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 |
---|---|---|
|
@@ -2,9 +2,6 @@ | |
|
||
typeabbrev simple int. % simple | ||
|
||
pred map.simple i:simple, o:simple. | ||
map.simple A B :- ((=) A B). | ||
|
||
|
||
|
||
|
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 |
---|---|---|
@@ -1,37 +1,23 @@ | ||
|
||
|
||
% tctx | ||
kind tctx type. | ||
% tyctx | ||
kind tyctx type. | ||
type tentry nominal -> string -> bool -> prop. % TEntry | ||
|
||
% ty | ||
kind ty type. | ||
type tapp string -> ty -> ty. % TApp | ||
type tall bool -> string -> (ty -> ty) -> ty. % TAll | ||
|
||
pred map.ty i:ty, o:ty. | ||
map.ty (tvar A0) (tvar B0) :- ((=) A0 B0). | ||
map.ty (tapp A0 A1) (tapp B0 B1) :- ((=) A0 B0), (map.ty A1 B1). | ||
map.ty (tall A0 A1 A2) (tall B0 B1 B2) :- ((=) A0 B0), ((=) A1 B1), (pi x fixme x => (=) A2 B2). | ||
|
||
|
||
|
||
% ctx | ||
kind ctx type. | ||
% tctx | ||
kind tctx type. | ||
type entry nominal -> string -> ty -> prop. % Entry | ||
|
||
% term | ||
kind term type. | ||
type app term -> term -> term. % App | ||
type lam ty -> string -> (term -> term) -> term. % Lam | ||
|
||
pred map.term i:term, o:term. | ||
map.term (var A0) (var B0) :- ((=) A0 B0). | ||
map.term (app A0 A1) (app B0 B1) :- (map.term A0 B0), (map.term A1 B1). | ||
map.term (lam A0 A1 A2) (lam B0 B1 B2) :- ((=) A0 B0), ((=) A1 B1), (pi x fixme x => (=) A2 B2). | ||
|
||
|
||
|
||
|
||
|
||
|
Oops, something went wrong.