L1.sml

(* 2002-11-08 -- Time-stamp: <2006-10-25 09:22:33 pes20>    -*-SML-*- *)
(* Peter Sewell                                                       *)

(* This file contains an interpreter, pretty-printer and type-checker
   for the language L1.  To make it go, copy it into a working
   directory, ensure Moscow ML is available, and type

       mosml -P full l1.ml 

   That will give you a MoscowML top level in which these definitions
   are present.  You can then type
      
      doit ();

   to show the reduction sequence of < l1:=3;!l1 , {l1=0 } >, and

      doit2 ();

   to run the type-checker on the same simple example; you can try
   other examples analogously.  This file doesn't have a parser for
   l1, so you'll have to enter the abstract syntax directly, eg

      prettyreduce (Seq( Assign ("l1",Integer 3), Deref "l1"), [("l1",0)]);

   This has been tested with Moscow ML version 2.00 (June 2000), but
   should work with any other implementation of Standard ML.   *)


(* *********************)
(* the abstract syntax *)
(* *********************)

type loc = string

datatype oper = Plus | GTEQ

datatype expr = 
         Integer of int
       | Boolean of bool
       | Op of expr * oper * expr
       | If of expr * expr * expr
       | Assign of loc * expr
       | Deref of loc
       | Skip
       | Seq of expr * expr
       | While of expr * expr


(* **********************************)
(* an interpreter for the semantics *)
(* **********************************)

fun is_value (Integer n) = true
  | is_value (Boolean b) = true
  | is_value (Skip) = true
  | is_value _ = false

  (* In the semantics, a store is a finite partial function from
  locations to integers.  In the implementation, we represent a store
  as a list of loc*int pairs containing, for each l in the domain of
  the store, exactly one element of the form (l,n).  The operations

    lookup : store * loc         -> int option
    update : store * (loc * int) -> store option

  both return NONE if given a location that is not in the domain of
  the store.  This is not a very efficient implementation, but it is
  simple. *)

type store = (loc * int) list

fun lookup ( [], l ) = NONE
  | lookup ( (l',n')::pairs, l) = 
    if l=l' then SOME n' else lookup (pairs,l)

fun update'  front [] (l,n) = NONE
 |  update'  front ((l',n')::pairs) (l,n) = 
    if l=l' then 
        SOME(front @ ((l,n)::pairs) )
    else 
        update' ((l',n')::front) pairs (l,n)

fun update (s, (l,n)) = update' [] s (l,n)


  (* now define the single-step function

     reduce :  expr * store -> (expr * store) option 

  which takes a configuration (e,s) and returns either NONE, if it has
  no transitions, or SOME (e',s'), if it has a transition (e,s) -->
  (e',s'). 

  Note that the code depends on global properties of the semantics,
  including the fact that it defines a deterministic transition
  system, so the comments indicating that particular lines of code
  implement particular semantic rules are not the whole story.  *)

