From ac9aa3b73181cf6f8a0bbcf2c59562ec17c7c8ea Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Sun, 14 Aug 2016 12:37:46 +0100 Subject: Start adding form for (a,b,c) := foo() Not working yet --- src/initial_check.ml | 15 +++++-- src/initial_check_full_ast.ml | 9 ++++ src/pretty_print.ml | 6 ++- src/rewriter.ml | 4 ++ src/rewriter.mli | 1 + src/type_check.ml | 98 ++++++++++++++++++++++++++++++------------- src/type_internal.ml | 4 +- src/type_internal.mli | 2 + 8 files changed, 104 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/initial_check.ml b/src/initial_check.ml index beaac9c2..5b813c04 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -450,7 +450,18 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp = LEXP_aux( (match exp with - | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) + | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) + | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> + LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) + | Parse_ast.E_tuple(tups) -> + let ltups = List.map (to_ast_lexp k_env def_ord) tups in + let is_ok_in_tup (LEXP_aux (le,(l,_))) = + match le with + | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () + | LEXP_memory _ -> + typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in + List.iter is_ok_in_tup ltups; + LEXP_tup(ltups) | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> (match f with | Parse_ast.Id(id) -> @@ -459,8 +470,6 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps) | args -> LEXP_memory(to_ast_id f', args)) | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) - | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) -> - LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id) | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp) | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2) diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml index 1443af5d..562d778e 100644 --- a/src/initial_check_full_ast.ml +++ b/src/initial_check_full_ast.ml @@ -381,6 +381,15 @@ and to_lexp (k_env : kind Envmap.t) (def_ord : Ast.order) (LEXP_aux(exp,(l,_)) : | args -> LEXP_memory(f, args)) | LEXP_cast(typ,id) -> LEXP_cast(to_typ k_env def_ord typ, id) + | LEXP_tup tups -> + let ltups = List.map (to_lexp k_env def_ord) tups in + let is_ok_in_tup (LEXP_aux (le,(l,_))) = + match le with + | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> () + | LEXP_memory _ -> + typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in + List.iter is_ok_in_tup ltups; + LEXP_tup(ltups) | LEXP_vector(vexp,exp) -> LEXP_vector(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp) | LEXP_vector_range(vexp,exp1,exp2) -> LEXP_vector_range(to_lexp k_env def_ord vexp, to_exp k_env def_ord exp1, to_exp k_env def_ord exp2) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 6680ef60..8cf95575 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -290,11 +290,12 @@ and pp_format_o o = | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" -let pp_format_tag = function +let rec pp_format_tag = function | Emp_local -> "Tag_empty" | Emp_intro -> "Tag_intro" | Emp_set -> "Tag_set" | Emp_global -> "Tag_global" + | Tuple_assign tags -> "(Tag_tuple_assign [" ^ list_format " ;" pp_format_tag tags ^ "])" | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" | External None -> "(Tag_extern Nothing)" | Default -> "Tag_default" @@ -495,12 +496,15 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) = | LEXP_memory(id,args) -> fprintf ppf "(LEXP_memory %a [%a])" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id + | LEXP_tup tups -> fprintf ppf "(LEXP_tuple [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups | 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 +and pp_semi_lem_lexp ppf le = fprintf ppf "@[<1>%a%a@]" pp_lem_lexp le kwd ";" + let pp_lem_default ppf (DT_aux(df,l)) = let print_de ppf df = diff --git a/src/rewriter.ml b/src/rewriter.ml index f9959814..9b97f296 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -457,6 +457,7 @@ let rewrite_lexp rewriters map (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp + | LEXP_tup tupls -> rewrap (LEXP_tup (List.map (rewriters.rewrite_lexp rewriters map) tupls)) | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters map) exps)) | LEXP_vector (lexp,exp) -> rewrap (LEXP_vector (rewriters.rewrite_lexp rewriters map lexp,rewriters.rewrite_exp rewriters map exp)) @@ -622,6 +623,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_id : id -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux ; lEXP_cast : Ast.typ * id -> 'lexp_aux + ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux @@ -749,6 +751,7 @@ let id_exp_alg = ; lEXP_id = (fun id -> LEXP_id id) ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es)) ; lEXP_cast = (fun (typ,id) -> LEXP_cast (typ,id)) + ; lEXP_tup = (fun tups -> LEXP_tup tups) ; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2)) ; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3)) ; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id)) @@ -1602,6 +1605,7 @@ let find_updated_vars exp = ; lEXP_id = (fun id -> (Some id,[],([],[]))) ; lEXP_memory = (fun (_,es) -> (None,[],lapp2 es)) ; lEXP_cast = (fun (_,id) -> (Some id,[],([],[]))) + ; lEXP_tup = (fun tups -> failwith "FORCHRISTOPHER:: this needs implementing, not sure what you want to do") ; lEXP_vector = (fun ((ids,acc),e1) -> (None,ids,acc @@ e1)) ; lEXP_vector_range = (fun ((ids,acc),e1,e2) -> (None,ids,acc @@ e1 @@ e2)) ; lEXP_field = (fun ((ids,acc),_) -> (None,ids,acc)) diff --git a/src/rewriter.mli b/src/rewriter.mli index ab4645f3..a9ba973e 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -85,6 +85,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; lEXP_id : id -> 'lexp_aux ; lEXP_memory : id * 'exp list -> 'lexp_aux ; lEXP_cast : Ast.typ * id -> 'lexp_aux + ; lEXP_tup : 'lexp list -> 'lexp_aux ; lEXP_vector : 'lexp * 'exp -> 'lexp_aux ; lEXP_vector_range : 'lexp * 'exp * 'exp -> 'lexp_aux ; lEXP_field : 'lexp * id -> 'lexp_aux diff --git a/src/type_check.ml b/src/type_check.ml index bd576dbb..9a99cc36 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -540,7 +540,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) | 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 = Base(([],t),(match tag with | External _ -> Emp_global | _ -> tag),cs,pure_e,pure_e,bounds) in + let tannot = Base(([],t),(match tag with | External _ -> Emp_global | _ -> tag), + cs,pure_e,pure_e,bounds) in let t',cs' = type_consistent (Expr l) d_env Require widen_vec t' expect_t' in (rebuild tannot,t,t_env,cs@cs',bounds,ef) | Tapp("register",[TA_typ(t')]),Tuvar _ -> @@ -675,11 +676,11 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let _,cs,ef,parm' = type_coerce (Expr l) d_env Guarantee false false b_env arg_t parm expect_arg_t in [parm'],ef,cs | parms -> - (match - type_coerce (Expr l) d_env Guarantee false false b_env arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t - with + (match type_coerce (Expr l) d_env Guarantee false false b_env arg_t + (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t with | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs) - | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) + | _ -> + raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) in let check_result ret imp tag cs ef efr parms = match (imp,imp_param) with @@ -708,7 +709,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) type_coerce (Expr l) d_env Require false true b_env ret (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t | (IP_none,_) -> - (*let _ = Printf.eprintf "no implicit: ret %s and expect_t %s\n" (t_to_string ret) (t_to_string expect_t) in*) + (*let _ = Printf.eprintf "no implicit: ret %s and expect_t %s\n" + (t_to_string ret) (t_to_string expect_t) in*) type_coerce (Expr l) d_env Require false true b_env ret (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t in @@ -718,7 +720,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) | Some(Base(tp,Default,_,_,_,_)) -> typ_error l ("Function " ^ i ^ " must be specified, not just declared as a default, before use") | Some(Base((params,t),tag,cs,efl,_,bounds)) -> - (*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" + (*let _ = Printf.eprintf "Going to check func call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*) let t,cs,efl,_ = subst params false false t cs efl in (match t.t with @@ -730,7 +732,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let parms,arg_t,cs_p,ef_p = check_parms arg parms in (*let _ = Printf.eprintf "Checked parms of %s\n" i in*) let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs efl' (union_effects efl' ef_p) parms in - (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*) + (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" + i (constraints_to_string cs_r) in*) (e',ret_t,t_env,cs@cs_p@cs_r, bounds,union_effects efl' (union_effects ef_p ef_r)) | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ @@ -976,8 +979,10 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) then (esn,csn,efn,(((i-prev) > 1) || skips),i) else if i = prev then (typ_error l ("Indexed vector contains a duplicate definition of index " ^ (string_of_int i))) - else (typ_error l ("Indexed vector is not consistently " ^ (if is_inc then "increasing" else "decreasing")))) - (List.map (fun (i,e) -> let (e,_,_,cs,_,eft) = (check_exp envs imp_param true true ret_t item_t e) in ((i,e),cs,eft)) + else (typ_error l ("Indexed vector is not consistently " ^ + (if is_inc then "increasing" else "decreasing")))) + (List.map (fun (i,e) -> + let (e,_,_,cs,_,eft) = (check_exp envs imp_param true true ret_t item_t e) in ((i,e),cs,eft)) eis) ([],[],pure_e,false,(if is_inc then (last+1) else (last-1)))) in let (default',fully_enumerate,cs_d,ef_d) = match (default,contains_skip) with | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,simple_annot item_t)),true,[],pure_e) @@ -1151,7 +1156,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let sub_effects = union_effects ef (union_effects ef_i1 (union_effects ef_i2 ef_e)) in let (t,cs3,ef3,e') = type_coerce (Expr l) d_env Require false false b_env nt - (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot_efr nt cs_loc sub_effects))) expect_t in + (E_aux(E_vector_update_subrange(vec',i1',i2',e'), + (l,constrained_annot_efr nt cs_loc sub_effects))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,nob,(union_effects ef3 sub_effects)) | E_vector_append(v1,v2) -> let item_t,ord = match expect_t_actual.t with @@ -1162,9 +1168,11 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let base1,rise1 = new_n(), new_n() in let base2,rise2 = new_n(),new_n() in let (v1',t1',_,cs_1,_,ef_1) = - check_exp envs imp_param true true ret_t {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in + check_exp envs imp_param true true ret_t + {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in let (v2',t2',_,cs_2,_,ef_2) = - check_exp envs imp_param true true ret_t {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in + check_exp envs imp_param true true ret_t + {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in let result_rise = mk_add rise1 rise2 in let result_base = match ord.order with | Odec -> mk_sub result_rise n_one @@ -1217,7 +1225,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) | Some(((i,Record,(Base((params,t),tag,cs,eft,_,bounds)),fields) as r)) -> let (ts,cs,eft,subst_env) = subst params false false t cs eft in if (List.length fexps = List.length fields) - then let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag n) fexps ([],[],pure_e) in + then let fexps,cons,ef = + List.fold_right (field_walker r subst_env bounds tag n) fexps ([],[],pure_e) in let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot_efr u ef)) in let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') @@ -1263,7 +1272,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes") | _ -> - typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) + typ_error l ("Expected a struct or register, instead found an expression with type " ^ i)) | Tuvar _ -> let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in (match lookup_possible_records field_names d_env.rec_env with @@ -1275,7 +1284,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in (e',t',t_env,cs@cons@cs',nob,union_effects ef ef') | [(i,Register,tannot,fields)] -> typ_error l "Expected a value with register type, found a struct" - | records -> typ_error l "Multiple structs contain this set of fields, try adding a cast to disambiguate") + | records -> typ_error l "Multiple structs contain this set of fields, try adding a cast") | _ -> typ_error l ("Expected a struct to update but found an expression of type " ^ t_to_string expect_t)) | E_field(exp,id) -> let (e',t',env_sub,c_sub,bounds,ef_sub) = check_exp envs imp_param true true ret_t (new_t()) exp in @@ -1304,7 +1313,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) expect_t in (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' (union_effects ef_update ef_sub))) | _ -> - typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)) + typ_error l ("Expected a struct or register, instead found an expression with type " ^ i)) | Tuvar _ -> (match lookup_possible_records [fi] d_env.rec_env with | [] -> typ_error l ("No struct or register has a field " ^ fi) @@ -1320,7 +1329,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let (e',t',_,c_sub,_,ef_sub),ef_update = match rec_kind with | Register -> - (check_exp envs imp_param true true ret_t (into_register_typ t') exp, add_effect (BE_aux(BE_rreg, l)) pure_e) + (check_exp envs imp_param true true ret_t (into_register_typ t') exp, + add_effect (BE_aux(BE_rreg, l)) pure_e) | Record -> ((e',t',env_sub,c_sub,bounds,ef_sub), pure_e) in let (et',c',ef',acc) = type_coerce (Expr l) d_env Require false false b_env ft @@ -1330,7 +1340,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' (union_effects ef_update ef_sub))) | records -> typ_error l ("Multiple structs or registers contain field " ^ fi ^ ", try adding a cast to disambiguate")) - | _ -> typ_error l ("Expected a struct or register for access but found an expression of type " ^ t_to_string t')) + | _ -> typ_error l ("Expected a struct or register but found an expression of type " ^ t_to_string t')) | E_case(exp,pexps) -> let (e',t',_,cs,_,ef) = check_exp envs imp_param true true ret_t (new_t()) exp in (*let _ = Printf.eprintf "Type of pattern after expression check %s\n" (t_to_string t') in*) @@ -1342,7 +1352,8 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool) let (pexps',t,cs',ef') = check_cases envs imp_param ret_t t' expect_t (if (List.length pexps) = 1 then Solo else Switch) pexps in let effects = union_effects ef ef' in - (E_aux(E_case(e',pexps'),(l,simple_annot_efr t effects)),t,t_env,cs@[BranchCons(Expr l, None, cs')],nob,effects) + (E_aux(E_case(e',pexps'),(l,simple_annot_efr t effects)),t, + t_env,cs@[BranchCons(Expr l, None, cs')],nob,effects) | E_let(lbind,body) -> let (lb',t_env',cs,b_env',ef) = (check_lbind envs imp_param false (Some ret_t) Emp_local lbind) in let new_env = @@ -1397,7 +1408,8 @@ and recheck_for_register envs imp_param widen_num widen_vec ret_t expect_t exp = match exp' with | E_aux(_, (l, Base(_, _, _, leff, ceff, _))) -> if has_rreg_effect ceff - then try let (exp',t',_,cs,_,ef) = check_exp envs imp_param widen_num widen_vec ret_t (into_register_typ t') exp in + then try let (exp',t',_,cs,_,ef) = + check_exp envs imp_param widen_num widen_vec ret_t (into_register_typ t') exp in (exp',t',cs,ef),(add_effect (BE_aux(BE_rreg,l)) pure_e),External None with | _ -> (exp',t',cs,ef),pure_e, Emp_local else (exp',t',cs,ef),pure_e, Emp_local @@ -1548,11 +1560,12 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) typ_error l ("Expected arguments with types " ^ (t_to_string args_t) ^ "for assignment function " ^ i) | args,es -> - (match check_exp envs imp_param true true ret_t args_t (E_aux (E_tuple exps,(l,NoTyp))) with - | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e) - | _ -> - raise (Reporting_basic.err_unreachable l - "Gave check_exp a tuple, didn't get a tuple back")) + (match check_exp envs imp_param true true ret_t args_t + (E_aux (E_tuple exps,(l,NoTyp))) with + | (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e) + | _ -> + raise (Reporting_basic.err_unreachable l + "Gave check_exp a tuple, didn't get a tuple back")) in let ef_all = union_effects ef' ef_es in (LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef',ef_all,nob))), @@ -1603,12 +1616,14 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) | Tuvar _,_ -> let u' = {t=Tapp("reg",[TA_typ ty])} in equate_t t u'; - (LEXP_aux(lexp,(l,(Base((([],u'),Emp_set,cs,ef,pure_e,bs))))),ty,false,Envmap.empty,Emp_set,[],bs,ef,ef) + (LEXP_aux(lexp,(l,(Base((([],u'),Emp_set,cs,ef,pure_e,bs))))), + ty,false,Envmap.empty,Emp_set,[],bs,ef,ef) | (Tfn _ ,_) -> (match tag with | External _ | Spec | Emp_global -> let tannot = (Base(([],ty),Emp_intro,[],pure_e,pure_e,new_bounds)) in - (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e,pure_e) + (LEXP_aux(lexp,(l,tannot)),ty, + false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e,pure_e) | _ -> typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) | _,_ -> @@ -1624,6 +1639,26 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) let t = {t=Tapp("reg",[TA_typ ty])} in let tannot = (Base(([],t),Emp_intro,[],pure_e,pure_e,new_bounds)) in (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_intro,[],new_bounds,pure_e,pure_e)) + | LEXP_tup tuples -> + if is_top + then + if tuples = [] + then typ_error l "Attempt to set an empty tuple, which is not allowed" + else + let tuple_checks = List.map (check_lexp envs imp_param ret_t true) tuples in + let tuple_vs = List.map (fun (le,_,_,_,_,_,_,_,_) -> le) tuple_checks in + let tuple_typs = List.map (fun (_,le_t,_,_,_,_,_,_,_) -> le_t) tuple_checks in + let tuple_tags = List.map (fun (_,_,_,_,tag,_,_,_,_) -> tag) tuple_checks in + let env = List.fold_right (fun (_,_,_,env,_,_,_,_,_) envf -> Envmap.union env envf) + tuple_checks Envmap.empty in + let cs = List.fold_right (fun (_,_,_,_,_,cs,_,_,_) csf -> cs @csf) tuple_checks [] in + let bounds = List.fold_right (fun (_,_,_,_,_,_,bs,_,_) bf -> merge_bounds bs bf) tuple_checks nob in + let efr = List.fold_right (fun (_,_,_,_,_,_,_,_,efr) efrf -> union_effects efr efrf) tuple_checks pure_e in + let ty = mk_tup tuple_typs in + let tag = Tuple_assign tuple_tags in + let tannot = (Base(([],ty),tag,[],pure_e,efr,bounds)) in + (LEXP_aux (LEXP_tup tuple_vs, (l,tannot)), ty,false,env, tag,cs,bounds,pure_e,efr) + else typ_error l "Tuples in assignments may only be at the top level or within other tuples" | LEXP_vector(vec,acc) -> let (vec',vec_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param ret_t false vec in let vec_t,cs' = get_abbrev d_env vec_t in @@ -1715,7 +1750,9 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier" else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],res_t),tag,cs,efl,ef,nob))), res_t,reg_required&®_still_required && needs_reg,env,tag,cs,bounds,efl,ef) - | Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation." + | Tuvar _ -> + typ_error l + "Assignement to a range of items requires a vector with a known order, try adding an annotation." | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) | LEXP_field(vec,id)-> let (vec',item_t,reg_required,env,tag,csi,bounds,efl,efr) = check_lexp envs imp_param ret_t false vec in @@ -1738,7 +1775,8 @@ and check_lexp envs imp_param ret_t is_top (LEXP_aux(lexp,(l,annot))) (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,efr,nob)))), ft,false,env,tag,csi@cs@cs_sub',bounds,eft,efr)) | _ -> - typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)) + typ_error l + ("Expected a register or struct for this update, instead found an expression with type " ^ i)) | _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t))) and check_lbind envs imp_param is_top_level opt_ret_t emp_tag (LB_aux(lbind,(l,annot))) diff --git a/src/type_internal.ml b/src/type_internal.ml index ff6cd08d..c7b47831 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -88,6 +88,7 @@ type tag = | Emp_global | Emp_intro | Emp_set + | Tuple_assign of tag list | External of string option | Default | Constructor of int @@ -364,11 +365,12 @@ and o_to_string o = | Odec -> "dec" | Ouvar({oindex=i;osubst=a}) -> if !debug_mode then string_of_int i ^ "()" else "_" -let tag_to_string = function +let rec tag_to_string = function | Emp_local -> "Emp_local" | Emp_global -> "Emp_global" | Emp_intro -> "Emp_intro" | Emp_set -> "Emp_set" + | Tuple_assign tags -> "Tuple_assign (" ^ string_of_list ", " tag_to_string tags ^ ")" | External None -> "External" | External (Some s) -> "External " ^ s | Default -> "Default" diff --git a/src/type_internal.mli b/src/type_internal.mli index fc274409..3ce674dd 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -90,6 +90,7 @@ type tag = | Emp_global (* Variable from global instead of local scope *) | Emp_intro (* Local mutable variable, and this is its introduction *) | Emp_set (* Local mutable expression being set *) + | Tuple_assign of tag list (* Tuple of assignments, should not be External, Default, Construct, etc*) | External of string option (* External function or register name *) | Default (* Variable has default type, has not been bound *) | Constructor of int (* Variable is a data constructor, int says how many variants are in this family *) @@ -148,6 +149,7 @@ val mk_inexact : unit -> nexp val set_imp_param : nexp -> unit val mk_atom : nexp -> t +val mk_tup : t list -> t type variable_range = | VR_eq of string * nexp -- cgit v1.2.3