diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 47 | ||||
| -rw-r--r-- | src/type_internal.ml | 24 | ||||
| -rw-r--r-- | src/type_internal.mli | 7 |
3 files changed, 41 insertions, 37 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 5117e9c2..d4739543 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -88,24 +88,21 @@ let rec typ_to_t imp_ok fun_ok (Typ_aux(typ,l)) = match typ with | Typ_id i -> {t = Tid (id_to_string i)} | Typ_var (Kid_aux((Var i),l')) -> {t = Tvar i} - (*Need to look here for the implicit parameter within the ty1, so typ_to_t may need an optional additional return*) | Typ_fn (ty1,ty2,e) -> if fun_ok - then begin + then if has_typ_app false "implicit" ty1 - then if imp_ok + then + if imp_ok then (match extract_if_first true "implicit" ty1 with | Some(imp,new_ty1) -> (match imp with | Typ_app(_,[Typ_arg_aux(Typ_arg_nexp ((Nexp_aux(n,l')) as ne),_)]) -> - (match n with - | Nexp_var (Kid_aux((Var i),l')) -> - {t = Tfn (trans new_ty1, trans ty2, IP_var (anexp_to_nexp ne), aeffect_to_effect e)} - | _ -> typ_error l' "Declaring an implicit parameter related to an Nat term must be a variable") - | _ -> typ_error l "Declaring an implicit parameter requires a variable") - | None -> typ_error l "A function type with an implicit parameter must have the implicit declaration first") - else typ_error l "This function type has an (possibly two) implicit parameter that is not permitted here" - else {t = Tfn (trans ty1,trans ty2,IP_none,aeffect_to_effect e)} end - else typ_error l "Function types are not permitted here" + {t = Tfn (trans new_ty1, trans ty2, IP_user (anexp_to_nexp ne), aeffect_to_effect e)} + | _ -> typ_error l "Declaring an implicit parameter requires a Nat specification") + | None -> typ_error l "A function type with an implicit parameter must declare the implicit first") + else typ_error l "This function has one (or more) implicit parameter(s) not permitted here" + else {t = Tfn (trans ty1,trans ty2,IP_none,aeffect_to_effect e)} + else typ_error l "Function types are only permitted at the top level." | Typ_tup(tys) -> {t = Ttup (List.map trans tys) } | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) } | Typ_wild -> new_t () @@ -166,7 +163,6 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env)) as env) qis : (t_params * t_ | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs))) - let typq_to_params envs (TypQ_aux(tq,l)) = match tq with | TypQ_tq(qis) -> quants_to_consts envs qis @@ -591,23 +587,22 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) in let check_result ret imp tag cs ef parms = - (*TODO How do I want to pass the information about start along?*) - - (* TODO MAJOR!!!! It may be that the return is a tuple or some bigger structure. THIS IS OK. I need to tie the variable in the implicit to the variable in the type and then put that type here. - COME BACK AND look at return type more, look in bounds etc*) match (imp,imp_param) with - | (IP_length,None) | (IP_var _,None) -> + | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) -> (*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*) - (*TODO may need to use bindings here?*) - let internal_exp = match expect_t.t,ret.t with + (*let internal_exp = + let internal_typ = {t= Toptions(expect_t,Some ret)} in + let annot = Base(([],internal_typ),Emp_local,[],pure_e,b_env) in + E_aux(E_internal_exp(l,annot),(l,simple_annot nat_t)) in*) + let internal_exp = match expect_t.t,ret.t with | Tapp("vector",_),_ -> - (*let _ = Printf.printf "adding internal exp on expext_t: %s %s \n" (t_to_string expect_t) (t_to_string ret) in*) E_aux (E_internal_exp (l,simple_annot expect_t), (l,simple_annot nat_t)) - | _,Tapp("vector",_) -> + | _,Tapp("vector",_) -> E_aux (E_internal_exp (l,simple_annot ret), (l,simple_annot nat_t)) | _ -> typ_error l (i ^ " expected either the return type or the expected type to be a vector") in - type_coerce (Expr l) d_env false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t - | (IP_length,Some ne) | (IP_var _,Some ne) -> + type_coerce (Expr l) + d_env false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> (*let _ = Printf.printf "implicit length or var required with imp_param\n" in*) let internal_exp = (match expect_t.t,ret.t with | Tapp("vector",[_;TA_nexp len;_;_]),_ -> @@ -683,7 +678,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") in let check_result ret imp tag cs ef lft rht = match imp with - | IP_length -> + | IP_length _ -> let internal_exp = match expect_t.t,ret.t with | Tapp("vector",_),_ -> E_aux (E_internal_exp (l,simple_annot expect_t), (l, simple_annot nat_t)) @@ -1715,7 +1710,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let _,cs = type_consistent (Specc l) d_env false t u in (*let _ = Printf.printf "valspec consistent with declared type for %s\n" id in*) let imp_param = match u.t with - | Tfn(_,_,IP_var n,_) -> Some n + | Tfn(_,_,IP_user n,_) -> Some n | _ -> None in let t_env = if is_rec then t_env else Envmap.remove t_env id in let funcls,cs_ef = check t_env imp_param in diff --git a/src/type_internal.ml b/src/type_internal.ml index 7a745ee6..d93f8f99 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -36,7 +36,7 @@ and t_aux = | Tuvar of t_uvar and t_uvar = { index : int; mutable subst : t option } and implicit_parm = - | IP_none | IP_length | IP_start | IP_var of nexp + | IP_none | IP_length of nexp | IP_start of nexp | IP_user of nexp and nexp = { mutable nexp : nexp_aux } and nexp_aux = | Nvar of string @@ -348,6 +348,13 @@ let rec get_var n = | Nmult (_,n1) -> get_var n1 | _ -> None +let rec get_all_nvar n = + match n.nexp with + | Nvar _ | Nuvar _ -> [n] + | Nneg n | N2n(n,_) | Npow(n,_) -> get_all_nvar n + | Nmult(n1,n2) | Nadd(n1,n2) -> (get_all_nvar n1)@(get_all_nvar n2) + | _ -> [] + let get_factor n = match n.nexp with | Nvar _ | Nuvar _ -> n_one @@ -852,7 +859,7 @@ let mk_ord_params l = List.map (fun i -> (i,{k=K_Ord})) l 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 reg = {t = Tfn (arg,reg,IP_length,pure_e)} +let mk_pure_imp arg ret var = {t = Tfn (arg,ret,IP_length {nexp = Nvar var},pure_e)} let mk_nv v = {nexp = Nvar v} let mk_add n1 n2 = {nexp = Nadd (n1,n2) } @@ -1266,11 +1273,9 @@ let initial_typ_env = (mk_range (mk_nv "m") n_zero))), External (Some "length"),[],pure_e,nob)); (* incorrect types for typechecking processed sail code; do we care? *) - ("to_num_inc",Base(([("a",{k=K_Typ})], (mk_pure_imp {t=Tvar "a"} nat_typ)),External None,[],pure_e,nob)); - ("to_num_dec",Base(([("a",{k=K_Typ})], (mk_pure_imp {t=Tvar "a"} nat_typ)),External None,[],pure_e,nob)); ("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") (Nvar "n") (Nvar "m")) - (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "p") (Nvar "o")))), + (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "p") (Nvar "o")) "o")), External (Some "mask"), [GtEq(Specc(Parse_ast.Int("mask",None)), (mk_nv "m"), (mk_nv "o"))],pure_e,nob)); (*TODO These should be IP_start *) @@ -1488,8 +1493,10 @@ let rec t_subst s_env t = | Toptions(t1,Some t2) -> {t = Toptions(t_subst s_env t1,Some (t_subst s_env t2)) } and ip_subst s_env ip = match ip with - | IP_none | IP_length | IP_start -> ip - | IP_var n -> IP_var (n_subst s_env n) + | IP_none -> ip + | IP_length n -> IP_length (n_subst s_env n) + | IP_start n -> IP_start (n_subst s_env n) + | IP_user n -> IP_user (n_subst s_env n) and ta_subst s_env ta = match ta with | TA_typ t -> TA_typ (t_subst s_env t) @@ -1817,6 +1824,7 @@ let merge_bounds b1 b2 = if nexp_eq n1 n2 then b1 else VR_vec_r(v,[Eq((Patt Unknown),n1,n2)]) | VR_vec_eq(v,n),VR_vec_r(_,ranges) | VR_vec_r(v,ranges),VR_vec_eq(_,n) -> VR_vec_r(v,(Eq((Patt Unknown),n,n)::ranges)) + | _ -> b1 )::(merge b1s b2s) in Bounds (merge b1s b2s) @@ -2389,7 +2397,7 @@ let check_tannot l annot imp_param constraints efs = ignore (remove_internal_unifications s_env); (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) let t' = match (t.t,imp_param) with - | Tfn(p,r,_,e),Some x -> {t = Tfn(p,r,IP_var x,e) } + | Tfn(p,r,_,e),Some x -> {t = Tfn(p,r,IP_user x,e) } | _ -> t in Base((params,t'),tag,cs,e,bindings) | NoTyp -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation") diff --git a/src/type_internal.mli b/src/type_internal.mli index f3a2249c..aa2453ec 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -38,9 +38,9 @@ and t_aux = (*Implicit nexp parameters for library and special function calls*) and implicit_parm = | IP_none (*Standard function*) - | IP_length (*Library function to take length of a vector as first parameter*) - | IP_start (*Library functions to take start of a vector as first parameter*) - | IP_var of nexp (*Special user functions, must be declared with val, will pass stated parameter to functions as above*) + | IP_length of nexp (*Library function to take length of a vector as first parameter*) + | IP_start of nexp (*Library functions to take start of a vector as first parameter*) + | IP_user of nexp (*Special user functions, must be declared with val, will pass stated parameter to function from return type*) and nexp = { mutable nexp : nexp_aux } and nexp_aux = | Nvar of string @@ -186,6 +186,7 @@ val merge_bounds : bounds_env -> bounds_env -> bounds_env val normalize_nexp : nexp -> nexp val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*) +val get_all_nvar : nexp -> nexp list (*Pull out all of the contained nvar and nuvars in nexp*) val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> tannot list |