lsf.flx

macro val testing = true;

/////////////////////////////////////////////////////////////////////////////////////
// A CRUDE LEXER

chip lex (s:string) 
  connector io
    pin out: %>string
{
  var n = s.len.int;
  variant state_t = Skip | Grab;
  var token = "";
  proc emit() { 
    if token != "" perform write (io.out,token);
    token = "";
    state = Skip;
  }

  var state = Skip;
  nextch: for ch in s do
    match state with
    | Skip =>
      if ch in "()." do
        write (io.out,string ch);
      elif ch > char ' '  do
        token += ch;
        state = Grab; 
      done
    | Grab =>
      if ch in "()." do
        emit;
        write (io.out,string ch);
      elif ch <= char ' ' do
        emit;
      else
       token += ch;
      done
    endmatch;
  done
  emit;
  write (io.out, "End");
}

if testing do
  var testlsf = 
    "lam x. lam y. S F (lam z. F a z) x"
  ; 

  proc testlex(s:string) {
    proc printstring (s:string) { println$ "Lexeme= " + s; }
    #(lex s |-> procedure printstring);
  }

  testlex(testlsf);
done

/////////////////////////////////////////////////////////////////////////////////////
// TOKEN DEFINITION

variant token_t = 
  | TVar of string
  | TokS
  | TokF
  | Left
  | Right
  | TLam
  | Dot
  | TEnd
;

instance Str[token_t] {
  fun str: token_t -> string = 
  | TVar s => s
  | TokS => "S"
  | TokF => "F"
  | Left => "("
  | Right => ")"
  | TLam => "Lam" 
  | Dot => "."
  | TEnd => "End"
  ;
}

  
/////////////////////////////////////////////////////////////////////////////////////
// TOKENISER

chip tokeniser 
  connector io
   pin inp: %<string
   pin out: %>token_t
{
  while true do
    var x = read io.inp;
    write (io.out, 
      match x with
      | "(" => Left
      | ")" => Right
      | "S" => TokS
      | "F" => TokF
      | "." => Dot
      | "lam" => TLam
      | "End" => TEnd
      | _ => TVar x
      endmatch
    );
  done
}

if testing do
  proc testtok (s:string) {
    var counter = 0;
    proc printtok (t:token_t) { ++counter; println$ "Token #" + counter.str + "=" + t.str; }
    #(lex s |-> tokeniser |-> procedure printtok);
  }

  testtok (testlsf);
done


/////////////////////////////////////////////////////////////////////////////////////
// TERM DEFINITION

variant term_t = 
  | Var of string
  | Lam of string * term_t
  | Node of term_t * term_t
  | S 
  | F 
  | Error of string
;

instance Str[term_t] {
  fun str: term_t -> string =
  | Var s => s 
  | Lam (s,t) => "{lam " + s + "." + t.str+"}"
  | Node (t1, t2) => "(" + t1.str + " " +t2.str + ")"
  | S => "\\S"
  | F => "\\F"
  | Error s => "ERROR " + s
  ;
}

// We can write N M in Felix code to mean Node (N,M)
// but only in expressions, not in patterns unfortunately
fun apply (l:term_t,r:term_t) => Node (l,r);

/////////////////////////////////////////////////////////////////////////////////////
// PARSER
//
// term = |  var | lam var . term | term term | S  | F | ( term )
// constraint: lam must be preceded by either .  or ( or be the first symbol

chip lsfparser
  connector io
    pin inp: %<token_t
    pin out: %>term_t
{
  var counter = 0;
  var tok : token_t;
  proc fetch () { tok = read io.inp; ++counter; }
  
  proc fail () {
    write (io.out, Error ("Syntax Error on token #" + counter.str +  "=" + tok.str + "\nStack=" + stack.str));
    goto terminate;
  }

  variant elt_t = 
    | Tok of token_t
    | Term of term_t
  ;
  instance Str[elt_t] {
    fun str : elt_t -> string =
    | Tok t => "Tok " + t.str
    | Term t => "Term " + t.str
    ;
  }
  var stack = Empty[elt_t];
  proc push () { stack = Tok tok ! stack; }
  proc maybe_node () { 
    match stack with
    | Term a ! Term b ! tail => stack = Term (Node (b,a)) ! tail;
    | _ => ; 
    endmatch;
  }

  while true do
    maybe_node;
    fetch();
    match tok with
    | TEnd =>
reduce_lam1:>
      match stack with
      | ([Term term]) => write (io.out, term);

      | Term term ! Tok Dot ! Tok (TVar v) ! Tok TLam ! tail =>
        stack = Term (Lam (v,term)) ! tail;
        maybe_node;
        goto reduce_lam1;

      | Empty => write (io.out, Error "No input");
      | _ => fail;
      endmatch;

    | Left =>
      push;

    | Right =>
reduce_lam2:>
      match stack with
      | Term t ! Tok Left ! tail => stack = Term t ! tail;

      | Term term ! Tok Dot ! Tok (TVar v) ! Tok TLam ! tail =>
        stack = Term (Lam (v,term)) ! tail;
        maybe_node;
        goto reduce_lam2;

      | _ => fail;
      endmatch;

    | TokS =>
      match stack with
      | Term t ! tail => stack =  Term (Node (t, S)) ! tail;
      | _ => stack = Term S ! stack;
      endmatch;

    | TokF =>
      match stack with
      | Term t ! tail => stack = Term (Node (t, F)) ! tail;
      | _ => stack = Term F ! stack;
      endmatch;
   
    | TLam =>
      match stack with
      | (Empty | ((Tok Dot | Tok Left) ! _)) =>  push;
      | _ => fail;
      endmatch;

    | TVar v =>
      match stack with
      | Tok TLam ! _ => push; 
      | Term t ! tail => stack = Term (Node (t, Var v)) ! tail;
      | _ => stack = Term (Var v) ! stack;
      endmatch; 

    | Dot =>
      match stack with
      | Tok (TVar v) ! Tok TLam ! tail => push;
      | _ => fail;
      endmatch;

    endmatch;
  done 

terminate:> ;    

}

