Committing/pushing progress on interp (adding pattern matching and moving closer to function calls) now that there's internet available.

1 files changed, 130 insertions, 38 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b4affe37..3699b62b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -2,40 +2,40 @@ open Pervasives
 open Pmap
 open Ast
 
-type box_ref = id * nat
-
 type mem 'a = map 'a value
 
 type value =
-     | V_box of box_ref (* For local reg types *)
-     | V_lit of lit
-     | V_tuple of list value
-     | V_list of list value
-     | V_vector of list value
-     | V_record of list (id * value)
+ | V_box of id (* For local reg types *)
+ | V_lit of lit
+ | V_tuple of list value
+ | V_list of list value
+     (* TODO: once there is type information, it would be better to use Lem vectors if at all possible *)
+ | V_vector of nat * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
+ | V_record of list (id * value)
 
 (* These may need to be refined or expanded based on memory requirement *)
 type action = 
-     | Read_reg of id * nat * nat
-     | Write_reg id * nat * nat * value
-     | Read_mem id * nat * nat
-     | Write_mem id * nat * nat * value
+ | Read_reg of id * nat * nat
+ | Write_reg id * nat * nat * value
+ | Read_mem id * nat * nat
+ | Write_mem id * nat * nat * value
 
+(* Either a case must be added for parallel options or action must be tied to a list *)
 type outcome =
-     | Value of value
-     | Action of action * id * exp * mem nat
-     | Error of string (* When we store location information, it should be added here *)
+ | Value of value
+ | Action of action * id * exp * mem id
+ | Error of string (* When we store location information, it should be added here *)
 
-val to_value : map id nat  -> exp -> value
+val to_value : exp -> value
 val to_exp : value -> exp
 
 val read_hex : string -> value
 val read_bin : string -> value
 
