summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem841
-rw-r--r--src/lem_interp/interp_lib.lem36
-rw-r--r--src/lem_interp/run_interp.ml57
3 files changed, 592 insertions, 342 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8a68f8eb..854ed202 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,19 +1,33 @@
open import Pervasives
import Map
import Map_extra
-import Maybe
import List_extra
-import String
+open import String_extra
open import Interp_ast
+type tannot = maybe (t * tag * list nec * effect)
+
+val pure : effect
+let pure = Effect_aux(Effect_set []) Unknown
+
+val intern_annot : tannot -> tannot
+let intern_annot annot =
+ match annot with
+ | Just (t,_,ncs,effect) ->
+ Just (t,Tag_empty,ncs,pure)
+ | Nothing -> Nothing
+ end
+
+let val_annot typ = Just(typ,Tag_empty,[],pure)
+
(* Workaround Lem's inability to scrap my (type classes) boilerplate.
* Implementing only Eq, and only for literals - hopefully this will
* be enough, but we should in principle implement ordering for everything in
* Interp_ast *)
val lit_eq: lit -> lit -> bool
-let lit_eq left right =
+let lit_eq (L_aux left _) (L_aux right _) =
match (left, right) with
| (L_unit, L_unit) -> true
| (L_zero, L_zero) -> true
@@ -39,16 +53,16 @@ end
let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
-let get_id id = match id with Id s -> s | DeIid s -> s end
+let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
type value =
- | V_boxref of nat
+ | V_boxref of nat * t
| V_lit of lit
| V_tuple of list value
| V_list of list value
| V_vector of natural * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
- | V_record of list (id * value)
- | V_ctor of id * value
+ | V_record of t * list (id * value)
+ | V_ctor of id * t * value
(* seems useless currently:
let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
@@ -78,7 +92,7 @@ type env = list (id * value)
let emem = Mem 1 Map.empty
type reg_form =
- | Reg of id * typ
+ | Reg of id * t
| SubReg of id * reg_form * index_range
(* These may need to be refined or expanded based on memory requirement *)
@@ -92,34 +106,35 @@ type action =
(* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
type stack =
| Top
- | Frame of id * exp * env * mem * stack
+ | Frame of id * exp tannot * env * mem * stack
(* 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 * stack
- | Error of string (* When we store location information, it should be added here *)
+ | Error of l * string
(* 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
+val interp : defs tannot -> exp tannot -> outcome
-val to_registers : defs -> list (id * reg_form)
-let rec to_registers (Defs defs) =
- match defs with
+val to_registers : defs tannot -> list (id * reg_form)
+let rec to_registers (Defs defs) = []
+(* match defs with
| [ ] -> [ ]
- | def::defs ->
+ | (DEF_aux def _)::defs ->
match def with
| DEF_spec valsp ->
match valsp with
- | VS_val_spec (TypSchm_ts tq ((Typ_app (Id "reg") _) as t)) id -> (id, Reg id t):: (to_registers (Defs defs))
+ | (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts tq ((Typ_aux (Typ_app (Id_aux (Id "reg") _) _) _) as t)) _) id) _) ->
+ (id, Reg id t):: (to_registers (Defs defs))
| _ -> to_registers (Defs defs)
end
| DEF_reg_dec typ id -> (id, Reg id typ) :: (to_registers (Defs defs))
| DEF_type tdef ->
match tdef with
- | TD_register id n1 n2 ranges ->
- (id,Reg id (Typ_app (Id "vector")[]))::
- ((to_reg_ranges id (Reg id (Typ_app (Id "vector")[])) ranges) ++ (to_registers (Defs defs)))
+ | (TD_aux (TD_register id n1 n2 ranges) _) ->
+ (id,Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown))::
+ ((to_reg_ranges id (Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown)) ranges) ++ (to_registers (Defs defs)))
| _ -> to_registers (Defs defs)
end
| _ -> to_registers (Defs defs)
@@ -129,13 +144,13 @@ and to_reg_ranges base_id base_reg ranges =
match ranges with
| [ ] -> [ ]
| (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges)
- end
+ end*)
val has_memory_effect : list base_effect -> bool
let rec has_memory_effect efcts =
match efcts with
| [] -> false
- | e::efcts ->
+ | (BE_aux e _)::efcts ->
match e with
| BE_wreg -> true
| BE_wmem -> true
@@ -143,53 +158,66 @@ let rec has_memory_effect efcts =
end
end
+let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
+let get_effects (Typ_aux t _) =
+ match t with
+ | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
+ | _ -> []
+ end
+
(*Look for externs as well*)
-val to_memory_ops : defs -> list (id * typ)
-let rec to_memory_ops (Defs defs) =
- match defs with
+val to_memory_ops : defs tannot -> list (id * typ)
+let rec to_memory_ops (Defs defs) = []
+(* match defs with
| [] -> []
- | def ::defs ->
+ | (DEF_aux def _) ::defs ->
match def with
- | DEF_spec valsp ->
+ | DEF_spec (VS_aux valsp _) ->
match valsp with
- | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+ | VS_val_spec ts id ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
- | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id _ ->
+ | VS_extern_spec ts id _ ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
- | VS_extern_no_rename (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+ | VS_extern_no_rename ts id ->
+ let t = get_typ ts in
+ let eff = get_effects t in
if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
| _ -> to_memory_ops (Defs defs) end
| _ -> to_memory_ops (Defs defs) end
- end
+ end*)
-val to_externs : defs -> list (id * string)
-let rec to_externs (Defs defs) =
- match defs with
+val to_externs : defs tannot -> list (id * string)
+let rec to_externs (Defs defs) = []
+(* match defs with
| [] -> []
- | def ::defs ->
+ | (DEF_aux def _) ::defs ->
match def with
- | DEF_spec valsp ->
+ | DEF_spec (VS_aux valsp _) ->
match valsp with
- | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r e) as t)) id s ->
+ | VS_extern_spec (TypSchm_aux (TypSchm_ts tq (Typ_aux (Typ_fn a r e) _)) _) id s ->
(id,s)::(to_externs (Defs defs))
| _ -> to_externs (Defs defs) end
| _ -> to_externs (Defs defs) end
- end
+ end*)
-val to_data_constructors : defs -> list (id * typ)
+val to_data_constructors : defs tannot -> list (id * typ)
let rec to_data_constructors (Defs defs) =
match defs with
| [] -> []
- | def :: defs ->
+ | (DEF_aux def _) :: defs ->
match def with
- | DEF_type t ->
+ | DEF_type (TD_aux t _)->
match t with
| TD_variant id _ tq tid_list _ ->
(List.map
- (fun t ->
+ (fun (Tu_aux t _) ->
match t with
| (Tu_ty_id x y) -> (y,x)
- | Tu_id x -> (id,Typ_app (Id "unit") []) end) tid_list)++(to_data_constructors (Defs defs))
+ | Tu_id x -> (id,Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown) end) tid_list)++(to_data_constructors (Defs defs))
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
@@ -198,7 +226,7 @@ val in_env : env -> id -> maybe value
let rec in_env env id =
match env with
| [] -> Nothing
- | (eid,value)::env -> if eid = id then Just value else in_env env id
+ | (eid,value)::env -> if (get_id eid) = (get_id id) then Just value else in_env env id
end
val in_mem : mem -> nat -> value
@@ -213,7 +241,7 @@ let update_mem (Mem c m) loc value =
Mem c m'
val is_lit_vector : lit -> bool
-let is_lit_vector l =
+let is_lit_vector (L_aux l _) =
match l with
| L_bin _ -> true
| L_hex _ -> true
@@ -221,16 +249,16 @@ let is_lit_vector l =
end
val litV_to_vec : lit -> value
-let litV_to_vec l =
- match l with
+let litV_to_vec (L_aux lit l) =
+ match lit with
| L_hex s ->
let hexes = String.toCharList s in
(* XXX unimplemented *)
V_vector 0 true []
| L_bin s ->
let bits = String.toCharList s in
- let exploded_bits = List.map (fun c -> String.toString [c]) bits in
- let bits = List.map (fun s -> match s with | "0" -> (V_lit L_zero) | "1" -> (V_lit L_one) end) exploded_bits in
+ let exploded_bits = bits in (*List.map (fun c -> String.toString [c]) bits in*)
+ let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) exploded_bits in
(* XXX assume binary constants are written in big-endian, convert them to
* little-endian by default - we might need syntax to change both of those
* assumptions. *)
@@ -281,18 +309,18 @@ end
val fupdate_record : value -> value -> value
let fupdate_record base updates =
match (base,updates) with
- | (V_record bs,V_record us) -> V_record (update_field_list bs us) end
+ | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) end
val update_vector_slice : value -> value -> mem -> mem
let rec update_vector_slice vector value mem =
match (vector,value) with
| ((V_vector m inc vs),(V_vector n inc2 vals)) ->
foldr2 (fun vbox v mem -> match vbox with
- | V_boxref n -> update_mem mem n v end)
+ | V_boxref n t -> update_mem mem n v end)
mem vs vals
| ((V_vector m inc vs),v) ->
List.foldr (fun vbox mem -> match vbox with
- | V_boxref n -> update_mem mem n v end)
+ | V_boxref n t -> update_mem mem n v end)
mem vs
end
@@ -326,13 +354,13 @@ val in_reg : list (id * reg_form) -> id -> maybe reg_form
let rec in_reg regs id =
match regs with
| [] -> Nothing
- | (eid,regf)::regs -> if eid = id then Just regf else in_reg regs id
+ | (eid,regf)::regs -> if (get_id eid) = (get_id id) then Just regf else in_reg regs id
end
val in_ctors : list (id * typ) -> id -> maybe typ
let rec in_ctors ctors id =
match ctors with
| [] -> Nothing
- | (cid,typ)::ctors -> if cid = id then Just typ else in_ctors ctors id
+ | (cid,typ)::ctors -> if (get_id cid) = (get_id id) then Just typ else in_ctors ctors id
end
let add_to_top_frame e_builder stack =
@@ -340,33 +368,105 @@ let add_to_top_frame e_builder stack =
| Frame id e env mem stack -> Frame id (e_builder e) env mem stack
end
-let rec to_exp v =
- match v with
- | V_boxref n -> E_id (Id ("XXX string_of_num n"))
- | V_lit lit -> E_lit lit
- | V_tuple(vals) -> E_tuple (List.map to_exp vals)
- | V_vector n inc vals ->
- if (inc && n=0)
- then E_vector (List.map to_exp vals)
- else if inc then
- E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
- else
- E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
- | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
- | V_list(vals) -> E_list (List.map to_exp vals)
- | V_ctor id vals -> E_app id [to_exp vals]
- end
+let id_of_string s = (Id_aux (Id s) Unknown)
+
+let rec combine_typs ts =
+ match ts with
+ | [] -> T_var (Kid_aux (Var "fresh") Unknown)
+ | [t] -> t
+ | t::ts ->
+ let t' = combine_typs ts in
+ match (t,t') with
+ | (_,T_var _) -> t
+ | ((T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
+ (T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
+ let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
+ let r = (larger + larger_r) - smaller in
+ T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
+ | ((T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1);
+ T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
+ (T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2);
+ T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
+ let t = combine_typs [t1;t2] in
+ match (o1,o2) with
+ | (Ord_inc,Ord_inc) ->
+ let larger_start = if b1 < b2 then b2 else b1 in
+ let smaller_rise = if r1 < r2 then r1 else r2 in
+ (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
+ (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+ | (Ord_dec,Ord_dec) ->
+ let smaller_start = if b1 < b2 then b1 else b2 in
+ let smaller_fall = if r1 < r2 then r2 else r2 in
+ (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
+ (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+ | _ -> T_var (Kid_aux (Var "fresh") Unknown)
+ end
+ | _ -> t'
+ end
+ end
-val find_type_def : defs -> id -> maybe type_def
-val find_function : defs -> id -> maybe (list funcl)
-let get_funcls id (FD_function _ _ _ fcls) =
- List.filter (fun (FCL_Funcl name pat exp) -> id = name) fcls
+let rec val_typ v =
+ match v with
+ | V_boxref n t -> T_app (id_of_string "reg") (T_args [T_arg_typ t])
+ | V_lit (L_aux lit _) ->
+ match lit with
+ | L_unit -> T_id (id_of_string "unit")
+ | L_true -> T_id (id_of_string "bool")
+ | L_false -> T_id (id_of_string "bool")
+ | L_one -> T_id (id_of_string "bit")
+ | L_zero -> T_id (id_of_string "bit")
+ | L_string _ -> T_id (id_of_string "string")
+ | L_num n -> T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
+ | L_undef -> T_var (Kid_aux (Var "fresh") Unknown)
+ end
+ | V_tuple vals -> T_tup (List.map val_typ vals)
+ | V_vector n inc vals ->
+ let ts = List.map val_typ vals in
+ let t = combine_typs ts in
+ T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
+ T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
+ T_arg_typ t])
+ | V_record t ivals -> t
+ | V_list vals ->
+ let ts = List.map val_typ vals in
+ let t = combine_typs ts in
+ T_app (id_of_string "list") (T_args [T_arg_typ t])
+ | V_ctor id t vals -> t
+ end
+
+let rec to_exp v =
+ E_aux
+ (match v with
+ | V_boxref n t -> E_id (Id_aux (Id (show n)) Unknown)
+ | V_lit lit -> E_lit lit
+ | V_tuple(vals) -> E_tuple (List.map to_exp vals)
+ | V_vector n inc vals ->
+ if (inc && n=0)
+ then E_vector (List.map to_exp vals)
+ else if inc then
+ E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+ else
+ E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
+ | V_record t ivals ->
+ E_record(FES_aux (FES_Fexps
+ (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false)
+ (Unknown,Nothing))
+ | V_list(vals) -> E_list (List.map to_exp vals)
+ | V_ctor id t vals -> E_app id [to_exp vals]
+ end)
+ (Unknown,(val_annot (val_typ v)))
+
+val find_type_def : defs tannot -> id -> maybe (type_def tannot)
+val find_function : defs tannot -> id -> maybe (list (funcl tannot))
+
+let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
+ List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
let rec find_function (Defs defs) id =
match defs with
| [] -> Nothing
- | def::defs ->
+ | (DEF_aux def _)::defs ->
match def with
| DEF_fundef f -> match get_funcls id f with
| [] -> find_function (Defs defs) id
@@ -380,8 +480,8 @@ let find_memory mems id = List.lookup id mems
val find_extern : list ( id * string ) -> id -> maybe string
let find_extern externs id = List.lookup id externs
-val match_pattern : pat -> value -> bool * list (id * value)
-let rec match_pattern p value =
+val match_pattern : pat tannot -> value -> bool * list (id * value)
+let rec match_pattern (P_aux p _) value =
match p with
| P_lit(lit) ->
if is_lit_vector lit then
@@ -411,7 +511,7 @@ let rec match_pattern p value =
| P_id id -> (true, [(id,value)])
| P_app id pats ->
match value with
- | V_ctor cid (V_tuple vals) ->
+ | V_ctor cid t (V_tuple vals) ->
if (id = cid && ((List.length pats) = (List.length vals)))
then foldr2
(fun pat value (matched_p,bounds) ->
@@ -423,9 +523,9 @@ let rec match_pattern p value =
| _ -> (false,[]) end
| P_record fpats _ ->
match value with
- | V_record fvals ->
+ | V_record t fvals ->
List.foldr
- (fun (FP_Fpat id pat) (matched_p,bounds) ->
+ (fun (FP_aux (FP_Fpat id pat) _) (matched_p,bounds) ->
if matched_p then
let (matched_p,new_bounds) = match in_env fvals id with
| Nothing -> (false,[])
@@ -465,7 +565,7 @@ let rec match_pattern p value =
| V_vector n inc vals ->
let (matched_p,bounds,remaining_vals) =
List.foldl
- (fun (matched_p,bounds,r_vals) pat ->
+ (fun (matched_p,bounds,r_vals) (P_aux pat _) ->
match pat with
| P_vector pats -> vec_concat_match pats r_vals
| P_id id -> (false,[],[]) (*Need to have at least a guess of how many to consume*)
@@ -512,37 +612,37 @@ and vec_concat_match pats r_vals =
end
-val find_funcl : list funcl -> value -> maybe (env * exp)
+val find_funcl : list (funcl tannot) -> value -> maybe (env * (exp tannot))
let rec find_funcl funcls value =
match funcls with
| [] -> Nothing
- | (FCL_Funcl id pat exp)::funcls ->
+ | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
let (is_matching,env) = match_pattern pat value in
if is_matching then Just (env,exp) else find_funcl funcls value
end
-val find_case : list pexp -> value -> maybe (env * exp)
+val find_case : list (pexp tannot) -> value -> maybe (env * (exp tannot))
let rec find_case pexps value =
match pexps with
| [] -> Nothing
- | (Pat_exp p e)::pexps ->
+ | (Pat_aux (Pat_exp p e) _)::pexps ->
let (is_matching,env) = match_pattern p value in
if is_matching then Just(env,e) else find_case pexps value
end
(*top_level is a tuple of
(all definitions, external functions, letbound values, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
-type top_level = Env of defs * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
+type top_level = Env of (defs tannot) * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
-val interp_main : top_level -> env -> mem -> exp -> (outcome * mem * env)
-val exp_list : top_level -> (list exp -> exp) -> (list value -> value) -> env -> mem -> list value -> list exp -> (outcome * mem * env)
-val interp_lbind : top_level -> env -> mem -> letbind -> ((outcome * mem * env) * (maybe (exp -> letbind)))
+val interp_main : top_level -> env -> mem -> (exp tannot) -> (outcome * mem * env)
+val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> mem -> list value -> list (exp tannot) -> (outcome * mem * env)
+val interp_lbind : top_level -> env -> mem -> (letbind tannot) -> ((outcome * mem * env) * (maybe ((exp tannot) -> (letbind tannot))))
let resolve_outcome to_match value_thunk action_thunk =
match to_match with
| (Value v,lm,le) -> value_thunk v lm le
| (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
- | (Error s,lm,le) -> (Error s,lm,le)
+ | (Error l s,lm,le) -> (Error l s,lm,le)
end
let update_stack (Action act stack) fn = Action act (fn stack)
@@ -557,166 +657,232 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
(fun a -> update_stack a (add_to_top_frame (fun e -> (build_e ((List.map to_exp vals)++(e::exps))))))
end
-and interp_main t_level l_env l_mem exp =
- match exp with
- | E_lit lit -> if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
+and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
+ let (Env defs externs lets regs mems ctors) = t_level in
+ let (typ,tag,ncs,effect) = match annot with
+ | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown),
+ Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+ | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
+ match exp with
+ | E_lit lit ->
+ if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
| E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
- | E_id id -> match in_env l_env id with
- | Just(value) -> match value with
- | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env)
- | _ -> (Value value,l_mem,l_env) end
- | Nothing -> match t_level with
- | (Env defs externs lets regs mems ctors) ->
- match in_env lets id with
- | Just(value) -> (Value value,l_mem,l_env)
- | Nothing ->
- match in_reg regs id with
- | Just(regf) ->
- (Action (Read_reg regf Nothing) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env)
- | Nothing ->
- let name = get_id id in
- (Error (String.stringAppend "unbound identifier " name ),l_mem,l_env)
- end
- end
- end
- end
+ | E_id id ->
+ let name = get_id id in
+ match tag with
+ | Tag_empty ->
+ match in_env l_env id with
+ | Just(value) -> match value with
+ | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
+ | _ -> (Value value,l_mem,l_env) end
+ | Nothing ->
+ match in_env lets id with
+ | Just(value) -> (Value value,l_mem,l_env)
+ | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_none " name), l_mem,l_env)
+ end end
+ | Tag_enum ->
+ match in_env lets id with
+ | Just(value) -> (Value value,l_mem,l_env)
+ | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env)
+ end
+ | Tag_extern _ -> (* Need to change from "register" to which register where different from id *)
+ let regf = Reg id typ in
+ (Action (Read_reg regf Nothing)
+ (Frame (Id_aux (Id "0") Unknown)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),
+ l_mem,l_env)
+ | _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
+ end
| E_if cond thn els ->
resolve_outcome (interp_main t_level l_env l_mem cond)
(fun value lm le ->
match value with
- | V_lit(L_true) -> interp_main t_level l_env lm thn
- | V_lit(L_false) -> interp_main t_level l_env lm els
- | _ -> (Error "Type error, not provided boolean for if",lm,l_env) end)
- (fun a -> update_stack a (add_to_top_frame (fun c -> (E_if c thn els))))
- | E_for id from to_ by order exp ->
+ | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
+ | V_lit(L_aux L_false _) -> interp_main t_level l_env lm els end)
+ (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) (l,annot)))))
+ | E_for id from to_ by ((Ord_aux o _) as order) exp ->
+ let is_inc = match o with
+ | Ord_inc -> true
+ | _ -> false end in
resolve_outcome (interp_main t_level l_env l_mem from)
(fun from_val lm le ->
match from_val with
- | V_lit(L_num from_num) ->
+ | (V_lit(L_aux(L_num from_num) fl) as fval) ->
resolve_outcome (interp_main t_level le lm to_)
(fun to_val lm le ->
match to_val with
- | V_lit(L_num to_num) ->
+ | (V_lit(L_aux (L_num to_num) tl) as tval) ->
resolve_outcome
(interp_main t_level le lm by)
(fun by_val lm le ->
match by_val with
- | V_lit (L_num by_num) ->
+ | (V_lit (L_aux (L_num by_num) bl) as bval) ->
if (from_num = to_num)
- then (Value(V_lit L_unit),lm,le)
- else interp_main t_level le lm
- (E_block [(E_let (LB_val_implicit (P_id id) (E_lit (L_num from_num))) exp);
- (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) order exp)])
- | _ -> (Error "by must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b order exp))))
- | _ -> (Error "to must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by order exp))))
- | _ -> (Error "from must be a number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by order exp))))
+ then (Value(V_lit (L_aux L_unit l)),lm,le)
+ else
+ let (ftyp,ttyp,btyp) = (val_typ fval,val_typ tval,val_typ bval) in
+ interp_main t_level le lm
+ (E_aux
+ (E_block
+ [(E_aux (E_let
+ (LB_aux (LB_val_implicit
+ (P_aux (P_id id) (fl,val_annot ftyp))
+ (E_aux (E_lit(L_aux(L_num from_num) fl)) (fl,val_annot ftyp)))
+ (Unknown,val_annot ftyp))
+ exp) (l,annot));
+ (E_aux (E_for id
+ (if is_inc
+ then (E_aux (E_lit (L_aux (L_num (from_num + by_num)) fl)) (fl,val_annot (combine_typs [ftyp;ttyp])))
+ else (E_aux (E_lit (L_aux (L_num (from_num - by_num)) fl)) (fl,val_annot (combine_typs [ttyp;ftyp]))))
+ (E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,val_annot ttyp))
+ (E_aux (E_lit (L_aux (L_num by_num) bl)) (bl,val_annot btyp))
+ order exp) (l,annot))])
+ (l,annot))
+ | _ -> (Error l "internal error: by must be a number",lm,le) end)
+ (fun a -> update_stack a
+ (add_to_top_frame (fun b ->
+ (E_aux (E_for id
+ (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,(val_annot (val_typ fval))))
+ (E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,(val_annot (val_typ tval))))
+ b order exp) (l,annot)))))
+ | _ -> (Error l "internal error: to must be a number",lm,le) end)
+ (fun a -> update_stack a
+ (add_to_top_frame (fun t ->
+ (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,val_annot (val_typ fval)))
+ t by order exp) (l,annot)))))
+ | _ -> (Error l "internal error: from must be a number",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) (l,annot)))))
| E_case exp pats ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun v lm le ->
match find_case pats v with
- | Nothing -> (Error "No matching patterns in case",lm,le)
+ | Nothing -> (Error l "No matching patterns in case",lm,le)
| Just (env,exp) -> interp_main t_level (env++l_env) lm exp end)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_case e pats)))
- | E_record(FES_Fexps fexps _) ->
- let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
- exp_list t_level (fun es -> (E_record(FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
- (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps
- | E_record_update exp (FES_Fexps fexps _) ->
+ (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) (l,annot)))))
+ | E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
+ let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+ exp_list t_level
+ (fun es ->
+ (E_aux (E_record
+ (FES_aux (FES_Fexps (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot))
+ (l,annot)))
+ (fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
+ | E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun rv lm le ->
match rv with
- | V_record fvs ->
- let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
- resolve_outcome (exp_list t_level (fun es -> (E_record_update (to_exp rv) (FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
- (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps)
+ | V_record t fvs ->
+ let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+ resolve_outcome (exp_list t_level
+ (fun es ->
+ (E_aux (E_record_update (to_exp rv)
+ (FES_aux (FES_Fexps
+ (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
+ fields es) false) fes_annot))
+ (l,annot)))
+ (fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
(fun vs lm le ->
(Value (fupdate_record rv vs), lm, le))
(fun a -> a)
- | _ -> (Error "record upate requires record",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_record_update e (FES_Fexps fexps false))))
+ | _ -> (Error l "record upate requires record",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame
+ (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot))))
| E_list(exps) ->
- exp_list t_level E_list V_list l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_list exps) (l,annot)) V_list l_env l_mem [] exps
| E_cons hd tl ->
resolve_outcome (interp_main t_level l_env l_mem hd)
(fun hdv lm le -> resolve_outcome
(interp_main t_level l_env lm tl)
(fun tlv lm le -> match tlv with
| V_list t -> (Value(V_list (hdv::t)),lm,le)
- | _ -> (Error ":: of non-list value",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun t -> E_cons (to_exp hdv) t))))
- (fun a -> update_stack a (add_to_top_frame (fun h -> E_cons h tl)))
+ | _ -> (Error l ":: of non-list value",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) (l,annot)))))
+ (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) (l,annot))))
| E_field exp id ->
resolve_outcome (interp_main t_level l_env l_mem exp)
(fun value lm le ->
match value with
- | V_record fexps -> match in_env fexps id with
+ | V_record t fexps -> match in_env fexps id with
| Just v -> (Value v,lm,l_env)
- | Nothing -> (Error "Field not found in record",lm,le) end
- | _ -> (Error "Field access requires a record",lm,le)
+ | Nothing -> (Error l "Field not found in record",lm,le) end
+ | _ -> (Error l "Field access requires a record",lm,le)
end )
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_field e id)))
+ (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))))
| E_vector_access vec i ->
resolve_outcome (interp_main t_level l_env l_mem i)
(fun iv lm le ->
match iv with
- | V_lit (L_num n) ->
+ | V_lit (L_aux (L_num n) ln) ->
resolve_outcome (interp_main t_level l_env lm vec)
(fun vvec lm le ->
match vvec with
| V_vector base inc vals -> (Value (access_vector vvec n),lm,le)
- | _ -> (Error "Vector access of non-vector",lm,le)end)
- (fun a -> update_stack a (add_to_top_frame (fun v -> (E_vector_access v (E_lit (L_num n))))))
- | _ -> (Error "Vector access not given a number for index",lm,l_env) end)
- (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_access vec i)))
+ | _ -> (Error l "Vector access of non-vector",lm,le)end)
+ (fun a -> update_stack a
+ (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))))
+ | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
+ (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot))))
| E_vector_subrange vec i1 i2 ->
resolve_outcome (interp_main t_level l_env l_mem i1)
(fun i1v lm le ->
match i1v with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome (interp_main t_level l_env lm i2)
(fun i2v lm le ->
match i2v with
- | V_lit (L_num n2) ->
+ | V_lit (L_aux (L_num n2) ln2) ->
resolve_outcome (interp_main t_level l_env lm vec)
(fun vvec lm le ->
match vvec with
| V_vector base inc vals -> (Value (slice_vector vvec n1 n2),lm,le)
- | _ -> (Error "Vector slice of non-vector",lm,le)end)
+ | _ -> (Error l "Vector slice of non-vector",lm,le)end)
(fun a -> update_stack a
- (add_to_top_frame (fun v -> (E_vector_subrange v (E_lit (L_num n1)) (E_lit (L_num n2))))))
- | _ -> (Error "vector slice given non number for last index",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i2 -> (E_vector_subrange vec (E_lit (L_num n1)) i2))))
- | _ -> (Error "Vector slice given non-number for first index",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_vector_subrange vec i1 i2))))
+ (add_to_top_frame
+ (fun v -> (E_aux (E_vector_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+ (l,annot)))))
+ | _ -> (Error l "vector slice given non number for last index",lm,le) end)
+ (fun a -> update_stack a
+ (add_to_top_frame
+ (fun i2 -> (E_aux (E_vector_subrange vec
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ i2) (l,annot)))))
+ | _ -> (Error l "Vector slice given non-number for first index",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) (l,annot)))))
| E_vector_update vec i exp ->
resolve_outcome (interp_main t_level l_env l_mem i)
(fun vi lm le ->
match vi with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome (interp_main t_level le lm exp)
(fun vup lm le ->
resolve_outcome (interp_main t_level le lm vec)
(fun vec lm le ->
match vec with
| V_vector base inc vals -> (Value (fupdate_vec vec n1 vup), lm,le)
- | _ -> (Error "Update of vector given non-vector",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun v -> E_vector_update v (E_lit (L_num n1)) (to_exp vup)))))
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_vector_update vec (E_lit (L_num n1)) e)))
- | _ -> (Error "Update of vector requires number for access",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_update vec i exp)))
+ | _ -> (Error l "Update of vector given non-vector",lm,le) end)
+ (fun a -> update_stack a
+ (add_to_top_frame
+ (fun v -> E_aux (E_vector_update v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (to_exp vup)) (l,annot)))))
+ (fun a -> update_stack a
+ (add_to_top_frame (fun e -> E_aux (E_vector_update vec
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ e) (l,annot))))
+ | _ -> (Error l "Update of vector requires number for access",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) (l,annot))))
| E_vector_update_subrange vec i1 i2 exp ->
resolve_outcome (interp_main t_level l_env l_mem i1)
(fun vi1 lm le ->
match vi1 with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
resolve_outcome
(interp_main t_level l_env lm i2)
(fun vi2 lm le ->
match vi2 with
- | V_lit (L_num n2) ->
+ | V_lit (L_aux (L_num n2) ln2) ->
resolve_outcome (interp_main t_level l_env lm exp)
(fun v_rep lm le ->
(resolve_outcome
@@ -724,90 +890,131 @@ and interp_main t_level l_env l_mem exp =
(fun vvec lm le ->
match vvec with
| V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
- | _ -> (Error "Vector update requires vector",lm,le) end)
+ | _ -> (Error l "Vector update requires vector",lm,le) end)
(fun a -> update_stack a
- (add_to_top_frame (fun v -> E_vector_update_subrange v (E_lit (L_num n1)) (E_lit (L_num n2)) (to_exp v_rep))))))
+ (add_to_top_frame
+ (fun v -> E_aux (E_vector_update_subrange v
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))
+ (to_exp v_rep)) (l,annot))))))
(fun a -> update_stack a
- (add_to_top_frame (fun e -> E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e)))
- | _ -> (Error "vector update requires number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i2 -> E_vector_update_subrange vec (to_exp vi1) i2 exp)))
- | _ -> (Error "vector update requires number",lm,le) end)
- (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_vector_update_subrange vec i1 i2 exp)))
+ (add_to_top_frame
+ (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) (l,annot))))
+ | _ -> (Error l "vector update requires number",lm,le) end)
+ (fun a ->
+ update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) (l,annot))))
+ | _ -> (Error l "vector update requires number",lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot))))
| E_tuple(exps) ->
- exp_list t_level E_tuple V_tuple l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
- exp_list t_level E_vector (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
+ exp_list t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
| E_vector_indexed(iexps) ->
let (indexes,exps) = List.unzip iexps in
- exp_list t_level (fun es -> (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)))
- (fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps
+ let is_inc = match typ with
+ | T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
+ | _ -> false end in
+ exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot)))
+ (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
| E_block(exps) -> interp_block t_level l_env l_env l_mem exps
| E_app f args ->
- (match (exp_list t_level (fun es -> E_app f es) (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] args) with
+ (match (exp_list t_level (fun es -> E_aux (E_app f es) (l,annot))
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] args) with
| (Value v,lm,le) ->
- (match (f,t_level) with
- | (id,(Env defs externs lets regs mems ctors)) ->
- (match find_function defs id with
- | Just(funcls) ->
- (match find_funcl funcls v with
- | Nothing ->
- let name = get_id id in
- (Error (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
- | Just(env,exp) ->
- resolve_outcome (interp_main t_level env l_mem exp)
- (fun ret lm le -> (Value ret, lm,l_env))
- (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
+ let name = get_id f in
+ (match tag with
+ | Tag_empty ->
+ (match find_function defs f with
+ | Just(funcls) ->
+ (match find_funcl funcls v with
+ | Nothing ->
+ (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
+ | Just(env,exp) ->
+ resolve_outcome (interp_main t_level env l_mem exp)
+ (fun ret lm le -> (Value ret, lm,l_env))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
end)
- | Nothing ->
- (match in_ctors ctors id with
- | Just(typ) -> (Value (V_ctor id v), lm, le)
- | Nothing ->
- (match find_memory mems id with
- | Just(typ) ->
- (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
- | Nothing ->
- (match find_extern externs id with
- | Just(str) ->
- (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
- | Nothing -> (Error (String.stringAppend "Unknown function call " (get_id id)),lm,le) end)
- end) end) end) end)
- | out -> out end)
- | E_app_infix l op r ->
+ | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
+ | Tag_spec ->
+ (match find_function defs f with
+ | Just(funcls) ->
+ (match find_funcl funcls v with
+ | Nothing ->
+ (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
+ | Just(env,exp) ->
+ resolve_outcome (interp_main t_level env l_mem exp)
+ (fun ret lm le -> (Value ret, lm,l_env))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+ end)
+ | Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
+ | Tag_ctor ->
+ (match in_ctors ctors f with
+ | Just(_) -> (Value (V_ctor f typ v), lm, le)
+ | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
+ end)
+ | Tag_extern opt_name ->
+ let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
+ if has_memory_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end)
+ then
+ (Action (Read_mem (id_of_string name_ext) v Nothing)
+ (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top), lm, le)
+ else
+ (Action (Call_extern name_ext v)
+ (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top), lm, le)
+ | _ -> (Error l (String.stringAppend "Tag other than empty, spec, ctor, or extern on function call " name),lm,le) end)
+ | out -> out end)
+ | E_app_infix lft op r ->
let op = match op with
- | Id x -> DeIid x
- | DeIid _ -> op
+ | Id_aux (Id x) il -> Id_aux (DeIid x) il
+ | _ -> op
end in
- resolve_outcome (interp_main t_level l_env l_mem l)
+ let name = get_id op in
+ resolve_outcome (interp_main t_level l_env l_mem lft)
(fun lv lm le ->
resolve_outcome (interp_main t_level l_env lm r)
(fun rv lm le ->
- (match t_level with
- | (Env defs externs lets regs mems ctors) ->
+ match tag with
+ | Tag_empty ->
(match find_function defs op with
- | Nothing ->
- (match find_extern externs op with
- | Just(str) ->
- (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le)
- | Nothing ->
- (Error (String.stringAppend
- "No matching function "
- (get_id op)),lm,l_env) end)
- | Just (funcls) ->
+ | Nothing -> (Error l (String.stringAppend "Internal error, no function def for " name),lm,le)
+ | Just (funcls) ->
(match find_funcl funcls (V_tuple [lv;rv]) with
- | Nothing -> (Error "No matching pattern for function",lm,l_env)
+ | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
| Just(env,exp) ->
resolve_outcome (interp_main t_level env emem exp)
- (fun ret lm le -> (Value ret,l_mem,l_env))
- (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
- end)
- end)
- end))
- (fun a -> update_stack a (add_to_top_frame (fun r -> (E_app_infix (to_exp lv) op r)))))
- (fun a -> update_stack a (add_to_top_frame (fun l -> (E_app_infix l op r))))
- | E_let lbind exp ->
+ (fun ret lm le -> (Value ret,l_mem,l_env))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (Id_aux (Id "0") l)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+ end)end)
+ | Tag_spec ->
+ (match find_function defs op with
+ | Nothing -> (Error l (String.stringAppend "No function definition found for " name),lm,le)
+ | Just (funcls) ->
+ (match find_funcl funcls (V_tuple [lv;rv]) with
+ | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
+ | Just(env,exp) ->
+ resolve_outcome (interp_main t_level env emem exp)
+ (fun ret lm le -> (Value ret,l_mem,l_env))
+ (fun a -> update_stack a
+ (fun stack -> (Frame (Id_aux (Id "0") l)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+ end)end)
+ | Tag_extern ext_name ->
+ let ext_name = match ext_name with Just s -> s | Nothing -> name end in
+ (Action (Call_extern ext_name (V_tuple [lv;rv]))
+ (Frame (Id_aux (Id "0") l)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top),lm,le) end)
+ (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) (l,annot)))))
+ (fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot)))))
+ | E_let (lbind : letbind tannot) exp ->
match (interp_letbind t_level l_env l_mem lbind) with
| ((Value v,lm,le),_) -> interp_main t_level le lm exp
- | (((Action a s as o),lm,le),Just lbuild) -> ((update_stack o (add_to_top_frame (fun e -> (E_let (lbuild e) exp)))),lm,le)
+ | (((Action a s as o),lm,le),Just lbuild) ->
+ ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) (l,annot))))),lm,le)
| (e,_) -> e end
| E_assign lexp exp ->
resolve_outcome (interp_main t_level l_env l_mem exp)
@@ -823,98 +1030,123 @@ and interp_main t_level l_env l_mem exp =
(Action (Write_reg regf range value) stack)
| (Action (Write_mem id a range value) stack) ->
(Action (Write_mem id a range value) stack)
- | _ -> update_stack a (add_to_top_frame (fun e -> (E_assign (lexp_builder e) (to_exp v)))) end))
+ | _ -> update_stack a (add_to_top_frame
+ (fun e -> (E_aux (E_assign (lexp_builder e) (to_exp v)) (l,annot)) )) end))
end))
- (fun a -> update_stack a (add_to_top_frame (fun v -> (E_assign lexp v))))
+ (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) (l,annot)))))
end
and interp_block t_level init_env local_env local_mem exps =
match exps with
- | [ ] -> (Value (V_lit (L_unit)), local_mem, init_env)
+ | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
| [ exp ] -> interp_main t_level local_env local_mem exp
| exp:: exps ->
resolve_outcome (interp_main t_level local_env local_mem exp)
(fun _ lm le -> interp_block t_level init_env le lm exps)
- (fun a -> update_stack a (add_to_top_frame (fun e -> E_block(e::exps))))
+ (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (Unknown,Nothing)))))
end
-and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
+and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
let (Env defs externs lets regs mems ctors) = t_level in
+ let (typ,tag,ncs,ef) = match annot with
+ | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+ | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
match lexp with
| LEXP_id id ->
- match in_env l_env id with
- | Just (V_boxref n) ->
- if is_top_level
- then ((Value (V_lit L_unit), update_mem l_mem n value, l_env),Nothing)
- else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_id id))
- | Just v -> if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e -> LEXP_id id))
- | Nothing ->
- match in_reg regs id with
- | Just regf -> let request = (Action (Write_reg regf Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env) in
- if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_id id))
- | Nothing ->
- if is_top_level
- then begin
- let (Mem c m) = l_mem in
- let l_mem = (Mem (c+1) m) in
- ((Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing)
- end
- else ((Error "Undefined id",l_mem,l_env),Nothing)
- end
+ match tag with
+ | Tag_empty ->
+ match in_env l_env id with
+ | Just (V_boxref n t) ->
+ if is_top_level
+ then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+ else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+ | Just v ->
+ if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
+ else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
+ | Nothing ->
+ if is_top_level
+ then begin
+ let (Mem c m) = l_mem in
+ let l_mem = (Mem (c+1) m) in
+ ((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+ end
+ else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+ end
+ | Tag_extern _ ->
+ let regf = Reg id typ in
+ let request = (Action (Write_reg regf Nothing value)
+ (Frame (Id_aux (Id "0") l)
+ (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
+ if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+ | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
end
| LEXP_memory id exps ->
- match (exp_list t_level E_tuple (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] exps) with
+ match (exp_list t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing))
+ (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
+ l_env l_mem [] exps) with
| (Value v,lm,le) ->
- let request = (Action (Write_mem id v Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
- if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end))))
- | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es)))
+ (match tag with
+ | Tag_extern ->
+ let request = (Action (Write_mem id v Nothing value)
+ (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env lm Top),lm,l_env) in
+ if is_top_level then (request,Nothing)
+ else (request,Just (fun e ->
+ (LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) (l,annot))))
+ end)
+ | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
| e -> (e,Nothing) end
| LEXP_vector lexp exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value i,lm,le) ->
(match i with
- | V_lit (L_num n) ->
- let next_builder le_builder = (fun e -> LEXP_vector (le_builder e) (E_lit (L_num n))) in
+ | V_lit (L_aux (L_num n) ln) ->
+ let next_builder le_builder = (fun e ->
+ LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in
(match (create_write_message_or_update t_level value l_env lm false lexp) with
| ((Value v,lm,le),maybe_builder) ->
(match v with
| V_vector inc m vs ->
let nth = access_vector v n in
(match (nth,is_top_level,maybe_builder) with
- | (V_boxref n,true,_) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
- | (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),Nothing)
- | ((V_boxref n),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+ | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+ | (v,true,_) -> ((Error l "Vector does not contain reg values",lm,l_env),Nothing)
+ | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
| (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
- | _ -> ((Error "Vector access of non-vector",lm,l_env),Nothing) end)
+ | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end)
| ((Action a s,lm,le),Just lexp_builder) ->
(match (a,is_top_level) with
| ((Write_reg regf Nothing value),true) -> ((Action (Write_reg regf (Just (n,n)) value) s, lm,le), Nothing)
- | ((Write_reg regf Nothing value),false) -> ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+ | ((Write_reg regf Nothing value),false) ->
+ ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
- | ((Write_mem id a Nothing value),false) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+ | ((Write_mem id a Nothing value),false) ->
+ ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
| _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
| e -> e end)
- | _ -> ((Error "Vector access must be a number",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_vector lexp e)))
+ | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end)
+ | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) (l,annot))))
| e -> (e,Nothing) end
| LEXP_vector_range lexp exp1 exp2 ->
match (interp_main t_level l_env l_mem exp1) with
| (Value i1, lm, le) ->
(match i1 with
- | V_lit (L_num n1) ->
+ | V_lit (L_aux (L_num n1) ln1) ->
(match (interp_main t_level l_env l_mem exp2) with
| (Value i2,lm,le) ->
(match i2 with
- | V_lit (L_num n2) ->
- let next_builder le_builder = (fun e -> LEXP_vector_range (le_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))) in
+ | V_lit (L_aux (L_num n2) ln2) ->
+ let next_builder le_builder =
+ (fun e -> LEXP_aux (LEXP_vector_range (le_builder e)
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in
(match (create_write_message_or_update t_level value l_env lm false lexp) with
| ((Value v,lm,le), Just lexp_builder) ->
(match (v,is_top_level) with
| (V_vector m inc vs,true) ->
- ((Value (V_lit L_unit), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
+ ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
| (V_vector m inc vs,false) ->
((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
- | _ -> ((Error "Vector required",lm,le),Nothing) end)
+ | _ -> ((Error l "Vector required",lm,le),Nothing) end)
| ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
((Action (Write_reg regf (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
| ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
@@ -922,63 +1154,66 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
| ((Action a s,lm,le), Just lexp_builder) ->
((Action a s,lm,le), Just (next_builder lexp_builder))
| e -> e end)
- | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
+ | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
| (Action a s,lm,le) ->
- ((Action a s,lm, le), Just (fun e -> LEXP_vector_range lexp (E_lit (L_num n1)) e))
+ ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp
+ (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+ e) (l,annot)))
| e -> (e,Nothing) end)
- | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
+ | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
| (Action a s,lm,le) ->
- ((Action a s, lm,le), Just (fun e -> LEXP_vector_range lexp e exp2))
+ ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot)))
| e -> (e,Nothing) end
| LEXP_field lexp id ->
(match (create_write_message_or_update t_level value l_env l_mem false lexp) with
- | ((Value (V_record fexps),lm,le),Just lexp_builder) ->
+ | ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
match (in_env fexps id,is_top_level) with
- | (Just (V_boxref n),true) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
- | (Just (V_boxref n),false) -> ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
- | (Just v, true) -> ((Error "Field access requires record",lm,le),Nothing)
- | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
- | (Nothing,_) -> ((Error "Field not found in specified record",lm,le),Nothing) end
+ | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+ | (Just (V_boxref n t),false) ->
+ ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+ | (Just v, true) -> ((Error l "Field access requires record",lm,le),Nothing)
+ | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+ | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
| ((Action a s,lm,le), Just lexp_builder) ->
match a with
- | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
- | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
- | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
- | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
+ | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+ | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+ | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+ | _ -> ((Error l "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
end
| e -> e end)
end
-and interp_letbind t_level l_env l_mem lbind =
+and interp_letbind t_level l_env l_mem (LB_aux lbind (l,annot)) =
match lbind with
| LB_val_explicit t pat exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value v,lm,le) ->
(match match_pattern pat v with
- | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
- | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_explicit t pat e)))
+ | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+ | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
+ | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot)))))
| e -> (e,Nothing) end
| LB_val_implicit pat exp ->
match (interp_main t_level l_env l_mem exp) with
| (Value v,lm,le) ->
(match match_pattern pat v with
- | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
- | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
- | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_implicit pat e)))
+ | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+ | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
+ | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
| e -> (e,Nothing) end
end
let rec to_global_letbinds (Defs defs) t_level =
let (Env defs' externs lets regs mems ctors) = t_level in
match defs with
- | [] -> ((Value (V_lit L_unit), emem, []),t_level)
- | def ::defs ->
+ | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, []),t_level)
+ | (DEF_aux def (l,_))::defs ->
match def with
| DEF_val lbind ->
match interp_letbind t_level [] emem lbind with
| ((Value v,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' externs (lets++le) regs mems ctors)
- | ((Action a s,lm,le),_) -> ((Error "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
+ | ((Action a s,lm,le),_) -> ((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
| (e,_) -> (e,t_level) end
| _ -> to_global_letbinds (Defs defs) t_level
end
@@ -998,7 +1233,7 @@ let interp defs exp =
let rec resume_main t_level stack value =
match stack with
- | Top -> Error "Top hit without place to put value"
+ | Top -> Error Unknown "Top hit without place to put value"
| Frame id exp env mem Top ->
match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end
| Frame id exp env mem stack ->
@@ -1006,7 +1241,7 @@ let rec resume_main t_level stack value =
| Value v ->
match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end
| Action action stack -> Action action (Frame id exp env mem stack)
- | Error s -> Error s
+ | Error l s -> Error l s
end
end
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index aeb81085..b18d031e 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -8,51 +8,51 @@ open import Word
let compose f g x = f (V_tuple [g x]) ;;
-let is_one (V_lit b) = V_lit (if b = L_one then L_true else L_false) ;;
+let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
-let eq (V_tuple [x; y]) = V_lit (if x = y then L_true else L_false) ;;
+let eq (V_tuple [x; y]) = V_lit (L_aux (if x = y then L_true else L_false) Unknown) ;;
-let neg (V_tuple [V_lit arg]) = V_lit (match arg with
+let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
| L_true -> L_false
- | L_false -> L_true end) ;;
+ | L_false -> L_true end) la) ;;
let neq = compose neg eq ;;
let bit_to_bool b = match b with
- V_lit L_zero -> false
- | V_lit L_one -> true
+ V_lit (L_aux L_zero _) -> false
+ | V_lit (L_aux L_one _) -> true
end ;;
let bool_to_bit b = match b with
- false -> V_lit L_zero
- | true -> V_lit L_one
+ false -> V_lit (L_aux L_zero Unknown)
+ | true -> V_lit (L_aux L_one Unknown)
end ;;
(* XXX always interpret as positive ? *)
let to_num_dec (V_vector idx false l) =
- V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l)))));;
+ V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
let to_num_inc (V_vector idx true l) =
- V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l))));;
+ V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;
(* XXX not quite sure about list reversal here - what is the convention for
* V_vector? cf. above too *)
-let to_vec_dec len (V_lit(L_num n)) =
- let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
+ let (BitSeq _ false l) = bitSeqFromNatural len n in
V_vector 0 false (map bool_to_bit (reverse l)) ;;
-let to_vec_inc len (V_lit(L_num n)) =
- let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
+ let (BitSeq _ false l) = bitSeqFromNatural len n in
V_vector 0 true (map bool_to_bit l) ;;
let rec add (V_tuple args) = match args with
(* vector case *)
| [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
- let V_lit (L_num x) = (if d then to_num_inc else to_num_dec) v in
- let V_lit (L_num y) = (if d' then to_num_inc else to_num_dec) v' in
+ let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
+ let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
(* XXX how shall I decide this? max? max+1? *)
let len = max (List.length l) (List.length l') in
(* XXX assume d = d' *)
- (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_num (x+y)))
+ (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_aux (L_num (x+y)) lx))
(* integer case *)
- | [V_lit(L_num x); V_lit(L_num y)] -> V_lit(L_num (x+y))
+ | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
(* assume other literals are L_bin or L_hex, ie. vectors *)
| [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
| [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 98b8e6fe..19c27b56 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -19,18 +19,26 @@ let lit_to_string = function
;;
let id_to_string = function
- | Id s | DeIid s -> s
+ | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
+;;
+
+let loc_to_string = function
+ | Unknown -> "Unknown"
+ | Trans(s,_) -> s
+ | Range(s,fline,fchar,tline,tchar) ->
+ "in " ^ s ^ " from line " ^ (string_of_int fline) ^ " character " ^ (string_of_int fchar) ^
+ " to line " ^ (string_of_int tline) ^ " character " ^ (string_of_int tchar)
;;
let bitvec_to_string l = "0b" ^ (String.concat "" (List.map (function
- | V_lit(L_zero) -> "0"
- | V_lit(L_one) -> "1"
+ | V_lit(L_aux(L_zero, _)) -> "0"
+ | V_lit(L_aux(L_one, _)) -> "1"
| _ -> assert false) l))
;;
let rec val_to_string = function
- | V_boxref n -> sprintf "boxref %d" n
- | V_lit l -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
+ | V_boxref(n, t) -> sprintf "boxref %d" n
+ | V_lit (L_aux(l,_)) -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
| V_tuple l ->
let repr = String.concat ", " (List.map val_to_string l) in
sprintf "tuple <%s>" repr
@@ -43,11 +51,11 @@ let rec val_to_string = function
try bitvec_to_string l
with Failure _ -> String.concat "; " (List.map val_to_string l) in
sprintf "vector [%s] (%s, from %s)" repr order (string_of_big_int first_index)
- | V_record l ->
+ | V_record(_, l) ->
let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string value) in
let repr = String.concat "; " (List.map pp l) in
sprintf "record {%s}" repr
- | V_ctor (id, value) ->
+ | V_ctor (id,_, value) ->
sprintf "constructor %s %s" (id_to_string id) (val_to_string value)
;;
@@ -82,15 +90,22 @@ let act_to_string = function
sprintf "extern call %s applied to %s" name (val_to_string arg)
;;
+let id_compare i1 i2 =
+ match (i1, i2) with
+ | (Id_aux(Id(i1),_),Id_aux(Id(i2),_))
+ | (Id_aux(Id(i1),_),Id_aux(DeIid(i2),_))
+ | (Id_aux(DeIid(i1),_),Id_aux(Id(i2),_))
+ | (Id_aux(DeIid(i1),_),Id_aux(DeIid(i2),_)) -> compare i1 i2
+
module Reg = struct
- include Map.Make(struct type t = id let compare = compare end)
+ include Map.Make(struct type t = id let compare = id_compare end)
end ;;
module Mem = struct
include Map.Make(struct
type t = (id * big_int)
let compare (i1, v1) (i2, v2) =
- match compare i1 i2 with
+ match id_compare i1 i2 with
| 0 -> compare_big_int v1 v2
| n -> n
end)
@@ -114,22 +129,22 @@ let vconcat v v' = vec_concat (V_tuple [v; v']) ;;
let perform_action ((reg, mem) as env) = function
| Read_reg ((Reg (id, _) | SubReg (id, _, _)), sub) ->
slice (Reg.find id reg) sub, env
- | Read_mem (id, V_lit(L_num n), sub) ->
+ | Read_mem (id, V_lit(L_aux((L_num n),_)), sub) ->
slice (Mem.find (id, n) mem) sub, env
| Write_reg ((Reg (id, _) | SubReg (id, _, _)), None, value) ->
- V_lit L_unit, (Reg.add id value reg, mem)
+ V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id value reg, mem)
| Write_reg ((Reg (id, _) | SubReg (id, _, _)), Some (start, stop), value) ->
(* XXX if updating a single element, wrap value into a vector -
* should the typechecker do that coercion for us automatically? *)
let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
let old_val = Reg.find id reg in
let new_val = fupdate_vector_slice old_val value start stop in
- V_lit L_unit, (Reg.add id new_val reg, mem)
- | Write_mem (id, V_lit(L_num n), None, value) ->
- V_lit L_unit, (reg, Mem.add (id, n) value mem)
+ V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id new_val reg, mem)
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) ->
+ V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) value mem)
(* multi-byte accesses to memory *)
(* XXX this doesn't deal with endianess at all *)
- | Read_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], sub) ->
+ | Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], sub) ->
let rec fetch k acc =
if eq_big_int k size then slice acc sub else
let slice = Mem.find (id, add_big_int n k) mem in
@@ -139,7 +154,7 @@ let perform_action ((reg, mem) as env) = function
(* XXX no support for multi-byte slice write at the moment - not hard to add,
* but we need a function basic read/write first since slice access involves
* read, fupdate, write. *)
- | Write_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], None, V_vector (m, inc, vs)) ->
+ | Write_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, V_vector (m, inc, vs)) ->
(* normalize input vector so that it is indexed from 0 - for slices *)
let value = V_vector (zero_big_int, inc, vs) in
(* assumes smallest unit of memory is 8 bit *)
@@ -151,15 +166,15 @@ let perform_action ((reg, mem) as env) = function
let slice = slice_vector value n1 n2 in
let mem' = Mem.add (id, add_big_int n k) slice mem in
update (succ_big_int k) mem'
- in V_lit L_unit, (reg, update zero_big_int mem)
+ in V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, update zero_big_int mem)
(* This case probably never happens in the POWER spec anyway *)
- | Write_mem (id, V_lit(L_num n), Some (start, stop), value) ->
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), Some (start, stop), value) ->
(* XXX if updating a single element, wrap value into a vector -
* should the typechecker do that coercion for us automatically? *)
let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
let old_val = Mem.find (id, n) mem in
let new_val = fupdate_vector_slice old_val value start stop in
- V_lit L_unit, (reg, Mem.add (id, n) new_val mem)
+ V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) new_val mem)
| Call_extern (name, arg) -> eval_external name arg, env
| _ -> assert false
;;
@@ -174,8 +189,8 @@ let run (name, test) =
let return, env' = perform_action env a in
eprintf "%s: action returned %s\n" name (val_to_string return);
loop env' (resume test s return)
- | Error e -> eprintf "%s: error: %s\n" name e; false in
- let entry = E_app((Id "main"), [E_lit L_unit]) in
+ | Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false in
+ let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in
eprintf "%s: starting\n" name;
try
Printexc.record_backtrace true;
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 22:00:03 +0000