diff options
| author | Kathy Gray | 2015-10-23 15:14:07 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-10-23 15:14:59 +0100 |
| commit | 89f9c0e89ca3722e7248c70300c239374842b93e (patch) | |
| tree | c744f94e0f51803f28531d81bda336d1847c56a4 | |
| parent | a43119b131d87309e51b851466c9a4b489b8bec7 (diff) | |
More of sail correctly generating ocaml; including using polymorphic variants when there are more than 246 constructors
| -rw-r--r-- | src/gen_lib/sail_values.ml | 122 | ||||
| -rw-r--r-- | src/pretty_print.ml | 110 | ||||
| -rw-r--r-- | src/type_check.ml | 58 | ||||
| -rw-r--r-- | src/type_internal.ml | 580 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
5 files changed, 509 insertions, 363 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 42f0bfde..c789ff52 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -131,11 +131,11 @@ let set_vector_subrange_bit v n m new_v = done; end in - match v with - | Vvector(array,start,is_inc) -> + match v,new_v with + | Vvector(array,start,is_inc),Vvector(new_v,_,_) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in walker array length offset new_v - | Vregister(array,start,is_inc,fields) -> + | Vregister(array,start,is_inc,fields),Vvector(new_v,_,_) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in walker !array length offset new_v | _ -> () @@ -240,6 +240,44 @@ let bitwise_not = function | Vregister(array,s,d,_) -> Vvector( Array.map bitwise_not_bit !array,s,d) | _ -> assert false +let bool_to_bit b = if b then Vone else Vzero + +let bitwise_binop_bit op (l,r) = + match l,r with + | Vundef,_ | _,Vundef -> Vundef (*Do we want to do this or to respect | of One and & of Zero rules?*) + | Vone,Vone -> bool_to_bit (op true true) + | Vone,Vzero -> bool_to_bit (op true false) + | Vzero,Vone -> bool_to_bit (op false true) + | Vzero,Vzero -> bool_to_bit (op false false) + +let bitwise_and_bit = bitwise_binop_bit (&&) +let bitwise_or_bit = bitwise_binop_bit (||) +let bitwise_xor_bit = bitwise_binop_bit (fun x y -> (1 = (if x then 1 else 0) lxor (if y then 0 else 1))) + +let bitwise_binop op (l,r) = + let bop l arrayl arrayr = + let array = Array.make l Vzero in + begin + for i = 0 to l do + array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i)) + done; + array + end in + match l,r with + | Vvector(arrayl, start, dir), Vvector(arrayr,_,_) -> + Vvector(bop (Array.length arrayl) arrayl arrayr, start,dir) + | Vvector(arrayl, start, dir), Vregister(arrayr,_,_,_) -> + Vvector(bop (Array.length arrayl) arrayl !arrayr, start, dir) + | Vregister(arrayl, start,dir,_), Vvector(arrayr,_,_) -> + Vvector(bop (Array.length arrayr) !arrayl arrayr, start,dir) + | Vregister(arrayl, start, dir, _), Vregister(arrayr,_,_,_) -> + Vvector(bop (Array.length !arrayl) !arrayl !arrayr, start,dir) + | _ -> Vbit Vundef + +let bitwise_and = bitwise_binop (&&) +let bitwise_or = bitwise_binop (||) +let bitwise_xor = bitwise_binop (fun x y -> (1 = (if x then 1 else 0) lxor (if y then 0 else 1))) + let unsigned = function | (Vvector(array,_,_) as v) -> if has_undef v @@ -342,6 +380,14 @@ let to_vec ord len n = let to_vec_inc (len,n) = to_vec true len n let to_vec_dec (len,n) = to_vec false len n +let to_vec_undef ord len = + let len = int_of_big_int len in + let array = Array.make len Vundef in + let start = if ord then 0 else len-1 in + Vvector(array, start, ord) + +let to_vec_inc_undef len = to_vec_undef true len +let to_vec_dec_undef len = to_vec_undef false len let arith_op op (l,r) = op l r let add = arith_op add_big_int @@ -493,11 +539,14 @@ let rec arith_op_no0 op (l,r) = then None else Some (op l r) +let modulo = arith_op_no0 mod_big_int +let quot = arith_op_no0 div_big_int + let rec arith_op_vec_no0 op sign size (l,r) = let ord = get_ord l in let act_size = int_of_big_int (mult_big_int (length l) size) in let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op op (l',r') in + let n = arith_op_no0 op (l',r') in let representable,n' = match n with | Some n' -> @@ -512,6 +561,10 @@ let rec arith_op_vec_no0 op sign size (l,r) = Vvector((Array.make act_size Vundef), start, ord) | _ -> assert false +let mod_vec = arith_op_vec_no0 mod_big_int false unit_big_int +let quot_vec = arith_op_vec_no0 div_big_int false unit_big_int +let quot_vec_signed = arith_op_vec_no0 div_big_int true unit_big_int + let arith_op_overflow_no0_vec op sign size (l,r) = let ord = get_ord l in let rep_size = mult_big_int (length r) size in @@ -537,8 +590,67 @@ let arith_op_overflow_no0_vec op sign size (l,r) = let overflow = if representable then Vzero else Vone in (correct_size_num,overflow,most_significant one_more) +let quot_overflow_vec = arith_op_overflow_no0_vec div_big_int false unit_big_int +let quot_overflow_vec_signed = arith_op_overflow_no0_vec div_big_int true unit_big_int + let arith_op_vec_range_no0 op sign size (l,r) = let ord = get_ord l in arith_op_vec_no0 op sign size (l,(to_vec ord (length l) r)) - +let mod_vec_range = arith_op_vec_range_no0 mod_big_int false unit_big_int + +(*Need to have a default top level direction reference I think*) +let duplicate (bit,length) = + Vvector((Array.make (int_of_big_int length) bit), 0, true) + + +let compare_op op (l,r) = + if (op l r) + then Vone + else Vzero + +let lt = compare_op lt_big_int +let gt = compare_op gt_big_int +let lteq = compare_op le_big_int +let gteq = compare_op ge_big_int + +let compare_op_vec op sign (l,r) = + let (l',r') = (to_num sign l, to_num sign r) in + compare_op op (l',r') + +let lt_vec = compare_op_vec lt_big_int true +let gt_vec = compare_op_vec gt_big_int true +let lteq_vec = compare_op_vec le_big_int true +let gteq_vec = compare_op_vec ge_big_int true +let lt_vec_signed = compare_op_vec lt_big_int true +let gt_vec_signed = compare_op_vec gt_big_int true +let lteq_vec_signed = compare_op_vec le_big_int true +let gteq_vec_signed = compare_op_vec ge_big_int true +let lt_vec_unsigned = compare_op_vec lt_big_int false +let gt_vec_unsigned = compare_op_vec gt_big_int false +let lteq_vec_unsigned = compare_op_vec le_big_int false +let gteq_vec_unsigned = compare_op_vec ge_big_int false + +let compare_op_vec_range op sign (l,r) = + compare_op op ((to_num sign l),r) + +let lt_vec_range = compare_op_vec_range lt_big_int true +let gt_vec_range = compare_op_vec_range gt_big_int true +let lteq_vec_range = compare_op_vec_range le_big_int true +let gteq_vec_range = compare_op_vec_range ge_big_int true + +let compare_op_range_vec op sign (l,r) = + compare_op op (l, (to_num sign r)) + +let lt_range_vec = compare_op_range_vec lt_big_int true +let gt_range_vec = compare_op_range_vec gt_big_int true +let lteq_range_vec = compare_op_range_vec le_big_int true +let gteq_range_vec = compare_op_range_vec ge_big_int true + +let eq (l,r) = if l == r then Vone else Vzero +let eq_vec_range (l,r) = eq (to_num false l,r) +let eq_range_vec (l,r) = eq (l, to_num false r) +let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) + +let neq (l,r) = bitwise_not_bit (eq (l,r)) +let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r)) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 7ec83696..f979efca 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -294,7 +294,7 @@ let pp_format_tag = function | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" | External None -> "(Tag_extern Nothing)" | Default -> "Tag_default" - | Constructor -> "Tag_ctor" + | Constructor _ -> "Tag_ctor" | Enum i -> "(Tag_enum " ^ (lemnum string_of_int i) ^ ")" | Alias alias_inf -> "Tag_alias" | Spec -> "Tag_spec" @@ -1225,10 +1225,10 @@ let doc_id_ocaml_type (Id_aux(i,_)) = * token in case of x ending with star. *) parens (separate space [colon; string (String.uncapitalize x); empty]) -let doc_id_ocaml_ctor (Id_aux(i,_)) = +let doc_id_ocaml_ctor n (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" - | Id i -> string (String.capitalize i) + | Id i -> string ((if n > 246 then "`" else "") ^ (String.capitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) @@ -1300,13 +1300,21 @@ let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = let doc_pat_ocaml = let rec pat pa = app_pat pa and app_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp pat pats)) + | P_app(id, ((_ :: _) as pats)) -> + (match annot with + | Base(_,Constructor n,_,_,_,_) -> + doc_unop (doc_id_ocaml_ctor n id) (parens (separate_map comma_sp pat pats)) + | _ -> empty) | P_lit lit -> doc_lit_ocaml true lit | P_wild -> underscore | P_id id -> doc_id_ocaml id | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) - | P_app(id,[]) -> doc_id_ocaml_ctor id + | P_app(id,[]) -> + (match annot with + | Base(_,Constructor n,_,_,_,_) -> + doc_id_ocaml_ctor n id + | _ -> empty) | P_vector pats -> let non_bit_print () = parens @@ -1337,18 +1345,18 @@ let doc_exp_ocaml, doc_let_ocaml = (match le_act with | LEXP_id _ | LEXP_cast _ -> (*Setting local variable fully *) - doc_op coloneq (doc_lexp_ocaml le) (exp e) + doc_op coloneq (doc_lexp_ocaml true le) (exp e) | LEXP_vector _ -> doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e) | LEXP_vector_range _ -> - parens ((string "set_vector_range") ^^ space ^^ (doc_lexp_ocaml le) ^^ space ^^ (exp e))) + doc_lexp_rwrite le e) | _ -> (match le_act with | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> (doc_lexp_rwrite le e) | LEXP_memory _ -> (doc_lexp_fcall le e))) | E_vector_append(l,r) -> - parens (string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r) + parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) | E_if(c,t,E_aux(E_block [], _)) -> parens (string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ @@ -1396,7 +1404,7 @@ let doc_exp_ocaml, doc_let_ocaml = | E_app(f,args) -> let call = match annot with | Base(_,External (Some n),_,_,_,_) -> string n - | Base(_,Constructor,_,_,_,_) -> doc_id_ocaml_ctor f + | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i f | _ -> doc_id_ocaml f in parens (doc_unop call (parens (separate_map comma exp args))) | E_vector_access(v,e) -> @@ -1432,7 +1440,7 @@ let doc_exp_ocaml, doc_let_ocaml = if read_registers then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" else doc_id_ocaml id - | Base(_,(Constructor|Enum _),_,_,_,_) -> doc_id_ocaml_ctor id + | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_ocaml_ctor i id | Base((_,t),Alias alias_info,_,_,_,_) -> (match alias_info with | Alias_field(reg,field) -> @@ -1532,7 +1540,7 @@ let doc_exp_ocaml, doc_let_ocaml = parens (separate space [call; parens (separate_map comma exp [e1;e2])]) | E_internal_let(lexp, eq_exp, in_exp) -> separate space [string "let"; - doc_lexp_ocaml lexp; (*Rewriter/typecheck should ensure this is only cast or id*) + doc_lexp_ocaml true lexp; (*Rewriter/typecheck should ensure this is only cast or id*) equals; string "ref"; exp eq_exp; @@ -1560,42 +1568,56 @@ let doc_exp_ocaml, doc_let_ocaml = and doc_case (Pat_aux(Pat_exp(pat,e),_)) = doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) - and doc_lexp_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = + and doc_lexp_ocaml top_call ((LEXP_aux(lexp,(l,annot))) as le) = let exp = top_exp false in match lexp with - | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (exp e) + | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ (doc_lexp_ocaml false v)) ^^ dot ^^ parens (exp e) | LEXP_vector_range(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ doc_lexp_ocaml v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> doc_lexp_ocaml v ^^ dot ^^ doc_id_ocaml id - | LEXP_id id -> doc_id_ocaml id - | LEXP_cast(typ,id) -> (doc_id_ocaml id) + parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) + | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id + | LEXP_id id | LEXP_cast(_,id) -> + let name = doc_id_ocaml id in + match annot,top_call with + | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false -> + string "!" ^^ name + | _ -> name and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml v) ^^ dot ^^ parens (top_exp false e) - | _ -> empty + | LEXP_vector(v,e) -> + (match annot with + | Base((_,t),_,_,_,_,_) -> + let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in + (match t_act.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> + parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e) + | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)) + | _ -> + parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)) + | _ -> empty and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = let exp = top_exp false in - let is_bit = match e_new_v with + let (is_bit,is_bitv) = match e_new_v with | E_aux(_,(_,Base((_,t),_,_,_,_,_))) -> (match t.t with | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) | Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) -> - true - | _ -> false) - | _ -> false in + (false,true) + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false) + | _ -> (false,false)) + | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml v)) ^^ + (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^ dot ^^ parens (exp e)) (exp e_new_v) | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ - doc_lexp_ocaml v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) | LEXP_field(v,id) -> - parens ((string "set_register_field") ^^ space ^^ - doc_lexp_ocaml v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) + parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ + doc_lexp_ocaml false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) | LEXP_id id | LEXP_cast (_,id) -> (match annot with | Base(_,Alias alias_info,_,_,_,_) -> @@ -1611,7 +1633,7 @@ let doc_exp_ocaml, doc_let_ocaml = dot ^^ parens (doc_int start)) (exp e_new_v) else - parens ((string (if is_bit then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ + parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) | Alias_pair(reg1,reg2) -> parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) @@ -1625,9 +1647,9 @@ let doc_exp_ocaml, doc_let_ocaml = in top_exp false, let_exp (*TODO Upcase and downcase type and constructors as needed*) -let doc_type_union_ocaml (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml_ctor id; string "of"; doc_typ_ocaml typ;] - | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor id] +let doc_type_union_ocaml n (Tu_aux(typ_u,_)) = match typ_u with + | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml_ctor n id; string "of"; doc_typ_ocaml typ;] + | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor n id] let rec doc_range_ocaml (BF_aux(r,_)) = match r with | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) @@ -1643,18 +1665,22 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc)) | TD_variant(id,nm,typq,ar,_) -> - let ar_doc = group (separate_map (break 1) doc_type_union_ocaml ar) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (doc_typquant_ocaml typq ar_doc) + let n = List.length ar in + let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in + doc_op equals + (concat [string "type"; space; doc_id_ocaml_type id;]) + (if n > 246 + then brackets (space ^^(doc_typquant_ocaml typq ar_doc)) + else (doc_typquant_ocaml typq ar_doc)) | TD_enum(id,nm,enums,_) -> - let enums_doc = group (separate_map (break 1 ^^ pipe) doc_id_ocaml_ctor enums) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (enums_doc) + let n = List.length enums in + let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor n) enums) in + doc_op equals + (concat [string "type"; space; doc_id_ocaml_type id;]) + (enums_doc) | TD_register(id,n1,n2,rs) -> - let doc_rid (r,id) = separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;] in - let doc_rids = group (separate_map (break 1) doc_rid rs) in + let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in + let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> let dir = i1 < i2 in diff --git a/src/type_check.ml b/src/type_check.ml index 59b5df44..4fb2cfc1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -258,14 +258,14 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | Some n -> Base(([],expect_t), Enum n, cs,pure_e,pure_e,default_bounds) in (P_aux(p,(l,pat_annot)),Envmap.from_list [(i,id_annot)],cs,default_bounds,expect_t) in (match Envmap.apply t_env i with - | Some(Base((params,t),Constructor,cs,efl,efr,bounds)) -> + | Some(Base((params,t),Constructor n,cs,efl,efr,bounds)) -> let t,cs,ef,_ = subst params false t cs efl in (match t.t with | Tfn({t = Tid "unit"},t',IP_none,ef) -> if conforms_to_t d_env false false t' expect_t then let tp,cp = type_consistent (Expr l) d_env Guarantee false t' expect_t in - (P_aux(P_app(id,[]),(l,tag_annot t Constructor)),Envmap.empty,cs@cp,bounds,tp) + (P_aux(P_app(id,[]),(l,tag_annot t (Constructor n))),Envmap.empty,cs@cp,bounds,tp) else default | Tfn(t1,t',IP_none,e) -> if conforms_to_t d_env false false t' expect_t @@ -285,28 +285,28 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*) (match Envmap.apply t_env i with | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined") - | Some(Base((params,t),Constructor,constraints,efl,efr,bounds)) -> + | Some(Base((params,t),Constructor n,constraints,efl,efr,bounds)) -> let t,dec_cs,_,_ = subst params false t constraints efl in (match t.t with | Tid id -> if pats = [] then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in - (P_aux(p,(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') + (P_aux(p,(l,cons_tag_annot t' (Constructor n) dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') else typ_error l ("Constructor " ^ i ^ " does not expect arguments") | Tfn(t1,t2,IP_none,ef) -> let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in (match pats with | [] -> let _ = type_consistent (Patt l) d_env Guarantee false unit_t t1 in - (P_aux(P_app(id,[]),(l,cons_tag_annot t' Constructor dec_cs)), + (P_aux(P_app(id,[]),(l,cons_tag_annot t' (Constructor n) dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') | [p] -> let (p',env,p_cs,bounds,u) = check_pattern envs emp_tag t1 p in (P_aux(P_app(id,[p']), - (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t') + (l,cons_tag_annot t' (Constructor n) dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t') | pats -> let (pats',env,p_cs,bounds,u) = match check_pattern envs emp_tag t1 (P_aux(P_tup(pats),(l,annot))) with | ((P_aux(P_tup(pats'),_)),env,constraints,bounds,u) -> (pats',env,constraints,bounds,u) | _ -> assert false in (P_aux(P_app(id,pats'), - (l,cons_tag_annot t' Constructor dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t')) + (l,cons_tag_annot t' (Constructor n) dec_cs)),env,dec_cs@p_cs@ret_cs,bounds,t')) | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor")) | Some(Base((params,t),tag,constraints,efl,efr,bounds)) -> typ_error l ("Identifier " ^ i ^ " used in pattern is not a union constructor")) @@ -478,12 +478,12 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | E_id id -> let i = id_to_string id in (match Envmap.apply t_env i with - | Some(Base((params,t),Constructor,cs,ef,_,bounds)) -> + | Some(Base((params,t),(Constructor n),cs,ef,_,bounds)) -> let t,cs,ef,_ = subst params false t cs ef in (match t.t with | Tfn({t = Tid "unit"},t',IP_none,ef) -> let e = E_aux(E_app(id, []), - (l, (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}), Constructor, cs, ef,pure_e, bounds)))) in + (l, (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}), (Constructor n), cs, ef,pure_e, bounds)))) in let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false b_env t' e expect_t in (e',t',t_env,cs@cs',nob,union_effects ef ef') | Tfn(t1,t',IP_none,e) -> @@ -596,13 +596,13 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tapp ("vector",[TA_nexp base;TA_nexp {nexp = rise};TA_ord o;(TA_typ {t=Tid "bit"})]) | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp { nexp = rise}; TA_ord o;(TA_typ {t=Tid "bit"})])}])-> - let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" + let f = match o.order with | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef" | _ -> (match d_env.default_o.order with - | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" - | _ -> "to_vec_inc") in + | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef" + | _ -> "to_vec_inc_undef") in let tannot = (l,Base(([],expect_t),External (Some f),[],ef,ef,b_env)) in E_aux(E_app((Id_aux((Id f),l)), - [(E_aux (E_internal_exp(tannot), tannot));simp_exp e l bit_t]),tannot),[],ef + [(E_aux (E_internal_exp(tannot), tannot));]),tannot),[],ef | _ -> simp_exp e l (new_t ()),[],ef)) in let t',cs',_,e' = type_coerce (Expr l) d_env Require false true b_env (get_e_typ e) e expect_t in (e',t',t_env,cs@cs',nob,effect) @@ -775,15 +775,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (match t_p.t with | Tfn(arg,ret,_,ef') -> check_parms arg lft rht | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in - (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" - i (t_to_string t_p) (t_to_string arg_t) in*) + let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n" + i (t_to_string t_p) (t_to_string arg_t) in (match (select_overload_variant d_env true overload_return variants arg_t) with | [] -> typ_error l ("No function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) | [Base((params,t),tag,cs,ef,_,b)] -> - (*let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) + let _ = Printf.eprintf "Selected an overloaded function for %s, + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in (match t.t with | Tfn(arg,ret,imp,ef') -> (match arg.t,arg_t.t with @@ -795,15 +795,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type")) | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function")) | variants -> - (*let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" - (List.length variants) in*) + let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" + (List.length variants) in (match (select_overload_variant d_env false true variants expect_t) with | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t)) | [Base((params,t),tag,cs,ef,_,b)] -> - (*let _ = Printf.eprintf "Selected an overloaded function for %s, - variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*) + let _ = Printf.eprintf "Selected an overloaded function for %s, + variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in (match t.t with | Tfn(arg,ret,imp,ef') -> (match arg.t,arg_t.t with @@ -859,9 +859,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let t_cs = CondCons((Expr l),Positive,None,c1p,then_c@then_c') in let e_cs = CondCons((Expr l),Negative,None,c1n,else_c@else_c') in let sub_effects = union_effects ef1 (union_effects then_ef else_ef) in + let resulting_env = Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env in (E_aux(E_if(cond',then',else'),(l,simple_annot_efr expect_t sub_effects)), - expect_t, - Envmap.intersect_merge (tannot_merge (Expr l) d_env true) then_env else_env, + expect_t, resulting_env, [BranchCons(Expr l, None, [t_cs;e_cs])], merge_bounds then_bs else_bs, (*TODO Should be an intersecting merge*) sub_effects) @@ -1299,7 +1299,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | E_exit e -> let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in (E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e) - | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _ -> + | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _ + | E_internal_plet _ | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker") and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) = @@ -1665,11 +1666,12 @@ let check_type_def envs (TD_aux(td,(l,annot))) = | TD_variant(id,nmscm,typq,arms,_) -> let id' = id_to_string id in let (params,typarms,constraints) = typq_to_params envs typq in + let num_arms = List.length arms in let ty = match params with | [] -> {t=Tid id'} | params -> {t = Tapp(id', typarms) }in - let tyannot = Base((params,ty),Constructor,constraints,pure_e,pure_e,nob) in - let arm_t input = Base((params,{t=Tfn(input,ty,IP_none,pure_e)}),Constructor,constraints,pure_e,pure_e,nob) in + let tyannot = Base((params,ty),Constructor num_arms,constraints,pure_e,pure_e,nob) in + let arm_t input = Base((params,{t=Tfn(input,ty,IP_none,pure_e)}),Constructor num_arms,constraints,pure_e,pure_e,nob) in let arms' = List.map (fun (Tu_aux(tu,l')) -> match tu with @@ -1841,8 +1843,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let check t_env tp_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> - (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" - (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) + let _ = Printf.eprintf "checking function %s : %s -> %s\n" + (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in let _, _ = type_consistent (Patt l) d_env Require false param_t t' in let exp',_,_,cs_e,_,ef = diff --git a/src/type_internal.ml b/src/type_internal.ml index 3c7d5ff6..660ef20a 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -85,7 +85,7 @@ type tag = | Emp_set | External of string option | Default - | Constructor + | Constructor of int | Enum of int | Alias of alias_inf | Spec @@ -328,7 +328,7 @@ let tag_to_string = function | External None -> "External" | External (Some s) -> "External " ^ s | Default -> "Default" - | Constructor -> "Constructor" + | Constructor _ -> "Constructor" | Enum _ -> "Enum" | Alias _ -> "Alias" | Spec -> "Spec" @@ -1446,6 +1446,9 @@ let mk_tup ts = {t = Ttup ts } let mk_pure_fun arg ret = {t = Tfn (arg,ret,IP_none,pure_e)} let mk_pure_imp arg ret var = {t = Tfn (arg,ret,IP_length (mk_nv var),pure_e)} +let lib_tannot param_typs func cs = + Base(param_typs, External func, cs, pure_e, pure_e, nob) + let mk_range n1 n2 = {t=Tapp("range",[TA_nexp n1;TA_nexp n2])} let mk_atom n1 = {t = Tapp("atom",[TA_nexp n1])} let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp start; TA_nexp size; TA_ord {order}; TA_typ typ])} @@ -1461,326 +1464,313 @@ let mk_bitwise_op name symb arity = then List.hd single_bit_vec_args,List.hd vec_args,List.hd bit_args,List.hd gen_args else mk_tup single_bit_vec_args,mk_tup vec_args,mk_tup bit_args, mk_tup gen_args in (symb, - Overload(Base(((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}), External (Some name),[],pure_e,pure_e,nob),true, - [Base(((mk_nat_params ["n";"m"]@mk_ord_params["o"]), mk_pure_fun varg vec_typ), - External (Some name),[],pure_e,pure_e,nob); - Base((["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg bit_t), - External(Some (name ^ "_range_bit")),[],pure_e,pure_e,nob); - Base(([],mk_pure_fun barg bit_t),External (Some (name ^ "_bit")),[],pure_e,pure_e,nob)])) + Overload(lib_tannot ((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}) (Some name) [], true, + [lib_tannot ((mk_nat_params ["n";"m"]@mk_ord_params["o"]), mk_pure_fun varg vec_typ) (Some name) []; + lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg bit_t) (Some (name ^ "_range_bit")) []; + lib_tannot ([],mk_pure_fun barg bit_t) (Some (name ^ "_bit")) []])) let initial_typ_env = Envmap.from_list [ - ("ignore",Base(([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t),External None,[],pure_e,pure_e,nob)); + ("ignore",lib_tannot ([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t) None []); ("+",Overload( - Base(((mk_typ_params ["a";"b";"c"]), - (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),External (Some "add"),[],pure_e,pure_e,nob), + lib_tannot ((mk_typ_params ["a";"b";"c"]), + (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) (Some "add") [], true, - [Base(((mk_nat_params ["n";"m"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) - (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))), - External (Some "add"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))), - External (Some "add_vec"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))), - External (Some "add_vec_vec_range"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "add_vec_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))), - External (Some "add_overflow_vec"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "add_vec_range_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "add_range_vec"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_sub (mk_2n (mk_nv "m")) n_one))))), - External (Some "add_range_vec_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)], - pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))), - External (Some "add_vec_bit"), [], pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))), - External (Some "add_bit_vec"), [], pure_e,pure_e,nob); + [lib_tannot ((mk_nat_params ["n";"m"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) + (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))) + (Some "add") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (Some "add_vec") []; + lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))) + (Some "add_vec_vec_range") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "add_vec_range") + [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (Some "add_overflow_vec") []; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "add_vec_range_range") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "add_range_vec") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_sub (mk_2n (mk_nv "m")) n_one))))) + (Some "add_range_vec_range") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (Some "add_vec_bit") []; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (Some "add_bit_vec") []; ])); ("+_s",Overload( - Base(((mk_typ_params ["a";"b";"c"]), - (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),External (Some "add"),[],pure_e,pure_e,nob), + lib_tannot ((mk_typ_params ["a";"b";"c"]), + (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) (Some "add") [], true, - [Base(((mk_nat_params ["n";"m"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) - (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))), - External (Some "add_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))), - External (Some "add_vec_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))), - External (Some "add_vec_vec_range_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "add_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))), - External (Some "add_overflow_vec_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "add_vec_range_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "add_range_vec_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))], - pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "add_range_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))], - pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))), - External (Some "add_vec_bit_signed"), [], pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))), - External (Some "add_overflow_vec_bit_signed"), [], pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))), - External (Some "add_bit_vec_signed"), [], pure_e,pure_e,nob); + [lib_tannot ((mk_nat_params ["n";"m"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) + (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))) + (Some "add_signed") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (Some "add_vec_signed") []; + lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_range (mk_nv "q") (mk_2n (mk_nv "n"))))) + (Some "add_vec_vec_range_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "add_vec_range_signed") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (Some "add_overflow_vec_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "add_vec_range_range_signed") + [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)]; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "add_range_vec_signed") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "add_range_vec_range_signed") + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))]; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (Some "add_vec_bit_signed") []; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (Some "add_overflow_vec_bit_signed") []; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")))) + (Some "add_bit_vec_signed") []; ])); ("-_s",Overload( - Base(((mk_typ_params ["a";"b";"c"]), - (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - External (Some "minus"),[],pure_e,pure_e,nob), + lib_tannot ((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) + (Some "minus") [], true, - [Base(((mk_nat_params["n";"m"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) - (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))), - External (Some "minus"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))), - External (Some "minus_vec_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "minus_vec_range_signed"), - [],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "minus_vec_range_range_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "minus_range_vec_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "minus_range_vec_range_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))), - External (Some "minus_overflow_vec_signed"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))), - External (Some "minus_overflow_vec_bit_signed"), [], pure_e,pure_e,nob); + [lib_tannot ((mk_nat_params["n";"m"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) + (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))) + (Some "minus") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (Some "minus_vec_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "minus_vec_range_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "minus_vec_range_range_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "minus_range_vec_signed") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "minus_range_vec_range_signed") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (Some "minus_overflow_vec_signed") []; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (Some "minus_overflow_vec_bit_signed") []; ])); ("-",Overload( - Base(((mk_typ_params ["a";"b";"c"]), - (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - External (Some "minus"),[],pure_e,pure_e,nob), + lib_tannot ((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) + (Some "minus") [], true, - [Base(((mk_nat_params["n";"m"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) - (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))), - External (Some "minus"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))), - External (Some "minus_vec"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["m";"n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_atom (mk_nv "m")))), External (Some "minus_vec_vec_range"),[],pure_e,pure_e,nob); (*Need a bound on m*) - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "minus_vec_range"),[],pure_e,pure_e,nob); (*Need a bound on o?*) - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); - mk_atom (mk_nv "o")]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "minus_vec_range_range"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "minus_range_vec"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); - mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) - (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))), - External (Some "minus_range_vec_range"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); - mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))), - External (Some "minus_overflow_vec"),[],pure_e,pure_e,nob); - Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), - (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) - (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))), - External (Some "minus_overflow_vec_bit"), [], pure_e,pure_e,nob); + [lib_tannot ((mk_nat_params["n";"m"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) + (mk_atom (mk_sub (mk_nv "n") (mk_nv "m"))))) + (Some "minus") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")))) + (Some "minus_vec") []; + lib_tannot ((mk_nat_params ["m";"n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_atom (mk_nv "m")))) (Some "minus_vec_vec_range") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "minus_vec_range") []; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "minus_vec_range_range") []; + lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) + (Some "minus_range_vec") []; + lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");]) + (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m")))))) + (Some "minus_range_vec_range") []; + lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); + mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t]))) + (Some "minus_overflow_vec") []; + lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t]))) + (Some "minus_overflow_vec_bit") []; ])); ("*",Overload( - Base(((mk_typ_params ["a";"b";"c"]), - (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]){t=Tvar "c"})), - External (Some "multiply"),[],pure_e,pure_e,nob), + lib_tannot ((mk_typ_params ["a";"b";"c"]), + (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]){t=Tvar "c"})) + (Some "multiply") [], true, - [Base(((mk_nat_params["n";"m"]), - (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) - (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))), - External (Some "multiply"), [],pure_e,pure_e,nob); + [lib_tannot ((mk_nat_params["n";"m"]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) + (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))) + (Some "multiply") []; Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "n") (mk_nv "n"))))), - External (Some "multiply_vec"), [],pure_e,pure_e,nob); + (External (Some "multiply_vec")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), - External (Some "mult_range_vec"),[],pure_e,pure_e,nob); + (External (Some "mult_range_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))), - External (Some "mult_vec_range"),[],pure_e,pure_e,nob); + (External (Some "mult_vec_range")),[],pure_e,pure_e,nob); ])); ("*_s",Overload( Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]){t=Tvar "c"})), - External (Some "multiply"),[],pure_e,pure_e,nob), + (External (Some "multiply")),[],pure_e,pure_e,nob), true, [Base(((mk_nat_params["n";"m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))), - External (Some "multiply_signed"), [],pure_e,pure_e,nob); + (External (Some "multiply_signed")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))))), - External (Some "multiply_vec_signed"), [],pure_e,pure_e,nob); + (External (Some "multiply_vec_signed")), [],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), - External (Some "mult_range_vec_signed"),[],pure_e,pure_e,nob); + (External (Some "mult_range_vec_signed")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))), - External (Some "mult_vec_range_signed"),[],pure_e,pure_e,nob); + (External (Some "mult_vec_range_signed")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))); bit_t;bit_t]))), - External (Some "mult_overflow_vec_signed"), [],pure_e,pure_e,nob); + (External (Some "mult_overflow_vec_signed")), [],pure_e,pure_e,nob); ])); ("**", Base(((mk_nat_params ["o"]), (mk_pure_fun (mk_tup [(mk_atom n_two); (mk_atom (mk_nv "o"))]) (mk_atom (mk_2n (mk_nv "o"))))), - External (Some "power"), [],pure_e,pure_e,nob)); + (External (Some "power")), [],pure_e,pure_e,nob)); ("mod", Overload( Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - External (Some "modulo"),[],pure_e,pure_e,nob), + (External (Some "modulo")),[],pure_e,pure_e,nob), true, [Base(((mk_nat_params["n";"o";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ; mk_atom (mk_nv "o")]) (mk_range n_zero (mk_sub (mk_nv "o") n_one)))), - External (Some "modulo"), + (External (Some "modulo")), [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_range n_one (mk_nv "o")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "mod_vec_range"), + (External (Some "mod_vec_range")), [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "mod_vec"),[],pure_e,pure_e,nob)])); + (External (Some "mod_vec")),[],pure_e,pure_e,nob)])); ("quot", Overload( Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - External (Some "quot"),[],pure_e,pure_e,nob), + (External (Some "quot")),[],pure_e,pure_e,nob), true, [Base(((mk_nat_params["n";"m";"o";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) (mk_atom (mk_nv "o")))), - External (Some "quot"),[GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one); + (External (Some "quot")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one); LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee, (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))], pure_e,pure_e,nob); @@ -1788,24 +1778,24 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], + (External (Some "quot_vec")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), - External (Some "quot_overflow_vec"), + (External (Some "quot_overflow_vec")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], pure_e,pure_e,nob)])); ("quot_s", Overload( Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - External (Some "quot_signed"),[],pure_e,pure_e,nob), + (External (Some "quot_signed")),[],pure_e,pure_e,nob), true, [Base(((mk_nat_params["n";"m";"o";"p";"q";"r"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "q") (mk_nv "r")))), - External (Some "quot_signed"), + (External (Some "quot_signed")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one); LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")], pure_e,pure_e,nob); @@ -1813,39 +1803,39 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), - External (Some "quot_vec_signed"), + (External (Some "quot_vec_signed")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")]) (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))), - External (Some "quot_overflow_vec_signed"), + (External (Some "quot_overflow_vec_signed")), [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob); ])); ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_atom (mk_nv "m")))), - External (Some "length"),[],pure_e,pure_e,nob)); + (External (Some "length")),[],pure_e,pure_e,nob)); (* incorrect types for typechecking processed sail code; do we care? *) ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]), (mk_pure_imp (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "p") (mk_nv "o")) "o")), - External (Some "mask"), + (External (Some "mask")), [GtEq(Specc(Parse_ast.Int("mask",None)),Guarantee, (mk_nv "m"), (mk_nv "o"))],pure_e,pure_e,nob)); (*TODO These should be IP_start *) ("to_vec_inc",Base(([("a",{k=K_Typ})],{t=Tfn(nat_typ,{t=Tvar "a"},IP_none,pure_e)}), - External None,[],pure_e,pure_e,nob)); + (External None),[],pure_e,pure_e,nob)); ("to_vec_dec",Base(([("a",{k=K_Typ})],{t=Tfn(nat_typ,{t=Tvar "a"},IP_none,pure_e)}), - External None,[],pure_e,pure_e,nob)); + (External None),[],pure_e,pure_e,nob)); (*Correct types again*) ("==", Overload( Base((mk_typ_params ["a";"b"],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "eq"),[],pure_e,pure_e,nob), + (External (Some "eq")),[],pure_e,pure_e,nob), false, [Base((mk_nat_params["n";"m";], mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ;mk_atom (mk_nv "m")]) bit_t), - External (Some "eq"), + (External (Some "eq")), [Predicate(Specc(Parse_ast.Int("==",None)), Eq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"), NtEq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"))], @@ -1855,25 +1845,25 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), - External (Some "eq_range_vec"),[],pure_e,pure_e,nob); + (External (Some "eq_range_vec")),[],pure_e,pure_e,nob); (* == : [:'o:] * bit['n] -> bit_t *) Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), - External (Some "eq_vec_range"),[],pure_e,pure_e,nob); + (External (Some "eq_vec_range")),[],pure_e,pure_e,nob); Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "eq"),[],pure_e,pure_e,nob)])); + (External (Some "eq")),[],pure_e,pure_e,nob)])); ("!=",Base((["a",{k=K_Typ}; "b",{k=K_Typ}], (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "neq"),[],pure_e,pure_e,nob)); + (External (Some "neq")),[],pure_e,pure_e,nob)); ("<", Overload( Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "lt"),[],pure_e,pure_e,nob), + (External (Some "lt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n"; "m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ;mk_atom (mk_nv "m")]) bit_t)), - External (Some "lt"), + (External (Some "lt")), [Predicate(Specc(Parse_ast.Int("<",None)), Lt(Specc(Parse_ast.Int("<",None)),Guarantee, mk_nv "n", mk_nv "m"), GtEq(Specc(Parse_ast.Int("<",None)),Guarantee, mk_nv "n", mk_nv "m"))], @@ -1881,20 +1871,20 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "lt_vec"),[],pure_e,pure_e,nob); + (External (Some "lt_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o"]@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), - External (Some "lt_vec_range"), [], pure_e,pure_e, nob); + (External (Some "lt_vec_range")), [], pure_e,pure_e, nob); ])); ("<_s", Overload( Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "lt"),[],pure_e,pure_e,nob), + (External (Some "lt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n"; "m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) bit_t)), - External (Some "lt_signed"), + (External (Some "lt_signed")), [Predicate(Specc(Parse_ast.Int("<_s",None)), Lt(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_nv "n", mk_nv "m"), GtEq(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_nv "n", mk_nv "m"))], @@ -1902,16 +1892,16 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "lt_vec_signed"),[],pure_e,pure_e,nob); + (External (Some "lt_vec_signed")),[],pure_e,pure_e,nob); ])); ("<_u", Overload( Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "lt"),[],pure_e,pure_e,nob), + (External (Some "lt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n"; "m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) bit_t)), - External (Some "lt_unsigned"), + (External (Some "lt_unsigned")), [Predicate(Specc(Parse_ast.Int("<",None)), Lt(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_nv "n", mk_nv "m"), GtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_nv "n", mk_nv "m"))], @@ -1919,16 +1909,16 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "lt_vec_unsigned"),[],pure_e,pure_e,nob); + (External (Some "lt_vec_unsigned")),[],pure_e,pure_e,nob); ])); (">", Overload( Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "gt"),[],pure_e,pure_e,nob), + (External (Some "gt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n";"m"]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")]) bit_t)), - External (Some "gt"), + (External (Some "gt")), [Predicate(Specc(Parse_ast.Int(">",None)), Gt(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "n", mk_nv "m"), LtEq(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "n", mk_nv "m"))], @@ -1936,20 +1926,20 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "gt_vec"),[],pure_e,pure_e,nob); + (External (Some "gt_vec")),[],pure_e,pure_e,nob); Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); mk_atom (mk_nv "o")]) bit_t)), - External (Some "gt_vec_range"), [], pure_e,pure_e, nob); + (External (Some "gt_vec_range")), [], pure_e,pure_e, nob); ])); (">_s", Overload( Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "gt"),[],pure_e,pure_e,nob), + (External (Some "gt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n";"m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) bit_t)), - External (Some "gt_signed"), + (External (Some "gt_signed")), [Predicate(Specc(Parse_ast.Int(">_s",None)), Gt(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "n", mk_nv "m"), LtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_nv "m"))], @@ -1957,16 +1947,16 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "gt_vec_signed"),[],pure_e,pure_e,nob); + (External (Some "gt_vec_signed")),[],pure_e,pure_e,nob); ])); (">_u", Overload( Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), - External (Some "gt"),[],pure_e,pure_e,nob), + (External (Some "gt")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n";"m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) bit_t)), - External (Some "gt_unsigned"), + (External (Some "gt_unsigned")), [Predicate(Specc(Parse_ast.Int(">_u",None)), Gt(Specc(Parse_ast.Int(">_u",None)),Guarantee, mk_nv "n", mk_nv "m"), LtEq(Specc(Parse_ast.Int(">_u",None)),Guarantee, mk_nv "n", mk_nv "n"))], @@ -1974,74 +1964,90 @@ let initial_typ_env = Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "gt_vec_unsigned"),[],pure_e,pure_e,nob); + (External (Some "gt_vec_unsigned")),[],pure_e,pure_e,nob); ])); ("<=", Overload( - Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "lteq"),[],pure_e,pure_e,nob), + Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)), + (External (Some "lteq")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n"; "m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) bit_t)), - External (Some "lteq"), + (External (Some "lteq")), [Predicate(Specc(Parse_ast.Int("<=",None)), LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "m"), Gt(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "m"))], pure_e,pure_e,nob); + Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) bit_t)), + (External (Some "lteq_vec_range")), [], pure_e,pure_e, nob); + Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), + (External (Some "lteq_range_vec")), [], pure_e,pure_e, nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "lteq_vec"),[],pure_e,pure_e,nob); + (External (Some "lteq_vec")),[],pure_e,pure_e,nob); ])); ("<=_s", Overload( Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "lteq"),[],pure_e,pure_e,nob), + (External (Some "lteq")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n"; "m";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) bit_t)), - External (Some "lteq_signed"), + (External (Some "lteq_signed")), [LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "o"); LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "m",mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "lteq_vec_signed"),[],pure_e,pure_e,nob); + (External (Some "lteq_vec_signed")),[],pure_e,pure_e,nob); ])); (">=", Overload( Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "gteq"),[],pure_e,pure_e,nob), + (External (Some "gteq")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), - External (Some "gteq"), + (External (Some "gteq")), [GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "n", mk_nv "o"); GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "m", mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "gteq_vec"),[],pure_e,pure_e,nob); + (External (Some "gteq_vec")),[],pure_e,pure_e,nob); + Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_atom (mk_nv "o")]) bit_t)), + (External (Some "gteq_vec_range")), [], pure_e,pure_e, nob); + Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "o"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)), + (External (Some "gteq_range_vec")), [], pure_e,pure_e, nob); ])); (">=_s", Overload( Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), - External (Some "gteq"),[],pure_e,pure_e,nob), + (External (Some "gteq")),[],pure_e,pure_e,nob), false, [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), - External (Some "gteq_signed"), + (External (Some "gteq_signed")), [GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "n", mk_nv "o"); GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "m", mk_nv "p")], pure_e,pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"); mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), - External (Some "gteq_vec_signed"),[],pure_e,pure_e,nob); + (External (Some "gteq_vec_signed")),[],pure_e,pure_e,nob); ])); - ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),External (Some "is_one"),[],pure_e,pure_e,nob)); + ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),(External (Some "is_one")),[],pure_e,pure_e,nob)); ("signed",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})], (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")) (mk_atom (mk_nv "o")))), diff --git a/src/type_internal.mli b/src/type_internal.mli index f38a7fe5..ac1ae525 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -87,7 +87,7 @@ type tag = | Emp_set (* Local mutable expression being set *) | External of string option (* External function or register name *) | Default (* Variable has default type, has not been bound *) - | Constructor (* Variable is a data constructor *) + | Constructor of int (* Variable is a data constructor, int says how many variants are in this family *) | Enum of int (* Variable came from an enumeration, int tells me the highest possible numeric value *) | Alias of alias_inf (* Variable came from a register alias *) | Spec (* Variable came from a val specification *) |