README

README.md

@@ -0,0 +1,78 @@
+HCPL is a programming language and a proof checker based on illative
+combinatory logic - a foundational system dating back to the work of
+Haskell Curry and his school. In one sentence, one could (somewhat
+metaphorically) say that the logic is dynamically typed. As a
+programming language, HCPL is similar to Lisp but with more syntactic
+sugar.
+
+Features
+========
+* Functional language with pattern matching, macros, modules and
+  custom syntax extensions.
+* Relatively efficient interpreter, with unboxed values, etc.
+* Higher-order illative logic with basic support for inductive
+  datatypes.
+* Rudimentary tactics and standard library.
+* Syntax highlighting for Kate.
+
+The current version is a prototype, but it is complete and stable
+enough to be usable.
+
+Examples
+========
+
+The [`examples/`](examples) subdirectory of the data directory
+contains commented examples which form a tutorial introduction to
+HCPL. Some knowledge of logic and functional programming is necessary
+to understand them. You should read the examples in their numerical
+order. Preferably, *.hcpl files should be edited in Kate as syntax
+highlighting is installed for this editor. In case the highlighting
+does not work, there are also html versions of the examples.
+
+Requirements
+============
+* OCaml
+* dune
+* m4, sed, diff, GNU make
+* Kate text editor
+
+The Kate text editor is not strictly necessary, but highly
+recommended, because syntax highlighting is available and
+automatically installed for it.
+
+Installation and usage
+======================
+
+To compile HCPL type:
+```
+make
+```
+
+To run tests type:
+```
+make test
+```
+
+To install HCPL type:
+```
+make configure
+make
+make install
+```
+
+During installation you will be asked for the data directory. In this
+directory the examples, the standard library and other data files of
+HCPL will be stored.
+
+After installation you should be able to run HCPL with: `hcpl
+file.hcpl` or `hcpl -i` for REPL.  Type `hcpl --help` for a list of
+options. To remove HCPL from your system type: `uninstall-hcpl` (note:
+this will remove the data directory completely).
+
+Copyright and license
+=====================
+
+Copyright (C) 2013-2021 by Lukasz Czajka
+
+HCPL is distributed under the MIT license. See the [LICENSE](LICENSE)
+file.

examples/example_001.hcpl

@@ -1,9 +1,8 @@
-
 /* Example 01
 
    Programming in HCPL.
 
-   In this example it is shown how to write programs in IPL. This does not
+   In this example it is shown how to write programs in HCPL. This does not
    cover the whole language. In particular, macros are not covered.
 
    Proving theorems is covered in succeeding examples.
@@ -66,7 +65,7 @@ print (power 3 4); // prints 81
 print (power 2 16); // prints 65536
 print (power 5 7); // prints 78125
 
-// Evaluation in IPL is eager by default, but this should not be relied on.
+// Evaluation in HCPL is eager by default, but this should not be relied on.
 
 /* The brackets {} and () are used to embrace expressions so
    that they will be treated as single terms.

examples/example_001.html

@@ -11,9 +11,9 @@
 
 <i><span style='color:#898887;'>/* Example 01</span></i>
 
-<i><span style='color:#898887;'>   Programming in IPL.</span></i>
+<i><span style='color:#898887;'>   Programming in HCPL.</span></i>
 
-<i><span style='color:#898887;'>   In this example it is shown how to write programs in IPL. This does not</span></i>
+<i><span style='color:#898887;'>   In this example it is shown how to write programs in HCPL. This does not</span></i>
 <i><span style='color:#898887;'>   cover the whole language. In particular, macros are not covered.</span></i>
 
 <i><span style='color:#898887;'>   Proving theorems is covered in succeeding examples.</span></i>
@@ -76,7 +76,7 @@
 print (power <span style='color:#b08000;'>2</span> <span style='color:#b08000;'>16</span>); <i><span style='color:#898887;'>// prints 65536</span></i>
 print (power <span style='color:#b08000;'>5</span> <span style='color:#b08000;'>7</span>); <i><span style='color:#898887;'>// prints 78125</span></i>
 
-<i><span style='color:#898887;'>// Evaluation in IPL is eager by default, but this should not be relied on.</span></i>
+<i><span style='color:#898887;'>// Evaluation in HCPL is eager by default, but this should not be relied on.</span></i>
 
 <i><span style='color:#898887;'>/* The brackets {} and () are used to embrace expressions so</span></i>
 <i><span style='color:#898887;'>   that they will be treated as single terms.</span></i>

examples/example_002.hcpl

@@ -1,4 +1,3 @@
-
 /* Example 02
 
    Propositional logic.
@@ -59,7 +58,7 @@ qed;
  lib/logic/core-logic.ipl which implement basic inference rules. Inference rules
  are implemented as functions which given proofs of premises (and possibly some
  additional arguments) evaluate to a proof of the conclusion. Derived rules and
- proof tactics may be simply implemented as functions in IPL which manipulate proofs
+ proof tactics may be simply implemented as functions in HCPL which manipulate proofs
  using the primitive or previously defined rules.
 */
 
