Handle type/kind variables in val spec vs function declaration as equal, although the function ones are optional

3 files changed, 60 insertions, 21 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 2cb9b492..1939d5c9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -241,8 +241,8 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
       let t = typ_to_t false false typ in
       let t = typ_subst tp_env t in
       let (pat',env,constraints,bounds,u) = check_pattern envs emp_tag t pat in
-      (*potentially this should refine bounds*)
-      (P_aux(P_typ(typ,pat'),(l,tag_annot t emp_tag)),env,cs@constraints,bounds,t)
+      let t,cs_consistent = type_consistent (Patt l) d_env false t expect_t in
+      (P_aux(P_typ(typ,pat'),(l,tag_annot t emp_tag)),env,cs@constraints@cs_consistent,bounds,t)
     | P_id id -> 
       let i = id_to_string id in
       let default_bounds = extract_bounds d_env i expect_t in
@@ -633,12 +633,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       | Some(Base(tp,Default,_,_,_)) ->
         typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use")
       | Some(Base((params,t),tag,cs,ef,bounds)) ->
+	(*let _ = Printf.eprintf "Going to check a function call %s with unsubstituted types %s and constraints %s \n" i (t_to_string t) (constraints_to_string cs) in*)
         let t,cs,ef,_ = subst params t cs ef in
         (match t.t with
         | Tfn(arg,ret,imp,ef') ->
-	  (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in*)
+	  (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in
+	  let _ = Printf.eprintf "Substituted types and constraints are %s and %s\n" (t_to_string t) (constraints_to_string cs) in*)
           let parms,arg_t,cs_p,ef_p = check_parms arg parms in
-	  (*let _ = Printf.printf "Checked parms of %s\n" i in*)
+	  (*let _ = Printf.eprintf "Checked parms of %s\n" i in*)
           let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in
 	  (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*)
           (e',ret_t,t_env,cs@cs_p@cs_r, bounds,union_effects ef' (union_effects ef_p ef_r))
@@ -1711,15 +1713,13 @@ 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 _ = Printf.printf "cs_p for %s %s\n" (id_to_string id) (constraints_to_string cs_p) in*)
-        (*let _ = Printf.printf "about to see if %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let t', _ = type_consistent (Patt l) d_env false param_t t' in
 	let exp',_,_,cs_e,_,ef = 
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', 
 			 merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in
-	(*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
+(*	let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
 	let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in*)
 	let cs = [CondCons(Fun l,cs_p,cs_e)] in
 	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in
@@ -1733,26 +1733,26 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   match (in_env,tannot) with
     | Some(Base( (params,u),Spec,constraints,eft,_)), Base( (p',t),_,c',eft',_) ->
       (*let _ = Printf.eprintf "Function %s is in env\n" id in*)
-      let u,constraints,eft,t_param_env = subst params u constraints eft in
+      let u,constraints,eft,t_param_env_spec = subst params u constraints eft in
+      let t_param_cs = type_param_consistent l t_param_env_spec t_param_env in
       let _,cs_decs = type_consistent (Specc l) d_env false t u in
-      (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %i constraints \n" id (t_to_string t) (t_to_string u) (List.length cs_decs) in*)
+      (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in*)
       let imp_param = match u.t with 
 	| 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 t_param_env imp_param in
+      let funcls,cs_ef = check t_env t_param_env_spec imp_param in
       let cs,ef = ((fun (cses,efses) -> 
 	(List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
-      let cs' = resolve_constraints (cs@cs_decs@constraints) in
-      (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in
-     let _ = Printf.eprintf "checking tannot for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
+      let cs' = resolve_constraints (cs@cs_decs@constraints@c'@t_param_cs) in
+      (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in*)
       let tannot = check_tannot l tannot imp_param cs' ef in
-     (*let _ = Printf.printf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
+     (*let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
       let funcls = match imp_param with
 	| Some {nexp = Nvar i} -> List.map (update_pattern i) funcls 
 	| _ -> funcls
       in
-      (*let _ = Printf.printf "done funcheck case 1\n" in*)
+      (*let _ = Printf.eprintf "done funcheck case 1\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,Envmap.insert t_env (id,tannot),b_env,tp_env)
     | _ , _-> 
@@ -1760,7 +1760,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let funcls,cs_ef = check t_env t_param_env None in
       let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
       let cs' = resolve_constraints cs in
-      (*let _ = Printf.eprintf "checking tannot for %s 2\n" id in*)
+      (*let _ = Printf.eprintf "checking tannot for %s 2  remaining constraints are %s\n" id (constraints_to_string cs') in*)
       let tannot = check_tannot l tannot None cs' ef in
       (*let _ = Printf.eprintf "done funcheck case2\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 4220ea5f..b74fa8ae 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -754,6 +754,16 @@ and occurs_in_nexp n_box nuvar : bool =
     | Nneg nb | N2n(nb,None) | Npow(nb,_) -> occurs_in_nexp nb nuvar
     | _ -> false
 
+let rec reduce_n_unifications n = 
+  match n.nexp with
+    | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> ()
+    | N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1
+    | Nadd(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2
+    | Nuvar nu ->
+      (match nu.nsubst with
+	| None -> ()
+	| Some(nexp) -> reduce_n_unifications(nexp); n.nexp <- nexp.nexp)
+
 let equate_n (n_box : nexp) (n : nexp) : bool =
   (*let _ = Printf.eprintf "equate_n given n_box %s and n %s\n" (n_to_string n_box) (n_to_string n) in*)
   if n_box.nexp == n.nexp then true
@@ -1573,7 +1583,7 @@ and ta_subst s_env ta =
 and n_subst s_env n =
   match n.nexp with
   | Nvar i -> (match Envmap.apply s_env i with
-               | Some(TA_nexp n1) -> n1
+               | Some(TA_nexp n1) ->  n1
                | _ -> { nexp = Nvar i })
   | Nuvar _ -> new_n()
   | Nconst _ | Npos_inf | Nneg_inf -> n
@@ -1625,6 +1635,28 @@ let subst (k_env : (Envmap.k * kind) list) (t : t) (cs : nexp_range list) (e : e
   in
   (typ_subst subst_env t, cs_subst subst_env cs, e_subst subst_env e, subst_env)
 
+let rec typ_param_eq l spec_param fun_param = 
+  match (spec_param,fun_param) with
+    | ([],[]) -> []
+    | (_,[]) -> raise (Reporting_basic.err_typ l "Specification type variables and function definition variables must match")
+    | ([],_) -> raise (Reporting_basic.err_typ l "Function definition declares more type variables than specification variables")
+    | ((ids,tas)::spec_param,(idf,taf)::fun_param) ->
+      if ids=idf
+      then match (tas,taf) with
+	| (TA_typ tas_t,TA_typ taf_t) -> (equate_t tas_t taf_t); typ_param_eq l spec_param fun_param
+	| (TA_nexp tas_n, TA_nexp taf_n) -> Eq((Specc l),tas_n,taf_n)::typ_param_eq l spec_param fun_param
+	| (TA_ord tas_o,TA_ord taf_o) -> (equate_o tas_o taf_o); typ_param_eq l spec_param fun_param
+	| (TA_eft tas_e,TA_eft taf_e) -> (equate_e tas_e taf_e); typ_param_eq l spec_param fun_param
+	| _ -> raise (Reporting_basic.err_typ l ("Specification and function definition have different kinds for variable " ^ ids))
+      else raise (Reporting_basic.err_typ l ("Specification type variables must match in order and number the function definition type variables, stopped matching at " ^ ids ^ " and " ^ idf))
+
+let type_param_consistent l spec_param fun_param =
+  let specs = Envmap.to_list spec_param in
+  let funs = Envmap.to_list fun_param in
+  match specs,funs with
+    | [],[] | _,[] -> []
+    | _ -> typ_param_eq l specs funs
+
 let rec t_remove_unifications s_env t =
   match t.t with
   | Tvar _ | Tid _-> s_env
@@ -1675,6 +1707,7 @@ and e_remove_unifications s_env e =
       | Some ks -> Envmap.insert s_env ks
       | None -> s_env)
   | _ -> s_env
+	
 
 let remove_internal_unifications s_env =
   let rec rem remove s_env u_list = match u_list with
@@ -2331,7 +2364,7 @@ let freshen n =
 
 let rec simple_constraint_check in_env cs = 
   let check = simple_constraint_check in_env in
-  (*let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in *)
+(*  let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in *)
   match cs with 
   | [] -> []
   | Eq(co,n1,n2)::cs -> 
@@ -2374,14 +2407,14 @@ let rec simple_constraint_check in_env cs =
         if not(u.nin) && ok_to_set && not(occurs)
         then if (equate_n n2' n1') then  None else (Some (Eq(co,n1',n2')))
         else if occurs 
-	then eq_to_zero ok_to_set n1' n2'
+	then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end
 	else Some (Eq(co,n1',n2')) 
       | Nuvar u, _ ->
 	let occurs = occurs_in_nexp n2' n1' in
         if not(u.nin) && ok_to_set && not(occurs)
         then if equate_n n1' n2' then None else (Some (Eq(co,n1',n2')))
         else if occurs
-	then eq_to_zero ok_to_set n1' n2'
+	then begin (reduce_n_unifications n1'); (reduce_n_unifications n2'); eq_to_zero ok_to_set n1' n2' end
 	else Some (Eq(co,n1',n2'))
       | _,_ -> 
 	if nexp_eq_check n1' n2'
@@ -2390,6 +2423,7 @@ let rec simple_constraint_check in_env cs =
     in
     (match contains_in_vars in_env n1, contains_in_vars in_env n2 with
       | _,_ ->	
+	let _ = reduce_n_unifications n1; reduce_n_unifications n2 in
 	(match check_eq true n1 n2 with
 	  | None -> (check cs)
 	  | Some(c) -> c::(check cs))
@@ -2481,6 +2515,9 @@ let check_tannot l annot imp_param constraints efs =
       ignore(effects_eq (Specc l) efs e);
       let s_env = (t_remove_unifications (Envmap.from_list params) t) in
       let params = Envmap.to_list s_env in
+      (*let _ = Printf.eprintf "parameters going to save are " in
+      let _ = List.iter (fun (s,_) -> Printf.eprintf "%s " s) params in
+      let _ = Printf.eprintf "\n" in*)
       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
diff --git a/src/type_internal.mli b/src/type_internal.mli
index adfd0cbe..d43e4650 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -182,6 +182,8 @@ val equate_t : t -> t -> unit
 
 val typ_subst : t_arg emap -> t -> t 
 val subst : (Envmap.k * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect * t_arg emap
+val type_param_consistent : Parse_ast.l -> t_arg emap -> t_arg emap -> nexp_range list
+
 val get_abbrev : def_envs -> t -> (t * nexp_range list)
 
 val extract_bounds : def_envs -> string -> t -> bounds_env