Middlend Fixes

spectec/src/exe-spectec/main.ml

@@ -152,6 +152,16 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | LetIntroMech -> Middlend.Letintromech.transform
   | ElseSimp -> Middlend.Elsesimp.transform
 
+(* Argument parsing - Specific for undep pass *)
+let set_wf_state s =
+  Middlend.Undep.wf_state :=
+    match s with
+    | "minimal" -> Middlend.Undep.WfMinimal
+    | "all" -> Middlend.Undep.WfAll
+    | "none" -> Middlend.Undep.WfNone
+    | _ ->
+        raise (Arg.Bad "wf-state must be minimal, all, or none")
+
 (* Argument parsing *)
 
 let banner () =
@@ -224,7 +234,11 @@ let argspec = Arg.align (
   "--all-passes", Arg.Unit (fun () -> List.iter enable_pass all_passes)," Run all passes";
 
   "--test-version", Arg.Int (fun i -> Backend_interpreter.Construct.version := i; Il2al.Translate.version := i), " Wasm version to assume for tests (default: 3)";
-
+  "--wf-state", Arg.String set_wf_state, " Denotes the placement of wfness relations for the remove-indexed-types pass 
+    (default: minimal):
+    minimal: Places wfness premises for terms that do not appear in the conclusion
+    all: Places wfness premises whenever it encounters a term that needs it
+    none: Does not place any wfness premises";
   "-help", Arg.Unit ignore, "";
   "--help", Arg.Unit ignore, "";
 ] )

spectec/src/il/iter.ml

@@ -19,6 +19,7 @@ sig
   val visit_typ : typ -> unit
   val visit_deftyp : deftyp -> unit
   val visit_exp : exp -> unit
+  val visit_arg : arg -> unit
   val visit_path : path -> unit
   val visit_sym : sym -> unit
   val visit_prem : prem -> unit
@@ -46,6 +47,7 @@ struct
   let visit_typ _ = ()
   let visit_deftyp _ = ()
   let visit_exp _ = ()
+  let visit_arg _ = ()
   let visit_path _ = ()
   let visit_sym _ = ()
   let visit_prem _ = ()
@@ -219,6 +221,7 @@ and prems prs = list prem prs
 (* Definitions *)
 
 and arg a =
+  visit_arg a;
   match a.it with
   | ExpA e -> exp e
   | TypA t -> typ t
@@ -268,4 +271,4 @@ let rec def d =
   | GramD (x, ps, t, prods) -> gramid x; params ps; typ t; list prod prods
   | RecD ds -> list def ds
   | HintD hd -> hintdef hd
-end
+end

spectec/src/il/walk.ml

@@ -226,6 +226,8 @@ type 'a collector = {
   default: 'a;
   compose: 'a -> 'a -> 'a;
   collect_exp: exp -> 'a * bool;
+  collect_path: path -> 'a * bool;
+  collect_quant: quant -> 'a * bool;
   collect_prem: prem -> 'a * bool;
   collect_iterexp: iterexp -> 'a * bool;
   collect_typ: typ -> 'a * bool;
