Dependent types Mechanization backend

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 *)

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

spectec/src/middlend/dune

@@ -15,5 +15,6 @@
     aliasDemut
     improveids
     ite
+    subdep
   )
 )

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,13 +199,15 @@ 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;
   il_env = Env.env_of_script il
 }
 
 let transform (il : script): script =
-  let env = create_env il in 
-  List.map (t_def env) il
+  let env = create_env il in  
+  List.map (t_def env) il

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''