-(* interprets the exp sequentially in the presence of a set of top level definitions, a register memory, and a main memory *)
+(* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
 val interp : defs -> exp -> outcome
 
-let rec to_value env exp =
+let rec to_value exp =
     match exp with
     | E_lit lit ->
       match lit with
@@ -43,12 +43,12 @@ let rec to_value env exp =
       | L_bin(s) -> read_bin s
       | _ -> V_lit lit
       end
-    | E_tuple(exps) -> V_tuple (List.map (to_value env) exps)
-    | E_vector(exps) -> V_vector (List.map (to_value env) exps)
-    | E_list(exps) -> V_list (List.map (to_value env) exps)
-    | E_record(fexps) -> V_record (List.map (fun (FE_exp(id,exp)) -> (id, to_value env exp))
+    | E_tuple(exps) -> V_tuple (List.map to_value exps)
+    | E_vector(exps) -> V_vector 0 true (List.map to_value exps)
+    | E_list(exps) -> V_list (List.map to_value exps)
+    | E_record(fexps) -> V_record (List.map (fun (FE_exp(id,exp)) -> (id, to_value exp))
                                                                 ((fun (FES_fexps(fexps,_)) -> fexps) fexps))
-    | E_id id -> V_box(id,find id env)
+    | E_id id -> V_box(id)
     | _ -> V_error_value
     end
 
@@ -57,43 +57,135 @@ let rec to_exp v =
     | V_box(id,nat) -> E_id id
     | V_lit lit -> E_lit lit
     | V_tuple(vals) -> E_tuple (List.map to_exp vals)
-    | V_vector(vals) -> V_vector (List.map to_exp vals)
+    | V_vector(n,inc,vals) -> E_vector (List.map to_exp vals) (*Todo, if n not 0 or inc not true, should generate an indexed vector *)
     | V_record(ivals) -> E_record(FES_fexps(List.map (fun (id,val) -> FE_exp(id, to_exp val)) ivals, false))
     end
 
-let rec interp_main defs local_mem exp =
+val find_type_def : defs -> id -> option type_def
+val find_function : defs -> id -> option list funcl
+
+let get_funcls id (FD_funciton r e t fcls) =
+  List.filter (fun (FCL_funcl name pat exp) -> id = name) fcls (* Is this = ok here? *)
+
+let rec find_function defs id =
+  match defs with 
+  | [] -> None
+  | def::defs -> 
+    match def with
+    | DEF_fundef f -> get_funcls id f
+    | _ -> find_function defs id
+    end end
+
+val match_pattern : pat -> value -> bool * list (id * value)
+
+let rec match_pattern p value =
+  match p with 
+  | P_lit(lit) -> 
+    match value with
+    | V_lit(litv) -> lit = litv, [] (*Is this = ok? or do I need to write my own here*)
+    | _ -> false,[]
+    end
+ | P_wild -> true,[]
+ | P_as (pat,id) ->  let matched_p,bounds = match_pattern pat value in
+		     if matched_p then
+		       matched_p,(id,value)::bounds
+		     else false,[]
+ | P_typ (typ,pat) -> match_pattern pat value (* Might like to destructure against the type to get information *)
+ | P_id (id) -> true, (id,value)::bounds
+(* | P_app (id, list pat) -> (* union constructor pattern *) need defs for this case, to check that id is a constructor *)
+(* | P_record of list fpat * bool (* struct pattern *) todo *)
+ | P_vector(pats) ->
+   match value with
+   | V_vector(n,inc,vals) ->
+     if ((List.length vals) = (List.length pats))
+     then List.fold_right2
+       (fun pat value (matched_p,bounds) -> if matched_p then
+	   let matched_p,new_bounds = match_pattern pat value in
+	   matched_p, new_bounds@bounds) 
+       (if inc then pats else List.reverse pats) (true,[])
+   | _ -> false,[]
+     end
+ | P_vector_indexed(ipats) ->
+   match value with
+   | V_vector(n,inc,vals) ->
+     let v_len = if inc then List.length vals + n else n - List.length vals in
+     List.fold_right
+       (fun (i,pat) (matched_p,bounds) -> if matched_p && i < v_len then
+	   let matched_p,new_bounds = match_pattern pat (List.nth (if inc then i+n else i-n)) in
+	   matched_p,new_bounds@bounds)
+       ipats (true,[])
+   | _ -> false, []
+   end
+(* | P_vector_concat of list pat (* concatenated vector pattern *) TODO *)
+ | P_tup(pats) ->
+   match value with 
+   | V_tuple(vals) ->
+     if ((List.length pats)= (List.length vals))
+     then List.fold_right2 
+       (fun pat v (matched_p,bounds) -> if matched_p then
+	   let matched_p,new_bounds = match_pattern pat v in
+	   matched_p,bounds@new_bounds)
+       pats vals (true,[])
+   | _ -> false,[]
+     end 
+ | P_list(pats)
+   match value with 
+   | V_list(vals) ->
+     if ((List.length pats)= (List.length vals))
+     then List.fold_right2 
+       (fun pat v (matched_p,bounds) -> if matched_p then
+	   let matched_p,new_bounds = match_pattern pat v in
+	   matched_p,bounds@new_bounds)
+       pats vals (true,[])
+   | _ -> false,[]
+     end 
+
+
+val interp_main : defs -> map id typ -> map id value -> mem id -> exp -> (outcome * mem id)
+
+let rec exp_list defs build_e build_v l_env local_mem vals exps =
+  match exps with
+  | [ ] -> Value (build_v vals), local_mem
+  | e::exps -> 
+    match (interp_main defs l_env local_mem e) with
+    | Value(v),lm -> exp_list defs build_e build_v l_env lm build_e vals@[v] exps
+    | Action(action, id, e, mem),lm -> Action(action, id, (build_e (List.map to_exp vals)@(e::exps)), mem),lm
+    | Error s, lm -> Error s, lm end
+  end
+
+and interp_main defs l_env l_mem exp =
     match exp with
-    | E_lit lit -> (Value (V_lit lit), local_mem)
-    | E_cast(typ,exp) -> interp_main defs local_mem exp (* Potentially introduce coercions between vectors and numbers here? *)
+    | E_lit lit -> (Value (V_lit lit), l_mem)
+    | E_cast(typ,exp) -> interp_main defs l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
     | E_if(cond,thn,els) ->
-      let (val,lm) = interp_main defs local_mem cond in
+      let (val,lm) = interp_main defs l_env l_mem cond in
       match val with
       | Value val -> 
             match val with
-                | V_lit(L_true) -> interp_main defs lm thn
-                | V_lit(L_false) -> interp_main defs lm els
-                | Error "Type error, not provided boolean for if" end
+                | V_lit(L_true) -> interp_main defs l_env lm thn
+                | V_lit(L_false) -> interp_main defs l_env lm els
+                | _ -> Error "Type error, not provided boolean for if" end
       | Action(action, id, c, mem) -> Action action (E_if c thn els) c mem, lm
       | Error s -> Error s, lm
       end end
+    | E_list(exps) ->
+      exp_list defs E_list V_list l_env l_mem [] exps
     | E_cons(h,t) ->
       let (v,lm) = interp_main defs local_mem h in
       match v with
       | Value h -> (let (v,lm) = interp_main defs lm t in
                           match v with 
                           | Value (V_list(t) -> Value(V_list(h::t)), lm
-                          | Action action id t mem -> Action action id (E_cons(to_exp h) t) mem (* need to maintain a mapping from the id to the mem *), lm
+                          | Action action id t mem -> Action action id (E_cons(to_exp h) t) mem, lm
                           | Error s -> Error s, lm
                            end end
       | Action action id h mem -> Action action id (E_cons h t) mem, lm
       | Error s -> Error s, lm
       end end
-    | E_tuple(exps) -> let vals, local_mem = 
-                                 List.fold_right (fun exp (tups,local_mem) -> 
-                                                                    let val, lm = interp_main defs local_mem exp in
-                                                                    (tups@[val],lm) end)
-                                                       exps ([], local_mem) in
-                                V_tuple vals, local_mem end
+    | E_tuple(exps) -> 
+      exp_list defs E_tuple V_tuple local_mem [] exps
+    | E_vector(exps) ->
+      exp_list defs E_vector (fun vals -> V_vector 0 true vals) local_mem [] exps
     | E_block(exps) -> List.fold_right (fun exp (val,local_mem,reg_mem,main_mem) -> interp_main defs local_mem reg_mem main_mem exp)
                                                      exps
                                                      (V_lit(Lit_unit),local_mem,reg_mem,main_mem)