@@ -238,6 +240,8 @@ let base_collector default compose = {
   default = default;
   compose = compose;
   collect_exp = no_collect default;
+  collect_path = no_collect default;
+  collect_quant = no_collect default;
   collect_prem = no_collect default;
   collect_iterexp = no_collect default;
   collect_typ = no_collect default;
@@ -301,11 +305,16 @@ and collect_iterexp c iterexp =
 
 and collect_path c p =
   let ( $@ ) = c.compose in
-  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
+  let f = c.collect_path in
+  let traverse_list = 
+    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
+  in
+  let (res, continue) = f p in
+  res $@ if continue then traverse_list else c.default
 
 and collect_arg c a =
   let f = c.collect_arg in
@@ -342,6 +351,13 @@ and collect_param c p =
   | DefP (_, params, typ) -> compose_list c (collect_param c) params $@ collect_typ c typ
   | GramP (_, params, typ) -> compose_list c (collect_param c) params $@ collect_typ c typ
 
+and collect_quant c q =
+  let ( $@ ) = c.compose in
+  let f = c.collect_quant in
+  let traverse_list = collect_param c q in
+  let (res, continue) = f q in
+  res $@ if continue then traverse_list else c.default
+
 and collect_sym c s =
   let ( $@ ) = c.compose in
   match s.it with

spectec/src/middlend/improveids.ml

@@ -4,6 +4,7 @@ open Il.Walk
 open Util.Source
 (* open Util *)
 open Xl.Atom
+open Xl
 
 module StringMap = Map.Make(String)
 module StringSet = Set.Make(String)
@@ -19,19 +20,20 @@ let fun_prefix = "fun_"
 let res_prefix = "r_"
 
 type id_type = 
-  | VAR         (* Variables *)
-  | USERDEF     (* Types, type constructors and relations *)
-  | FUNCDEF     (* function definitions *)
+  | Var         (* Variables *)
+  | Userdef     (* Types and relations *)
+  | Funcdef     (* function definitions *)
+  | Atoms       (* Type constructors *)
 
-let empty_info: region * Xl.Atom.info = (no_region, {def = ""; case = ""})
+let empty_info typ_id: region * Xl.Atom.info = (no_region, {def = typ_id; case = ""})
 
 (* Id transformation *)
-let rec transform_id' (env : env) (id_type : id_type) (s : text) = 
-  let t_func = transform_id' env id_type in 
+let transform_id' (env : env) (id_type : id_type) (s : text) = 
   let change_id s' = 
     String.map (function
      | '.' -> '_'
      | '-' -> '_'
+     | '#' -> '_'
      | c -> c
     ) s'
     (* This suffixes any '*' with '_lst' and '?' with '_opt' for clarity *)
@@ -42,24 +44,26 @@ let rec transform_id' (env : env) (id_type : id_type) (s : text) =
   match id_type with
   (* Leave naming hole as is *)
   | _ when s' = "_" -> s' 
-  | VAR when Il.Env.mem_typ env.il_env (s' $ no_region) 
+  | Var when Il.Env.mem_typ env.il_env (s' $ no_region) 
     || Il.Env.mem_rel env.il_env (s' $ no_region) 
     || Il.Env.mem_def env.il_env (s' $ no_region) 
-    || StringSet.mem s' env.atom_str_set -> t_func (var_prefix ^ s')
-  | FUNCDEF when Il.Env.mem_typ env.il_env (s' $ no_region) 
+    || StringSet.mem s' env.atom_str_set -> (var_prefix ^ s')
+  | Funcdef when Il.Env.mem_typ env.il_env (s' $ no_region) 
     || Il.Env.mem_rel env.il_env (s' $ no_region) 
-    || StringSet.mem s' env.atom_str_set -> t_func (fun_prefix ^ s')
+    || StringSet.mem s' env.atom_str_set -> (fun_prefix ^ s')
+  | Userdef when StringSet.mem s' env.atom_str_set -> (res_prefix ^ s')
   (* Checking whether an id is an int - if so, put a reserved prefix *)
-  | _ when Option.is_some (int_of_string_opt s') -> t_func (res_prefix ^ s')
+  | _ when Option.is_some (int_of_string_opt s') -> (res_prefix ^ s')
   | _ -> s'
 
-let t_var_id env id = transform_id' env VAR id.it $ id.at
-let t_def_id env id = transform_id' env FUNCDEF id.it $ id.at
-let t_user_def_id env id = transform_id' env USERDEF id.it $ id.at
+let t_var_id env id = transform_id' env Var id.it $ id.at
+let t_def_id env id = transform_id' env Funcdef id.it $ id.at
+let t_user_def_id env id = transform_id' env Userdef id.it $ id.at
+let t_atom_id env id = transform_id' env Atoms id.it $ id.at
 let transform_rule_id env rule_id rel_id = 
   match rule_id.it with
   | "" -> make_prefix ^ rel_id.it
-  | _ -> transform_id' env USERDEF rule_id.it
+  | _ -> transform_id' env Atoms rule_id.it
 
 let is_atomid a = 
   match a.it with
@@ -71,22 +75,37 @@ let has_atom_hole m =
   | [{it = Atom "_"; _}] -> true
   | _ -> false
 
+let register_atom_id env s =
+  env.atom_str_set <- StringSet.add s env.atom_str_set
+
 (* Atom functions *)
 let transform_atom env typ_id a = 
   match a.it with
-  | Atom s -> Atom (t_user_def_id env (s $ a.at)).it $$ a.at % a.note
-  | _ -> Atom (make_prefix ^ typ_id) $$ a.at % a.note
+  | Atom s -> 
+    register_atom_id env (t_atom_id env (s $ a.at)).it;
+    Atom (t_atom_id env (s $ a.at)).it $$ a.at % a.note
+  | _ -> 
+    register_atom_id env (make_prefix ^ typ_id);
+    Atom (make_prefix ^ typ_id) $$ a.at % a.note
+
+(* Atom transformation where there might be other atom constructs, leave them be *)
+let transform_atom' env a = 
+  match a.it with
+  | Atom s -> 
+    register_atom_id env (t_atom_id env (s $ a.at)).it;
+    Atom (t_atom_id env (s $ a.at)).it $$ a.at % a.note
+  | _ -> a
 
 let transform_mixop env typ_id (m : mixop) =
-(* TODO! Not sure what the expected result is for this one. *)
-ignore (env, typ_id, empty_info, is_atomid, has_atom_hole, transform_atom); m
-(*
-  let m' = List.map (fun inner_m -> List.filter is_atomid inner_m) m in
+  let m' = List.map (fun inner_m -> List.filter is_atomid inner_m) (Mixop.flatten m) in
   let len = List.length m' in 
   match m' with
-  | _ when List.for_all (fun l -> l = [] || has_atom_hole l) m' -> [(Atom (make_prefix ^ typ_id) $$ empty_info)] :: List.init (len - 1) (fun _ -> [])
-  | _ -> Xl.Mixop.map_atoms (transform_atom env typ_id)) m'
-*)
+  | _ when List.for_all (fun l -> l = [] || has_atom_hole l) m' -> 
+    register_atom_id env (make_prefix ^ typ_id);
+    let atom = Xl.Mixop.Atom (Atom (make_prefix ^ typ_id) $$ empty_info typ_id) in
+    Xl.Mixop.(Seq (atom :: List.init (len - 1) (fun _ -> Arg ())))
+  | _ -> Xl.Mixop.map_atoms (transform_atom' env) m
+
 
 let rec check_iteration_naming e iterexp = 
   match e.it, iterexp with
@@ -95,14 +114,6 @@ let rec check_iteration_naming e iterexp =
     Eq.eq_id id id' && check_iteration_naming e i
   | _ -> false 
 
-and t_typ env t = 
-  (match t.it with
-  | VarT (id, []) when not (Env.mem_typ env.il_env id) -> 
-    (* Type parameter - treat it as such *)
-    VarT (t_var_id env id, [])
-  | typ -> typ
-  ) $ t.at
-
 and t_exp env e = 
   (match e.it with
   | CaseE (m, e1) -> 
@@ -160,10 +171,31 @@ let transform_rule tf env rel_id rule =
   )
   ) $ rule.at
 
+let is_wf_hint hintid = hintid.it = Undep.wf_hint_id
+let transform_el_exp env hintid e = 
+  (match e.it with
+  | El.Ast.VarE (id, args) when is_wf_hint hintid -> El.Ast.VarE (t_user_def_id env id, args)
+  | e' -> e'
+  ) $ e.at
+
+let transform_hintdef env hintdef = 
+  let t_hint h = 
+    { h with hintexp = transform_el_exp env h.hintid h.hintexp} 
+  in
+  let t_hints hs = List.map t_hint hs in
+  let h = match hintdef.it with
+  | TypH (id, hints) -> TypH (t_user_def_id env id, t_hints hints)
+  | RelH (id, hints) -> RelH (t_user_def_id env id, t_hints hints)
+  | DecH (id, hints) -> DecH (t_user_def_id env id, t_hints hints)
+  | GramH (id, hints) -> GramH (t_user_def_id env id, t_hints hints)
+  | RuleH (id, rid, hints) -> 
+    RuleH (t_user_def_id env id, transform_rule_id env rid id $ rid.at, t_hints hints)
+  in
+  { hintdef with it = h }
+
 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;
@@ -191,7 +223,7 @@ let rec t_def env def =
     transform_typ tf typ, 
     List.map (transform_prod tf) prods)
   | RecD defs -> RecD (List.map (t_def env) defs)
-  | HintD hintdef -> HintD hintdef
+  | HintD hintdef -> HintD (transform_hintdef env hintdef)
   ) $ def.at
 
 let create_env il = {

spectec/src/middlend/improveids.mli

@@ -2,15 +2,30 @@
   This pass simply ensures that there is no ambiguity between any names.
 
   It does this by creating a massive set of names, separated by the
-  different main constructs (i.e. TypD, RelD, DecD, etc.).
+  different namespaces (i.e. TypD, RelD, DecD, etc.). This is done using
+  the existing environment generator that the IL has.
 
-  It makes sure that variables don't have the same name as anything else,
-  as this could cause shadowing in some cases for ITPs. If it does have
-  the same name, then it adds the prefix "v_" until the name is unique.
+  It makes sure that variables don't have the same name as any other
+  namespace, as this could cause shadowing in some cases for ITPs. 
+  If it does have the same name, then it adds the prefix 
+  "v_".
 
-  For functions, we unsure that they don't have the same name as
+  For functions, we ensure that they don't have the same name as
   user-defined types and relations. If it does, then it adds the prefix
-  "fun_" until the name is unique.
+  "fun_".
+
+  For user-defined types and relations, we make sure that they don't have
+  the same name as Atoms. If it does, then it adds the prefix "r_"
+
+  Atoms are considered a namespace as well, and it is made sure that the
+  other namespaces don't clash with this one. However, no disambiguation
+  is made for Atoms of the same name. This is due to some ITPs having
+  already builtin mechanisms to handle this.
+
+  NOTE: This is not a guaranteed name clash avoidance pass, as it has a very
+  naive renaming strategy. This will get revisited in the future 
+  to ensure that this works for all cases
+  but for now it is sufficient.
 
 *)
 

