search

KiJeong-Lim / portfolio

My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.
14 stars 0 forks source link

Aladdin Proposals #4

Open KiJeong-Lim opened 3 years ago

KiJeong-Lim commented 3 years ago
  1. Introduce module system.
  2. Introduce Haskell's feature (data rather than kind, type synonym, type class).
  3. Make error messages pretty.
  4. Allow D ::= D /\ D.
  5. Allow user-defined operators.
  6. Introduce constraint handling rules (CHR) like Elpi.
KiJeong-Lim commented 3 years ago

  1. CHR: <Goal> ::= <Var> "with" <Goal> G with P successes iff X is a logic variable. if X with P successes then yields constraint P for X.

  2. Meta Aladdin:

    
module TC.

from Std import Aladdin.MetaAladdin as MA.

data ty : * where all : (ty -> ty) -> ty. arr : ty -> ty -> ty.

data tm : * where abs : (tm -> tm) -> tm. app : tm -> tm -> tm. let : tm -> (tm -> tm) -> tm.

check (let Rhs Body) Tau :- MA.runMeta (MA.mkNewVar (Sigma0\ MA.solve (check Rhs Sigma0) (Res Sigma0))), -- Res := Sigma0\ sigma (Alpha_1\ ... sigma (Alpha_n\ Sigma = Gen Alpha_1 ... Alphan)) for some skeleton Gen generalize (Res ) Scheme, -- Scheme := all (Alpha_1\ ... all (Alpha_n\ Gen Alpha_1 ... Alpha_n)) pi (X\ check X Scheme => check (Body X) Tau).