IPL -> HCPL: remaining name changes

lukaszcz · Mar 14, 2014 · f9f749a · f9f749a
1 parent e63fb4e
commit f9f749a
Show file tree

Hide file tree

Showing 10 changed files with 20 additions and 30 deletions.
diff --git a/README.bin b/README.bin
@@ -1,15 +1,15 @@
 
-You should be able to run HCPL from the unpacked directory with: `./hcpl
-file.hcpl'.  Type `./hcpl --help' for a list of options. It is important
-that you always run ipl from its directory, otherwise it won't start
-because it won't find the standard library in `lib/'. To test whether
-ipl works on your system you may run `scripts/run-tests.sh'. To edit
-*.hcpl files, it is recommended to use the Kate text editor. Syntax
-highlighting files for Kate may be installed with:
-`scripts/install-kate-files.sh'.
+You should be able to run HCPL from the unpacked directory with:
+`./hcpl file.hcpl'.  Type `./hcpl --help' for a list of options. It is
+important that you always run hcpl from its directory, otherwise it
+won't start because it won't find the standard library in `lib/'. To
+test whether hcpl works on your system you may run
+`scripts/run-tests.sh'. To edit *.hcpl files, it is recommended to use
+the Kate text editor. Syntax highlighting files for Kate may be
+installed with: `scripts/install-kate-files.sh'.
 
 The `examples/' subdirectory contains commented examples which form a
-tutorial introduction to IPL. Some knowledge of logic and functional
+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. In case the highlighting does not
 work, there are also html versions of the examples.
diff --git a/lib/logic.hcpl b/lib/logic.hcpl
@@ -1,4 +1,4 @@
-/* logic.ipl: Illative logic implementation.
+/* logic.hcpl: Illative logic implementation.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */

diff --git a/lib/logic/core-logic.hcpl b/lib/logic/core-logic.hcpl
@@ -1,4 +1,4 @@
-/* core-logic.ipl: Illative logic rules. This is the 'kernel' of the logic
+/* core-logic.hcpl: Illative logic rules. This is the 'kernel' of the logic
  * implementation. This file implements all basic reasoning rules. All other
  * rules and tactics are supposed to use rules from this file and NOT use
  * 'proof-of', and NOT use definitions from this file which are not a part

diff --git a/lib/logic/derived.hcpl b/lib/logic/derived.hcpl
@@ -1,4 +1,4 @@
-/* derived.ipl: Derived rules and lemmas which don't require standard proof
+/* derived.hcpl: Derived rules and lemmas which don't require standard proof
  * tactics.
  *
  * Copyright (C) 2013 by Lukasz Czajka

diff --git a/lib/logic/derived2.hcpl b/lib/logic/derived2.hcpl
@@ -1,4 +1,4 @@
-/* derived2.ipl: Derived rules and lemmas which require standard proof tactics.
+/* derived2.hcpl: Derived rules and lemmas which require standard proof tactics.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */

diff --git a/lib/logic/macros.hcpl b/lib/logic/macros.hcpl
@@ -1,4 +1,4 @@
-/* macros.ipl: Convenience logic macros.
+/* macros.hcpl: Convenience logic macros.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */
@@ -30,7 +30,7 @@ macro axiom = \args {
    | %_ -> error "axiom: wrong arguments"
 }
 
-let __ipl_ex_all_aux = \args \quant \msg {
+let __hcpl_ex_all_aux = \args \quant \msg {
    match List.split-once (== #< : >#) args with
    | [%lst1, %lst2] ->
       begin
@@ -62,8 +62,8 @@ let __ipl_ex_all_aux = \args \quant \msg {
    | %_ -> error msg
 }
 
-macro ex = \args { __ipl_ex_all_aux args #< EX ># "ex: wrong arguments" }
-macro all = \args { __ipl_ex_all_aux args #< ALL ># "all: wrong arguments" }
+macro ex = \args { __hcpl_ex_all_aux args #< EX ># "ex: wrong arguments" }
+macro all = \args { __hcpl_ex_all_aux args #< ALL ># "all: wrong arguments" }
 
 
 macro(0) last = \_ #< (hd facts) >#

diff --git a/lib/tactics/auto-type.hcpl b/lib/tactics/auto-type.hcpl
@@ -1,4 +1,4 @@
-/* auto-type.ipl: Automatic typing proof tactic.
+/* auto-type.hcpl: Automatic typing proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */

diff --git a/lib/tactics/auto.hcpl b/lib/tactics/auto.hcpl
@@ -1,4 +1,4 @@
-/* auto.ipl: Automatic proof tactic.
+/* auto.hcpl: Automatic proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */

diff --git a/lib/tactics/fact.hcpl b/lib/tactics/fact.hcpl
@@ -1,4 +1,4 @@
-/* fact.ipl: 'fact' proof tactic.
+/* fact.hcpl: 'fact' proof tactic.
  *
  * Copyright (C) 2013 by Lukasz Czajka
  */

diff --git a/src/builtins/core_builtins.ml b/src/builtins/core_builtins.ml
@@ -88,16 +88,6 @@ let xmatch lst =
 
 (* quoting etc *)
 
-let ipl_quote lst =
-  match lst with
-  | [Closure(x, env, _)] ->
-      Quote.quote x env
-  | [LambdaClosure(body, env, env_len, call_type, times_entered, attrs)] ->
-      Quote.quote (Lambda(body, env_len, call_type, times_entered, attrs)) env
-  | [x] ->
-      Quote.quote x Env.empty
-  | _ -> assert false
-
 let mark lst =
   match lst with
   | y :: Quoted(x) :: _ ->