Skip to content

About

Semantic type refutation

Resources

Stars

3 stars

Watchers

0 watching

Forks

Repository files navigation

caprice-lang

This project implements the Caprice programming language.

Caprice is a semantically typed functional language with types as values.

Installation

Caprice is built with OCaml 5.5.

Via opam, install OCaml 5.5 and then install the dependencies. Answer y/yes to all questions:

opam update
opam switch create 5.5.2
opam install . --deps-only

Then, build the repository with dune:

dune build
make test

The installation is tested on WSL2 for Windows 11.

Developing

Develop in the caprice-lang repository with the following developer tools:

opam install ocaml-lsp-server ocamlformat

If you are using VS Code, use the OCaml Platform extension.

To write programs in the Caprice language, it's suggested to install the VS Code language extension. Navigate to the caprice-language-extension directory and follow the instructions in README.md there.

Benchmarking

For benchmarking, it is recommended to use a compiler switch with flambda for better optimization.

opam update
opam switch create 5.5+flambda 5.5.2+options ocaml-option-flambda
opam install . --deps-only

Then, build in release mode to perform optimizations.

dune build --profile=release

Now, run benchmarks on entire folders or specific files. Benchmark throughput with --sec or some number of trials with --trials. All type checker options still work as command line arguments. E.g.

./bench.exe file/path/or/directory --sec 4 -s never -r
./bench.exe file/path/or/directory --trials 1000 -s only -w no

Programming with Caprice

Write Caprice programs in .caprice files. With the project built, you can run the type checker with the ./typecheck.exe executable. For example,

./typecheck.exe path/to/file/name.caprice

type checks filename.caprice. The output may contain one of several messages:

  • Exhausted: every possible program path was run and exhausted, and the program is well-typed.
  • Found error: the type checker found some type refutation, so the program is ill-typed.
  • Exhausted pruned tree: many program paths were run, and the tree was exhausted up to some depth without error, but the program may still be ill-typed.
  • Timeout: no error was found within the allowed time, so the program may still be ill-typed.
  • Unknown: the SMT solver failed to return an answer quickly, so some program path was skipped, but no error was found otherwise; the program may still be ill-typed.

About

Semantic type refutation

Resources

Stars

3 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages