[printing] fix printing issue

Author: thibautbenjamin

lib/equality.ml

@@ -32,10 +32,10 @@ struct
       TmT.t * Unchecked_types(CohT)(TmT).sub
   end) =
   struct
-    module P = Printing.Printing (CohT) (TmT)
-    module Printing = P.Make (Coh) (Tm)
     module U = Unchecked.Unchecked (CohT) (TmT)
     module Unchecked = U.Make (Coh) (Tm)
+    module P = Printing.Printing (CohT) (TmT) (Unchecked)
+    module Printing = P.Make (Coh) (Tm)
 
     let rec is_equal_ps ps1 ps2 =
       match (ps1, ps2) with

lib/kernel.ml

@@ -34,7 +34,7 @@ end = struct
   open Unchecked (Coh) (Tm)
   module Unchecked = Make (Coh) (Tm)
   module Types = Unchecked_types (Coh) (Tm)
-  open Printing (Coh) (Tm)
+  open Printing (Coh) (Tm) (Unchecked)
   module Printing = Make (Coh) (Tm)
 
   let tbl : (Ctx.t * PS.t * Types.sub_ps, Sub.t) Hashtbl.t = Hashtbl.create 7829
@@ -105,7 +105,7 @@ end = struct
   open Unchecked_types (Coh) (Tm)
   module U = Unchecked (Coh) (Tm)
   module Unchecked = U.Make (Coh) (Tm)
-  module P = Printing (Coh) (Tm)
+  module P = Printing (Coh) (Tm) (Unchecked)
   module Printing = P.Make (Coh) (Tm)
   module E = Equality (Coh) (Tm)
   module Equality = E.Make (Coh) (Tm)
@@ -184,7 +184,7 @@ end = struct
 
   module U = Unchecked (Coh) (Tm)
   module Unchecked = U.Make (Coh) (Tm)
-  module P = Printing (Coh) (Tm)
+  module P = Printing (Coh) (Tm) (Unchecked)
   module Printing = P.Make (Coh) (Tm)
   module E = Equality (Coh) (Tm)
   module Equality = E.Make (Coh) (Tm)
@@ -344,7 +344,7 @@ end = struct
   module Types = Unchecked_types (Coh) (Tm)
   module U = Unchecked (Coh) (Tm)
   module Unchecked = U.Make (Coh) (Tm)
-  module P = Printing (Coh) (Tm)
+  module P = Printing (Coh) (Tm) (Unchecked)
   module Printing = P.Make (Coh) (Tm)
   module E = Equality (Coh) (Tm)
   module Equality = E.Make (Coh) (Tm)
@@ -470,7 +470,7 @@ end = struct
   module Unchecked = U.Make (Coh) (Tm)
   module Types = Unchecked_types (Coh) (Tm)
   module Display_maps = Unchecked.Display_maps
-  module P = Printing (Coh) (Tm)
+  module P = Printing (Coh) (Tm) (Unchecked)
   module Printing = P.Make (Coh) (Tm)
   module E = Equality (Coh) (Tm)
   module Equality = E.Make (Coh) (Tm)
@@ -680,7 +680,7 @@ end = struct
   open Unchecked (Coh) (Tm)
   module Unchecked = Make (Coh) (Tm)
   module Display_maps = Unchecked.Display_maps
-  open Printing (Coh) (Tm)
+  open Printing (Coh) (Tm) (Unchecked)
   module Printing = Make (Coh) (Tm)
 
   let ps = function Inv (data, _) -> data.ps | NonInv (data, _) -> data.ps
@@ -839,7 +839,7 @@ end
 module U = Unchecked (Coh) (Tm)
 module Unchecked = U.Make (Coh) (Tm)
 module Display_maps = Unchecked.Display_maps
-module P = Printing (Coh) (Tm)
+module P = Printing (Coh) (Tm) (Unchecked)
 module Printing = P.Make (Coh) (Tm)
 module E = Equality (Coh) (Tm)
 module Equality = E.Make (Coh) (Tm)

lib/printing.ml

