From a9bb74b28e93387f985a59ebaad85a489482b36e Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Tue, 22 May 2012 15:51:50 +0200
Subject: [PATCH] coinductive predicates
---
CHANGES | 1 +
doc/theory.bnf | 1 +
share/emacs/why.el | 2 +-
share/lang/why.lang | 3 ++-
share/vim/why3.vim | 2 +-
src/coq-tactic/why3tac.ml | 3 ++-
src/core/decl.ml | 30 +++++++++++++++------------
src/core/decl.mli | 8 +++++--
src/core/pretty.ml | 14 ++++++++-----
src/core/pretty.mli | 2 +-
src/core/task.ml | 2 +-
src/core/task.mli | 2 +-
src/core/theory.ml | 8 +++----
src/core/theory.mli | 2 +-
src/parser/lexer.mll | 1 +
src/parser/parser.mly | 11 +++++++---
src/parser/ptree.ml | 2 +-
src/parser/typing.ml | 10 ++++-----
src/printer/alt_ergo.ml | 2 +-
src/printer/coq.ml | 17 ++++++++-------
src/printer/pvs.ml | 5 ++++-
src/printer/why3printer.ml | 14 ++++++++-----
src/programs/pgm_ocaml.ml | 2 +-
src/programs/pgm_typing.ml | 2 +-
src/session/termcode.ml | 2 +-
src/transform/eliminate_definition.ml | 4 ++--
src/transform/eliminate_inductive.ml | 2 +-
src/transform/encoding_explicit.ml | 6 +++---
src/transform/encoding_guard.ml | 6 +++---
src/transform/libencoding.ml | 4 ++--
src/whyml/mlw_module.ml | 3 ++-
src/whyml/mlw_module.mli | 2 +-
32 files changed, 103 insertions(+), 72 deletions(-)
diff --git a/CHANGES b/CHANGES
index 0eb830acea..fcc57cb4ee 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,7 @@
* marks an incompatible change
+ o co-inductive predicates
o new option -e for "why3session latex" allows to specify when to
split tables in parts
diff --git a/doc/theory.bnf b/doc/theory.bnf
index 9c1cdc538e..b316f316c9 100644
--- a/doc/theory.bnf
+++ b/doc/theory.bnf
@@ -6,6 +6,7 @@
| "function" function-decl ("with" logic-decl)* ;
| "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ;
+ | "coinductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
| "goal" ident ":" formula ;
diff --git a/share/emacs/why.el b/share/emacs/why.el
index b7b3235f97..a7d847a3d6 100644
--- a/share/emacs/why.el
+++ b/share/emacs/why.el
@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
- `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "reads" "writes" "raises")) . font-lock-builtin-face)
+ `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
diff --git a/share/lang/why.lang b/share/lang/why.lang
index 69bbcadacd..241fadb46c 100644
--- a/share/lang/why.lang
+++ b/share/lang/why.lang
@@ -147,10 +147,11 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>abstract</keyword>
<keyword>axiom</keyword>
<keyword>clone</keyword>
+ <keyword>coinductive</keyword>
+ <keyword>constant</keyword>
<keyword>end</keyword>
<keyword>exception</keyword>
<keyword>export</keyword>
- <keyword>constant</keyword>
<keyword>function</keyword>
<keyword>goal</keyword>
<keyword>ghost</keyword>
diff --git a/share/vim/why3.vim b/share/vim/why3.vim
index e556d9fea1..c3617130af 100644
--- a/share/vim/why3.vim
+++ b/share/vim/why3.vim
@@ -87,7 +87,7 @@ syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\|prop\)
syn keyword whyKeyword as constant
syn keyword whyKeyword else epsilon exists
syn keyword whyKeyword false forall function
-syn keyword whyKeyword if in inductive
+syn keyword whyKeyword if in inductive coinductive
syn keyword whyKeyword let meta
syn keyword whyKeyword not predicate
syn keyword whyKeyword then true type with
diff --git a/src/coq-tactic/why3tac.ml b/src/coq-tactic/why3tac.ml
index d792eaedfd..0178ccdad5 100644
--- a/src/coq-tactic/why3tac.ml
+++ b/src/coq-tactic/why3tac.ml
@@ -728,7 +728,8 @@ and decompose_inductive dep env i =
if cl = [] then Decl.create_param_decl ls :: pl, dl else pl, d :: dl
in
let pl, dl = List.fold_right add dl ([], []) in
- pl, if dl = [] then None else Some (Decl.create_ind_decl dl)
+ let s = if mib.mind_finite then Decl.Ind else Decl.Coind in
+ pl, if dl = [] then None else Some (Decl.create_ind_decl s dl)
(* translation of a Coq term
assumption: t:T:Set *)
diff --git a/src/core/decl.ml b/src/core/decl.ml
index 38082b15c2..479ae2a4fb 100644
--- a/src/core/decl.ml
+++ b/src/core/decl.ml
@@ -288,6 +288,10 @@ let create_prsymbol n = { pr_name = id_register n }
type ind_decl = lsymbol * (prsymbol * term) list
+type ind_sign = Ind | Coind
+
+type ind_list = ind_sign * ind_decl list
+
(** Proposition declaration *)
type prop_kind =
@@ -312,7 +316,7 @@ and decl_node =
| Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive functions and predicates *)
- | Dind of ind_decl list (* inductive predicates *)
+ | Dind of ind_list (* (co)inductive predicates *)
| Dprop of prop_decl (* axiom / lemma / goal *)
(** Declarations *)
@@ -341,7 +345,7 @@ module Hsdecl = Hashcons.Make (struct
| Ddata l1, Ddata l2 -> list_all2 eq_td l1 l2
| Dparam s1, Dparam s2 -> ls_equal s1 s2
| Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2
- | Dind l1, Dind l2 -> list_all2 eq_ind l1 l2
+ | Dind (s1,l1), Dind (s2,l2) -> s1 = s2 && list_all2 eq_ind l1 l2
| Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2
| _,_ -> false
@@ -365,7 +369,7 @@ module Hsdecl = Hashcons.Make (struct
| Ddata l -> Hashcons.combine_list hs_td 3 l
| Dparam s -> ls_hash s
| Dlogic l -> Hashcons.combine_list hs_ld 5 l
- | Dind l -> Hashcons.combine_list hs_ind 7 l
+ | Dind (_,l) -> Hashcons.combine_list hs_ind 7 l
| Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
let tag n d = { d with d_tag = Hashweak.create_tag n }
@@ -506,7 +510,7 @@ let rec f_pos_ps sps pol f = match f.t_node, pol with
f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
| _ -> TermTF.t_all (t_pos_ps sps) (f_pos_ps sps pol) f
-let create_ind_decl idl =
+let create_ind_decl s idl =
if idl = [] then raise EmptyDecl;
let add acc (ps,_) = Sls.add ps acc in
let sps = List.fold_left add Sls.empty idl in
@@ -537,7 +541,7 @@ let create_ind_decl idl =
List.fold_left (check_ax ps) (syms,news) al
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
- mk_decl (Dind idl) syms news
+ mk_decl (Dind (s, idl)) syms news
let create_prop_decl k p f =
let syms = syms_term Sid.empty f in
@@ -554,10 +558,10 @@ let decl_map fn d = match d.d_node with
close ls vl (fn e)
in
create_logic_decl (List.map fn l)
- | Dind l ->
+ | Dind (s, l) ->
let fn (pr,f) = pr, fn f in
let fn (ps,l) = ps, List.map fn l in
- create_ind_decl (List.map fn l)
+ create_ind_decl s (List.map fn l)
| Dprop (k,pr,f) ->
create_prop_decl k pr (fn f)
@@ -569,7 +573,7 @@ let decl_fold fn acc d = match d.d_node with
fn acc e
in
List.fold_left fn acc l
- | Dind l ->
+ | Dind (_, l) ->
let fn acc (_,f) = fn acc f in
let fn acc (_,l) = List.fold_left fn acc l in
List.fold_left fn acc l
@@ -591,9 +595,9 @@ let decl_map_fold fn acc d = match d.d_node with
in
let acc,l = Util.map_fold_left fn acc l in
acc, create_logic_decl l
- | Dind l ->
+ | Dind (s, l) ->
let acc, l = list_rpair_map_fold (list_rpair_map_fold fn) acc l in
- acc, create_ind_decl l
+ acc, create_ind_decl s l
| Dprop (k,pr,f) ->
let acc, f = fn acc f in
acc, create_prop_decl k pr f
@@ -642,7 +646,7 @@ let find_constructors kn ts =
let find_inductive_cases kn ps =
match (Mid.find ps.ls_name kn).d_node with
- | Dind dl -> List.assq ps dl
+ | Dind (_, dl) -> List.assq ps dl
| Dlogic _ -> []
| Dtype _ -> []
| _ -> assert false
@@ -655,7 +659,7 @@ let find_logic_definition kn ls =
let find_prop kn pr =
match (Mid.find pr.pr_name kn).d_node with
- | Dind dl ->
+ | Dind (_, dl) ->
let test (_,l) = List.mem_assq pr l in
List.assq pr (snd (List.find test dl))
| Dprop (_,_,f) -> f
@@ -663,7 +667,7 @@ let find_prop kn pr =
let find_prop_decl kn pr =
match (Mid.find pr.pr_name kn).d_node with
- | Dind dl ->
+ | Dind (_, dl) ->
let test (_,l) = List.mem_assq pr l in
Paxiom, List.assq pr (snd (List.find test dl))
| Dprop (k,_,f) -> k,f
diff --git a/src/core/decl.mli b/src/core/decl.mli
index 0edf679364..c413a79433 100644
--- a/src/core/decl.mli
+++ b/src/core/decl.mli
@@ -81,6 +81,10 @@ val pr_hash : prsymbol -> int
type ind_decl = lsymbol * (prsymbol * term) list
+type ind_sign = Ind | Coind
+
+type ind_list = ind_sign * ind_decl list
+
(* Proposition declaration *)
type prop_kind =
@@ -105,7 +109,7 @@ and decl_node =
| Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive functions and predicates *)
- | Dind of ind_decl list (* inductive predicates *)
+ | Dind of ind_list (* (co)inductive predicates *)
| Dprop of prop_decl (* axiom / lemma / goal *)
module Mdecl : Map.S with type key = decl
@@ -121,7 +125,7 @@ val create_ty_decl : tysymbol -> decl
val create_data_decl : data_decl list -> decl
val create_param_decl : lsymbol -> decl
val create_logic_decl : logic_decl list -> decl
-val create_ind_decl : ind_decl list -> decl
+val create_ind_decl : ind_sign -> ind_decl list -> decl
val create_prop_decl : prop_kind -> prsymbol -> term -> decl
(* exceptions *)
diff --git a/src/core/pretty.ml b/src/core/pretty.ml
index 6f262f364c..8a7aae4a67 100644
--- a/src/core/pretty.ml
+++ b/src/core/pretty.ml
@@ -358,9 +358,13 @@ let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
print_pr pr print_ident_labels pr.pr_name print_term f
-let print_ind_decl fst fmt (ps,bl) =
+let ind_sign = function
+ | Ind -> "inductive"
+ | Coind -> "coinductive"
+
+let print_ind_decl s fst fmt (ps,bl) =
fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]"
- (if fst then "inductive" else "with") print_ls ps
+ (if fst then ind_sign s else "with") print_ls ps
print_ident_labels ps.ls_name
(print_list nothing print_ty_arg) ps.ls_args
(print_list newline print_ind) bl;
@@ -390,15 +394,15 @@ let print_decl fmt d = match d.d_node with
| Ddata tl -> print_list_next newline print_data_decl fmt tl
| Dparam ls -> print_param_decl fmt ls
| Dlogic ll -> print_list_next newline print_logic_decl fmt ll
- | Dind il -> print_list_next newline print_ind_decl fmt il
+ | Dind (s, il) -> print_list_next newline (print_ind_decl s) fmt il
| Dprop p -> print_prop_decl fmt p
let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true
let print_next_logic_decl = print_logic_decl false
let print_logic_decl = print_logic_decl true
-let print_next_ind_decl = print_ind_decl false
-let print_ind_decl = print_ind_decl true
+let print_next_ind_decl = print_ind_decl Ind false
+let print_ind_decl fmt s = print_ind_decl s true fmt
let print_inst_ts fmt (ts1,ts2) =
fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
diff --git a/src/core/pretty.mli b/src/core/pretty.mli
index 410bfa20bc..4f9302209c 100644
--- a/src/core/pretty.mli
+++ b/src/core/pretty.mli
@@ -58,7 +58,7 @@ val print_ty_decl : formatter -> tysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
val print_param_decl : formatter -> lsymbol -> unit
val print_logic_decl : formatter -> logic_decl -> unit
-val print_ind_decl : formatter -> ind_decl -> unit
+val print_ind_decl : formatter -> ind_sign -> ind_decl -> unit
val print_next_data_decl : formatter -> data_decl -> unit
val print_next_logic_decl : formatter -> logic_decl -> unit
val print_next_ind_decl : formatter -> ind_decl -> unit
diff --git a/src/core/task.ml b/src/core/task.ml
index 05f548c1f3..cdd86a3be0 100644
--- a/src/core/task.ml
+++ b/src/core/task.ml
@@ -172,7 +172,7 @@ let add_ty_decl tk ts = add_decl tk (create_ty_decl ts)
let add_data_decl tk dl = add_decl tk (create_data_decl dl)
let add_param_decl tk ls = add_decl tk (create_param_decl ls)
let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
-let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
+let add_ind_decl tk s dl = add_decl tk (create_ind_decl s dl)
let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)
(* task constructors *)
diff --git a/src/core/task.mli b/src/core/task.mli
index 4a4af4d7c4..a8f5b951cb 100644
--- a/src/core/task.mli
+++ b/src/core/task.mli
@@ -80,7 +80,7 @@ val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task
val add_logic_decl : task -> logic_decl list -> task
-val add_ind_decl : task -> ind_decl list -> task
+val add_ind_decl : task -> ind_sign -> ind_decl list -> task
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
(** {2 utilities} *)
diff --git a/src/core/theory.ml b/src/core/theory.ml
index c10406ea99..8b8d131f31 100644
--- a/src/core/theory.ml
+++ b/src/core/theory.ml
@@ -380,7 +380,7 @@ let add_decl uc d =
| Ddata dl -> List.fold_left add_data uc dl
| Dparam ls -> add_symbol add_ls ls.ls_name ls uc
| Dlogic dl -> List.fold_left add_logic uc dl
- | Dind dl -> List.fold_left add_ind uc dl
+ | Dind (_, dl) -> List.fold_left add_ind uc dl
| Dprop p -> add_prop uc p
(** Declaration constructors + add_decl *)
@@ -389,7 +389,7 @@ let add_ty_decl uc ts = add_decl uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl uc (create_data_decl dl)
let add_param_decl uc ls = add_decl uc (create_param_decl ls)
let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
-let add_ind_decl uc dl = add_decl uc (create_ind_decl dl)
+let add_ind_decl uc s dl = add_decl uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
(** Use *)
@@ -566,7 +566,7 @@ let cl_logic cl inst ldl =
in
create_logic_decl (List.map add_logic ldl)
-let cl_ind cl inst idl =
+let cl_ind cl inst (s, idl) =
let add_case (pr,f) =
if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal
then raise (CannotInstantiate pr.pr_name)
@@ -577,7 +577,7 @@ let cl_ind cl inst idl =
then raise (CannotInstantiate ps.ls_name)
else cl_find_ls cl ps, List.map add_case la
in
- create_ind_decl (List.map add_ind idl)
+ create_ind_decl s (List.map add_ind idl)
let cl_prop cl inst (k,pr,f) =
let k' = match k with
diff --git a/src/core/theory.mli b/src/core/theory.mli
index e2e346aad1..e6f4d72a04 100644
--- a/src/core/theory.mli
+++ b/src/core/theory.mli
@@ -140,7 +140,7 @@ val add_ty_decl : theory_uc -> tysymbol -> theory_uc
val add_data_decl : theory_uc -> data_decl list -> theory_uc
val add_param_decl : theory_uc -> lsymbol -> theory_uc
val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
-val add_ind_decl : theory_uc -> ind_decl list -> theory_uc
+val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
(** Use *)
diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll
index 3eba9b366c..f47e42c462 100644
--- a/src/parser/lexer.mll
+++ b/src/parser/lexer.mll
@@ -45,6 +45,7 @@
"as", AS;
"axiom", AXIOM;
"clone", CLONE;
+ "coinductive", COINDUCTIVE;
"constant", CONSTANT;
"else", ELSE;
"end", END;
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index d81e102dd0..daf0b3c9d5 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -202,7 +202,7 @@ end
/* keywords */
-%token AS AXIOM CLONE CONSTANT
+%token AS AXIOM CLONE COINDUCTIVE CONSTANT
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
@@ -336,8 +336,8 @@ decl:
{ LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
{ LogicDecl $2 }
-| INDUCTIVE list1_inductive_decl
- { IndDecl $2 }
+| inductive list1_inductive_decl
+ { IndDecl ($1, $2) }
| AXIOM ident labels COLON lexpr
{ PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
| LEMMA ident labels COLON lexpr
@@ -348,6 +348,11 @@ decl:
{ Meta (floc (), $2, $3) }
;
+inductive:
+| INDUCTIVE { Decl.Ind }
+| COINDUCTIVE { Decl.Coind }
+;
+
/* Use and clone */
use_clone:
diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml
index 1c711e7d54..5b78080dc3 100644
--- a/src/parser/ptree.ml
+++ b/src/parser/ptree.ml
@@ -167,7 +167,7 @@ type use_clone = loc * use * clone_subst list option
type decl =
| TypeDecl of type_decl list
| LogicDecl of logic_decl list
- | IndDecl of ind_decl list
+ | IndDecl of Decl.ind_sign * ind_decl list
| PropDecl of loc * prop_kind * ident * lexpr
| Meta of loc * ident * metarg list
diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 8afd7bb55e..fb7c51ed5f 100644
--- a/src/parser/typing.ml
+++ b/src/parser/typing.ml
@@ -156,7 +156,7 @@ let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls = add_decl_with_tuples uc (create_param_decl ls)
let add_logic_decl uc dl = add_decl_with_tuples uc (create_logic_decl dl)
-let add_ind_decl uc dl = add_decl_with_tuples uc (create_ind_decl dl)
+let add_ind_decl uc s dl = add_decl_with_tuples uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
let rec dty uc env = function
@@ -1036,7 +1036,7 @@ let add_prop k loc s f th =
let loc_of_id id = of_option id.Ident.id_loc
-let add_inductives dl th =
+let add_inductives s dl th =
(* 1. create all symbols and make an environment with these symbols *)
let denv = create_denv () in
let psymbols = Hashtbl.create 17 in
@@ -1062,7 +1062,7 @@ let add_inductives dl th =
in
ps, List.map clause d.in_def
in
- try add_ind_decl th (List.map type_decl dl)
+ try add_ind_decl th s (List.map type_decl dl)
with
| ClashSymbol s ->
error ~loc:(Hashtbl.find propsyms s) (ClashSymbol s)
@@ -1115,8 +1115,8 @@ let add_decl th = function
add_types dl th
| LogicDecl dl ->
add_logics dl th
- | IndDecl dl ->
- add_inductives dl th
+ | IndDecl (s, dl) ->
+ add_inductives s dl th
| PropDecl (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th
| Meta (loc, id, al) ->
diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml
index 2a7eb5acc2..0ee1e53d62 100644
--- a/src/printer/alt_ergo.ml
+++ b/src/printer/alt_ergo.ml
@@ -296,7 +296,7 @@ let print_decl info fmt d = match d.d_node with
| Dlogic dl ->
print_list nothing (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
- "alt-ergo : inductive definition are not supported"
+ "alt-ergo: inductive definitions are not supported"
| Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
diff --git a/src/printer/coq.ml b/src/printer/coq.ml
index edbd621d5a..cf39cdd0be 100644
--- a/src/printer/coq.ml
+++ b/src/printer/coq.ml
@@ -648,18 +648,19 @@ let print_recursive_decl info fmt dl =
let print_ind info fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) f
-let print_ind_decl info fmt (ps,bl) =
+let print_ind_decl info s fmt (ps,bl) =
let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ps in
- fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Inductive %a%a : %a -> Prop :=@ @[<hov>%a@].@]@\n"
+ fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>%s %a%a : %a -> Prop :=@ @[<hov>%a@].@]@\n"
+ (match s with Ind -> "Inductive" | Coind -> "CoInductive")
print_ls ps print_implicit_params all_ty_params
(print_arrow_list (print_ty info)) ps.ls_args
(print_list newline (print_ind info)) bl;
print_implicits fmt ps ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n"
-let print_ind_decl info fmt d =
+let print_ind_decl info s fmt d =
if not (Mid.mem (fst d).ls_name info.info_syn) then
- (print_ind_decl info fmt d; forget_tvs ())
+ (print_ind_decl info s fmt d; forget_tvs ())
let print_prop_decl ~prev info fmt (k,pr,f) =
let params = t_ty_freevars Stv.empty f in
@@ -687,11 +688,11 @@ let print_decl ~old info fmt d =
| Ddata ((ts, _)::_) -> id_unique iprinter ts.ts_name
| Dparam ls
| Dlogic ((ls,_)::_)
- | Dind ((ls,_)::_) -> id_unique iprinter ls.ls_name
+ | Dind (_, (ls,_)::_) -> id_unique iprinter ls.ls_name
| Dprop (_,pr,_) -> id_unique iprinter pr.pr_name
| Ddata []
| Dlogic []
- | Dind [] -> assert false in
+ | Dind (_, []) -> assert false in
let prev = output_till_statement fmt old name in
match d.d_node with
| Dtype ts ->
@@ -704,8 +705,8 @@ let print_decl ~old info fmt d =
print_logic_decl info fmt ld
| Dlogic ll ->
print_recursive_decl info fmt ll
- | Dind il ->
- print_list nothing (print_ind_decl info) fmt il
+ | Dind (s, il) ->
+ print_list nothing (print_ind_decl info s) fmt il
| Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn ->
()
| Dprop pr ->
diff --git a/src/printer/pvs.ml b/src/printer/pvs.ml
index 235df98346..983b0ef185 100644
--- a/src/printer/pvs.ml
+++ b/src/printer/pvs.ml
@@ -764,8 +764,11 @@ let print_decl ~old info fmt d = match d.d_node with
print_logic_decl ~old info fmt ld
| Dlogic ll ->
print_recursive_decl info fmt ll
- | Dind il ->
+ | Dind (Ind, il) ->
print_list nothing (print_ind_decl info) fmt il
+ | Dind (Coind, _) ->
+ unsupportedDecl d
+ "PVS: coinductive definitions are not supported"
| Dprop (_, pr, _) when Mid.mem pr.pr_name info.info_syn ->
()
| Dprop (k, pr, f) ->
diff --git a/src/printer/why3printer.ml b/src/printer/why3printer.ml
index fc47bb0778..b3288bb023 100644
--- a/src/printer/why3printer.ml
+++ b/src/printer/why3printer.ml
@@ -306,16 +306,20 @@ let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
print_pr pr print_ident_labels pr.pr_name print_term f
-let print_ind_decl fst fmt (ps,bl) =
+let ind_sign = function
+ | Ind -> "inductive"
+ | Coind -> "coinductive"
+
+let print_ind_decl s fst fmt (ps,bl) =
fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]@\n@\n"
- (if fst then "inductive" else "with") print_ls ps
+ (if fst then ind_sign s else "with") print_ls ps
print_ident_labels ps.ls_name
(print_list nothing print_ty_arg) ps.ls_args
(print_list newline print_ind) bl
-let print_ind_decl first fmt d =
+let print_ind_decl s first fmt d =
if not (query_remove (fst d).ls_name) then
- (print_ind_decl first fmt d; forget_tvs ())
+ (print_ind_decl s first fmt d; forget_tvs ())
let print_pkind = Pretty.print_pkind
@@ -338,7 +342,7 @@ let print_decl fmt d = match d.d_node with
| Ddata tl -> print_list_next nothing print_data_decl fmt tl
| Dparam ls -> print_param_decl fmt ls
| Dlogic ll -> print_list_next nothing print_logic_decl fmt ll
- | Dind il -> print_list_next nothing print_ind_decl fmt il
+ | Dind (s, il) -> print_list_next nothing (print_ind_decl s) fmt il
| Dprop p -> print_prop_decl fmt p
let print_inst_ts fmt (ts1,ts2) =
diff --git a/src/programs/pgm_ocaml.ml b/src/programs/pgm_ocaml.ml
index 58894cf66f..620bed13ad 100644
--- a/src/programs/pgm_ocaml.ml
+++ b/src/programs/pgm_ocaml.ml
@@ -414,7 +414,7 @@ let logic_decl fmt d = match d.d_node with
print_param_decl fmt ls
| Dlogic ll ->
print_list_next newline print_logic_decl fmt ll
- | Dind il ->
+ | Dind (_, il) ->
print_list_next newline print_ind_decl fmt il
| Dprop (pk, pr, _) ->
fprintf fmt "(* %a %a *)" Pretty.print_pkind pk Pretty.print_pr pr
diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml
index b09cfb27c0..3903500411 100644
--- a/src/programs/pgm_typing.ml
+++ b/src/programs/pgm_typing.ml
@@ -2264,7 +2264,7 @@ let add_logics uc d =
in
match d with
| LogicDecl dl -> List.fold_left add uc dl
- | IndDecl dl -> List.fold_left addi uc dl
+ | IndDecl (_, dl) -> List.fold_left addi uc dl
| Meta _ | PropDecl _ | TypeDecl _ -> assert false
let find_module penv lmod q id = match q with
diff --git a/src/session/termcode.ml b/src/session/termcode.ml
index 2aea5a4b08..67edf9f0d4 100644
--- a/src/session/termcode.ml
+++ b/src/session/termcode.ml
@@ -208,7 +208,7 @@ let decl_shape ~(push:string->'a->'a) (acc:'a) d : 'a =
List.fold_right
(fun d acc -> logic_decl_shape ~push acc d)
ldl (push tag_Dlogic acc)
- | Decl.Dind idl ->
+ | Decl.Dind (_, idl) ->
List.fold_right
(fun d acc -> logic_ind_decl_shape ~push acc d)
idl (push tag_Dind acc)
diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml
index 81f8af9a25..f65e6b0f18 100644
--- a/src/transform/eliminate_definition.ml
+++ b/src/transform/eliminate_definition.ml
@@ -33,9 +33,9 @@ let elim q spr d = match d.d_node with
| Dlogic l ->
let ld, id = List.fold_right (add_id q) l ([],[]) in
ld @ (if id = [] then [] else [create_logic_decl id])
- | Dind l ->
+ | Dind (s, l) ->
let ld, id = List.fold_right (add_id q) l ([],[]) in
- ld @ (if id = [] then [] else [create_ind_decl id])
+ ld @ (if id = [] then [] else [create_ind_decl s id])
| Dprop (Paxiom,pr,_) when Spr.mem pr spr -> []
| _ -> [d]
diff --git a/src/transform/eliminate_inductive.ml b/src/transform/eliminate_inductive.ml
index 22a036001c..2ab962888a 100644
--- a/src/transform/eliminate_inductive.ml
+++ b/src/transform/eliminate_inductive.ml
@@ -52,7 +52,7 @@ let inv acc (ps,al) =
create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
let elim d = match d.d_node with
- | Dind il ->
+ | Dind (_, il) ->
let dl = List.fold_left log [] il in
let dl = List.fold_left imp dl il in
let dl = List.fold_left inv dl il in
diff --git a/src/transform/encoding_explicit.ml b/src/transform/encoding_explicit.ml
index 88c70875c3..583f8dc60e 100644
--- a/src/transform/encoding_explicit.ml
+++ b/src/transform/encoding_explicit.ml
@@ -104,10 +104,10 @@ module Transform = struct
[Decl.create_logic_decl (List.map helper decls)]
(** transform an inductive declaration *)
- let ind_transform idl =
+ let ind_transform s idl =
let iconv (pr,f) = pr, Libencoding.t_type_close term_transform f in
let conv (ls,il) = findL ls, List.map iconv il in
- [Decl.create_ind_decl (List.map conv idl)]
+ [Decl.create_ind_decl s (List.map conv idl)]
(** transforms a proposition into another (mostly a substitution) *)
let prop_transform (prop_kind, prop_name, f) =
@@ -126,7 +126,7 @@ let decl d = match d.d_node with
not supported, run eliminate_algebraic"
| Dparam ls -> Transform.param_transform ls
| Dlogic ldl -> Transform.logic_transform ldl
- | Dind idl -> Transform.ind_transform idl
+ | Dind (s, idl) -> Transform.ind_transform s idl
| Dprop prop -> Transform.prop_transform prop
let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
diff --git a/src/transform/encoding_guard.ml b/src/transform/encoding_guard.ml
index dc075764ce..4795a31f62 100644
--- a/src/transform/encoding_guard.ml
+++ b/src/transform/encoding_guard.ml
@@ -209,10 +209,10 @@ module Transform = struct
"Recursively-defined symbols are not supported, run eliminate_recursion"
(** transform an inductive declaration *)
- let ind_transform kept idl =
+ let ind_transform kept s idl =
let iconv (pr,f) = pr, f_type_close_select kept f in
let conv (ls,il) = findL ls, List.map iconv il in
- [Decl.create_ind_decl (List.map conv idl)]
+ [Decl.create_ind_decl s (List.map conv idl)]
(** transforms a proposition into another (mostly a substitution) *)
let prop_transform kept (prop_kind, prop_name, f) =
@@ -231,7 +231,7 @@ let decl kept d = match d.d_node with
not supported, run eliminate_algebraic"
| Dparam ls -> Transform.param_transform kept ls
| Dlogic ldl -> Transform.logic_transform kept d ldl
- | Dind idl -> Transform.ind_transform kept idl
+ | Dind (s, idl) -> Transform.ind_transform kept s idl
| Dprop prop -> Transform.prop_transform kept prop
let empty_th =
diff --git a/src/transform/libencoding.ml b/src/transform/libencoding.ml
index cbad3a1c5f..5f28b2e633 100644
--- a/src/transform/libencoding.ml
+++ b/src/transform/libencoding.ml
@@ -228,10 +228,10 @@ let d_monomorph kept lsmap d =
close ls vl (t_mono vmap e)
in
[create_logic_decl (List.map conv ldl)]
- | Dind idl ->
+ | Dind (s, idl) ->
let iconv (pr,f) = pr, t_mono Mvs.empty f in
let conv (ls,il) = lsmap ls, List.map iconv il in
- [create_ind_decl (List.map conv idl)]
+ [create_ind_decl s (List.map conv idl)]
| Dprop (k,pr,f) ->
[create_prop_decl k pr (t_mono Mvs.empty f)]
in
diff --git a/src/whyml/mlw_module.ml b/src/whyml/mlw_module.ml
index c2bd475fcb..f9065a95ff 100644
--- a/src/whyml/mlw_module.ml
+++ b/src/whyml/mlw_module.ml
@@ -204,7 +204,8 @@ let add_ty_decl = add_to_theory Theory.add_ty_decl
let add_data_decl = add_to_theory Theory.add_data_decl
let add_param_decl = add_to_theory Theory.add_param_decl
let add_logic_decl = add_to_theory Theory.add_logic_decl
-let add_ind_decl = add_to_theory Theory.add_ind_decl
+let add_ind_decl uc s dl =
+ { uc with muc_theory = Theory.add_ind_decl uc.muc_theory s dl }
let add_prop_decl uc k pr f =
{ uc with muc_theory = Theory.add_prop_decl uc.muc_theory k pr f }
diff --git a/src/whyml/mlw_module.mli b/src/whyml/mlw_module.mli
index 8b9762ffa4..997d59396a 100644
--- a/src/whyml/mlw_module.mli
+++ b/src/whyml/mlw_module.mli
@@ -90,7 +90,7 @@ val add_ty_decl : module_uc -> tysymbol -> module_uc
val add_data_decl : module_uc -> Decl.data_decl list -> module_uc
val add_param_decl : module_uc -> lsymbol -> module_uc
val add_logic_decl : module_uc -> logic_decl list -> module_uc
-val add_ind_decl : module_uc -> ind_decl list -> module_uc
+val add_ind_decl : module_uc -> ind_sign -> ind_decl list -> module_uc
val add_prop_decl : module_uc -> prop_kind -> prsymbol -> term -> module_uc
val use_export_theory: module_uc -> theory -> module_uc
--
GitLab