diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 36 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 2 | ||||
| -rw-r--r-- | src/pretty_print.ml | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 58 | ||||
| -rw-r--r-- | src/type_internal.ml | 46 | ||||
| -rw-r--r-- | src/type_internal.mli | 4 |
6 files changed, 121 insertions, 29 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index e994fdfe..0b7bb74a 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -49,6 +49,28 @@ let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) = let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in V_vector idx inc (List.map apply (List.zip v v')) +let bitwise_xor_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with + | (L_zero,L_zero) -> V_lit (L_aux l1 loc1) + | (L_zero,L_one) -> V_lit (L_aux l2 loc2) + | (L_one,L_zero) -> V_lit (L_aux l1 loc1) + | (L_one,L_one) -> V_lit (L_aux L_zero loc1) +end;; + +let bitwise_or_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with + | (L_zero,L_zero) -> V_lit (L_aux l1 loc1) + | (L_zero,L_one) -> V_lit (L_aux l2 loc2) + | (L_one,L_zero) -> V_lit (L_aux l1 loc1) + | (L_one,L_one) -> V_lit (L_aux l1 loc1) +end;; + +let bitwise_and_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with + | (L_zero,L_zero) -> V_lit (L_aux l1 loc1) + | (L_zero,L_one) -> V_lit (L_aux l1 loc1) + | (L_one,L_zero) -> V_lit (L_aux l2 loc2) + | (L_one,L_one) -> V_lit (L_aux l1 loc1) +end;; + + (* BitSeq expects LSB first. * By convention, MSB is on the left, so increasing = Big-Endian (MSB0), * hence MSB first. @@ -91,6 +113,15 @@ let arith_op_vec_range op (V_tuple args) = match args with else arith_op_vec op (V_tuple [l1;(to_vec_dec (List.length cs) n)]) end ;; +let arith_op_range_vec_range op (V_tuple args) = match args with + | [n;(V_vector _ _ _ as l2)] -> + arith_op op (V_tuple [n;(to_num true l2)]) +end ;; +let arith_op_vec_range_range op (V_tuple args) = match args with + | [(V_vector _ _ _ as l1);n] -> + arith_op op (V_tuple [(to_num true l1);n]) +end ;; + let compare_op op (V_tuple args) = match args with | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> if (op x y) @@ -116,7 +147,9 @@ let function_map = [ ("add", arith_op (+)); ("add_vec", arith_op_vec (+)); ("add_vec_range", arith_op_vec_range (+)); + ("add_vec_range_range", arith_op_vec_range_range (+)); ("add_range_vec", arith_op_range_vec (+)); + ("add_range_vec_range", arith_op_range_vec_range (+)); ("minus", arith_op (-)); ("minus_vec", arith_op_vec (-)); ("eq", eq); @@ -132,8 +165,11 @@ let function_map = [ ("bitwise_not", bitwise_not); ("bitwise_not_bit", bitwise_not_bit); ("bitwise_and", bitwise_binop (&&)); + ("bitwise_and_bit", bitwise_and_bit); ("bitwise_or", bitwise_binop (||)); + ("bitwise_or_bit", bitwise_or_bit); ("bitwise_xor", bitwise_binop xor); + ("bitwise_xor_bit", bitwise_xor_bit); ("lt", compare_op (<)); ("gt", compare_op (>)); ("lt_vec", compare_op_vec (<)); diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 7e992e3a..45768966 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -214,7 +214,7 @@ let run ?(reg=Reg.empty) ?(mem=Mem.empty) (name, test) = - let mode = {eager_eval = true} in + let mode = {eager_eval = false} in let rec loop env = function | Value (v, _) -> debugf "%s: returned %s\n" name (val_to_string v); true, env | Action (a, s) -> diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 7ade113c..6145c7c4 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -363,7 +363,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot (* XXX missing cases *) - | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false + | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false in print_e ppf e @@ -844,7 +844,7 @@ let doc_exp, doc_let = (* doc_op (doc_id op) (exp l) (exp r) *) (* XXX missing case AAA internal_cast should never have an overload, if it's been seen it's a bug *) - | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false + | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> diff --git a/src/type_check.ml b/src/type_check.ml index 5311b0b6..d198b525 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -470,7 +470,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (ret_t,cs_r',e') = type_coerce (Expr l) d_env false ret (E_aux(E_app(id, parms'),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef')) | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) - | Some(Overload(Base((params,t),tag,cs,ef),variants)) -> + | Some(Overload(Base((params,t),tag,cs,ef),overload_return,variants)) -> let t_p,cs_p,ef_p = subst params t cs ef in let args,arg_t,arg_cs,arg_ef = (match t_p.t with @@ -486,9 +486,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let ((E_aux(E_tuple parms',tannot')),arg_t,_,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,NoTyp))) in (parms',arg_t,cs',ef_p)) | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in - (match (select_overload_variant d_env variants arg_t) with - | NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) - | Base((params,t),tag,cs,ef) -> + (match (select_overload_variant d_env true overload_return variants arg_t) with + | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) + | [Base((params,t),tag,cs,ef)] -> (match t.t with | Tfn(arg,ret,ef') -> let args',arg_cs' = @@ -502,8 +502,28 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp parms',cs) in let (ret_t,cs_r,e') = type_coerce (Expr l) d_env false ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in - (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef')) - | _ -> assert false)) + (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef')) + | _ -> assert false) + | variants' -> + (match select_overload_variant d_env false true variants' expect_t with + | [] -> typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t)) + | [Base((params,t),tag,cs,ef)] -> + (match t.t with + |Tfn(arg,ret,ef') -> + let args',arg_cs' = + (match args with + | [parm] -> + let _,cs,parm' = type_coerce (Expr l) d_env false arg_t parm arg in + [parm'],cs + | parms -> + let (_,cs,(E_aux(E_tuple parms',tannot'))) = + type_coerce (Expr l) d_env false arg_t (E_aux(E_tuple parms,(l,NoTyp))) arg in + parms',cs) in + let (ret_t,cs_r,e') = + type_coerce (Expr l) d_env false ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in + (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef')) + | _ -> assert false) + | _ -> typ_error l ("More than one function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " and returns " ^ (t_to_string expect_t) ^ ". Try adding a cast"))) | _ -> typ_error l ("Unbound function " ^ i)) | E_app_infix(lft,op,rht) -> let i = id_to_string op in @@ -520,7 +540,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let ret_t,cs_r',e' = type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef') | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) - | Some(Overload(Base((params,t),tag,cs,ef),variants)) -> + | Some(Overload(Base((params,t),tag,cs,ef),overload_return,variants)) -> let t_p,cs_p,ef_p = subst params t cs ef in let lft',rht',arg_t,arg_cs,arg_ef = (match t_p.t with @@ -529,9 +549,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (lft',rht',arg_t,cs',ef') | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in (*let _ = Printf.printf "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 variants arg_t) with - | NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) - | Base((params,t),tag,cs,ef) -> + (match (select_overload_variant d_env true overload_return variants arg_t) with + | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t)) + | [Base((params,t),tag,cs,ef)] -> (*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,ef') -> @@ -543,7 +563,23 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,union_effects ef_p (union_effects arg_ef ef')) |_ -> assert false) - | _ -> assert false)) + | _ -> assert false) + | variants -> + (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)] -> + (match t.t with + | Tfn(arg,ret,ef') -> + (match arg.t,arg_t.t with + | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) -> + let (_,cs_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in + let (_,cs_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in + let (ret_t,cs_r,e') = + type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in + (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,union_effects ef_p (union_effects arg_ef ef')) + |_ -> assert false) + | _ -> assert false) + | _ -> typ_error l ("More than one function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t) ^ ". Try adding a cast"))) | _ -> typ_error l ("Unbound infix function " ^ i)) | E_tuple(exps) -> (match expect_t.t with diff --git a/src/type_internal.ml b/src/type_internal.ml index f8799d37..8423ecf5 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -95,7 +95,7 @@ type t_params = (string * kind) list type tannot = | NoTyp | Base of (t_params * t) * tag * nexp_range list * effect - | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *) + | Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the boolean indicates whether the overloaded functions can use the return type; the list includes all variants. All t to be Tfn *) (*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*) type 'a emap = 'a Envmap.t @@ -178,7 +178,7 @@ let rec tannot_to_string = function | NoTyp -> "No tannot" | Base((vars,t),tag,ncs,ef) -> "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef - | Overload(poly,variants) -> + | Overload(poly,_,variants) -> "Overloaded: poly = " ^ tannot_to_string poly let rec effect_remove_dups = function @@ -758,7 +758,7 @@ let mk_bitwise_op name symb arity = let gen_args = Array.to_list (Array.make arity {t = Tvar "a"}) in let varg,barg,garg = if (arity = 1) then List.hd vec_args,List.hd bit_args,List.hd gen_args else 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), + (symb,Overload(Base(((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}), External (Some name),[],pure_e),true, [Base((["n",{k=K_Nat}; "o",{k=K_Ord}], mk_pure_fun varg vec_typ),External (Some name),[],pure_e); Base(([],mk_pure_fun barg bit_t),External (Some (name ^ "_bit")),[],pure_e)])) @@ -767,6 +767,7 @@ let initial_typ_env = ("ignore",Base(([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t),External None,[],pure_e)); ("+",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), + true, [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")]) (mk_range (mk_add (mk_nv "n") (mk_nv "o")) (mk_add (mk_nv "m") (mk_nv "p"))))), @@ -781,12 +782,25 @@ let initial_typ_env = (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_vec_range"), [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); + Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); + mk_range (mk_nv "o") (mk_nv "p")]) + (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), + External (Some "add_vec_range_range"), + [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_range_vec"), [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e); + Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); + mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) + (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), + External (Some "add_range_vec_range"), + [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); + Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t]) (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))), @@ -802,6 +816,7 @@ let initial_typ_env = External (Some "multiply"),[],pure_e)); ("-",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), + true, [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")]) @@ -829,6 +844,7 @@ let initial_typ_env = Overload(Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "mod"),[],pure_e), + true, [Base(((mk_nat_params["n";"m";"o"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") {nexp = Nconst zero}]) (mk_range {nexp = Nconst zero} (mk_sub (mk_nv "o") {nexp = Nconst one})))), @@ -842,6 +858,7 @@ let initial_typ_env = 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), + 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")))), @@ -861,6 +878,7 @@ let initial_typ_env = ("to_vec_dec",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e)); ("==", 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), + false, [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})], {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "eq"), [Eq(Specc(Parse_ast.Int("==",None)), @@ -870,6 +888,7 @@ let initial_typ_env = ("!=",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e)); ("<", Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e), + false, [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})], {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "lt_vec"), [LtEq(Specc(Parse_ast.Int("<",None)), @@ -880,6 +899,7 @@ let initial_typ_env = mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])},bit_t,pure_e)}), External (Some "lt"),[],pure_e);])); (">", Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e), + false, [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})], {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "gt_vec"), [GtEq(Specc(Parse_ast.Int(">",None)), @@ -1374,7 +1394,7 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 = and type_coerce co d_env is_explicit t1 e t2 = type_coerce_internal co d_env is_explicit t1 [] e t2 [];; let rec conforms_to_t spec actual = - (*let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in*) + let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in match spec.t,actual.t with | Tuvar _,_ -> true | Ttup ss, Ttup acs -> (List.length ss = List.length acs) && List.for_all2 conforms_to_t ss acs @@ -1398,14 +1418,14 @@ and conforms_to_ta spec actual = | TA_eft s, TA_eft a -> conforms_to_e s a | _ -> false and conforms_to_n spec actual = - (*let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in*) + let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in match spec.nexp,actual.nexp with | Nuvar _,_ -> true | Nconst si,Nconst ai -> eq_big_int si ai - | _,_ -> false + | _,_ -> true and conforms_to_o spec actual = match spec.order,actual.order with - | Ouvar _,_ | Oinc,Oinc | Odec,Odec -> true + | Ouvar _,_ | Oinc,Oinc | Odec,Odec | _, Ouvar _ -> true | _,_ -> false and conforms_to_e spec actual = match spec.effect,actual.effect with @@ -1413,18 +1433,18 @@ and conforms_to_e spec actual = | _,Euvar _ -> false | _,_ -> false -let rec select_overload_variant d_env variants actual_type = +let rec select_overload_variant d_env params_check get_all variants actual_type = match variants with - | [] -> NoTyp - | NoTyp::variants | Overload _::variants -> select_overload_variant d_env variants actual_type + | [] -> [] + | NoTyp::variants | Overload _::variants -> select_overload_variant d_env params_check get_all variants actual_type | Base((parms,t),tag,cs,ef)::variants -> let t,cs,ef = subst parms t cs ef in let t,cs' = get_abbrev d_env t in (match t.t with | Tfn(a,r,e) -> - if conforms_to_t a actual_type - then Base(([],t),tag,cs@cs',ef) - else select_overload_variant d_env variants actual_type + if (if params_check then conforms_to_t a actual_type else conforms_to_t actual_type r) + then (Base(([],t),tag,cs@cs',ef))::(if get_all then (select_overload_variant d_env params_check get_all variants actual_type) else []) + else select_overload_variant d_env params_check get_all variants actual_type | _ -> assert false (*Turn into unreachable error*)) let rec in_constraint_env = function diff --git a/src/type_internal.mli b/src/type_internal.mli index 2aff6db3..7c0c2645 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -93,7 +93,7 @@ type t_params = (string * kind) list type tannot = | NoTyp | Base of (t_params * t) * tag * nexp_range list * effect - | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *) + | Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *) (*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*) type 'a emap = 'a Envmap.t @@ -142,7 +142,7 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list) val normalize_nexp : nexp -> nexp val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*) -val select_overload_variant : def_envs -> tannot list -> t -> tannot +val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> tannot list (*May raise an exception if a contradiction is found*) val resolve_constraints : nexp_range list -> nexp_range list |