Commit c4820cae authored by Andrei Paskevich's avatar Andrei Paskevich

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.
parent 96ace312
...@@ -964,7 +964,12 @@ let let_rec fdl = ...@@ -964,7 +964,12 @@ let let_rec fdl =
"All functions in a recursive definition must use the same \ "All functions in a recursive definition must use the same \
well-founded order for the first component of the variant" in well-founded order for the first component of the variant" in
List.iter check_variant (List.tl fdl); 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 eff_diverge eff_empty else eff_empty in
(* create the first substitution *) (* create the first substitution *)
let update sm (s,({c_cty = c} as d),varl,_) = let update sm (s,({c_cty = c} as d),varl,_) =
......
...@@ -435,9 +435,16 @@ let create_let_decl ld = ...@@ -435,9 +435,16 @@ let create_let_decl ld =
List.fold_right add_rd rdl ([],[],[]) List.fold_right add_rd rdl ([],[],[])
| LDsym (s,c) -> | LDsym (s,c) ->
add_ls Mrs.empty s c ([],[],[]) in 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 defn = if defn = [] then [] else
let dl = List.map (fun (s,vl,t) -> make_ls_defn s vl t) defn in 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 abst = List.map (fun (s,_) -> create_param_decl s) dl in
let mk_ax ({ls_name = id} as s, vl, t) = let mk_ax ({ls_name = id} as s, vl, t) =
let nm = id.id_string ^ "_def" in let nm = id.id_string ^ "_def" in
......
...@@ -16,7 +16,7 @@ theory Length ...@@ -16,7 +16,7 @@ theory Length
use import int.Int use import int.Int
use import List use import List
let rec function length (l: list 'a) : int variant {l} = let rec function length (l: list 'a) : int =
match l with match l with
| Nil -> 0 | Nil -> 0
| Cons _ r -> 1 + length r | Cons _ r -> 1 + length r
...@@ -65,7 +65,7 @@ theory Nth ...@@ -65,7 +65,7 @@ theory Nth
use import option.Option use import option.Option
use import int.Int 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 match l with
| Nil -> None | Nil -> None
| Cons x r -> if n = 0 then Some x else nth (n - 1) r | Cons x r -> if n = 0 then Some x else nth (n - 1) r
...@@ -163,7 +163,7 @@ theory Append ...@@ -163,7 +163,7 @@ theory Append
use import List 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 match l1 with
| Nil -> l2 | Nil -> l2
| Cons x1 r1 -> Cons x1 (r1 ++ l2) | Cons x1 r1 -> Cons x1 (r1 ++ l2)
...@@ -218,7 +218,7 @@ theory Reverse ...@@ -218,7 +218,7 @@ theory Reverse
use import List use import List
use import Append 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 match l with
| Nil -> Nil | Nil -> Nil
| Cons x r -> reverse r ++ Cons x Nil | Cons x r -> reverse r ++ Cons x Nil
...@@ -258,7 +258,7 @@ theory RevAppend ...@@ -258,7 +258,7 @@ theory RevAppend
use import List 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 match s with
| Cons x r -> rev_append r (Cons x t) | Cons x r -> rev_append r (Cons x t)
| Nil -> t | Nil -> t
...@@ -295,7 +295,6 @@ theory Combine ...@@ -295,7 +295,6 @@ theory Combine
use import List use import List
let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b) let rec function combine (x: list 'a) (y: list 'b) : list ('a, 'b)
variant {x}
= match x, y with = match x, y with
| Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y) | Cons x0 x, Cons y0 y -> Cons (x0, y0) (combine x y)
| _ -> Nil | _ -> Nil
...@@ -496,7 +495,7 @@ theory Prefix ...@@ -496,7 +495,7 @@ theory Prefix
use import List use import List
use import int.Int 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 if n <= 0 then Nil else
match l with match l with
| Nil -> Nil | Nil -> Nil
...@@ -510,7 +509,7 @@ theory Sum ...@@ -510,7 +509,7 @@ theory Sum
use import List use import List
use import int.Int 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 match l with
| Nil -> 0 | Nil -> 0
| Cons x r -> x + sum r | Cons x r -> x + sum r
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment