Else simplification pass

spectec/src/exe-spectec/main.ml

@@ -27,6 +27,7 @@ type pass =
   | AliasDemut
   | ImproveIds
   | Ite
+  | ElseSimp
   | LetIntro
 
 (* This list declares the intended order of passes.
@@ -43,6 +44,7 @@ let all_passes = [
   Undep;
   Totalize;
   Else;
+  ElseSimp;
   Uncaseremoval;
   Sideconditions;
   SubExpansion;
@@ -114,6 +116,7 @@ let pass_flag = function
   | Uncaseremoval -> "uncase-removal"
   | ImproveIds -> "improve-ids"
   | Ite -> "ite"
+  | ElseSimp -> "else-simplification"
   | LetIntro -> "let-intro"
 
 let pass_desc = function
@@ -129,6 +132,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"
+  | ElseSimp -> "Simplifies generated otherwise relations (after else pass)"
   | LetIntro -> "Let Premise introduction"
 
 
@@ -145,6 +149,7 @@ let run_pass : pass -> Il.Ast.script -> Il.Ast.script = function
   | AliasDemut -> Middlend.AliasDemut.transform
   | ImproveIds -> Middlend.Improveids.transform
   | Ite -> Middlend.Ite.transform
+  | ElseSimp -> Middlend.Elsesimp.transform
   | LetIntro -> Middlend.Letintro.transform
 
 

spectec/src/middlend/dune

@@ -15,6 +15,7 @@
     aliasDemut
     improveids
     ite
+    elsesimp
     letintro
   )
 )

spectec/src/middlend/else.ml

@@ -27,6 +27,8 @@ module StringSet = Set.Make(String)
 
 let env_ref = ref Il.Env.empty
 
+let else_relation_hint_id = "else-relation"
+
 (* Brought from Apart.ml *)
 
 (* Looks at an expression of type list from the back and chops off all
@@ -153,6 +155,8 @@ let unarize rule = match rule.it with
 let not_apart lhs rule = match rule.it with
   | RuleD (_, _, _, lhs2, _) -> not (apart lhs lhs2)
 
+let generate_else_rel_hint rel_id at: hint = { hintid = else_relation_hint_id $ at; hintexp = El.Ast.TextE rel_id.it $ at} 
+
 let rec go hint_map used_names at id mixop typ typ1 prev_rules : rule list -> def list = function
   | [] -> [ RelD (id, mixop, typ, List.rev prev_rules) $ at ]
   | r :: rules -> match r.it with
@@ -177,8 +181,8 @@ let rec go hint_map used_names at id mixop typ typ1 prev_rules : rule list -> de
         else
         [ RelD (aux_name, unary_mixfix, typ1, applicable_prev_rules) $ r.at ] @
         let extra_hintdef = match (StringMap.find_opt id.it hint_map) with
-          | Some hints -> [ HintD (RelH (aux_name, hints) $ at) $ at ]
-          | _ -> []
+          | Some hints -> [ HintD (RelH (aux_name, generate_else_rel_hint id at :: hints) $ at) $ at ]
+          | _ -> [ HintD (RelH (aux_name, [generate_else_rel_hint id at]) $ at) $ at ]
         in
         let prems' = List.map (replace_else aux_name lhs) prems in
         let rule' = { r with it = RuleD (rid, binds, rmixop, exp, prems') } in

spectec/src/middlend/else.mli

@@ -1 +1,2 @@
+val else_relation_hint_id: string
 val transform : Il.Ast.script -> Il.Ast.script

spectec/src/middlend/elsesimp.ml