@@ -94,20 +93,20 @@ proof
 qed;
 
 /*
- The logic of IPL could be described as "dynamically typed". No typing discipline is statically
+ The logic of HCPL could be described as "dynamically typed". No typing discipline is statically
  enforced (unless such enforcement is explicitly asked for), but some inference rules need
  to be supplied with typing derivations to ensure consistency of the logic. Such derivations are
  usually obtained automatically with the auto-type tactic, which given a formula of the form
  '(phi in T) tries to find its proof, and returns the proof when successful, or fails with
  an error message otherwise.
 
- Types in IPL are thus similar to sets in set theory as they may freely occur in formulas, and
+ Types in HCPL are thus similar to sets in set theory as they may freely occur in formulas, and
  the relation `in' of belonging to a type is an ordinary function. In fact, `in' is simply
  defined as \x \y (y x). Hence, a type is just a function which returns true for some of its
  arguments (but not every function returning true for some arguments is a type!). The functions
  which are types are often non-computable.
 
- Despite being similar to sets, the types of IPL are also close to types in programming languages
+ Despite being similar to sets, the types of HCPL are also close to types in programming languages
  or type theory. Typing rules in the logic (to be found in lib/logic/core-logic.ipl) closely
  resemble rules in type theory. In fact, the tactic `auto-type' (currently) just implements
  a variation of the type-checking algorithm for simple types.

examples/example_002.html

@@ -69,7 +69,7 @@
 <i><span style='color:#898887;'> lib/logic/core-logic.ipl which implement basic inference rules. Inference rules</span></i>
 <i><span style='color:#898887;'> are implemented as functions which given proofs of premises (and possibly some</span></i>
 <i><span style='color:#898887;'> additional arguments) evaluate to a proof of the conclusion. Derived rules and</span></i>
-<i><span style='color:#898887;'> proof tactics may be simply implemented as functions in IPL which manipulate proofs</span></i>
+<i><span style='color:#898887;'> proof tactics may be simply implemented as functions in HCPL which manipulate proofs</span></i>
 <i><span style='color:#898887;'> using the primitive or previously defined rules.</span></i>
 <i><span style='color:#898887;'>*/</span></i>
 
@@ -104,20 +104,20 @@
 <b><span style='color:#000000;'>qed</span></b>;
 
 <i><span style='color:#898887;'>/*</span></i>
-<i><span style='color:#898887;'> The logic of IPL could be described as &quot;dynamically typed&quot;. No typing discipline is statically</span></i>
+<i><span style='color:#898887;'> The logic of HCPL could be described as &quot;dynamically typed&quot;. No typing discipline is statically</span></i>
 <i><span style='color:#898887;'> enforced (unless such enforcement is explicitly asked for), but some inference rules need</span></i>
 <i><span style='color:#898887;'> to be supplied with typing derivations to ensure consistency of the logic. Such derivations are</span></i>
 <i><span style='color:#898887;'> usually obtained automatically with the auto-type tactic, which given a formula of the form</span></i>
 <i><span style='color:#898887;'> '(phi in T) tries to find its proof, and returns the proof when successful, or fails with</span></i>
 <i><span style='color:#898887;'> an error message otherwise.</span></i>
 
-<i><span style='color:#898887;'> Types in IPL are thus similar to sets in set theory as they may freely occur in formulas, and</span></i>
+<i><span style='color:#898887;'> Types in HCPL are thus similar to sets in set theory as they may freely occur in formulas, and</span></i>
 <i><span style='color:#898887;'> the relation `in' of belonging to a type is an ordinary function. In fact, `in' is simply</span></i>
 <i><span style='color:#898887;'> defined as \x \y (y x). Hence, a type is just a function which returns true for some of its</span></i>
 <i><span style='color:#898887;'> arguments (but not every function returning true for some arguments is a type!). The functions</span></i>
 <i><span style='color:#898887;'> which are types are often non-computable.</span></i>
 
-<i><span style='color:#898887;'> Despite being similar to sets, the types of IPL are also close to types in programming languages</span></i>
+<i><span style='color:#898887;'> Despite being similar to sets, the types of HCPL are also close to types in programming languages</span></i>
 <i><span style='color:#898887;'> or type theory. Typing rules in the logic (to be found in lib/logic/core-logic.ipl) closely</span></i>
 <i><span style='color:#898887;'> resemble rules in type theory. In fact, the tactic `auto-type' (currently) just implements</span></i>
 <i><span style='color:#898887;'> a variation of the type-checking algorithm for simple types.</span></i>

tests/slow/test_004.ml

@@ -1,7 +1,6 @@
-
 (* Note: This is a naive translation of test_004.ipl. It is actually
-   slower, because the IPL interpreter is better at keeping track of
-   what really needs a bignum and what doesn't. The IPL interpreter
+   slower, because the HCPL interpreter is better at keeping track of
+   what really needs a bignum and what doesn't. The HCPL interpreter
    uses unboxed integers whenever possible, but converts automatically
    to big integers when necessary.  *)