fun reduce (Integer n,s) = NONE
  | reduce (Boolean b,s) = NONE
  | reduce (Op (e1,opr,e2),s) = 
    (case (e1,opr,e2) of
         (Integer n1, Plus, Integer n2) => SOME(Integer (n1+n2), s)   (*op + *)
       | (Integer n1, GTEQ, Integer n2) => SOME(Boolean (n1 >= n2), s)(*op >=*)
       | (e1,opr,e2) => (                                               
         if (is_value e1) then (                                        
             case reduce (e2,s) of 
                 SOME (e2',s') => SOME (Op(e1,opr,e2'),s')     (* (op2) *)
               | NONE => NONE )                           
         else (                                                 
             case reduce (e1,s) of 
                 SOME (e1',s') => SOME(Op(e1',opr,e2),s')      (* (op1) *)
               | NONE => NONE ) ) )
  | reduce (If (e1,e2,e3),s) =
    (case e1 of
         Boolean(true) => SOME(e2,s)                           (* (if1) *)
       | Boolean(false) => SOME(e3,s)                          (* (if2) *)
       | _ => (case reduce (e1,s) of
                   SOME(e1',s') => SOME(If(e1',e2,e3),s')      (* (if3) *)
                 | NONE => NONE ))
  | reduce (Deref l,s) = 
    (case lookup  (s,l) of                
          SOME n => SOME(Integer n,s)                          (* (deref) *)
        | NONE => NONE )                  
  | reduce (Assign (l,e),s) =                                  
    (case e of                                                 
         Integer n => (case update (s,(l,n)) of 
                           SOME s' => SOME(Skip, s')           (* (assign1) *)
                         | NONE => NONE)                                   
       | _ => (case reduce (e,s) of                           
                   SOME (e',s') => SOME(Assign (l,e'), s')     (* (assign2) *)
                 | NONE => NONE  ) )                          
  | reduce (While (e1,e2),s) = SOME( If(e1,Seq(e2,While(e1,e2)),Skip),s) (* (while) *)
  | reduce (Skip,s) = NONE                                     
  | reduce (Seq (e1,e2),s) =                                   
    (case e1 of                                                 
        Skip => SOME(e2,s)                                     (* (seq1) *)
      | _ => ( case reduce (e1,s) of                           
                 SOME (e1',s') => SOME(Seq (e1',e2), s')       (* (seq2) *)
               | NONE => NONE ) )                                        


  (* now define the many-step evaluation function

     evaluate :  expr * store -> (expr * store) option 

  which takes a configuration (e,s) and returns the unique (e',s')
  such that   (e,s) -->* (e',s') -/->.  *)

fun evaluate (e,s) = case reduce (e,s) of 
                         NONE => (e,s)
                       | SOME (e',s') => evaluate (e',s')


(* **********************************)
(* typing                           *)
(* **********************************)

(* types *)

datatype type_L1 =
         int
       | unit
       | bool

datatype type_loc =
         intref

type typeEnv = (loc*type_loc) list 

(* in the semantics, type environments gamma are partial functions
from locations to the singleton set {intref}. Here, just as we did for
stores, we represent them as a list of loc*type_loc pairs containing,
for each l in the domain of the type environment, exactly one element
of the form (l,intref).  *)


(* ****************)
(* type inference *)
(* ****************)

(* infertype : typeEnv -> expr -> type_L1 option *)

(* again, we depend on a uniqueness property, without which we would
have to have infertype return a type_L1 list of all the possible types *)

fun infertype gamma (Integer n) = SOME int
  | infertype gamma (Boolean b) = SOME bool
  | infertype gamma (Op (e1,opr,e2)) 
    = (case (infertype gamma e1, opr, infertype gamma e2) of
          (SOME int, Plus, SOME int) => SOME int
        | (SOME int, GTEQ, SOME int) => SOME bool
        | _ => NONE)
  | infertype gamma (If (e1,e2,e3)) 
    = (case (infertype gamma e1, infertype gamma e2, infertype gamma e3) of
           (SOME bool, SOME t2, SOME t3) => 
           (if t2=t3 then SOME t2 else NONE)
         | _ => NONE)
  | infertype gamma (Deref l) 
    = (case lookup (gamma,l) of
           SOME intref => SOME int
         | NONE => NONE)
  | infertype gamma (Assign (l,e)) 
    = (case (lookup (gamma,l), infertype gamma e) of
           (SOME intref,SOME int) => SOME unit
         | _ => NONE)
  | infertype gamma (Skip) = SOME unit
  | infertype gamma (Seq (e1,e2))  
    = (case (infertype gamma e1, infertype gamma e2) of
           (SOME unit, SOME t2) => SOME t2
         | _ => NONE )
  | infertype gamma (While (e1,e2)) 
    = (case (infertype gamma e1, infertype gamma e2) of
           (SOME bool, SOME unit) => SOME unit 
         | _ => NONE )



(* ****************** *)
(* testing machinery  *)
(* ****************** *)
;
load "Listsort";
load "Int";
load "Bool";

(* pretty print expressions *)

fun prettyprintop Plus = "+"
  | prettyprintop GTEQ = ">="
                         
fun prettyprintexpr (Integer n) = Int.toString n
  | prettyprintexpr (Boolean b) = Bool.toString b
  | prettyprintexpr (Op (e1,opr,e2)) 
    = "(" ^ (prettyprintexpr e1) ^ (prettyprintop opr) 
      ^ (prettyprintexpr e2) ^ ")"
  | prettyprintexpr (If (e1,e2,e3)) 
    = "if " ^ (prettyprintexpr e1 ) ^ " then " ^ (prettyprintexpr e2)
      ^ " else " ^ (prettyprintexpr e3)
  | prettyprintexpr (Deref l) = "!" ^ l
  | prettyprintexpr (Assign (l,e)) =  l ^ ":=" ^ (prettyprintexpr e )
  | prettyprintexpr (Skip) = "skip"
  | prettyprintexpr (Seq (e1,e2)) =  (prettyprintexpr e1 ) ^ ";" 
                                     ^ (prettyprintexpr e2)
  | prettyprintexpr (While (e1,e2)) =  "while " ^ (prettyprintexpr e1 ) 
                                       ^ " do " ^ (prettyprintexpr e2)

(* pretty print stores, first sorting by location names for readability *)

fun rawprintstore [] = ""
  | rawprintstore ((l,n)::pairs) = l ^ "=" ^ (Int.toString n) 
                                   ^ " " ^ (rawprintstore pairs)

fun prettyprintstore pairs = 
    let val pairs' = Listsort.sort 
                         (fn ((l,n),(l',n')) => String.compare (l,l'))
                         pairs
    in
        "{" ^ rawprintstore pairs' ^ "}" end

(* pretty print configurations *)

fun prettyprintconfig (e,s) = "< " ^ (prettyprintexpr e) 
                             ^ " , " ^ (prettyprintstore s) ^ " >"

(* do a reduction sequence, printing the initial state and the state
   after each reduction step *)

fun prettyreduce' (e,s) = 
    case reduce (e,s) of 
        SOME (e',s') => 
        ( TextIO.print ("\n -->  " ^ prettyprintconfig (e',s') ) ;
          prettyreduce' (e',s'))
      | NONE => (TextIO.print "\n -/->  " ; 
                 if is_value e then 
                     TextIO.print "(a value)\n" 
                 else 
                     TextIO.print "(stuck - not a value)" )

fun prettyreduce (e,s) = (TextIO.print ("      "^(prettyprintconfig (e,s))) ;
                          prettyreduce' (e,s))

(* **************)
(* simple tests *)
(* **************)

fun doit () = prettyreduce (Seq( Assign ("l1",Integer 3), Deref "l1"), [("l1",0)] )
(*
 infertype [("l1",intref)] (Seq( Assign ("l1",Integer 3), Deref "l1"));;
*)
fun doit2 () = infertype [("l1",intref)] (Seq( Assign ("l1",Integer 3), Deref "l1"));