more more speed up

snu-sf · Jul 22, 2018 · 6f36188 · 6f36188
1 parent a85b819
commit 6f36188
Show file tree

Hide file tree

Showing 17 changed files with 1,218 additions and 1,217 deletions.
diff --git a/metasrc/paco.py b/metasrc/paco.py
@@ -287,39 +287,40 @@
     print ('End Arg'+str(n)+'_'+str(m)+'.')
     print ('')
 
-print ('End PACO'+str(n)+'.')
-print ('')
-
-for m in range(1,mutsize+1):
-    for i in range(m):
-        print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'.')
-    print ('')
-
     for i in range(m):
-        print ('Hint Unfold upaco'+str(n)+lev(m)+idx(m,i)+'.')
-    for i in range(m):
-        print ('Hint Resolve paco'+str(n)+lev(m)+idx(m,i)+'_fold.')
-    print ('Hint Unfold monotone'+str(n)+lev(m)+'.')
-    print ('')
-
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_acc'+" : clear implicits.")
     for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_acc'+ifpstr(n,'            ['+itrstr(" T",n)+' ].'," : clear implicits."))
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mon'+" : clear implicits.")
     for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mon'+ifpstr(n,'            ['+itrstr(" T",n)+' ].'," : clear implicits."))
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult_strong'+" : clear implicits.")
     for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult_strong'+ifpstr(n,'    ['+itrstr(" T",n)+' ].'," : clear implicits."))
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult'+" : clear implicits.")
     for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_mult'+ifpstr(n,'           ['+itrstr(" T",n)+' ].'," : clear implicits."))
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_fold'+" : clear implicits.")
     for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_fold'+ifpstr(n,'           ['+itrstr(" T",n)+' ].'," : clear implicits."))
-    for i in range(m):
-        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_unfold'+ifpstr(n,'         ['+itrstr(" T",n)+' ].'," : clear implicits."))
+        print ('Arguments paco'+str(n)+lev(m)+idx(m,i)+'_unfold'+" : clear implicits.")
     print ('')
 
     for i in range(m):
-        print ("Instance paco"+str(n)+lev(m)+idx(m,i)+"_inst "+itrstr(" T",n)+" ("+itridx("gf",m," ")+": rel"+str(n)+itrstr(" T",n)+"->_)"+itridx(" r",m)+itrstr(" x",n)+" : paco_class (paco"+str(n)+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(" r",m)+itrstr(" x",n)+") :=")
+        print ("Global Instance paco"+str(n)+lev(m)+idx(m,i)+"_inst "+" ("+itridx("gf",m," ")+": rel"+str(n)+itrstr(" T",n)+"->_)"+itridx(" r",m)+itrstr(" x",n)+" : paco_class (paco"+str(n)+lev(m)+idx(m,i)+itridx(" gf",m)+itridx(" r",m)+itrstr(" x",n)+") :=")
         print ("{ pacoacc    := paco"+str(n)+lev(m)+idx(m,i)+"_acc"+itridx(" gf",m)+";")
         print ("  pacomult   := paco"+str(n)+lev(m)+idx(m,i)+"_mult"+itridx(" gf",m)+";")
         print ("  pacofold   := paco"+str(n)+lev(m)+idx(m,i)+"_fold"+itridx(" gf",m)+";")
         print ("  pacounfold := paco"+str(n)+lev(m)+idx(m,i)+"_unfold"+itridx(" gf",m)+" }.")
         print ('')
+
+
+print ('End PACO'+str(n)+'.')
+print ('')
+
+for m in range(1,mutsize+1):
+    for i in range(m):
+        print ('Global Opaque paco'+str(n)+lev(m)+idx(m,i)+'.')
+    print ('')
+
+    for i in range(m):
+        print ('Hint Unfold upaco'+str(n)+lev(m)+idx(m,i)+'.')
+    for i in range(m):
+        print ('Hint Resolve paco'+str(n)+lev(m)+idx(m,i)+'_fold.')
+    print ('Hint Unfold monotone'+str(n)+lev(m)+'.')
+    print ('')
diff --git a/src/paco0.v b/src/paco0.v
@@ -231,6 +231,19 @@ Qed.
 
 End Arg0_1.
 
