Add negated premises

spectec/src/frontend/multiplicity.ml

@@ -363,6 +363,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/ast.ml

@@ -167,6 +167,7 @@ and premise' =
   | LetPr of exp * exp                                (* assignment *)
   | ElsePr                                            (* otherwise *)
   | IterPr of premise * iterexp                       (* iteration *)
+  | NegPr of premise                                  (* negation of a premise *)
 
 and hintdef = hintdef' phrase
 and hintdef' =

spectec/src/il/free.ml

@@ -124,6 +124,7 @@ and free_prem prem =
   | LetPr (e1, e2) -> union (free_exp e1) (free_exp e2)
   | ElsePr -> empty
   | IterPr (prem', iter) -> union (free_prem prem') (free_iterexp iter)
+  | NegPr prem' -> free_prem prem'
 
 
 (* Definitions *)

spectec/src/il/print.ml

@@ -209,6 +209,7 @@ and 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'
 
 
 (* Definitions *)

spectec/src/il/validation.ml

@@ -531,6 +531,8 @@ and valid_prem env prem =
   | IterPr (prem', iter) ->
     let env' = valid_iterexp env iter in
     valid_prem env' prem'
+  | NegPr prem' ->
+    valid_prem env prem'
 
 
 (* Definitions *)

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)
 
@@ -128,6 +128,10 @@ let rec t_prem env prem = match prem.it with
      t_iterexp env iterexp @
      let env' = env_under_iter env iterexp in
      List.map (fun pr -> IterPr (pr, iterexp) $ prem.at) (t_prem env' prem)
+  | 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

@@ -138,6 +138,7 @@ let rec t_prem' env = function
   | LetPr (e1, e2) -> LetPr (t_exp env e1, t_exp env e2)
   | 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

@@ -97,6 +97,7 @@ let rec t_prem' env = function
   | LetPr (e1, e2) -> LetPr (t_exp env e1, t_exp env e2)
   | 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

@@ -182,6 +182,9 @@ 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 prem ->
+    let eqns, prem' = t_prem n prem in
+    eqns, NegPr prem'
 
 let t_prems n k  = t_list t_prem n k (fun x -> x)
 

spectec/src/middlend/wild.ml

@@ -205,6 +205,9 @@ and t_prem' env prem : binds * premise' =
     let iterexp', binds1' = under_iterexp iterexp binds1 in
     let binds2, iterexp'' = t_iterexp env iterexp' in
     binds1' @ binds2, IterPr (prem', iterexp'')
+  | NegPr prem ->
+    let binds, prem' = t_prem env prem in
+    binds, NegPr prem'
 
 let t_prems env k  = t_list t_prem env k (fun x -> x)