Permalink
Commits on Mar 8, 2017
Commits on Mar 6, 2017
  1. Fix examples/bool.m31

    SkySkimmer committed Mar 6, 2017
Commits on Feb 5, 2017
  1. Merge pull request #377 from andrejbauer/better-externals

    SkySkimmer committed Feb 5, 2017
    OCaml style externals.
Commits on Feb 4, 2017
Commits on Feb 2, 2017
  1. Merge pull request #380 from andrejbauer/print-with-colon-greater

    SkySkimmer committed Feb 2, 2017
    Print with colon greater, close #379
Commits on Jan 5, 2017
  1. Merge pull request #376 from andrejbauer/let-patterns

    SkySkimmer committed Jan 5, 2017
    Let patterns
  2. Allow ML-type annotations in let-patterns.

    andrejbauer committed Jan 5, 2017
    We can now write
    
        let (?p) : schema = c
  3. Print ML-type-meta-variables with underscores.

    andrejbauer committed Jan 5, 2017
    It's confusing that ML-type existential variables are printed the same
    way as pattern variables. Let's use underscores, like other MLs.
  4. Incorporate let-patterns into lets.

    andrejbauer committed Jan 5, 2017
    This allows us to write
    
        let x = ...
        and (?p) = ...
Commits on Dec 28, 2016
  1. OCaml style externals.

    andrejbauer committed Dec 28, 2016
    Declare externals with a top-level command
    
        external foo : mlschema = "bar"
    
    This follows OCaml and Eff syntax. The benefit is that we can write down the type in a
    humane way, instead of having to put it in the OCaml source.
Commits on Dec 27, 2016
  1. Merge branch 'haselwarter-fix-application-locations'

    andrejbauer committed Dec 27, 2016
    rge is necessary,
  2. Merge branch 'fix-application-locations' of https://github.com/haselw…

    andrejbauer committed Dec 27, 2016
    …arter/andromeda into haselwarter-fix-application-locations
Commits on Dec 26, 2016
  1. Merge pull request #375 from SkySkimmer/dynamic-builtin

    andrejbauer committed Dec 26, 2016
    Dynamic builtin ML type
Commits on Dec 25, 2016
  1. Tests for let-patterns.

    andrejbauer committed Dec 25, 2016
  2. Allow tuples in let-patterns.

    andrejbauer committed Dec 25, 2016
    This alows one to write
    
        let (?x, ?y) = ...
    
    instead of
    
        let ((?x, ?y)) = ...
  3. Add let-statements with patterns.

    andrejbauer committed Dec 25, 2016
    The statement
    
        let (?p) = c1 in c2
    
    is equivalent to
    
        match c1 with ?p => c2 end
    
    And there is also a top-level form
    
        let (?p) = c
    
    There are other minor changes, mostly cosmetic. I got rid of `Mlty.ungeneralized_schema`
    because it was getting used in a dangerous way (it was easy to apply
    `Tyenv.normalize_schema` on it).
Commits on Dec 24, 2016
  1. Dynamic variables are used through a builtin type.

    SkySkimmer committed Dec 24, 2016
    It has toplevel-only constructor `dynamic x = c`, toplevel update
    `now x = c`, in computation update `now x = c in c'` and access
    `current x`.
  2. Merge pull request #373 from andrejbauer/ml-ascription

    SkySkimmer committed Dec 24, 2016
    Type annotations
Commits on Dec 23, 2016
  1. Allow TT annotations in let bindings.

    andrejbauer committed Dec 23, 2016
    The only form which is allowed is
    
        let x : t = c
    
    where `t` is a TT type. It is equivalent to
    
        let x = c : t
    
    In particular, this does not make sense:
    
        let f x y : t = c
    
    Is it a function or a lambda?
  2. Arguments in recursive definitions cannot be polymorphic.

    andrejbauer committed Dec 23, 2016
    Because they are just like arguments of functions, which cannot
    be polymorphic either (why?).
  3. Rename `bound` to `ctx`.

    andrejbauer committed Dec 23, 2016
    Historically desugaring only carried around a list of bound variables,
    but later we switched to a context. This finally renames `bound` to `ctx`
    to correctly indicate the role.
  4. Reorganization of syntax (WIP).

    andrejbauer committed Dec 23, 2016
    This is a partial commit which does not compile. But the plan is
    to create more intermediate langauges:
    
    * `Input` is produced by the parser and consumed by desugaring
    * `Dsyntax` is produced by desugaring and consumed by typechecking
    * `Rsyntax` is produced by typechekcing and consumed by runtime
    
    This is necessary because with fancier typing annotations we cannot get
    away with the polymorphic `Syntax` anymore. And that was ugly as hell
    anyhow, and had no chance of surviving for long.
    
    At the same time this code is implementing `let`-annotations (they
    caused the split of syntax levels).