noCanren

Translator from subset of OCaml to OCanren
README

| Upstream master | Kakadu dune | Kakadu 4.13 | Kakadu 4.13 + eucpp |
| ------------------------|----------------------|----------------------|----------------------|
| | | | |

README

noCanren is translator from subset of OCaml to OCanren.

Installatiom

noCanren can be installing using opam:

opam pin add noCanren https://github.com/Lozov-Petr/noCanren.git -y

To run the tests, you should install OCanren manually.

Subset of OCaml

Available syntax of OCaml subset:

S = x, y, z                                   (Variables)
  | fun x -> S                                (Abstaction)
  | S S                                       (Application)
  | false, 1, 2.0, '3', "4", etc.             (Constant)
  | (S, S)                                    (Pair)
  | C (S1, ..., Sn)                           (Constructor)
  | not, (&&), (||), (==), (<>)               (Boolean functions)
  | let f x1 ... xn = S in S                  (Let-binding)
  | let rec f x1 ... xn = S in S              (Recursive let-binding)
  | if S then S else S                        (If-then-else)
  | pattern matching                          (Pattern matching)

Pattern matching

Available patterns for pattern matching:

P = _                                         (Wildcard)
  | x, y, z                                   (Variables)
  | (P, P)                                    (Pairs)
  | C (P1, ..., Pn)                           (Constructors)

Patterns must be disjunct.

Pattern matching can be used in the following form:

match S with
| P1 -> S1
| P2 -> S2
...
| Pn -> Sn

Translating

Usage:

noCanren <options> <input-file>

Available options:

-o <file>  Set output file name to <file>
-high-order-mode  Switch to high-order mode
-unnesting-mode  Switch to unnesting mode
-without-activate-tactics  Disable activate tactic (only for high-order mode)
-non-deterministic-activate-tactic  Use non-deterministic activate tactic (only for high-order mode)
-deterministic-activate-tactic  Use deterministic activate tactic (only for high-order mode)
-use-call-by-need  Use call-by-need extension of high-order mode (only for high-order mode)
-need-polymorphism  For supporting of polymorphism (only for unnesting mode)
-without-false  For simplified logical relational (only for unnesting mode)
-standart-bool  Enable standart bool relations (only for unnesting mode)
-without-beta-reduction  Disable beta-redactions after conversion (for both modes)
-without-normalization  Disable normalization after conversion (for both modes)
-not-move-unifications  Don't move unifications and disequality constrains after conversion (for both modes)
-leave-constuctors  Conversion is without lawercase-renaming of constructors (for both modes)
-subst-only-util-vars  Use beta-reduction only for additional variables (for both modes)
-spec-tree <file>  Set output file name for specialization tree to <file>
-show-result  Show result of conversion in terminal
-help  Display this list of options
Install
Published
03 May 2022
Maintainers
Sources
0.3.0.tar.gz
sha256=18c8bdd588e445c6683062beb7d811d2ce609c00aaf3fcaf5da944dcf4d2cc54
sha512=cc53c64ba5ab4022d9ec086337bb30668fcf0369d60ba5777ea7703aff847b67400b61a870333cc36eb13b6c1e8d435245f8ceacd34a317a9bdfb43b85aed9da
Dependencies
ocamlformat
with-test
odoc
with-doc
OCanren-ppx
>= "0.3.0~"
OCanren
>= "0.3.0~"
ocaml
>= "4.13" & < "4.15"
dune
>= "2.8"
Reverse Dependencies