package elpi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=a8795ed981e55227f1edffb71f7620d0534f14d2de276127e275b2efa9237a0c
sha512=d964eac99057425e9dd67a5186b42b934fad538923b9e78c563c7be4bf22339944f9edcc3ea2f836d775264826cbcfa856ab6dddb9437c89cc1444c6a5b33cac
CHANGES.md.html
v1.10.2 (February 2020)
Builtin:
occurs now accepts arguments of different types
API:
expose beta reduction on raw terms
v1.10.1 (February 2020)
make API.Builtin_checker module public so that third parties can reuse the source
v1.10.0 (February 2020)
Compiler:
large refactoring to separate the table of global (statically initialized) symbols, the table of symbols of a program being compiled and the table of symbols used at runtime.
API for separate compilation.
API:
Setup.init now returns a handle to an elpi instance to be passed to many other APIs.
New APIs Compile.unit and Compile.assemble for separate compilation.
Constants.from_stringc and Constants.mk*S API removed in favor for Constants.declare_global_symbol (to be used in module initialization code).
v1.9.1 (January 2020)
Tests:
Fix testing framework on runners pre 1.9.0.
Parser:
Line numbers after quotations were wrong, since
\n
inside quotations were not taken into account.
Typing:
Name alias abbreviations are not refolded in error messages. Eg.
typeabbrev x int
does not take overint
, whiletypeabbrev x (list int)
does overlist int
.Fix type abbreviation refolding, was not working on some cases.
Stdlib:
Fix
is
functionint_of_string
to do what it saysNew
is
functionrhc : string -> int
computes the inverse ofchr
v1.9.0 (January 2020)
Typing:
typeabbrev
declarations are now taken into account and unfolded by the compiler. The type checker refolds abbreviations when printing error messages with the following caveat: when two type abbreviations can be refolded the last declared one wins.
Compiler:
@macro
are no more accepted in types, sincetypeabbrev
provides the same functionality.fix clash between builtin names and type names
accumulate
is idempotent: accumulating the same file a second time has no effect.
FFI:
built in predicate are allowed to not assign (not produce a value) for output and input-output arguments.
input-output arguments are forced to be
Conversion.t
of type'a ioarg
, and recommended to wrap any nested type not able to represent variables inioarg
. Egint option
should beint ioarg option ioarg
. In this way one can safely call these builtins with non-ground terms, such assome _
, for example to assert the result is notnone
but without providing a ground term such assome 3
.MLData
declarations forOpaqueData
are no more named using a macro but rather using a type abbreviation. This can break user code. The fix is to substitute@myopaquetype
withmyopaquetype
everywhere.
Stdlib:
diagnostic
data type to be used as anioarg
for builtins that can fail with a relevant error message. On the ML side one can usedElpi.Builtin.mkOK
andElpi.Builtin.mkERROR "msg"
to build its values.std.assert-ok!
,std.forall-ok
,std.do-ok!
,std.lift-ok
andstd.while-ok-do!
commodity predicates.All operators for
calc
(infix_ is _
) now come with a type declaration.
v1.8.0 (October 2019)
Bugfix:
shorten foo.{ bar }.
whenfoo.bar
is a builtin used to be miscompiled.elpi-typechecker.elpi
now correclty stops printing warnings after it printed 10 (used to stop after he processed 10, that may not be the same thing, since some warnings are suppressed).
Parser:
Interpret
-2
(with no space) as the negative2
not as the constant-2
. This wayX is 3 - 2
andY is 3 + -2
are both valid.
FFI:
OpaqueData
now requires a ternary comparison, not just equality.
Stdlib:
new data type
cmp
for ternary comparison.std.set
andstd.map
now based on ternary comparison.
Builtin:
cmp_term
giving an order on ground terms.ground_term
to check if a term is ground.
v1.7.0 (September 2019)
Parser:
Tolerate trailing
,
in lists, eg[1,2,3,]
is now parsed as[1,2,3]
.Error if the input of
Parse.goal_from_string
contains extra tokensBinary conjunction
&
is now turned on the fly into the nary one,
.
Bugfix:
Nasty bug in pruning during higher order unification, see #36.
Discard
is now considered a stack term, and is turned into an unification variable on heapification.API.RawData.look
now expandsUVar
correctly
Stdlib:
set
andmap
for arbitrary terms equipped with an order relation. Based on the code of OCaml'sMap
andSet
library.New API
map.remove
for maps on builtin data.
FFI:
New
ContextualConversion
module andctx_readback
type. In an FFI call one can specify a readback for the hypothetical context that is run once and its output is give to the ML code instead of the "raw" constraints and hyp list.
API:
Commodity functions in
Elpi.Builtin
to export as built-in OCaml'sSet.S
andMap.S
interfaces (the output ofSet.Make
andMap.Make
). All data is limited to be a closed term.Constants.andc2
was removedFlexibleData.Elpi.make
takes no~lvl
argument (it is always0
)RawData.view
no more containsDiscard
since it is not an heap term
Misc:
Pretty printer for unification variable made re-entrant w.r.t. calls to the CHR engine (used to lose the mapping between heap cells and names)
Pretty printer for solution abstracted over a context (part of the solution). In this way the result can be printed correctly even if the runtime has been destroyed.
Default paths for finding
.elpi
files fixed after the switch to duneA few more tests regarding unification, data structures and performance
v1.6.0 (July 2019)
Builtin:
same_term
(infix==
) for Prolog's non-logical comparison (without instantiation).set
andmap A
(A
only allowed to be a closed term) onstring
,int
andloc
keys.
Compiler:
provide line number on error about duplicate mode declaration
elpi-checker is faster and bails out after 10 seconds
FFI:
allow
AlgebraicData
declarations to mixM
andMS
constructorsConversion.t
for closed terms (no unification variable and no variables bound by the program)
Tests:
typecheck all tests and measure type checking time
v1.5.2 (July 2019)
Test suite: ship elpi-quoted_syntax.elpi
v1.5.1 (July 2019)
Test suite: print the log of the first failure to ease debugging on third party CI.
v1.5.0 (July 2019)
Elpi 1.5 requires OCaml 4.04 or newer
REPL:
type errors are considered fatal, pass
-no-tc
to skip type checking.use dune subst in order to implement
-version
flag to the command line utility.
Runtime:
reset unification variables names map at each execution. This makes the names of variable printed in a reproducible way across executions.
FFI:
readback
is now as powerful asembed
and can generate extra goals. The two types are now dual.
v1.4 (June 2019)
Elpi 1.4 requires OCaml 4.04 or newer
Sources and build: Switch to dune, with a little make base wrapper. As a result of dune wrapping the library all sources are renamed from
elpi_x.ml
tox.ml
, and each moduleElpi_X
is now available asElpi.X
. In particular clients must now useElpi.API
andElpi.Builtin
.FFI:
Conversion.TypeErr
now carries the depth at which the error is found, so that the term payload can be correctly printed.Built in predicates are allowed to raise TypeErr in their body
BuiltInPredicate.Full
now returns a list ofextra_goals
, exactly asConversion.embed
does making conversion code easy to call in the body of a predicate.
v1.3 (June 2019)
Elpi 1.3 requires OCaml 4.04 or newer
API: Major reorganization: The Extend module has gone; the module structure is flat and ordered by complexity. Most modules are named after the kind of data they let one represent. Eg
AlgebraicData
,OpaqueData
,FlexibleData
or for low level accessRawOpaqueData
orRawData
for naked terms.FFI:
RawData.mkAppL
andRawData.mkAppSL
handy constructorscustom_state
renamedstate
No more
solution
in the type of builtin predicates but ratherconstraints
andstate
explicitlyOnly one type of extensible state to that the same code can be used to generate the query at compile time and convert data at run time
Unify
MLCData
andMLADT
intoMLData
AlgebraicData.t
supportsC
for containers, so that one can modeltype t = A | B of list t
as
K("a", N, .. K("b",(C ((fun x -> list x),N)), ..
new
FlexibleTerm.Elpi.t
andFlexibleTerm.Map
to represent Elpi's unification variables and keep a bijective map between them and any host application data.RawData.term
contains no moreUVar
,AppUVar
,Arg
andAppArg
but onlyUnifVar of FlexibleTerm.Elpi.t * term list
.Simple GADT for describing a query. When a query is built that way, the
solution
contains an output field holding data of the type described by the query.
Library:
replace
mode (std.mem i i)
with(std.mem i o)
: member can be assignedseparate
std.mem!
andstd.mem
v1.2 (April 2019)
Fix:
equality up-to eta on rigid terms (used to work only on flexible terms)
expand_*
in charge of putting unification variables in canonical form was sometimes omitting some lambdas in one of its outputs
Language:
shorten
directive to give short names to symbols that live in namespaces, e.g.shorten std.{ rev }
lets one writerev
instead ofstd.rev
spilling understands implication and conjunction, e.g.
g { h => (a, f) }
becomes(h => (a, f X)), g X
syntax of
.. as X
to bind subterms in the head of a clause changed precedence. In particularlam x\ B as X
bindslam x\ B
toX
(instead of justB
, as it was the case in previous versions):index(...)
attribute for predicates to select which argument(s) should be indexed and at which depth. Multi-argument indexing and deep-indexing are based on unification hashes, see ELPI.md for more details
Library:
predefined types:
bool
withtt
andff
option A
withnone
andsome A
pair A B
withpr A B
,fst
andsnd
predefined control structure:
if C T E
standard library (taken from coq-elpi) in the
std
namespace.Conventions:
all errors are signalled using one of the following two symbols that can be overridden by grafting clauses to hide them, namely
fatal-error
andfatal-error-w-data
the
!
suffix is for (variants) of predicates that generate only the first solutionall predicates have mode declarations that follow their functional interpretation; variants keeping the relational interpretation are named using the
R
suffix
Symbols:
debug-print
,ignore-failure!
,assert!
,spy
,spy!
,unsafe-cast
,length
,rev
,last
,append
,appendR
,take
,drop
,drop-last
,split-at
,fold
,fold2
,map
,map-i
,map2
,map2_filter
,nth
,lookup
,lookup!
,mem
,exists
,exists2
,forall
,forall2
,filter
,zip
,unzip
,flatten
,null
,iota
,flip
,time
,do!
,spy-do!
,any->string
,random.init
,random.self_init
,random.int
While the predicates in the library are reasonably tested, their names and name spaces may change in the future, e.g. a specific name space for list related code may be created (as well for strings, debug, etc).
Builtin:
name
is now typed asany -> variadic any prop
to support the following two use cases:name T
succeeds ifT
is an eigenvariable (even if it is applied)name T HD ARGS
relatesT
(an applied eigenvariable) to its head and arguments (as a list):pi f x y\ name (f x y) f [x,y]
new builtin
constant
working asname
but for non-eigenvariableshalt
now accepts any term, not just stringsgetenv
is now typed asstring -> option string
and never fails. The old semantics can be obtained by just writinggetenv Name (some Value)
API:
new data type of locations in the source file:
Ast.Loc.t
exception
ParseError(loc, message)
systematically used in the parsing API (no more leak of exceptions or data types from the internal parsing engine, i.e. no moreNotInProlog
orStream.Error
exceptions)type of quotations handlers changed: they now receive in input the location of the quoted text in order to be able to locate their own parsing errors
simplified term constructors:
mkConst
split intomkGlobal
andmkBound
variants with trailing
S
taking astring
rather than a global constant, e.g.mkAppS
,mkGlobalS
,mkBuiltinS
mkBuiltinName
removed (replace bymkBuiltinS
)constant
spillc
exported: one can not build a term such asf {g a}
by writingmkAppS "f" (mkApp spillc (mkAppS "g" (mkGlobalS "a") []) []
FFI:
to_term
andof_term
renamed toembed
andreadback
and made stateful. They can access the state, the hypothetical context and the constraint store (exactly asFull
ffi builtins do) and can return an updated state. Moreoverembed
can generate new goals (eg declaration of constraints) so that data that requires companion constraints fits the capabilities of the FFI (no need to simulate that by using aFull
predicate with arguments of typeany
, as coq-elpi was doing)Arguments to builtin predicates now distinguish between
In
ML code must receive the data, type error is the data cannot be represented in MLOut
ML code receivedKeep
orDiscard
so that it can avoid generating data the caller is not binding backInOut
ML code receivesData of 'a
orNoData
. The latter case is when the caller passed_
, while the former contains the actual data
In the declaration of a data type for the FFI, the
ty
field is no more a string but an AST, so that containers (egval list : 'a data -> 'a list data
) can more easily generate the composite typeNew GADT to describe simple ADTs (with no binders)
Compiler:
handling of locations for quotations
better error reporting: many errors now come with a location
REPL:
more structure in the output of
--help
including hints for the tracing optionsnew option
-print-passes
to debug the compiler
Test Suite:
rewritten using more OCaml & Dune and less bash & make. Requires
dune
,cmdliner
andANSITerminal
in order to build
v1.1.1 (October 2018)
Fix:
beta
was not callingderef_*
in all cases, possibly terminating reduction too early (and raising an anomaly)
v1.1 (September 2018)
Language:
CHR semantics conformed to the "revised operational semantics", that is roughly the following:
1 for each active constraint (just declared via declare_constraint)
2 for each rule
3 for each position j of the active constraint (from 0 to n)
4 for each permutation of constraints having the active at j
5 try apply the rule
6 remove constraints to be removed from the current set of permutations and the set of active or passive constraints
In Elpi 1.0 loops 3 and 2 were swapped (by mistake)
CHR keys refined. In
declare_constraints C KEYS
:KEYS
must be a list of variables (no more special caseKEYS = Var
)KEYS
=[_,...]
labels the constraint with the unique variable_
. In other words_
is a master key one can use to label constraints that share no other variable and that have to be combined together. The master key will never be assigned, hence it does not count for resumptionKEYS
=[]
is accepted with the following meaning: constraints with no key are never resumed automatically and are never combined with other constraints
Builtin:
halt
is now typed asvariadic string prop
and the strings passed are printed when the interpreter halts
Aesthetic:
bound variables are now printed as
c0, c1, ...
instead ofx0, x1, ...
to avoid ambiguity withX0, X1, ...
on small/far-away screens
API changes:
rename:
custom_constraints
->state
(record field)syntactic_constraints
->constraints
(type)CustomConstraint
->CustomState
(module)
add:
StrMap
andStrSet
: exposepp
andshow
alias:
Data.Extend.solution
~Data.solution
(cast:Data.Extend.of_solution
)
Compilation:
require re >= 1.7.2 (the version introducing
Re_str
->Re.str
)
Misc:
improved some error messages, minor fixes to elpi-checker
v1.0 (April 2018)
Second public release, developed in tandem with coq-elpi and matita-elpi.
The programming language features syntactic constraints (suspended goals) and a meta language (inspired by CHR) to manipulate the constrain store.
There is an API for clients letting one drive the interpreter and extend the set of built-in predicates, register quotations and anti-quotations, etc.
The software is now built using findlib into a library. The standalone interpreter is just a regular client of the API.
LPAR 2015 (Jul 12, 2015)
First public release accompanying the paper ELPI: fast, Embeddable, λProlog Interpreter