Skip to content

GitLab

why3
why3
Commit e8691321 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

hide the implementation of fs_defn/ps_defn in Theory

parent a481bbc5
Hide whitespace changes
Inline Side-by-side
Showing with 98 additions and 95 deletions
src/core/term.ml
View file @ e8691321
......@@ -168,18 +168,17 @@ let pat_any pr pat =
exception BadArity
exception ConstructorExpected
let pat_app f pl ty =
if not f.fs_constr then raise ConstructorExpected else
let args, res = f.fs_scheme in
let _ =
try List.fold_left2 matching
(matching Mid.empty res ty)
exception ConstructorExpected of fsymbol
let pat_app fs pl ty =
if not fs.fs_constr then raise (ConstructorExpected fs);
let args, res = fs.fs_scheme in
ignore (try
List.fold_left2 Ty.matching
(Ty.matching Mid.empty res ty)
args (List.map (fun p -> p.pat_ty) pl)
with Invalid_argument _ -> raise BadArity
in
pat_app f pl ty
with Invalid_argument _ -> raise BadArity);
pat_app fs pl ty
let pat_as p v =
if p.pat_ty == v.vs_ty then pat_as p v else raise TypeMismatch
......@@ -975,12 +974,16 @@ let f_let v t1 f2 =
let t_eps v f = t_eps v (f_abst_single v f)
exception NonLinear of vsymbol
let f_quant q vl tl f = if vl = [] then f else
let i = ref (-1) in
let add m v = incr i; Mvs.add v !i m in
let add m v =
if Mvs.mem v m then raise (NonLinear v);
incr i; Mvs.add v !i m
in
let m = List.fold_left add Mvs.empty vl in
let tl = tr_map (t_abst m 0) (f_abst m 0) tl in
(* FIXME: should we do any checks for triggers? *)
f_quant q vl (!i + 1) tl (f_abst m 0 f)
let f_forall = f_quant Fforall
......@@ -1004,16 +1007,14 @@ let f_app p tl =
in
f_app p tl
exception NonLinear
let pat_varmap p =
let i = ref (-1) in
let rec mk_map acc p = match p.pat_node with
| Pvar n ->
if Mvs.mem n acc then raise NonLinear;
if Mvs.mem n acc then raise (NonLinear n);
incr i; Mvs.add n !i acc
| Pas (p, n) ->
if Mvs.mem n acc then raise NonLinear;
if Mvs.mem n acc then raise (NonLinear n);
incr i; mk_map (Mvs.add n !i acc) p
| _ -> pat_fold mk_map acc p
in
......@@ -1022,15 +1023,15 @@ let pat_varmap p =
let t_case t bl ty =
let t_make_branch (p, tbr) =
if tbr.t_ty != ty then raise TypeMismatch else
if p.pat_ty != t.t_ty then raise TypeMismatch else
if tbr.t_ty != ty then raise TypeMismatch;
if p.pat_ty != t.t_ty then raise TypeMismatch;
let m, nv = pat_varmap p in (p, nv, t_abst m 0 tbr)
in
t_case t (List.map t_make_branch bl) ty
let f_case t bl =
let f_make_branch (p, fbr) =
if p.pat_ty != t.t_ty then raise TypeMismatch else
if p.pat_ty != t.t_ty then raise TypeMismatch;
let m, nv = pat_varmap p in (p, nv, f_abst m 0 fbr)
in
f_case t (List.map f_make_branch bl)
......
src/core/term.mli
View file @ e8691321
......@@ -20,10 +20,6 @@
open Ident
open Ty
exception NonLinear
exception BadArity
exception ConstructorExpected
(** Variable symbols *)
type vsymbol = private {
......@@ -64,6 +60,12 @@ module Sps : Set.S with type elt = psymbol
module Mps : Map.S with type key = psymbol
module Hps : Hashtbl.S with type key = psymbol
(** Exceptions *)
exception BadArity
exception NonLinear of vsymbol
exception ConstructorExpected of fsymbol
(** Patterns *)
type pattern = private {
......
src/core/theory.ml
View file @ e8691321
......@@ -35,9 +35,12 @@ type ty_decl = tysymbol * ty_def
(* logic declaration *)
type fs_defn = fsymbol * vsymbol list * term * fmla
type ps_defn = psymbol * vsymbol list * fmla * fmla
type logic_decl =
| Lfunction of fsymbol * fmla option
| Lpredicate of psymbol * fmla option
| Lfunction of fsymbol * fs_defn option
| Lpredicate of psymbol * ps_defn option
| Linductive of psymbol * (ident * fmla) list
(* proposition declaration *)
......@@ -74,7 +77,7 @@ module D = struct
| _ -> false
let eq_fd fs1 fd1 fs2 fd2 = fs1 == fs2 && match fd1,fd2 with
| Some fd1, Some fd2 -> fd1 == fd2
| Some (_,_,_,fd1), Some (_,_,_,fd2) -> fd1 == fd2
| None, None -> true
| _ -> false
......@@ -97,7 +100,7 @@ module D = struct
let tag fs = fs.fs_name.id_tag in
1 + Hashcons.combine_list tag ts.ts_name.id_tag l
let hs_fd fd = Hashcons.combine_option (fun f -> f.f_tag) fd
let hs_fd fd = Hashcons.combine_option (fun (_,_,_,f) -> f.f_tag) fd
let hs_ld ld = match ld with
| Lfunction (fs,fd) -> Hashcons.combine fs.fs_name.id_tag (hs_fd fd)
......@@ -137,16 +140,29 @@ exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition of fmla
exception MalformedDefinition
exception UnboundVars of Svs.t
let make_fdef fs vl t =
let check_fvs f =
let fvs = f_freevars Svs.empty f in
if Svs.is_empty fvs then f else raise (UnboundVars fvs)
let make_fs_defn fs vl t =
if fs.fs_constr then raise (IllegalConstructor fs);
let hd = t_app fs (List.map t_var vl) t.t_ty in
Lfunction (fs, Some (f_forall vl [] (f_equ hd t)))
let fd = f_forall vl [] (f_equ hd t) in
fs, vl, t, check_fvs fd
let make_pdef ps vl f =
let make_ps_defn ps vl f =
let hd = f_app ps (List.map t_var vl) in
Lpredicate (ps, Some (f_forall vl [] (f_iff hd f)))
let pd = f_forall vl [] (f_iff hd f) in
ps, vl, f, check_fvs pd
let open_fs_defn (fs,vl,t,_) = (fs,vl,t)
let open_ps_defn (ps,vl,f,_) = (ps,vl,f)
let fs_defn_axiom (_,_,_,fd) = fd
let ps_defn_axiom (_,_,_,pd) = pd
let create_type tdl =
let check_constructor ty fs =
......@@ -175,43 +191,18 @@ let create_type tdl =
create_type tdl
let create_logic ldl =
let check_fv f =
let fvs = f_freevars Svs.empty f in
if not (Svs.is_empty fvs) then raise (UnboundVars fvs);
in
let check_def fd =
check_fv fd;
match fd.f_node with
| Fquant (Fforall, fq) -> f_open_quant fq
| _ -> ([],[],fd)
in
let check_ax (_,f) =
check_fv f;
assert false (* TODO *)
in
let check_decl = function
| Lfunction (fs, Some fd) ->
if fs.fs_constr then raise (IllegalConstructor fs);
let (vl,_,f) = check_def fd in
let hd = match f.f_node with
| Fapp (ps, [hd; _]) when ps == ps_equ -> hd
| _ -> raise (MalformedDefinition fd)
in
let t = try t_app fs (List.map t_var vl) hd.t_ty with
| _ -> raise (MalformedDefinition fd)
in
if t != hd then raise (MalformedDefinition fd)
let (s,_,_,_) = fd in
if fs != s then raise MalformedDefinition
| Lpredicate (ps, Some pd) ->
let (vl,_,f) = check_def pd in
let hd = match f.f_node with
| Fbinop (Fiff, hd, _) -> hd
| _ -> raise (MalformedDefinition pd)
in
let f = try f_app ps (List.map t_var vl) with
| _ -> raise (MalformedDefinition pd)
in
if f != hd then raise (MalformedDefinition pd)
let (s,_,_,_) = pd in
if ps != s then raise MalformedDefinition
| Linductive (ps,la) ->
let check_ax (_,f) =
ignore (check_fvs f);
assert false (* TODO *)
in
List.iter check_ax la
| _ -> ()
in
......@@ -459,13 +450,13 @@ let check_logic kn = function
known_ty kn (snd fs.fs_scheme);
List.iter (known_ty kn) (fst fs.fs_scheme);
begin match df with
| Some f -> known_fmla kn f
| Some (_,_,_,f) -> known_fmla kn f
| None -> ()
end
| Lpredicate (ps, dp) ->
List.iter (known_ty kn) ps.ps_scheme;
begin match dp with
| Some f -> known_fmla kn f
| Some (_,_,_,f) -> known_fmla kn f
| None -> ()
end
| Linductive (ps, la) ->
......@@ -509,7 +500,7 @@ let clone_export uc th i =
let ts_table = Hashtbl.create 17 in
let known = ref th.th_known in
let rec memo_ts ts =
try
try
Hashtbl.find ts_table ts.ts_name
with Not_found ->
let nm = id_clone ts.ts_name in
......@@ -522,14 +513,14 @@ let clone_export uc th i =
known := Mid.add ts'.ts_name uc.uc_name (Mid.remove ts.ts_name !known);
ts'
in
let find_ts ts =
let find_ts ts =
let tid = Mid.find ts.ts_name th.th_known in
if tid == th.th_name then memo_ts ts else ts
in
(* 1. merge in the new namespace *)
let rec merge_namespace acc ns =
let acc =
Mnm.fold (fun n ts acc -> add_ts n (find_ts ts) acc) ns.ns_ts acc
let acc =
Mnm.fold (fun n ts acc -> add_ts n (find_ts ts) acc) ns.ns_ts acc
in
(* ... *)
(* let acc = Mnm.fold (fun n ns acc -> ) ns.ns_ns acc in *)
......
src/core/theory.mli
View file @ e8691321
......@@ -33,9 +33,12 @@ type ty_decl = tysymbol * ty_def
(* logic declaration *)
type fs_defn
type ps_defn
type logic_decl =
| Lfunction of fsymbol * fmla option
| Lpredicate of psymbol * fmla option
| Lfunction of fsymbol * fs_defn option
| Lpredicate of psymbol * ps_defn option
| Linductive of psymbol * (ident * fmla) list
(* proposition declaration *)
......@@ -61,8 +64,14 @@ type decl = private {
(* smart constructors *)
val make_fdef : fsymbol -> vsymbol list -> term -> logic_decl
val make_pdef : psymbol -> vsymbol list -> fmla -> logic_decl
val make_fs_defn : fsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : psymbol -> vsymbol list -> fmla -> ps_defn
val open_fs_defn : fs_defn -> fsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> psymbol * vsymbol list * fmla
val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla
val create_type : ty_decl list -> decl
val create_logic : logic_decl list -> decl
......@@ -75,7 +84,7 @@ exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception IllegalConstructor of fsymbol
exception MalformedDefinition of fmla
exception MalformedDefinition
exception UnboundVars of Svs.t
(** Theory *)
......
src/parser/typing.ml
View file @ e8691321
......@@ -657,32 +657,30 @@ let add_logics loc dl th =
match d.ld_type with
| None -> (* predicate *)
let ps = Hashtbl.find psymbols id in
begin match d.ld_def with
| None ->
Lpredicate (ps, None)
let defn = match d.ld_def with
| None -> None
| Some f ->
let f = dfmla denv f in
let vl = mk_vlist ps.ps_scheme in
let env = env_of_vsymbol_list vl in
make_pdef ps vl (fmla env f)
end
Some (make_ps_defn ps vl (fmla env f))
in
Lpredicate (ps, defn)
| Some ty -> (* function *)
let fs = Hashtbl.find fsymbols id in
begin match d.ld_def with
| None ->
Lfunction (fs, None)
let defn = match d.ld_def with
| None -> None
| Some t ->
let loc = t.pp_loc in
let t = dterm denv t in
let vl = mk_vlist (fst fs.fs_scheme) in
let env = env_of_vsymbol_list vl in
try
make_fdef fs vl (term env t)
with _ ->
error ~loc (TermExpectedType
((fun f -> print_dty f t.dt_ty),
(fun f -> print_dty f (dty denv ty))))
end
try Some (make_fs_defn fs vl (term env t))
with _ -> error ~loc (TermExpectedType
((fun f -> print_dty f t.dt_ty),
(fun f -> print_dty f (dty denv ty))))
in
Lfunction (fs, defn)
in
let dl = List.map type_decl dl in
add_decl th (create_logic dl)
......
src/pretty.ml
View file @ e8691321
......@@ -126,11 +126,11 @@ let print_logic_decl fmt = function
| Lfunction (fs,None) -> fprintf fmt "@[<hov 2>logic %a@]" print_fsymbol fs
| Lfunction (fs,Some fd) ->
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident fs.fs_name
print_fmla fd
print_fmla (fs_defn_axiom fd)
| Lpredicate (fs,None) -> fprintf fmt "@[<hov 2>logic %a@]" print_psymbol fs
| Lpredicate (ps,Some fd) ->
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ps_name
print_fmla fd
print_fmla (ps_defn_axiom fd)
| Linductive _ -> assert false (*TODO*)
let print_decl fmt d = match d.d_node with
......
src/transform/simplify_recursive_definition.ml
View file @ e8691321
......@@ -102,13 +102,15 @@ let elt d =
let s = match l with
| None -> Sid.empty
| Some fd ->
let fd = fs_defn_axiom fd in
f_s_fold tyoccurences toccurences foccurences Sid.empty fd in
Mid.add fs.fs_name s acc
| Lpredicate (ps,l) ->
let s = match l with
| None -> Sid.empty
| Some fd ->
f_s_fold tyoccurences toccurences foccurences Sid.empty fd in
let fd = ps_defn_axiom fd in
f_s_fold tyoccurences toccurences foccurences Sid.empty fd in
Mid.add ps.ps_name s acc
| Linductive (ps,l) ->
let s = List.fold_left
......
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