Il-to-Il: General otherwise elimination [archival branch]

spectec/src/exe-watsup/main.ml

@@ -33,6 +33,7 @@ let pass_sub = ref false
 let pass_totalize = ref false
 let pass_unthe = ref false
 let pass_sideconditions = ref false
+let pass_else_elim = ref false
 
 
 (* Argument parsing *)
@@ -69,6 +70,7 @@ let argspec = Arg.align
   "--totalize", Arg.Set pass_totalize, "Run function totalization";
   "--the-elimination", Arg.Set pass_unthe, "Eliminate the ! operator in relations";
   "--sideconditions", Arg.Set pass_sideconditions, "Infer side conditoins";
+  "--else-elimination", Arg.Set pass_else_elim, "Eliminate otherwise/else";
 
   "-help", Arg.Unit ignore, "";
   "--help", Arg.Unit ignore, "";
@@ -135,6 +137,17 @@ let () =
       )
     in
 
+    let il = if not !pass_else_elim then il else
+      ( log "Else elimination";
+        let il = Middlend.Else.transform il in
+        if !print_all_il then
+          Printf.printf "%s\n%!" (Il.Print.string_of_script il);
+        log "IL Validation...";
+        Il.Validation.valid il;
+        il
+      )
+    in
+
     if !print_final_il && not !print_all_il then
       Printf.printf "%s\n%!" (Il.Print.string_of_script il);
 

spectec/src/frontend/multiplicity.ml

@@ -302,6 +302,9 @@ and annot_prem env prem : Il.Ast.premise * occur =
       let prem1', occur1 = annot_prem env prem1 in
       let iter', occur' = annot_iterexp env occur1 iter prem.at in
       IterPr (prem1', iter'), occur'
+    | NegPr prem1 ->
+      let prem1', occur = annot_prem env prem1 in
+      NegPr prem1', occur
   in {prem with it}, occur
 
 let annot_exp env e =

spectec/src/il/apart.ml

