Implement references and ;, close #136

src/nucleus/eval.ml

@@ -32,6 +32,10 @@ let as_handler ~loc v =
   let e = Value.as_handler ~loc v in
   Value.return e
 
+let as_ref ~loc v =
+  let e = Value.as_ref ~loc v in
+  Value.return e
+
 (** Evaluate a computation -- infer mode. *)
 let rec infer env (c',loc) =
   match c' with
@@ -121,6 +125,26 @@ let rec infer env (c',loc) =
   | Syntax.Let (xcs, c) ->
      let_bind env xcs >>= (fun env -> infer env c)
 
+  | Syntax.Ref c ->
+     infer env c >>= fun v ->
+     Value.return (Value.mk_ref v)
+
+  | Syntax.Lookup c ->
+     infer env c >>= as_ref ~loc >>= fun (r : Value.value ref) ->
+     Value.return (!r)
+
+  | Syntax.Update (c1, c2) ->
+     infer env c1 >>= as_ref ~loc >>= fun r ->
+     infer env c2 >>= fun v ->
+     r := v ;
+     Value.return_unit
+
+  | Syntax.Sequence (c1, c2) ->
+     infer env c1 >>= fun _ ->
+     (* XXX is it a good idea to ignore the value? Maybe a warning would be nice
+        when the value is not unit. *)
+     infer env c2
+
   | Syntax.Assume ((x, t), c) ->
      check_ty env t >>= fun t ->
      let _, _ , env = Value.Env.add_free ~loc env x t in
@@ -230,8 +254,8 @@ let rec infer env (c',loc) =
               Value.apply_closure env f >>= fun v ->
               fold v cs
           end
-        | Value.Ty _ | Value.Handler _ | Value.Tag _ ->
-          Error.runtime ~loc "%t expressions cannot be applied" (Value.print_value_key v)
+        | Value.Ty _ | Value.Handler _ | Value.Tag _ | Value.Ref _ ->
+          Error.runtime ~loc "cannot apply %s" (Value.name_of v)
     in
     infer env c >>= fun v -> fold v cs
 
@@ -363,7 +387,11 @@ and check env ((c',loc) as c) (((ctx_check, t_check') as t_check) : Judgement.ty
   | Syntax.Yield _
   | Syntax.Context
   | Syntax.Reduce _
-  | Syntax.Congruence _ ->
+  | Syntax.Congruence _
+  | Syntax.Ref _
+  | Syntax.Lookup _
+  | Syntax.Update _
+  | Syntax.Sequence _ ->
     (** this is the [check-infer] rule, which applies for all term formers "foo"
         that don't have a "check-foo" rule *)
 

src/nucleus/external.ml

@@ -8,7 +8,7 @@ let externals =
     ("print",
      Value.mk_closure Value.Env.empty (fun _ v ->
          Format.printf "%t@\n" (Value.print_value [] v) ;
-         Value.return (Value.from_unit ())
+         Value.return_unit
        )) ;
     ("time",
      Value.mk_closure Value.Env.empty (fun _ _ ->

src/nucleus/value.ml

@@ -24,6 +24,7 @@ type value =
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | Ref of value ref
 
 and ('a,'b) closure = dynamic -> 'a -> 'b result
 
@@ -49,6 +50,7 @@ type env = {
 let mk_term j = Term j
 let mk_ty j = Ty j
 let mk_handler h = Handler h
+let mk_ref v = Ref (ref v)
 
 let mk_closure' env f = (fun dyn v -> f {env with dynamic = dyn} v)
 let mk_closure env f = Closure (mk_closure' env f)
@@ -84,42 +86,41 @@ and print_value ?max_level xs v ppf =
   | Closure f -> print_closure xs f ppf
   | Handler h -> print_handler xs h ppf
   | Tag (t, lst) -> print_tag ?max_level xs t lst ppf
+  | Ref v -> Print.print ?max_level ~at_level:1 ppf "ref@ %t" (print_value ~max_level:0 xs (!v))
 
-let print_value_key v ppf =
+let name_of v =
   match v with
-    | Term _ -> Print.print ~at_level:0 ppf "<term>"
-    | Ty _ -> Print.print ~at_level:0 ppf "<type>"
-    | Closure _ -> Print.print ~at_level:0 ppf "<function>"
-    | Handler _ -> Print.print ~at_level:0 ppf "<handler>"
-    | Tag _ -> Print.print ~at_level:0 ppf "<tag>"
+    | Term _ -> "a term"
+    | Ty _ -> "a type"
+    | Closure _ -> "a function"
+    | Handler _ -> "a handler"
+    | Tag _ -> "a data tag"
+    | Ref _ -> "a reference"
 
 let as_term ~loc = function
   | Term e -> e
-  | Ty _ -> Error.runtime ~loc "expected a term but got a type"
-  | Closure _ -> Error.runtime ~loc "expected a term but got a function"
-  | Handler _ -> Error.runtime ~loc "expected a term but got a handler"
-  | Tag _  -> Error.runtime ~loc "expected a term but got a tag"
+  | (Ty _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_ty ~loc = function
-  | Term _ -> Error.runtime ~loc "expected a type but got a term"
   | Ty t -> t
-  | Closure _ -> Error.runtime ~loc "expected a type but got a function"
-  | Handler _ -> Error.runtime ~loc "expected a type but got a handler"
-  | Tag _  -> Error.runtime ~loc "expected a type but got a tag"
+  | (Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_closure ~loc = function
-  | Term _ -> Error.runtime ~loc "expected a function but got a term"
-  | Ty _ -> Error.runtime ~loc "expected a function but got a type"
   | Closure f -> f
-  | Handler _ -> Error.runtime ~loc "expected a function but got a handler"
-  | Tag _  -> Error.runtime ~loc "expected a function but got a tag"
+  | (Ty _ | Term _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_handler ~loc = function
-  | Term _ -> Error.runtime ~loc "expected a handler but got a term"
-  | Ty _ -> Error.runtime ~loc "expected a handler but got a type"
-  | Closure _ -> Error.runtime ~loc "expected a handler but got a function"
   | Handler h -> h
-  | Tag _  -> Error.runtime ~loc "expected a handler but got a tag"
+  | (Ty _ | Term _ | Closure _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
+
+let as_ref ~loc = function
+  | Ref v -> v
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let name_some = Name.make "Some"
 let name_none = Name.make "None"
@@ -138,22 +139,17 @@ let predefined_tags = [
 ]
 
 let as_option ~loc = function
-  | Term _ -> Error.runtime ~loc "expected an option but got a term"
-  | Ty _ -> Error.runtime ~loc "expected an option but got a type"
-  | Closure _ -> Error.runtime ~loc "expected an option but got a function"
-  | Handler h -> Error.runtime ~loc "expected an option but got a handler"
   | Tag (t,[]) when (Name.eq_ident t name_none)  -> None
   | Tag (t,[x]) when (Name.eq_ident t name_some) -> Some x
-  | Tag _ -> Error.runtime ~loc "expected an option but got a tag"
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let from_option = function
   | None -> Tag (name_none, [])
   | Some v -> Tag (name_some, [v])
 
 let from_pair (v1, v2) = Tag (name_pair, [v1; v2])
 
-let from_unit () = Tag (name_unit, [])
-
 let rec from_list = function
   | [] -> Tag (name_nil, [])
   | v :: vs -> Tag (name_cons, [v; from_list vs])
@@ -164,6 +160,8 @@ let return x = Return x
 
 let return_term e = Return (Term e)
 
+let return_unit = Return (Tag (name_unit, []))
+
 let return_ty t = Return (Ty t)
 
 let return_closure env f = Return (mk_closure env f)
@@ -235,18 +233,23 @@ let rec equal_value v1 v2 =
         in
       fold vs1 vs2
 
-    | Term _, (Ty _ | Closure _ | Handler _ | Tag _)
-    | Ty _, (Term _ | Closure _ | Handler _ | Tag _)
-    | Closure _, (Term _ | Ty _ | Handler _ | Tag _)
-    | Handler _, (Term _ | Ty _ | Closure _ | Tag _)
-    | Tag _, (Term _ | Ty _ | Closure _ | Handler _) ->
-      false
+    | Ref v1, Ref v2 ->
+       (* XXX should we compare references by value instead? *)
+       v1 == v2
 
     | Closure _, Closure _
     | Handler _, Handler _ ->
+       (* XXX should we use physical comparison == instead? *)
+       false
+
+    | Term _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
+    | Ty _, (Term _ | Closure _ | Handler _ | Tag _ | Ref _)
+    | Closure _, (Term _ | Ty _ | Handler _ | Tag _ | Ref _)
+    | Handler _, (Term _ | Ty _ | Closure _ | Tag _ | Ref _)
+    | Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Ref _)
+    | Ref _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _) ->
       false
 
-
 let (>>=) = bind
 
 module AtomSet = Name.AtomSet
@@ -674,7 +677,7 @@ module Env = struct
        raise Match_fail
 
   let rec collect_pattern env xvs (p,loc) v =
-    match p, v with 
+    match p, v with
     | Syntax.Patt_Anonymous, _ -> xvs
 
     | Syntax.Patt_As (p,k), v ->
@@ -702,8 +705,8 @@ module Env = struct
     | Syntax.Patt_Tag (tag, ps), Tag (tag', vs) when Name.eq_ident tag tag' ->
       multicollect_pattern env xvs ps vs
 
-    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _)
-    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _) ->
+    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
+    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | Ref _) ->
        raise Match_fail
 
   and multicollect_pattern env xvs ps vs =

src/nucleus/value.mli

@@ -21,6 +21,7 @@ type value = private
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | Ref of value ref
 
 and ('a,'b) closure
 
@@ -38,6 +39,7 @@ and handler = {
 val mk_term : Judgement.term -> value
 val mk_ty : Judgement.ty -> value
 val mk_handler : handler -> value
+val mk_ref : value -> value
 
 val mk_closure' : env -> (env -> 'a -> 'b result) -> ('a,'b) closure
 val mk_closure : env -> (env -> value -> value result) -> value
@@ -47,15 +49,14 @@ val as_term : loc:Location.t -> value -> Judgement.term
 val as_ty : loc:Location.t -> value -> Judgement.ty
 val as_closure : loc:Location.t -> value -> (value,value) closure
 val as_handler : loc:Location.t -> value -> handler
-
+val as_ref : loc:Location.t -> value -> value ref
 
 (** Names and arities of predefined data constructors *)
 val predefined_tags : (Name.ident * int) list
 
 (** Wrappers for making tags *)
 val from_option : value option -> value
 val from_pair : value * value -> value
-val from_unit : unit -> value
 val from_list : value list -> value
 
 (** Convert tags to ocaml types *)
@@ -66,6 +67,7 @@ val mk_tag : Name.ident -> value list -> value
 val return : 'a -> 'a result
 val return_term : Judgement.term -> value result
 val return_ty : Judgement.ty -> value result
+val return_unit : value result
 val return_closure : env -> (env -> value -> value result) -> value result
 
 val return_handler : env ->
@@ -95,7 +97,8 @@ val top_handle : loc:Location.t -> env -> 'a result -> 'a
 (** Pretty-print a value. *)
 val print_value : ?max_level:int -> Name.ident list -> value -> Format.formatter -> unit
 
-val print_value_key : value -> Format.formatter -> unit
+(** a descriptive name of a value, e.g. the name of [Handler _] is ["a handler"] *)
+val name_of : value -> string
 
 (** Check that a result is a value and return it, or complain. *)
 val to_value : loc:Location.t -> 'a result -> 'a

src/parser/desugar.ml

@@ -259,6 +259,24 @@ let rec comp ~yield (env : Value.Env.t) bound (c',loc) =
       let c2 = comp ~yield env bound c2 in
       Syntax.Let (xcs, c2), loc
 
+    | Input.Lookup c ->
+       let c = comp ~yield env bound c in
+       Syntax.Lookup c, loc
+
+    | Input.Ref c ->
+       let c = comp ~yield env bound c in
+       Syntax.Ref c, loc
+
+    | Input.Update (c1, c2) ->
+       let c1 = comp ~yield env bound c1
+       and c2 = comp ~yield env bound c2 in
+       Syntax.Update (c1, c2), loc
+
+    | Input.Sequence (c1, c2) ->
+       let c1 = comp ~yield env bound c1
+       and c2 = comp ~yield env bound c2 in
+       Syntax.Sequence (c1, c2), loc
+
     | Input.Assume ((x, t), c) ->
        let t = comp ~yield env bound t in
        let bound = add_bound x bound in

src/parser/input.mli

@@ -47,6 +47,10 @@ and term' =
   | Tag of Name.ident * comp list
   | Match of comp * match_case list
   | Let of (Name.ident * comp) list * comp
+  | Lookup of comp
+  | Update of comp * comp
+  | Ref of comp
+  | Sequence of comp * comp
   | Assume of (Name.ident * comp) * comp
   | Where of comp * expr * comp
   | Ascribe of comp * ty

src/parser/lexer.ml

@@ -30,6 +30,7 @@ let reserved = [
   ("in", IN) ;
   ("operation", OPERATION) ;
   ("rec", REC) ;
+  ("ref", REF) ;
   ("refl", REFL) ;
   ("Type", TYPE) ;
   ("typeof", TYPEOF) ;
@@ -109,6 +110,9 @@ and token_aux ({ stream;_ } as lexbuf) =
   | "->" | 8594 | 10230      -> f (); ARROW
   | "=>" | 8658 | 10233      -> f (); DARROW
   | "==" | 8801              -> f (); EQEQ
+  | '!'                      -> f (); BANG
+  | ":="                     -> f (); COLONEQ
+  | ';'                      -> f (); SEMICOLON
   | prefixop                 -> f (); PREFIXOP (lexeme lexbuf, Location.of_lexeme lexbuf)
   | infixop0                 -> f (); INFIXOP0 (lexeme lexbuf, Location.of_lexeme lexbuf)
   | infixop1                 -> f (); INFIXOP1 (lexeme lexbuf, Location.of_lexeme lexbuf)