Git Product home page Git Product logo

subml's Introduction

SubML (prototype) language

The SubML language provides polymorphic types and subtyping, but also existential types, inductive types and coinductive types.

Online interpreter

The easyest way to try SubML is to use our online interpreter, which can be found here.

Compiling from source

If you prefer, you can also compile SubML from source, and run it on your machine. To do so, you will need a working version of OCaml (at least 4.07.0) and opam.

You can run the following commands to get the source and install the dependencies (SubML itself will not be installed).

git clone [email protected]:rlepigre/subml.git
cd subml
opam install . --deps-only
make

You can then run Subml using dune exec -- subml. For example, you can run file lib/nat.typ with dune exec -- subml lib/nat.typ.

Note: you must run the program in the main directory (where the lib directory is accessible).

Documentation

Useful links:

  • File tutorial.typ gives an introduction to the language and its syntax.
  • The online interpreter lets you evaluate existing programs, and also write new ones.
  • The documentation of the code gives some informations on the implementation.

Editor support

Vim

Just use the install_vim target.

make install_vim

Note: the syntax coloring and automatic format detection for .typ files is user-specific by default. Files are installed under $HOME/.vim in the standard way.

Neovim

Just use the install_nvim target.

make install_nvim

Note: the syntax coloring and automatic format detection for .typ files is user-specific by default. Files are installed under $HOME/.config/nvim in the standard way.

Emacs

Just use the install_emacs target.

make install_emacs

Note: the mode is installed under the standard share/emacs/site-lisp folder, according the the $PREFIX.

Removing editor modes

To remove all installed editor modes just use the uninstall_editor_modes.

make uninstall_editor_modes

subml's People

Contributors

craff avatar rlepigre avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar

subml's Issues

Parse error may show as a type error...

In the following, the missing dot leads to the second case of the pattern matching begin left out by the parser (for the next value). But without this second case the typing is not right, and since we type-check before parsing the following value we get a type error.

type Bool = [Tru | Fls]
type SList(α,A) = μα X.[Nil | Cons of {hd : A; tl : X}]
type F(A,X) = [Nil | Cons of {hd : A; tl : X}]

val rec partition : ∀A.∀α.(A → Bool) → SList(α,A) → (SList(α,A) × SList(α,A)) =
  fun test l →
    case l of
    | []   → ([], [])
    | x::l → let α,A such that l : SList(α,A) in
             let c : (μα X F(A,X)) × (μα X.F(A,X)) = partition test l in (* <-- HERE *)
             if test x then ((x::c.1) , c.2) else (c.2,(x::c.1))

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.