Commit aa51f5fd authored by Andrei Paskevich's avatar Andrei Paskevich

introduce suitable combinators for the expr type

parent 2d3b47ba
......@@ -246,11 +246,9 @@ and print_fbranch fmt br =
and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma print_tr)) tl
(print_list alt (print_list comma print_expr)) tl
and print_tr fmt = function
| Term t -> print_term fmt t
| Fmla f -> print_fmla fmt f
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
(** Declarations *)
......@@ -279,21 +277,18 @@ let print_type_decl fmt (ts,def) = match def with
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
let print_ld fmt ld =
let print_ls_defn fmt ld =
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t -> print_term fmt t
| Fmla f -> print_fmla fmt f
end;
fprintf fmt " =@ %a" print_expr e;
List.iter forget_var vl
let print_ls_defn fmt = option_iter (fprintf fmt " =@ %a" print_ld)
let print_ls_type fmt = option_iter (fprintf fmt " :@ %a" print_ty)
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
let print_logic_decl fmt (ls,ld) =
fprintf fmt "@[<hov 2>logic %a%a%a%a@]"
print_ls ls (print_paren_l print_ty) ls.ls_args
print_ls_type ls.ls_value print_ls_defn ld;
(print_option print_ls_type) ls.ls_value
(print_option print_ls_defn) ld;
forget_tvs ()
let print_ind fmt (pr,f) =
......
......@@ -41,6 +41,7 @@ val print_const : formatter -> constant -> unit (* int/real constant *)
val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_fmla : formatter -> fmla -> unit (* formula *)
val print_expr : formatter -> expr -> unit (* term or formula *)
val print_pkind : formatter -> prop_kind -> unit
......
......@@ -266,15 +266,14 @@ and expr =
and trigger = expr list
(* trigger traversal *)
(* expr and trigger traversal *)
let tr_map fnT fnF =
let fn = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f) in
List.map (List.map fn)
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 tr_fold fnT fnF =
let fn acc = function Term t -> fnT acc t | Fmla f -> fnF acc f in
List.fold_left (List.fold_left fn)
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))
module T = struct
......
......@@ -211,7 +211,11 @@ val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla
(* trigger traversal *)
(* 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_apply : (term -> 'a) -> (fmla -> 'a) -> expr -> 'a
val tr_map : (term -> term) ->
(fmla -> fmla) -> trigger list -> trigger list
......
......@@ -70,9 +70,8 @@ let make_ps_defn ps vl f =
let pd = f_forall vl [] (f_iff hd f) in
ps, vl, Fmla f, check_fvs pd
let make_ls_defn ls vl = function
| Term t -> make_fs_defn ls vl t
| Fmla f -> make_ps_defn ls vl f
let make_ls_defn ls vl =
e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
let extract_ls_defn f =
let vl, ef = f_open_forall f in
......
......@@ -128,11 +128,9 @@ let rec print_fmla drv fmt f = match f.f_node with
| Fcase _ ->
assert false
and print_trigger drv fmt = function
| Term t -> (print_term drv) fmt t
| Fmla f -> (print_fmla drv) fmt f
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
and print_triggers drv fmt tl = print_list comma (print_trigger drv) fmt tl
and print_triggers drv fmt tl = print_list comma (print_expr drv) fmt tl
let print_logic_binder drv fmt v =
......@@ -150,22 +148,6 @@ let print_type_decl drv fmt = function
let ac_th = ["algebra";"AC"]
let print_ld drv fmt ld =
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t -> print_term drv fmt t
| Fmla f -> print_fmla drv fmt f
end;
List.iter forget_var vl
let print_ls_defn drv fmt =
Util.option_iter (fprintf fmt " =@ %a" (print_ld drv))
let print_ls_type drv fmt = function
| Some ty -> print_type drv fmt ty
| None -> fprintf fmt "prop"
let print_logic_decl drv ctxt fmt (ls,ld) =
match Driver.query_ident drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
......@@ -176,7 +158,7 @@ let print_logic_decl drv ctxt fmt (ls,ld) =
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
sac print_ident ls.ls_name
(print_list comma (print_type drv)) ls.ls_args
(print_ls_type drv) ls.ls_value
(print_option_or_default "prop" (print_type drv)) ls.ls_value
| Some ld ->
let _,vl,e = open_ls_defn ld in
begin match e with
......@@ -188,7 +170,7 @@ let print_logic_decl drv ctxt fmt (ls,ld) =
(print_type drv) (Util.of_option ls.ls_value)
(print_term drv) t
| Fmla f ->
fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_fmla drv) f
......
......@@ -248,11 +248,9 @@ and print_fbranch drv fmt br =
and print_tl drv fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma (print_tr drv))) tl
(print_list alt (print_list comma (print_expr drv))) tl
and print_tr drv fmt = function
| Term t -> print_term drv fmt t
| Fmla f -> print_fmla drv fmt f
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
(** Declarations *)
......@@ -281,21 +279,18 @@ let print_type_decl drv fmt (ts,def) = match def with
let print_type_decl drv fmt d = print_type_decl drv fmt d; forget_tvs ()
let print_ld drv fmt ld =
let print_ls_defn drv fmt ld =
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t -> print_term drv fmt t
| Fmla f -> print_fmla drv fmt f
end;
fprintf fmt " =@ %a" (print_expr drv) e;
List.iter forget_var vl
let print_ls_defn drv fmt = option_iter (fprintf fmt " =@ %a" (print_ld drv))
let print_ls_type drv fmt = option_iter (fprintf fmt " :@ %a" (print_ty drv))
let print_ls_type drv fmt = fprintf fmt " :@ %a" (print_ty drv)
let print_logic_decl drv fmt (ls,ld) =
fprintf fmt "@[<hov 2>logic %a%a%a%a@]"
print_ls ls (print_paren_l (print_ty drv)) ls.ls_args
(print_ls_type drv) ls.ls_value (print_ls_defn drv) ld;
(print_option (print_ls_type drv)) ls.ls_value
(print_option (print_ls_defn drv)) ld;
forget_tvs ()
let print_ind drv fmt (pr,f) =
......
......@@ -95,15 +95,12 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
(List.map (fun (ps,fmlal) -> ps, List.map
(fun (pr,f) -> pr, replacep env f) fmlal) dl))
| Dlogic dl ->
let replacee = function
| Term t -> Term (replacet env t)
| Fmla f -> Fmla (replacep env f)
in
env,
add_decl ctxt (create_logic_decl
(List.map (fun (ls,ld) -> ls, Util.option_map (fun ld ->
let _,vs,e = open_ls_defn ld in
make_ls_defn ls vs (replacee e)) ld) dl))
let e = e_map (replacet env) (replacep env) e in
make_ls_defn ls vs e) ld) dl))
| Dtype dl -> env,add_decl ctxt d
| Dprop (k,pr,f) ->
env,add_decl ctxt (create_prop_decl k pr (replacep env f))
......
......@@ -169,17 +169,14 @@ let identity =
clear = (fun () -> ()); }
let rewrite_elt rt rf d =
let re = function
| Term t -> Term (rt t)
| Fmla f -> Fmla (rf f)
in
match d.d_node with
| Dtype _ -> [d]
| Dlogic l -> [create_logic_decl (List.map
(function
| (ls,Some def) ->
let (ls,vsl,expr) = open_ls_defn def in
(ls,Some (make_ls_defn ls vsl (re expr)))
let expr = e_map rt rf expr in
(ls,Some (make_ls_defn ls vsl expr))
| l -> l) l)]
| Dind indl -> [create_ind_decl
(List.map (fun (ls,pl) -> ls,
......
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