~dannypsnl/violet

a1b3cce59985ff8d9ab16ffeaa3d78e491103308 — Lîm Tsú-thuàn 3 months ago 2b8840b
minimal open command

Signed-off-by: Lîm Tsú-thuàn <dannypsnl@tuta.io>
M Main.lean => Main.lean +2 -4
@@ 1,9 1,7 @@
import Violet
import Violet.CLI
open System
open Lean Meta Elab Command
open Violet.Parser (parseFile)
open Violet.Ast.Surface
open Lean System
open Violet Ast.Surface Parser

register_option violet.verbose : Bool := {
  defValue := false

M Tests/Parsing.lean => Tests/Parsing.lean +1 -1
@@ 2,7 2,7 @@ import LSpec
import Violet.Parser

open LSpec
open Violet.Parser Violet.Ast.Surface
open Violet Parser Ast.Surface

def dummyPos : Lean.Position := { line := 0, column := 0 }


M Violet.lean => Violet.lean +1 -5
@@ 1,13 1,10 @@
import Lean.Elab.Command
import Violet.CliContext
import Violet.Ast.Surface
import Violet.Parser
import Violet.Core.Elaboration
open Lean Meta Elab Command

namespace Violet.Core
open Violet.Ast
open Violet.Ast.Surface (Program)
open Violet Ast Surface

abbrev ElabM := StateT MetaCtx (ExceptT String IO)
abbrev ProgramM := StateT ElabContext (StateT MetaCtx (ExceptT String IO))


@@ 88,7 85,6 @@ partial def repl : ProgramM Unit := do
    repl
  | .error ε => throw ε


def Program.checkAux (p : Program) (src : System.FilePath)
  : CmdM (ElabContext × MetaCtx) := do
  let opts := (← read).options

M Violet/Core/Elaboration.lean => Violet/Core/Elaboration.lean +5 -6
@@ 4,8 4,7 @@ import Violet.Ast.Surface

namespace Violet.Core
open Lean
open Violet.Ast
open Violet.Ast.Core
open Violet.Ast Core

def addPos [Monad m] [MonadExcept String m]
  (s e : Position) (f : m α) : m α := do


@@ 80,7 79,7 @@ def ElabContext.infer [Monad m] [MonadState MetaCtx m] [MonadExcept String m]
    return (.pi x mode a' b', .type)
  -- infer `(x : a) × b`
  | .sigma x a b =>
    let a' ← ctx.check a .type 
    let a' ← ctx.check a .type
    let b' ← (ctx.bind x (← ctx.env.eval a')).check b .type
    return (.sigma x a' b', .type)
  | .let x a t u =>


@@ 100,7 99,7 @@ def ElabContext.infer [Monad m] [MonadState MetaCtx m] [MonadExcept String m]
    let (snd', sndTy) ← ctx.infer snd
    let sndTy := Closure.mk ctx.env (← quote ctx.lvl sndTy)
    return (.pair fst' snd', .sigma "_" fstTy sndTy)
  | .proj raw idx p => 
  | .proj raw idx p =>
    let (p', pTy) ← ctx.infer p
    match ← force pTy with
    | .sigma _ a b =>


@@ 130,7 129,7 @@ def ElabContext.check [Monad m] [MonadState MetaCtx m] [MonadExcept String m]
  match tm, ← force ty with
  | .src startPos endPos tm, ty => addPos startPos endPos (check ctx tm ty)
  -- if lambda has same mode as pi type, then just check it
  | .lam m@.implicit x t, .pi _ .implicit a b 
  | .lam m@.implicit x t, .pi _ .implicit a b
  | .lam m@.explicit x t, .pi _ .explicit a b  =>
    let t ← (ctx.bind x a).check t (← b.apply (vvar x ctx.lvl))
    return .lam x m t


@@ 144,7 143,7 @@ def ElabContext.check [Monad m] [MonadState MetaCtx m] [MonadExcept String m]
    let snd' ← ctx.check snd (← b.apply <| ← ctx.env.eval fst')
    return .pair fst' snd'
  | .let x a t u, a' =>
    let a ← ctx.check a .type 
    let a ← ctx.check a .type
    let va ← ctx.env.eval a
    let t ← ctx.check t va
    let vt ← ctx.env.eval t

M Violet/Core/Value.lean => Violet/Core/Value.lean +1 -2
@@ 2,8 2,7 @@ import Lean.Data.HashMap
import Violet.Ast.Core

namespace Violet.Core
open Violet.Ast.Core
open Violet.Ast
open Violet.Ast Core

mutual


M Violet/Parser.lean => Violet/Parser.lean +2 -4
@@ 4,10 4,8 @@ import Lean.Data.Position
import Violet.Ast.Surface

namespace Violet.Parser
open Lean
open Lean.Parsec
open Violet.Ast
open Violet.Ast.Surface
open Lean Parsec
open Violet Ast Surface

def whitespace : Parsec Unit := do
  repeat do