+Arguments paco0_acc : clear implicits.
+Arguments paco0_mon : clear implicits.
+Arguments paco0_mult_strong : clear implicits.
+Arguments paco0_mult : clear implicits.
+Arguments paco0_fold : clear implicits.
+Arguments paco0_unfold : clear implicits.
+
+Global Instance paco0_inst  (gf : rel0->_) r : paco_class (paco0 gf r) :=
+{ pacoacc    := paco0_acc gf;
+  pacomult   := paco0_mult gf;
+  pacofold   := paco0_fold gf;
+  pacounfold := paco0_unfold gf }.
+
 (** 2 Mutual Coinduction *)
 
 Section Arg0_2.
@@ -408,6 +421,31 @@ Qed.
 
 End Arg0_2.
 
+Arguments paco0_2_0_acc : clear implicits.
+Arguments paco0_2_1_acc : clear implicits.
+Arguments paco0_2_0_mon : clear implicits.
+Arguments paco0_2_1_mon : clear implicits.
+Arguments paco0_2_0_mult_strong : clear implicits.
+Arguments paco0_2_1_mult_strong : clear implicits.
+Arguments paco0_2_0_mult : clear implicits.
+Arguments paco0_2_1_mult : clear implicits.
+Arguments paco0_2_0_fold : clear implicits.
+Arguments paco0_2_1_fold : clear implicits.
+Arguments paco0_2_0_unfold : clear implicits.
+Arguments paco0_2_1_unfold : clear implicits.
+
+Global Instance paco0_2_0_inst  (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_0 gf_0 gf_1 r_0 r_1) :=
+{ pacoacc    := paco0_2_0_acc gf_0 gf_1;
+  pacomult   := paco0_2_0_mult gf_0 gf_1;
+  pacofold   := paco0_2_0_fold gf_0 gf_1;
+  pacounfold := paco0_2_0_unfold gf_0 gf_1 }.
+
+Global Instance paco0_2_1_inst  (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_1 gf_0 gf_1 r_0 r_1) :=
+{ pacoacc    := paco0_2_1_acc gf_0 gf_1;
+  pacomult   := paco0_2_1_mult gf_0 gf_1;
+  pacofold   := paco0_2_1_fold gf_0 gf_1;
+  pacounfold := paco0_2_1_unfold gf_0 gf_1 }.
+
 (** 3 Mutual Coinduction *)
 
 Section Arg0_3.
@@ -661,73 +699,6 @@ Qed.
 
 End Arg0_3.
 
-End PACO0.
-
-Global Opaque paco0.
-
-Hint Unfold upaco0.
-Hint Resolve paco0_fold.
-Hint Unfold monotone0.
-
-Arguments paco0_acc : clear implicits.
-Arguments paco0_mon : clear implicits.
-Arguments paco0_mult_strong : clear implicits.
-Arguments paco0_mult : clear implicits.
-Arguments paco0_fold : clear implicits.
-Arguments paco0_unfold : clear implicits.
-
-Instance paco0_inst  (gf : rel0->_) r : paco_class (paco0 gf r) :=
-{ pacoacc    := paco0_acc gf;
-  pacomult   := paco0_mult gf;
-  pacofold   := paco0_fold gf;
-  pacounfold := paco0_unfold gf }.
-
-Global Opaque paco0_2_0.
-Global Opaque paco0_2_1.
-
-Hint Unfold upaco0_2_0.
-Hint Unfold upaco0_2_1.
-Hint Resolve paco0_2_0_fold.
-Hint Resolve paco0_2_1_fold.
-Hint Unfold monotone0_2.
-
-Arguments paco0_2_0_acc : clear implicits.
-Arguments paco0_2_1_acc : clear implicits.
-Arguments paco0_2_0_mon : clear implicits.
-Arguments paco0_2_1_mon : clear implicits.
-Arguments paco0_2_0_mult_strong : clear implicits.
-Arguments paco0_2_1_mult_strong : clear implicits.
-Arguments paco0_2_0_mult : clear implicits.
-Arguments paco0_2_1_mult : clear implicits.
-Arguments paco0_2_0_fold : clear implicits.
-Arguments paco0_2_1_fold : clear implicits.
-Arguments paco0_2_0_unfold : clear implicits.
-Arguments paco0_2_1_unfold : clear implicits.
-
-Instance paco0_2_0_inst  (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_0 gf_0 gf_1 r_0 r_1) :=
-{ pacoacc    := paco0_2_0_acc gf_0 gf_1;
-  pacomult   := paco0_2_0_mult gf_0 gf_1;
-  pacofold   := paco0_2_0_fold gf_0 gf_1;
-  pacounfold := paco0_2_0_unfold gf_0 gf_1 }.
-
-Instance paco0_2_1_inst  (gf_0 gf_1 : rel0->_) r_0 r_1 : paco_class (paco0_2_1 gf_0 gf_1 r_0 r_1) :=
-{ pacoacc    := paco0_2_1_acc gf_0 gf_1;
-  pacomult   := paco0_2_1_mult gf_0 gf_1;
-  pacofold   := paco0_2_1_fold gf_0 gf_1;
-  pacounfold := paco0_2_1_unfold gf_0 gf_1 }.
-
-Global Opaque paco0_3_0.
-Global Opaque paco0_3_1.
-Global Opaque paco0_3_2.
-
-Hint Unfold upaco0_3_0.
-Hint Unfold upaco0_3_1.
-Hint Unfold upaco0_3_2.
-Hint Resolve paco0_3_0_fold.
-Hint Resolve paco0_3_1_fold.
-Hint Resolve paco0_3_2_fold.
-Hint Unfold monotone0_3.
-
 Arguments paco0_3_0_acc : clear implicits.
 Arguments paco0_3_1_acc : clear implicits.
 Arguments paco0_3_2_acc : clear implicits.
