Commit 8a0f0ab5 authored by Andrei Paskevich's avatar Andrei Paskevich

merge expr with term/fmla

parent 6258e2fd
......@@ -67,15 +67,15 @@ let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let open_ls_defn (_,f) =
let vl, ef = f_open_forall f in
match ef.t_node with
| Tapp (_, [_; t2]) -> vl, Term t2
| Fbinop (_, _, f2) -> vl, Fmla f2
| Tapp (_, [_; t2]) -> vl, t2
| Fbinop (_, _, f2) -> vl, f2
| _ -> assert false
let open_fs_defn ld = let vl,e = open_ls_defn ld in
match e with Term t -> vl,t | _ -> assert false
if e.t_ty = None then assert false else vl,e
let open_ps_defn ld = let vl,e = open_ls_defn ld in
match e with Fmla f -> vl,f | _ -> assert false
if e.t_ty = None then vl,e else assert false
let ls_defn_axiom (_,f) = f
......@@ -636,7 +636,7 @@ let rec check_matchT kn () t = match t.t_node with
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Term t)));
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,t)));
t_fold (check_matchT kn) (check_matchF kn) () t
| _ -> t_fold (check_matchT kn) (check_matchF kn) () t
......@@ -644,7 +644,7 @@ and check_matchF kn () f = match f.t_node with
| Tcase (t1,bl) ->
let bl = List.map (fun b -> let p,f = f_open_branch b in [p],f) bl in
ignore (try Pattern.CompileFmla.compile (find_constructors kn) [t1] bl
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));
with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,f)));
f_fold (check_matchT kn) (check_matchF kn) () f
| _ -> f_fold (check_matchT kn) (check_matchF kn) () f
......
......@@ -230,7 +230,7 @@ let query_syntax sm id = Mid.find_option id sm
exception UnsupportedTysymbol of tysymbol * string
exception UnsupportedType of ty * string
exception UnsupportedExpr of expr * string
exception UnsupportedTerm of term * string
exception UnsupportedDecl of decl * string
exception NotImplemented of string
exception Unsupported of string
......@@ -239,9 +239,8 @@ exception Unsupported of string
let unsupportedTysymbol e s = raise (UnsupportedTysymbol (e,s))
let unsupportedType e s = raise (UnsupportedType (e,s))
let unsupportedTerm e s = raise (UnsupportedExpr (Term e,s))
let unsupportedFmla e s = raise (UnsupportedExpr (Fmla e,s))
let unsupportedExpr e s = raise (UnsupportedExpr (e,s))
let unsupportedTerm e s = raise (UnsupportedTerm (e,s))
let unsupportedFmla e s = raise (UnsupportedTerm (e,s))
let unsupportedDecl e s = raise (UnsupportedDecl (e,s))
let notImplemented s = raise (NotImplemented s)
let unsupported s = raise (Unsupported s)
......@@ -255,12 +254,6 @@ let catch_unsupportedTysymbol f e =
let catch_unsupportedTerm f e =
try f e with Unsupported s -> unsupportedTerm e s
let catch_unsupportedFmla f e =
try f e with Unsupported s -> unsupportedFmla e s
let catch_unsupportedExpr f e =
try f e with Unsupported s -> unsupportedExpr e s
let catch_unsupportedDecl f e =
try f e with Unsupported s -> unsupportedDecl e s
......@@ -287,7 +280,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
| UnsupportedTysymbol (e,s) ->
fprintf fmt "@[<hov 3> This type isn't supported:@\n%a@\n%s@]"
Pretty.print_ts e s
| UnsupportedExpr (e,s) ->
| UnsupportedTerm (e,s) ->
fprintf fmt "@[<hov 3> This expression isn't supported:@\n%a@\n%s@]"
Pretty.print_expr e s
| UnsupportedDecl (d,s) ->
......
......@@ -74,7 +74,7 @@ val syntax_arguments_typed : string -> term pp -> ty pp ->
exception UnsupportedTysymbol of tysymbol * string
exception UnsupportedType of ty * string
exception UnsupportedExpr of expr * string
exception UnsupportedTerm of term * string
exception UnsupportedDecl of decl * string
exception NotImplemented of string
......@@ -82,7 +82,6 @@ val unsupportedTysymbol : tysymbol -> string -> 'a
val unsupportedType : ty -> string -> 'a
val unsupportedTerm : term -> string -> 'a
val unsupportedFmla : fmla -> string -> 'a
val unsupportedExpr : expr -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented : string -> 'a
......@@ -99,7 +98,6 @@ val catch_unsupportedType : (ty -> 'a) -> (ty -> 'a)
- return [f arg] if [f arg] does not raise {!Unsupported} exception
- raise [UnsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)
val catch_unsupportedTysymbol : (tysymbol -> 'a) -> (tysymbol -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedTysymbol]
instead of [UnsupportedType]*)
......@@ -108,14 +106,6 @@ val catch_unsupportedTerm : (term -> 'a) -> (term -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val catch_unsupportedFmla : (fmla -> 'a) -> (fmla -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val catch_unsupportedExpr : (expr -> 'a) -> (expr -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
val catch_unsupportedDecl : (decl -> 'a) -> (decl -> 'a)
(** same as {! catch_unsupportedType} but use [UnsupportedDecl]
instead of [UnsupportedType] *)
......
......@@ -287,6 +287,7 @@ and term_node =
| Ffalse
and fmla = term
and expr = term
and term_bound = vsymbol * bind_info * term
and fmla_bound = term_bound
......@@ -304,17 +305,15 @@ and bind_info = {
and trigger = expr list
and expr =
| Term of term
| Fmla of fmla
(* term and fmla equality *)
let t_equal : term -> term -> bool = (==)
let f_equal = t_equal
let e_equal = t_equal
let t_hash t = t.t_tag
let f_hash = t_hash
let e_hash = t_hash
(* extract the type of a term *)
......@@ -326,7 +325,7 @@ let t_type t = match t.t_ty with
| None -> raise (TermExpected t)
let t_prop f =
if oty_prop f.t_ty then f else raise (FmlaExpected f)
if f.t_ty = None then f else raise (FmlaExpected f)
let check_t_ty o t = match o, t.t_ty with
| Some l, Some r -> check_ty_equal l r
......@@ -336,22 +335,19 @@ let check_t_ty o t = match o, t.t_ty with
(* expr and trigger equality *)
let e_equal e1 e2 = match e1, e2 with
| Term t1, Term t2 -> t_equal t1 t2
| Fmla f1, Fmla f2 -> f_equal f1 f2
| _ -> false
let tr_equal = list_all2 (list_all2 e_equal)
(* expr and trigger traversal *)
let e_map fnT fnF = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f)
let e_fold fnT fnF acc = function Term t -> fnT acc t | Fmla f -> fnF acc f
let e_apply fnT fnF = function Term t -> fnT t | Fmla f -> fnF f
let e_apply fnT fnF e =
if e.t_ty = None then fnF e else fnT e
let e_map_fold fnT fnF acc = function
| Term t -> let acc, t = fnT acc t in acc, Term t
| Fmla f -> let acc, f = fnF acc f in acc, Fmla f
let e_map = e_apply
let e_fold fnT fnF acc e =
if e.t_ty = None then fnF acc e else fnT acc e
let e_map_fold = e_fold
let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))
......@@ -421,8 +417,6 @@ module Hsterm = Hashcons.Make (struct
let t_hash_branch (p,b,t) =
Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
let e_hash = function Term t -> t_hash t | Fmla f -> f_hash f
let f_hash_quant (vl,b,tl,f) =
let h = bnd_hash b (f_hash f) in
let h = Hashcons.combine_list vs_hash h vl in
......@@ -1059,7 +1053,7 @@ let f_map_sign fnT fnF sign f = f_label_copy f (match f.t_node with
else f_implies (f_or f1n f2n) (f_and f1p f2p)
| Fnot f1 ->
f_not (fnF (not sign) f1)
| Tif (f1, f2, f3) when oty_prop f.t_ty ->
| Tif (f1, f2, f3) when f.t_ty = None ->
let f1p = fnF sign f1 in let f1n = fnF (not sign) f1 in
let f2 = fnF sign f2 in let f3 = fnF sign f3 in
if f_equal f1p f1n then f_if f1p f2 f3 else if sign
......@@ -1141,9 +1135,7 @@ let rec list_map_cont fnL contL = function
| [] ->
contL []
let e_map_cont fnT fnF contE = function
| Term t -> fnT (fun t -> contE (Term t)) t
| Fmla f -> fnF (fun f -> contE (Fmla f)) f
let e_map_cont = e_fold
let tr_map_cont fnT fnF =
list_map_cont (list_map_cont (e_map_cont fnT fnF))
......
......@@ -150,6 +150,7 @@ and term_node = private
| Ffalse
and fmla = term
and expr = term
and term_bound
and fmla_bound = term_bound
......@@ -160,10 +161,6 @@ and fmla_branch = term_branch
and term_quant
and fmla_quant = term_quant
and expr =
| Term of term
| Fmla of fmla
and trigger = expr list
module Mterm : Map.S with type key = term
......@@ -182,6 +179,7 @@ val tr_equal : trigger list -> trigger list -> bool
val t_hash : term -> int
val f_hash : fmla -> int
val e_hash : expr -> int
(** close bindings *)
......@@ -321,7 +319,7 @@ val f_forall_close_merge : vsymbol list -> fmla -> fmla
(** Expr and trigger traversal *)
val e_map : (term -> term) -> (fmla -> fmla) -> expr -> expr
val e_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> expr -> 'a
val e_fold : ('a -> term -> 'b) -> ('a -> fmla -> 'b) -> 'a -> expr -> 'b
val e_apply : (term -> 'a) -> (fmla -> 'a) -> expr -> 'a
val e_map_fold : ('a -> term -> 'a * term) ->
......
......@@ -244,8 +244,6 @@ type oty = ty option
exception UnexpectedProp
let oty_ty = function Some ty -> ty | None -> raise UnexpectedProp
let oty_prop = (=) None
let oty_value = (<>) None
let oty_equal = Util.option_eq ty_equal
let oty_hash = Util.option_apply 1 ty_hash
......
......@@ -127,13 +127,10 @@ type oty = ty option
exception UnexpectedProp
val oty_ty : oty -> ty
val oty_prop : oty -> bool
val oty_value : oty -> bool
val oty_equal : oty -> oty -> bool
val oty_hash : oty -> int
val oty_ty : oty -> ty
val oty_map : (ty -> ty) -> oty -> oty
val oty_iter : (ty -> unit) -> oty -> unit
val oty_apply : 'a -> (ty -> 'a) -> oty -> 'a
......
......@@ -244,8 +244,8 @@ and fmla env = function
in
let env, vl = map_fold_left uquant env uqu in
let trigger = function
| TRterm t -> Term (term env t)
| TRfmla f -> Fmla (fmla env f)
| TRterm t -> term env t
| TRfmla f -> fmla env f
in
let trl = List.map (List.map trigger) trl in
f_quant_close q vl trl (fmla env f1)
......@@ -386,8 +386,8 @@ and specialize_fmla_node ~loc htv = function
Fmatch (specialize_term ~loc htv t, List.map branch fbl)
| Term.Tvar _ | Term.Tconst _ | Term.Teps _ -> assert false
and specialize_trigger ~loc htv = function
| Term.Term t -> TRterm (specialize_term ~loc htv t)
| Term.Fmla f -> TRfmla (specialize_fmla ~loc htv f)
and specialize_trigger ~loc htv e = if e.t_ty = None
then TRfmla (specialize_fmla ~loc htv e)
else TRterm (specialize_term ~loc htv e)
......@@ -143,8 +143,8 @@ and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_triggers info fmt tl =
let filter = function
| Term _ -> true
| Fmla {t_node = Tapp (ps,_)} -> not (ls_equal ps ps_equ)
| { t_ty = Some _ } -> true
| { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
| _ -> false in
let tl = List.map (List.filter filter) tl in
let tl = List.filter (function [] -> false | _::_ -> true) tl in
......@@ -179,19 +179,19 @@ let print_logic_decl info fmt (ls,ld) =
(print_option_or_default "prop" (print_type info)) ls.ls_value
| Some ld ->
let vl,e = open_ls_defn ld in
begin match e with
| Term t ->
begin match e.t_ty with
| Some _ ->
(* TODO AC? *)
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n"
print_ident ls.ls_name
(print_list comma (print_logic_binder info)) vl
(print_type info) (Util.of_option ls.ls_value)
(print_term info) t
| Fmla f ->
(print_term info) e
| None ->
fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder info)) vl
(print_fmla info) f
(print_fmla info) e
end;
List.iter forget_var vl
......
......@@ -134,7 +134,7 @@ and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
and print_trigger info fmt = function
| [] -> ()
| [Term ({t_node=Tvar _} as t)] -> fprintf fmt "(MPAT %a)" (print_term info) t
| [{t_node=Tvar _} as t] -> fprintf fmt "(MPAT %a)" (print_term info) t
| [t] -> print_expr info fmt t
| tl -> fprintf fmt "(MPAT %a)" (print_list space (print_expr info)) tl
......
......@@ -205,7 +205,7 @@ let add_indexer (state,task) ts ty csl =
let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
let ix = t_const (ConstInt (string_of_int !index)) in
let ax = f_equ (t_app mt_ls [hd] ty_int) ix in
let ax = f_forall_close (List.rev vl) [[Term hd]] ax in
let ax = f_forall_close (List.rev vl) [[hd]] ax in
add_decl tsk (create_prop_decl Paxiom pr ax)
in
let task = List.fold_left mt_add task csl in
......@@ -220,8 +220,8 @@ let add_discriminator (state,task) ts ty csl =
let t1 = t_app c1 (List.rev_map t_var ul) ty in
let t2 = t_app c2 (List.rev_map t_var vl) ty in
let ax = f_neq t1 t2 in
let ax = f_forall_close (List.rev vl) [[Term t2]] ax in
let ax = f_forall_close (List.rev ul) [[Term t1]] ax in
let ax = f_forall_close (List.rev vl) [[t2]] ax in
let ax = f_forall_close (List.rev ul) [[t1]] ax in
add_decl task (create_prop_decl Paxiom pr ax)
in
let rec dl_add task = function
......
......@@ -82,17 +82,17 @@ let add_ld func pred axl d = match d with
| _, None ->
axl, d
| ls, Some ld ->
let vl,e = open_ls_defn ld in begin match e with
| Term t when func ->
let vl,e = open_ls_defn ld in begin match e.t_ty with
| Some _ when func ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = e_app ls (List.map t_var vl) t.t_ty in
let ax = f_forall_close vl [] (t_insert hd t) in
let hd = e_app ls (List.map t_var vl) e.t_ty in
let ax = f_forall_close vl [] (t_insert hd e) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| Fmla f when pred ->
| None when pred ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = f_app ls (List.map t_var vl) in
let ax = f_forall_close vl [] (f_insert hd f) in
let ax = f_forall_close vl [] (f_insert hd e) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| _ -> axl, d
......@@ -112,9 +112,9 @@ let is_rec = function
| [_, None] -> false
| [ls, Some ld] ->
let _, e = open_ls_defn ld in
begin match e with
| Term t -> t_s_any (const false) (ls_equal ls) t
| Fmla f -> f_s_any (const false) (ls_equal ls) f
begin match e.t_ty with
| Some _ -> t_s_any (const false) (ls_equal ls) e
| None -> f_s_any (const false) (ls_equal ls) e
end
| _ -> true
......
......@@ -72,12 +72,12 @@ let add_ld axl d = match d with
| _, None -> axl, d
| ls, Some ld ->
let vl,e = open_ls_defn ld in
begin match e with
| Term t when has_if t ->
begin match e.t_ty with
| Some _ when has_if e ->
let nm = ls.ls_name.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
let hd = e_app ls (List.map t_var vl) t.t_ty in
let f = f_forall_close vl [] (elim_f (f_equ hd t)) in
let hd = e_app ls (List.map t_var vl) e.t_ty in
let f = f_forall_close vl [] (elim_f (f_equ hd e)) in
create_prop_decl Paxiom pr f :: axl, (ls, None)
| _ ->
axl, make_ls_defn ls vl (e_map elim_t elim_f e)
......
......@@ -104,12 +104,12 @@ module Transform = struct
vs :: vl, Mtv.add v (t_var vs) vm
in
let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
(match expr with
| Term t ->
let t = term_transform varM t in
(match expr.t_ty with
| Some _ ->
let t = term_transform varM expr in
Decl.make_fs_defn new_lsymbol vars t
| Fmla f ->
let f = fmla_transform varM f in
| None ->
let f = fmla_transform varM expr in
Decl.make_ps_defn new_lsymbol vars f)
| (lsymbol, None) ->
(findL lsymbol, None)
......
......@@ -225,12 +225,12 @@ module Transform = struct
| Some ty_value ->
let new_ty = ty_freevars Stv.empty ty_value in
Stv.fold add new_ty (vars,Mtv.empty) in
(match expr with
| Term t ->
let t = term_transform kept varM t in
(match expr.t_ty with
| Some _ ->
let t = term_transform kept varM expr in
Decl.make_fs_defn new_lsymbol vars t
| Fmla f ->
let f = fmla_transform kept varM f in
| None ->
let f = fmla_transform kept varM expr in
Decl.make_ps_defn new_lsymbol vars f)
| (lsymbol, None) ->
(findL lsymbol, None)
......
......@@ -46,10 +46,7 @@ let remove_triggers =
let () = Trans.register_transform "remove_triggers" remove_triggers
let keep_no_predicate = function
| Term _ -> true
| _ -> false
let keep_no_predicate e = e.t_ty <> None
let filter_trigger_no_predicate =
let rt,rf = make_rt_rf keep_no_predicate in
......@@ -60,10 +57,9 @@ let () = Trans.register_transform "filter_trigger_no_predicate"
let keep_no_fmla = function
| Term _ -> true
| Fmla {t_node = Tapp (ps,_)} -> not (ls_equal ps ps_equ)
| _ -> false
| { t_ty = Some _ } -> true
| { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
| _ -> false
let filter_trigger =
let rt,rf = make_rt_rf keep_no_fmla in
......@@ -73,8 +69,8 @@ let () = Trans.register_transform "filter_trigger" filter_trigger
let keep_no_builtin rem_ls = function
| Term _ -> true
| Fmla {t_node = Tapp (ps,_)} -> not (Sls.mem ps rem_ls)
| { t_ty = Some _ } -> true
| { t_node = Tapp (ps,_) } -> not (Sls.mem ps rem_ls)
| _ -> false
......
......@@ -29,24 +29,20 @@ let t_unfold env fs tl ty =
match Mls.find_option fs env with
| None ->
e_app fs tl ty
| Some (vl, Term e) ->
| Some (vl,e) ->
let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl tl in
let mt = oty_match mt e.t_ty ty in
t_ty_subst mt mv e
| _ ->
assert false
let f_unfold env ps tl =
match Mls.find_option ps env with
| None ->
f_app ps tl
| Some (vs, Fmla e) ->
| Some (vs,e) ->
let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
f_ty_subst mt mv e
| _ ->
assert false
(* inline every symbol *)
......@@ -90,9 +86,9 @@ let fold in_goal notdeft notdeff notls d (env, task) =
match d.d_node with
| Dlogic [ls,Some ld] when not (notls ls) ->
let vl,e = open_ls_defn ld in
let inline = match e with
| Term t when notdeft t || t_s_any ffalse (ls_equal ls) t -> false
| Fmla f when notdeff f || f_s_any ffalse (ls_equal ls) f -> false
let inline = match e.t_ty with
| Some _ when notdeft e || t_s_any ffalse (ls_equal ls) e -> false
| None when notdeff e || f_s_any ffalse (ls_equal ls) e -> false
| _ -> true
in
let env = if inline then Mls.add ls (vl,e) env else env in
......
......@@ -58,7 +58,7 @@ let ls_selects_def_of_ts acc ts =
let acc =
let t = t_app ls tvars ty_type in
let f = f_equ (t_app ls_int_of_ty [t] ty_int) (t_int_const id) in
let f = f_forall_close vars [[Term t]] f in
let f = f_forall_close vars [[t]] f in
let prsymbol = create_prsymbol (id_clone ts.ts_name) in
create_prop_decl Paxiom prsymbol f :: acc
in
......@@ -69,7 +69,7 @@ let ls_selects_def_of_ts acc ts =
let t = t_app ls tvars ty_type in
let t = t_app ls_select [t] ty_type in
let f = f_equ t value in
let f = f_forall_close vars [[Term t]] f in
let f = f_forall_close vars [[t]] f in
f)
ls_selects tvars in
let create_props ls_select fmla =
......@@ -241,10 +241,7 @@ let d_monomorph ty_base kept lsmap d =
let vl = List.map (vs_monomorph ty_base kept) ul in
let add acc u v = Mvs.add u (t_var v) acc in
let vmap = List.fold_left2 add Mvs.empty ul vl in
let e = match e with
| Term t -> Term (t_mono vmap t)
| Fmla f -> Fmla (f_mono vmap f)
in
let e = e_fold t_mono f_mono vmap e in
make_ls_defn ls vl e
| None ->
ls, None
......
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