diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 10 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 841 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 36 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 57 | ||||
| -rw-r--r-- | src/pretty_print.ml | 525 | ||||
| -rw-r--r-- | src/process_file.ml | 1 | ||||
| -rw-r--r-- | src/test/vectors.sail | 7 | ||||
| -rw-r--r-- | src/type_check.ml | 31 | ||||
| -rw-r--r-- | src/type_internal.ml | 37 | ||||
| -rw-r--r-- | src/type_internal.mli | 3 |
10 files changed, 978 insertions, 570 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index e7b92019..ed4a0208 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -530,17 +530,17 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = | Parse_ast.Rec_rec -> Rec_rec ),l) -let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t * kind Envmap.t= +let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot_opt * kind Envmap.t * kind Envmap.t= match tp with | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none") | Parse_ast.Typ_annot_opt_some(tq,typ) -> let typq,k_env,k_local = to_ast_typquant k_env tq in - Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local + Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),l),k_env,k_local -let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : tannot effect_opt = +let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : effect_opt = match e with - | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,(l,None)) - | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),(l,None)) + | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l) + | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l) let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) = match fcl with 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; diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 236bfc91..4190ad9b 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1,3 +1,4 @@ +open Type_internal open Ast open Format @@ -349,86 +350,115 @@ let pp_defs ppf (Defs(defs)) = (**************************************************************************** - * source to Lem ast pretty printer + * annotated source to Lem ast pretty printer ****************************************************************************) -let pp_format_id_lem (Id_aux(i,_)) = - match i with - | Id(i) -> "(Id \"" ^ i ^ "\")" - | DeIid(x) -> "(DeIid \"" ^ x ^ "\")" +let rec pp_format_l_lem = function + | Parse_ast.Unknown -> "Unknown" + | Parse_ast.Trans(s,None) -> "(Trans \"" ^ s ^ "\" Nothing)" + | Parse_ast.Trans(s,(Some l)) -> "(Trans \"" ^ s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))" + | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^ + (string_of_int p1.Lexing.pos_lnum) ^ " " ^ + (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^ + (string_of_int p2.Lexing.pos_lnum) ^ " " ^ + (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")" + +let pp_lem_l ppf l = base ppf (pp_format_l_lem l) + +let pp_format_id_lem (Id_aux(i,l)) = + "(Id_aux " ^ + (match i with + | Id(i) -> "(Id \"" ^ i ^ "\")" + | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_id ppf id = base ppf (pp_format_id_lem id) -let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")" +let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")" let pp_lem_var ppf var = base ppf (pp_format_var_lem var) -let pp_format_bkind_lem (BK_aux(k,_)) = - match k with - | BK_type -> "BK_type" - | BK_nat -> "BK_nat" - | BK_order -> "BK_order" - | BK_effect -> "BK_effect" +let pp_format_bkind_lem (BK_aux(k,l)) = + "(BK_aux " ^ + (match k with + | BK_type -> "BK_type" + | BK_nat -> "BK_nat" + | BK_order -> "BK_order" + | BK_effect -> "BK_effect") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) -let pp_format_kind_lem (K_aux(K_kind(klst),_)) = - "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])" +let pp_format_kind_lem (K_aux(K_kind(klst),l)) = + "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")" let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k) -let rec pp_format_typ_lem (Typ_aux(t,_)) = - match t with - | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")" - | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")" - | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ - pp_format_typ_lem ret ^ " " ^ - (pp_format_effects_lem efct) ^ ")" - | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])" - | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])" - | Typ_wild -> "Typ_wild" -and pp_format_nexp_lem (Nexp_aux(n,_)) = - match n with - | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" - | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")" - | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" - | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" - | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")" -and pp_format_ord_lem (Ord_aux(o,_)) = - match o with - | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" - | Ord_inc -> "Ord_inc" - | Ord_dec -> "Ord_dec" -and pp_format_effects_lem (Effect_aux(e,_)) = - match e with +let rec pp_format_typ_lem (Typ_aux(t,l)) = + "(Typ_aux " ^ + (match t with + | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")" + | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")" + | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ + pp_format_typ_lem ret ^ " " ^ + (pp_format_effects_lem efct) ^ ")" + | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])" + | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])" + | Typ_wild -> "Typ_wild") ^ " " ^ + (pp_format_l_lem l) ^ ")" +and pp_format_nexp_lem (Nexp_aux(n,l)) = + "(Nexp_aux " ^ + (match n with + | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" + | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")" + | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" + | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" + | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^ + (pp_format_l_lem l) ^ ")" +and pp_format_ord_lem (Ord_aux(o,l)) = + "(Ord_aux " ^ + (match o with + | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" + | Ord_inc -> "Ord_inc" + | Ord_dec -> "Ord_dec") ^ " " ^ + (pp_format_l_lem l) ^ ")" +and pp_format_base_effect_lem (BE_aux(e,l)) = + "(BE_aux " ^ + (match e with + | BE_rreg -> "BE_rreg" + | BE_wreg -> "BE_wreg" + | BE_rmem -> "BE_rmem" + | BE_wmem -> "BE_wmem" + | BE_undef -> "BE_undef" + | BE_unspec -> "BE_unspec" + | BE_nondet -> "BE_nondet") ^ " " ^ + (pp_format_l_lem l) ^ ")" +and pp_format_effects_lem (Effect_aux(e,l)) = + "(Effect_aux " ^ + (match e with | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")" | Effect_set(efcts) -> "(Effect_set [" ^ - (list_format "; " - (fun (BE_aux(e,l)) -> - match e with - | BE_rreg -> "BE_rreg" - | BE_wreg -> "BE_wreg" - | BE_rmem -> "BE_rmem" - | BE_wmem -> "BE_wmem" - | BE_undef -> "BE_undef" - | BE_unspec -> "BE_unspec" - | BE_nondet -> "BE_nondet") - efcts) ^ " ])" -and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = - match t with + (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^ + (pp_format_l_lem l) ^ ")" +and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = + "(Typ_arg_aux " ^ + (match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")" - | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")" + | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t) let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n) let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o) let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e) +let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be) -let pp_format_nexp_constraint_lem (NC_aux(nc,_)) = - match nc with +let pp_format_nexp_constraint_lem (NC_aux(nc,l)) = + "(NC_aux " ^ + (match nc with | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" @@ -436,38 +466,46 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) = pp_format_var_lem id ^ " [" ^ list_format "; " string_of_int bounds ^ - "])" + "])") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc) -let pp_format_qi_lem (QI_aux(qi,_)) = - match qi with +let pp_format_qi_lem (QI_aux(qi,lq)) = + "(QI_aux " ^ + (match qi with | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")" - | QI_id(KOpt_aux(ki,_)) -> - "(QI_id " ^ + | QI_id(KOpt_aux(ki,lk)) -> + "(QI_id (KOpt_aux " ^ (match ki with | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")" - | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")" + | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^ + (pp_format_l_lem lk) ^ "))") ^ " " ^ + (pp_format_l_lem lq) ^ ")" let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi) -let pp_format_typquant_lem (TypQ_aux(tq,_)) = - match tq with +let pp_format_typquant_lem (TypQ_aux(tq,l)) = + "(TypQ_aux " ^ + (match tq with | TypQ_no_forall -> "TypQ_no_forall" | TypQ_tq(qlist) -> "(TypQ_tq [" ^ (list_format "; " pp_format_qi_lem qlist) ^ - "])" + "])") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq) -let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) = - "(TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ")" +let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) = + "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts) -let pp_format_lit_lem (L_aux(l,_)) = - match l with +let pp_format_lit_lem (L_aux(lit,l)) = + "(L_aux " ^ + (match lit with | L_unit -> "L_unit" | L_zero -> "L_zero" | L_one -> "L_one" @@ -477,12 +515,81 @@ let pp_format_lit_lem (L_aux(l,_)) = | L_hex(n) -> "(L_hex \"" ^ n ^ "\")" | L_bin(n) -> "(L_bin \"" ^ n ^ "\")" | L_undef -> "L_undef" - | L_string(s) -> "(L_string \"" ^ s ^ "\")" + | L_string(s) -> "(L_string \"" ^ s ^ "\")") ^ " " ^ + (pp_format_l_lem l) ^ ")" let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l) -let rec pp_format_pat_lem (P_aux(p,l)) = - match p with + +let rec pp_format_t t = + match t.t with + | Tid i -> "(T_id (Id_aux (Id \"" ^ i ^ "\") Unknown))" + | Tvar i -> "(T_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" + | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")" + | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])" + | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^ list_format "; " pp_format_targ args ^ "]))" + | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))" +and pp_format_targ = function + | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")" + | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")" + | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")" + | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")" +and pp_format_n n = + match n.nexp with + | Nvar i -> "(Ne_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" + | Nconst i -> "(Ne_const " ^ string_of_int i ^ ")" + | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])" + | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" + | N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")" + | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")" + | Nuvar(_) -> "(Ne_var (Kid_aux (Var \"fresh_v\") Unknown))" +and pp_format_e e = + "(Effect_aux " ^ + (match e.effect with + | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" + | Eset es -> "(Effect_set [" ^ + (list_format "; " pp_format_base_effect_lem es) ^ " ])" + | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))") + ^ " Unknown)" +and pp_format_o o = + "(Ord_aux " ^ + (match o.order with + | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" + | Oinc -> "Ord_inc" + | Odec -> "Ord_dec" + | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))") + ^ " Unknown)" + +let pp_format_tag = function + | Emp -> "Tag_empty" + | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" + | External None -> "(Tag_extern Nothing)" + | Default -> "Tag_default" + | Constructor -> "Tag_ctor" + | Enum -> "Tag_enum" + | Spec -> "Tag_spec" + +let pp_format_nes nes = + "[" ^ + (list_format "; " + (fun ne -> match ne with + | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" + | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" + | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" + | In(_,i,ns) -> "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])") + nes) ^ "]" + +let pp_format_annot = function + | None -> "Nothing" + | Some((_,t),tag,nes,efct) -> + "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))" + +let pp_annot ppf ant = base ppf (pp_format_annot ant) + + +let rec pp_format_pat_lem (P_aux(p,(l,annot))) = + "(P_aux " ^ + (match p with | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")" | P_wild -> "P_wild" | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")" @@ -499,156 +606,182 @@ let rec pp_format_pat_lem (P_aux(p,l)) = "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])" | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])" - | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])" + | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ + " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))" let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p) -let rec pp_lem_let ppf (LB_aux(lb,_)) = - match lb with - | LB_val_explicit(ts,pat,exp) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp - | LB_val_implicit(pat,exp) -> - fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp - -and pp_lem_exp ppf (E_aux(e,_)) = - match e with - | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" +let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) = + let print_lb ppf lb = + match lb with + | LB_val_explicit(ts,pat,exp) -> + fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp + | LB_val_implicit(pat,exp) -> + fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in + fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot + +and pp_lem_exp ppf (E_aux(e,(l,annot))) = + let print_e ppf e = + match e with + | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_block" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" - | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id - | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit - | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp - | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args - | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r - | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" - | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e - | E_for(id,exp1,exp2,exp3,order,exp4) -> - fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" - kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 - | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps - | E_vector_indexed(iexps) -> - let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in - let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in - fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps - | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e - | E_vector_subrange(v,e1,e2) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 - | E_vector_update(v,e1,e2) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 - | E_vector_update_subrange(v,e1,e2,e3) -> - fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 - | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps - | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2 - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> - fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps - | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) -> - fprintf ppf "@[<0>(%a %a (%a [%a]))@]" - kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps - | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id - | E_case(exp,pexps) -> - fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps - | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp - | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp + | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id + | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit + | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp + | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args + | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r + | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" + | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e + | E_for(id,exp1,exp2,exp3,order,exp4) -> + fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" + kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 + | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps + | E_vector_indexed(iexps) -> + let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in + let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in + fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps + | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e + | E_vector_subrange(v,e1,e2) -> + fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 + | E_vector_update(v,e1,e2) -> + fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 + | E_vector_update_subrange(v,e1,e2,e3) -> + fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 + | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps + | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2 + | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps + | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) -> + fprintf ppf "@[<0>(%a %a (%a [%a]))@]" + kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps + | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id + | E_case(exp,pexps) -> + fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps + | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp + | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp + in + fprintf ppf "@[<0>(E_aux %a (%a, %a))@]" print_e e pp_lem_l l pp_annot annot and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";" -and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp +and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = + fprintf ppf "@[<1>(FE_aux (%a %a %a) (%a, %a))@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";" -and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = - fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp +and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = + fprintf ppf "@[<1>(Pat_aux (%a %a@ %a) (%a, %a))@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";" -and pp_lem_lexp ppf (LEXP_aux(lexp,_)) = - match lexp with - | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id - | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args - | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp - | LEXP_vector_range(v,e1,e2) -> - fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2 - | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id - -let pp_lem_default ppf (DT_aux(df,_)) = - match df with - | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var - | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id - -let pp_lem_spec ppf (VS_aux(v,_)) = - match v with - | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id - | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s - | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id - -let pp_lem_namescm ppf (Name_sect_aux(ns,_)) = +and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) = + let print_le ppf lexp = + match lexp with + | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id + | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args + | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp + | LEXP_vector_range(v,e1,e2) -> + fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2 + | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id + in + fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot + +let pp_lem_default ppf (DT_aux(df,(l,annot))) = + let print_de ppf df = + match df with + | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var + | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id + in + fprintf ppf "@[<0>(DT_aux %a (%a, %a))@]" print_de df pp_lem_l l pp_annot annot + +let pp_lem_spec ppf (VS_aux(v,(l,annot))) = + let print_spec ppf v = + match v with + | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id + | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s + | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id + in + fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot + +let pp_lem_namescm ppf (Name_sect_aux(ns,l)) = match ns with - | Name_sect_none -> fprintf ppf "Name_sect_none" - | Name_sect_some(s) -> fprintf ppf "(%a \"%s\")" kwd "Name_sect_some" s + | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l + | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l -let rec pp_lem_range ppf (BF_aux(r,_)) = +let rec pp_lem_range ppf (BF_aux(r,l)) = match r with - | BF_single(i) -> fprintf ppf "(BF_single %i)" i - | BF_range(i1,i2) -> fprintf ppf "(BF_range %i %i)" i1 i2 - | BF_concat(ir1,ir2) -> fprintf ppf "(%a %a %a)" kwd "BF_concat" pp_lem_range ir1 pp_lem_range ir2 - -let pp_lem_typdef ppf (TD_aux(td,_)) = - match td with - | TD_abbrev(id,namescm,typschm) -> - fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm - | TD_record(id,nm,typq,fs,_) -> - let f_pp ppf (typ,id) = - fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" - kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs - | TD_variant(id,nm,typq,ar,_) -> - let a_pp ppf (Tu_aux(typ_u,_)) = - match typ_u with - | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id - | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id - in - fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" - kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar - | TD_enum(id,ns,enums,_) -> - let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a [%a] false)@]" - kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums - | TD_register(id,n1,n2,rs) -> - let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in - let pp_rids = (list_pp pp_rid pp_rid) in - fprintf ppf "@[<0>(%a %a %a %a [%a])@]" - kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs - -let pp_lem_rec ppf (Rec_aux(r,_)) = + | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l + | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l + | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l + +let pp_lem_typdef ppf (TD_aux(td,(l,annot))) = + let print_td ppf td = + match td with + | TD_abbrev(id,namescm,typschm) -> + fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm + | TD_record(id,nm,typq,fs,_) -> + let f_pp ppf (typ,id) = + fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" + kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs + | TD_variant(id,nm,typq,ar,_) -> + let a_pp ppf (Tu_aux(typ_u,l)) = + match typ_u with + | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" + pp_lem_typ typ pp_lem_id id pp_lem_l l + | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l + in + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" + kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar + | TD_enum(id,ns,enums,_) -> + let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in + fprintf ppf "@[<0>(%a %a %a [%a] false)@]" + kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums + | TD_register(id,n1,n2,rs) -> + let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in + let pp_rids = (list_pp pp_rid pp_rid) in + fprintf ppf "@[<0>(%a %a %a %a [%a])@]" + kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs + in + fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot + +let pp_lem_rec ppf (Rec_aux(r,l)) = match r with - | Rec_nonrec -> fprintf ppf "Rec_nonrec" - | Rec_rec -> fprintf ppf "Rec_rec" - -let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) = + | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l + | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l + +let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) = match t with - | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ + | Typ_annot_opt_some(tq,typ) -> + fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l -let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) = +let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) = match e with - | Effect_opt_pure -> fprintf ppf "Effect_opt_pure" - | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effect %a)" pp_lem_effects e + | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l + | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l -let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp +let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) = + fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a, %a))@]@\n" + kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot -let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) = +let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) = let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a [%a])@]" + fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]" kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls - -let pp_lem_def ppf (DEF_aux(d,(l,_))) = - match d with - | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df - | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec - | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def - | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def - | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind - | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id - | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs") + pp_lem_l l pp_annot annot + +let pp_lem_def ppf (DEF_aux(d,(l,annot))) = + let print_d ppf d = + match d with + | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df + | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec + | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def + | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def + | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind + | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id + | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs") + in + fprintf ppf "@[<0>(DEF_aux %a (%a, %a))@];@\n" print_d d pp_lem_l l pp_annot annot let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs diff --git a/src/process_file.ml b/src/process_file.ml index 25fbe49b..592c8cf5 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -159,6 +159,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo let (o, ext_o) = open_output_with_check (f' ^ ".lem") in Format.fprintf o "(* %s *)@\n" (generated_line filename); Format.fprintf o "open import Interp_ast@\n"; + Format.fprintf o "open import Pervasives@\n"; Format.fprintf o "let defs = "; Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o diff --git a/src/test/vectors.sail b/src/test/vectors.sail index 70cc5973..482ef902 100644 --- a/src/test/vectors.sail +++ b/src/test/vectors.sail @@ -2,6 +2,9 @@ let (bit[32]) v = 0b101 let (bit[4]) v2 = [0,1,0,0] register (bit[32]) i +let (bit[10]) v3 = 0b0101010111 +register (bit[5]) slice_check + register nat match_success function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1 @@ -9,6 +12,10 @@ and decode x = match_success := x function bit main _ = { + slice_check := v3; + slice_check := v3[1..10]; + slice_check := v3[5..10]; + i := [bitzero, bitzero, bitone, bitzero]; (* literal match *) diff --git a/src/type_check.ml b/src/type_check.ml index a75c690f..e5211d72 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -377,12 +377,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (match t.t,expect_t.t with | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value") | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> - let tannot = Some(([],t),External,cs,ef) in + let tannot = Some(([],t),External (Some "register"),cs,ef) in let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in (e',t',t_env,cs@cs',ef) | Tapp("register",[TA_typ(t')]),_ -> let ef' = add_effect (BE_aux(BE_rreg,l)) ef in - let tannot = Some(([],t),External,cs,ef') in + let tannot = Some(([],t),External (Some "register"),cs,ef') in let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in (e',t',t_env,cs@cs',ef) | Tapp("reg",[TA_typ(t)]),_ -> @@ -456,13 +456,13 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (ret_t,cs_r,e') = type_coerce l d_env ret (rebuild (Some(([],ret),tag,cs@cs',ef))) expect_t in (e',ret_t,t_env,cs@cs'@cs_r,ef) | [parm] -> - let (parm',arg_t,t_env,cs',ef') = check_exp envs arg parm in - let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs,ef))))) expect_t in - (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef') + let (parm',arg_t,t_env,cs',ef_p) = check_exp envs arg parm in + let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in + (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef') | parms -> - let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in - let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs,ef))))) expect_t in - (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef')) + let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in + let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in + (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef')) | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) | _ -> typ_error l ("Unbound function " ^ i)) | E_app_infix(lft,op,rht) -> @@ -866,7 +866,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema (match t.t with | Tapp("register",[TA_typ u]) -> let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in - (LEXP_aux(lexp,(l,(Some(([],t),External,cs,ef)))),u,Envmap.empty,External,[],ef) + (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),u,Envmap.empty,External (Some "register"),[],ef) | Tapp("reg",[TA_typ u]) -> (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),u,Envmap.empty,Emp,[],pure_e) | _ -> @@ -881,7 +881,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema let i = id_to_string id in (match Envmap.apply t_env i with | Some(Some((parms,t),tag,cs,ef)) -> - let is_external = match tag with | External -> true | _ -> false in + let is_external = match tag with | External any -> true | _ -> false in let t,cs,ef = subst parms t cs ef in let t,cs,ef = match get_abbrev d_env t with | None -> t,cs,ef @@ -1109,11 +1109,11 @@ let check_val_spec envs (VS_aux(vs,(l,annot))) = (VS_aux(vs,(l,tannot)), Env(d_env,(Envmap.insert t_env (id_to_string id,tannot)))) | VS_extern_no_rename(typs,id) -> - let tannot = typschm_to_tannot envs typs External in + let tannot = typschm_to_tannot envs typs (External None) in (VS_aux(vs,(l,tannot)), Env(d_env,(Envmap.insert t_env (id_to_string id,tannot)))) | VS_extern_spec(typs,id,s) -> - let tannot = typschm_to_tannot envs typs External in + let tannot = typschm_to_tannot envs typs (External (Some s)) in (VS_aux(vs,(l,tannot)), Env(d_env,(Envmap.insert t_env (id_to_string id,tannot)))) @@ -1141,7 +1141,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, | None -> Some(id_to_string id)) funcls None in let in_env = Envmap.apply t_env id in let ret_t,param_t,tannot = match tannotopt with - | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),(l',annot')) -> + | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') -> let (ids,constraints) = typq_to_params envs typq in let t = typ_to_t typ in let p_t = new_t () in @@ -1190,8 +1190,9 @@ let check_def envs (DEF_aux(def,(l,annot))) = (DEF_aux((DEF_default(ds)),(l,annot)),envs) | DEF_reg_dec(typ,id) -> let t = (typ_to_t typ) in - let tannot = into_register (Some(([],t),External,[],pure_e)) in - (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env ((id_to_string id),tannot)))) + let i = id_to_string id in + let tannot = into_register (Some(([],t),External (Some i),[],pure_e)) in + (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot)))) (*val check : envs -> tannot defs -> tannot defs*) diff --git a/src/type_internal.ml b/src/type_internal.ml index f43b797c..73bd5bc4 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -59,7 +59,7 @@ and t_arg = type tag = | Emp - | External + | External of string option | Default | Constructor | Enum @@ -198,11 +198,11 @@ let nat_typ = {t=Tid "nat"} let pure_e = {effect=Eset []} let initial_typ_env = Envmap.from_list [ - ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External,[],pure_e)); - ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); - ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); - ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); - ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External,[],pure_e)); + ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External None,[],pure_e)); + ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "add"),[],pure_e)); + ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e)); + ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e)); + ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External (Some "bitwise_or"),[],pure_e)); ] let initial_abbrev_env = @@ -308,6 +308,21 @@ and o_to_string o = | Odec -> "dec" | Ouvar({oindex=i;osubst=a}) -> string_of_int i ^ "()" +let tag_to_string = function + | Emp -> "Emp" + | External None -> "External" + | External (Some s) -> "External " ^ s + | Default -> "Default" + | Constructor -> "Constructor" + | Enum -> "Enum" + | Spec -> "Spec" + + +let tannot_to_string = function + | None -> "No tannot" + | Some((vars,t),tag,ncs,ef) -> + "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef + let get_abbrev d_env t = match t.t with | Tid i -> @@ -479,11 +494,11 @@ let rec type_coerce l d_env t1 e t2 = | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd(b1,r1)})})] in - (t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd({nexp=Nneg b1},r1)})})] in - (t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert a vector to an enum without an order" | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> @@ -494,12 +509,12 @@ let rec type_coerce l d_env t1 e t2 = | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(l,b1,{nexp=Nconst 0});Eq(l,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in - (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [Eq(l,b1,{nexp=N2n{nexp=Nadd(b2,{nexp=Nneg r2})}}); Eq(l,r1,b1)] in - (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert an enum to a vector without an order" | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> @@ -542,7 +557,7 @@ let rec type_coerce l d_env t1 e t2 = (l,Some(([],t2),Emp,[],pure_e)))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))) | Tid("bit"),Tid("bool") -> - let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External,[],pure_e))) in + let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in (t2,[],e') | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> (match get_abbrev d_env t1 with diff --git a/src/type_internal.mli b/src/type_internal.mli index 13cb56ea..63583d28 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -54,7 +54,7 @@ and t_arg = type tag = | Emp - | External + | External of string option | Default | Constructor | Enum @@ -102,6 +102,7 @@ val bit_t : t val pure_e : effect val t_to_string : t -> string +val tannot_to_string : tannot -> string val reset_fresh : unit -> unit val new_t : unit -> t |