@@ -5,6 +5,11 @@ module Printing (CohT : sig
   type t
 end) (TmT : sig
   type t
+end) (App : sig
+  val tm_apply_sub :
+    Unchecked_types(CohT)(TmT).tm ->
+    Unchecked_types(CohT)(TmT).sub ->
+    Unchecked_types(CohT)(TmT).tm
 end) =
 struct
   open Unchecked_types (CohT) (TmT)
@@ -65,14 +70,14 @@ struct
               let func = Coh.func_data c in
               Printf.sprintf "(%s%s)" (Coh.to_string c)
                 (sub_ps_to_string ~func s)
-        | App (t, s) ->
-            let name =
-              match Tm.name t with Some name -> name | None -> "anonymous_tm"
-            in
-            let func = Tm.func_data t in
-            let str_s, expl = sub_to_string ?func s in
-            let expl_str = if expl then "@" else "" in
-            Printf.sprintf "(%s%s%s)" expl_str name str_s
+        | App (t, s) -> (
+            match Tm.name t with
+            | Some name ->
+                let func = Tm.func_data t in
+                let str_s, expl = sub_to_string ?func s in
+                let expl_str = if expl then "@" else "" in
+                Printf.sprintf "(%s%s%s)" expl_str name str_s
+            | None -> tm_to_string (App.tm_apply_sub (Tm.develop t) s))
 
       and sub_ps_to_string ?(func = []) s =
         match func with

lib/printing.mli

@@ -5,6 +5,11 @@ module Printing (Coh : sig
   type t
 end) (Tm : sig
   type t
+end) (_ : sig
+  val tm_apply_sub :
+    Unchecked_types(Coh)(Tm).tm ->
+    Unchecked_types(Coh)(Tm).sub ->
+    Unchecked_types(Coh)(Tm).tm
 end) : sig
   open Unchecked_types(Coh)(Tm)
 

test.t/run.t

@@ -704,8 +704,6 @@
   [=^.^=] check cylcomp(3,1,3)
   [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.26,1) (.22,1) (.18,1) (.14,1) (.9,1) (.4,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .4 .18)] .23) (!1builtin_comp3 (intch_src_op{3} .3 .17 .23) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .17 .23) (builtin_comp2_op{2} .3 [.25]) (assoc_op{3} .3 .11 .21) (builtin_comp2_op{2} [.13] .21) (builtin_assc_op{3} .10 .8 .21))) (intch_tgt_op{3} .10 .8 .21))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .16 .23) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .23) (builtin_comp2_op{2} .2 [.24]) (assoc_op{3} .2 .11 .20) (builtin_comp2_op{2} [.12] .20) (builtin_assc_op{3} .10 .7 .20))) (intch_tgt_op{3} .10 .7 .20)) (builtin_comp2_op{2} .10 [(builtin_comp2_func[(.4,1) (.8,1)]_op{3} .9 .22)])).
   [=^.^=] check cylcomp(3,2,3)
-  [=D.D=] substitution: (.0, .0) (.1, .6) (.2, (builtin_comp2 .2 .11)) (.3, (builtin_comp2 .3 .11)) (.4, (builtin_comp2 [.4] .11)) (.5, (builtin_comp2 .10 .7)) (.6, (builtin_comp2 .10 .8)) (.7, (builtin_comp2 .10 [.9])) (.8, .12) (.9, .13) (.10, .14) (.11, (builtin_comp2 .15 .11)) (.12, (builtin_comp2 [.16] .11)) (.13, (builtin_comp2 .10 .17)) (.14, (builtin_comp2 .10 [.18])) (.15, .19) (.16, .20)
-
   [=I.I=] valid term builtin_conecomp(3,2,3) of type (!1builtin_comp2 (builtin_comp2 [(!1builtin_comp2 .4 .16)] .11) .19) -> (!1builtin_comp2 .12 (builtin_comp2_func[(.4,1)]_op{1} (!1builtin_comp2 .9 .18) .10)).
   [=^.^=] check cylcomp(3,1,2)
   [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.14,1) (.9,1) (.4,1)]_op{3} of type (!1builtin_comp2 (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .16)] .19) (!1builtin_comp3 (intch_src_op{3} .3 .16 .19) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .16 .19) (builtin_comp2_op{2} .3 [.20]) (assoc_op{3} .3 .11 .18) (builtin_comp2_op{2} [.13] .18) (builtin_assc_op{3} .10 .8 .18))) (intch_tgt_op{3} .10 .8 .18))) -> (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .16 .19) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .16 .19) (builtin_comp2_op{2} .2 [.20]) (assoc_op{3} .2 .11 .18) (builtin_comp2_op{2} [.12] .18) (builtin_assc_op{3} .10 .7 .18))) (intch_tgt_op{3} .10 .7 .18)) (builtin_comp2_op{2} .10 [(builtin_comp2_op{2} [.9] .18)])).
