From 84abc0c1125903ccc0a48de2cf414398c36c9733 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 9 Apr 2023 22:29:41 +0200 Subject: [PATCH 1/3] Add negated premises --- spectec/src/frontend/multiplicity.ml | 1 + spectec/src/il/ast.ml | 1 + spectec/src/il/free.ml | 1 + spectec/src/il/print.ml | 1 + spectec/src/il/validation.ml | 2 ++ spectec/src/middlend/totalize.ml | 1 + 6 files changed, 7 insertions(+) diff --git a/spectec/src/frontend/multiplicity.ml b/spectec/src/frontend/multiplicity.ml index e9e716b0ef..a8b209856e 100644 --- a/spectec/src/frontend/multiplicity.ml +++ b/spectec/src/frontend/multiplicity.ml @@ -288,6 +288,7 @@ 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') $ prem.at, occur' + | NegPr prem' -> annot_prem env prem' let annot_exp env e = diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index 2730a0cd9f..4978cd6869 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -153,6 +153,7 @@ and premise' = | IfPr of exp (* side condition *) | ElsePr (* otherwise *) | IterPr of premise * iterexp (* iteration *) + | NegPr of premise (* negation of a premise *) and hint = {hintid : id; hintexp : string list} (* hint *) diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index 7d2128735e..bb3e6436a8 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -118,6 +118,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 diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index a76d8ca95e..83d6717b03 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -199,6 +199,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 string_of_rule rule = diff --git a/spectec/src/il/validation.ml b/spectec/src/il/validation.ml index fcdd4c52c6..2e9b1398ad 100644 --- a/spectec/src/il/validation.ml +++ b/spectec/src/il/validation.ml @@ -494,6 +494,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 = diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml index f291c0173f..31b1940815 100644 --- a/spectec/src/middlend/totalize.ml +++ b/spectec/src/middlend/totalize.ml @@ -95,6 +95,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 } From ca57e9e8592e1e5dfd38fdfa502719359919f5a2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 24 Apr 2023 09:49:23 +0200 Subject: [PATCH 2/3] Update sideconditions --- spectec/src/middlend/sideconditions.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml index 81b7ec1273..541c0ebd4f 100644 --- a/spectec/src/middlend/sideconditions.ml +++ b/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 let is_null e = CmpE (EqOp, e, OptE None $ no_region) $ no_region let iffE e1 e2 = IfPr (BinE (EquivOp, e1, e2) $ no_region) $ no_region @@ -94,6 +94,11 @@ let rec t_prem prem = match prem.it with | IterPr (prem, iterexp) -> iter_side_conditions iterexp @ List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_prem prem) @ t_iterexp iterexp + | NegPr prem' + -> match t_prem prem' with + | [] -> [] + | _ -> error prem.at "side condition in negated premise" + let t_prems = List.concat_map t_prem From a21e2164f8911816a532527dfdb942e970b284cd Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 17 Oct 2023 15:56:54 +0200 Subject: [PATCH 3/3] Update more middleend passes --- spectec/src/middlend/sub.ml | 1 + spectec/src/middlend/unthe.ml | 3 +++ spectec/src/middlend/wild.ml | 3 +++ 3 files changed, 7 insertions(+) diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index bc21cbd5cf..f643ebaa4c 100644 --- a/spectec/src/middlend/sub.ml +++ b/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 } diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml index 3ed9ef98b3..d6324ae690 100644 --- a/spectec/src/middlend/unthe.ml +++ b/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) diff --git a/spectec/src/middlend/wild.ml b/spectec/src/middlend/wild.ml index f2b395555f..434c055402 100644 --- a/spectec/src/middlend/wild.ml +++ b/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)