From c4820caec713995bc150a763cd150e36bcde9ede Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Sat, 19 Sep 2015 15:34:37 +0200
Subject: [PATCH] Mlw: do not require "variant" for toplevel let-functions

If we have a top-level total let-function definition and
no variants are supplied, then we expect the definition
to be terminating with respect to Decl.check_termination.
---
 src/mlw/expr.ml   |  7 ++++++-
 src/mlw/pdecl.ml  |  9 ++++++++-
 theories/list.why | 15 +++++++--------
 3 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/src/mlw/expr.ml b/src/mlw/expr.ml
index f10ee2039..9e320044f 100644
--- a/src/mlw/expr.ml
+++ b/src/mlw/expr.ml
@@ -964,7 +964,12 @@ let let_rec fdl =
         "All functions in a recursive definition must use the same \
         well-founded order for the first component of the variant" in
   List.iter check_variant (List.tl fdl);
-  let start_eff = if varl1 = [] then
+  (* if we have a top-level total let-function definition and
+     no variants are supplied, then we expect the definition
+     to be terminating with respect to Decl.check_termination *)
+  let impure (_,d,_,k) =
+    (k <> RKfunc && k <> RKpred) || d.c_cty.cty_pre <> [] in
+  let start_eff = if varl1 = [] && List.exists impure fdl then
     eff_diverge eff_empty else eff_empty in
   (* create the first substitution *)
   let update sm (s,({c_cty = c} as d),varl,_) =
diff --git a/src/mlw/pdecl.ml b/src/mlw/pdecl.ml
index 67908f4ec..f795cfb12 100644
--- a/src/mlw/pdecl.ml
+++ b/src/mlw/pdecl.ml
@@ -435,9 +435,16 @@ let create_let_decl ld =
         List.fold_right add_rd rdl ([],[],[])
     | LDsym (s,c) ->
         add_ls Mrs.empty s c ([],[],[]) in
+  let fail_trusted_rec ls =
+    Loc.error ?loc:ls.ls_name.id_loc (Decl.NoTerminationProof ls) in
+  let is_trusted_rec = match ld with
+    | LDrec ({rec_sym = {rs_logic = RLls ls; rs_cty = c}; rec_varl = []}::_)
+      when not c.cty_effect.eff_oneway -> abst = [] || fail_trusted_rec ls
+    | _ -> false in
   let defn = if defn = [] then [] else
     let dl = List.map (fun (s,vl,t) -> make_ls_defn s vl t) defn in
-    try [create_logic_decl dl] with Decl.NoTerminationProof _ ->
+    try [create_logic_decl dl] with Decl.NoTerminationProof ls ->
+    if is_trusted_rec then fail_trusted_rec ls;
     let abst = List.map (fun (s,_) -> create_param_decl s) dl in
     let mk_ax ({ls_name = id} as s, vl, t) =
       let nm = id.id_string ^ "_def" in
diff --git a/theories/list.why b/theories/list.why
index 8df7107d7..a79c43d95 100644
--- a/theories/list.why
+++ b/theories/list.why
@@ -16,7 +16,7 @@ theory Length
   use import int.Int
   use import List
 
-  let rec function length (l: list 'a) : int variant {l} =
+  let rec function length (l: list 'a) : int =
     match l with
     | Nil      -> 0
     | Cons _ r -> 1 + length r
@@ -65,7 +65,7 @@ theory Nth
   use import option.Option
   use import int.Int
 
-  let rec function nth (n: int) (l: list 'a) : option 'a variant {l} =
+  let rec function nth (n: int) (l: list 'a) : option 'a =
     match l with
     | Nil      -> None
     | Cons x r -> if n = 0 then Some x else nth (n - 1) r
@@ -163,7 +163,7 @@ theory Append
 
   use import List
 
-  let rec function (++) (l1 l2: list 'a) : list 'a variant {l1} =
+  let rec function (++) (l1 l2: list 'a) : list 'a =
     match l1 with
     | Nil -> l2
     | Cons x1 r1 -> Cons x1 (r1 ++ l2)
@@ -218,7 +218,7 @@ theory Reverse
   use import List
   use import Append
 
-  let rec function reverse (l: list 'a) : list 'a variant {l} =
+  let rec function reverse (l: list 'a) : list 'a =
     match l with
     | Nil      -> Nil
     | Cons x r -> reverse r ++ Cons x Nil
@@ -258,7 +258,7 @@ theory RevAppend
 
   use import List
 
-  let rec function rev_append (s t: list 'a) : list 'a variant {s} =
+  let rec function rev_append (s t: list 'a) : list 'a =
     match s with
     | Cons x r -> rev_append r (Cons x t)
     | Nil -> t
@@ -295,7 +295,6 @@ theory Combine
   use import List
 
   let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b)
-    variant {x}
   = match x, y with
     | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y)
     | _ -> Nil
@@ -496,7 +495,7 @@ theory Prefix
   use import List
   use import int.Int
 
-  let rec function prefix (n: int) (l: list 'a) : list 'a variant {l} =
+  let rec function prefix (n: int) (l: list 'a) : list 'a =
     if n <= 0 then Nil else
     match l with
     | Nil -> Nil
@@ -510,7 +509,7 @@ theory Sum
   use import List
   use import int.Int
 
-  let rec function sum (l: list int) : int variant {l} =
+  let rec function sum (l: list int) : int =
     match l with
     | Nil -> 0
     | Cons x r -> x + sum r
-- 
GitLab