@@ -716,10 +714,6 @@
   [=^.^=] check cylcomp(4,2,4)
   [=I.I=] valid term builtin_conecomp(3,2,3)_func[(.32,1) (.28,1) (.24,1) (.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (!1builtin_comp2 [.6] [.24]) .15)] .29) (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .5 .23 .15)] .29) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.23] .15) .29) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.5] .15) (builtin_comp2_op{2} [.23] .15) .29) (!1builtin_comp2 (builtin_comp2_op{2} [.5] .15) [.31]) (!1assoc (builtin_comp2_op{2} [.5] .15) .17 (builtin_comp2_op{2} .14 [.27])) (!1builtin_comp2 [.19] (builtin_comp2_op{2} .14 [.27])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.27])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.12]) (builtin_comp2_op{2} .14 [.27]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .12 .27)]))) -> (!2builtin_comp2 (!2builtin_comp3 (!1builtin_comp2 [(builtin_comp_1_0_intch_op{4} .4 .22 .15)] .29) (!2builtin_comp3 (!1intch_src (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .29) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp5 (!1builtin_assc (builtin_comp2_op{2} [.4] .15) (builtin_comp2_op{2} [.22] .15) .29) (!1builtin_comp2 (builtin_comp2_op{2} [.4] .15) [.30]) (!1assoc (builtin_comp2_op{2} [.4] .15) .17 (builtin_comp2_op{2} .14 [.26])) (!1builtin_comp2 [.18] (builtin_comp2_op{2} .14 [.26])) (!1builtin_assc .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.26])))) (!1intch_tgt .16 (builtin_comp2_op{2} .14 [.11]) (builtin_comp2_op{2} .14 [.26]))) (!1builtin_comp2 .16 [(builtin_comp_1_0_intch_op{1}^-1 .14 .11 .26)])) (!1builtin_comp2 .16 [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (!1builtin_comp2 [.13] [.28]))])).
   [=^.^=] check cylcomp(4,3,4)
