coinductive predicates

parent 739714d4
* marks an incompatible change * marks an incompatible change
o co-inductive predicates
o new option -e for "why3session latex" allows to specify when to o new option -e for "why3session latex" allows to specify when to
split tables in parts split tables in parts
......
...@@ -6,6 +6,7 @@ ...@@ -6,6 +6,7 @@
| "function" function-decl ("with" logic-decl)* ; | "function" function-decl ("with" logic-decl)* ;
| "predicate" predicate-decl ("with" logic-decl)* ; | "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ; | "inductive" inductive-decl ("with" inductive-decl)* ;
| "coinductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ; | "axiom" ident ":" formula ;
| "lemma" ident ":" formula ; | "lemma" ident ":" formula ;
| "goal" ident ":" formula ; | "goal" ident ":" formula ;
......
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries ;; Note: comment font-lock is guaranteed by suitable syntax entries
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face) '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-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 '("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) ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
) )
......
...@@ -147,10 +147,11 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. ...@@ -147,10 +147,11 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>abstract</keyword> <keyword>abstract</keyword>
<keyword>axiom</keyword> <keyword>axiom</keyword>
<keyword>clone</keyword> <keyword>clone</keyword>
<keyword>coinductive</keyword>
<keyword>constant</keyword>
<keyword>end</keyword> <keyword>end</keyword>
<keyword>exception</keyword> <keyword>exception</keyword>
<keyword>export</keyword> <keyword>export</keyword>
<keyword>constant</keyword>
<keyword>function</keyword> <keyword>function</keyword>
<keyword>goal</keyword> <keyword>goal</keyword>
<keyword>ghost</keyword> <keyword>ghost</keyword>
......
...@@ -87,7 +87,7 @@ syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\|prop\) ...@@ -87,7 +87,7 @@ syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\|prop\)
syn keyword whyKeyword as constant syn keyword whyKeyword as constant
syn keyword whyKeyword else epsilon exists syn keyword whyKeyword else epsilon exists
syn keyword whyKeyword false forall function 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 let meta
syn keyword whyKeyword not predicate syn keyword whyKeyword not predicate
syn keyword whyKeyword then true type with syn keyword whyKeyword then true type with
......
...@@ -728,7 +728,8 @@ and decompose_inductive dep env i = ...@@ -728,7 +728,8 @@ and decompose_inductive dep env i =
if cl = [] then Decl.create_param_decl ls :: pl, dl else pl, d :: dl if cl = [] then Decl.create_param_decl ls :: pl, dl else pl, d :: dl
in in
let pl, dl = List.fold_right add 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 (* translation of a Coq term
assumption: t:T:Set *) assumption: t:T:Set *)
......
...@@ -288,6 +288,10 @@ let create_prsymbol n = { pr_name = id_register n } ...@@ -288,6 +288,10 @@ let create_prsymbol n = { pr_name = id_register n }
type ind_decl = lsymbol * (prsymbol * term) list type ind_decl = lsymbol * (prsymbol * term) list
type ind_sign = Ind | Coind
type ind_list = ind_sign * ind_decl list
(** Proposition declaration *) (** Proposition declaration *)
type prop_kind = type prop_kind =
...@@ -312,7 +316,7 @@ and decl_node = ...@@ -312,7 +316,7 @@ and decl_node =
| Ddata of data_decl list (* recursive algebraic types *) | Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *) | Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive 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 *) | Dprop of prop_decl (* axiom / lemma / goal *)
(** Declarations *) (** Declarations *)
...@@ -341,7 +345,7 @@ module Hsdecl = Hashcons.Make (struct ...@@ -341,7 +345,7 @@ module Hsdecl = Hashcons.Make (struct
| Ddata l1, Ddata l2 -> list_all2 eq_td l1 l2 | Ddata l1, Ddata l2 -> list_all2 eq_td l1 l2
| Dparam s1, Dparam s2 -> ls_equal s1 s2 | Dparam s1, Dparam s2 -> ls_equal s1 s2
| Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2 | 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) -> | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2 k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2
| _,_ -> false | _,_ -> false
...@@ -365,7 +369,7 @@ module Hsdecl = Hashcons.Make (struct ...@@ -365,7 +369,7 @@ module Hsdecl = Hashcons.Make (struct
| Ddata l -> Hashcons.combine_list hs_td 3 l | Ddata l -> Hashcons.combine_list hs_td 3 l
| Dparam s -> ls_hash s | Dparam s -> ls_hash s
| Dlogic l -> Hashcons.combine_list hs_ld 5 l | 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)) | 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 } 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 ...@@ -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 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 | _ -> 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; if idl = [] then raise EmptyDecl;
let add acc (ps,_) = Sls.add ps acc in let add acc (ps,_) = Sls.add ps acc in
let sps = List.fold_left add Sls.empty idl in let sps = List.fold_left add Sls.empty idl in
...@@ -537,7 +541,7 @@ let create_ind_decl idl = ...@@ -537,7 +541,7 @@ let create_ind_decl idl =
List.fold_left (check_ax ps) (syms,news) al List.fold_left (check_ax ps) (syms,news) al
in in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl 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 create_prop_decl k p f =
let syms = syms_term Sid.empty f in let syms = syms_term Sid.empty f in
...@@ -554,10 +558,10 @@ let decl_map fn d = match d.d_node with ...@@ -554,10 +558,10 @@ let decl_map fn d = match d.d_node with
close ls vl (fn e) close ls vl (fn e)
in in
create_logic_decl (List.map fn l) create_logic_decl (List.map fn l)
| Dind l -> | Dind (s, l) ->
let fn (pr,f) = pr, fn f in let fn (pr,f) = pr, fn f in
let fn (ps,l) = ps, List.map fn l 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) -> | Dprop (k,pr,f) ->
create_prop_decl k pr (fn f) create_prop_decl k pr (fn f)
...@@ -569,7 +573,7 @@ let decl_fold fn acc d = match d.d_node with ...@@ -569,7 +573,7 @@ let decl_fold fn acc d = match d.d_node with
fn acc e fn acc e
in in
List.fold_left fn acc l List.fold_left fn acc l
| Dind l -> | Dind (_, l) ->
let fn acc (_,f) = fn acc f in let fn acc (_,f) = fn acc f in
let fn acc (_,l) = List.fold_left fn acc l in let fn acc (_,l) = List.fold_left fn acc l in
List.fold_left fn acc l List.fold_left fn acc l
...@@ -591,9 +595,9 @@ let decl_map_fold fn acc d = match d.d_node with ...@@ -591,9 +595,9 @@ let decl_map_fold fn acc d = match d.d_node with
in in
let acc,l = Util.map_fold_left fn acc l in let acc,l = Util.map_fold_left fn acc l in
acc, create_logic_decl l 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 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) -> | Dprop (k,pr,f) ->
let acc, f = fn acc f in let acc, f = fn acc f in
acc, create_prop_decl k pr f acc, create_prop_decl k pr f
...@@ -642,7 +646,7 @@ let find_constructors kn ts = ...@@ -642,7 +646,7 @@ let find_constructors kn ts =
let find_inductive_cases kn ps = let find_inductive_cases kn ps =
match (Mid.find ps.ls_name kn).d_node with match (Mid.find ps.ls_name kn).d_node with
| Dind dl -> List.assq ps dl | Dind (_, dl) -> List.assq ps dl
| Dlogic _ -> [] | Dlogic _ -> []
| Dtype _ -> [] | Dtype _ -> []
| _ -> assert false | _ -> assert false
...@@ -655,7 +659,7 @@ let find_logic_definition kn ls = ...@@ -655,7 +659,7 @@ let find_logic_definition kn ls =
let find_prop kn pr = let find_prop kn pr =
match (Mid.find pr.pr_name kn).d_node with match (Mid.find pr.pr_name kn).d_node with
| Dind dl -> | Dind (_, dl) ->
let test (_,l) = List.mem_assq pr l in let test (_,l) = List.mem_assq pr l in
List.assq pr (snd (List.find test dl)) List.assq pr (snd (List.find test dl))
| Dprop (_,_,f) -> f | Dprop (_,_,f) -> f
...@@ -663,7 +667,7 @@ let find_prop kn pr = ...@@ -663,7 +667,7 @@ let find_prop kn pr =
let find_prop_decl kn pr = let find_prop_decl kn pr =
match (Mid.find pr.pr_name kn).d_node with match (Mid.find pr.pr_name kn).d_node with
| Dind dl -> | Dind (_, dl) ->
let test (_,l) = List.mem_assq pr l in let test (_,l) = List.mem_assq pr l in
Paxiom, List.assq pr (snd (List.find test dl)) Paxiom, List.assq pr (snd (List.find test dl))
| Dprop (k,_,f) -> k,f | Dprop (k,_,f) -> k,f
......
...@@ -81,6 +81,10 @@ val pr_hash : prsymbol -> int ...@@ -81,6 +81,10 @@ val pr_hash : prsymbol -> int
type ind_decl = lsymbol * (prsymbol * term) list type ind_decl = lsymbol * (prsymbol * term) list
type ind_sign = Ind | Coind
type ind_list = ind_sign * ind_decl list
(* Proposition declaration *) (* Proposition declaration *)
type prop_kind = type prop_kind =
...@@ -105,7 +109,7 @@ and decl_node = ...@@ -105,7 +109,7 @@ and decl_node =
| Ddata of data_decl list (* recursive algebraic types *) | Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *) | Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive 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 *) | Dprop of prop_decl (* axiom / lemma / goal *)
module Mdecl : Map.S with type key = decl module Mdecl : Map.S with type key = decl
...@@ -121,7 +125,7 @@ val create_ty_decl : tysymbol -> decl ...@@ -121,7 +125,7 @@ val create_ty_decl : tysymbol -> decl
val create_data_decl : data_decl list -> decl val create_data_decl : data_decl list -> decl
val create_param_decl : lsymbol -> decl val create_param_decl : lsymbol -> decl
val create_logic_decl : logic_decl list -> 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 val create_prop_decl : prop_kind -> prsymbol -> term -> decl
(* exceptions *) (* exceptions *)
......
...@@ -358,9 +358,13 @@ let print_ind fmt (pr,f) = ...@@ -358,9 +358,13 @@ let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a%a :@ %a@]" fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
print_pr pr print_ident_labels pr.pr_name print_term f 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@]@]" 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_ident_labels ps.ls_name
(print_list nothing print_ty_arg) ps.ls_args (print_list nothing print_ty_arg) ps.ls_args
(print_list newline print_ind) bl; (print_list newline print_ind) bl;
...@@ -390,15 +394,15 @@ let print_decl fmt d = match d.d_node with ...@@ -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 | Ddata tl -> print_list_next newline print_data_decl fmt tl
| Dparam ls -> print_param_decl fmt ls | Dparam ls -> print_param_decl fmt ls
| Dlogic ll -> print_list_next newline print_logic_decl fmt ll | 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 | Dprop p -> print_prop_decl fmt p
let print_next_data_decl = print_data_decl false let print_next_data_decl = print_data_decl false
let print_data_decl = print_data_decl true let print_data_decl = print_data_decl true
let print_next_logic_decl = print_logic_decl false let print_next_logic_decl = print_logic_decl false
let print_logic_decl = print_logic_decl true let print_logic_decl = print_logic_decl true
let print_next_ind_decl = print_ind_decl false let print_next_ind_decl = print_ind_decl Ind false
let print_ind_decl = print_ind_decl true let print_ind_decl fmt s = print_ind_decl s true fmt
let print_inst_ts fmt (ts1,ts2) = let print_inst_ts fmt (ts1,ts2) =
fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2 fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
......
...@@ -58,7 +58,7 @@ val print_ty_decl : formatter -> tysymbol -> unit ...@@ -58,7 +58,7 @@ val print_ty_decl : formatter -> tysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit val print_data_decl : formatter -> data_decl -> unit
val print_param_decl : formatter -> lsymbol -> unit val print_param_decl : formatter -> lsymbol -> unit
val print_logic_decl : formatter -> logic_decl -> 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_data_decl : formatter -> data_decl -> unit
val print_next_logic_decl : formatter -> logic_decl -> unit val print_next_logic_decl : formatter -> logic_decl -> unit
val print_next_ind_decl : formatter -> ind_decl -> unit val print_next_ind_decl : formatter -> ind_decl -> unit
......
...@@ -172,7 +172,7 @@ let add_ty_decl tk ts = add_decl tk (create_ty_decl ts) ...@@ -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_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_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_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) let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)
(* task constructors *) (* task constructors *)
......
...@@ -80,7 +80,7 @@ val add_ty_decl : task -> tysymbol -> task ...@@ -80,7 +80,7 @@ val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task val add_param_decl : task -> lsymbol -> task
val add_logic_decl : task -> logic_decl list -> 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 val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
(** {2 utilities} *) (** {2 utilities} *)
......
...@@ -380,7 +380,7 @@ let add_decl uc d = ...@@ -380,7 +380,7 @@ let add_decl uc d =
| Ddata dl -> List.fold_left add_data uc dl | Ddata dl -> List.fold_left add_data uc dl
| Dparam ls -> add_symbol add_ls ls.ls_name ls uc | Dparam ls -> add_symbol add_ls ls.ls_name ls uc
| Dlogic dl -> List.fold_left add_logic uc dl | 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 | Dprop p -> add_prop uc p
(** Declaration constructors + add_decl *) (** Declaration constructors + add_decl *)
...@@ -389,7 +389,7 @@ let add_ty_decl uc ts = add_decl uc (create_ty_decl ts) ...@@ -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_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_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_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) let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
(** Use *) (** Use *)
...@@ -566,7 +566,7 @@ let cl_logic cl inst ldl = ...@@ -566,7 +566,7 @@ let cl_logic cl inst ldl =
in in
create_logic_decl (List.map add_logic ldl) 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) = let add_case (pr,f) =
if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal
then raise (CannotInstantiate pr.pr_name) then raise (CannotInstantiate pr.pr_name)
...@@ -577,7 +577,7 @@ let cl_ind cl inst idl = ...@@ -577,7 +577,7 @@ let cl_ind cl inst idl =
then raise (CannotInstantiate ps.ls_name) then raise (CannotInstantiate ps.ls_name)
else cl_find_ls cl ps, List.map add_case la else cl_find_ls cl ps, List.map add_case la
in 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 cl_prop cl inst (k,pr,f) =
let k' = match k with let k' = match k with
......
...@@ -140,7 +140,7 @@ val add_ty_decl : theory_uc -> tysymbol -> theory_uc ...@@ -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_data_decl : theory_uc -> data_decl list -> theory_uc
val add_param_decl : theory_uc -> lsymbol -> theory_uc val add_param_decl : theory_uc -> lsymbol -> theory_uc
val add_logic_decl : theory_uc -> logic_decl list -> 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 val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
(** Use *) (** Use *)
......
...@@ -45,6 +45,7 @@ ...@@ -45,6 +45,7 @@
"as", AS; "as", AS;
"axiom", AXIOM; "axiom", AXIOM;
"clone", CLONE; "clone", CLONE;
"coinductive", COINDUCTIVE;
"constant", CONSTANT; "constant", CONSTANT;
"else", ELSE; "else", ELSE;
"end", END; "end", END;
......
...@@ -202,7 +202,7 @@ end ...@@ -202,7 +202,7 @@ end
/* keywords */ /* keywords */
%token AS AXIOM CLONE CONSTANT %token AS AXIOM CLONE COINDUCTIVE CONSTANT
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION %token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA %token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE %token LET MATCH META NAMESPACE NOT PROP PREDICATE
...@@ -336,8 +336,8 @@ decl: ...@@ -336,8 +336,8 @@ decl:
{ LogicDecl $2 } { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate | PREDICATE list1_logic_decl_predicate
{ LogicDecl $2 } { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl | inductive list1_inductive_decl
{ IndDecl $2 } { IndDecl ($1, $2) }
| AXIOM ident labels COLON lexpr | AXIOM ident labels COLON lexpr
{ PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) } { PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
| LEMMA ident labels COLON lexpr | LEMMA ident labels COLON lexpr
...@@ -348,6 +348,11 @@ decl: ...@@ -348,6 +348,11 @@ decl:
{ Meta (floc (), $2, $3) } { Meta (floc (), $2, $3) }
; ;
inductive:
| INDUCTIVE { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;
/* Use and clone */ /* Use and clone */
use_clone: use_clone:
......
...@@ -167,7 +167,7 @@ type use_clone = loc * use * clone_subst list option ...@@ -167,7 +167,7 @@ type use_clone = loc * use * clone_subst list option
type decl = type decl =
| TypeDecl of type_decl list | TypeDecl of type_decl list
| LogicDecl of logic_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 | PropDecl of loc * prop_kind * ident * lexpr
| Meta of loc * ident * metarg list | Meta of loc * ident * metarg list
......
...@@ -156,7 +156,7 @@ let add_ty_decl uc ts = add_decl_with_tuples uc (create_ty_decl ts) ...@@ -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_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_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_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 add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
let rec dty uc env = function let rec dty uc env = function
...@@ -1036,7 +1036,7 @@ let add_prop k loc s f th = ...@@ -1036,7 +1036,7 @@ let add_prop k loc s f th =
let loc_of_id id = of_option id.Ident.id_loc 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 *) (* 1. create all symbols and make an environment with these symbols *)
let denv = create_denv () in let denv = create_denv () in
let psymbols = Hashtbl.create 17 in let psymbols = Hashtbl.create 17 in
...@@ -1062,7 +1062,7 @@ let add_inductives dl th = ...@@ -1062,7 +1062,7 @@ let add_inductives dl th =
in in
ps, List.map clause d.in_def ps, List.map clause d.in_def
in in
try add_ind_decl th (List.map type_decl dl) try add_ind_decl th s (List.map type_decl dl)
with with
| ClashSymbol s -> | ClashSymbol s ->
error ~loc:(Hashtbl.find propsyms s) (ClashSymbol s) error ~loc:(Hashtbl.find propsyms s) (ClashSymbol s)
...@@ -1115,8 +1115,8 @@ let add_decl th = function ...@@ -1115,8 +1115,8 @@ let add_decl th = function
add_types dl th add_types dl th
| LogicDecl dl -> | LogicDecl dl ->
add_logics dl th add_logics dl th
| IndDecl dl -> | IndDecl (s, dl) ->
add_inductives dl th add_inductives s dl th
| PropDecl (loc, k, s, f) -> | PropDecl (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th add_prop (prop_kind k) loc s f th
| Meta (loc, id, al) -> | Meta (loc, id, al) ->
......
...@@ -296,7 +296,7 @@ let print_decl info fmt d = match d.d_node with ...@@ -296,7 +296,7 @@ let print_decl info fmt d = match d.d_node with
| Dlogic dl -> | Dlogic dl ->
print_list nothing (print_logic_decl info) fmt dl print_list nothing (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d | 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 | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt) let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
......
...@@ -648,18 +648,19 @@ let print_recursive_decl info fmt dl = ...@@ -648,18 +648,19 @@ let print_recursive_decl info fmt dl =
let print_ind info fmt (pr,f) = let print_ind info fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) 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 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_ls ps print_implicit_params all_ty_params
(print_arrow_list (print_ty info)) ps.ls_args (print_arrow_list (print_ty info)) ps.ls_args
(print_list newline (print_ind info)) bl; (print_list newline (print_ind info)) bl;
print_implicits fmt ps ty_vars_args ty_vars_value all_ty_params; print_implicits fmt ps ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n" 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 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 print_prop_decl ~prev info fmt (k,pr,f) =
let params = t_ty_freevars Stv.empty f in let params = t_ty_freevars Stv.empty f in
...@@ -687,11 +688,11 @@ let print_decl ~old info fmt d = ...@@ -687,11 +688,11 @@ let print_decl ~old info fmt d =
| Ddata ((ts, _)::_) -> id_unique iprinter ts.ts_name | Ddata ((ts, _)::_) -> id_unique iprinter ts.ts_name
| Dparam ls | Dparam ls
| Dlogic ((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 | Dprop (_,pr,_) -> id_unique iprinter pr.pr_name
| Ddata [] | Ddata []
| Dlogic [] | Dlogic []
| Dind [] -> assert false in | Dind (_, []) -> assert false in
let prev = output_till_statement fmt old name in let prev = output_till_statement fmt old name in
match d.d_node with match d.d_node with
| Dtype ts -> | Dtype ts ->
...@@ -704,8 +705,8 @@ let print_decl ~old info fmt d = ...@@ -704,8 +705,8 @@ let print_decl ~old info fmt d =
print_logic_decl info fmt ld print_logic_decl info fmt ld
| Dlogic ll -> | Dlogic ll ->
print_recursive_decl info fmt ll print_recursive_decl info fmt ll
| Dind il -> | Dind (s, il) ->
print_list nothing (print_ind_decl info) fmt il print_list nothing (print_ind_decl info s) fmt il
| Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn -> | Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn ->
() ()
| Dprop pr -> | Dprop pr ->
......
...@@ -764,8 +764,11 @@ let print_decl ~old info fmt d = match d.d_node with ...@@ -764,8 +764,11 @@ let print_decl ~old info fmt d = match d.d_node with
print_logic_decl ~old info fmt ld print_logic_decl ~old info fmt ld
| Dlogic ll -> | Dlogic ll ->
print_recursive_decl info fmt ll print_recursive_decl info fmt ll
| Dind il -> | Dind (Ind, il) ->
print_list nothing (print_ind_decl info) fmt 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 (_, pr, _) when Mid.mem pr.pr_name info.info_syn ->
() ()