mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Add support for Reason (#3336)
This commit is contained in:
Darin Morrison
committed by
Brandon Black
Brandon Black
parent
a4d12cc8e4
commit
7867b946b9
344
samples/Reason/Machine.re
Normal file
344
samples/Reason/Machine.re
Normal file
@@ -0,0 +1,344 @@
|
||||
open Format;
|
||||
|
||||
let module Endo = {
|
||||
type t 'a = 'a => 'a;
|
||||
};
|
||||
|
||||
let module Syntax = {
|
||||
let module Var = {
|
||||
type t = int;
|
||||
};
|
||||
let module Term = {
|
||||
type t =
|
||||
| App t t
|
||||
| Lam t
|
||||
| Var Var.t
|
||||
;
|
||||
};
|
||||
let module Sub = {
|
||||
type t 'a =
|
||||
| Cmp (t 'a) (t 'a)
|
||||
| Dot 'a (t 'a)
|
||||
| Id
|
||||
| Shift
|
||||
;
|
||||
|
||||
let map f sgm => {
|
||||
let rec go = fun
|
||||
| Cmp sgm0 sgm1 => Cmp (go sgm0) (go sgm1)
|
||||
| Dot a sgm => Dot (f a) (go sgm)
|
||||
| Id => Id
|
||||
| Shift => Shift
|
||||
;
|
||||
go sgm;
|
||||
};
|
||||
|
||||
let rec apply sgm e =>
|
||||
switch (sgm, e) {
|
||||
| (sgm, Term.App e0 e1) => Term.App (apply sgm e0) (apply sgm e1)
|
||||
| (sgm, Term.Lam e) => Term.Lam (apply (Dot (Term.Var 0) (Cmp sgm Shift)) e)
|
||||
| (Dot e _, Term.Var 0) => e
|
||||
| (Dot _ sgm, Term.Var i) => apply sgm (Term.Var (i - 1))
|
||||
| (Id, Term.Var i) => Term.Var i
|
||||
| (Shift, Term.Var i) => Term.Var (i + 1)
|
||||
| (Cmp rho sgm, e) => apply sgm (apply rho e)
|
||||
};
|
||||
};
|
||||
};
|
||||
|
||||
let module Zip = {
|
||||
open Syntax;
|
||||
type t 'a =
|
||||
| App0 (t 'a) 'a
|
||||
| App1 'a (t 'a)
|
||||
| Halt
|
||||
| Lam (t 'a)
|
||||
;
|
||||
|
||||
let map f sgm => {
|
||||
let rec go = fun
|
||||
| App0 zip e1 => App0 (go zip) (f e1)
|
||||
| App1 e0 zip => App1 (f e0) (go zip)
|
||||
| Halt => Halt
|
||||
| Lam zip => Lam (go zip)
|
||||
;
|
||||
go sgm;
|
||||
};
|
||||
|
||||
let rec apply zip acc => switch zip {
|
||||
| App0 zip e1 => apply zip (Term.App acc e1)
|
||||
| App1 e0 zip => apply zip (Term.App e0 acc)
|
||||
| Halt => acc
|
||||
| Lam zip => apply zip (Term.Lam acc)
|
||||
};
|
||||
};
|
||||
|
||||
let module Clo = {
|
||||
open Syntax;
|
||||
type t =
|
||||
| Clo Term.t (Sub.t t);
|
||||
let rec from (Clo term sgm) => Sub.apply (Sub.map from sgm) term;
|
||||
};
|
||||
|
||||
let module Pretty = {
|
||||
let module Delim = {
|
||||
type t = string;
|
||||
let pp prev next fmt token => if (prev < next) { fprintf fmt "%s" token };
|
||||
};
|
||||
let module Prec = {
|
||||
type t = int;
|
||||
open Syntax.Term;
|
||||
let calc = fun
|
||||
| App _ _ => 1
|
||||
| Lam _ => 2
|
||||
| Var _ => 0
|
||||
;
|
||||
};
|
||||
let module Name = {
|
||||
type t = string;
|
||||
|
||||
let suffix = {
|
||||
let script = fun
|
||||
| 0 => "₀"
|
||||
| 1 => "₁"
|
||||
| 2 => "₂"
|
||||
| 3 => "₃"
|
||||
| 4 => "₄"
|
||||
| 5 => "₅"
|
||||
| 6 => "₆"
|
||||
| 7 => "₇"
|
||||
| 8 => "₈"
|
||||
| 9 => "₉"
|
||||
| _ => failwith "bad subscript";
|
||||
let rec go acc => fun
|
||||
| 0 => acc
|
||||
| n => go (script (n mod 10) ^ acc) (n / 10);
|
||||
go ""
|
||||
};
|
||||
|
||||
let gen = {
|
||||
let offset = 97;
|
||||
let width = 26;
|
||||
fun () i => {
|
||||
let code = i mod width + offset;
|
||||
let char = Char.chr code;
|
||||
let prime = i / width;
|
||||
let suffix = suffix prime;
|
||||
let name = Char.escaped char ^ suffix;
|
||||
Some name;
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
let module Env = {
|
||||
type t = {
|
||||
used: list Name.t,
|
||||
rest: Stream.t Name.t,
|
||||
};
|
||||
let mk () => {
|
||||
let used = [];
|
||||
let rest = Stream.from @@ Name.gen ();
|
||||
{ used, rest };
|
||||
};
|
||||
};
|
||||
|
||||
type printer 'a = Env.t => Prec.t => formatter => 'a => unit;
|
||||
|
||||
let module Term = {
|
||||
open Syntax.Term;
|
||||
let rec pp ({ Env.used: used, rest } as env) prev fmt e => {
|
||||
let next = Prec.calc e;
|
||||
switch e {
|
||||
| App e0 e1 =>
|
||||
fprintf fmt "@[%a%a@ %a%a@]"
|
||||
(Delim.pp prev next) "("
|
||||
(pp env 1) e0
|
||||
(pp env 0) e1
|
||||
(Delim.pp prev next) ")"
|
||||
| Lam e =>
|
||||
let name = Stream.next rest;
|
||||
let env = { ...env, Env.used: [name, ...used] };
|
||||
fprintf fmt "%aλ%a.%a%a"
|
||||
(Delim.pp prev next) "("
|
||||
(pp_print_string) name
|
||||
(pp env next) e
|
||||
(Delim.pp prev next) ")"
|
||||
| Var index =>
|
||||
fprintf fmt "%s" @@ try (List.nth used index) {
|
||||
| _ => "#" ^ string_of_int index
|
||||
}
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
let module Sub = {
|
||||
open Syntax.Sub;
|
||||
let rec pp pp_elem env prev fmt => fun
|
||||
| Cmp sgm1 sgm0 =>
|
||||
fprintf fmt "@[%a;@ %a@]"
|
||||
(pp pp_elem env prev) sgm1
|
||||
(pp pp_elem env prev) sgm0
|
||||
| Dot e sgm =>
|
||||
fprintf fmt "@[%a@ ·@ %a@]"
|
||||
(pp_elem env prev) e
|
||||
(pp pp_elem env prev) sgm
|
||||
| Id =>
|
||||
fprintf fmt "ι"
|
||||
| Shift =>
|
||||
fprintf fmt "↑"
|
||||
;
|
||||
};
|
||||
|
||||
let module Clo = {
|
||||
let rec pp env prev fmt (Clo.Clo e sgm) => {
|
||||
let next = Prec.calc e;
|
||||
fprintf fmt "@[%a%a%a[%a]@]"
|
||||
(Delim.pp prev next) "("
|
||||
(Term.pp env next) e
|
||||
(Delim.pp prev next) ")"
|
||||
(Sub.pp pp env next) sgm
|
||||
};
|
||||
};
|
||||
|
||||
let module Zip = {
|
||||
open Zip;
|
||||
let rec pp pp_elem env prev fmt => fun
|
||||
| App0 zip elem =>
|
||||
fprintf fmt "inl@[<v -1>⟨@,%a@,%a⟩@]"
|
||||
(pp pp_elem env prev) zip
|
||||
(pp_elem env prev) elem
|
||||
| App1 elem zip =>
|
||||
fprintf fmt "inr@[<v -1>⟨@,%a@,%a⟩@]"
|
||||
(pp_elem env prev) elem
|
||||
(pp pp_elem env prev) zip
|
||||
| Halt =>
|
||||
fprintf fmt "halt"
|
||||
| Lam zip =>
|
||||
fprintf fmt "lam@[<v -1>⟨@,%a⟩@]"
|
||||
(pp pp_elem env prev) zip
|
||||
;
|
||||
};
|
||||
};
|
||||
|
||||
let module Machine = {
|
||||
type t = {
|
||||
clo: Clo.t,
|
||||
ctx: Zip.t Clo.t,
|
||||
};
|
||||
|
||||
let into e => {
|
||||
open Clo;
|
||||
open Syntax.Sub;
|
||||
let clo = Clo e Id;
|
||||
let ctx = Zip.Halt;
|
||||
{ clo, ctx }
|
||||
};
|
||||
|
||||
let from { clo, ctx } => Zip.apply (Zip.map Clo.from ctx) (Clo.from clo);
|
||||
|
||||
let pp fmt rule state => {
|
||||
fprintf fmt "@[<v>ctx ::@[<v -5>@,%a@]@,clo ::@[<v -5>@,%a@]@,rule ::@[<v -5>@,%a@]@,term ::@[<v -5>@,%a@]@]@."
|
||||
(Pretty.Zip.pp Pretty.Clo.pp (Pretty.Env.mk ()) 2) state.ctx
|
||||
(Pretty.Clo.pp (Pretty.Env.mk ()) 2) state.clo
|
||||
(pp_print_string) rule
|
||||
(Pretty.Term.pp (Pretty.Env.mk ()) 2) (from state)
|
||||
};
|
||||
|
||||
let halted state => {
|
||||
open Clo;
|
||||
open Syntax.Sub;
|
||||
open Syntax.Term;
|
||||
switch state {
|
||||
| { clo: Clo (Var _) Id, _ } => true
|
||||
| _ => false
|
||||
} [@warning "-4"];
|
||||
};
|
||||
|
||||
let step state => {
|
||||
open Clo;
|
||||
open Syntax.Sub;
|
||||
open Syntax.Term;
|
||||
let rule = ref "";
|
||||
let state = switch state {
|
||||
/* left */
|
||||
| { clo: Clo (App e0 e1) sgm, ctx } =>
|
||||
let clo = Clo e0 sgm;
|
||||
let ctx = Zip.App0 ctx (Clo e1 sgm);
|
||||
rule := "LEFT";
|
||||
{ clo, ctx };
|
||||
/* beta */
|
||||
| { clo: Clo (Lam e) sgm, ctx: Zip.App0 ctx c0 } =>
|
||||
let clo = Clo e (Cmp (Dot c0 sgm) Id);
|
||||
rule := "BETA";
|
||||
{ clo, ctx };
|
||||
/* lambda */
|
||||
| { clo: Clo (Lam e) sgm, ctx } =>
|
||||
let clo = Clo e (Cmp (Dot (Clo (Var 0) Id) (Cmp sgm Shift)) Id);
|
||||
let ctx = Zip.Lam ctx;
|
||||
rule := "LAMBDA";
|
||||
{ clo, ctx };
|
||||
/* associate */
|
||||
| { clo: Clo (Var n) (Cmp (Cmp pi rho) sgm), ctx } =>
|
||||
let clo = Clo (Var n) (Cmp pi (Cmp rho sgm));
|
||||
rule := "ASSOCIATE";
|
||||
{ clo, ctx };
|
||||
/* head */
|
||||
| { clo: Clo (Var 0) (Cmp (Dot (Clo e pi) _) sgm), ctx } =>
|
||||
let clo = Clo e (Cmp pi sgm);
|
||||
rule := "HEAD";
|
||||
{ clo, ctx };
|
||||
/* tail */
|
||||
| { clo: Clo (Var n) (Cmp (Dot (Clo _ _) rho) sgm), ctx } =>
|
||||
let clo = Clo (Var (n - 1)) (Cmp rho sgm);
|
||||
rule := "TAIL";
|
||||
{ clo, ctx };
|
||||
/* shift */
|
||||
| { clo: Clo (Var n) (Cmp Shift sgm), ctx } =>
|
||||
let clo = Clo (Var (n + 1)) sgm;
|
||||
rule := "SHIFT";
|
||||
{ clo, ctx };
|
||||
/* id */
|
||||
| { clo: Clo (Var n) (Cmp Id sgm), ctx } =>
|
||||
let clo = Clo (Var n) sgm;
|
||||
rule := "ID";
|
||||
{ clo, ctx };
|
||||
| _ =>
|
||||
pp std_formatter !rule state;
|
||||
failwith "bad state";
|
||||
} [@warning "-4"];
|
||||
pp std_formatter !rule state;
|
||||
state;
|
||||
};
|
||||
|
||||
let norm e => {
|
||||
let count = ref 0;
|
||||
let state = ref (into e);
|
||||
while (not (halted !state)) {
|
||||
fprintf std_formatter "@\n--- step[%d] ---@\n" !count;
|
||||
incr count;
|
||||
state := step !state;
|
||||
};
|
||||
from !state;
|
||||
};
|
||||
};
|
||||
|
||||
let module Test = {
|
||||
open Syntax.Term;
|
||||
let l e => Lam e;
|
||||
let ( *@ ) e0 e1 => App e0 e1;
|
||||
let ff = l (l (Var 1));
|
||||
let tt = l (l (Var 0));
|
||||
let zero = l (l (Var 1));
|
||||
let succ = l (l (l (Var 0 *@ Var 2)));
|
||||
let one = succ *@ zero;
|
||||
let two = succ *@ one;
|
||||
let three = succ *@ two;
|
||||
let const = l (l (Var 1));
|
||||
let fix = l (l (Var 1 *@ (Var 0 *@ Var 0)) *@ l (Var 1 *@ (Var 0 *@ Var 0)));
|
||||
let add = fix *@ l (l (l (Var 1 *@ Var 0 *@ l (succ *@ Var 3 *@ Var 0 *@ Var 1))));
|
||||
let init = l (l (Var 0) *@ l (l (Var 1)));
|
||||
};
|
||||
|
||||
let module Run = {
|
||||
let go () => Machine.norm Test.init;
|
||||
};
|
||||
Reference in New Issue
Block a user