36 val file=Source.fromFile("zrepo_Dont_deleteWholeLine_Dont_addNewLineBeforeSomeLine").mkString.split('\n')
37 val naiveTheorems = file.zipWithIndex.drop(1).map( a=>{
38 val isNaive = !a._1.contains(" ")
39 if( isNaive) {new Theorem( a._2 +"___" + a._1 )}
40 })
41 val complexTheorems = file.zipWithIndex.drop(1).map( a=>{
42 val isNaive = !a._1.contains(" ")
43 if( !isNaive) {
64 val proofs = a._1.split(" ").drop(1).map( aNameCountAndTheorem => {
65 val name= aNameCountAndTheorem.split(' ')(0)
66 val count = aNameCountAndTheorem.split(' ')(1)
67 val theoremsUsedByThisProof:Seq[Theorem] = aNameCountAndTheorem.split(' ').drop(2).map( a=> naiveTheorems(Integer.parseInt(a)).asInstanceOf[Theorem] ) 这个技巧很要，从Array到Seq
129 val ts = Seq( naiveTheorems(2).asInstanceOf[Theorem], naiveTheorems(3).asInstanceOf[Theorem] )
130 //Class.forName( "Proof").getConstructors()(2).newInstance( name, count, ts).asInstanceOf[Proof]
131 Class.forName( "Proof").getConstructors()(2).newInstance( name, count, theoremsUsedByThisProof ).asInstanceOf[Proof]
132 //Array.range( 1, 1+ aNameCountAndTheorem._2 )
133 })
134 println("此定理的所有证明方法:")
135 proofs foreach println
没什么好解释的，不明白解释了也不明白。。。
但是下面的注释代表的实验过程，很重要，需要的话可以参考。
68 /* get a Tuple2
69 val theoremsUsedByThisProof = aNameCountAndTheorem.split(' ').drop(2).map( a=> naiveTheorems(Integer.parseInt(a)).asInstanceOf[Theorem] ) match {
70 case Array(x,y) => (x,y)
71 }
72 println(" theoremsUsedByThisProof ")
73 println(theoremsUsedByThisProof.getClass)
74 println(theoremsUsedByThisProof.asInstanceOf[AnyRef].getClass.getName)
75 println("它的内容")
76 //theoremsUsedByThisProof foreach println
77 to find the type of above
78 class B(name:String) {override def toString():String = "hi " + name}
79
80 scala> val bs = Array.range(1,5).map( a=> new B(""+a) )
81 bs: Array[B] = Array(hi 1, hi 2, hi 3, hi 4)
82 这个技巧很要，从Array到tuple
83 scala> val refsMatched=Array.range(1,3).map( a=> bs(a).asInstanceOf[B]) match {case Array(x,y)=>(x,y)}
84 refsMatched: (B, B) = (hi 2,hi 3)
85 scala> refsMatched.getClass
86 res1: Class[_ <: (B, B)] = class scala.Tuple2 我现在需要的是Seq不是Tuple2。array转seq需要
87
88 scala> val zseq: Seq[B] = bs
89 zseq: Seq[B] = WrappedArray(hi 1, hi 2, hi 3, hi 4)
90 scala> zseq.getClass
91 res2: Class[_ <: Seq[B]] = class scala.collection.mutable.WrappedArray$ofRef
92
93 scala> val refs=Array.range(1,3).map( a=> bs(a).asInstanceOf[B])
94 refs: Array[B] = Array(hi 2, hi 3)
95
96 scala> refs.getClass 这类型，好奇怪啊，到底是什么？
97 res2: Class[_ <: Array[B]] = class [LB;
98
99 scala> println(refs.getClass)
100 class [L$line3.$read$$iw$$iw$B;
101
102 scala> println(refs.asInstanceOf[AnyRef].getClass.getName)
103 [L$line3.$read$$iw$$iw$B;
104
105 scala> println(bs.getClass) 但是bs，类型一样啊，为什么不行？再弄个seq的看看
106 class [L$line3.$read$$iw$$iw$B;
107
108 scala> println(bs.asInstanceOf[AnyRef].getClass.getName)
109 [L$line3.$read$$iw$$iw$B;
110
111 scala> bs
112 res9: Array[B] = Array(hi 1, hi 2, hi 3, hi 4)
113
114 scala> refs
115 res10: Array[B] = Array(hi 2, hi 3)
116
117 scala> bs.getClass
118 res11: Class[_ <: Array[B]] = class [LB;
119
120 scala> val seq = ( bs(1).asInstanceOf[B], bs(2).asInstanceOf[B] )
121 seq: (B, B) = (hi 2,hi 3)
122
123 scala> println(seq.asInstanceOf[AnyRef].getClass.getName) 确实不同啊，是Tuple2
124 scala.Tuple2
125
126 scala> println(seq.getClass)
127 class scala.Tuple2
128 */