@@ -747,21 +718,50 @@ Arguments paco0_3_0_unfold : clear implicits.
 Arguments paco0_3_1_unfold : clear implicits.
 Arguments paco0_3_2_unfold : clear implicits.
 
-Instance paco0_3_0_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
+Global Instance paco0_3_0_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_0 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
 { pacoacc    := paco0_3_0_acc gf_0 gf_1 gf_2;
   pacomult   := paco0_3_0_mult gf_0 gf_1 gf_2;
   pacofold   := paco0_3_0_fold gf_0 gf_1 gf_2;
   pacounfold := paco0_3_0_unfold gf_0 gf_1 gf_2 }.
 
-Instance paco0_3_1_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
+Global Instance paco0_3_1_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_1 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
 { pacoacc    := paco0_3_1_acc gf_0 gf_1 gf_2;
   pacomult   := paco0_3_1_mult gf_0 gf_1 gf_2;
   pacofold   := paco0_3_1_fold gf_0 gf_1 gf_2;
   pacounfold := paco0_3_1_unfold gf_0 gf_1 gf_2 }.
 
-Instance paco0_3_2_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
+Global Instance paco0_3_2_inst  (gf_0 gf_1 gf_2 : rel0->_) r_0 r_1 r_2 : paco_class (paco0_3_2 gf_0 gf_1 gf_2 r_0 r_1 r_2) :=
 { pacoacc    := paco0_3_2_acc gf_0 gf_1 gf_2;
   pacomult   := paco0_3_2_mult gf_0 gf_1 gf_2;
   pacofold   := paco0_3_2_fold gf_0 gf_1 gf_2;
   pacounfold := paco0_3_2_unfold gf_0 gf_1 gf_2 }.
 
+End PACO0.
+
+Global Opaque paco0.
+
+Hint Unfold upaco0.
+Hint Resolve paco0_fold.
+Hint Unfold monotone0.
+
+Global Opaque paco0_2_0.
+Global Opaque paco0_2_1.
+
+Hint Unfold upaco0_2_0.
+Hint Unfold upaco0_2_1.
+Hint Resolve paco0_2_0_fold.
+Hint Resolve paco0_2_1_fold.
+Hint Unfold monotone0_2.
+
+Global Opaque paco0_3_0.
+Global Opaque paco0_3_1.
+Global Opaque paco0_3_2.
+
+Hint Unfold upaco0_3_0.
+Hint Unfold upaco0_3_1.
+Hint Unfold upaco0_3_2.
+Hint Resolve paco0_3_0_fold.
+Hint Resolve paco0_3_1_fold.
+Hint Resolve paco0_3_2_fold.
+Hint Unfold monotone0_3.
+