spectec/src/middlend/sideconditions.ml

@@ -6,7 +6,7 @@ open Il.Walk
 
 (* Errors *)
 
-let error at msg = Error.error at "side condition" msg
+let _error at msg = Error.error at "side condition" msg
 
 module Env = Map.Make(String)
 
@@ -21,6 +21,7 @@ let iterPr (pr, (iter, vars)) =
   let vars' = List.filter (fun (id, _) ->
     Set.mem id.it frees.varid
   ) vars in
+  if iter <= List1 && vars' = [] then pr.it else 
   IterPr (pr, (iter, vars'))
 
 let is_null e = CmpE (`EqOp, `BoolT, e, OptE None $$ e.at % e.note) $$ e.at % (BoolT $ e.at)
@@ -68,6 +69,7 @@ let rec t_exp env e =
     collect_iter collector1 iter @ 
     List.map (fun pr -> iterPr (pr, iterexp) $ e.at) (collect_exp collector2 e1), false)
   | _ -> ([], true)
+
 and t_prem env prem =
   let res, continue = (match prem.it with
   | IterPr (prem', ((iter, _) as iterexp))
@@ -127,7 +129,7 @@ let t_params env =
   List.fold_left (fun env param ->
     match param.it with
     | ExpP (v, t) -> Env.add v.it t env
-    | TypP _ | DefP _ | GramP _ -> error param.at "unexpected paramater or quantifier in rule"
+    | _ -> env
   ) env
 
 let t_rule' env = function

spectec/src/middlend/sub.ml

@@ -148,7 +148,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 ] @
@@ -177,7 +177,7 @@ let insert_injections env (def : def) : def list =
         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
+          transform_exp transformer (CaseE (m, xe false) $$ no_region % sup_ty), []) $ no_region
       | _ ->
         let x = "x" $ no_region in
         let xe = VarE x $$ no_region % arg_typ in
@@ -194,6 +194,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''