if testing do
  proc testlsfparser (s:string) {
    proc printterm (t:term_t) { println$ "Term=" + t.str; }
    #(lex s |-> tokeniser |-> lsfparser |-> procedure printterm);
  }

  var testexpr = "lam x. lam y. S F (lam z. F a z) x";
  testlsfparser(testexpr);
done

fun lsfparse (s:string) : term_t = {
  var t: term_t;
  proc saveterm (x:term_t) { t = x; }
  run (lex s |-> tokeniser |-> lsfparser |-> procedure saveterm);
  return t;
}

if testing do
  println$ "Parsed again = " + (lsfparse testexpr).str;
done

/////////////////////////////////////////////////////////////////////////////////////
// ALPHA CONVERSION

// fresh integer generator for alpha conversion
gen freshint_gen () : int = { for i in 100.. yield i; }
var freshint =  freshint_gen;

// alpha conversion
fun alpha (t:term_t) : term_t =>
  let fun aux (env:list[string * string]) (t:term_t) : term_t =>
    match t with
    | Var s' as t =>  
      match find env s' with
      | None => t
      | Some x => Var x
      endmatch

    | Lam (s', t') => 
      let r = "_" + #freshint.str in
      Lam (r, aux ((s',r) ! env) t')

    | Node (a,b) => Node (aux env a, aux env b)

    | x => x // S or F
  in aux Empty[string * string]  t
;

/////////////////////////////////////////////////////////////////////////////////////
// BETA REDUCTION
fun beta (s: string, bdy: term_t, r: term_t) : term_t =>
  let b = alpha bdy in
  let fun aux (t:term_t) =>
    match t with
    | Var v when v == s => r
    | Lam (s,t) => Lam (s, aux t)
    | Node (a,b) => Node (aux a, aux b) 
    | x => x
    endmatch
  in aux b
;

if testing do
  proc checkbeta (s:string, b: term_t, r: term_t) {
    var a = Node (Lam (s,b),r);
    println$ "To reduce = " + a.str;
    println$ "Reduced = " + (beta (s,b,r)).str;
  }

  var testexpr2 = "x y";
  var testexpr3 = "z";
  checkbeta ("x", lsfparse testexpr2, lsfparse testexpr3);
done

/////////////////////////////////////////////////////////////////////////////////////
// DEFINE ACTIVE VARIABLE
fun active: term_t -> opt[string] =
  | Var x => Some x
  | S => None[string]
  | F => None[string]
  | Lam (s,t) =>
    match active t with // active t - {s}
    | Some s' as a => if s == s' then None[string] else a
    | None => None[string]
    endmatch
  | Node ((S|F),m) => None[string]
  | Node (Node ((S|F),m),n) => None[string]
  | Node (Node(Node(S,m),n),p) => None[string]
  | Node (Node(Node(F,m),n),p) => active m
  | Node (m,n) => active m
; 

fun has_active (t:term_t): bool =>
  match active t with
  | Some _ => true
  | None => false
;

/////////////////////////////////////////////////////////////////////////////////////
// DEFINE STAR REDUCTION
// 
// Eliminates lambda terms

var K = F F;
var I = S K K; 
var abs_left = S K F;

fun star (s:string, t:term_t) => match t with
  | Var x when x == s => I
  | Var y => K (Var y)
  | (S|F) as O => K O
  | Lam (y,m) => Lam (s, star (y,m))
  | Node (m,n) => S (Lam(s,m)) (Lam(s,n))
;

if testing do
  var teststar = "lam x. lam y. y";
  println$ lsfparse teststar;
  println$ star("x",lsfparse "lam y.y");
done

/////////////////////////////////////////////////////////////////////////////////////
// DEFINE LEFT AND RIGHT COMPONENTS
fun left : term_t -> term_t =
  | Node (m,n) => m
  | _ => S K F
;

fun right : term_t -> term_t =
  | Node (m,n) => n
  | Lam (s,t) => star (s,t)
  | m => m
;

fun split (t:term_t) : term_t => t.left t.right;

/////////////////////////////////////////////////////////////////////////////////////
// DEFINE NORMAL FORM

fun normal: term_t -> bool =
 | (S|F|Var _) => true
 | Lam (_,t) => normal t
 | Node (m,n) as t =>
   normal m and normal n and (compound t or has_active t)
;

/////////////////////////////////////////////////////////////////////////////////////
// DEFINE COMPOUND
fun compound : term_t -> bool =
 | (S|F) => false
 | _ => true
;


/////////////////////////////////////////////////////////////////////////////////////
// REDUCTION

fun sfreduce: term_t -> term_t =
  | Node (f,x) => 
    match f,x with
    | Lam (s,f), x => beta (s,f,x)
    | S,Node (m,Node (n,p)) => (m n) (n p)
    | F,Node(Node (p,m),n) =>
      match p with
      | (S|F) => m
      | _ => n p.split
      endmatch
    endmatch
  | x => x
;