Commit 8527ea1d authored by Andrei Paskevich's avatar Andrei Paskevich

Term: revert the two discussion points from the last commit

- hide the closure variable
- split t_app_beta into t_func_app_beta, which returns terms,
  and t_pred_app_beta which returns formulas

Also:
- check for non-recursivity in t_open_lambda
- implement t_is_lambda via t_open_lambda (less efficient,
  but the correct code without opening would be horrendous)
- drop t_app_lambda, subsumed by t_[func|pred]_app_beta
- support nested lambdas in t_[func|pred]_app_beta
parent 235fac91
......@@ -930,113 +930,6 @@ let t_pred_app pr t = t_equ (t_func_app pr t) t_bool_true
let t_func_app_l fn tl = List.fold_left t_func_app fn tl
let t_pred_app_l pr tl = t_equ (t_func_app_l pr tl) t_bool_true
(* Lambdas *)
let t_lambda id vl trl t =
let ty = Opt.get_def ty_bool t.t_ty in
let add_ty v ty = ty_func v.vs_ty ty in
let ty = List.fold_right add_ty vl ty in
let fc = create_vsymbol id ty in
let copy_loc e = if id.pre_loc = None then e
else t_label ?loc:id.pre_loc e.t_label e in
let mk_t_var v = if v.vs_name.id_loc = None then t_var v
else t_label ?loc:v.vs_name.id_loc Slab.empty (t_var v) in
let add_arg h v = copy_loc (t_func_app h (mk_t_var v)) in
let h = List.fold_left add_arg (mk_t_var fc) vl in
let f = match t.t_ty with
| Some _ -> t_equ h t
| None -> t_iff (copy_loc (t_equ h t_bool_true)) t in
t_eps_close fc (copy_loc (t_forall_close vl trl (copy_loc f)))
let t_lambda id vl trl t =
let t = match t.t_node with
| Tapp (ps,[l;{t_node = Tapp (fs,[])}])
when ls_equal ps ps_equ && ls_equal fs fs_bool_true ->
t_label_copy t l
| _ -> t in
if vl <> [] then t_lambda id vl trl t
else if t.t_ty <> None then t
else t_if t t_bool_true t_bool_false
let t_is_lambda t = match t.t_ty, t.t_node with
| Some {ty_node = Tyapp (ts,_)},
Teps (fc,_,{t_node = Tquant (Tforall,(vl,_,_,f))})
when ts_equal ts ts_func ->
let rec check h vl = match h.t_node, vl with
| Tvar u, [] when vs_equal u fc -> true
| Tapp (fs,[h;{t_node = Tvar u}]), (v::vl)
when ls_equal fs fs_func_app && vs_equal u v -> check h vl
| _ -> false in
let vl = List.rev vl in
begin match f.t_node with
| Tapp (ps,[h;_]) when ls_equal ps ps_equ -> check h vl
| Tbinop (Tiff,{t_node = Tapp (ps,[h;{t_node = Tapp (fs,[])}])},_)
when ls_equal ps ps_equ && ls_equal fs fs_bool_true -> check h vl
| _ -> false
end
| _ -> false
let t_open_lambda t = match t.t_ty, t.t_node with
| Some {ty_node = Tyapp (ts,_)}, Teps fb when ts_equal ts ts_func ->
let fc,f = t_open_bound fb in
let vl,trl,f = match f.t_node with
| Tquant (Tforall,fq) -> t_open_quant fq
| _ -> invalid_arg "Term.t_open_lambda" in
let h,e = match f.t_node with
| Tapp (ps,[h;e]) when ls_equal ps ps_equ -> h, e
| Tbinop (Tiff,{t_node = Tapp (ps,[h;{t_node = Tapp (fs,[])}])},e)
when ls_equal ps ps_equ && ls_equal fs fs_bool_true -> h, e
| _ -> invalid_arg "Term.t_open_lambda" in
let rec check h vl = match h.t_node, vl with
| Tvar u, [] when vs_equal u fc -> ()
| Tapp (fs,[h;{t_node = Tvar u}]), (v::vl)
when ls_equal fs fs_func_app && vs_equal u v -> check h vl
| _ -> invalid_arg "Term.t_open_lambda" in
check h (List.rev vl);
fc, vl, trl, e
| _ -> invalid_arg "Term.t_open_lambda"
let t_open_lambda_cb t =
let fc, vl, trl, e = t_open_lambda t in
let close vl' trl' e' =
if e == e' &&
Lists.equal (Lists.equal ((==) : term -> term -> bool)) trl trl' &&
Lists.equal vs_equal vl vl'
then t else t_lambda (id_clone fc.vs_name) vl' trl' e' in
fc, vl, trl, e, close
let t_closure ls tyl ty =
let mk_v i ty = create_vsymbol (id_fresh ("y" ^ string_of_int i)) ty in
let vl = Lists.mapi mk_v tyl in
let t = t_app ls (List.map t_var vl) ty in
t_lambda (id_clone ls.ls_name) vl [] t
let t_app_partial ls tl tyl ty =
if tyl = [] then t_app ls tl ty else
let tyl = List.fold_right (fun t tyl -> t_type t :: tyl) tl tyl in
t_func_app_l (t_closure ls tyl ty) tl
let t_app_lambda_l lam tl =
if tl = [] then lam else
let fc, vl, trl, e = t_open_lambda lam in
let rec add m vl tl = match vl, tl with
| [], tl ->
t_func_app_l (t_subst_unsafe m e) tl
| vl, [] ->
let trl = List.map (List.map (t_subst_unsafe m)) trl in
t_lambda (id_clone fc.vs_name) vl trl (t_subst_unsafe m e)
| v::vl, t::tl ->
vs_check v t; add (Mvs.add v t m) vl tl in
add Mvs.empty vl tl
let t_app_lambda lam t = t_app_lambda_l lam [t]
let t_app_beta_l lam tl =
if t_is_lambda lam then t_app_lambda_l lam tl
else t_func_app_l lam tl
let t_app_beta lam t = t_app_beta_l lam [t]
(** Term library *)
(* generic map over types, symbols and variables *)
......@@ -1417,6 +1310,111 @@ let t_replace t1 t2 t =
t_ty_check t2 t1.t_ty;
t_replace t1 t2 t
(* lambdas *)
let t_lambda vl trl t =
let ty = Opt.get_def ty_bool t.t_ty in
let add_ty v ty = ty_func v.vs_ty ty in
let ty = List.fold_right add_ty vl ty in
let fc = create_vsymbol (id_fresh "fc") ty in
let copy_loc e = if t.t_loc = None then e
else t_label ?loc:t.t_loc e.t_label e in
let mk_t_var v = if v.vs_name.id_loc = None then t_var v
else t_label ?loc:v.vs_name.id_loc Slab.empty (t_var v) in
let add_arg h v = copy_loc (t_func_app h (mk_t_var v)) in
let h = List.fold_left add_arg (mk_t_var fc) vl in
let f = match t.t_ty with
| Some _ -> t_equ h t
| None -> t_iff (copy_loc (t_equ h t_bool_true)) t in
t_eps_close fc (copy_loc (t_forall_close vl trl (copy_loc f)))
let t_lambda vl trl t =
let t = match t.t_node with
| Tapp (ps,[l;{t_node = Tapp (fs,[])}])
when ls_equal ps ps_equ && ls_equal fs fs_bool_true ->
t_label_copy t l
| _ -> t in
if vl <> [] then t_lambda vl trl t
else if t.t_ty <> None then t
else t_if t t_bool_true t_bool_false
let t_open_lambda t = match t.t_ty, t.t_node with
| Some {ty_node = Tyapp (ts,_)}, Teps fb when ts_equal ts ts_func ->
let fc,f = t_open_bound fb in
let vl,trl,f = match f.t_node with
| Tquant (Tforall,fq) -> t_open_quant fq
| _ -> [], [], t (* fail the next check *) in
let h,e = match f.t_node with
| Tapp (ps,[h;e]) when ls_equal ps ps_equ -> h, e
| Tbinop (Tiff,{t_node = Tapp (ps,[h;{t_node = Tapp (fs,[])}])},e)
when ls_equal ps ps_equ && ls_equal fs fs_bool_true -> h, e
| _ -> t, t (* fail the next check *) in
let rec check h xl = match h.t_node, xl with
| Tapp (fs,[h;{t_node = Tvar u}]), x::xl
when ls_equal fs fs_func_app && vs_equal u x -> check h xl
| Tvar u, [] when vs_equal u fc && t_v_occurs u e = 0 -> vl, trl, e
| _ -> [], [], t in
check h (List.rev vl)
| _ -> [], [], t
(* it is rather tricky to check if a term is a lambda without properly
opening the binders. The deferred substitution in the quantifier
may obscure the closure variable or, on the contrary, introduce it
on the RHS of the definition, making it recursive. We cannot simply
reject such deferred substitutions, because the closure variable is
allowed in the triggers and it can appear there via the deferred
substitution, why not? Therefore, t_is_lambda is a mere shim around
t_open_lambda. *)
let t_is_lambda t = let vl,_,_ = t_open_lambda t in vl <> []
let t_open_lambda_cb t =
let vl, trl, e = t_open_lambda t in
let close vl' trl' e' =
if e == e' &&
Lists.equal (Lists.equal ((==) : term -> term -> bool)) trl trl' &&
Lists.equal vs_equal vl vl'
then t else t_lambda vl' trl' e' in
vl, trl, e, close
let t_closure ls tyl ty =
let mk_v i ty = create_vsymbol (id_fresh ("y" ^ string_of_int i)) ty in
let vl = Lists.mapi mk_v tyl in
let t = t_app ls (List.map t_var vl) ty in
t_lambda vl [] t
let t_app_partial ls tl tyl ty =
if tyl = [] then t_app ls tl ty else
let tyl = List.fold_right (fun t tyl -> t_type t :: tyl) tl tyl in
t_func_app_l (t_closure ls tyl ty) tl
let rec t_app_beta_l lam tl =
let vl, trl, e = t_open_lambda lam in
if vl = [] then t_func_app_l lam tl else
let rec add m vl tl = match vl, tl with
| [], [] ->
t_subst_unsafe m e
| [], tl ->
t_app_beta_l (t_subst_unsafe m e) tl
| vl, [] ->
let trl = List.map (List.map (t_subst_unsafe m)) trl in
t_lambda vl trl (t_subst_unsafe m e)
| v::vl, t::tl ->
vs_check v t; add (Mvs.add v t m) vl tl in
add Mvs.empty vl tl
let t_func_app_beta_l lam tl =
if tl = [] then lam else
let e = t_app_beta_l lam tl in
if e.t_ty = None then t_if e t_bool_true t_bool_false else e
let t_pred_app_beta_l lam tl =
if tl = [] then lam else
let e = t_app_beta_l lam tl in
if e.t_ty = None then e else t_equ e t_bool_true
let t_func_app_beta lam t = t_func_app_beta_l lam [t]
let t_pred_app_beta lam t = t_pred_app_beta_l lam [t]
(* constructors with propositional simplification *)
let keep_on_simp_label = create_label "keep_on_simp"
......
......@@ -308,28 +308,58 @@ val t_pred_app_l : term -> term list -> term (* prop-typed application *)
(** {2 Lambda-term manipulation} *)
val t_lambda : preid -> vsymbol list -> trigger -> term -> term
val t_lambda : vsymbol list -> trigger -> term -> term
(** [t_lambda vl tr e] produces a term [eps f. (forall vl [tr]. f@vl = e)]
or [eps f. (forall vl [tr]. f@vl = True <-> e] if [e] is prop-typed.
If [vl] is empty, [t_lambda] returns [e] or [if e then True else False],
if [e] is prop-typed. *)
val t_open_lambda : term -> vsymbol list * trigger * term
(** [t_open_lambda t] returns a triple [(vl,tr,e)], such that [t] is equal
to [t_lambda vl tr e]. If [t] is not a lambda-term, then [vl] is empty,
[tr] is empty, and [e] is [t]. The term [e] may be prop-typed. *)
val t_open_lambda_cb : term -> vsymbol list * trigger * term *
(vsymbol list -> trigger -> term -> term)
(** the same as [t_open_lambda] but returns additionally an instance of
[t_lambda] that restores the original term if applied to the physically
same arguments. Should be used in mapping functions. *)
val t_is_lambda : term -> bool
val t_open_lambda : term -> vsymbol * vsymbol list * trigger * term
val t_open_lambda_cb :
term -> vsymbol * vsymbol list * trigger * term *
(vsymbol list -> trigger -> term -> term)
(** [t_is_lambda t] returns [true] if [t] is a lambda-term. Do not use
this function if you call [t_open_lambda] afterwards. Internally,
[t_is_lambda] opens binders itself, so you will pay twice the price.
It is better to optimistically call [t_open_lambda] on any [Teps],
and handle the generic case if an empty argument list is returned. *)
val t_closure : lsymbol -> ty list -> ty option -> term
(** [t_closure ls tyl oty] returns a type-instantiated lambda-term
[\xx:tyl.(ls xx : oty)], or [ls : oty] if [ls] is a constant.
The length of [tyl] must be equal to that of [ls.ls_args], and
[oty] should be [None] if and only if [ls] is a predicate symbol. *)
val t_app_partial : lsymbol -> term list -> ty list -> ty option -> term
val t_app_lambda : term -> term -> term (* may return a formula *)
val t_app_beta : term -> term -> term
(* if the first argument is a lambda then execute
[t_app_lambda], otherwise execute [t_func_app] *)
val t_app_lambda_l : term -> term list -> term
val t_app_beta_l : term -> term list -> term
(** [t_app_partial ls tl tyl oty] produces a closure of [ls] and applies
it to [tl] using [t_func_app]. The type signature of the closure is
obtained by prepending the list of types of terms in [tl] to [tyl].
The resulting list must have the same length as [ls.ls_args], and
[oty] should be [None] if and only if [ls] is a predicate symbol.
If the symbol is fully applied ([tyl] is empty), the [Tapp] term
is returned. Otherwise, no beta-reduction is performed, in order
to preserve the closure. *)
val t_func_app_beta : term -> term -> term
(** [t_func_app_beta f a] applies [f] to [a] performing beta-reduction
when [f] is a lambda-term. Always returns a value-typed term, even
if [f] is a lambda-term built on top of a formula. *)
val t_pred_app_beta : term -> term -> term
(** [t_pred_app_beta f a] applies [f] to [a] performing beta-reduction
when [f] is a lambda-term. Always returns a formula, even if [f] is
a lambda-term built on top of a bool-typed term. *)
val t_func_app_beta_l : term -> term list -> term
val t_pred_app_beta_l : term -> term list -> term
(** {2 Term library} *)
......
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