diff options
| -rw-r--r-- | src/spec_analysis.ml | 448 | ||||
| -rw-r--r-- | src/spec_analysis.mli | 12 |
2 files changed, 460 insertions, 0 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 278243b8..ca005b4b 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -5,6 +5,16 @@ open Type_internal type typ = Type_internal.t +let mt = Nameset.empty + +let set_to_string n = + let rec list_to_string = function + | [] -> "" + | [n] -> n + | n::ns -> n ^ ", " ^ list_to_string ns in + list_to_string (Nameset.elements n) + + (*Query a spec for its default order if one is provided. Assumes Inc if not *) let get_default_order_sp (DT_aux(spec,_)) = match spec with @@ -132,3 +142,441 @@ let is_within_range candidate range constraints = let is_within_machine64 candidate constraints = is_within_range candidate int64_t constraints +(************************************************************************************************) +(*FV finding analysis: identifies the free variables of a function, expression, etc *) + +let id_to_string (Ast.Id_aux (i,_)) = match i with + | Ast.Id s | Ast.DeIid s -> s + +let conditional_add typ_or_exp bound used id = + let known_list = + if typ_or_exp (*true for typ*) + then ["bit";"vector";"unit";"string";"int";"bool"] + else ["=="; "!="; "|";"~";"&";"add_int"] in + let i = (id_to_string id) in + if Nameset.mem i bound || List.mem i known_list + then used + else Nameset.add i used + +let conditional_add_typ = conditional_add true +let conditional_add_exp = conditional_add false + +let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = + match t with + | Typ_wild -> used + | Typ_var (Kid_aux (Var v,l)) -> + if consider_var + then conditional_add_typ bound used (Ast.Id_aux (Ast.Id v,l)) + else used + | Typ_id id -> conditional_add_typ bound used id + | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret + | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used + | Typ_app(id,targs) -> + List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) + +and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with + | Typ_arg_typ t -> fv_of_typ consider_var bound used t + | Typ_arg_nexp n -> fv_of_nexp consider_var bound used n + | _ -> used + +and fv_of_nexp consider_var bound used (Ast.Nexp_aux(n,_)) = match n with + | Nexp_id id -> conditional_add_typ bound used id + | Nexp_var (Ast.Kid_aux (Ast.Var i,_)) -> + if consider_var + then conditional_add_typ bound used (Ast.Id_aux (Ast.Id i, Parse_ast.Unknown)) + else used + | Nexp_times (n1,n2) | Ast.Nexp_sum (n1,n2) | Ast.Nexp_minus(n1,n2) -> + fv_of_nexp consider_var bound (fv_of_nexp consider_var bound used n1) n2 + | Nexp_exp n | Ast.Nexp_neg n -> fv_of_nexp consider_var bound used n + | _ -> used + +let typq_bindings (TypQ_aux(tq,_)) = match tq with + | TypQ_tq quants -> + List.fold_right (fun (QI_aux (qi,_)) bounds -> + match qi with + | QI_id (KOpt_aux(k,_)) -> + (match k with + | KOpt_none (Kid_aux (Var s,_)) -> Nameset.add s bounds + | KOpt_kind (_, Kid_aux (Var s,_)) -> Nameset.add s bounds) + | _ -> bounds) quants mt + | TypQ_no_forall -> mt + +let fv_of_typschm consider_var bound used (Ast.TypSchm_aux ((Ast.TypSchm_ts(typq,typ)),_)) = + let ts_bound = if consider_var then typq_bindings typq else mt in + ts_bound, fv_of_typ consider_var (Nameset.union bound ts_bound) used typ + +let rec pat_bindings consider_var bound used (P_aux(p,_)) = + let list_fv bound used ps = List.fold_right (fun p (b,n) -> pat_bindings consider_var b n p) ps (bound, used) in + match p with + | P_as(p,id) -> let b,ns = pat_bindings consider_var bound used p in + Nameset.add (id_to_string id) b,ns + | P_typ(t,p) -> let ns = fv_of_typ consider_var bound used t in pat_bindings consider_var bound ns p + | P_id id -> Nameset.add (id_to_string id) bound,used + | P_app(id,pats) -> + list_fv bound (Nameset.add (id_to_string id) used) pats + | P_record(fpats,_) -> + List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) -> + pat_bindings consider_var bound used p) fpats (bound,used) + | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats + | P_vector_indexed ipats -> + List.fold_right (fun (_,p) (b,n) -> pat_bindings consider_var b n p) ipats (bound,used) + | _ -> bound,used + +let rec fv_of_exp consider_var bound used set (E_aux (e,_)) : (Nameset.t * Nameset.t * Nameset.t) = + let list_fv b n s es = List.fold_right (fun e (b,n,s) -> fv_of_exp consider_var b n s e) es (b,n,s) in + match e with + | E_block es | Ast.E_nondet es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es -> + list_fv bound used set es + | E_id id -> bound,conditional_add_exp bound used id,set + | E_cast (t,e) -> + let u = fv_of_typ consider_var (if consider_var then bound else mt) used t in + fv_of_exp consider_var bound u set e + | E_app(id,es) -> + let us = conditional_add_exp bound used id in + list_fv bound us set es + | E_app_infix(l,id,r) -> + let us = conditional_add_exp bound used id in + list_fv bound us set [l;r] + | E_if(c,t,e) -> list_fv bound used set [c;t;e] + | E_for(id,from,to_,by,_,body) -> + let _,used,set = list_fv bound used set [from;to_;by] in + fv_of_exp consider_var (Nameset.add (id_to_string id) bound) used set body + | E_vector_indexed (es_i,(Ast.Def_val_aux(default,_))) -> + let bound,used,set = + List.fold_right + (fun (_,e) (b,u,s) -> fv_of_exp consider_var b u s e) es_i (bound,used,set) in + (match default with + | Def_val_empty -> bound,used,set + | Def_val_dec e -> fv_of_exp consider_var bound used set e) + | E_vector_access(v,i) -> list_fv bound used set [v;i] + | E_vector_subrange(v,i1,i2) -> list_fv bound used set [v;i1;i2] + | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e] + | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e] + | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2] + | E_record (FES_aux(FES_Fexps(fexps,_),_)) -> + List.fold_right + (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set) + | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> + let b,u,s = fv_of_exp consider_var bound used set e in + List.fold_right + (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (b,u,s) + | E_field(e,_) -> fv_of_exp consider_var bound used set e + | E_case(e,pes) -> + let b,u,s = fv_of_exp consider_var bound used set e in + fv_of_pes consider_var b u s pes + | E_let(lebind,e) -> + let b,u,s = fv_of_let consider_var bound used set lebind in + fv_of_exp consider_var b u s e + | E_assign(lexp,e) -> + let b,u,s = fv_of_lexp consider_var bound used set lexp in + let _,used,set = fv_of_exp consider_var bound u s e in + b,used,set + | E_exit e -> fv_of_exp consider_var bound used set e + | E_assert(c,m) -> list_fv bound used set [c;m] + | _ -> bound,used,set + +and fv_of_pes consider_var bound used set pes = + match pes with + | [] -> bound,used,set + | Pat_aux(Pat_exp (p,e),_)::pes -> + let bound_p,us_p = pat_bindings consider_var bound used p in + let bound_e,us_e,set_e = fv_of_exp consider_var bound_p us_p set e in + fv_of_pes consider_var bound us_e set_e pes + +and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with + | LB_val_explicit(typsch,pat,exp) -> + let bound_t,us_t = fv_of_typschm consider_var bound used typsch in + let bound_p, us_p = pat_bindings consider_var (Nameset.union bound bound_t) used pat in + let _,us_e,set_e = fv_of_exp consider_var (Nameset.union bound bound_t) used set exp in + (Nameset.union bound_t bound_p),Nameset.union us_t (Nameset.union us_p us_e),set_e + | LB_val_implicit(pat,exp) -> + let bound_p, us_p = pat_bindings consider_var bound used pat in + let _,us_e,set_e = fv_of_exp consider_var bound used set exp in + bound_p,Nameset.union us_p us_e,set_e + +and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,_)) = + match lexp with + | LEXP_id id -> + let i = id_to_string id in + if Nameset.mem i bound + then bound, used, Nameset.add i set + else Nameset.add i bound, Nameset.add i used, set + | LEXP_cast(typ,id) -> + let i = id_to_string id in + let used_t = fv_of_typ consider_var bound used typ in + if Nameset.mem i bound + then bound, used_t, Nameset.add i set + else Nameset.add i bound, Nameset.add i used_t, set + | LEXP_tup(tups) -> + List.fold_right (fun l (b,u,s) -> fv_of_lexp consider_var b u s l) tups (bound,used,set) + | LEXP_memory(id,args) -> + let (bound,used,set) = + List.fold_right + (fun e (b,u,s) -> + fv_of_exp consider_var b u s e) args (bound,used,set) in + bound,Nameset.add (id_to_string id) used,set + | LEXP_field(lexp,_) -> fv_of_lexp consider_var bound used set lexp + | LEXP_vector(lexp,exp) -> + let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in + let _,used,set = fv_of_exp consider_var bound used set exp in + bound_l,used,set + | LEXP_vector_range(lexp,e1,e2) -> + let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in + let _,used,set = fv_of_exp consider_var bound used set e1 in + let _,used,set = fv_of_exp consider_var bound used set e2 in + bound_l,used,set + +let init_env s = Nameset.singleton s + +let typ_variants consider_var bound tunions = + List.fold_right + (fun (Tu_aux(t,_)) (b,n) -> match t with + | Tu_id id -> Nameset.add (id_to_string id) b,n + | Tu_ty_id(t,id) -> Nameset.add (id_to_string id) b, fv_of_typ consider_var b n t) + tunions + (bound,mt) + +let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with + | KD_nabbrev(_,id,_,nexp) -> init_env (id_to_string id), fv_of_nexp consider_var mt mt nexp + | KD_abbrev(_,id,_,typschm) -> + init_env (id_to_string id), snd (fv_of_typschm consider_var mt mt typschm) + | KD_record(_,id,_,typq,tids,_) -> + let binds = init_env (id_to_string id) in + let bounds = if consider_var then typq_bindings typq else mt in + binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt + | KD_variant(_,id,_,typq,tunions,_) -> + let bindings = Nameset.add (id_to_string id) (if consider_var then typq_bindings typq else mt) in + typ_variants consider_var bindings tunions + | KD_enum(_,id,_,ids,_) -> + Nameset.of_list (List.map id_to_string (id::ids)),mt + | KD_register(_,id,n1,n2,_) -> + init_env (id_to_string id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2 + +let fv_of_type_def consider_var (TD_aux(t,_)) = match t with + | TD_abbrev(id,_,typschm) -> init_env (id_to_string id), snd (fv_of_typschm consider_var mt mt typschm) + | TD_record(id,_,typq,tids,_) -> + let binds = init_env (id_to_string id) in + let bounds = if consider_var then typq_bindings typq else mt in + binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt + | TD_variant(id,_,typq,tunions,_) -> + let bindings = Nameset.add (id_to_string id) (if consider_var then typq_bindings typq else mt) in + typ_variants consider_var bindings tunions + | TD_enum(id,_,ids,_) -> + Nameset.of_list (List.map id_to_string (id::ids)),mt + | TD_register(id,n1,n2,_) -> + init_env (id_to_string id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2 + +let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) = + match t with + | Typ_annot_opt_some (typq,typ) -> + let bindings = if consider_var then typq_bindings typq else mt in + let free = fv_of_typ consider_var bindings mt typ in + (bindings,free) + +(*Unlike the other fv, the bound returns are the names bound by the pattern for use in the exp*) +let fv_of_funcl consider_var base_bounds (FCL_aux(FCL_Funcl(id,pat,exp),l)) = + let pat_bs,pat_ns = pat_bindings consider_var base_bounds mt pat in + let _, exp_ns, exp_sets = fv_of_exp consider_var pat_bs pat_ns mt exp in + (pat_bs,exp_ns,exp_sets) + +let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)) = + let fun_name = match funcls with + | [] -> failwith "fv_of_fun fell off the end looking for the function name" + | FCL_aux(FCL_Funcl(id,_,_),_)::_ -> id_to_string id in + let base_bounds = match rec_opt with + | Rec_aux(Ast.Rec_rec,_) -> init_env fun_name + | _ -> mt in + let base_bounds,ns_r = match tannot_opt with + | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) -> + let bindings = if consider_var then typq_bindings typq else mt in + let bound = Nameset.union bindings base_bounds in + bound, fv_of_typ consider_var bound mt typ in + let ns = List.fold_right (fun (FCL_aux(FCL_Funcl(_,pat,exp),_)) ns -> + let pat_bs,pat_ns = pat_bindings consider_var base_bounds ns pat in + let _, exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in + exp_ns) funcls mt in + init_env fun_name,Nameset.union ns ns_r + +let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with + | VS_val_spec(ts,id) | VS_extern_no_rename (ts,id) | VS_extern_spec(ts,id,_)-> + init_env (id_to_string id), snd (fv_of_typschm consider_var mt mt ts) + +let rec find_scattered_of name = function + | [] -> [] + | DEF_scattered (SD_aux(sda,_) as sd):: defs -> + (match sda with + | SD_scattered_function(_,_,_,id) + | SD_scattered_funcl(FCL_aux(FCL_Funcl(id,_,_),_)) + | SD_scattered_unioncl(id,_) -> + if name = id_to_string id + then [sd] else [] + | _ -> [])@ + (find_scattered_of name defs) + | _::defs -> find_scattered_of name defs + +let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,_)) = match sd with + | SD_scattered_function(_,tannot_opt,_,id) -> + let b,ns = (match tannot_opt with + | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) -> + let bindings = if consider_var then typq_bindings typq else mt in + bindings, fv_of_typ consider_var bindings mt typ) in + init_env (id_to_string id),ns + | SD_scattered_funcl (FCL_aux(FCL_Funcl(id,pat,exp),_)) -> + let pat_bs,pat_ns = pat_bindings consider_var mt mt pat in + let _,exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in + let scattered_binds = match pat with + | P_aux(P_app(pid,_),_) -> init_env ((id_to_string id) ^ "/" ^ (id_to_string pid)) + | _ -> mt in + scattered_binds, exp_ns + | SD_scattered_variant (id,_,_) -> + let name = id_to_string id in + let uses = + if consider_scatter_as_one + then + let variant_defs = find_scattered_of name all_defs in + let pieces_uses = + List.fold_right (fun (binds,uses) all_uses -> Nameset.union uses all_uses) + (List.map (fv_of_scattered consider_var false []) variant_defs) mt in + Nameset.remove name pieces_uses + else mt in + init_env name, uses + | SD_scattered_unioncl(id, type_union) -> + let typ_name = id_to_string id in + let b = init_env typ_name in + let (b,r) = typ_variants consider_var b [type_union] in + (Nameset.remove typ_name b, Nameset.add typ_name r) + | SD_scattered_end id -> + let name = id_to_string id in + let uses = if consider_scatter_as_one + (*Note: if this is a function ending, the dec is included *) + then + let scattered_defs = find_scattered_of name all_defs in + List.fold_right (fun (binds,uses) all_uses -> Nameset.union (Nameset.union binds uses) all_uses) + (List.map (fv_of_scattered consider_var false []) scattered_defs) (init_env name) + else init_env name in + init_env (name ^ "/end"), uses + +let fv_of_rd consider_var (DEC_aux (d,_)) = match d with + | DEC_reg(t,id) -> + init_env (id_to_string id), fv_of_typ consider_var mt mt t + | DEC_alias(id,alias) -> + init_env (id_to_string id),mt + | DEC_typ_alias(t,id,alias) -> + init_env (id_to_string id), mt + +let fv_of_def consider_var consider_scatter_as_one all_defs = function + | DEF_kind kdef -> fv_of_kind_def consider_var kdef + | DEF_type tdef -> fv_of_type_def consider_var tdef + | DEF_fundef fdef -> fv_of_fun consider_var fdef + | DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind)) + | DEF_spec vspec -> fv_of_vspec consider_var vspec + | DEF_default def -> mt,mt + | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef + | DEF_reg_dec rdec -> fv_of_rd consider_var rdec + | DEF_comm _ -> mt,mt + +let group_defs consider_scatter_as_one (Ast.Defs defs) = + List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs + +(******************************************************************************* + * Reorder defs take 2 +*) + +(*remove all of ns1 instances from ns2*) +let remove_all ns1 ns2 = + List.fold_right Nameset.remove (Nameset.elements ns1) ns2 + +let remove_from_all_uses bs dbts = + List.map (fun ((b,uses),d) -> (b,remove_all bs uses),d) dbts + +let remove_local_or_lib_vars dbts = + let bound_in_dbts = List.fold_right (fun ((b,_),_) bounds -> Nameset.union b bounds) dbts mt in + let is_bound_in_defs s = Nameset.mem s bound_in_dbts in + let rec remove_from_uses = function + | [] -> [] + | ((b,uses),d)::defs -> + ((b,(Nameset.filter is_bound_in_defs uses)),d)::remove_from_uses defs in + remove_from_uses dbts + +let compare_dbts ((_,u1),_) ((_,u2),_) = Pervasives.compare (Nameset.cardinal u1) (Nameset.cardinal u2) + +let rec print_dependencies orig_queue work_queue names = + match work_queue with + | [] -> () + | ((binds,uses),_)::wq -> + (if not(Nameset.is_empty(Nameset.inter names binds)) + then ((Printf.eprintf "binds of %s has uses of %s\n" (set_to_string binds) (set_to_string uses)); + print_dependencies orig_queue orig_queue uses)); + print_dependencies orig_queue wq names + +let rec topological_sort work_queue defs = + match work_queue with + | [] -> List.rev defs + | ((binds,uses),def)::wq -> + (*Assumes work queue given in sorted order, invariant mantained on appropriate recursive calls*) + if (Nameset.cardinal uses = 0) + then (*let _ = Printf.eprintf "Adding def that binds %s to definitions\n" (set_to_string binds) in*) + topological_sort (remove_from_all_uses binds wq) (def::defs) + else if not(Nameset.is_empty(Nameset.inter binds uses)) + then topological_sort (((binds,(remove_all binds uses)),def)::wq) defs + else + match List.sort compare_dbts work_queue with (*We wait to sort until there are no 0 dependency nodes on top*) + | [] -> failwith "sort shrunk the list???" + | (((n,uses),_)::_) as wq -> + if (Nameset.cardinal uses = 0) + then topological_sort wq defs + else let _ = Printf.eprintf "Uses on failure are %s, binds are %s\n" (set_to_string uses) (set_to_string n) + in let _ = print_dependencies wq wq uses in failwith "A dependency was unmet" + +let rec add_to_partial_order ((binds,uses),def) = function + | [] -> +(* let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n Eol case.\n" (set_to_string binds) (set_to_string uses) in*) + [(binds,uses),def] + | (((bf,uf),deff)::defs as full_defs) -> + (*let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n None eol case. With first def binding %s, uses %s\n" (set_to_string binds) (set_to_string uses) (set_to_string bf) (set_to_string uf) in*) + if Nameset.is_empty uses + then ((binds,uses),def)::full_defs + else if Nameset.subset binds uf (*deff relies on def, so def must be defined first*) + then ((binds,uses),def)::((bf,(remove_all binds uf)),deff)::defs + else if Nameset.subset bf uses (*def relies at least on deff, but maybe more, push in*) + then ((bf,uf),deff)::(add_to_partial_order ((binds,(remove_all bf uses)),def) defs) + else (*These two are unrelated but new def might need to go further in*) + ((bf,uf),deff)::(add_to_partial_order ((binds,uses),def) defs) + +let rec gather_defs name already_included def_bind_triples = + match def_bind_triples with + | [] -> [],already_included,mt + | ((binds,uses),def)::def_bind_triples -> + let (defs,already_included,requires) = gather_defs name already_included def_bind_triples in + let bound_names = Nameset.elements binds in + if List.mem name already_included || List.exists (fun b -> List.mem b already_included) bound_names + then (defs,already_included,requires) + else + let uses = List.fold_right Nameset.remove already_included uses in + if Nameset.mem name binds + then (def::defs,(bound_names@already_included), Nameset.remove name (Nameset.union uses requires)) + else (defs,already_included,requires) + +let rec gather_all names already_included def_bind_triples = + let rec gather ns already_included defs reqs = match ns with + | [] -> defs,already_included,reqs + | name::ns -> + if List.mem name already_included + then gather ns already_included defs (Nameset.remove name reqs) + else + let (new_defs,already_included,new_reqs) = gather_defs name already_included def_bind_triples in + gather ns already_included (new_defs@defs) (Nameset.remove name (Nameset.union new_reqs reqs)) + in + let (defs,already_included,reqs) = gather names already_included [] mt in + if Nameset.is_empty reqs + then defs + else (gather_all (Nameset.elements reqs) already_included def_bind_triples)@defs + +let restrict_defs defs name_list = + let defsno = gather_all name_list [] (group_defs false defs) in + let rdbts = group_defs true (Defs defsno) in + (*let partial_order = + List.fold_left (fun po d -> add_to_partial_order d po) [] rdbts in + let defs = List.map snd partial_order in*) + let defs = topological_sort (List.sort compare_dbts (remove_local_or_lib_vars rdbts)) [] in + Defs defs diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 731bd822..6aeb711b 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -18,3 +18,15 @@ val default_order : tannot defs -> order *) val is_within_range: typ -> typ -> nexp_range list -> triple val is_within_machine64 : typ -> nexp_range list -> triple + +(* free variables and dependencies *) + +(*fv_of_def consider_ty_vars consider_scatter_as_one all_defs all_defs def -> (bound_by_def, free_in_def) *) +val fv_of_def: bool -> bool -> (tannot def) list -> tannot def -> Nameset.t * Nameset.t + +(*group_defs consider_scatter_as_one all_defs -> ((bound_by_def, free_in_def), def) list *) +val group_defs : bool -> tannot defs -> ((Nameset.t * Nameset.t) * (tannot def)) list + +(*reodering definitions, initial functions *) +(* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *) +val restrict_defs : tannot defs -> string list -> tannot defs |