-  [=D.D=] substitution: (.0, .0) (.1, .6) (.2, (builtin_comp2 .2 .11)) (.3, (builtin_comp2 .3 .11)) (.4, (builtin_comp2 [.4] .11)) (.5, (builtin_comp2 .10 .7)) (.6, (builtin_comp2 .10 .8)) (.7, (builtin_comp2 .10 [.9])) (.8, .12) (.9, .13) (.10, .14) (.11, (builtin_comp2 .15 .11)) (.12, (builtin_comp2 [.16] .11)) (.13, (builtin_comp2 .10 .17)) (.14, (builtin_comp2 .10 [.18])) (.15, .19) (.16, .20)
-
-  [=D.D=] substitution: (.0, .0) (.1, .8) (.2, (builtin_comp2 .2 .15)) (.3, (builtin_comp2 .3 .15)) (.4, (builtin_comp2 [.4] .15)) (.5, (builtin_comp2 [.5] .15)) (.6, (builtin_comp2 [[.6]] .15)) (.7, (builtin_comp2 .14 .9)) (.8, (builtin_comp2 .14 .10)) (.9, (builtin_comp2 .14 [.11])) (.10, (builtin_comp2 .14 [.12])) (.11, (builtin_comp2 .14 [[.13]])) (.12, .16) (.13, .17) (.14, .18) (.15, .19) (.16, .20) (.17, (builtin_comp2 [.21] .15)) (.18, (builtin_comp2 [[.22]] .15)) (.19, (builtin_comp2 .14 [.23])) (.20, (builtin_comp2 .14 [[.24]])) (.21, .25) (.22, .26)
-
   [=I.I=] valid term builtin_conecomp(4,3,4) of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2 [[(!2builtin_comp2 .6 .22)]] .15)] .17) .25) -> (!2builtin_comp2 .18 (!1builtin_comp2 .16 [(builtin_comp2_func[(.6,2)]_op{1} (!2builtin_comp2 .13 .24) .14)])).
   [=^.^=] check cylcomp(4,1,2)
   [=I.I=] valid term builtin_conecomp(2,1,2)_func[(.14,1) (.9,1) (.4,1)]_op{3}_func[(.20,1) (.13,1) (.6,1)]_op{4} of type (!2builtin_comp2 (!1builtin_comp2 [(builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} (builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} .6 .22) .25)] (!1builtin_comp3 (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24))) (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 [(intch_src_func[(.4,1)]_op{3} .5 .22 .25)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.5] .22)] .25)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1)]_op{3} .5 .22 .25) (builtin_comp2_func[(.8,1)][(.4,1)]_op{3} .5 .26) (assoc_func[(.4,1)]_op{3} .5 .15 .24) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .19 .24) (builtin_assc_func[(.6,1)]_op{3} .14 .12 .24)))] (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) [(intch_tgt_func[(.6,1)]_op{3} .14 .12 .24)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.12] .24)])))) -> (!2builtin_comp2 (!2builtin_comp3 (intch_tgt_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp5_red_func[(.6,1)]_op{3} (!2builtin_comp7 (!1builtin_assc_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25) (intch_src_op{3} .3 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 [(intch_src_func[(.4,1)]_op{3} .4 .22 .25)] (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} [(builtin_comp2_op{2} [.4] .22)] .25)) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .3 .22 .25) (builtin_comp2_op{2} .3 [.26]) (assoc_op{3} .3 .15 .24) (builtin_comp2_op{2} [.17] .24) (builtin_assc_op{3} .14 .10 .24))) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) [(builtin_comp2_red_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} (!1builtin_comp5_func[(.2~,1) (.3~,1) (.4~,1) (.5~,1) (.6~,1) (.7~,1) (.8~,1) (.9~,1) (.10~,1) (.11~,1) (.12~,1)]_op{3} (builtin_assc_func[(.4,1)]_op{3} .4 .22 .25) (builtin_comp2_func[(.8,1)][(.4,1)]_op{3} .4 .26) (assoc_func[(.4,1)]_op{3} .4 .15 .24) (builtin_comp2_func[(.4,1)][(.2~,1) (.3~,1) (.4~,1)]_op{3} .18 .24) (builtin_assc_func[(.6,1)]_op{3} .14 .11 .24)))] (intch_tgt_op{3} .14 .10 .24)) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (builtin_comp2_red_func[(.4,1)]_op{3} (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)])) (intch_tgt_op{3} .14 .10 .24)) (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) [(intch_tgt_func[(.6,1)]_op{3} .14 .11 .24)]) (!1builtin_assc_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)])))) (intch_src_op{3} (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24) (builtin_comp2_op{2} .14 [(builtin_comp2_op{2} [.11] .24)]))) (!1builtin_comp2 (!1builtin_comp3 (intch_src_op{3} .2 .22 .25) (builtin_comp2_red_func[(.4,1)]_op{3} (!1builtin_comp5 (builtin_assc_op{3} .2 .22 .25) (builtin_comp2_op{2} .2 [.26]) (assoc_op{3} .2 .15 .24) (builtin_comp2_op{2} [.16] .24) (builtin_assc_op{3} .14 .9 .24))) (intch_tgt_op{3} .14 .9 .24)) [(builtin_comp2_func[(.6,1)]_red_func[(.8,1)]_op{3} .14 (builtin_comp2_func[(.4,1)]_red_func[(.6,1)]_op{3} .13 .24))])).