diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 84 | ||||
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | src/type_internal.ml | 23 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
4 files changed, 69 insertions, 43 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index b47f808a..84efbf56 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -219,6 +219,10 @@ and pp_exp ppf (E_aux(e,_)) = | E_id(id) -> pp_id ppf id | E_lit(lit) -> pp_lit ppf lit | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp + | E_internal_cast((_,None),e) -> pp_exp ppf e + | E_internal_cast((_,Some((_,t),_,_,_)), exp) -> + (*check if the internal exp has the same vector start as the annot, and if so, drop *) + fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_comma_exp pp_exp) args | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")" @@ -631,44 +635,48 @@ let rec pp_lem_let ppf (LB_aux(lb,(l,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 e2 - | 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_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_internal_cast((_,None),e) -> pp_lem_exp ppf e + | E_internal_cast((_,Some((_,t),_,_,_)), exp) -> + (*check if the internal exp has the same vector start as the annot, and if so, drop *) + fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) 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 e2 + | 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 diff --git a/src/type_check.ml b/src/type_check.ml index 0c3f25af..b3836761 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1118,7 +1118,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) = match basei.nexp,topi.nexp with | Nconst b, Nconst t -> if b <= t then ( - let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp{nexp=Nconst(t-b)}; + let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp{nexp=Nconst(t-b+1)}; TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in let franges = List.map @@ -1133,7 +1133,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) = | BF_range(i1,i2) -> if i1<i2 then if b<=i1 && i2<=t - then {t=Tapp("vector",[TA_nexp {nexp=Nconst i1}; TA_nexp {nexp=Nconst (i2 - i1)}; TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])} + then {t=Tapp("vector",[TA_nexp {nexp=Nconst i1}; TA_nexp {nexp=Nconst ((i2 - i1) +1)}; TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])} else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size") else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing") | BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp_global,[],pure_e))) diff --git a/src/type_internal.ml b/src/type_internal.ml index 5eb2b85a..af4bd49d 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -203,6 +203,7 @@ let lookup_field_type (field: string) ((id,r_kind,fields) : rec_env) : tannot = (* eval an nexp as much as possible *) let rec eval_nexp n = + (*let _ = Printf.printf "eval_nexp of %s\n" (n_to_string n) in*) match n.nexp with | Nconst i -> n | Nmult(n1,n2) -> @@ -667,7 +668,7 @@ and n_to_nexp n = | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2) | N2n n -> Nexp_exp (n_to_nexp n) | Nneg n -> Nexp_neg (n_to_nexp n) - | Nuvar _ -> assert false), Parse_ast.Unknown) + | Nuvar _ -> Nexp_var (Kid_aux((Var "fresh"),Parse_ast.Unknown))), Parse_ast.Unknown) and e_to_ef ef = Effect_aux( (match ef.effect with @@ -847,9 +848,23 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = (t2,cs,e') else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^ " but expected a tuple of length " ^ (string_of_int tl2)) | Tapp(id1,args1),Tapp(id2,args2) -> - if id1=id2 + if id1=id2 && (id1 <> "vector") then let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e) else (match id1,id2 with + | "vector","vector" -> + (match args1,args2 with + | [TA_nexp b1;TA_nexp r1;TA_ord o1;TA_typ t1i], + [TA_nexp b2;TA_nexp r2;TA_ord o2;TA_typ t2i] -> + (match o1.order,o2.order with + | Oinc,Oinc | Odec,Odec -> () + | Oinc,Ouvar _ | Odec,Ouvar _ -> o2.order <- o1.order + | Ouvar _,Oinc | Ouvar _, Oinc -> o1.order <- o2.order + | _,_ -> equate_o o1 o2); + let cs = [Eq(l,r1,r2)]@cs1@cs2 in + let t',cs' = type_consistent l d_env t1i t2i in + let tannot = Some(([],t2),Emp_local,cs,pure_e) in + let e' = E_aux(E_internal_cast ((l,(Some(([],t2),Emp_local,[],pure_e))),e),(l,tannot)) in + (t2,cs@cs',e')) | "vector","range" -> (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], @@ -943,7 +958,9 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = and type_coerce l d_env t1 e t2 = type_coerce_internal l d_env t1 [] e t2 [] -let rec simple_constraint_check = function +let rec simple_constraint_check cs = + let _ = Printf.printf "simple_constraint_check\n" in + match cs with | [] -> [] | Eq(l,n1,n2)::cs -> let n1',n2' = eval_nexp n1,eval_nexp n2 in diff --git a/src/type_internal.mli b/src/type_internal.mli index 496db9df..eec077d6 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -106,6 +106,7 @@ val pure_e : effect val t_to_string : t -> string val tannot_to_string : tannot -> string +val t_to_typ : t -> Ast.typ val reset_fresh : unit -> unit val new_t : unit -> t |