@@ -0,0 +1,62 @@
+(*
+This module implements a (consservative) apartness check: Given two (open)
+expression (typically reduction rules LHSs), are they definitely apart.
+*)
+
+open Util.Source
+open Ast
+
+(* Looks at an expression of type list from the back and chops off all
+   known _elements_, followed by the list of all list expressions.
+   Returns it all in reverse order.
+ *)
+let rec to_snoc_list (e : exp) : exp list * exp list = match e.it with
+  | ListE es -> List.rev es, []
+  | CatE (e1, e2) ->
+    let tailelems2, listelems2 = to_snoc_list e2 in
+    if listelems2 = []
+    (* Second list is fully known? Can look at first list *)
+    then let tailelems1, listelems1 = to_snoc_list e1 in
+         tailelems2 @ tailelems1, listelems1
+    (* Second list has unknown elements, have to stop there *)
+    else tailelems2, listelems2 @ [e1]
+  | _ -> [], [e]
+
+(* We assume the expressions to be of the same type; for ill-typed inputs
+   no guarantees are made. *)
+let rec apart (e1 : exp) (e2: exp) : bool =
+  if Eq.eq_exp e1 e2 then false else
+  (*
+  (fun b -> if not b then Printf.eprintf "apart\n  %s\n  %s\n  %b\n" (Print.string_of_exp e1) (Print.string_of_exp e2) b; b)
+  *)
+  (match e1.it, e2.it with
+  (* A literal is never a literal of other type *)
+  | NatE n1, NatE n2 -> not (n1 = n2)
+  | BoolE b1, BoolE b2 -> not (b1 = b2)
+  | TextE t1, TextE t2 -> not (t1 = t2)
+  | CaseE (a1, exp1), CaseE (a2, exp2) ->
+    not (a1 = a2) || apart exp1 exp2
+  | TupE es1, TupE es2 when List.length es1 = List.length es2 ->
+    List.exists2 apart es1 es2
+  | (CatE _ | ListE _), (CatE _ | ListE _) ->
+    list_exp_apart e1 e2
+  | SubE (e1, _, _), SubE (e2, _, _) -> apart e1 e2
+  | MixE (mixop1, e1), MixE (mixop2, e2) ->
+    not (mixop1 = mixop2) || apart e1 e2
+  (* We do not know anything about variables and functions *)
+  | _ , _ -> false (* conservative *)
+  )
+
+(* Two list expressions are apart if either their manifest tail elements are apart *)
+and list_exp_apart e1 e2 = snoc_list_apart (to_snoc_list e1) (to_snoc_list e2)
+
+and snoc_list_apart (tailelems1, listelems1) (tailelems2, listelems2) =
+  match tailelems1, listelems1, tailelems2, listelems2 with
+  (* If the heads are apart, the lists are apart *)
+  | e1 :: e1s, _, e2 :: e2s, _ -> apart e1 e2 || snoc_list_apart (e1s, listelems1) (e2s, listelems2)
+  (* If one list is definitely empty and the other list definitely isn't *)
+  | [], [], _ :: _, _ -> false
+  | _ :: _, _, [], [] -> false
+  (* Else, can't tell *)
+  | _, _, _, _ -> false
+

spectec/src/il/apart.mli

@@ -0,0 +1,2 @@
+open Ast
+val apart : exp -> exp -> bool

spectec/src/il/ast.ml

@@ -158,6 +158,7 @@ and premise' =
   | IfPr of exp                                       (* side condition *)
   | ElsePr                                            (* otherwise *)
   | IterPr of premise * iterexp                       (* iteration *)
+  | NegPr of premise                                  (* negation of a premise *)
 
 and hintdef = hintdef' phrase
 and hintdef' =

spectec/src/il/dune

@@ -1,5 +1,5 @@
 (library
   (name il)
   (libraries util)
-  (modules ast eq free print validation)
+  (modules ast eq free print validation apart)
 )

spectec/src/il/eq.ml

@@ -105,4 +105,5 @@ let rec eq_prem prem1 prem2 =
   | ElsePr, ElsePr -> true
   | IterPr (prem1, e1), IterPr (prem2, e2) ->
     eq_prem prem1 prem2 && eq_iterexp e1 e2
+  | NegPr prem1, NegPr prem2 -> eq_prem prem1 prem2
   | _, _ -> false

spectec/src/il/free.ml

@@ -127,6 +127,7 @@ let rec free_prem prem =
   | IfPr e -> free_exp e
   | ElsePr -> empty
   | IterPr (prem', iter) -> union (free_prem prem') (free_iterexp iter)
+  | NegPr prem' -> free_prem prem'
 
 let free_rule rule =
   match rule.it with

spectec/src/il/print.ml

@@ -203,6 +203,7 @@ let rec string_of_prem prem =
     string_of_prem prem' ^ string_of_iterexp iter
   | IterPr (prem', iter) ->
     "(" ^ string_of_prem prem' ^ ")" ^ string_of_iterexp iter
+  | NegPr prem' -> "unless " ^ string_of_prem prem'
 
 let region_comment indent at =
   if at = no_region then "" else

spectec/src/il/validation.ml

@@ -503,6 +503,8 @@ let rec valid_prem env prem =
   | IterPr (prem', iter) ->
     let env' = valid_iterexp env iter in
     valid_prem env' prem'
+  | NegPr prem' ->
+    valid_prem env prem'
 
 
 let valid_rule env mixop t rule =

spectec/src/middlend/dune

@@ -1,5 +1,5 @@
 (library
   (name middlend)
   (libraries util il)
-  (modules sub totalize unthe sideconditions)
+  (modules sub totalize unthe sideconditions else)
 )

spectec/src/middlend/else.ml

@@ -0,0 +1,79 @@
+(*
+This transformation removes uses of the `otherwise` (`ElsePr`) premise from
+inductive relations.
+
+It only supports binary relations.
+
+1. It figures out which rules are meant by “otherwise”:
+
+   * All previous rules
+   * Excluding those that definitely can’t apply when the present rule applies
+     (decided by a simple and conservative comparision of the LHS).
+
+2. It creates an auxillary inductive unary predicate with these rules (LHS only).
+
+3. It replaces the `ElsePr` with the negation of that rule.
+
+*)
+
+open Util
+open Source
+open Il.Ast
+
+(* Errors *)
+
+let error at msg = Source.error at "else removal" msg
+
+let unary_mixfix : mixop = [[Atom ""]; [Atom ""]]
+
+let is_else prem = prem.it = ElsePr
+
+let replace_else aux_name lhs prem = match prem.it with
+  | ElsePr -> NegPr (RulePr (aux_name, unary_mixfix, lhs) $ prem.at) $ prem.at
+  | _ -> prem
+
+let unarize rule = match rule.it with 
+    | RuleD (rid, binds, _mixop, exp, prems) ->
+      let lhs = match exp.it with
+        | TupE [lhs; _] -> lhs
+        | _ -> error exp.at "expected manifest pair"
+      in
+      { rule with it = RuleD (rid, binds, unary_mixfix, lhs, prems) }
+
+let not_apart lhs rule = match rule.it with
+    | RuleD (_, _, _, lhs2, _) -> not (Il.Apart.apart lhs lhs2)
+
+let rec go 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
+    | RuleD (rid, binds, rmixop, exp, prems) ->
+      if List.exists is_else prems
+      then
+        let lhs = match exp.it with
+          | TupE [lhs; _] -> lhs
+          | _ -> error exp.at "expected manifest pair"
+        in
+        let aux_name = id.it ^ "_before_" ^ rid.it $ rid.at in
+        let applicable_prev_rules = prev_rules
+              |> List.map unarize
+              |> List.filter (not_apart lhs)
+              |> List.rev in
+        [ RelD (aux_name, unary_mixfix, typ1, List.rev applicable_prev_rules) $ r.at ] @
+        let prems' = List.map (replace_else aux_name lhs) prems in
+        let rule' = { r with it = RuleD (rid, binds, rmixop, exp, prems') } in
+        go at id mixop typ typ1 (rule' :: prev_rules) rules
+      else
+        go at id mixop typ typ1 (r :: prev_rules) rules
+
+let rec t_def (def : def) : def list = match def.it with
+  | RecD defs -> [ { def with it = RecD (List.concat_map t_def defs) } ]
+  | RelD (id, mixop, typ, rules) -> begin match typ.it with
+    | TupT [typ1; _typ2] ->
+      go def.at id mixop typ typ1 [] rules
+    | _ -> [def]
+    end
+  | _ -> [ def ]
+
+let transform (defs : script) =
+  List.concat_map t_def defs
+

spectec/src/middlend/else.mli

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

spectec/src/middlend/sideconditions.ml

@@ -16,7 +16,7 @@ open Il.Ast
 
 (* Errors *)
 
-let _error at msg = Source.error at "sideconditions" msg
+let error at msg = Source.error at "sideconditions" msg
 
 module Env = Map.Make(String)
 
@@ -99,6 +99,10 @@ let rec t_prem env prem = match prem.it with
   | IterPr (prem, iterexp)
   -> iter_side_conditions env iterexp @
      List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_prem env prem) @ t_iterexp env iterexp
+  | NegPr prem'
+  -> match t_prem env prem' with
+    | [] -> []
+    | _ -> error prem.at "side condition in negated premise"
 
 let t_prems env = List.concat_map (t_prem env)
 

spectec/src/middlend/sub.ml

@@ -137,6 +137,7 @@ let rec t_prem' env = function
   | IfPr e -> IfPr (t_exp env e)
   | ElsePr -> ElsePr
   | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+  | NegPr prem -> NegPr (t_prem env prem)
 
 and t_prem env x = { x with it = t_prem' env x.it }
 

spectec/src/middlend/totalize.ml

@@ -96,6 +96,7 @@ let rec t_prem' env = function
   | IfPr e -> IfPr (t_exp env e)
   | ElsePr -> ElsePr
   | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+  | NegPr prem -> NegPr (t_prem env prem)
 
 and t_prem env x = { x with it = t_prem' env x.it }
 

spectec/src/middlend/unthe.ml

@@ -181,6 +181,7 @@ and t_prem' n prem : eqns * premise' =
     let eqns2, iterexp'' = t_iterexp n iterexp' in
     let iterexp''' = update_iterexp_vars (Il.Free.free_prem prem') iterexp'' in
     eqns1' @ eqns2, IterPr (prem', iterexp''')
+  | NegPr p -> error p.at "Cannot extract side-conditions from negated premises"
 
 let t_prems n k  = t_list t_prem n k (fun x -> x)