From 0184374f91fd420e6f0439651725f64138df11f0 Mon Sep 17 00:00:00 2001 From: DCupello1 Date: Tue, 10 Feb 2026 11:07:59 +0000 Subject: [PATCH 1/3] Added new subdep pass that preserves type families semantics. --- spectec/src/exe-spectec/main.ml | 7 +- spectec/src/il/walk.ml | 7 +- spectec/src/middlend/dune | 1 + spectec/src/middlend/subdep.ml | 226 ++++++++++++++++++++++++++++++++ spectec/src/middlend/subdep.mli | 1 + spectec/src/middlend/utils.ml | 6 + 6 files changed, 244 insertions(+), 4 deletions(-) create mode 100644 spectec/src/middlend/subdep.ml create mode 100644 spectec/src/middlend/subdep.mli diff --git a/spectec/src/exe-spectec/main.ml b/spectec/src/exe-spectec/main.ml index ae86b09d9e..ab72815628 100644 --- a/spectec/src/exe-spectec/main.ml +++ b/spectec/src/exe-spectec/main.ml @@ -27,6 +27,7 @@ type pass = | AliasDemut | ImproveIds | Ite + | SubDep (* This list declares the intended order of passes. @@ -43,10 +44,11 @@ let all_passes = [ Else; Uncaseremoval; Sideconditions; + SubDep; SubExpansion; Sub; AliasDemut; - ImproveIds + ImproveIds; ] type file_kind = @@ -112,6 +114,7 @@ let pass_flag = function | Uncaseremoval -> "uncase-removal" | ImproveIds -> "improve-ids" | Ite -> "ite" + | SubDep -> "sub-dep" let pass_desc = function | Sub -> "Synthesize explicit subtype coercions" @@ -126,6 +129,7 @@ let pass_desc = function | AliasDemut -> "Lifts type aliases out of mutual groups" | ImproveIds -> "Disambiguates ids used from each other" | Ite -> "If-then-else introduction" + | SubDep -> "Synthesize explicit subtype coercions and expand subtype matching (Dep version)" let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function @@ -141,6 +145,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function | AliasDemut -> Middlend.AliasDemut.transform | ImproveIds -> Middlend.Improveids.transform | Ite -> Middlend.Ite.transform + | SubDep -> Middlend.Subdep.transform (* Argument parsing *) diff --git a/spectec/src/il/walk.ml b/spectec/src/il/walk.ml index c723fe3def..6508359a72 100644 --- a/spectec/src/il/walk.ml +++ b/spectec/src/il/walk.ml @@ -272,7 +272,7 @@ and collect_exp c e = | SubE (e1, t1, t2) -> c_exp e1 $@ collect_typ c t1 $@ collect_typ c t2 in let (res, continue) = f e in - res $@ if continue then traverse_list else c.default + res $@ if continue then traverse_list $@ collect_typ c e.note else c.default and collect_iter c iter = match iter with @@ -289,11 +289,12 @@ and collect_iterexp c iterexp = and collect_path c p = let ( $@ ) = c.compose in - match p.it with + (match p.it with | RootP -> c.default | DotP (p', _) -> collect_path c p' | IdxP (p', e) -> collect_path c p' $@ collect_exp c e - | SliceP (p', e1, e2) -> collect_path c p' $@ collect_exp c e1 $@ collect_exp c e2 + | SliceP (p', e1, e2) -> collect_path c p' $@ collect_exp c e1 $@ collect_exp c e2) $@ + collect_typ c p.note and collect_arg c a = let f = c.collect_arg in diff --git a/spectec/src/middlend/dune b/spectec/src/middlend/dune index c2bc064072..6fa995fe05 100644 --- a/spectec/src/middlend/dune +++ b/spectec/src/middlend/dune @@ -15,5 +15,6 @@ aliasDemut improveids ite + subdep ) ) diff --git a/spectec/src/middlend/subdep.ml b/spectec/src/middlend/subdep.ml new file mode 100644 index 0000000000..73471d9ab4 --- /dev/null +++ b/spectec/src/middlend/subdep.ml @@ -0,0 +1,226 @@ +open Util +open Source +open Il.Ast +open Il +open Il.Walk + +(* Errors *) + +let error at msg = Error.error at "sub expression expansion" msg + +(* Environment *) + +(* Global IL env *) +let env_ref = ref Il.Env.empty + +let empty_tuple_exp at = TupE [] $$ at % (TupT [] $ at) + +(* Computes the cartesian product of a given list. *) +let product_of_lists (lists : 'a list list) = + List.fold_left (fun acc lst -> + List.concat_map (fun existing -> + List.map (fun v -> v :: existing) lst) acc) [[]] lists + +let product_of_lists_append (lists : 'a list list) = + List.fold_left (fun acc lst -> + List.concat_map (fun existing -> + List.map (fun v -> existing @ [v]) lst) acc) [[]] lists + +let get_quant_id q = + match q.it with + | ExpP (id, _) | TypP id + | DefP (id, _, _) | GramP (id, _, _) -> id.it + +let eq_sube (id, t1, t2) (id', t1', t2') = + Eq.eq_id id id' && Eq.eq_typ t1 t1' && Eq.eq_typ t2 t2' + +let collect_sube_exp e = + match e.it with + (* Assumption - nested sub expressions do not exist. Must also be a varE. *) + | SubE ({it = VarE id; _}, t1, t2) -> ([id, t1, t2], false) + | _ -> ([], true) + +let check_matching c_args match_args = + Option.is_some (try + Eval.match_list Eval.match_arg !env_ref Subst.empty c_args match_args + with Eval.Irred -> None) + +let get_case_typ t = + match t.it with + | TupT typs -> typs + | _ -> ["_" $ t.at, t] + +let collect_all_instances case_typ ids at inst = + match inst.it with + | InstD (_, _, {it = VariantT typcases; _}) when + List.for_all (fun (_, (t, _, _), _) -> t.it = TupT []) typcases -> + List.map (fun (m, _, _) -> ([], CaseE (m, empty_tuple_exp no_region) $$ at % case_typ)) typcases + | InstD (_, _, {it = VariantT typcases; _}) -> + let _, new_cases = + List.fold_left (fun (ids', acc) (m, (t, _, _), _) -> + let typs = get_case_typ t in + let new_quants, typs' = Utils.improve_ids_quants ids' true t.at typs in + let exps = List.map (fun (id, t) -> VarE id $$ id.at % t) typs' in + let tup_exp = TupE exps $$ at % t in + let case_exp = CaseE (m, tup_exp) $$ at % case_typ in + let new_ids = List.map get_quant_id new_quants in + (new_ids @ ids', (new_quants, case_exp) :: acc) + ) (ids, []) typcases + in + new_cases + | _ -> error at "Expected a variant type" + +let rec collect_all_instances_typ ids at typ = + match typ.it with + | VarT (var_id, dep_args) -> let (_, insts) = Il.Env.find_typ !env_ref var_id in + (match insts with + | [] -> [] (* Should never happen *) + | _ -> + let inst_opt = List.find_opt (fun inst -> + match inst.it with + | InstD (_, args, _) -> check_matching dep_args args + ) insts in + match inst_opt with + | None -> error at ("Could not find specific instance for typ: " ^ Il.Print.string_of_typ typ) + | Some inst -> collect_all_instances typ ids at inst + ) + | TupT exp_typ_pairs -> + let instances_list = List.map (fun (_, t) -> + collect_all_instances_typ ids at t + ) exp_typ_pairs in + let product = product_of_lists_append instances_list in + List.map (fun lst -> + let quants, exps = List.split lst in + List.concat quants, TupE exps $$ at % typ) product + | _ -> [] + +let compute_cases quants subs = + let ids = List.map get_quant_id quants in + (* Collect all cases for the specific subtype, generating any potential quants in the process *) + let _, cases = + List.fold_left (fun (quants, cases) (id, t1, _) -> + let ids' = List.map get_quant_id quants @ ids in + let instances = collect_all_instances_typ ids' id.at t1 in + let new_quants = List.concat_map fst instances in + let cases'' = List.map (fun case_data -> (id, case_data)) instances in + (new_quants @ quants, cases'' :: cases) + ) (quants, []) subs + in + (* Compute cartesian product for all cases and generate a subst *) + let cases' = product_of_lists cases in + List.map (List.fold_left (fun (quants, subst) (id, (quants', exp)) -> + (quants' @ quants, Il.Subst.add_varid subst id exp)) ([], Il.Subst.empty) + ) cases' + +let collect_typ_fam typ = + match typ.it with + | VarT (id, _) -> + let opt = Env.find_opt_typ !env_ref id in + begin match opt with + | Some (_, insts) when Utils.check_type_family insts -> + ([typ], false) + | _ -> ([], true) + end + | _ -> ([], true) + +let generate_subst_list lhs quants rhs prems = + let base_sube_collector = base_collector [] (@) in + let base_tf_collector = base_collector [] (@) in + let collector = { base_sube_collector with collect_exp = collect_sube_exp } in + let tf_collector = { base_tf_collector with collect_typ = collect_typ_fam } in + let tfs = + List.concat_map (collect_param tf_collector) quants @ + collect_exp tf_collector rhs @ + List.concat_map (collect_prem tf_collector) prems + in + let subs = List.concat_map (collect_arg collector) lhs @ List.concat_map (collect_typ collector) tfs + |> Lib.List.nub eq_sube in + compute_cases quants subs + +let t_clause clause = + match clause.it with + | DefD (quants, lhs, rhs, prems) -> + let subst_list = generate_subst_list lhs quants rhs prems in + List.map (fun (quants', subst) -> + (* Subst all occurrences of the subE id *) + let new_lhs = Il.Subst.subst_args subst lhs in + let new_prems = Il.Subst.subst_list Il.Subst.subst_prem subst prems in + let new_rhs = Il.Subst.subst_exp subst rhs in + + (* Filtering quants - only the subst ids *) + let quants_filtered = Lib.List.filter_not (fun b -> match b.it with + | ExpP (id, _) -> Il.Subst.mem_varid subst id + | _ -> false + ) (quants' @ quants) in + let new_quants, _ = Il.Subst.subst_params subst quants_filtered in + (* Reduction is done here to remove subtyping expressions *) + DefD (new_quants, List.map (Il.Eval.reduce_arg !env_ref) new_lhs, new_rhs, new_prems) $ clause.at + ) subst_list + +let t_inst inst = + match inst.it with + | InstD (quants, lhs, deftyp) -> + let base_sube_collector : (id * typ * typ) list collector = base_collector [] (@) in + let collector = { base_sube_collector with collect_exp = collect_sube_exp } in + (* Collect all unique sub expressions for each argument *) + let subs = List.concat_map (collect_arg collector) lhs |> Lib.List.nub eq_sube in + let subst_list = compute_cases quants subs in + List.map (fun (quants', subst) -> + (* Subst all occurrences of the subE id *) + let new_lhs = Il.Subst.subst_args subst lhs in + let new_rhs = Il.Subst.subst_deftyp subst deftyp in + + (* Filtering quants - only the subst ids *) + let quants_filtered = Lib.List.filter_not (fun b -> match b.it with + | ExpP (id, _) -> Il.Subst.mem_varid subst id + | _ -> false + ) (quants' @ quants) in + + let new_quants, _ = Il.Subst.subst_params subst quants_filtered in + (* Reduction is done here to remove subtyping expressions *) + InstD (new_quants, List.map (Il.Eval.reduce_arg !env_ref) new_lhs, new_rhs) $ inst.at + ) subst_list + +let t_rule rule = + let RuleD (id, quants, m, exp, prems) = rule.it in + let base_tf_collector = base_collector [] (@) in + let tf_collector = { base_tf_collector with collect_typ = collect_typ_fam } in + let tfs = + List.concat_map (collect_param tf_collector) quants @ + collect_exp tf_collector exp @ + List.concat_map (collect_prem tf_collector) prems + in + let base_sub_collector = base_collector [] (@) in + let sub_collector = { base_sub_collector with collect_exp = collect_sube_exp } in + let subs = List.concat_map (collect_typ sub_collector) tfs |> Util.Lib.List.nub eq_sube in + let subst_list = compute_cases quants subs in + List.map (fun (quants', subst) -> + (* Subst all occurrences of the subE id *) + let new_exp = Il.Subst.subst_exp subst exp in + let new_prems = Il.Subst.subst_list Il.Subst.subst_prem subst prems in + + (* Filtering quants - only the subst ids *) + let quants_filtered = Lib.List.filter_not (fun b -> match b.it with + | ExpP (id, _) -> Il.Subst.mem_varid subst id + | _ -> false + ) (quants' @ quants) in + + let new_quants, _ = Il.Subst.subst_params subst quants_filtered in + (* Reduction is done here to remove subtyping expressions *) + RuleD (id, new_quants, m, new_exp, new_prems) $ rule.at + ) subst_list + +let rec t_def def = + match def.it with + | RecD defs -> { def with it = RecD (List.map t_def defs) } + | DecD (id, params, typ, clauses) -> + { def with it = DecD (id, params, typ, List.concat_map t_clause clauses) } + | TypD (id, params, insts) -> + { def with it = TypD (id, params, List.concat_map t_inst insts)} + | RelD (id, quants, mixop, typ, rules) -> + { def with it = RelD (id, quants, mixop, typ, List.concat_map t_rule rules) } + | _ -> def + +let transform (defs : script) = + env_ref := Il.Env.env_of_script defs; + List.map (t_def) defs |> Sub.transform \ No newline at end of file diff --git a/spectec/src/middlend/subdep.mli b/spectec/src/middlend/subdep.mli new file mode 100644 index 0000000000..542bbf8052 --- /dev/null +++ b/spectec/src/middlend/subdep.mli @@ -0,0 +1 @@ +val transform : Il.Ast.script -> Il.Ast.script diff --git a/spectec/src/middlend/utils.ml b/spectec/src/middlend/utils.ml index 2096591915..8a7ce7e4fc 100644 --- a/spectec/src/middlend/utils.ml +++ b/spectec/src/middlend/utils.ml @@ -12,6 +12,12 @@ let check_normal_type_creation (inst : inst) : bool = | _ -> false ) args +let check_type_family insts = + match insts with + | [] -> false + | [inst] when check_normal_type_creation inst -> false + | _ -> true + let rec reduce_type_aliasing env t = match t.it with | VarT(id, args) -> From 09eb09052fb2476c2925643c944466741c3152f2 Mon Sep 17 00:00:00 2001 From: DCupello1 Date: Tue, 10 Feb 2026 11:11:23 +0000 Subject: [PATCH 2/3] Fix on sub in order to take into account of dependent types on projection functions. --- spectec/src/middlend/sub.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index bf692504b6..36eb37eefa 100644 --- a/spectec/src/middlend/sub.ml +++ b/spectec/src/middlend/sub.ml @@ -167,7 +167,7 @@ let rec rename_params s = function let lookup_arg_typ typcases m = List.find_map (fun (m', (arg_typ, _, _), _) -> if Il.Eq.eq_mixop m m' then Some arg_typ else None) typcases -let insert_injections env (def : def) : def list = +let insert_injections transformer env (def : def) : def list = add_type_info env def; let pairs = ready_pairs env in [ def ] @ @@ -184,8 +184,13 @@ let insert_injections env (def : def) : def list = match arg_typ.it, arg_typ2 with | TupT ts, Some {it = TupT ts'; _} -> let quants = List.mapi (fun i (_, arg_typ_i) -> ExpP ("x" ^ string_of_int i $ no_region, arg_typ_i) $ no_region) ts in - let xes is_lhs = List.map2 (fun quant (_, arg_typ_i2) -> - match quant.it with + let vals = List.mapi (fun i (old_id, typ) -> "x" ^ string_of_int i $ no_region, (old_id, typ)) ts in + let subst = List.fold_left (fun subst (new_name, (old_id, old_typ)) -> + Il.Subst.add_varid subst old_id (VarE (new_name) $$ new_name.at % old_typ) + ) Il.Subst.empty vals + in + let xes is_lhs = List.map2 (fun bind (_, arg_typ_i2) -> + match bind.it with | ExpP (x, arg_typ_i) -> let base_exp = VarE x $$ no_region % arg_typ_i in if is_lhs || Il.Eq.eq_typ arg_typ_i arg_typ_i2 @@ -194,9 +199,11 @@ let insert_injections env (def : def) : def list = | TypP _ | DefP _ | GramP _ -> assert false) quants ts' in let xe is_lhs = TupE (xes is_lhs) $$ no_region % arg_typ in - DefD (quants, - [ExpA (CaseE (m, xe true) $$ no_region % real_ty) $ no_region], - t_exp env (CaseE (m, xe false) $$ no_region % sup_ty), []) $ no_region + let lhs = ExpA (CaseE (m, xe true) $$ no_region % real_ty) $ no_region in + let rhs = transform_exp transformer (CaseE (m, xe false) $$ no_region % sup_ty) in + DefD (Il.Subst.subst_params subst quants |> fst, + [Il.Subst.subst_arg subst lhs], + Il.Subst.subst_exp subst rhs, []) $ no_region | _ -> let x = "x" $ no_region in let xe = VarE x $$ no_region % arg_typ in @@ -213,6 +220,6 @@ let transform (defs : script) = let transformer = { base_transformer with transform_exp = t_exp env } in let defs' = List.map (transform_def transformer) defs in env.pairs_mutable <- false; - let defs'' = List.concat_map (insert_injections env) defs' in + let defs'' = List.concat_map (insert_injections transformer env) defs' in S.iter (fun (sub, sup) -> error sup.at ("left-over subtype coercion `" ^ sub.it ^ "` <: `" ^ sup.it ^ "`")) env.pairs; defs'' From c4c5fafa91fb2f03df3b50d48feac59c28b51cbc Mon Sep 17 00:00:00 2001 From: DCupello1 Date: Tue, 10 Feb 2026 12:03:21 +0000 Subject: [PATCH 3/3] Fixed improvedids pass so that reduction of types works with an updated environment. --- spectec/src/middlend/improveids.ml | 37 +++++++++++++++++------------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/spectec/src/middlend/improveids.ml b/spectec/src/middlend/improveids.ml index 0d1125c8f4..348ed1ff36 100644 --- a/spectec/src/middlend/improveids.ml +++ b/spectec/src/middlend/improveids.ml @@ -14,7 +14,7 @@ module StringSet = Set.Make(String) type env = { mutable atom_str_set : StringSet.t; - il_env : Il.Env.t; + mutable il_env : Il.Env.t; } let make_prefix = "mk_" @@ -99,6 +99,17 @@ let rec check_iteration_naming e iterexp = Eq.eq_id id id' && check_iteration_naming e i | _ -> false +and create_transformer env = + { base_transformer with + transform_exp = t_exp env; + transform_typ = t_typ env; + transform_path = t_path env; + transform_var_id = t_var_id env; + transform_typ_id = t_user_def_id env; + transform_rel_id = t_user_def_id env; + transform_def_id = t_def_id env; + } + and t_typ env t = (match t.it with | VarT (id, []) when not (Env.mem_typ env.il_env id) -> @@ -111,12 +122,12 @@ and t_exp env e = (match e.it with | CaseE (m, e1) -> let id = Print.string_of_typ_name (Eval.reduce_typ env.il_env e.note) in - CaseE(transform_mixop env id m, e1) + CaseE (transform_mixop env id m, e1) | StrE fields -> let id = Print.string_of_typ_name (Eval.reduce_typ env.il_env e.note) in StrE (List.map (fun (a, e1) -> (transform_atom env id a, e1)) fields) | UncaseE (e1, m) -> - let id = Print.string_of_typ_name (Eval.reduce_typ env.il_env e.note) in + let id = Print.string_of_typ_name (Eval.reduce_typ env.il_env e1.note) in UncaseE (e1, transform_mixop env id m) | DotE (e1, a) -> let id = Print.string_of_typ_name (Eval.reduce_typ env.il_env e1.note) in @@ -165,16 +176,8 @@ let transform_rule tf env rel_id rule = ) $ rule.at let rec t_def env def = - let tf = { base_transformer with - transform_exp = t_exp env; - transform_typ = t_typ env; - transform_path = t_path env; - transform_var_id = t_var_id env; - transform_typ_id = t_user_def_id env; - transform_rel_id = t_user_def_id env; - transform_def_id = t_def_id env; - } in - (match def.it with + let tf = create_transformer env in + let def = (match def.it with | TypD (id, params, insts) -> TypD (t_user_def_id env id, List.map (transform_param tf) params |> Utils.improve_ids_params, @@ -196,7 +199,9 @@ let rec t_def env def = List.map (transform_prod tf) prods) | RecD defs -> RecD (List.map (t_def env) defs) | HintD hintdef -> HintD hintdef - ) $ def.at + ) $ def.at in + env.il_env <- Env.env_of_def env.il_env def; + def let create_env il = { atom_str_set = StringSet.empty; @@ -204,5 +209,5 @@ let create_env il = { } let transform (il : script): script = - let env = create_env il in - List.map (t_def env) il \ No newline at end of file + let env = create_env il in + List.map (t_def env) il