open Support.Pervasive open Support.Error open G_ast open Prim open Union_find open Printf open G2str open List (* This is an implementation of the congruence closure algorithm from the paper "Fast Decision Procedures Based on Congruence CLosure" by Greg Nelson and Derek C. Oppen. JACM, Vol 27, No 2, April 1980, pp 356-364. *) let max_model_depth = 20 let set_insert x s = if (mem x s) then s else x::s exception Ambiguous_overload exception No_matching_overload of string exception Unify_failure of string exception No_matching_model of string exception No_associated_type of string exception Under_construction exception Depth_limit let position x ls = let rec loop ls i = (match ls with [] -> i | y::ls -> if (x = y) then i else loop ls (1 + i)) in loop ls 0 let make_model_class_name ts cn targs (rs,ss) = let sub = map2 (fun t n -> (t, VarT (UNKNOWN, sprintf "T%d" n))) ts (iota (length ts)) in let targs = map (fun t -> subst_typ sub t) targs in let rs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs)) rs in let ss = map (fun (s,t) -> (subst_typ sub s, subst_typ sub t)) ss in sprintf "model_%s_%s_%s_%s" cn (String.concat "_" (map typ2mangled_name targs)) (String.concat "_" (map (fun (cn,targs) -> sprintf "%s_%s" cn (String.concat "" (map typ2mangled_name targs))) rs)) (String.concat "_" (map (fun (s,t) -> sprintf "%seq%s" (typ2mangled_name s) (typ2mangled_name t)) ss)) type match_kind = Exact | QualifierCoerce | TypeCoerce | Dont of string let match_more_specific m1 m2 = (match (m1,m2) with (Exact, QualifierCoerce) | (Exact, TypeCoerce) | (Exact, Dont _) | (QualifierCoerce, TypeCoerce) | (QualifierCoerce, Dont _) | (TypeCoerce, Dont _) -> true | _ -> false) let combine_match_kind m1 m2 = if match_more_specific m1 m2 then m2 else m1 let match2str m = (match m with Exact -> "exact" | QualifierCoerce -> "qual" | TypeCoerce -> "type" | Dont _ -> "don't") let debug = false let unify_debug = ref false let cong_debug = false let merge_debug = ref false let equal_type_debug = ref false let lookup_dict_debug = ref false let lookup_class n env = (try assoc n env.classes with Not_found -> assoc n env.unions) let subdict_member_name n targs = sprintf "subdict_%s_%s" n (String.concat "_" (map typ2mangled_name targs)) let print_vars (env : environment) = if cong_debug then (printf "global vars\n%s\n" (String.concat "\n" (map (fun (n,b) -> (match b with VarB (e,t,m,bk) -> sprintf "%s : %s %s" n (g2string_typ t) (mut2str m) | OvldB ls -> sprintf "%s : { %s }" n (String.concat ", " (map (fun (e,t,bk) -> g2string_typ t) ls)) )) env.vars)); printf "local vars\n%s\n" (String.concat "\n" (map (fun (n,b) -> (match b with VarB (e,t,m,bk) -> sprintf "%s : %s %s" n (mut2str m) (g2string_typ t) | OvldB ls -> sprintf "%s : { %s }" n (String.concat ", " (map (fun (e,t,bk) -> g2string_typ t) ls)))) env.local_vars))) else () let print_reps (uf : union_find) = if cong_debug then (printf "============\n"; Array.iteri (fun i _ -> printf "%d: %d\n" i (Union_find.find i uf)) uf; printf "-----------\n") else () let print_graph (g : graph) = if cong_debug then (printf "<<<<<<<<<<\n"; Array.iteri (fun i n -> printf "%d: %s\n" i (g2string_typ n.ty)) g; printf ">>>>>>>>>>\n") else () let print_subst sub = if !unify_debug then (printf "SUBSTITUTIONS=\n"; iter (fun (n,t) -> printf "\t%s : %s\n" n (g2string_typ t)) sub) else () let rec lookup_dictionary is_refine i cn targs env depth = let (dict,assocs,env) = lookup_model is_refine i cn targs env depth in (dict, env) and lookup_model is_refine i cn targs env depth = let raise_no_match env cn targs = raise (No_matching_model (sprintf "Model %s<%s> needed to satisfy requirement, but it is not defined." cn (String.concat ", " (map (typ2str env) targs)))) in if !lookup_dict_debug then (printf "Looking for dictionary %s<%s> at depth %d\n" cn (String.concat ", " (map (typ2str env) targs)) depth; flush stdout); if depth > max_model_depth then raise (No_matching_model (sprintf "Model %s<%s> needed to satisfy requirement, but it is not defined (max model depth hit)." cn (String.concat ", " (map (typ2str env) targs)))) else let depth = depth + 1 in let ms = (try assoc cn env.models with Not_found -> raise_no_match env cn targs) in if debug then (printf "found models for concept %s\n" cn; flush stdout); (try let fts = map (fun (dk,ts,w,mtargs,assocs,dn,dp) -> let ps = map (fun t -> (t,Lvalue,Constant)) mtargs in let ft = FunT (i,ts,w,ps, (ConstT (i, BoolT i), Lvalue, Constant)) in (*printf "model %s\n" (g2string_typ ft);*) ft) ms in let args = map (fun t -> (t, Lvalue, Constant)) targs in let (_,k) = resolve_overload depth env fts args in let m = nth ms k in model_match is_refine i env cn targs m depth with Ambiguous_overload -> raise (No_matching_model (sprintf "ambiguous models for %s<%s>" cn (String.concat ", " (map g2string_typ targs)))) | No_matching_overload msg -> raise_no_match env cn targs) and model_match is_refine i env cn targs m depth = let (dk,ts,(rs,ss),mtargs,assocs,dn,dp) = m in let concept_string = sprintf "%s<%s>" cn (String.concat ", " (map g2string_typ targs)) in let model_string = sprintf "model<%s> %s<%s>" (String.concat ", " ts) cn (String.concat ", " (map g2string_typ mtargs)) in if !lookup_dict_debug then printf "model_match: possible %s\n" model_string; let omtargs = mtargs in let ors = rs and oss = ss in let nts = map (fun t -> uniquify_name t) ts in let rename = combine ts (map (fun nt -> VarT (i, nt)) nts) in let ors = rs in let rs = map (fun (cn,targs) -> let targs = map (subst_typ rename) targs in (cn,targs)) rs in let ss = map (fun (s,t) -> (subst_typ rename s, subst_typ rename t)) ss in let assocs = map (fun (n,t) -> (n, subst_typ rename t)) assocs in let mtargs = map (subst_typ rename) mtargs in (try let sub = unify_list nts i env [] mtargs targs in if debug then (printf "found a match with %s, sub:\n" model_string; iter (fun (n,t) -> printf "%s : %s\n" n (typ2str env t)) sub); let mtargs = map (subst_typ sub) mtargs in let assocs = (map (fun (n,t) -> (n, subst_typ sub t)) assocs) in let srs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs)) rs in (try let find_dict is_refine = (fun (env,dicts) (cn,targs) -> let (dict,env) = lookup_dictionary is_refine i cn targs env depth in (env, dicts @ [dict])) in let (env,ds) = fold_left (find_dict false) (env,[]) srs in if !lookup_dict_debug then printf "yep, conditions satisfied for %s\n" model_string; (* if this was a polymorphic model, cache the result. This screws up compilation. Need to cache in the C++ output as well. -Jeremy *) let env = if false(*ts != []*) then (if !lookup_dict_debug then printf "caching a model\n"; if !lookup_dict_debug then (iter (fun (n,t) -> printf "type %s = %s;\n" n (g2string_typ t)) assocs); env_add_model env cn [] empty_where mtargs assocs dn dp ) else env in let env = extend_env_with_same_types env (map (fun (n,t) -> (AssocT (i,cn,mtargs,n), subst_typ sub t)) assocs) in (* was benv *) let env = if is_refine then extend_env_with_same_types env (map (fun (n,t) -> (VarT (i, n), subst_typ sub t)) assocs) else env in if length rs = 0 then (make_dict_access (Cpp_ast.VarE dn) dp, assocs, env) else (* Find dictionaries for refines and requires *) (if !lookup_dict_debug then (printf "finding dicts for refines/requires in %s\n" cn; flush stdout); let (cts,cats,crefs,creqs,cfs,css) = assoc cn env.concepts in (* env or benv? *) let sub = (combine cts mtargs) @ assocs in let crefs = map (fun (n,ts) -> (n, map (subst_typ sub) ts)) crefs in let creqs = map (fun (n,ts) -> (n, map (subst_typ sub) ts)) creqs in if !lookup_dict_debug then (printf "finding dicts for refines %s\n" cn; flush stdout); let (env,ref_dicts) = fold_left (find_dict true) (env,[]) crefs in (* env or benv? *) if !lookup_dict_debug then (printf "finding dicts for requires %s\n" cn; flush stdout); let (env,req_dicts) = fold_left (find_dict false) (env,[]) creqs in (* env or benv? *) if !lookup_dict_debug then (printf "finished finding dicts needed for %s\n" cn; flush stdout); let model_class_name = make_model_class_name ts cn omtargs (ors,oss) in (Cpp_ast.ClassE (GCHeap, model_class_name, 0, ref_dicts @ req_dicts @ ds), assocs, env)) with No_matching_model msg -> let msg = (sprintf "For requirement %s, failed to match %s because %s\n" concept_string model_string msg) in if debug then printf "%s" msg; raise (No_matching_model msg) ) with Unify_failure msg -> let msg = (sprintf "For requirement %s, failed to unify with %s because %s\n" concept_string model_string msg) in if debug then printf "%s" msg; raise (No_matching_model msg)) (* returns a list of dictionary access expressions *) and lookup_dictionaries i rs env depth = (match rs with [] -> ([], env) | (cn,targs)::rs -> let (dict,env) = lookup_dictionary false i cn targs env depth in let (ds,env) = lookup_dictionaries i rs env depth in (dict::ds, env)) and make_dict_access dict dict_path = let i = UNKNOWN in (match dict_path with [] -> dict | k::ks -> let e = make_dict_access dict ks in Cpp_ast.MemE (Cpp_ast.ApplyE (Cpp_ast.PrimE DerefP, [e]), k)) and make_dict_name (ts : string list) cn targs = let sub = map2 (fun t n -> (t, VarT (UNKNOWN, sprintf "T%d" n))) ts (iota (length ts)) in let targs = map (fun t -> subst_typ sub t) targs in sprintf "__%s_%s" cn (String.concat "_" (map typ2mangled_name targs)) and make_dict_params (ts : string list) i rs = map (fun (cn,targs) -> (make_dict_name ts cn targs, Cpp_ast.PtrT (Cpp_ast.ClassT cn))) rs and make_refine_dict_name cn targs = sprintf "__refine_%s_%s" cn (String.concat "_" (map typ2mangled_name targs)) and make_refine_dict_params i rs = map (fun (cn,targs) -> (make_refine_dict_name cn targs, Cpp_ast.PtrT (Cpp_ast.ClassT cn))) rs and well_formed_typ (env : environment) (t : typ) : typ = well_formed_typ_impl true env t and well_formed_typ_impl check (env : environment) (t : typ) : typ = (match t with VarT (i, n) -> (try let newt = assoc n env.tparams in if cong_debug then printf "in well_formed, type params %s\n" (String.concat ", " (map (fun (n, _) -> n) env.tparams)); (*get_canonical env (VarT (i,nn))*) newt with Not_found -> (try let (ts,_,_,_) = lookup_class n env in if debug then printf "in well_formed, class type %s\n" n; if (length ts = 0) then ClassT (i, n, []) else error i (sprintf "%s is a polymorphic type, and therefore requires type arguments" n) with Not_found -> error i (sprintf "Type is not well formed, undefined type name: %s" n))) | VertexT _ -> error UNKNOWN "well_formed_typ_impl: unhandled vertex" | ClassT (i, n, targs) -> if debug then printf "Well formed typeargs to class?\n"; let targs = map (well_formed_typ_impl check env) targs in (try let (ts,(rs,sms),_,_) = lookup_class n env in if (length ts) != (length targs) then error i "number of type arguments does not match number of type parameters" else (if check then (if debug then printf "Well formed class, type reqs?\n"; (* Check that the class's where clause is satisfied *) let sub = combine ts targs in let rs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs)) rs in let sms = map (fun (s,t) -> (subst_typ sub s, subst_typ sub t)) sms in let (_,menv) = (try lookup_dictionaries i rs env 0 with No_matching_model msg -> error i (sprintf "Type %s<%s> is not well formed\n%s" n (String.concat ", " (map g2string_typ targs)) msg)) in iter (fun (s,t) -> if not (equal_type menv s t) then error i (sprintf "Same type requirement violated, %s != %s" (typ2str env s) (typ2str env t)) else ()) sms; if debug then printf "Well formed class, done\n"; ClassT (i, n, targs)) else ClassT (i, n, targs)) with Not_found -> error i (sprintf "Type %s is not defined" n)) | UnsignedT (i,t) -> UnsignedT (i, well_formed_typ_impl check env t) | SignedT (i,t) -> SignedT (i, well_formed_typ_impl check env t) | ConstT (i,t) -> ConstT (i, well_formed_typ_impl check env t) | PtrT (i, t) -> PtrT (i, well_formed_typ_impl check env t) | FunT (i, ts, w, ps, (rt,rv,rm)) -> let (env,nts) = env_extend_type_params ts env in let w = well_formed_where env w in let ps = map (fun (t,v,m) -> (well_formed_typ_impl check env t, v, m)) ps in let rt = well_formed_typ_impl check env rt in FunT (i, nts, w, ps, (rt,rv,rm)) | AssocT (i, cn, targs, tn) -> let targs = map (well_formed_typ_impl check env) targs in (try find_associated_type i env cn targs tn with No_associated_type msg -> error i msg) | OvldT (i, ts) -> error i "well_formed_typ_impl: unhandled ovld type" | ElipsesT _ | NullT _ | VoidT _ | CharT _ | WCharT _ | StringT _ | BoolT _ | LongDoubleT _ | DoubleT _ | FloatT _ | ShortT _ | LongLongT _ | LongT _ | IntT _ -> t ) and find_associated_type i env cn targs tn = let (_,assocs,benv) = (try lookup_model false i cn targs env 0 with No_matching_model msg -> error i msg) in let (ts,ats,refs,reqs,fs,ss) = (try assoc cn env.concepts with Not_found -> raise (No_associated_type (sprintf "Concept %s is not defined." cn))) in if mem tn ats then (try let t = assoc tn assocs in let t = get_canonical benv t in t with Not_found -> AssocT (i, cn, targs, tn)) else let sub = combine ts targs in let rec loop refs = match refs with [] -> raise (No_associated_type (sprintf "There is no associated type named %s in concept %s" tn cn)) | (cn,targs)::refs -> let targs = map (subst_typ sub) targs in (try find_associated_type i env cn targs tn with No_associated_type msg -> loop refs) in loop refs and well_formed_where env (rs,sms) = let rs = map (fun (cn,targs) -> (cn, map (well_formed_typ_impl false env) targs)) rs in let sms = map (fun (s,t) -> (well_formed_typ_impl false env s, well_formed_typ_impl false env t)) sms in (rs,sms) and env_add_model env cn ts rs targs assocs dict_name dict_path = if !lookup_dict_debug then printf "adding model<%s> %s<%s>\n" (String.concat ", " ts) cn (String.concat ", " (map g2string_typ targs)); let ms = (try assoc cn env.models with Not_found -> []) in let ms = if exists (fun (_,_,_,targs2,_,_,_) -> (* This needs improvement, take into account ts and where. -Jeremy *) for_all2 (equal_type env) targs targs2) ms then ms else (Defn,ts, rs, targs, assocs, dict_name, dict_path)::ms in { env with models = (cn,ms)::env.models } and env_add_model_fwd env cn ts rs targs assocs dict_name dict_path = if debug then printf "adding model<%s> %s<%s>\n" (String.concat ", " ts) cn (String.concat ", " (map g2string_typ targs)); let ms = (try assoc cn env.models with Not_found -> []) in let ms = (FwdDecl, ts, rs, targs, assocs, dict_name, dict_path)::ms in { env with models = (cn,ms)::env.models } and collect_models_from_where make_dname (bare_assocs : bool) (i : info) (env : environment) (ts : string list) (rs : (string * typ list) list) : environment * ((string * typ list) list) * ((string * typ list * string * string list) list) = if debug then printf "env_add_models_from_where\n" ; let rec loop rs env = (match rs with [] -> if debug then printf "finished with env_add_models_from_where\n" ; (env, [], []) | (cn,targs)::rs -> let targs = map (well_formed_typ_impl false env) targs in let (cts, ats, refs, reqs, cfs, sms) = (try assoc cn env.concepts with Not_found -> error i (sprintf "Invalid requirement in where clause, concept %s is not defined." cn)) in if (length cts != length targs) then error i (sprintf "Number of type arguments (%d) does not match number of parameters (%d) for %s" (length targs) (length cts) cn); let dname = make_dname ts cn targs in (* Check to see if this model is already present. If so, don't add. This is needed to allow for diamonds. *) let assocs = [] in (* ?? *) let env = env_add_model env cn [] empty_where targs assocs dname [] in (* Add concept members to the environment *) let env = if bare_assocs then let qual_assocs = List.map (fun at -> (at, AssocT (i,cn, targs, at))) ats in { env with tparams = qual_assocs @ env.tparams } else env in (* redundant let (cts, ats, refs, reqs, cfs, sames) = assoc cn env.concepts in*) (* substitute type arguments for concept parameters and qualified type names for associated types *) let sub = (combine cts targs) @ (map (fun at -> (at, AssocT (i,cn, targs, at))) ats) in let refs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs, targs)) refs in let reqs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs, targs)) reqs in let sms = map (fun (s,t) -> (subst_typ sub s, subst_typ sub t)) sms in (* let cfs = map (fun (n,(mn,t,t_cpp, ps,b)) -> (n, mn, subst_typ sub t)) cfs in *) (* add refinements and requirements to the environment *) let (env,ms1) = env_add_models_from_refine bare_assocs i env refs dname [] in let (env,ms2) = env_add_models_from_refine false i env reqs dname [] in (* add concept's operations and same type constraints to the environment *) if debug then printf "\tadding model for %s\n" cn; (* let env = fold_left (fun env (fn, mfn, ft) -> let fe = make_dict_access (Cpp_ast.VarE dname) [mfn] in if debug then printf "adding override = %s : %s\n" fn (g2string_typ ft); env_add_override i env fn (VarB (fe, ft, Constant, Defn))) env cfs in *) let env = extend_env_with_same_types env sms in let (env, rs, ms0) = loop rs env in (env, (cn,targs)::rs, ms1 @ ms2 @ ms0 @ [(cn,targs,dname,[])]) ) in loop rs env and env_add_models_from_refine (bare_assocs : bool) (i : info) (env : environment) (rs : (string * typ list * typ list) list) (* the refinements *) dname path : (environment * ((string * typ list * string * string list) list)) = if debug then printf "env_add_models_from_refine , path = %s\n" (String.concat ", " path); let rec loop rs env = (match rs with [] -> (env, []) | (cn,targs,old_targs)::rs -> let path = (subdict_member_name cn old_targs)::path in let (cts, ats, refs, reqs, cfs, sms) = (try assoc cn env.concepts with Not_found -> error i (sprintf "Concept %s is not defined" cn)) in let assocs = [] in (* ??? *) let env = env_add_model env cn [] empty_where targs assocs dname path in (* Add concept members to the environment *) let env = if bare_assocs then let qual_assocs = List.map (fun at -> (at, AssocT (i,cn, targs, at))) ats in { env with tparams = qual_assocs @ env.tparams } else env in (*redundant let (cts, ats, refs, reqs, cfs, sames) = assoc cn env.concepts in*) let sub = (combine cts targs) @ (map (fun at -> (at, AssocT (i,cn, targs, at))) ats) in let refs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs, targs)) refs in let reqs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs, targs)) reqs in let (env,rs1) = env_add_models_from_refine bare_assocs i env refs dname path in let (env,rs2) = env_add_models_from_refine false i env reqs dname path in let sms = map (fun (s,t) -> (subst_typ sub s, subst_typ sub t)) sms in if debug then (printf "operations before subst\n"; iter (fun (n,(mn,t,t_cpp,ps,b)) -> printf "\t%s : %s\n" mn (g2string_typ t)) cfs); if debug then printf "\t\tadding refine/require %s<%s>\n" cn (String.concat ", " (map g2string_typ targs)); (* let cfs = map (fun (n,(mn,t,t_cpp,ps,b)) -> (n, mn, subst_typ sub t)) cfs in let env = fold_left (fun env (fn,mfn, ft) -> (* need to substitute qualified type names for associated types *) let sub = map (fun at -> (at, AssocT (i,cn, targs, at))) ats in let ft = subst_typ sub ft in let fe = make_dict_access (Cpp_ast.VarE dname) (mfn::path) in if debug then printf "in refine, adding override = %s : %s\n" fn (g2string_typ ft); env_add_override i env fn (VarB (fe, ft, Constant, Defn))) env cfs in *) let env = extend_env_with_same_types env sms in let (env, rs0) = loop rs env in (env, rs1 @ rs2 @ rs0 @ [(cn,targs,dname,path)]) ) in loop rs env and coerce_model_member i env cn mangled_member_name ft new_ft dict_exp = let dt = Cpp_ast.PtrT (Cpp_ast.ClassT cn) in (match ft with FunT (_, fts, (frs,fsms), fps, frt) -> let params = map (fun t -> (sprintf "param_%d" (make_id()), cvt_exp_typ env t)) fps in let args = map (fun (n,t) -> Cpp_ast.VarE n) params in let inits = [("dict", (dict_exp,dt))] in let rt = cvt_exp_typ env frt in let deref_de = Cpp_ast.ApplyE (Cpp_ast.PrimE DerefP, [Cpp_ast.VarE "dict"]) in if frs = [] then let body = Cpp_ast.CompoundS [Cpp_ast.ReturnS (Some (Cpp_ast.ApplyE (Cpp_ast.MemE (deref_de, mangled_member_name), args)))] in let fe = Cpp_ast.FunE (params, rt, inits, body) in (coerce_poly env i (ft, Rvalue, Constant) fe new_ft, (new_ft, Rvalue, Constant)) else raise Under_construction | _ -> error i "find_model_member, expected a function type") (* targs already well formed *) and env_add_model_ops (i : info) (env : environment) (cn : string) (targs : typ list) dname dpath : environment = let (cts, ats, refs, reqs, cfs, sms) = (try assoc cn env.concepts with Not_found -> error i (sprintf "env_add_model_ops: concept %s is not defined" cn)) in let sub = (combine cts targs) @ (map (fun at -> (at, AssocT (i, cn, targs, at))) ats) in let cfs = map (fun (n,(mn,t,t_cpp, ps,b)) -> (n, mn, t, subst_typ sub t)) cfs in let add_concept_op env (fn, mfn, ft, new_ft) = let fe = make_dict_access (Cpp_ast.VarE dname) dpath in let (fe,(ft,_,_)) = coerce_model_member i env cn mfn ft new_ft fe in if debug then printf "adding override = %s : %s\n" fn (g2string_typ ft); env_add_override i env fn (VarB (fe, ft, Constant, Defn)) in fold_left add_concept_op env cfs and remove_duplicate_models env ms = (match ms with [] -> [] | (cn,targs,dname,dpath)::ms -> if exists (fun (cn2,targs2,_,_) -> cn = cn2 && for_all2 (equal_type env) targs targs2) ms then remove_duplicate_models env ms else (cn,targs,dname,dpath)::(remove_duplicate_models env ms)) and process_generic_intro i env ts rs ss = let orig_models = env.models in let benv = copy_env env in let (benv,nts) = env_extend_type_params ts benv in (* Extend the environment with the associated types and check for well formed types in the where clause *) let (benv, rs, ms) = collect_models_from_where make_dict_name false i benv nts rs in (* Need to check for well formed same types after adding models for example model3.g line 88 *) let ss = map (fun (s,t) -> (well_formed_typ benv s, well_formed_typ benv t)) ss in let benv = extend_env_with_same_types benv ss in (* duplicates may arrise due to same type constraints *) if debug && ms != [] then (printf "before removing duplicates=\n"; iter (fun (cn,targs,dname,dpath) -> printf "\t\t%s<%s>\n" cn (String.concat ", " (map g2string_typ targs))) ms); let ms = remove_duplicate_models benv ms in if debug && ms != [] then (printf "after removing duplicates=\n"; iter (fun (cn,targs,dname,dpath) -> printf "\t\t%s<%s>\n" cn (String.concat ", " (map g2string_typ targs))) ms); let benv = { benv with models = orig_models } in let benv = fold_left (fun env (cn,targs,dname,dpath) -> let env = env_add_model env cn [] empty_where targs [] dname dpath in env_add_model_ops i env cn targs dname dpath) benv ms in (benv, nts, rs, ss) and remove_ambiguous i env vars n b = (try let old_b = assoc n vars in let old_fs = binding2list old_b in let new_fs = binding2list b in (* filter out overloads that would be ambiguous *) let old_fs = filter_map (fun (old_fe,old_ft, old_bk) -> if exists (fun (_,new_ft, _) -> (match new_ft with FunT (j, ts, (rs,sms), ps, rt) -> let (env,nts,rs,sms) = process_generic_intro i env ts rs sms in (match callable env ps (old_ft,0) 0 with Dont _ -> false | _ -> true) | _ -> error i "expected a function type")) new_fs then None else Some (old_fe,old_ft, old_bk)) old_fs in let b = (match old_fs with [(fe,ft,bk)] -> VarB (fe,ft,Constant,bk) | _ -> OvldB old_fs) in (n, b)::vars with Not_found -> vars) (* This adds overrides to LOCAL environment *) and env_add_override i (env : environment) n (b : binding) : environment = let locals = remove_ambiguous i env env.local_vars n b in let globals = remove_ambiguous i env env.vars n b in let env = {env with local_vars = locals; vars = globals} in let insert_binding = (fun n b env -> { env with local_vars = (n,b)::env.local_vars }) in let lookup_var = (fun n env -> assoc n env.local_vars) in (* The following is an exact copy of env_add_ovld_impl *) (try let old_b = lookup_var n env in let old_fs = binding2list old_b in let new_fs = binding2list b in (* filter out fwd declarations that are now being defined *) let old_fs = filter_map (fun old_b -> match old_b with (e,ft,FwdDecl) -> if exists (fun b -> match b with (ne,nft,_) -> equal_type env ft nft) (* if more_specific env (nft,0) (ft,0) then false else if more_specific env (ft,0) (nft,0) then false else true *) new_fs then None else Some (e,ft,FwdDecl) | (e,ft,Defn) -> Some old_b) old_fs in let fs = new_fs @ old_fs in let new_b = (match fs with [(fe,ft,bk)] -> VarB (fe,ft,Constant,bk) | _ -> OvldB fs) in insert_binding n new_b env with Not_found -> insert_binding n b env) and binding2list b = (match b with OvldB fs -> fs | VarB (e, ft, _, bk) -> [(e,ft,bk)]) and env_add_ovld_impl (insert_binding : 'a -> binding -> environment -> environment) (lookup_var : 'a -> environment -> binding) i (env : environment) (n : 'a) (b : binding) : environment = (try let old_b = lookup_var n env in let old_fs = binding2list old_b in let new_fs = binding2list b in (* filter out fwd declarations that are now being defined *) let old_fs = filter_map (fun old_b -> match old_b with (e,ft,FwdDecl) -> if exists (fun b -> match b with (ne,nft,_) -> equal_type env ft nft) (*if more_specific env (nft,0) (ft,0) then false else if more_specific env (ft,0) (nft,0) then false else true*) new_fs then None else Some (e,ft,FwdDecl) | _ -> Some old_b) old_fs in let fs = new_fs @ old_fs in let new_b = (match fs with [(fe,ft,bk)] -> VarB (fe,ft,Constant,bk) | _ -> OvldB fs) in insert_binding n new_b env with Not_found -> insert_binding n b env) and more_specific env (ft1,i) (ft2,j) depth = (match (ft1,ft2) with (FunT (inf,ts1,(rs1,sms1),ps1,rt1), FunT (_,ts2,(rs2,sms2),ps2,rt2)) -> if debug then printf "In more specific\n"; let (env1,nts1,rs1,sms1) = process_generic_intro inf env ts1 rs1 sms1 in let ps1 = map (fun (t,v,m) -> (well_formed_typ env1 t, v, m)) ps1 in let (env2,nts2,rs2,sms2) = process_generic_intro inf env ts2 rs2 sms2 in let ps2 = map (fun (t,v,m) -> (well_formed_typ env2 t, v, m)) ps2 in let m2 = callable env1 ps1 (ft2,0) depth in let m1 = callable env2 ps2 (ft1,0) depth in let ret = match_more_specific m2 m1 in if debug then printf "more specific = %b\n" ret; (if ret then (if debug then printf "%s\n\n is more specific than \n\n%s\n\n\n" (typ2str env ft1) (typ2str env ft2)) else (if debug then printf "%s\n\n is not more specific than \n\n%s\n\n\n" (typ2str env ft1) (typ2str env ft2))); ret | _ -> error UNKNOWN "more_specific: expected functions") and most_specific_overload depth env (best : typ * int) ovlds = (match ovlds with [] -> best | ft::ovlds -> if (more_specific env best ft depth) then most_specific_overload depth env best ovlds else if (more_specific env ft best depth) then most_specific_overload depth env ft ovlds else raise Ambiguous_overload) (* A function with type ft may be called with type arguments targs and arguments of type argtys in the environment env *) and callable env (argtys : exp_typ list) (ft,_) depth = (match ft with FunT (i, ts, (rs,sms), ps, rt) -> if debug then printf "Callable? %s with (%s)\n" (g2string_typ ft) (String.concat ", " (map g2string_exp_typ argtys)); let nts = map (fun t -> uniquify_name t) ts in let sub1 = map2 (fun t nt -> (t, VarT (i,nt))) ts nts in let ps = map (fun (t,v,m) -> (subst_typ sub1 t, v, m)) ps in let rs = map (fun (cn,targs) -> (cn, map (subst_typ sub1) targs)) rs in let sms = map (fun (s,t) -> (subst_typ sub1 s, subst_typ sub1 t)) sms in (try let args = map (fun _ -> Cpp_ast.BoolE true) argtys in let (sub,_,mk,env) = subtype_unify_list false nts i env [] argtys args ps in if debug then printf "!! Parameters and arguments match !! for %s\n" (typ2str env ft); print_subst sub; if debug then printf "match kind = %s\n" (match2str mk); let rs = map (fun (cn,targs) -> (cn, map (subst_typ sub) targs)) rs in let (_,env) = lookup_dictionaries i rs env depth in print_graph env.type_graph; print_reps env.type_reps; if debug then printf "checking non-deducible contexts\n"; let _ = subtype_unify_list true nts i env sub argtys args ps in if debug then printf "passed non-deducible contexts\n"; let sms = map (fun (s,t) -> (subst_typ sub s, subst_typ sub t)) sms in if debug then printf "checking same type constraints\n"; iter (fun (s,t) -> if not (equal_type env s t) then let msg = (sprintf "Same type requirement violated, %s != %s" (typ2str env s) (typ2str env t)) in if debug then printf "%s\n" msg; raise (Unify_failure msg)) sms; mk with Unify_failure msg -> if debug then printf "not callable %s\nbecause %s\n" (typ2str env ft) msg; Dont msg | No_matching_model msg -> if debug then printf "not callable %s\nbecause %s\n" (typ2str env ft) msg; Dont msg) | _ -> error UNKNOWN (sprintf "in callable, expected a function type, not %s" (typ2str env ft))) and subst_where env rs sms sub = let (env,rs) = fold_left (fun (env,rest) (cn,targs) -> let (env,targs) = fold_left (fun (env,rest) t -> let t = vtyp2typ env t in let t = subst_typ sub t in let (t,env) = add_type_to_graph t env in (env,t::rest)) (env,[]) targs in (env,(cn,targs)::rest)) (env,[]) rs in let (env,sms) = fold_left (fun (env,rest) (s,t) -> let t = vtyp2typ env t in let t = subst_typ sub t in let (t,env) = add_type_to_graph t env in let s = vtyp2typ env s in let s = subst_typ sub s in let (s,env) = add_type_to_graph s env in (env,(s,t)::rest)) (env,[]) sms in (env,rs,sms) and unify_callable sub check uvars env (argtys : exp_typ list) (ft,_) = (match ft with FunT (i, ts, (rs,sms), ps, rt) -> if !unify_debug then printf "Unify Callable? %s with (%s)\n" (typ2str env ft) (String.concat ", " (map g2string_exp_typ argtys)); (* rename type parameters *) let nts = map (fun t -> uniquify_name t) ts in let sub1 = map2 (fun t nt -> if !unify_debug then printf "rename %s -> %s\n" t nt; (t, VarT (i,nt))) ts nts in (* What a pain! *) let (env,ps) = fold_left (fun (env,rest) (t,v,m) -> let t = vtyp2typ env t in let t = subst_typ sub1 t in let (t,env) = add_type_to_graph t env in (env,(t, v, m)::rest)) (env,[]) ps in let (env,rs,sms) = subst_where env rs sms sub1 in let (env,rt) = (match rt with (t,v,m) -> let t = vtyp2typ env t in let t = subst_typ sub1 t in let (t,env) = add_type_to_graph t env in (env, (t, v, m))) in let ft2 = FunT (i, nts, (rs,sms), ps, rt) in if !unify_debug then printf "(alpha renamed) Unify Callable? %s with (%s)\n" (typ2str env ft2) (String.concat ", " (map g2string_exp_typ argtys)); let args = map (fun _ -> Cpp_ast.BoolE true) argtys in let asi = map (fun (t,_,_) -> t) argtys in let psi = map (fun (t,_,_) -> t) ps in let (sub,_,exact,env) = subtype_unify_list_impl false (nts@uvars) i env sub asi argtys args psi ps in if !unify_debug then printf "finished unifying params, args\n"; print_subst sub; (try let (env,rs,sms) = subst_where env rs sms sub in let (_,env) = lookup_dictionaries i rs env 0 in let _ = subtype_unify_list_impl check (nts@uvars) i env sub asi argtys args psi ps in if !unify_debug then printf "finished second unify\n"; iter (fun (s,t) -> if not (equal_type env s t) then raise (Unify_failure (sprintf "Same type requirement violated, %s != %s" (typ2str env s) (typ2str env t)))) sms; let (env,rt) = (match rt with (t,v,m) -> let t = vtyp2typ env t in let t = subst_typ sub t in let (t,env) = add_type_to_graph t env in (env, (t, v, m))) in (env,sub,exact, rt) with No_matching_model _ -> raise (Unify_failure "")) | _ -> error UNKNOWN "unify_callable: expected a function type") (* returns the position of the best matching overload and its return type. Given precedence to exact matches, those that do not need coercion *) and resolve_overload depth env (ts : typ list) (argtys : exp_typ list) : (typ * int) = let tsi = map2 (fun t i -> (t,i)) ts (iota (length ts)) in if debug then (printf "overloads =\n%s\n" (String.concat "\n" (map g2string_typ ts)); printf "args = %s\n" (String.concat ", " (map g2string_exp_typ argtys)) ); let ovlds_call = map (fun t -> let c = callable env argtys t depth in (t,c)) tsi in let ovlds = let exact_ovlds = filter_map (fun (t,c) -> match c with Exact -> Some t | _ -> None) ovlds_call in let qual_ovlds = filter_map (fun (t,c) -> match c with QualifierCoerce -> Some t | _ -> None) ovlds_call in if (0 < length exact_ovlds) then (if debug then printf "got exact matches\n"; exact_ovlds) else if (0 < length qual_ovlds) then qual_ovlds else filter_map (fun (t,c) -> match c with Dont _ -> None | _ -> Some t) ovlds_call in if debug then printf "overload, potential matches =\n%s\n" (String.concat "\n" (map (fun (t,i) -> typ2str env t) ovlds)); if (length ovlds < 1) then let msgs = filter_map (fun ((ft,i),c) -> match c with Dont m -> let msg = sprintf "Could not call:\n%s\nbecause\n%s" (sprintInfo (match ft with FunT (inf,_,_,_,_) -> inf | _ -> error UNKNOWN "blah")) m in Some msg | _ -> None) ovlds_call in let msg = String.concat "\n\n" msgs in raise (No_matching_overload msg) else most_specific_overload depth env (hd ovlds) (tl ovlds) and basic_unify check uvars env (sub : (string * typ) list) (t1 : typ) (t2 : typ) : (string * typ) list = if !unify_debug then printf "basic_unify %s == %s?\n" (g2string_typ t1) (g2string_typ t2); print_graph env.type_graph; print_reps env.type_reps; if !unify_debug then printf "uvars = %s\n" (String.concat ", " uvars); (*printf "basic_unify reps %d = %d\n" v1 v2;*) if (equal_type env t1 t2) then (if debug then printf "basic unify = congruent\n"; sub) else let dt1 = deref env t1 and dt2 = deref env t2 in (match (dt1, dt2) with (VarT (_,n), VarT (_,m)) when n = m -> sub | (VarT (_,n), VarT (_,m)) when mem n uvars && mem m uvars -> let i = position n uvars and j = position m uvars in if i < j then let v1 = typ2v env dt1 in let v2 = typ2v env dt2 in union_fst_rep v2 v1 env.type_reps; merge v1 v2 env; if !unify_debug then printf "%s := %s\n" n (typ2str env t2); (n,t2)::sub else let v1 = typ2v env dt1 in let v2 = typ2v env dt2 in union_fst_rep v1 v2 env.type_reps; merge v1 v2 env; if !unify_debug then printf "%s := %s\n" n (typ2str env t1); (n,t1)::sub | (VarT (_,n), _) when mem n uvars -> (* do occur check*) if debug then printf "*** %s -> %s\n" n (g2string_typ t2); let v1 = typ2v env dt1 in let v2 = typ2v env dt2 in union_fst_rep v2 v1 env.type_reps; merge v1 v2 env; if !unify_debug then printf "%s := %s\n" n (typ2str env t2); (n,t2)::sub | (_, VarT (_,n)) when mem n uvars -> (* do occur check*) if debug then printf "*** %s -> %s\n" n (g2string_typ t1); let v1 = typ2v env dt1 in let v2 = typ2v env dt2 in union_fst_rep v1 v2 env.type_reps; merge v1 v2 env; if !unify_debug then printf "%s := %s\n" n (typ2str env t2); (n,t1)::sub | (ClassT (_,n,ts1), ClassT (_,m,ts2)) -> if n = m then let rec loop sub ts1 ts2 = (match (ts1,ts2) with ([],[]) -> sub | (s::ss, t::tt) -> let sub = basic_unify check uvars env sub s t in loop sub (map (subst_typ sub) ss) (map (subst_typ sub) tt) | _ -> raise (Unify_failure "")) in loop sub ts1 ts2 else raise (Unify_failure "") | (PtrT (_,t1), PtrT (_,t2)) -> basic_unify check uvars env sub t1 t2 | (UnsignedT (_,t1), UnsignedT (_,t2)) -> basic_unify check uvars env sub t1 t2 | (SignedT (_,t1), SignedT (_,t2)) -> basic_unify check uvars env sub t1 t2 | (ConstT (_,t1), ConstT (_,t2)) -> basic_unify check uvars env sub t1 t2 | (FunT (i,ts1,_,ss,(s,vs,ms)), FunT (_,ts2,_,tt,(t,vt,mt))) -> if (length ts1 = length ts2) then let r = map2 (fun t1 t2 -> (t2, VarT (i,t1))) ts1 ts2 in let tt = map (fun (t,v,m) -> (subst_typ r t, v, m)) tt in let t = subst_typ r t in let rec loop sub ss tt = (match (ss,tt) with ([],[]) -> sub | ((s,sv,sm)::ss, (t,tv,tm)::tt) when sv = tv && sm = tm -> let sub = basic_unify check uvars env sub s t in loop sub (map (fun (s,v,m) -> (subst_typ sub s, v, m)) ss) (map (fun (t,v,m) -> (subst_typ sub t, v, m)) tt) | _ -> raise (Unify_failure "")) in let sub = loop sub ss tt in basic_unify check uvars env sub (subst_typ sub s) (subst_typ sub t) else raise (Unify_failure "") | (AssocT (_,_,_,_), _) | (_, AssocT (_,_,_,_)) when not check -> if debug then printf "ignoring associated type, non-deducible\n"; sub | (AssocT (i1,cn1,targs1,tn1), AssocT (i2,cn2,targs2,tn2)) when check -> if cn1 = cn2 && tn1 = tn2 then let rec loop sub ss tt = (match (ss,tt) with ([],[]) -> sub | (s::ss, t::tt) -> let sub = basic_unify check uvars env sub s t in loop sub (map (subst_typ sub) ss) (map (subst_typ sub) tt) | _ -> raise (Unify_failure "")) in loop sub targs1 targs2 else raise (Unify_failure "") | (IntT _, IntT _) | (BoolT _, BoolT _) | (FloatT _, FloatT _) | (DoubleT _, DoubleT _) | (LongDoubleT _, LongDoubleT _) | (StringT _, StringT _) | (CharT _, CharT _) | (WCharT _, WCharT _) | (ShortT _, ShortT _) | (LongT _, LongT _) | (LongLongT _, LongLongT _) | (VoidT _, VoidT _) | (NullT _, PtrT (_,_)) | (NullT _, NullT _) -> if debug then printf "matching basic types\n" else (); sub | _ -> if debug then printf "failing basic unify\n" else (); raise (Unify_failure (sprintf "Type (%s) does not match type (%s)" (typ2str env t1) (typ2str env t2)))) (* May coerce via: 1) instantiation 2) overload resolution 3) Non-const to const 4) const char* to string 5) int to char, since this is so common in C, like getchar() 5) int to bool, since this is so common in C, like isalpha() *) and const2mutable_violation t1 t2 = (match (t1,t2) with ((_, Lvalue, Constant),(_, Lvalue, Mutable)) -> true | ((PtrT (_,_), Rvalue, Constant), (PtrT (_,_), Rvalue, Mutable)) -> true (* preserve deep constness! *) (* ((_, Lvalue, Constant),(_, Lvalue, Mutable)) -> false | ((_, Rvalue, _),(_, Lvalue, Mutable)) -> false *) | _ -> false) and rvalue2non_const_lvalue t1 t2 = (match (t1,t2) with ((_, Rvalue, _), (_, Lvalue, Mutable)) -> true | _ -> false) and mutable_const t1 t2 = (match (t1,t2) with ((_, _, Mutable),(_, _, Constant)) -> true | _ -> false) and basic_subtype_unify check uvars env (sub : (string * typ) list) (a : exp_typ) (at_orig : typ) (arg : Cpp_ast.exp) (p : exp_typ) (pt_orig : typ) : ((string * typ) list (* subtitutions *) * Cpp_ast.exp (* coerced arg *) * match_kind * environment ) = (* mutable -> const should count as non-exact match -JGS *) if !unify_debug then printf "in basic_subtype_unify\n"; let ((at,av,am), (pt,pv,pm)) = (a, p) in if const2mutable_violation a p then raise (Unify_failure (sprintf "you may not convert from constant (%s) to mutable (%s)" (g2string_exp_typ (vtyp2typ env at, av, am)) (g2string_exp_typ (vtyp2typ env pt, pv, pm)))); if rvalue2non_const_lvalue a p then raise (Unify_failure (sprintf "you may not bind a temporary (%s) to a mutable reference (%s)" (g2string_exp_typ (vtyp2typ env at, av, am)) (g2string_exp_typ (vtyp2typ env pt, pv, pm)))); if !unify_debug then printf "basic_subtype_unify %s <= %s?\n" (typ2str env at) (typ2str env pt) else (); if !unify_debug then printf "uvars = %s\n" (String.concat ", " uvars); if (equal_type env at pt) then (if !unify_debug then printf "basic_subtype_unify: they are congruent\n" else (); (sub, coerce_poly env UNKNOWN (at_orig,av,am) arg pt_orig, (if mutable_const a p then QualifierCoerce else Exact), env)) else let at = deref env at in let pt = deref env pt in let orig_uvars = uvars in (match (at, pt) with (FunT _, FunT _) -> fun_subtype_unify check orig_uvars env sub (at,av,am) at_orig arg pt pt_orig | (OvldT (_,fts), FunT (i,ts,w,ps,rt)) -> (try let (at,k) = resolve_overload 0 env (map snd fts) ps in fun_subtype_unify check orig_uvars env sub (at,av,am) at_orig arg pt pt_orig with Ambiguous_overload -> raise (Unify_failure "") | No_matching_overload msg -> raise (Unify_failure msg)) | (PtrT (_, VertexT u), PtrT (_, VertexT v)) -> let s = env.type_graph.(u).ty in let t = env.type_graph.(v).ty in (match (s, t) with (_, VoidT _) -> (sub, arg, TypeCoerce, env) | (ConstT (_, VertexT u), ConstT (_, VertexT v)) -> let s = env.type_graph.(u).ty in let t = env.type_graph.(v).ty in (*let sub = basic_unify check uvars env sub s t in*) (* this isn't quite right. -JGS *) let (sub,_,_,env) = basic_subtype_unify check uvars env sub (s,av,am) at_orig arg (t,pv,pm) pt_orig in (sub, arg, (if mutable_const a p then QualifierCoerce else Exact), env) | (_, ConstT (_, VertexT v)) -> let t = env.type_graph.(v).ty in (*let sub = basic_unify check uvars env sub s t in*) (* this isn't quite right. -JGS *) let (sub,_,_,env) = basic_subtype_unify check uvars env sub (s,av,am) at_orig arg (t,pv,pm) pt_orig in (sub, arg, TypeCoerce, env) | _ -> let sub = basic_unify check uvars env sub s t in (sub, arg, (if mutable_const a p then QualifierCoerce else Exact), env)) | (PtrT (_,s), PtrT (_, t)) -> let sub = basic_unify check uvars env sub s t in (sub, arg, (if mutable_const a p then QualifierCoerce else Exact), env) | (PtrT (_, _), NullT _) -> (sub, arg, TypeCoerce, env) | (PtrT (_, VertexT v), StringT _) -> (match env.type_graph.(v).ty with CharT _ | WCharT _ -> (sub, arg, TypeCoerce, env) | ConstT (_, VertexT v) -> (match env.type_graph.(v).ty with CharT _ | WCharT _ -> (sub, arg, TypeCoerce, env) | _ -> raise (Unify_failure "")) | _ -> raise (Unify_failure "")) | (StringT _, PtrT (_, VertexT v)) -> (match env.type_graph.(v).ty with CharT _ | WCharT _ -> (sub, arg, TypeCoerce, env) | ConstT (_, VertexT v) -> (match env.type_graph.(v).ty with CharT _ | WCharT _ -> (sub, arg, TypeCoerce, env) | _ -> raise (Unify_failure "")) | _ -> raise (Unify_failure "")) | (_, VoidT _) -> (sub, arg, TypeCoerce, env) | (LongT _, IntT _) | (IntT _, LongT _) | (ShortT _, IntT _) | (IntT _, ShortT _) | (IntT _, CharT _) | (CharT _, IntT _) | (IntT _, WCharT _) | (WCharT _, IntT _) | (FloatT _, DoubleT _) | (DoubleT _, FloatT _) | (IntT _, DoubleT _) | (IntT _, FloatT _) | (BoolT _, IntT _) | (IntT _, BoolT _) -> (sub, Cpp_ast.CastE (cvt_typ_impl env pt, arg), TypeCoerce, env) (* the following is a hack, perhaps won't need with type defs? *) | (UnsignedT (_, VertexT v), IntT _) -> basic_subtype_unify check uvars env sub (env.type_graph.(v).ty, av, am) at_orig arg (pt,pv,pm) pt_orig | (IntT _, UnsignedT (_, VertexT v)) -> basic_subtype_unify check uvars env sub (at,av,am) at_orig arg (env.type_graph.(v).ty, pv, pm) pt_orig | (ClassT (_,"size_t",_), IntT _) | (IntT _, ClassT (_,"size_t",_)) -> (sub, arg, TypeCoerce, env) | _ -> (basic_unify check uvars env sub at pt, coerce_poly env UNKNOWN (at_orig,av,am) arg pt_orig, (if mutable_const a p then QualifierCoerce else Exact), env)) and fun_subtype_unify check uvars env (sub : (string * typ) list) (ate : exp_typ) (at_orig : typ) (arg : Cpp_ast.exp) (pt : typ) (pt_orig : typ) : ((string * typ) list (* subtitutions *) * Cpp_ast.exp (* coerced arg *) * match_kind * environment ) = let (at,av,am) = ate in (match (at, pt) with (FunT (i, ts1, (rs1,sms1), ss, s), FunT (j, ts2, (rs2,sms2), tt, t)) -> if !unify_debug then printf "basic subtype unify: inside function case\n" else (); (match (s,t) with ((_, Rvalue, _), (_, Lvalue, _)) -> raise (Unify_failure (sprintf "Function type %s does not match type %s.\nReturning temporary through a reference" (typ2str env at) (typ2str env pt))) | _ -> ()); let (env2,nts2,rs2,sms2) = process_generic_intro i env ts2 rs2 sms2 in let new_uvars = uvars @ nts2 in let sub_nts2 = map2 (fun t nt -> (t, VarT (i,nt))) ts2 nts2 in let tt = map (fun (t,v,m) -> (subst_typ sub_nts2 t,v,m)) tt in let t = (match t with (t,v,m) -> (subst_typ sub_nts2 t, v, m)) in let (env2, sub, exact1,s) = unify_callable sub check new_uvars env2 tt (at, 0) in if !unify_debug then printf "checking if return type is coercible\n"; let (sub,_,exact2,env2) = basic_subtype_unify check new_uvars env2 sub s (BoolT UNKNOWN) (Cpp_ast.BoolE true) t (BoolT UNKNOWN) in if !unify_debug then printf "finished checking if return type is coercible\n"; let sub = filter (fun (n,t) -> mem n uvars) sub in let fe = coerce_poly env i (at_orig,av,am) arg pt_orig in if !unify_debug then printf "finished coercing function\n"; (sub, fe, combine_match_kind exact1 exact2, env2) | _ -> error UNKNOWN "fun_subtype_unify: expected functions") and basic_subtype uvars env (t1 : exp_typ) (t2 : exp_typ) : bool = (try let (_,_,exact,_) = basic_subtype_unify false uvars env [] t1 (BoolT UNKNOWN) (Cpp_ast.BoolE true) t2 (BoolT UNKNOWN) in let _ = basic_subtype_unify true uvars env [] t1 (BoolT UNKNOWN) (Cpp_ast.BoolE true) t2 (BoolT UNKNOWN) in true with Unify_failure _ -> false) and need_coerce_poly env i (s : typ) (t : typ) : bool = if (poly s && poly t) then false else if (poly_ptr s && (poly_ptr t || poly t)) then false else if poly s || poly_ptr s then true else (* neither is a qualified polymorphic type *) (match (s, t) with (FunT (i,_,_, ss, (s,sv,sm)), FunT (j,_,_, tt, (t,tv,tm))) -> ((exists2 (fun (t,_,_) (s,_,_) -> need_coerce_poly env i t s) tt ss) || need_coerce_poly env i s t) | (PtrT (_, t1), PtrT (_, t2)) -> if (need_coerce_poly env i t1 t2) then error i (sprintf "Not allow to coerce from (%s) to (%s)" (g2string_typ s) (g2string_typ t)) else false | (VertexT u, VertexT v) -> need_coerce_poly env i env.type_graph.(u).ty env.type_graph.(v).ty | (_,_) -> false) and cvt_exp_typ env (t,v,m) : Cpp_ast.typ = cvt_exp_typ_impl env (get_canonical env t, v, m) and cvt_exp_typ_impl env (t,v,m) : Cpp_ast.typ = (match cvt_typ_impl env t with Cpp_ast.AnyT -> (match (m,v) with (Mutable, Lvalue) -> Cpp_ast.AnyRefT | (Mutable, Rvalue) -> Cpp_ast.AnyT | (Constant, Lvalue) -> Cpp_ast.AnyConstRefT | (Constant, Rvalue) -> Cpp_ast.AnyT) | Cpp_ast.AnyPtrT -> (match (m,v) with (Mutable, Lvalue) -> Cpp_ast.AnyPtrRefT | (Mutable, Rvalue) -> Cpp_ast.AnyPtrT | (Constant, Lvalue) -> Cpp_ast.AnyPtrConstRefT | (Constant, Rvalue) -> Cpp_ast.AnyPtrT) | Cpp_ast.AnyConstPtrT -> (match (m,v) with (Mutable, Lvalue) -> Cpp_ast.AnyConstPtrRefT | (Mutable, Rvalue) -> Cpp_ast.AnyConstPtrT | (Constant, Lvalue) -> Cpp_ast.AnyConstPtrConstRefT | (Constant, Rvalue) -> Cpp_ast.AnyConstPtrT) | t -> (match m with Constant -> (match v with Rvalue -> t | Lvalue -> Cpp_ast.RefT (Cpp_ast.ConstT t)) | Mutable -> (match v with Rvalue -> t | Lvalue -> Cpp_ast.RefT t) )) (* Convert to a C++ type. Assumes that well_formed_typ has already been applied to the type. *) and cvt_typ env (t : typ) : Cpp_ast.typ = cvt_typ_impl env (get_canonical env t) and cvt_typ_impl env (t : typ) : Cpp_ast.typ = (match t with VarT (i, n) -> Cpp_ast.AnyT | VertexT _ -> cvt_typ_impl env (vtyp2typ env t) | ClassT (i, n, ts) -> Cpp_ast.ClassT n | UnsignedT (i,t) -> Cpp_ast.UnsignedT (cvt_typ_impl env t) | SignedT (i,t) -> Cpp_ast.SignedT (cvt_typ_impl env t) | ConstT (i,t) -> Cpp_ast.ConstT (cvt_typ_impl env t) | PtrT (i, t) -> (match (cvt_typ_impl env t) with Cpp_ast.AnyT -> Cpp_ast.AnyPtrT | Cpp_ast.ConstT Cpp_ast.AnyT -> Cpp_ast.AnyConstPtrT | ct -> Cpp_ast.PtrT ct) | FunT (i, ts, rs, ps, rt) -> let ps = map (fun t -> cvt_exp_typ env t) ps in let rt = cvt_exp_typ env rt in Cpp_ast.FunT (ps, rt) | OvldT (i, ts) -> error i "cvt_typ_impl: unhandled ovld type" | AssocT (i, cn, targs, tn) -> Cpp_ast.AnyT | ElipsesT _ -> Cpp_ast.ElipsesT | NullT _ -> Cpp_ast.NullT | VoidT _ -> Cpp_ast.VoidT | CharT _ -> Cpp_ast.CharT | WCharT _ -> Cpp_ast.WCharT | StringT _ -> Cpp_ast.StringT | BoolT _ -> Cpp_ast.BoolT | LongDoubleT _ -> Cpp_ast.LongDoubleT | DoubleT _ -> Cpp_ast.DoubleT | FloatT _ -> Cpp_ast.FloatT | ShortT _ -> Cpp_ast.ShortT | LongLongT _ -> Cpp_ast.LongLongT | LongT _ -> Cpp_ast.LongT | IntT _ -> Cpp_ast.IntT) and coerce_poly env i (se : exp_typ) (e : Cpp_ast.exp) (t : typ) : Cpp_ast.exp = if debug then printf "coerce_poly %s\n -> %s\n" (g2string_exp_typ se) (g2string_typ t); let (s,sv,sm) = se in if (need_coerce_poly env i s t) then (if debug then printf "yep,needs coercing\n" else (); if poly s || poly_ptr s then (if debug then printf "any cast\n" else (); let t = cvt_typ_impl env t in let t = (match (sv,sm) with (Lvalue,Mutable) -> (match t with Cpp_ast.AnyT -> Cpp_ast.AnyRefT | Cpp_ast.AnyPtrT -> Cpp_ast.AnyPtrRefT | Cpp_ast.AnyConstPtrT -> Cpp_ast.AnyConstPtrRefT | _ -> Cpp_ast.RefT t) | (Lvalue,Constant) -> (match t with Cpp_ast.AnyT -> Cpp_ast.AnyConstRefT | Cpp_ast.AnyPtrT -> Cpp_ast.AnyPtrConstRefT | Cpp_ast.AnyConstPtrT -> Cpp_ast.AnyConstPtrConstRefT | _ -> Cpp_ast.RefT (Cpp_ast.ConstT t)) | (Rvalue,_) -> t) in Cpp_ast.AnyCastE (t, e)) else (match (s, t) with (FunT (i,_,_, ss, (s,sv,sm)), FunT (j,_,_, tt, (t,tv,tm))) -> let pns = map (fun t -> sprintf "__%d" (make_id())) tt in let pvs = map2 (fun n ((t,tv,tm),(s,_,_)) -> coerce_poly env i (t,tv,tm) (Cpp_ast.VarE n) s) pns (combine tt ss) in let en = sprintf "__f%d" (make_id()) in let app = Cpp_ast.ApplyE (Cpp_ast.VarE en, pvs) in let inits = [(en,(e,Cpp_ast.FunT (map (cvt_exp_typ_impl env) ss, cvt_exp_typ_impl env (s,sv,sm))))] in let body = Cpp_ast.CompoundS [Cpp_ast.ReturnS (Some (coerce_poly env i (s,sv,sm) app t))] in Cpp_ast.FunE (combine pns (map (cvt_exp_typ_impl env) tt), cvt_exp_typ_impl env (t,tv,tm), inits, body) | (PtrT (_, t1), PtrT (_, t2)) -> if (need_coerce_poly env i t1 t2) then error i (sprintf "May not coerce from (%s) to (%s)" (g2string_typ s) (g2string_typ t)) else e | (VertexT u, VertexT v) -> coerce_poly env i (env.type_graph.(u).ty,sv,sm) e env.type_graph.(v).ty | (_,_) -> e)) else (if debug then printf "no coercing needed\n" else (); e) (* Add v as a predecessor to the vertices us *) and add_pred us v g = iter (fun t -> match t with VertexT u -> g.(v).pred <- set_insert v g.(v).pred | _ -> error UNKNOWN "expected a vertex in add_pred") us and find_vertex_for_type env t = let i = ref 0 and found = ref false in while not !found && !i < Array.length env.type_graph do if (congruent env [] env.type_graph.(!i).ty t) then found := true else i := !i + 1 done; if !found then Some (Union_find.find !i env.type_reps) else None and add_types_to_graph (ts : typ list) (env : environment) : (typ list * environment) = (match ts with [] -> ([], env) | t::ts -> let (v,env) = add_type_to_graph t env in let (vs,env) = add_types_to_graph ts env in (v::vs,env)) (* This changes to a NEW type_reps array, NOT an in-place change *) and add_type_to_graph (t : typ) (env : environment) : (typ * environment) = if cong_debug then printf "Adding type to graph: %s\n" (g2string_typ t) else (); let t = uniquify_typ [] t in if cong_debug then printf "uniquified\n" else (); let find_add_one t u env = (match find_vertex_for_type env t with None -> let (v,uf) = make_set env.type_reps in if cong_debug then printf "new type, adding node %d\n" v; let g = Array.append env.type_graph (Array.of_list [{ty = t; pred = []}]) in add_pred [u] v g; (VertexT v, {env with type_reps = uf; type_graph = g}) | Some v -> if cong_debug then printf "old type, node %d\n" v else (); (VertexT v, env)) in let find_add_many t us env = (match find_vertex_for_type env t with None -> let (v,uf) = make_set env.type_reps in if cong_debug then printf "new type, adding node %d\n" v; let g = Array.append env.type_graph (Array.of_list [{ty = t; pred = []}]) in add_pred us v g; (VertexT v, {env with type_reps = uf; type_graph = g}) | Some v -> if cong_debug then printf "old type, node %d\n" v else (); (VertexT v, env)) in (match t with VertexT v -> (VertexT (Union_find.find v env.type_reps), env) | VarT (_, _) | IntT _ | LongT _ | LongLongT _ | ShortT _ | FloatT _ | DoubleT _ | LongDoubleT _ | BoolT _ | StringT _ | CharT _ | WCharT _ | VoidT _ | NullT _ | ElipsesT _ -> (match find_vertex_for_type env t with None -> if cong_debug then printf "new type!\n" else (); let (v,uf) = make_set env.type_reps in let g = Array.append env.type_graph (Array.of_list [{ty = t; pred = []}]) in (VertexT v, { env with type_reps = uf; type_graph = g}) | Some v -> if cong_debug then printf "old type!\n" else (); (VertexT v, env)) | ClassT (i, n, ts) -> let (ts,env) = add_types_to_graph ts env in let t = ClassT (i,n,ts) in find_add_many t ts env | PtrT (i, pt) -> let (u,env) = add_type_to_graph pt env in let t = PtrT (i,u) in find_add_one t u env | UnsignedT (i, pt) -> let (u,env) = add_type_to_graph pt env in let t = UnsignedT (i, u) in find_add_one t u env | SignedT (i, pt) -> let (u,env) = add_type_to_graph pt env in let t = SignedT (i, u) in find_add_one t u env | ConstT (i, pt) -> let (u,env) = add_type_to_graph pt env in let t = ConstT (i, u) in find_add_one t u env | FunT (i, ts, (rs,ss), ps, (rt,rv,rm)) -> let (pst,env) = add_types_to_graph (map (fun (t,_,_) -> t) ps) env in let us = ref pst in let (rt,env) = add_type_to_graph rt env in us := rt::!us; let rec rs_loop rs env = (match rs with [] -> ([],env) | (cn,targs)::rs -> let (targs,env) = add_types_to_graph targs env in us := targs @ !us; let (rs,env) = rs_loop rs env in ((cn,targs)::rs,env)) in let (rs,env) = rs_loop rs env in let rec ss_loop ss env = (match ss with [] -> ([],env) | (t1,t2)::ss -> let (t1,env) = add_type_to_graph t1 env in let (t2,env) = add_type_to_graph t2 env in us := [t1;t2]@(!us); let (ss,env) = ss_loop ss env in ((t1,t2)::ss,env)) in let (ss,env) = ss_loop ss env in let t = FunT (i, ts, (rs,ss), (map2 (fun t (_,v,m) -> (t,v,m)) pst ps), (rt,rv,rm)) in find_add_many t !us env | OvldT (i, ts) -> let (nts,env) = add_types_to_graph (map snd ts) env in let t = OvldT (i, combine (map fst ts) nts) in find_add_many t nts env | AssocT (i, cn, targs, tn) -> let (ts,env) = add_types_to_graph targs env in let t = AssocT (i,cn,ts,tn) in find_add_many t ts env) and vtyp2typ env (vt : typ) = (* print_graph env.type_graph; print_reps env.type_reps; printf "vtyp2typ: %s\n" (g2string_typ vt); *) (match vt with VertexT v -> vertex2typ env v | ClassT (i, cn, ts) -> let ts = map (vtyp2typ env) ts in ClassT (i, cn, ts) | PtrT (i, t) -> PtrT (i, vtyp2typ env t) | FunT (i, ts, (rs,ss), ps, (rt,rv,rm)) -> let rs = map (fun (n,targs) -> (n, map (vtyp2typ env) targs)) rs in let ss = map (fun (s,t) -> (vtyp2typ env s, vtyp2typ env t)) ss in let ps = map (fun (t,v,m) -> (vtyp2typ env t, v, m)) ps in let rt = vtyp2typ env rt in FunT (i, ts, (rs,ss), ps, (rt,rv,rm)) | OvldT (i, ts) -> let nts = map (vtyp2typ env) (map snd ts) in OvldT (i, combine (map fst ts) nts) | AssocT (i, cn, targs, tn) -> let targs = map (vtyp2typ env) targs in AssocT (i, cn, targs, tn) | UnsignedT (i, t) -> UnsignedT (i, vtyp2typ env t) | SignedT (i, t) -> SignedT (i, vtyp2typ env t) | ConstT (i, t) -> ConstT (i, vtyp2typ env t) | _ -> vt) and vertex2typ env (v : int) = (*printf "vertex2typ: %d\n" v;*) let v = Union_find.find v env.type_reps in (*printf "rep: %d\n" v;*) if (v < Array.length env.type_graph) then vtyp2typ env env.type_graph.(v).ty else error UNKNOWN (sprintf "vertex2typ: out of bounds vertex %d\n" v) and get_canonical env t = let (t,env) = add_type_to_graph t env in (match t with VertexT v -> vertex2typ env v | _ -> error UNKNOWN "expected a vertex in get canonical") and t2v t = (match t with VertexT v -> v | _ -> error UNKNOWN "expected a vertex in t2v") and typ2v env t = (match t with VertexT v -> v | _ -> get_vertex env t) and get_vertex env t = let (t,_) = add_type_to_graph t env in (match t with VertexT v -> v | _ -> error UNKNOWN "expected a vertex in get_vertex") (* Recently added the call to union-find -JGS *) and deref env t = (match t with VertexT v -> env.type_graph.(Union_find.find v env.type_reps).ty | _ -> t) and same_vertex s t = (match (s,t) with (VertexT u, VertexT v) when u = v -> true | _ -> false) and typ2str env t = g2string_typ (get_canonical env t) and equivalent_to v env = filter_map (fun u -> if (Union_find.find u env.type_reps = Union_find.find v env.type_reps) then Some u else None) (iota (Array.length env.type_reps)) (* The merge function updates uf in place. Precondition: u and v are congruent *) and merge (u : int) (v : int) (env : environment) : unit = if !merge_debug then printf "merge %d=%s, %d=%s\n" u (g2string_typ (vertex2typ env u)) v (g2string_typ (vertex2typ env v)); let u = Union_find.find u env.type_reps in let v = Union_find.find v env.type_reps in if cong_debug then printf "merge: reps are %d %d\n" u v; if (u = v) then () else (* Merge children of u and v. This part comes from p. 361, as it is not part of the main algorithm. *) let merge_ty t1 t2 = (match (t1, t2) with (VertexT u, VertexT v) -> merge u v env | _ -> error UNKNOWN "merge_ty: not vertex") in let merge_ty_lists ts1 ts2 = if (not (length ts1 = length ts2)) then printf "merge_ty_lists length error\n" else iter2 merge_ty ts1 ts2 in (match (env.type_graph.(u).ty, env.type_graph.(v).ty) with (ClassT (_, n1, ts1), ClassT (_, n2, ts2)) -> if (not (length ts1 = length ts2)) then printf "merge class type error: %s %s\n" n1 n2 else merge_ty_lists ts1 ts2 | (OvldT (_, ts1), OvldT (_, ts2)) -> if (not (length ts1 = length ts2)) then printf "merge overloads error\n" else merge_ty_lists (map snd ts1) (map snd ts2) | (FunT (_, ts1, (rs1,ss1), ps1, (rt1,_,_)), FunT (_, ts2, (rs2,ss2), ps2, (rt2,_,_))) -> if (not (length ts1 = length ts2 && length ps1 = length ps2)) then printf "merge function types length error\n" else (iter2 (fun (cn1,targs1) (cn2,targs2) -> if (not (length targs1 = length targs2)) then printf "merge concept type args error length\n" else merge_ty_lists targs1 targs2) rs1 rs2; iter2 (fun (s1,s2) (t1,t2) -> merge_ty s1 t1; merge_ty s2 t2) ss1 ss2; merge_ty_lists (map (fun (t,_,_) -> t) ps1) (map (fun (t,_,_) -> t) ps2); merge_ty rt1 rt2) | (PtrT (_,VertexT v1), PtrT (_,VertexT v2)) -> merge v1 v2 env | (UnsignedT (_,VertexT v1), UnsignedT (_,VertexT v2)) -> merge v1 v2 env | (SignedT (_,VertexT v1), SignedT (_,VertexT v2)) -> merge v1 v2 env | (ConstT (_,VertexT v1), ConstT (_,VertexT v2)) -> merge v1 v2 env | _ -> ()); (* merge congruent parents of u and v *) let pu = concat (map (fun i -> env.type_graph.(i).pred) (equivalent_to u env)) in let pv = concat (map (fun i -> env.type_graph.(i).pred) (equivalent_to v env)) in union u v env.type_reps; iter (fun x -> iter (fun y -> if not (Union_find.find x env.type_reps = Union_find.find y env.type_reps) then merge x y env else ()) pv) pu and congruent env param_match t1 t2 = (match (t1, t2) with (VarT (_,n), VarT (_,m)) -> n = m || (try assoc n param_match = m with Not_found -> false) | (VertexT i, VertexT j) -> let i = Union_find.find i env.type_reps and j = Union_find.find j env.type_reps in i = j || congruent env param_match (vertex2typ env i) (vertex2typ env j) | (ClassT (_,n,ts1), ClassT (_,m,ts2)) -> if n = m && length ts1 = length ts2 then for_all2 (congruent env param_match) ts1 ts2 else false | (PtrT (_,t1), PtrT (_,t2)) -> congruent env param_match t1 t2 | (UnsignedT (_,t1), UnsignedT (_,t2)) -> congruent env param_match t1 t2 | (SignedT (_,t1), SignedT (_,t2)) -> congruent env param_match t1 t2 | (ConstT (_,t1), ConstT (_,t2)) -> congruent env param_match t1 t2 | (FunT (i,ts1,(rs1,sms1),ss,(s,sv,sm)), FunT (_,ts2,(rs2,sms2),tt,(t,tv,tm))) -> if (length ts1 = length ts2) && (length rs1 = length rs2) && (length sms1 = length sms2) && (length ss = length tt) && sv = tv && sm = tm then let param_match = (combine ts1 ts2) @ param_match in let r = map2 (fun t1 t2 -> (t2, VarT (i,t1))) ts1 ts2 in let tt = map (fun (t,v,m) -> (subst_typ r t, v, m)) tt in let t = subst_typ r t in for_all2 (fun (c1,targs1) (c2,targs2) -> c1 = c2 && for_all2 (fun t1 t2 -> congruent env param_match t1 t2) targs1 targs2) rs1 rs2 && for_all2 (fun (s1,t1) (s2,t2) -> congruent env param_match s1 s2 && congruent env param_match t1 t2) sms1 sms2 && for_all2 (fun (s,sv,sm) (t,tv,tm) -> sv = tv && sm = tm && congruent env param_match s t) ss tt && congruent env param_match s t else false | (AssocT (i,cn1,targs1,tn1), AssocT (_,cn2,targs2,tn2)) -> cn1 = cn2 && tn1 = tn2 && length targs1 = length targs2 && for_all2 (congruent env param_match) targs1 targs2 | (IntT _, IntT _) | (BoolT _, BoolT _) | (FloatT _, FloatT _) | (DoubleT _, DoubleT _) | (LongDoubleT _, LongDoubleT _) | (StringT _, StringT _) | (CharT _, CharT _) | (WCharT _, WCharT _) | (ShortT _, ShortT _) | (LongT _, LongT _) | (LongLongT _, LongLongT _) | (VoidT _, VoidT _) | (NullT _, NullT _) -> true | _ -> false) and extend_env_with_same_type env s t = if debug then printf "asserting same type, %s == %s\n" (g2string_typ s) (g2string_typ t); let (u, env) = add_type_to_graph s env in let (v, env) = add_type_to_graph t env in merge (t2v u) (t2v v) env; print_graph env.type_graph; print_reps env.type_reps; env and extend_env_with_same_types env ss = (match ss with [] -> env | (s,t)::ss -> let env = extend_env_with_same_type env s t in extend_env_with_same_types env ss) and equal_type env s t = let (u, env) = add_type_to_graph s env in let (v, env) = add_type_to_graph t env in let ret = (Union_find.find (t2v u) env.type_reps = Union_find.find (t2v v) env.type_reps || congruent env [] u v) in if !equal_type_debug then printf "%s == %s ? %b\n" (g2string_typ s) (g2string_typ t) ret; ret and unify uvars env (sub : (string * typ) list) (t1 : typ) (t2 : typ) : (string * typ) list = if debug then printf "unify\n" else (); let (u, env) = add_type_to_graph t1 env in let (v, env) = add_type_to_graph t2 env in let sub = basic_unify false uvars env sub u v in let _ = basic_unify true uvars env [] u v in map (fun (n,t) -> (n, vtyp2typ env t)) sub and subtype_unify uvars env (sub : (string * typ) list) (a : exp_typ) (arg : Cpp_ast.exp) (p : exp_typ) : ((string * typ) list * Cpp_ast.exp) = if debug then printf "subtype_unify\n" else (); let (at,av,am) = a and (pt,pv,pm) = p in if !unify_debug then printf "subtype_unify! %s <= %s\n" (g2string_typ at) (g2string_typ pt) else (); let (u, env) = add_type_to_graph at env in let (v, env) = add_type_to_graph pt env in let (sub,e,_,_) = basic_subtype_unify false uvars env sub (u,av,am) at arg (v,pv,pm) pt in let _ = basic_subtype_unify true [] env [] (u,av,am) at arg (v,pv,pm) pt in (*printf "finished basic subtype unify\n";*) let sub = map (fun (n,t) -> (n, vtyp2typ env t)) sub in (*printf "vtyp2typ'd the sub\n";*) (sub, e) and subtype_unify_list check uvars i env sub (ats : exp_typ list) args (ps : exp_typ list) = if debug then printf "subtype_unify_list\n" else (); let rec add_types env ts = (match ts with [] -> ([], env) | t::ts -> let (u, env) = add_type_to_graph t env in let (us, env) = add_types env ts in (u::us, env)) in let (asi,env) = add_types env (map (fun (t,_,_)->t) ats) in let (psi,env) = add_types env (map (fun (t,_,_)->t) ps) in let (sub,args,exact,env) = subtype_unify_list_impl check uvars i env sub asi ats args psi ps in (sub,args,exact, env) (* inner part that does nto add types to the graph *) and subtype_unify_list_impl check uvars i env sub asi (ats : exp_typ list) args psi (ps : exp_typ list) = if debug then printf "subtype_unify_list_impl, args=%s\nparams=%s\n" (String.concat ", " (map g2string_exp_typ ats)) (String.concat ", " (map g2string_exp_typ ps)); print_graph env.type_graph; print_reps env.type_reps; let rec loop check sub atsi ats args psi ps env = let is_elipses p = (match env.type_graph.(Union_find.find (t2v p) env.type_reps).ty with ElipsesT _ -> true | _ -> false) in (match (atsi,ats,args,psi,ps) with ([],[],[],[],[]) -> (sub,[],Exact, env) | (atsi,ats, args, p::psi,ps) when is_elipses p -> (sub, args, TypeCoerce, env) | (ati::atsi, (at,avk,am)::ats, arg::args, pti::psi, (pt,pv,pm)::ps) -> if debug then printf "subtype_unify_list_impl starting\n"; let (sub,arg,exact1,env) = basic_subtype_unify check uvars env sub (ati,avk,am) at arg (pti,pv,pm) pt in if debug then printf "subtype_unify_list_impl substs\n"; print_subst sub; if debug then printf "subtype_unify_list_impl next\n"; let (sub,args,exact2,env) = loop check sub atsi ats args psi ps env in if debug then printf "subtype_unify_list_impl done\n"; print_subst sub; let m = combine_match_kind exact1 exact2 in if debug then printf "%s <= %s is %s\n" (typ2str env ati) (typ2str env pti) (match2str exact1); if debug then printf "rest match = %s\n" (match2str exact2); if debug then printf "combined = %s\n" (match2str m); (sub, arg::args, m, env) | _ -> raise (Unify_failure "Mismatch in length of argument and parameter lists")) in let (sub,args,exact, env) = loop check sub asi ats args psi ps env in if debug then printf "match for params is %s\n" (match2str exact); let sub = map (fun (n,t) -> (n, vtyp2typ env t)) sub in (sub,args,exact, env) and unify_list uvars i env sub ats ps = if debug then printf "unify_list\n" else (); let rec add_types env ts = (match ts with [] -> ([], env) | t::ts -> let (u, env) = add_type_to_graph t env in let (us, env) = add_types env ts in (u::us, env)) in let (asi,env) = add_types env ats in let (psi,env) = add_types env ps in let is_elipses p = (match env.type_graph.(Union_find.find (t2v p) env.type_reps).ty with ElipsesT _ -> true | _ -> false) in let rec loop check sub atsi psi = (match (atsi,psi) with ([],[]) -> sub | (atsi, p::psi) when is_elipses p -> sub | (ati::atsi, pti::psi) -> let sub = basic_unify check uvars env sub ati pti in loop check sub atsi psi | _ -> raise (Unify_failure "")) in let sub = loop false sub asi psi in let _ = loop true sub asi psi in (* This time check non-deducible contexts *) let sub = map (fun (n,t) -> (n, vtyp2typ env t)) sub in sub and subtype env (t1 : exp_typ) (t2 : exp_typ) : bool = if debug then printf "subtype\n" else (); let (t1,v1,m1) = t1 and (t2,v2,m2) = t2 in let (u, env) = add_type_to_graph t1 env in let (v, env) = add_type_to_graph t2 env in basic_subtype [] env (u,v1,m1) (v,v2,m2) let env_add_prim_ovld i (env : environment) (p : primitive) (b : binding) : environment = env_add_ovld_impl (fun p b env -> { env with prims = (p,b)::env.prims }) (fun p env -> assoc p env.prims) i env p b let env_add_ovld i (env : environment) (n : string) (b : binding) : environment = env_add_ovld_impl (fun n b env -> { env with vars = (n,b)::env.vars }) (fun n env -> assoc n env.vars) i env n b (* hmm, not used anymore *) let env_add_ovld_local i (env : environment) (n : string) (b : binding) : environment = env_add_ovld_impl (fun n b env -> { env with local_vars = (n,b)::env.local_vars }) (fun n env -> assoc n env.local_vars) i env n b