@@ -0,0 +1,166 @@
+open Il.Ast
+open Util.Source
+open Util
+open Il
+
+module StringMap = Map.Make(String)
+module StringSet = Set.Make(String)
+
+type env =
+{ 
+  il_env : Il.Env.t;
+  mutable rel_to_else_map : text list StringMap.t;
+  mutable else_set_to_remove : StringSet.t;
+  mutable wf_relations : StringSet.t
+}
+
+let new_env il = {
+  il_env = Il.Env.env_of_script il;
+  rel_to_else_map = StringMap.empty;
+  else_set_to_remove = StringSet.empty;
+  wf_relations = StringSet.empty
+}
+
+let is_else_rel_hint hint = hint.hintid.it = Else.else_relation_hint_id
+let is_wf_rel_hint hint = hint.hintid.it = Undep.wf_hint_id
+
+let bind_else_set env id = 
+  env.else_set_to_remove <- StringSet.add id env.else_set_to_remove
+
+let register_else_rel env id base_rel_id =
+  env.rel_to_else_map <- StringMap.update base_rel_id (fun opt -> 
+    match opt with
+    | Some ids -> Some (id.it :: ids)
+    | _ -> Some [id.it]  
+  ) env.rel_to_else_map
+
+let register_wf_rel env id = 
+  env.wf_relations <- StringSet.add id.it env.wf_relations
+
+let rec register_hints env (def : def) =
+  match def.it with
+  | HintD {it = RelH (id, hints); _} when List.exists is_wf_rel_hint hints ->
+    register_wf_rel env id
+  | HintD {it = RelH (id, hints); _} when List.exists is_else_rel_hint hints ->
+    begin match List.find_opt is_else_rel_hint hints with
+    | Some {hintexp = { it = TextE rel_id; _}; _} -> 
+      register_else_rel env id rel_id
+    | _ -> ()
+    end
+  | RecD defs -> List.iter (register_hints env) defs
+  | _ -> ()
+
+let (let*) = Option.bind
+
+let is_boolean_prem prem = 
+  match prem.it with
+  | IfPr _ -> true
+  (* | IterPr (p, _) -> is_boolean_prem p *)
+  | _ -> false
+
+let neg_cmpop cmpop =
+  match cmpop with
+  | `LeOp -> `GtOp
+  | `GtOp -> `LeOp
+  | `GeOp -> `LtOp
+  | `LtOp -> `GeOp
+  | `EqOp -> `NeOp
+  | `NeOp -> `EqOp
+
+let rec neg_exp exp = 
+  { exp with it = 
+  match exp.it with
+  | CmpE (cmpop, optyp, e1, e2) -> CmpE (neg_cmpop cmpop, optyp, e1, e2)
+  | BinE (`AndOp, optyp, e1, e2) -> BinE (`OrOp, optyp, neg_exp e1, neg_exp e2)
+  | BinE (`OrOp, optyp, e1, e2) -> BinE (`AndOp, optyp, neg_exp e1, neg_exp e2)
+  | UnE (`NotOp, _, e1) -> e1.it
+  | _ -> UnE (`NotOp, `BoolT, exp) 
+  }
+
+let get_exp prem =
+  match prem.it with
+  | IfPr exp -> Some (neg_exp exp)
+  | _ -> None
+
+let is_wf_or_neg_prem else_ids env prem =
+  match prem.it with
+  | RulePr (id, _, _) -> StringSet.mem id.it env.wf_relations
+  | NegPr { it = RulePr (id, _, _); _} -> List.mem id.it else_ids
+  | _ -> false
+
+let is_neg_prem else_ids prem = 
+  match prem.it with
+  | NegPr { it = RulePr (id, _, _); _} -> List.mem id.it else_ids
+  | _ -> false
+
+let is_in_bind (free_sets : Free.sets) b = 
+  match b.it with
+  | ExpB (id, _) -> Free.Set.mem id.it free_sets.varid
+  | TypB id -> Free.Set.mem id.it free_sets.typid
+  | DefB (id, _, _) -> Free.Set.mem id.it free_sets.defid
+  | GramB (id, _, _) -> Free.Set.mem id.it free_sets.gramid
+
+let t_rule env else_ids rule = 
+  let RuleD (id, binds, m, exp, prems) = rule.it in
+  let* else_id = List.find_opt (fun id -> List.exists (is_neg_prem [id]) prems) else_ids in
+  let* else_relation = Il.Env.find_opt_rel env.il_env (else_id $ no_region) in
+  let (_, _, rules) = else_relation in
+  let free_vars_binds = Free.free_list Free.bound_bind binds in 
+  let prems', binds' = List.map (fun r ->
+    let RuleD (_, binds', _, _, prems') = r.it in
+    let free_vars = Free.diff (Free.free_list Free.free_prem prems') free_vars_binds in 
+    Lib.List.filter_not (is_wf_or_neg_prem else_ids env) prems', List.filter (is_in_bind free_vars) binds'
+  ) rules |> List.split in
+  let prems', binds' = List.concat prems', List.concat binds' in
+
+  if prems' = [] || not (List.for_all is_boolean_prem prems') then None else
+  let neg_exps = List.filter_map get_exp prems' in
+  match neg_exps with
+  | [] -> None
+  | x :: xs -> 
+    let new_exp = List.fold_left (fun acc exp -> BinE (`OrOp, `BoolT, acc, exp) $$ x.at % (BoolT $ x.at)) x xs in 
+    let new_prem = IfPr new_exp $ x.at in
+    bind_else_set env else_id;
+    Some { rule with it = RuleD (id, binds @ binds', m, exp, new_prem :: Lib.List.filter_not (is_neg_prem else_ids) prems) }
+
+let rec t_def env d = 
+  {d with it = 
+  match d.it with
+  | RelD (id, m, typ, rules) when StringMap.mem id.it env.rel_to_else_map -> 
+    let else_ids = StringMap.find id.it env.rel_to_else_map in
+    RelD (id, m, typ, List.map (fun r -> match (t_rule env else_ids r) with
+      | None -> r
+      | Some r' -> r'
+    ) rules)
+  | RecD defs -> RecD (List.map (t_def env) defs)
+  | d' -> d'
+  }
+
+let is_part_of_else_set env d = 
+  match d.it with
+  | RelD (id, _, _, _) -> StringSet.mem id.it env.else_set_to_remove
+  | _ -> false
+
+let filter_else_set env: (module Iter.Arg) =
+  let module Arg = 
+    struct
+      include Iter.Skip 
+      let visit_prem prem = 
+        match prem.it with
+        | RulePr (id, _, _) when StringSet.mem id.it env.else_set_to_remove -> 
+          env.else_set_to_remove <- StringSet.remove id.it env.else_set_to_remove
+        | _ -> ()
+    end
+  in (module Arg)
+
+let transform defs =
+  let env = new_env defs in
+  List.iter (register_hints env) defs;
+  let defs' = List.map (t_def env) defs in
+  let (module Arg) = filter_else_set env in
+  let module Acc = Iter.Make(Arg) in
+  (* Remove still existing else relations from set*)
+  List.iter Acc.def defs';
+  (* Filter out remaining else relations *)
+  Lib.List.filter_not (is_part_of_else_set env) defs'
+

spectec/src/middlend/elsesimp.mli

@@ -0,0 +1 @@
+val transform : Il.Ast.script -> Il.Ast.script

spectec/src/middlend/undep.ml

@@ -64,6 +64,8 @@ let empty () = {
 let wf_pred_prefix = "wf_"
 let rule_prefix = "case_"
 
+let wf_hint_id = "wf-relation"
+
 (* flag that deactivates adding wellformedness predicates to relations *)
 let deactivate_wfness = false
 
@@ -239,7 +241,9 @@ let get_exp_typ b =
   match b.it with
   | ExpB (id, typ) -> Some (VarE id $$ id.at % typ, typ)
   | _ -> None
-
+
+let generate_well_formed_rel_hint at: hint = { hintid = wf_hint_id $ at; hintexp = El.Ast.SeqE [] $ at} 
+
 let create_well_formed_predicate env id inst = 
   let tf = { base_transformer with transform_exp = t_exp env; transform_typ = t_typ} in
   let at = id.at in 
@@ -250,6 +254,7 @@ let create_well_formed_predicate env id inst =
       | _ -> None
     ) binds) in
   let tupt pairs = TupT (pairs @ [(VarE ("_" $ at) $$ at % user_typ, user_typ)]) $ at in
+  let hint = HintD (RelH (wf_pred_prefix ^ id.it $ id.at, [generate_well_formed_rel_hint at]) $ at) $ at in 
   match inst.it with
   (* Variant well formedness predicate creation *)
   | InstD (binds, _args, {it = VariantT typcases; _}) -> 
@@ -275,10 +280,10 @@ let create_well_formed_predicate env id inst =
     let has_no_prems = List.for_all (fun rule -> match rule.it with
       | RuleD (_, _, _, _, prems) -> prems = []   
     ) rules in
-    if has_no_prems then None else 
-    let relation = RelD (wf_pred_prefix ^ id.it $ id.at, new_mixop dep_exp_typ_pairs, tupt pairs_without_names, rules) $ at in 
+    if has_no_prems then [] else 
+    let relation = RelD (wf_pred_prefix ^ id.it $ id.at, new_mixop dep_exp_typ_pairs, tupt pairs_without_names, rules) $ at in
     bind_wf_set env id.it;
-    Some relation
+    [relation; hint]
 
   (* Struct/Record well formedness predicate creation *)
   | InstD (binds, _args, {it = StructT typfields; _}) -> 
@@ -309,11 +314,11 @@ let create_well_formed_predicate env id inst =
       List.map (transform_prem tf) (new_prems)) $ at 
     in
 
-    if new_prems = [] then None else 
+    if new_prems = [] then [] else 
     let relation = RelD (wf_pred_prefix ^ id.it $ id.at, new_mixop dep_exp_typ_pairs, tupt pairs_without_names, [rule]) $ at in 
     bind_wf_set env id.it;
-    Some relation
-  | _ -> None
+    [relation; hint]
+  | _ -> []
 
 let get_extra_prems env binds exp prems = 
   if deactivate_wfness then [] else 
@@ -397,7 +402,7 @@ let rec t_def env def =
     (TypD (id, List.map (transform_param tf) params |> List.filter is_type_param, [inst]) $ def.at, [])
   | TypD (id, params, [inst]) -> 
     let relation = create_well_formed_predicate env id inst in
-    (TypD (id, List.map (transform_param tf) params |> List.filter is_type_param, [t_inst env inst]) $ def.at, Option.to_list relation)
+    (TypD (id, List.map (transform_param tf) params |> List.filter is_type_param, [t_inst env inst]) $ def.at, relation)
   | TypD (_, _, _) -> 
     error def.at "Multiples instances encountered, please run type family removal pass first."
   | RelD (id, m, typ, rules) -> 

spectec/src/middlend/undep.mli

@@ -1 +1,2 @@
+val wf_hint_id : string
 val transform : Il.Ast.script -> Il.Ast.script

spectec/test-middlend/dune.inc

@@ -5,9 +5,10 @@
 (rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/04-remove-indexed-types.il specification.act/04-remove-indexed-types.il))))
 (rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/05-totalize.il specification.act/05-totalize.il))))
 (rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/06-else.il specification.act/06-else.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-uncase-removal.il specification.act/07-uncase-removal.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/08-sideconditions.il specification.act/08-sideconditions.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/09-sub-expansion.il specification.act/09-sub-expansion.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/10-sub.il specification.act/10-sub.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/11-alias-demut.il specification.act/11-alias-demut.il))))
-(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/12-improve-ids.il specification.act/12-improve-ids.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/07-else-simplification.il specification.act/07-else-simplification.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/08-uncase-removal.il specification.act/08-uncase-removal.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/09-sideconditions.il specification.act/09-sideconditions.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/10-sub-expansion.il specification.act/10-sub-expansion.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/11-sub.il specification.act/11-sub.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/12-alias-demut.il specification.act/12-alias-demut.il))))
+(rule (alias runtest) (deps (alias dune.inc) (file specification.act) (glob_files_rec specification.exp/*)) (action (no-infer (diff specification.exp/13-improve-ids.il specification.act/13-improve-ids.il))))