Commit 3f464a21 authored by Andrei Paskevich's avatar Andrei Paskevich

cache the lex-order of arguments for termination in ls_defn

parent bf437866
......@@ -32,7 +32,7 @@ type data_decl = tysymbol * constructor list
(** Logic declaration *)
type ls_defn = lsymbol * term
type ls_defn = lsymbol * term * int list
type logic_decl = lsymbol * ls_defn
......@@ -62,9 +62,9 @@ let make_ls_defn ls vl t =
List.iter2 check_vl ls.ls_args vl;
t_ty_check t ls.ls_value;
(* return the definition *)
ls, (ls, fd)
ls, (ls, fd, [])
let open_ls_defn (_,f) =
let open_ls_defn (_,f,_) =
let vl,_,f = match f.t_node with
| Tquant (Tforall,b) -> t_open_quant b
| _ -> [],[],f in
......@@ -74,7 +74,7 @@ let open_ls_defn (_,f) =
| _ -> assert false
let open_ls_defn_cb ld =
let ls,_ = ld in
let ls,_,_ = ld in
let vl,t = open_ls_defn ld in
let close ls' vl' t' =
if t_equal t t' && list_all2 vs_equal vl vl' && ls_equal ls ls'
......@@ -82,7 +82,9 @@ let open_ls_defn_cb ld =
in
vl,t,close
let ls_defn_axiom (_,f) = f
let ls_defn_decrease (_,_,l) = l
let ls_defn_axiom (_,f,_) = f
let ls_defn_of_axiom f =
let _,_,f = match f.t_node with
......@@ -258,7 +260,8 @@ let check_termination ldl =
let cl = build_call_list cgr ls in
check_call_list ls cl
in
Mls.mapi check syms
let res = Mls.mapi check syms in
List.map (fun (ls,(_,f,_)) -> (ls,(ls,f,Mls.find ls res))) ldl
(** Inductive predicate declaration *)
......@@ -323,7 +326,7 @@ module Hsdecl = Hashcons.Make (struct
let eq_td (ts1,td1) (ts2,td2) =
ts_equal ts1 ts2 && list_all2 cs_equal td1 td2
let eq_ld (ls1,(_,f1)) (ls2,(_,f2)) =
let eq_ld (ls1,(_,f1,_)) (ls2,(_,f2,_)) =
ls_equal ls1 ls2 && t_equal f1 f2
let eq_iax (pr1,fr1) (pr2,fr2) =
......@@ -347,7 +350,7 @@ module Hsdecl = Hashcons.Make (struct
let hs_td (ts,td) = Hashcons.combine_list cs_hash (ts_hash ts) td
let hs_ld (ls,(_,f)) = Hashcons.combine (ls_hash ls) (t_hash f)
let hs_ld (ls,(_,f,_)) = Hashcons.combine (ls_hash ls) (t_hash f)
let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (t_hash f)
......@@ -472,14 +475,14 @@ let create_param_decl ls =
let create_logic_decl ldl =
if ldl = [] then raise EmptyDecl;
let check_decl (syms,news) (ls,((s,_) as ld)) =
let check_decl (syms,news) (ls,((s,_,_) as ld)) =
if not (ls_equal s ls) then raise (BadLogicDecl (ls, s));
let _, e = open_ls_defn ld in
let syms = List.fold_left syms_ty syms ls.ls_args in
syms_term syms e, news_id news ls.ls_name
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
ignore (check_termination ldl);
let ldl = check_termination ldl in
mk_decl (Dlogic ldl) syms news
exception InvalidIndDecl of lsymbol * prsymbol
......
......@@ -52,12 +52,14 @@ val ls_defn_of_axiom : term -> logic_decl option
this to recursive definitions: it may successfully build a logic_decl,
which will fail later because of non-assured termination *)
val check_termination : logic_decl list -> (int list) Mls.t
(** [check_termination ldl] returns a mapping of every logical
symbol defined in [ldl] to a list of its argument positions
val ls_defn_decrease : ls_defn -> int list
(** [ls_defn_decrease ld] returns a list of argument positions
(numbered from 0) that ensures a lexicographical structural
descent for every recursive call. Triggers are ignored.
@raise NoTerminationProof [ls] when no such list is found for [ls] *)
NOTE: This is only meaningful if the [ls_defn] comes
from a declaration; on the result of [make_ls_defn],
[ls_defn_decrease] will always return an empty list. *)
(** {2 Inductive predicate declaration} *)
......
......@@ -624,10 +624,10 @@ let print_logic_decl info fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl info fmt d; forget_tvs ())
let print_recursive_decl info tm fmt (ls,ld) =
let print_recursive_decl info fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let il = try Mls.find ls tm with Not_found -> assert false in
let i = match il with [i] -> i | _ -> assert false in
let i = match Decl.ls_defn_decrease ld with
| [i] -> i | _ -> assert false in
let vl,e = open_ls_defn ld in
fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
print_ls ls
......@@ -639,13 +639,12 @@ let print_recursive_decl info tm fmt (ls,ld) =
List.iter forget_var vl
let print_recursive_decl info fmt dl =
let tm = check_termination dl in
fprintf fmt "(* Why3 assumption *)@\nSet Implicit Arguments.@\n";
print_list_delim
~start:(fun fmt () -> fprintf fmt "@[<hov 2>Fixpoint ")
~stop:(fun fmt () -> fprintf fmt ".@\n")
~sep:(fun fmt () -> fprintf fmt "@\n@[<hov 2>with ")
(fun fmt d -> print_recursive_decl info tm fmt d; forget_tvs ())
(fun fmt d -> print_recursive_decl info fmt d; forget_tvs ())
fmt dl;
fprintf fmt "Unset Implicit Arguments.@\n@\n"
......
......@@ -688,10 +688,10 @@ let print_logic_decl ~old info fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
(print_logic_decl ~old info fmt d; forget_tvs ())
let print_recursive_decl info tm fmt (ls,ld) =
let print_recursive_decl info fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let il = try Mls.find ls tm with Not_found -> assert false in
let i = match il with [i] -> i | _ -> assert false in
let i = match Decl.ls_defn_decrease ld with
| [i] -> i | _ -> assert false in
let vl,e = open_ls_defn ld in
fprintf fmt "@[<hov 2>%a%a(%a): RECURSIVE %a =@ %a@\n"
print_ls ls print_params all_ty_params
......@@ -703,15 +703,14 @@ let print_recursive_decl info tm fmt (ls,ld) =
List.iter forget_var vl
let print_recursive_decl info fmt dl =
let tm = check_termination dl in
let d, dl = match dl with
| [d] -> d, []
| d :: dl -> d, dl (* PVS does not support mutual recursion *)
| [] -> assert false
in
fprintf fmt "@[<hov 2>";
print_recursive_decl info tm fmt d; forget_tvs ();
List.iter (print_recursive_decl info tm fmt) dl;
print_recursive_decl info fmt d; forget_tvs ();
List.iter (print_recursive_decl info fmt) dl;
fprintf fmt "@]@\n"
let print_ind info fmt (pr,f) =
......
......@@ -89,12 +89,10 @@ let elim_recursion d = match d.d_node with
| Dlogic l when List.length l > 1 -> elim_decl true true l
| _ -> [d]
let is_struct dl =
try
Mls.for_all (fun _ il -> List.length il = 1) (check_termination dl)
with NoTerminationProof _ ->
false
let is_struct dl = (* FIXME? Shouldn't 0 be allowed too? *)
List.for_all (fun (_,ld) -> List.length (ls_defn_decrease ld) = 1) dl
(* FIXME? We can have non-recursive functions in a group *)
let elim_non_struct_recursion d = match d.d_node with
| Dlogic ((s,_) :: _ as dl)
when Sid.mem s.ls_name d.d_syms && not (is_struct dl) ->
......
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