Commit f2575d8b authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Support reification of quantifiers

parent 4bd34e25
......@@ -587,6 +587,7 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
=
let n = a.rows in
let m = a.columns in
(* print n; print m; *)
let rec find_nonz (i j:int)
requires { 0 <= i <= n }
requires { 0 <= j < m }
......@@ -745,7 +746,6 @@ let rec predicate valid_ctx' (ctx:context')
let rec simp (e:expr') : expr
ensures { forall y z. interp result y z = interp' e y z }
ensures { valid_expr' e -> valid_expr result }
(* raises { NonLinear -> true }*)
raises { C.Unknown -> true }
variant { e }
=
......@@ -766,21 +766,6 @@ let rec simp (e:expr') : expr
| Coeff c -> Cst c
| ProdL e c | ProdR c e ->
mul_expr (simp e) (simp_c c)
(* | Prod (Var n) (Coeff c) -> Term c n
| Prod (Coeff c) (Var n) -> Term c n
| Prod (Coeff c1) (Coeff c2) -> Cst (C.mul c1 c2)
| Prod e1 e2 ->
let e1 = simp e1 in
let e2 = simp e2 in
match e1, e2 with
| Cst c1, Cst c2 -> Cst (C.mul c1 c2)
| Cst c1, Term c2 v | Term c2 v, Cst c1
-> Term (C.mul c1 c2) v
| Cst c, Add e1 e2 | Add e1 e2, Cst c ->
Add (mul_expr e1 c) (mul_expr e2 c)
| _ -> raise NonLinear; absurd
end *)
(*w/o absurd : type mismatch between () and expr in clone export 200 lines down ? *)
end
let simp_eq (eq:equality') : equality
......@@ -1496,10 +1481,7 @@ let mp_decision (l: context') (g: equality') : bool
requires { valid_eq' g }
ensures { forall y z. result -> pos_ctx' l z -> pos_eq' g z
-> interp_ctx' l g y z }
raises { R.Absurd -> true }
(* raises { R.NonLinear -> true } *)
raises { Unknown -> true }
raises { Q.Unknown -> true }
raises { R.Absurd -> true | Unknown -> true | Q.Unknown -> true }
=
R.decision (m_ctx l) (m_eq g)
......@@ -1545,4 +1527,49 @@ goal g: forall x y z: int.
y - z = 0 ->
x = 0
end
module Fmla
use import map.Map
use import int.Int
type value
constant dummy : value
predicate foo value
function add value value : value
type term = Val int | Add term term
type fmla = Forall fmla | Foo term
function interp_term (t:term) (b:int->value) : value =
match t with
| Val n -> b n
| Add t1 t2 -> add (interp_term t1 b) (interp_term t2 b)
end
function interp_fmla (f:fmla) (l:int) (b:int->value) : bool =
match f with
| Foo t -> foo (interp_term t b)
| Forall f -> forall v. interp_fmla f (l-1) b[l <- v]
end
function interp (f:fmla) (b: int -> value) : bool =
interp_fmla f (-1) b
let f (f:fmla) : bool
ensures { result -> forall b. interp f b }
= false
end
module TestFmla
use import Fmla
goal g:
forall a: value.
((forall x. forall y. foo (add x (add (add a dummy) y))) = True)
end
\ No newline at end of file
......@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
......@@ -1132,7 +1132,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true">
......@@ -1142,24 +1142,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true">
......@@ -1190,10 +1190,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.28" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.29" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true">
......@@ -1230,10 +1230,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.41" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
......@@ -1316,19 +1316,19 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.70" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.71" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.72" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -2832,7 +2832,24 @@
<theory name="Test2" sum="a38588d68003a039cb5d43eb15d507d6">
<goal name="g">
<transf name="reflection_f" arg1="int_decision">
<goal name="g.0" expl="reification check">
<goal name="g.0" expl="reification check" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="g.1">
</goal>
</transf>
</goal>
</theory>
<theory name="Fmla" proved="true" sum="8647779672ac66d512da2e0faec50ac9">
<goal name="VC f" expl="VC for f" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="TestFmla" sum="0859686c2acb7a6b6ce7336b34e3e29c">
<goal name="g">
<transf name="reflection_f" arg1="f">
<goal name="g.0" expl="reification check" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="g.1">
</goal>
......
......@@ -1440,7 +1440,7 @@ module N
invariant { (!rp).offset = r.offset + !i }
invariant { plength !rp = plength r }
invariant { pelts !rp = pelts r }
invariant { 0 <= !c <= 1 }
invariant { 0 <= !c <= 1 } (*TODO c=0*)
variant { sz - !i }
label StartLoop in
value_concat r !i (!i + sz);
......@@ -4525,7 +4525,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
assert { power radix sy
= power radix (sy - 2) * radix * radix };
assert { xp0 + radix * xp1
+ power radix 2 * !x1 at StartLoop (* radix * radix *)
+ radix * radix * !x1 at StartLoop
- !ql * (dl + radix * dh)
= rl + radix * rh };
begin ensures { value (xd at SubProd) sy
......
......@@ -9,7 +9,7 @@
<prover id="4" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mp2.mlw" proved="true">
<theory name="N" proved="true" sum="327068fd34ba69f640d394e074d7a998">
<theory name="N" proved="true" sum="4300fab5dcda41829bcbffedf4250d9f">
<goal name="VC map_eq_shift" expl="VC for map_eq_shift" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC map_eq_shift.0" expl="postcondition" proved="true">
......@@ -9485,25 +9485,10 @@
<proof prover="2" memlimit="2000"><result status="valid" time="0.81"/></proof>
</goal>
<goal name="VC div_sb_qr.150" expl="assertion" proved="true">
<transf name="replace" proved="true" arg1="(power radix 2)" arg2="(radix * radix)">
<goal name="VC div_sb_qr.150.0" expl="assertion" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC div_sb_qr.150.0.0" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC div_sb_qr.150.0.0.0" expl="assertion" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC div_sb_qr.150.1" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
<proof prover="2" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC div_sb_qr.151" expl="assertion" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="1.27"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="VC div_sb_qr.152" expl="assertion" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.19"/></proof>
......@@ -9548,7 +9533,7 @@
</goal>
<goal name="VC div_sb_qr.154.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.18"/></proof>
<proof prover="2" memlimit="2000"><result status="valid" time="0.38"/></proof>
<proof prover="2" memlimit="2000"><result status="valid" time="0.24"/></proof>
</goal>
</transf>
</goal>
......
......@@ -9,7 +9,9 @@ exception NoReification
exception Exit of string
let debug = false
let do_trans = true
(* automatically perform helpful transformations to prove side conditions, set to false for debugging *)
let print_id fmt id = Format.fprintf fmt "%s" id.id_string
let expl_reification_check = Ident.create_label "expl:reification check"
......@@ -24,6 +26,8 @@ type reify_env = { kn: known_map;
ty_to_map: vsymbol Mty.t;
env: Env.env;
task: Task.task;
bound_vars: Svs.t; (* bound variables, do not map them in a var map*)
bound_fr: int; (* separate, negative index for bound vars*)
}
let init_renv kn crc lv env task =
......@@ -37,6 +41,8 @@ let init_renv kn crc lv env task =
ty_to_map = Mty.empty;
env = env;
task = task;
bound_vars = Svs.empty;
bound_fr = -1;
}
let rec reify_term renv t rt =
......@@ -56,20 +62,54 @@ let rec reify_term renv t rt =
| _ -> false in
if debug then Format.printf "use_interp %a: %b@." Pretty.print_term t r;
r in
let add_to_maps renv vyl =
let var_maps, ty_to_map =
List.fold_left
(fun (var_maps, ty_to_map) vy ->
if Mty.mem vy.vs_ty ty_to_map
then (Mvs.add vy vy.vs_ty var_maps, ty_to_map)
else (Mvs.add vy vy.vs_ty var_maps,
Mty.add vy.vs_ty vy ty_to_map))
(renv.var_maps, renv.ty_to_map)
(List.map
(fun t -> match t.t_node with Tvar vy -> vy | _ -> assert false)
vyl)
in
{ renv with var_maps = var_maps; ty_to_map = ty_to_map }
in
let open Theory in
let th_list = Env.read_theory renv.env ["list"] "List" in
let ty_list = ns_find_ts th_list.th_export ["list"] in
let compat_h t rt =
match t.t_node, rt.t_node with
| Tapp (ls1,_), Tapp(ls2, _) -> ls_equal ls1 ls2
| Tquant (Tforall, _), Tquant (Tforall, _)
| Tquant (Texists, _), Tquant (Texists, _)-> true
| _ -> false in
let is_eq_true t = match t.t_node with
| Tapp (eq, [_; tr])
when ls_equal eq ps_equ && t_equal tr t_bool_true -> true
| _ -> false in
let lhs_eq_true t = match t.t_node with
| Tapp (eq, [t; tr])
when ls_equal eq ps_equ && t_equal tr t_bool_true -> t
| _ -> assert false in
let rec invert_nonvar_pat vl (renv:reify_env) (p,f) t =
if debug
then Format.printf
"invert_nonvar_pat p %a f %a t %a@."
Pretty.print_pat p Pretty.print_term f Pretty.print_term t;
if is_eq_true f && not (is_eq_true t)
then invert_nonvar_pat vl renv (p, lhs_eq_true f) t else
match p.pat_node, f.t_node, t.t_node with
| Pwild , _, _ | Pvar _,_,_ when t_equal_nt_nl f t ->
if debug then Format.printf "case equal@.";
renv, t
| Papp (cs, pl), Tapp(ls1, _), Tapp(ls2, _)
when ls_equal ls1 ls2
| Papp (cs, pl), _,_
when compat_h f t
&& Svs.for_all (fun v -> t_v_occurs v f = 1) p.pat_vars
&& List.for_all is_pvar pl
(* could remove this with a bit more work in term reconstruction *)
(* could remove this with a bit more work in term reconstruction *)
->
if debug then Format.printf "case app@.";
let rec rt_of_var svs f t v (renv, acc) =
......@@ -90,6 +130,13 @@ let rec reify_term renv t rt =
else aux l1 l2
| _ -> assert false in
aux la1 la2
| Tquant (Tforall, tq1), Tquant (Tforall, tq2)
| Tquant (Texists, tq1), Tquant (Texists, tq2) ->
let _, _, t1 = t_open_quant tq1 in
let vl, _, t2 = t_open_quant tq2 in
let bv = List.fold_left Svs.add_left renv.bound_vars vl in
let renv = { renv with bound_vars = bv } in
rt_of_var svs t1 t2 v (renv, acc)
| _ -> raise NoReification
in
let rec check_nonvar f t =
......@@ -137,6 +184,15 @@ let rec reify_term renv t rt =
renv, acc))
(renv,None) la1 la2 in
renv, Opt.get rt
| Pvar v, Tquant(Tforall, tq1), Tquant(Tforall, tq2)
| Pvar v, Tquant(Texists, tq1), Tquant(Texists, tq2)
when t_v_occurs v f = 1 ->
if debug then Format.printf "case quant_var@.";
let _,_,t1 = t_open_quant tq1 in
let vl,_,t2 = t_open_quant tq2 in
let bv = List.fold_left Svs.add_left renv.bound_vars vl in
let renv = { renv with bound_vars = bv } in
invert_nonvar_pat vl renv (p, t1) t2
| Por (p1, p2), _, _ ->
if debug then Format.printf "case or@.";
begin try invert_pat vl renv (p1, f) t
......@@ -207,11 +263,20 @@ let rec reify_term renv t rt =
else
begin
if debug then Format.printf "%a is new@." Pretty.print_term t;
let fr = renv.fr in
let vy = Mty.find vy.vs_ty renv.ty_to_map in
let store = Mterm.add t (vy, fr) renv.store in
let renv = { renv with store = store; fr = fr + 1 } in
(renv, app_pat (t_nat_const fr))
let bound = match t.t_node with
| Tvar v -> Svs.mem v renv.bound_vars
| _ -> false in
let renv, i=
if bound
then let i = renv.bound_fr in
{ renv with bound_fr = i-1 }, i
else
let vy = Mty.find vy.vs_ty renv.ty_to_map in
let fr = renv.fr in
let store = Mterm.add t (vy, fr) renv.store in
{ renv with store = store; fr = fr + 1 }, fr in
let const = Number.(ConstInt (int_const_of_int i)) in
(renv, app_pat (t_const const Ty.ty_int))
end
| _ -> raise NoReification
and invert_pat vl renv (p,f) t =
......@@ -234,7 +299,7 @@ let rec reify_term renv t rt =
Pretty.print_ty (Opt.get t.t_ty);
raise NoReification
end
and invert_interp renv ls (t:term) = (*la ?*)
and invert_interp renv ls (t:term) =
let ld = try Opt.get (find_logic_definition renv.kn ls)
with _ ->
if debug
......@@ -265,6 +330,9 @@ let rec reify_term renv t rt =
with NoReification ->
if debug then Format.printf "match failed@."; aux invert l in
(try aux invert_nonvar_pat bl with NoReification -> aux invert_var_pat bl)
| Tapp (ls', _) ->
if debug then Format.printf "case app@.";
invert_interp renv ls' t
| _ -> if debug then Format.printf "function body not handled@.";
if debug then Format.printf "f: %a@." Pretty.print_term f;
raise NoReification
......@@ -282,10 +350,7 @@ let rec reify_term renv t rt =
and invert_ctx_body renv ls vl f t l g =
match f.t_node with
| Tcase ({t_node = Tvar v}, [tbn; tbc] ) when vs_equal v (List.hd vl) ->
let open Theory in
let th_list = Env.read_theory renv.env ["list"] "List" in
let ty_g = g.vs_ty in
let ty_list = ns_find_ts th_list.th_export ["list"] in
let ty_list_g = ty_app ty_list [ty_g] in
if (not (ty_equal ty_list_g l.vs_ty))
then (if debug
......@@ -348,21 +413,6 @@ let rec reify_term renv t rt =
| _ -> if debug then Format.printf "not a match on list@.";
raise NoReification
in
let add_to_maps renv vyl =
let var_maps, ty_to_map =
List.fold_left
(fun (var_maps, ty_to_map) vy ->
if Mty.mem vy.vs_ty ty_to_map
then (Mvs.add vy vy.vs_ty var_maps, ty_to_map)
else (Mvs.add vy vy.vs_ty var_maps,
Mty.add vy.vs_ty vy ty_to_map))
(renv.var_maps, renv.ty_to_map)
(List.map
(fun t -> match t.t_node with Tvar vy -> vy | _ -> assert false)
vyl)
in
{ renv with var_maps = var_maps; ty_to_map = ty_to_map }
in
if debug then Format.printf "reify_term t %a rt %a@."
Pretty.print_term t Pretty.print_term rt;
if not (oty_equal t.t_ty rt.t_ty)
......@@ -391,6 +441,7 @@ let rec reify_term renv t rt =
reify_term (reify_term renv t1 rt1) t2 rt2
| _, Tapp(eq,[{t_node=Tapp(interp, {t_node = Tvar l}::{t_node = Tvar g}::vyl)}; tr])
when ls_equal eq ps_equ && t_equal tr t_bool_true
&& ty_equal (ty_app ty_list [g.vs_ty]) l.vs_ty
&& List.mem l renv.lv
&& List.mem g renv.lv
&& List.for_all
......@@ -402,6 +453,14 @@ let rec reify_term renv t rt =
if debug then Format.printf "case context@.";
let renv = add_to_maps renv vyl in
invert_ctx_interp renv interp t l g
| Tbinop(Tiff,t,{t_node=Ttrue}), Tapp(eq,[{t_node=Tapp(interp, {t_node = Tvar f}::vyl)}; tr])
when ls_equal eq ps_equ && t_equal tr t_bool_true
&& t.t_ty=None ->
if debug then Format.printf "case interp_fmla@.";
if debug then Format.printf "t %a rt %a@." Pretty.print_term t Pretty.print_term rt;
let renv = add_to_maps renv vyl in
let renv, rf = invert_interp renv interp t in
{ renv with subst = Mvs.add f rf renv.subst }
| _ -> if debug then Format.printf "no reify_term match@.";
if debug then Format.printf "lv = [%a]@."
(Pp.print_list Pp.space Pretty.print_vs)
......@@ -493,29 +552,34 @@ let build_goals prev prs subst env lp g rt =
with _ ->
if debug then Format.printf "no cut found@.";
let t = Trans.apply (Ind_itp.revert_tr_symbol [Tsprsymbol hr]) task_r in
let t = Trans.apply compute_in_goal t in
match t with
| [t] ->
let rewrite pr = Apply.rewrite None false pr None in
let lt, prs =
if do_trans
then
let t = Trans.apply compute_in_goal t in
match t with
| [t] ->
let rewrite pr = Apply.rewrite None false pr None in
let lt, prs =
List.fold_left
(fun (acc, f) pr ->
try (Lists.apply (Trans.apply (rewrite pr)) acc,f)
with _ -> acc, pr::f)
([t],[]) prs in
(* for the prs that failed once, trying again seems to work ? *)
List.fold_left
(fun (acc, f) pr ->
try (Lists.apply (Trans.apply (rewrite pr)) acc,f)
with _ -> acc, pr::f)
([t],[]) prs in
(* for the prs that failed once, trying again seems to work ? *)
List.fold_left
(fun acc pr ->
try Lists.apply (Trans.apply (rewrite pr)) acc
with _ -> acc)
lt (List.rev prs)
| [] -> []
| _ -> assert false in
(fun acc pr ->
try Lists.apply (Trans.apply (rewrite pr)) acc
with _ -> acc)
lt (List.rev prs)
| [] -> []
| _ -> assert false
else [t] in
let lt = List.map (fun ng -> Task.add_decl prev
(create_prop_decl Pgoal (create_prsymbol (id_fresh "G")) ng))
inst_lp in
let lt = Lists.apply (Trans.apply compute_in_goal) lt in
let lt = if do_trans
then Lists.apply (Trans.apply compute_in_goal) lt
else lt in
if debug then Format.printf "done@.";
ltask_r@lt
......
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