diff --git a/src/interpretation.ml b/src/interpretation.ml
index fe84a10acc9e9f2bbb92f11f21c518cdfd90f2f8..bcb91a37fe910b9b6ae5e4fc0d99472f87cb91bd 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -48,12 +48,12 @@ type caisar_env = {
let ls_of_caisar_op engine op ty_args ty =
let caisar_env = CRE.user_env engine in
- Fmt.pr "ls_of_caisar_op: %a@." pp_caisar_op op;
- Option.iter ty ~f:(Fmt.pr "ty: %a@." Pretty.print_ty);
+ (* Fmt.pr "ls_of_caisar_op: %a@." pp_caisar_op op; *)
+ (* Option.iter ty ~f:(Fmt.pr "ty: %a@." Pretty.print_ty); *)
Hashtbl.find_or_add caisar_env.ls_of_caisar_op op ~default:(fun () ->
let id = Ident.id_fresh "caisar_op" in
let ls = Term.create_lsymbol id ty_args ty in
- Fmt.pr "ls: %a@." Pretty.print_ls ls;
+ (* Fmt.pr "ls: %a@." Pretty.print_ls ls; *)
Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
Term.Hls.add caisar_env.caisar_op_of_ls ls op;
ls)
@@ -99,15 +99,15 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
(* Vector *)
let vget : _ CRE.builtin =
fun engine ls vl ty ->
- Fmt.pr "--@.vget: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ (* Fmt.pr "--@.vget: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [
- Term ({ t_node = Tapp (lsapp, _); _ } as t1);
- Term ({ t_node = Tconst (ConstInt i); _ } as t2);
+ Term ({ t_node = Tapp (lsapp, _); _ } as _t1);
+ Term ({ t_node = Tconst (ConstInt i); _ } as _t2);
] -> (
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
match caisar_op_of_ls engine lsapp with
| Dataset (DS_csv csv) ->
let row = List.nth_exn csv (Number.to_small_integer i) in
@@ -130,15 +130,15 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| [
Term ({ t_node = Tapp _; _ } as t1); Term ({ t_node = Tvar _; _ } as t2);
] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
let length : _ CRE.builtin =
- fun engine ls vl ty ->
- Fmt.pr "--@.length: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ fun engine ls vl _ty ->
+ (* Fmt.pr "--@.length: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [ Term { t_node = Tapp (ls, []); _ } ] -> (
match caisar_op_of_ls engine ls with
@@ -149,64 +149,64 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
(* Tensor *)
let tget : _ CRE.builtin =
- fun engine ls vl ty ->
- Fmt.pr "--@.tget: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ fun engine ls vl _ty ->
+ (* Fmt.pr "--@.tget: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [
- Term ({ t_node = Tapp (ls1, tl1); _ } as t1);
- Term ({ t_node = Tapp (ls2, _); _ } as t2);
+ Term ({ t_node = Tapp (ls1, tl1); _ } as _t1);
+ Term ({ t_node = Tapp (ls2, _); _ } as _t2);
] -> (
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
| Tensor n, Index (I_csv i) ->
assert (i <= n);
Term (List.nth_exn tl1 i)
| _ -> assert false)
| [ Term t1; Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
let tminus : _ CRE.builtin =
fun engine ls vl ty ->
- Fmt.pr "--@.tminus: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ (* Fmt.pr "--@.tminus: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [
- Term ({ t_node = Tapp (ls1, tl1); _ } as t1);
- Term ({ t_node = Tapp (ls2, _); _ } as t2);
+ Term ({ t_node = Tapp (ls1, tl1); _ } as _t1);
+ Term ({ t_node = Tapp (ls2, _); _ } as _t2);
] -> (
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
- | Tensor n, Data (D_csv d) ->
- assert (n = List.length d);
- let data_ty =
+ | Tensor n, Data (D_csv data) ->
+ assert (n = List.length data);
+ let ty_cst =
match ty with
| Some { ty_node = Tyapp (_, [ ty ]); _ } -> ty
| _ -> assert false
in
- let data_cst =
- List.map d ~f:(fun d ->
+ let csts =
+ List.map data ~f:(fun d ->
let cst = const_real_of_float (Float.of_string d) in
- Term.t_const cst data_ty)
+ Term.t_const cst ty_cst)
in
let minus =
- (* TODO: generalize wrt [data_ty]. *)
+ (* TODO: generalize wrt the type of constants [csts]. *)
let { env; _ } = CRE.user_env engine in
let th = Env.read_theory env [ "ieee_float" ] "Float64" in
Theory.(ns_find_ls th.th_export [ Ident.op_infix ".-" ])
in
let args =
- List.map2_exn tl1 data_cst ~f:(fun tl c ->
- (Term.t_app_infer minus [ tl; c ], data_ty))
+ List.map2_exn tl1 csts ~f:(fun tl c ->
+ (Term.t_app_infer minus [ tl; c ], ty_cst))
in
Term (term_of_caisar_op ~args engine (Tensor n) ty)
| _ -> assert false)
| [ Term t1; Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
@@ -214,9 +214,9 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
(* Classifier *)
let read_classifier : _ CRE.builtin =
fun engine ls vl ty ->
- Fmt.pr "--@.read_classifier: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ (* Fmt.pr "--@.read_classifier: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [
Term { t_node = Tconst (ConstStr classifier); _ };
@@ -231,16 +231,13 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| _ -> invalid_arg (error_message ls)
in
let apply_classifier : _ CRE.builtin =
- fun _engine ls vl ty ->
- Fmt.pr "--@.apply_classifier: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ fun _engine ls vl _ty ->
+ (* Fmt.pr "--@.apply_classifier: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
- | [ Term ({ t_node = Tvar _; _ } as t1); Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
- Term (Term.t_app_infer ls [ t1; t2 ])
- | [ Term ({ t_node = Tapp (_lsapp, _); _ } as t1); Term t2 ] ->
- Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2;
+ | [ Term t1; Term t2 ] ->
+ (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
Term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
@@ -248,9 +245,9 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
(* Dataset *)
let read_dataset : _ CRE.builtin =
fun engine ls vl ty ->
- Fmt.pr "--@.read_dataset: ls:%a , ty:%a@." Pretty.print_ls ls
- Fmt.(option ~none:nop Pretty.print_ty)
- ty;
+ (* Fmt.pr "--@.read_dataset: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.(option ~none:nop Pretty.print_ty) *)
+ (* ty; *)
match vl with
| [
Term { t_node = Tconst (ConstStr dataset); _ };
@@ -293,9 +290,11 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
| Tapp
( { ls_name = { id_string = "equal_shape"; _ }; _ },
[
- ({ t_node = Tapp (ls, _); _ } as t1); ({ t_node = Tvar vs2; _ } as t2);
+ ({ t_node = Tapp (ls, _); _ } as _t1);
+ ({ t_node = Tvar vs2; _ } as _t2);
] ) ->
- Fmt.pr "--@.equal_shape: %a %a@." Pretty.print_term t1 Pretty.print_term t2;
+ (* Fmt.pr "--@.equal_shape: %a %a@." Pretty.print_term t1 Pretty.print_term
+ t2; *)
if not (Term.vs_equal vs vs2)
then None
else
@@ -311,7 +310,7 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
in
let new_quant =
List.init n ~f:(fun _ ->
- let preid = Ident.id_fresh "caisar_es" in
+ let preid = Ident.id_fresh "caisar_v" in
Term.create_vsymbol preid ty)
in
let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
@@ -322,24 +321,22 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
| Tapp
( { ls_name = { id_string = "valid_index"; _ }; _ },
[
- ({ t_node = Tapp (ls, _); _ } as t1); ({ t_node = Tvar vs2; _ } as t2);
- ] ) ->
- Fmt.pr "--@.valid_index: %a %a@." Pretty.print_term t1 Pretty.print_term t2;
+ ({ t_node = Tapp (ls, _); _ } as _t1);
+ ({ t_node = Tvar vs2; _ } as _t2);
+ ] ) -> (
if not (Term.vs_equal vs vs2)
then None
else
- let n =
- match caisar_op_of_ls engine ls with
- | Tensor d -> d
- | _ -> assert false
- | exception _ -> 5
- in
- let new_quant = [] in
- let substitutions =
- List.init n ~f:(fun i ->
- term_of_caisar_op engine (Index (I_csv i)) (Some vs.vs_ty))
- in
- Some { new_quant; substitutions }
+ match caisar_op_of_ls engine ls with
+ | Tensor n ->
+ let new_quant = [] in
+ let substitutions =
+ List.init n ~f:(fun i ->
+ term_of_caisar_op engine (Index (I_csv i)) (Some vs.vs_ty))
+ in
+ Some { new_quant; substitutions }
+ | _ -> assert false
+ | exception _ -> None)
| _ -> None
let interpret_task ~cwd env task =
@@ -357,7 +354,7 @@ let interpret_task ~cwd env task =
CRE.create ~bounded_quant params env known_map caisar_env builtin_caisar
in
let f = Task.task_goal_fmla task in
- Fmt.pr "TERM: %a@." Pretty.print_term f;
+ (* Fmt.pr "TERM: %a@." Pretty.print_term f; *)
let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
f print_caisar_op caisar_env
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index 0f2c68326f6ff8ea79eb1370dc045ab2a8eb5d44..6d30617057aaa65b729bdcec368739681c76894d 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -35,14 +35,14 @@ type params = {
}
type bounded_quant_result = {
- new_quant: vsymbol list;
+ new_quant : vsymbol list;
substitutions : term list;
}
type 'a builtin = 'a engine -> lsymbol -> value list -> Ty.ty option -> value
-and 'a bounded_quant = 'a engine -> vsymbol -> cond:term ->
- bounded_quant_result option
+and 'a bounded_quant =
+ 'a engine -> vsymbol -> cond:term -> bounded_quant_result option
and 'a engine = {
env : Env.env;
@@ -113,11 +113,11 @@ let is_one v =
let eval_int_op op simpl _ ls l ty =
match l with
| [ t1; t2 ] -> (
- try
- let n1 = big_int_of_value t1 in
- let n2 = big_int_of_value t2 in
- Int (op n1 n2)
- with NotNum | Division_by_zero -> simpl ls t1 t2 ty)
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Int (op n1 n2)
+ with NotNum | Division_by_zero -> simpl ls t1 t2 ty)
| _ -> assert false
let simpl_add _ls t1 t2 _ty =
@@ -156,22 +156,22 @@ let simpl_minmax _ls v1 v2 _ty =
let eval_int_rel op _ _ls l _ty =
match l with
| [ t1; t2 ] -> (
- try
- let n1 = big_int_of_value t1 in
- let n2 = big_int_of_value t2 in
- Term (to_bool (op n1 n2))
- with NotNum | Division_by_zero ->
- raise Undetermined (* t_app_value ls l ty *))
+ try
+ let n1 = big_int_of_value t1 in
+ let n2 = big_int_of_value t2 in
+ Term (to_bool (op n1 n2))
+ with NotNum | Division_by_zero ->
+ raise Undetermined (* t_app_value ls l ty *))
| _ -> assert false
let eval_int_uop op _ _ls l _ty =
match l with
| [ t1 ] -> (
- try
- let n1 = big_int_of_value t1 in
- Int (op n1)
- with NotNum | Division_by_zero ->
- raise Undetermined (* t_app_value ls l ty *))
+ try
+ let n1 = big_int_of_value t1 in
+ Int (op n1)
+ with NotNum | Division_by_zero ->
+ raise Undetermined (* t_app_value ls l ty *))
| _ -> assert false
let real_align ~pow2 ~pow5 r =
@@ -184,43 +184,43 @@ let real_align ~pow2 ~pow5 r =
let eval_real_op op simpl _ ls l ty =
match l with
| [ t1; t2 ] -> (
- try
- let n1 = real_of_value t1 in
- let n2 = real_of_value t2 in
- Real (op n1 n2)
- with NotNum -> simpl ls t1 t2 ty)
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ Real (op n1 n2)
+ with NotNum -> simpl ls t1 t2 ty)
| _ -> assert false
let eval_real_uop op _ _ls l _ty =
match l with
| [ t1 ] -> (
- try
- let n1 = real_of_value t1 in
- Real (op n1)
- with NotNum -> raise Undetermined)
+ try
+ let n1 = real_of_value t1 in
+ Real (op n1)
+ with NotNum -> raise Undetermined)
| _ -> assert false
let eval_real_rel op _ _ls l _ty =
let open Number in
match l with
| [ t1; t2 ] -> (
- try
- let n1 = real_of_value t1 in
- let n2 = real_of_value t2 in
- let s1, s2 =
- let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = n1 in
- let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = n2 in
- if BigInt.sign s1 <> BigInt.sign s2
- then (s1, s2)
- else
- let pow2 = BigInt.min p21 p22 in
- let pow5 = BigInt.min p51 p52 in
- let s1 = real_align ~pow2 ~pow5 n1 in
- let s2 = real_align ~pow2 ~pow5 n2 in
- (s1, s2)
- in
- Term (to_bool (op s1 s2))
- with NotNum -> raise Undetermined (* t_app_value ls l ty *))
+ try
+ let n1 = real_of_value t1 in
+ let n2 = real_of_value t2 in
+ let s1, s2 =
+ let { rv_sig = s1; rv_pow2 = p21; rv_pow5 = p51 } = n1 in
+ let { rv_sig = s2; rv_pow2 = p22; rv_pow5 = p52 } = n2 in
+ if BigInt.sign s1 <> BigInt.sign s2
+ then (s1, s2)
+ else
+ let pow2 = BigInt.min p21 p22 in
+ let pow5 = BigInt.min p51 p52 in
+ let s1 = real_align ~pow2 ~pow5 n1 in
+ let s2 = real_align ~pow2 ~pow5 n2 in
+ (s1, s2)
+ in
+ Term (to_bool (op s1 s2))
+ with NotNum -> raise Undetermined (* t_app_value ls l ty *))
| _ -> assert false
let real_0 = Number.real_value BigInt.zero
@@ -323,10 +323,10 @@ let simpl_real_pow _ls t1 _t2 _ty =
let real_from_int _ _ls l _ty =
match l with
| [ t ] -> (
- try
- let n = big_int_of_value t in
- Real (Number.real_value n)
- with NotNum -> raise Undetermined)
+ try
+ let n = big_int_of_value t in
+ Real (Number.real_value n)
+ with NotNum -> raise Undetermined)
| _ -> assert false
type 'a built_in_theories =
@@ -336,7 +336,7 @@ type 'a built_in_theories =
* (string * lsymbol ref option * 'a builtin) list
let built_in_theories : unit -> 'a built_in_theories list =
- fun () ->
+ fun () ->
[
(* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
eval_false ; ] ; *)
@@ -401,14 +401,14 @@ let add_builtin_th env ((l, n, t, d) : 'a built_in_theories) =
let th = Env.read_theory env.env l n in
List.iter
(fun (id, r) ->
- let ts = Theory.ns_find_ts th.Theory.th_export [ id ] in
- r ts)
+ let ts = Theory.ns_find_ts th.Theory.th_export [ id ] in
+ r ts)
t;
List.iter
(fun (id, r, f) ->
- let ls = Theory.ns_find_ls th.Theory.th_export [ id ] in
- Hls.add env.builtins ls f;
- match r with None -> () | Some r -> r := ls)
+ let ls = Theory.ns_find_ls th.Theory.th_export [ id ] in
+ Hls.add env.builtins ls f;
+ match r with None -> () | Some r -> r := ls)
d
let get_builtins env built_in_user =
@@ -461,7 +461,7 @@ type cont =
type config = {
value_stack : value list;
cont_stack : (cont * term) list;
- (* second term is the original term, for attribute and loc copy *)
+ (* second term is the original term, for attribute and loc copy *)
}
(* This global variable is used to approximate a count of the elementary
@@ -476,22 +476,22 @@ let rec pattern_renaming (bound_vars, mt) p1 p2 =
match (p1.pat_node, p2.pat_node) with
| Pwild, Pwild -> (bound_vars, mt)
| Pvar v1, Pvar v2 -> (
- try
- let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
- let bound_vars = Mvs.add v2 v1 bound_vars in
- (bound_vars, mt)
- with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ (bound_vars, mt)
+ with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
| Papp (ls1, tl1), Papp (ls2, tl2) when ls_equal ls1 ls2 ->
List.fold_left2 pattern_renaming (bound_vars, mt) tl1 tl2
| Por (p1a, p1b), Por (p2a, p2b) ->
let bound_vars, mt = pattern_renaming (bound_vars, mt) p1a p2a in
pattern_renaming (bound_vars, mt) p1b p2b
| Pas (p1, v1), Pas (p2, v2) -> (
- try
- let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
- let bound_vars = Mvs.add v2 v1 bound_vars in
- pattern_renaming (bound_vars, mt) p1 p2
- with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
+ try
+ let mt = Ty.ty_match mt v1.vs_ty v2.vs_ty in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ pattern_renaming (bound_vars, mt) p1 p2
+ with Ty.TypeMismatch _ -> raise (NoMatchpat (Some (p1, p2))))
| _ -> raise (NoMatchpat (Some (p1, p2)))
let first_order_matching (vars : Svs.t) (largs : term list) (args : term list) :
@@ -500,121 +500,121 @@ let first_order_matching (vars : Svs.t) (largs : term list) (args : term list) :
match (largs, args) with
| [], [] -> sigma
| t1 :: r1, t2 :: r2 -> (
- (* Format.eprintf "matching terms %a and %a...@." Pretty.print_term t1
- Pretty.print_term t2; *)
- match t1.t_node with
- | Tvar vs when Svs.mem vs vars -> (
+ (* Format.eprintf "matching terms %a and %a...@." Pretty.print_term t1
+ Pretty.print_term t2; *)
+ match t1.t_node with
+ | Tvar vs when Svs.mem vs vars -> (
+ try
+ let t = Mvs.find vs mv in
+ if t_equal t t2
+ then loop bound_vars sigma r1 r2
+ else raise (NoMatch (Some (t1, t2, Some t)))
+ with Not_found -> (
+ try
+ let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
+ let fv2 = t_vars t2 in
+ if Mvs.is_empty (Mvs.set_inter bound_vars fv2)
+ then loop bound_vars (ts, Mvs.add vs t2 mv) r1 r2
+ else raise (NoMatch (Some (t1, t2, None)))
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))))
+ | Tapp (ls1, args1) -> (
+ match t2.t_node with
+ | Tapp (ls2, args2) when ls_equal ls1 ls2 -> (
+ let mt, mv =
+ loop bound_vars sigma (List.rev_append args1 r1)
+ (List.rev_append args2 r2)
+ in
+ try (Ty.oty_match mt t1.t_ty t2.t_ty, mv)
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None))))
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tquant (q1, bv1) -> (
+ match t2.t_node with
+ | Tquant (q2, bv2) when q1 = q2 ->
+ let vl1, _tl1, term1 = t_open_quant bv1 in
+ let vl2, _tl2, term2 = t_open_quant bv2 in
+ let bound_vars, term1, mt =
try
- let t = Mvs.find vs mv in
- if t_equal t t2
- then loop bound_vars sigma r1 r2
- else raise (NoMatch (Some (t1, t2, Some t)))
- with Not_found -> (
- try
- let ts = Ty.ty_match mt vs.vs_ty (t_type t2) in
- let fv2 = t_vars t2 in
- if Mvs.is_empty (Mvs.set_inter bound_vars fv2)
- then loop bound_vars (ts, Mvs.add vs t2 mv) r1 r2
- else raise (NoMatch (Some (t1, t2, None)))
- with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))))
- | Tapp (ls1, args1) -> (
- match t2.t_node with
- | Tapp (ls2, args2) when ls_equal ls1 ls2 -> (
- let mt, mv =
- loop bound_vars sigma (List.rev_append args1 r1)
- (List.rev_append args2 r2)
- in
- try (Ty.oty_match mt t1.t_ty t2.t_ty, mv)
- with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None))))
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tquant (q1, bv1) -> (
- match t2.t_node with
- | Tquant (q2, bv2) when q1 = q2 ->
- let vl1, _tl1, term1 = t_open_quant bv1 in
- let vl2, _tl2, term2 = t_open_quant bv2 in
- let bound_vars, term1, mt =
- try
- List.fold_left2
- (fun (bound_vars, term1, mt) e1 e2 ->
- let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
- let bound_vars = Mvs.add e2 e1 bound_vars in
- (bound_vars, term1, mt))
- (bound_vars, term1, mt) vl1 vl2
- with Invalid_argument _ | Ty.TypeMismatch _ ->
- raise (NoMatch (Some (t1, t2, None)))
- in
- loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tbinop (b1, t1_l, t1_r) -> (
- match t2.t_node with
- | Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
- loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tif (t11, t12, t13) -> (
- match t2.t_node with
- | Tif (t21, t22, t23) ->
- loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
- (t21 :: t22 :: t23 :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tlet (td1, tb1) -> (
- match t2.t_node with
- | Tlet (td2, tb2) ->
- let v1, tl1 = t_open_bound tb1 in
- let v2, tl2 = t_open_bound tb2 in
- let mt =
- try Ty.ty_match mt v1.vs_ty v2.vs_ty
- with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
- in
- let bound_vars = Mvs.add v2 v1 bound_vars in
- loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tcase (ts1, tbl1) -> (
- match t2.t_node with
- | Tcase (ts2, tbl2) -> (
- try
- let bound_vars, mt, l1, l2 =
- List.fold_left2
- (fun (bound_vars, mt, l1, l2) tb1 tb2 ->
- let p1, tb1 = t_open_branch tb1 in
- let p2, tb2 = t_open_branch tb2 in
- let bound_vars, mt =
- pattern_renaming (bound_vars, mt) p1 p2
- in
- (bound_vars, mt, tb1 :: l1, tb2 :: l2))
- (bound_vars, mt, ts1 :: r1, ts2 :: r2)
- tbl1 tbl2
+ List.fold_left2
+ (fun (bound_vars, term1, mt) e1 e2 ->
+ let mt = Ty.ty_match mt e1.vs_ty e2.vs_ty in
+ let bound_vars = Mvs.add e2 e1 bound_vars in
+ (bound_vars, term1, mt))
+ (bound_vars, term1, mt) vl1 vl2
+ with Invalid_argument _ | Ty.TypeMismatch _ ->
+ raise (NoMatch (Some (t1, t2, None)))
+ in
+ loop bound_vars (mt, mv) (term1 :: r1) (term2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tbinop (b1, t1_l, t1_r) -> (
+ match t2.t_node with
+ | Tbinop (b2, t2_l, t2_r) when b1 = b2 ->
+ loop bound_vars (mt, mv) (t1_l :: t1_r :: r1) (t2_l :: t2_r :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tif (t11, t12, t13) -> (
+ match t2.t_node with
+ | Tif (t21, t22, t23) ->
+ loop bound_vars (mt, mv) (t11 :: t12 :: t13 :: r1)
+ (t21 :: t22 :: t23 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tlet (td1, tb1) -> (
+ match t2.t_node with
+ | Tlet (td2, tb2) ->
+ let v1, tl1 = t_open_bound tb1 in
+ let v2, tl2 = t_open_bound tb2 in
+ let mt =
+ try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
+ in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: tl1 :: r1) (td2 :: tl2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tcase (ts1, tbl1) -> (
+ match t2.t_node with
+ | Tcase (ts2, tbl2) -> (
+ try
+ let bound_vars, mt, l1, l2 =
+ List.fold_left2
+ (fun (bound_vars, mt, l1, l2) tb1 tb2 ->
+ let p1, tb1 = t_open_branch tb1 in
+ let p2, tb2 = t_open_branch tb2 in
+ let bound_vars, mt =
+ pattern_renaming (bound_vars, mt) p1 p2
in
- loop bound_vars (mt, mv) l1 l2
- with Invalid_argument _ -> raise (NoMatch (Some (t1, t2, None))))
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Teps tb1 -> (
- match t2.t_node with
- | Teps tb2 ->
- let v1, td1 = t_open_bound tb1 in
- let v2, td2 = t_open_bound tb2 in
- let mt =
- try Ty.ty_match mt v1.vs_ty v2.vs_ty
- with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
- in
- let bound_vars = Mvs.add v2 v1 bound_vars in
- loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tnot t1 -> (
- match t2.t_node with
- | Tnot t2 -> loop bound_vars sigma (t1 :: r1) (t2 :: r2)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | Tvar v1 -> (
- match t2.t_node with
- | Tvar v2 -> (
- try
- if vs_equal v1 (Mvs.find v2 bound_vars)
- then loop bound_vars sigma r1 r2
- else raise (NoMatch (Some (t1, t2, None)))
- with Not_found -> assert false)
- | _ -> raise (NoMatch (Some (t1, t2, None))))
- | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
- loop bound_vars sigma r1 r2
- | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2, None))))
+ (bound_vars, mt, tb1 :: l1, tb2 :: l2))
+ (bound_vars, mt, ts1 :: r1, ts2 :: r2)
+ tbl1 tbl2
+ in
+ loop bound_vars (mt, mv) l1 l2
+ with Invalid_argument _ -> raise (NoMatch (Some (t1, t2, None))))
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Teps tb1 -> (
+ match t2.t_node with
+ | Teps tb2 ->
+ let v1, td1 = t_open_bound tb1 in
+ let v2, td2 = t_open_bound tb2 in
+ let mt =
+ try Ty.ty_match mt v1.vs_ty v2.vs_ty
+ with Ty.TypeMismatch _ -> raise (NoMatch (Some (t1, t2, None)))
+ in
+ let bound_vars = Mvs.add v2 v1 bound_vars in
+ loop bound_vars (mt, mv) (td1 :: r1) (td2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tnot t1 -> (
+ match t2.t_node with
+ | Tnot t2 -> loop bound_vars sigma (t1 :: r1) (t2 :: r2)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | Tvar v1 -> (
+ match t2.t_node with
+ | Tvar v2 -> (
+ try
+ if vs_equal v1 (Mvs.find v2 bound_vars)
+ then loop bound_vars sigma r1 r2
+ else raise (NoMatch (Some (t1, t2, None)))
+ with Not_found -> assert false)
+ | _ -> raise (NoMatch (Some (t1, t2, None))))
+ | (Tconst _ | Ttrue | Tfalse) when t_equal t1 t2 ->
+ loop bound_vars sigma r1 r2
+ | Tconst _ | Ttrue | Tfalse -> raise (NoMatch (Some (t1, t2, None))))
| _ -> raise (NoMatch None)
in
loop Mvs.empty (Ty.Mtv.empty, Mvs.empty) largs args
@@ -628,10 +628,10 @@ let one_step_reduce engine ls args =
match rules with
| [] -> raise Irreducible
| (vars, largs, rhs) :: rem -> (
- try
- let sigma = first_order_matching vars largs args in
- (sigma, rhs)
- with NoMatch _ -> loop rem)
+ try
+ let sigma = first_order_matching vars largs args in
+ (sigma, rhs)
+ with NoMatch _ -> loop rem)
in
loop rules
with Not_found -> raise Irreducible
@@ -641,17 +641,17 @@ let rec matching ((mt, mv) as sigma) t p =
| Pwild -> sigma
| Pvar v -> (mt, Mvs.add v t mv)
| Por (p1, p2) -> (
- try matching sigma t p1 with NoMatch _ -> matching sigma t p2)
+ try matching sigma t p1 with NoMatch _ -> matching sigma t p2)
| Pas (p, v) -> matching (mt, Mvs.add v t mv) t p
| Papp (ls1, pl) -> (
- match t.t_node with
- | Tapp (ls2, tl) ->
- if ls_equal ls1 ls2
- then List.fold_left2 matching sigma tl pl
- else if ls2.ls_constr > 0
- then raise (NoMatch None)
- else raise Undetermined
- | _ -> raise Undetermined)
+ match t.t_node with
+ | Tapp (ls2, tl) ->
+ if ls_equal ls1 ls2
+ then List.fold_left2 matching sigma tl pl
+ else if ls2.ls_constr > 0
+ then raise (NoMatch None)
+ else raise Undetermined
+ | _ -> raise Undetermined)
let rec extract_first n acc l =
if n = 0
@@ -668,26 +668,26 @@ let bounds ls_lt t1 t2 =
let lt order = function
(* match [i < vs] or [vs < i], return [i, vs] *)
| { t_node = Tapp (ls, [ t1; t2 ]) } when ls_equal ls ls_lt -> (
- assert (Ty.(ty_equal (t_type t1) ty_int && ty_equal (t_type t2) ty_int));
- match order t1 t2 with
- | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
- { t_node = Tvar vs } ) ->
- (i, vs)
- | _ -> raise Exit)
+ assert (Ty.(ty_equal (t_type t1) ty_int && ty_equal (t_type t2) ty_int));
+ match order t1 t2 with
+ | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
+ { t_node = Tvar vs } ) ->
+ (i, vs)
+ | _ -> raise Exit)
| _ -> raise Exit
in
let eq order = function
(* match [i = vs] or [vs = i], return [i, vs] *)
| { t_node = Tapp (ls, [ t1; t2 ]) }
when ls_equal ls Term.ps_equ
- && Ty.ty_equal (t_type t1) Ty.ty_int
- && Ty.ty_equal (t_type t2) Ty.ty_int -> (
- match order t1 t2 with
- | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
- { t_node = Tvar vs } )
- when Ty.ty_equal vs.vs_ty Ty.ty_int ->
- (i, vs)
- | _ -> raise Exit)
+ && Ty.ty_equal (t_type t1) Ty.ty_int
+ && Ty.ty_equal (t_type t2) Ty.ty_int -> (
+ match order t1 t2 with
+ | ( { t_node = Tconst (Constant.ConstInt { Number.il_int = i }) },
+ { t_node = Tvar vs } )
+ when Ty.ty_equal vs.vs_ty Ty.ty_int ->
+ (i, vs)
+ | _ -> raise Exit)
| _ -> raise Exit
in
let le order = function
@@ -723,9 +723,9 @@ let bounds ls_lt t1 t2 =
TODO:
- - expand to bounded quantifications on range values
- - compatiblity with reverse direction (forall i. b > i > a -> t)
- - detect SPARK-style [forall i. if a < i /\ i < b then t else true] *)
+ - expand to bounded quantifications on range values
+ - compatiblity with reverse direction (forall i. b > i > a -> t)
+ - detect SPARK-style [forall i. if a < i /\ i < b then t else true] *)
let reduce_bounded_quant engine ls_lt limit t sigma st rem =
match (st, rem) with
(* st = a < vs < b :: _; rem = -> :: forall vs :: _ *)
@@ -734,7 +734,7 @@ let reduce_bounded_quant engine ls_lt limit t sigma st rem =
:: (Kquant ((Tforall as quant), [ vs ], _), _)
:: rem
| (Kbinop Tand, _) :: (Kquant ((Texists as quant), [ vs ], _), _) :: rem
- ) )
+ ) )
when Ty.ty_equal vs.vs_ty Ty.ty_int ->
let t_empty, binop =
match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
@@ -760,78 +760,78 @@ let reduce_bounded_quant engine ls_lt limit t sigma st rem =
in
{ value_stack = st; cont_stack = loop rem b }
| ( Term cond :: st,
- ( (Kbinop Timplies, _)
- :: (Kquant ((Tforall as quant), [ vs ], _), t_orig)
- :: rem ))-> (
- match engine.bounded_quant engine vs ~cond with
- | None -> raise Exit
- | Some res ->
- let t_empty, binop =
- match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
- in
- let rem = match res.new_quant with [] -> rem | _ ->
- (Kquant ((quant, res.new_quant, [])),t_orig)::rem
- in
- let rec loop rem = function
- | [] -> rem
- | t_i::l ->
- let rem =
- match l with [] -> rem | _ ->
- (* conjunction *)
- (Kbinop binop, t_true) :: rem
- in
- let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
- loop rem l
- in
- match res.substitutions with
- | [] ->
- { value_stack = Term t_empty :: st; cont_stack = rem }
- | _ ->
- { value_stack = st; cont_stack = loop rem res.substitutions
- }
- )
+ (Kbinop Timplies, _)
+ :: (Kquant ((Tforall as quant), [ vs ], _), t_orig)
+ :: rem ) -> (
+ match engine.bounded_quant engine vs ~cond with
+ | None -> raise Exit
+ | Some res -> (
+ let t_empty, binop =
+ match quant with Tforall -> (t_true, Tand) | Texists -> (t_false, Tor)
+ in
+ let rem =
+ match res.new_quant with
+ | [] -> rem
+ | _ -> (Kquant (quant, res.new_quant, []), t_orig) :: rem
+ in
+ let rec loop rem = function
+ | [] -> rem
+ | t_i :: l ->
+ let rem =
+ match l with
+ | [] -> rem
+ | _ ->
+ (* conjunction *)
+ (Kbinop binop, t_true) :: rem
+ in
+ let rem = (Keval (t, Mvs.add vs t_i sigma), t_true) :: rem in
+ loop rem l
+ in
+ match res.substitutions with
+ | [] -> { value_stack = Term t_empty :: st; cont_stack = rem }
+ | _ -> { value_stack = st; cont_stack = loop rem res.substitutions }))
| _ -> raise Exit
let rec reduce engine c =
match (c.value_stack, c.cont_stack) with
| _, [] -> assert false
| st, (Keval (t, sigma), orig) :: rem -> (
- let limit = engine.params.compute_max_quantifier_domain in
- try reduce_bounded_quant engine engine.ls_lt limit t sigma st rem
- with Exit -> reduce_eval engine st t ~orig sigma rem)
+ let limit = engine.params.compute_max_quantifier_domain in
+ try reduce_bounded_quant engine engine.ls_lt limit t sigma st rem
+ with Exit -> reduce_eval engine st t ~orig sigma rem)
| [], (Kif _, _) :: _ -> assert false
| v :: st, (Kif (t2, t3, sigma), orig) :: rem -> (
- match v with
- | Term { t_node = Ttrue } ->
- incr rec_step_limit;
- {
- value_stack = st;
- cont_stack = (Keval (t2, sigma), t_attr_copy orig t2) :: rem;
- }
- | Term { t_node = Tfalse } ->
+ match v with
+ | Term { t_node = Ttrue } ->
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t2, sigma), t_attr_copy orig t2) :: rem;
+ }
+ | Term { t_node = Tfalse } ->
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t3, sigma), t_attr_copy orig t3) :: rem;
+ }
+ | Term t1 -> (
+ match (t1.t_node, t2.t_node, t3.t_node) with
+ | ( Tapp (ls, [ b0; { t_node = Tapp (ls1, _) } ]),
+ Tapp (ls2, _),
+ Tapp (ls3, _) )
+ when ls_equal ls ps_equ && ls_equal ls1 fs_bool_true
+ && ls_equal ls2 fs_bool_true && ls_equal ls3 fs_bool_false ->
incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b0) :: st; cont_stack = rem }
+ | _ ->
{
- value_stack = st;
- cont_stack = (Keval (t3, sigma), t_attr_copy orig t3) :: rem;
- }
- | Term t1 -> (
- match (t1.t_node, t2.t_node, t3.t_node) with
- | ( Tapp (ls, [ b0; { t_node = Tapp (ls1, _) } ]),
- Tapp (ls2, _),
- Tapp (ls3, _) )
- when ls_equal ls ps_equ && ls_equal ls1 fs_bool_true
- && ls_equal ls2 fs_bool_true && ls_equal ls3 fs_bool_false ->
- incr rec_step_limit;
- { value_stack = Term (t_attr_copy orig b0) :: st; cont_stack = rem }
- | _ ->
- {
- value_stack =
- Term
- (t_attr_copy orig (t_if t1 (t_subst sigma t2) (t_subst sigma t3)))
- :: st;
- cont_stack = rem;
- })
- | Int _ | Real _ -> assert false (* would be ill-typed *))
+ value_stack =
+ Term
+ (t_attr_copy orig (t_if t1 (t_subst sigma t2) (t_subst sigma t3)))
+ :: st;
+ cont_stack = rem;
+ })
+ | Int _ | Real _ -> assert false (* would be ill-typed *))
| [], (Klet _, _) :: _ -> assert false
| t1 :: st, (Klet (v, t2, sigma), orig) :: rem ->
incr rec_step_limit;
@@ -843,7 +843,6 @@ let rec reduce engine c =
| [], (Kcase _, _) :: _ -> assert false
| (Int _ | Real _) :: _, (Kcase _, _) :: _ -> assert false
| Term t1 :: st, (Kcase (tbl, sigma), orig) :: rem ->
- Fmt.pr "reduce_match@%a@." Pretty.print_term t1;
reduce_match st t1 ~orig tbl sigma rem
| ( ([] | [ _ ] | (Int _ | Real _) :: _ | Term _ :: (Int _ | Real _) :: _),
(Kbinop _, _) :: _ ) ->
@@ -883,26 +882,26 @@ and reduce_match st u ~orig tbl sigma cont =
match tbl with
| [] -> assert false (* pattern matching not exhaustive *)
| b :: rem -> (
- let p, t = t_open_branch b in
- try
- let mt', mv' = matching (Ty.Mtv.empty, sigma) u p in
- (* Format.eprintf "Pattern-matching succeeded:@\nmt' = @["; Ty.Mtv.iter
- (fun tv ty -> Format.eprintf "%a -> %a," Pretty.print_tv tv
- Pretty.print_ty ty) mt'; Format.eprintf "@]@\n"; Format.eprintf "mv'
- = @["; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
- Pretty.print_vs v Pretty.print_term t) mv'; Format.eprintf "@]@.";
- Format.eprintf "branch before inst: %a@." Pretty.print_term t; *)
- let mv'', t = t_subst_types mt' mv' t in
- (* Format.eprintf "branch after types inst: %a@." Pretty.print_term t;
- Format.eprintf "mv'' = @["; Mvs.iter (fun v t -> Format.eprintf "%a
- -> %a," Pretty.print_vs v Pretty.print_term t) mv''; Format.eprintf
- "@]@."; *)
- incr rec_step_limit;
- {
- value_stack = st;
- cont_stack = (Keval (t, mv''), t_attr_copy orig t) :: cont;
- }
- with NoMatch _ -> iter rem)
+ let p, t = t_open_branch b in
+ try
+ let mt', mv' = matching (Ty.Mtv.empty, sigma) u p in
+ (* Format.eprintf "Pattern-matching succeeded:@\nmt' = @["; Ty.Mtv.iter
+ (fun tv ty -> Format.eprintf "%a -> %a," Pretty.print_tv tv
+ Pretty.print_ty ty) mt'; Format.eprintf "@]@\n"; Format.eprintf "mv'
+ = @["; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t) mv'; Format.eprintf "@]@.";
+ Format.eprintf "branch before inst: %a@." Pretty.print_term t; *)
+ let mv'', t = t_subst_types mt' mv' t in
+ (* Format.eprintf "branch after types inst: %a@." Pretty.print_term t;
+ Format.eprintf "mv'' = @["; Mvs.iter (fun v t -> Format.eprintf "%a
+ -> %a," Pretty.print_vs v Pretty.print_term t) mv''; Format.eprintf
+ "@]@."; *)
+ incr rec_step_limit;
+ {
+ value_stack = st;
+ cont_stack = (Keval (t, mv''), t_attr_copy orig t) :: cont;
+ }
+ with NoMatch _ -> iter rem)
in
try iter tbl
with Undetermined ->
@@ -921,43 +920,43 @@ and reduce_eval eng st t ~orig sigma rem =
let orig = t_attr_copy orig t in
match t.t_node with
| Tvar v -> (
- match Ident.Mid.find v.vs_name eng.known_map with
- | Decl.{ d_node = Dlogic dl } ->
+ match Ident.Mid.find v.vs_name eng.known_map with
+ | Decl.{ d_node = Dlogic dl } ->
+ incr rec_step_limit;
+ let _, ls_defn =
+ List.find
+ (fun (ls, _) ->
+ String.equal ls.ls_name.Ident.id_string v.vs_name.Ident.id_string)
+ dl
+ in
+ let vs, t = Decl.open_ls_defn ls_defn in
+ let aux vs t =
+ (* Create ε fc. λ vs. fc @ vs = t to make the value from known_map
+ compatible to reduce_func_app *)
+ let ty = Opt.get t.t_ty in
+ let app_ty = Ty.ty_func vs.vs_ty ty in
+ let fc = create_vsymbol (Ident.id_fresh "fc") app_ty in
+ t_eps
+ (t_close_bound fc
+ (t_quant Tforall
+ (t_close_quant [ vs ] []
+ (t_app ps_equ
+ [ t_app fs_func_app [ t_var fc; t_var vs ] (Some ty); t ]
+ None))))
+ in
+ let t = List.fold_right aux vs t in
+ { value_stack = Term t :: st; cont_stack = rem }
+ | _ -> assert false
+ | exception Not_found -> (
+ match Mvs.find v sigma with
+ | t ->
incr rec_step_limit;
- let _, ls_defn =
- List.find
- (fun (ls, _) ->
- String.equal ls.ls_name.Ident.id_string v.vs_name.Ident.id_string)
- dl
- in
- let vs, t = Decl.open_ls_defn ls_defn in
- let aux vs t =
- (* Create ε fc. λ vs. fc @ vs = t to make the value from known_map
- compatible to reduce_func_app *)
- let ty = Opt.get t.t_ty in
- let app_ty = Ty.ty_func vs.vs_ty ty in
- let fc = create_vsymbol (Ident.id_fresh "fc") app_ty in
- t_eps
- (t_close_bound fc
- (t_quant Tforall
- (t_close_quant [ vs ] []
- (t_app ps_equ
- [ t_app fs_func_app [ t_var fc; t_var vs ] (Some ty); t ]
- None))))
- in
- let t = List.fold_right aux vs t in
- { value_stack = Term t :: st; cont_stack = rem }
- | _ -> assert false
- | exception Not_found -> (
- match Mvs.find v sigma with
- | t ->
- incr rec_step_limit;
- { value_stack = Term (t_attr_copy orig t) :: st; cont_stack = rem }
- | exception Not_found ->
- (* this may happen, e.g when computing below a quantified formula *)
- (* Format.eprintf "Tvar not found: %a@." Pretty.print_vs v; assert
- false *)
- { value_stack = Term orig :: st; cont_stack = rem }))
+ { value_stack = Term (t_attr_copy orig t) :: st; cont_stack = rem }
+ | exception Not_found ->
+ (* this may happen, e.g when computing below a quantified formula *)
+ (* Format.eprintf "Tvar not found: %a@." Pretty.print_vs v; assert
+ false *)
+ { value_stack = Term orig :: st; cont_stack = rem }))
| Tif (t1, t2, t3) ->
{
value_stack = st;
@@ -1013,15 +1012,15 @@ and reduce_app engine st ls ~orig ty rem_cont =
then
match st with
| t2 :: t1 :: rem_st -> (
- try reduce_equ ~orig rem_st t1 t2 rem_cont
- with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
+ try reduce_equ ~orig rem_st t1 t2 rem_cont
+ with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
| _ -> assert false
else if ls_equal ls fs_func_app
then
match st with
| t2 :: t1 :: rem_st -> (
- try reduce_func_app ~orig ty rem_st t1 t2 rem_cont
- with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
+ try reduce_func_app ~orig ty rem_st t1 t2 rem_cont
+ with Undetermined -> reduce_app_no_equ engine st ls ~orig ty rem_cont)
| _ -> assert false
else reduce_app_no_equ engine st ls ~orig ty rem_cont
@@ -1030,80 +1029,80 @@ and reduce_func_app ~orig _ty rem_st t1 t2 rem_cont =
body) that is equivalent to \x.body *)
match t1 with
| Term { t_node = Teps tb } -> (
- let fc, t = Term.t_open_bound tb in
- match t.t_node with
- | Tquant (Tforall, tq) -> (
- let vl, trig, t = t_open_quant tq in
- let process lhs body equ elim =
- let rvl = List.rev vl in
- let rec remove_var lhs rvh rvt =
- match lhs.t_node with
- | Tapp (ls2, [ lhs1; ({ t_node = Tvar v1 } as arg) ])
- when ls_equal ls2 fs_func_app && vs_equal v1 rvh -> (
- match (rvt, lhs1) with
- | rvh :: rvt, _ ->
- let lhs1, fc2 = remove_var lhs1 rvh rvt in
- let lhs2 = t_app ls2 [ lhs1; arg ] lhs.t_ty in
- (t_attr_copy lhs lhs2, fc2)
- | [], { t_node = Tvar fc1 } when vs_equal fc1 fc ->
- let fcn = fc.vs_name in
- let fc2 = Ident.id_derive fcn.Ident.id_string fcn in
- let fc2 = create_vsymbol fc2 (t_type lhs) in
- (t_attr_copy lhs (t_var fc2), fc2)
- | _ -> raise Undetermined)
- | _ -> raise Undetermined
- in
- match rvl with
- | rvh :: rvt -> (
- let lhs, fc2 = remove_var lhs rvh rvt in
- let vh, vl =
- match vl with [] -> assert false | vh :: vl -> (vh, vl)
- in
- let t2 = term_of_value t2 in
- match vl with
- | [] -> elim body vh t2
- | _ ->
- let eq = equ lhs body in
- let tq = t_quant Tforall (t_close_quant vl trig eq) in
- let body = t_attr_copy t (t_eps_close fc2 tq) in
- {
- value_stack = rem_st;
- cont_stack =
- (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
- :: rem_cont;
- })
- | _ -> raise Undetermined
+ let fc, t = Term.t_open_bound tb in
+ match t.t_node with
+ | Tquant (Tforall, tq) -> (
+ let vl, trig, t = t_open_quant tq in
+ let process lhs body equ elim =
+ let rvl = List.rev vl in
+ let rec remove_var lhs rvh rvt =
+ match lhs.t_node with
+ | Tapp (ls2, [ lhs1; ({ t_node = Tvar v1 } as arg) ])
+ when ls_equal ls2 fs_func_app && vs_equal v1 rvh -> (
+ match (rvt, lhs1) with
+ | rvh :: rvt, _ ->
+ let lhs1, fc2 = remove_var lhs1 rvh rvt in
+ let lhs2 = t_app ls2 [ lhs1; arg ] lhs.t_ty in
+ (t_attr_copy lhs lhs2, fc2)
+ | [], { t_node = Tvar fc1 } when vs_equal fc1 fc ->
+ let fcn = fc.vs_name in
+ let fc2 = Ident.id_derive fcn.Ident.id_string fcn in
+ let fc2 = create_vsymbol fc2 (t_type lhs) in
+ (t_attr_copy lhs (t_var fc2), fc2)
+ | _ -> raise Undetermined)
+ | _ -> raise Undetermined
+ in
+ match rvl with
+ | rvh :: rvt -> (
+ let lhs, fc2 = remove_var lhs rvh rvt in
+ let vh, vl =
+ match vl with [] -> assert false | vh :: vl -> (vh, vl)
in
- match t.t_node with
- | Tapp (ls1, [ lhs; body ]) when ls_equal ls1 ps_equ ->
- let equ lhs body = t_attr_copy t (t_app ps_equ [ lhs; body ] None) in
- let elim body vh t2 =
- {
- value_stack = rem_st;
- cont_stack =
- (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
- :: rem_cont;
- }
- in
- process lhs body equ elim
- | Tbinop (Tiff, ({ t_node = Tapp (ls1, [ lhs; tr ]) } as teq), body)
- when ls_equal ls1 ps_equ && t_equal tr t_bool_true ->
- let equ lhs body =
- let lhs = t_attr_copy teq (t_app ps_equ [ lhs; tr ] None) in
- t_attr_copy t (t_binary Tiff lhs body)
- in
- let elim body vh t2 =
- let body = t_if body t_bool_true t_bool_false in
- {
- value_stack = rem_st;
- cont_stack =
- (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
- :: rem_cont;
- }
- in
- process lhs body equ elim
- | _ -> raise Undetermined)
+ let t2 = term_of_value t2 in
+ match vl with
+ | [] -> elim body vh t2
+ | _ ->
+ let eq = equ lhs body in
+ let tq = t_quant Tforall (t_close_quant vl trig eq) in
+ let body = t_attr_copy t (t_eps_close fc2 tq) in
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ })
+ | _ -> raise Undetermined
+ in
+ match t.t_node with
+ | Tapp (ls1, [ lhs; body ]) when ls_equal ls1 ps_equ ->
+ let equ lhs body = t_attr_copy t (t_app ps_equ [ lhs; body ] None) in
+ let elim body vh t2 =
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ }
+ in
+ process lhs body equ elim
+ | Tbinop (Tiff, ({ t_node = Tapp (ls1, [ lhs; tr ]) } as teq), body)
+ when ls_equal ls1 ps_equ && t_equal tr t_bool_true ->
+ let equ lhs body =
+ let lhs = t_attr_copy teq (t_app ps_equ [ lhs; tr ] None) in
+ t_attr_copy t (t_binary Tiff lhs body)
+ in
+ let elim body vh t2 =
+ let body = t_if body t_bool_true t_bool_false in
+ {
+ value_stack = rem_st;
+ cont_stack =
+ (Keval (body, Mvs.add vh t2 Mvs.empty), t_attr_copy orig body)
+ :: rem_cont;
+ }
+ in
+ process lhs body equ elim
| _ -> raise Undetermined)
+ | _ -> raise Undetermined)
| _ -> raise Undetermined
and reduce_app_no_equ engine st ls ~orig ty rem_cont =
@@ -1114,109 +1113,109 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
let v = f engine ls args ty in
{ value_stack = v_attr_copy orig v :: rem_st; cont_stack = rem_cont }
with Not_found | Undetermined -> (
- let args = List.map term_of_value args in
- match Ident.Mid.find ls.ls_name engine.known_map with
- | exception Not_found ->
- Debug.dprintf debug "Reduction engine, ident not found: %s@."
- ls.ls_name.Ident.id_string;
- {
- value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
- cont_stack = rem_cont;
- }
- | d -> (
- let rewrite () =
- (* try a rewrite rule *)
- try
- (* Format.eprintf "try a rewrite rule on %a@." Pretty.print_ls ls; *)
- let (mt, mv), rhs = one_step_reduce engine ls args in
- (* Format.eprintf "rhs = %a@." Pretty.print_term rhs; Format.eprintf
- "sigma = "; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
- Pretty.print_vs v Pretty.print_term t) (snd sigma); Format.eprintf
- "@."; Format.eprintf "try a type match: %a and %a@."
- (Pp.print_option Pretty.print_ty) ty (Pp.print_option
- Pretty.print_ty) rhs.t_ty; *)
- (* let type_subst = Ty.oty_match Ty.Mtv.empty rhs.t_ty ty in
- Format.eprintf "subst of rhs: "; Ty.Mtv.iter (fun tv ty ->
- Format.eprintf "%a -> %a," Pretty.print_tv tv Pretty.print_ty ty)
- type_subst; Format.eprintf "@."; let rhs = t_ty_subst type_subst
- Mvs.empty rhs in let sigma = Mvs.map (t_ty_subst type_subst
- Mvs.empty) sigma in Format.eprintf "rhs = %a@." Pretty.print_term
- rhs; Format.eprintf "sigma = "; Mvs.iter (fun v t -> Format.eprintf
- "%a -> %a," Pretty.print_vs v Pretty.print_term t) sigma;
- Format.eprintf "@."; *)
- let mv, rhs = t_subst_types mt mv rhs in
- incr rec_step_limit;
- {
- value_stack = rem_st;
- cont_stack = (Keval (rhs, mv), orig) :: rem_cont;
- }
- with Irreducible ->
- {
- value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
- cont_stack = rem_cont;
- }
+ let args = List.map term_of_value args in
+ match Ident.Mid.find ls.ls_name engine.known_map with
+ | exception Not_found ->
+ Debug.dprintf debug "Reduction engine, ident not found: %s@."
+ ls.ls_name.Ident.id_string;
+ {
+ value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ | d -> (
+ let rewrite () =
+ (* try a rewrite rule *)
+ try
+ (* Format.eprintf "try a rewrite rule on %a@." Pretty.print_ls ls; *)
+ let (mt, mv), rhs = one_step_reduce engine ls args in
+ (* Format.eprintf "rhs = %a@." Pretty.print_term rhs; Format.eprintf
+ "sigma = "; Mvs.iter (fun v t -> Format.eprintf "%a -> %a,"
+ Pretty.print_vs v Pretty.print_term t) (snd sigma); Format.eprintf
+ "@."; Format.eprintf "try a type match: %a and %a@."
+ (Pp.print_option Pretty.print_ty) ty (Pp.print_option
+ Pretty.print_ty) rhs.t_ty; *)
+ (* let type_subst = Ty.oty_match Ty.Mtv.empty rhs.t_ty ty in
+ Format.eprintf "subst of rhs: "; Ty.Mtv.iter (fun tv ty ->
+ Format.eprintf "%a -> %a," Pretty.print_tv tv Pretty.print_ty ty)
+ type_subst; Format.eprintf "@."; let rhs = t_ty_subst type_subst
+ Mvs.empty rhs in let sigma = Mvs.map (t_ty_subst type_subst
+ Mvs.empty) sigma in Format.eprintf "rhs = %a@." Pretty.print_term
+ rhs; Format.eprintf "sigma = "; Mvs.iter (fun v t -> Format.eprintf
+ "%a -> %a," Pretty.print_vs v Pretty.print_term t) sigma;
+ Format.eprintf "@."; *)
+ let mv, rhs = t_subst_types mt mv rhs in
+ incr rec_step_limit;
+ {
+ value_stack = rem_st;
+ cont_stack = (Keval (rhs, mv), orig) :: rem_cont;
+ }
+ with Irreducible ->
+ {
+ value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ in
+ match d.Decl.d_node with
+ | Decl.Dtype _ | Decl.Dprop _ -> assert false
+ | Decl.Dlogic dl ->
+ (* regular definition *)
+ let d = List.assq ls dl in
+ if engine.params.compute_defs
+ || Term.Sls.mem ls engine.params.compute_def_set
+ then
+ let vl, e = Decl.open_ls_defn d in
+ let add (mt, mv) x y =
+ (Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv)
in
- match d.Decl.d_node with
- | Decl.Dtype _ | Decl.Dprop _ -> assert false
- | Decl.Dlogic dl ->
- (* regular definition *)
- let d = List.assq ls dl in
- if engine.params.compute_defs
- || Term.Sls.mem ls engine.params.compute_def_set
- then
- let vl, e = Decl.open_ls_defn d in
- let add (mt, mv) x y =
- (Ty.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 args in
- let mt = Ty.oty_match mt e.t_ty ty in
- let mv, e = t_subst_types mt mv e in
- {
- value_stack = rem_st;
- cont_stack = (Keval (e, mv), orig) :: rem_cont;
- }
- else rewrite ()
- | Decl.Dparam _ | Decl.Dind _ -> rewrite ()
- | Decl.Ddata dl -> (
- (* constructor or projection *)
- try
- match args with
- | [ { t_node = Tapp (ls1, tl1) } ] ->
- (* if ls is a projection and ls1 is a constructor, we should compute
- that projection *)
- let rec iter dl =
- match dl with
- | [] -> raise Exit
- | (_, csl) :: rem ->
- let rec iter2 csl =
- match csl with
- | [] -> iter rem
- | (cs, prs) :: rem2 ->
- if ls_equal cs ls1
+ let mt, mv = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl args in
+ let mt = Ty.oty_match mt e.t_ty ty in
+ let mv, e = t_subst_types mt mv e in
+ {
+ value_stack = rem_st;
+ cont_stack = (Keval (e, mv), orig) :: rem_cont;
+ }
+ else rewrite ()
+ | Decl.Dparam _ | Decl.Dind _ -> rewrite ()
+ | Decl.Ddata dl -> (
+ (* constructor or projection *)
+ try
+ match args with
+ | [ { t_node = Tapp (ls1, tl1) } ] ->
+ (* if ls is a projection and ls1 is a constructor, we should compute
+ that projection *)
+ let rec iter dl =
+ match dl with
+ | [] -> raise Exit
+ | (_, csl) :: rem ->
+ let rec iter2 csl =
+ match csl with
+ | [] -> iter rem
+ | (cs, prs) :: rem2 ->
+ if ls_equal cs ls1
+ then
+ (* we found the right constructor *)
+ let rec iter3 prs tl1 =
+ match (prs, tl1) with
+ | Some pr :: prs, t :: tl1 ->
+ if ls_equal ls pr
then
- (* we found the right constructor *)
- let rec iter3 prs tl1 =
- match (prs, tl1) with
- | Some pr :: prs, t :: tl1 ->
- if ls_equal ls pr
- then
- (* projection found! *)
- {
- value_stack = Term (t_attr_copy orig t) :: rem_st;
- cont_stack = rem_cont;
- }
- else iter3 prs tl1
- | None :: prs, _ :: tl1 -> iter3 prs tl1
- | _ -> raise Exit
- in
- iter3 prs tl1
- else iter2 rem2
+ (* projection found! *)
+ {
+ value_stack = Term (t_attr_copy orig t) :: rem_st;
+ cont_stack = rem_cont;
+ }
+ else iter3 prs tl1
+ | None :: prs, _ :: tl1 -> iter3 prs tl1
+ | _ -> raise Exit
in
- iter2 csl
- in
- iter dl
- | _ -> raise Exit
- with Exit -> rewrite ())))
+ iter3 prs tl1
+ else iter2 rem2
+ in
+ iter2 csl
+ in
+ iter dl
+ | _ -> raise Exit
+ with Exit -> rewrite ())))
and reduce_equ ~(* engine *) orig st v1 v2 cont =
(* try *)
@@ -1230,19 +1229,19 @@ and reduce_equ ~(* engine *) orig st v1 v2 cont =
incr rec_step_limit;
{ value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
| Int n, Term { t_node = Tconst c } | Term { t_node = Tconst c }, Int n -> (
- try
- let n' = big_int_of_const c in
- let b = to_bool (BigInt.eq n n') in
- incr rec_step_limit;
- { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
- with NotNum -> raise Undetermined)
+ try
+ let n' = big_int_of_const c in
+ let b = to_bool (BigInt.eq n n') in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ with NotNum -> raise Undetermined)
| Real r, Term { t_node = Tconst c } | Term { t_node = Tconst c }, Real r -> (
- try
- let r' = real_of_const c in
- let b = to_bool (Number.compare_real r r' = 0) in
- incr rec_step_limit;
- { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
- with NotNum -> raise Undetermined)
+ try
+ let r' = real_of_const c in
+ let b = to_bool (Number.compare_real r r' = 0) in
+ incr rec_step_limit;
+ { value_stack = Term (t_attr_copy orig b) :: st; cont_stack = cont }
+ with NotNum -> raise Undetermined)
| Real _, Term _ | Term _, Real _ -> raise Undetermined
| Int _, Term _ | Term _, Int _ -> raise Undetermined
| Int _, Real _ | Real _, Int _ -> assert false
@@ -1258,15 +1257,15 @@ and reduce_term_equ ~orig st t1 t2 cont =
else
match (t1.t_node, t2.t_node) with
| Tconst c1, Tconst c2 -> (
- match (c1, c2) with
- | Constant.ConstInt i1, Constant.ConstInt i2 ->
- let b = BigInt.eq i1.Number.il_int i2.Number.il_int in
- incr rec_step_limit;
- {
- value_stack = Term (t_attr_copy orig (to_bool b)) :: st;
- cont_stack = cont;
- }
- | _ -> raise Undetermined)
+ match (c1, c2) with
+ | Constant.ConstInt i1, Constant.ConstInt i2 ->
+ let b = BigInt.eq i1.Number.il_int i2.Number.il_int in
+ incr rec_step_limit;
+ {
+ value_stack = Term (t_attr_copy orig (to_bool b)) :: st;
+ cont_stack = cont;
+ }
+ | _ -> raise Undetermined)
| Tapp (ls1, tl1), Tapp (ls2, tl2)
when ls1.ls_constr > 0 && ls2.ls_constr > 0 ->
if ls_equal ls1 ls2
@@ -1343,30 +1342,31 @@ let normalize ?step_limit ~limit engine sigma t0 =
| [ Term t ], [] -> t
| _, [] -> assert false
| _ -> (
- if n = limit
- then
- let t1 = reconstruct c in
- (* Loc.warning "reduction of term %a takes more than %d steps, aborted at %a.@."
- * Pretty.print_term t0 limit Pretty.print_term t1; *)
- t1
- else
- match step_limit with
- | None ->
+ if n = limit
+ then
+ let t1 = reconstruct c in
+ (* Loc.warning "reduction of term %a takes more than %d steps, aborted at %a.@."
+ * Pretty.print_term t0 limit Pretty.print_term t1; *)
+ t1
+ else
+ match step_limit with
+ | None ->
+ let c = reduce engine c in
+ many_steps c (n + 1)
+ | Some step_limit ->
+ if !rec_step_limit >= step_limit
+ then reconstruct c
+ else
let c = reduce engine c in
- many_steps c (n + 1)
- | Some step_limit ->
- if !rec_step_limit >= step_limit
- then reconstruct c
- else
- let c = reduce engine c in
- many_steps c (n + 1))
+ many_steps c (n + 1))
in
let c = { value_stack = []; cont_stack = [ (Keval (t0, sigma), t0) ] } in
many_steps c 0
(* the rewrite engine *)
-let create ?(bounded_quant=(fun _ _ ~cond:_ -> None)) p env km user_env built_in_user =
+let create ?(bounded_quant = fun _ _ ~cond:_ -> None) p env km user_env
+ built_in_user =
let th = Env.read_theory env [ "int" ] "Int" in
let ls_lt = Theory.ns_find_ls th.Theory.th_export [ Ident.op_infix "<" ] in
let env =
@@ -1403,9 +1403,9 @@ let extract_rule _km t =
then raise (NotARewriteRule "lhs should contain all variables");
(* check the same with type variables *)
if not
- (Ty.Stv.subset
- (t_ty_freevars Ty.Stv.empty t2)
- (t_ty_freevars Ty.Stv.empty t2))
+ (Ty.Stv.subset
+ (t_ty_freevars Ty.Stv.empty t2)
+ (t_ty_freevars Ty.Stv.empty t2))
then raise (NotARewriteRule "lhs should contain all type variables")
in
@@ -1415,19 +1415,19 @@ let extract_rule _km t =
let vs, _, t = t_open_quant q in
aux (List.fold_left (fun acc v -> Svs.add v acc) acc vs) t
| Tbinop (Tiff, t1, t2) -> (
- match t1.t_node with
- | Tapp (ls, args) ->
- (* check_ls ls; *)
- check_vars acc t1 t2;
- (acc, ls, args, t2)
- | _ -> raise (NotARewriteRule "lhs of <-> should be a predicate symbol"))
+ match t1.t_node with
+ | Tapp (ls, args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ (acc, ls, args, t2)
+ | _ -> raise (NotARewriteRule "lhs of <-> should be a predicate symbol"))
| Tapp (ls, [ t1; t2 ]) when ls == ps_equ -> (
- match t1.t_node with
- | Tapp (ls, args) ->
- (* check_ls ls; *)
- check_vars acc t1 t2;
- (acc, ls, args, t2)
- | _ -> raise (NotARewriteRule "lhs of = should be a function symbol"))
+ match t1.t_node with
+ | Tapp (ls, args) ->
+ (* check_ls ls; *)
+ check_vars acc t1 t2;
+ (acc, ls, args, t2)
+ | _ -> raise (NotARewriteRule "lhs of = should be a function symbol"))
| _ ->
raise
(NotARewriteRule
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 1f5cb9597ced78bcfe566348af0c54f2a3ebc879..0b1a8f239d7c5a118814efc7ede0b25b406c9ef7 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -33,8 +33,8 @@ Test interpret on dataset
> forall perturbed_image: image.
> equal_shape i perturbed_image ->
> valid_image perturbed_image ->
- > let p = perturbed_image - i in
- > bounded_by_epsilon p eps ->
+ > let perturbation = perturbed_image - i in
+ > bounded_by_epsilon perturbation eps ->
> advises c perturbed_image l
>
> predicate robust (c: classifier) (d: dataset image label_) (eps: t) =
@@ -47,1398 +47,112 @@ Test interpret on dataset
> robust classifier dataset eps
> end
> EOF
- TERM: let classifier = read_classifier ("TestNetwork.nnet":string) NNet in
- let dataset =
- (read_dataset ("dataset.csv":string) CSV: vector (tensor t, int))
- in let eps = (0.375:t) in robust classifier dataset eps
- --
- read_classifier: ls:read_classifier , ty:classifier
- ls_of_caisar_op: (Interpretation.Classifier
- "$TESTCASE_ROOT/TestNetwork.nnet")
- ty: classifier
- ls: caisar_op
- --
- read_dataset: ls:read_dataset , ty:vector (tensor t,
- int)
- ls_of_caisar_op: (Interpretation.Dataset <csv>)
- ty: vector (tensor t,
- int)
- ls: caisar_op1
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image , v
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image , v
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image , y2
- --
- valid_index: perturbed_image - y2 v1
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
- ty: vector
- int
- ls: caisar_op2
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
- ty: vector
- int
- ls: caisar_op3
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
- ty: vector
- int
- ls: caisar_op4
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
- ty: vector
- int
- ls: caisar_op5
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
- ty: vector
- int
- ls: caisar_op6
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op6
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image - y2 , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , y3
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , y3
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , y3
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: y0 , perturbed_image
- --
- vget: ls:([]) , ty:t
- Terms: y0 @@ perturbed_image , 2
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 , v2
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 , v2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image1 , y21
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image1 - y21 , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , y31
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , y31
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image1
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image1 , y31
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 , v3
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 , v3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image2 , y22
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image2 - y22 , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , y32
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , y32
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image2
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image2 , y32
- reduce_match@e
- --
- length: ls:length , ty:int
- --
- vget: ls:([]) , ty:(tensor t,
- int)
- Terms: caisar_op1 , 0
- ls_of_caisar_op: (Interpretation.Data
- (Interpretation.D_csv
- ["0.0"; "1.0"; "0.784313725"; "0.019607843";
- "0.776470588"]))
- ty: tensor
- t
- ls: caisar_op7
- reduce_match@(caisar_op7,
- 1)
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 , v4
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 , v4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image3 , y23
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image3 - y23 , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , y33
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , y33
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image3
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image3 , y33
- --
- equal_shape: caisar_op7 perturbed_image4
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- ls: caisar_op8
- --
- valid_index: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 v5
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
- ty: vector
- int
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op6
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , caisar_op7
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es .- (0.0:t)) (caisar_es1 .- (1.0:t))
- (caisar_es2
- .- (0.78431372499999996161790249971090815961360931396484375:t))
- (caisar_es3
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es4
- .- (0.776470588000000017103729987866245210170745849609375:t)) , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3
- caisar_es4
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es caisar_es1 caisar_es2 caisar_es3 caisar_es4 , y34
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8
- caisar_es9
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es5 caisar_es6 caisar_es7 caisar_es8 caisar_es9 , 1
- --
- vget: ls:([]) , ty:(tensor t,
- int)
- Terms: caisar_op1 , 1
- ls_of_caisar_op: (Interpretation.Data
- (Interpretation.D_csv
- ["1.0"; "0.0"; "0.019607843"; "0.776470588";
- "0.784313725"]))
- ty: tensor
- t
- ls: caisar_op9
- reduce_match@(caisar_op9,
- 0)
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 , v6
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 , v6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: perturbed_image5 , y24
- --
- tget: ls:(#) , ty:t
- Terms: perturbed_image5 - y24 , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , y35
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , y35
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , perturbed_image5
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op @@ perturbed_image5 , y35
- --
- equal_shape: caisar_op9 perturbed_image6
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- valid_index: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 v7
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 4))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 3))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 2))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 1))
- ty: vector
- int
- ls_of_caisar_op: (Interpretation.Index (Interpretation.I_csv 0))
- ty: vector
- int
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op2
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op3
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op4
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op5
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op6
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op2
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op3
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op4
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op5
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op6
- --
- tminus: ls:(-) , ty:tensor
- t
- Terms: caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13 caisar_es14 , caisar_op9
- ls_of_caisar_op: (Interpretation.Tensor 5)
- ty: tensor
- t
- --
- tget: ls:(#) , ty:t
- Terms: caisar_op8 (caisar_es10 .- (1.0:t)) (caisar_es11 .- (0.0:t))
- (caisar_es12
- .- (0.01960784299999999980013143385804141871631145477294921875:t))
- (caisar_es13
- .- (0.776470588000000017103729987866245210170745849609375:t))
- (caisar_es14
- .- (0.78431372499999996161790249971090815961360931396484375:t)) , caisar_op6
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , y36
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , y36
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es10 caisar_es11 caisar_es12 caisar_es13
- caisar_es14 , y36
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 1
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 0
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 2
- --
- apply_classifier: ls:(@@) , ty:vector
- t
- Terms: caisar_op , caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19
- --
- vget: ls:([]) , ty:t
- Terms: caisar_op
- @@ caisar_op8 caisar_es15 caisar_es16 caisar_es17 caisar_es18
- caisar_es19 , 0
- G : (forall caisar_es20:t, caisar_es21:t, caisar_es22:t, caisar_es23:t,
- caisar_es24:t.
- ((((le (0.0:t) caisar_es24 /\ le caisar_es24 (1.0:t)) /\
- le (0.0:t) caisar_es23 /\ le caisar_es23 (1.0:t)) /\
- le (0.0:t) caisar_es22 /\ le caisar_es22 (1.0:t)) /\
- le (0.0:t) caisar_es21 /\ le caisar_es21 (1.0:t)) /\
- le (0.0:t) caisar_es20 /\ le caisar_es20 (1.0:t) ->
+ G : (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
+ ((((le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t)) /\
+ le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
+ le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
+ le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
+ le (0.0:t) caisar_v /\ le caisar_v (1.0:t) ->
((((le (neg (0.375:t))
- (sub RNE caisar_es24
+ (sub RNE caisar_v4
(0.776470588000000017103729987866245210170745849609375:t)) /\
le
- (sub RNE caisar_es24
+ (sub RNE caisar_v4
(0.776470588000000017103729987866245210170745849609375:t))
(0.375:t)) /\
le (neg (0.375:t))
- (sub RNE caisar_es23
+ (sub RNE caisar_v3
(0.01960784299999999980013143385804141871631145477294921875:t)) /\
le
- (sub RNE caisar_es23
+ (sub RNE caisar_v3
(0.01960784299999999980013143385804141871631145477294921875:t))
(0.375:t)) /\
le (neg (0.375:t))
- (sub RNE caisar_es22
+ (sub RNE caisar_v2
(0.78431372499999996161790249971090815961360931396484375:t)) /\
le
- (sub RNE caisar_es22
+ (sub RNE caisar_v2
(0.78431372499999996161790249971090815961360931396484375:t))
(0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_es21 (1.0:t)) /\
- le (sub RNE caisar_es21 (1.0:t)) (0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_es20 (0.0:t)) /\
- le (sub RNE caisar_es20 (0.0:t)) (0.375:t) ->
+ le (neg (0.375:t)) (sub RNE caisar_v1 (1.0:t)) /\
+ le (sub RNE caisar_v1 (1.0:t)) (0.375:t)) /\
+ le (neg (0.375:t)) (sub RNE caisar_v (0.0:t)) /\
+ le (sub RNE caisar_v (0.0:t)) (0.375:t) ->
lt
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[0]
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[1] /\
lt
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[2]
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[1]) /\
- (forall caisar_es20:t, caisar_es21:t, caisar_es22:t, caisar_es23:t,
- caisar_es24:t.
- ((((le (0.0:t) caisar_es24 /\ le caisar_es24 (1.0:t)) /\
- le (0.0:t) caisar_es23 /\ le caisar_es23 (1.0:t)) /\
- le (0.0:t) caisar_es22 /\ le caisar_es22 (1.0:t)) /\
- le (0.0:t) caisar_es21 /\ le caisar_es21 (1.0:t)) /\
- le (0.0:t) caisar_es20 /\ le caisar_es20 (1.0:t) ->
+ (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
+ ((((le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t)) /\
+ le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
+ le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
+ le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
+ le (0.0:t) caisar_v /\ le caisar_v (1.0:t) ->
((((le (neg (0.375:t))
- (sub RNE caisar_es24
+ (sub RNE caisar_v4
(0.78431372499999996161790249971090815961360931396484375:t)) /\
le
- (sub RNE caisar_es24
+ (sub RNE caisar_v4
(0.78431372499999996161790249971090815961360931396484375:t))
(0.375:t)) /\
le (neg (0.375:t))
- (sub RNE caisar_es23
+ (sub RNE caisar_v3
(0.776470588000000017103729987866245210170745849609375:t)) /\
le
- (sub RNE caisar_es23
+ (sub RNE caisar_v3
(0.776470588000000017103729987866245210170745849609375:t))
(0.375:t)) /\
le (neg (0.375:t))
- (sub RNE caisar_es22
+ (sub RNE caisar_v2
(0.01960784299999999980013143385804141871631145477294921875:t)) /\
le
- (sub RNE caisar_es22
+ (sub RNE caisar_v2
(0.01960784299999999980013143385804141871631145477294921875:t))
(0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_es21 (0.0:t)) /\
- le (sub RNE caisar_es21 (0.0:t)) (0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_es20 (1.0:t)) /\
- le (sub RNE caisar_es20 (1.0:t)) (0.375:t) ->
+ le (neg (0.375:t)) (sub RNE caisar_v1 (0.0:t)) /\
+ le (sub RNE caisar_v1 (0.0:t)) (0.375:t)) /\
+ le (neg (0.375:t)) (sub RNE caisar_v (1.0:t)) /\
+ le (sub RNE caisar_v (1.0:t)) (0.375:t) ->
lt
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[1]
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[0] /\
lt
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[2]
(caisar_op
- @@ caisar_op8 caisar_es20 caisar_es21 caisar_es22 caisar_es23
- caisar_es24)
+ @@ caisar_op1 caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
[0])
- caisar_op7,
+ caisar_op2,
+ (Interpretation.Data
+ (Interpretation.D_csv
+ ["1.0"; "0.0"; "0.019607843"; "0.776470588"; "0.784313725"]))
+ caisar_op3, (Interpretation.Index (Interpretation.I_csv 2))
+ caisar_op4, (Interpretation.Index (Interpretation.I_csv 1))
+ caisar_op5, (Interpretation.Index (Interpretation.I_csv 0))
+ caisar_op6,
(Interpretation.Data
(Interpretation.D_csv
["0.0"; "1.0"; "0.784313725"; "0.019607843"; "0.776470588"]))
caisar_op,
(Interpretation.Classifier
"$TESTCASE_ROOT/TestNetwork.nnet")
- caisar_op1, (Interpretation.Dataset <csv>)
+ caisar_op1, (Interpretation.Tensor 5)
+ caisar_op7, (Interpretation.Dataset <csv>)
+ caisar_op8, (Interpretation.Index (Interpretation.I_csv 4))
caisar_op9,
- (Interpretation.Data
- (Interpretation.D_csv
- ["1.0"; "0.0"; "0.019607843"; "0.776470588"; "0.784313725"]))
- caisar_op8, (Interpretation.Tensor 5)
- caisar_op2, (Interpretation.Index (Interpretation.I_csv 4))
- caisar_op3, (Interpretation.Index (Interpretation.I_csv 3))
- caisar_op4, (Interpretation.Index (Interpretation.I_csv 2))
- caisar_op5, (Interpretation.Index (Interpretation.I_csv 1))
- caisar_op6,
- (Interpretation.Index (Interpretation.I_csv 0))
+ (Interpretation.Index (Interpretation.I_csv 3))