Fixing issue sparverius#4.

DATS/classify_toks.dats

@@ -109,8 +109,14 @@ parse_two(xs) = let
       ifcase
       | tok_ide_eq(h, "the") &&
         tok_ide_eq(e, "static") &&
-        tok_ide_eq(y, "expression") => @(x0, x1, ERRsimpre(x2))
-      | _ => @(x0, x1, ERRexit2(x2))
+        tok_ide_eq(y, "expression") => (
+
+          ifcase
+          | tok_ide_eq(hey, "is") => @(x0, x1, ERRssort(x2))
+          | tok_ide_eq(hey, "of") => @(x0, x1, ERRssort(x2))
+          | (*else*)_ => @(x0, x1, ERRsimpre(x2))
+        )
+      | _ => (print "exit2";@(x0, x1, ERRexit2(x2)))
     ): errtup
     val () = free_token3(h,e,y)
     val () = free_token(hey)  
@@ -294,4 +300,4 @@ end
 
 (* ****** ****** *) 
 
-(* end of [classify_toks.dats] *)
+(* end of [classify_toks.dats] *)

DATS/errkind.dats

@@ -48,6 +48,7 @@ free_errkind
       | ~ERRnonex  l => free_toks(l)
       | ~ERRlast   l => (free_toktup(l))
       | ~ERRunit   _ => ()
+      | ~ERRssort  l => free_toks(l)
       //
       | ~ERRsimpre  l => free_toks(l)
   )
@@ -76,6 +77,7 @@ get_errkind_string
     | ERRsortu  _ => "ERRsortu"
     | ERRnonex  _ => "ERRnonex"
     | ERRunit   _ => "ERRunit"
+    | ERRssort  _ => "ERRssort"
     //
     | ERRsimpre _ => "ERRstaimpre"
 
@@ -101,6 +103,7 @@ implement{} print_show   (xs: toks, color: bool, verbose: bool): void = (free_to
 implement{} print_warn   (xs: toks, color: bool, verbose: bool): void = (free_toks(xs))
 implement{} print_unit   ((*    *)): void = ()
 implement{} print_last (xs: toktup, color: bool, verbose: bool): void = (free_toktup(xs))
+implement{} print_ssort  (xs: toks, color: bool, verbose: bool): void = (free_toks(xs))
 //
 implement{} print_simpre (xs: toks, color: bool, verbose: bool): void = (free_toks(xs))
 
@@ -127,6 +130,7 @@ print_errkind_single
   | ~ERRlast   x => print_last<>(x, color, verbose)
   | ~ERRwarn   x => print_warn<>(x, color, verbose)
   | ~ERRunit   _ => print_unit<>( )
+  | ~ERRssort  x => print_ssort<>(x, color, verbose)
   //
   | ~ERRsimpre x => print_simpre<>(x, color, verbose)
 ) 

DATS/print_errkind.dats

@@ -684,7 +684,53 @@ end
 implement{}
 print_unit(): void = print "ERRunit"
 
+implement{}
+print_ssort
+(xs, color, verbose) = let
+  // the static expression
+  //
+  //   [, s2e, ] is expected to be of a functional sort but is assigned sort [, s2e, ]
+  //   is of the sort [, s2e, ] but it is expected to be the sort [, s2e, ]
+  val (err, rest1) = takeskip_until_in_free(xs, lam i => is_col(i))
+
+  val rest = skip_while_free (rest1, lam i => is_spc(i))  
+  val (bef, aft) = takeskip_until_free (rest, lam i => is_osq i)
+
+  val (exp_sort, aft) = peek_square_list_osq (aft)
+  val _is = get_token_n_ide (aft, 0)
+  val exp_of = get_token_n_ide (aft, 1)  
+
+  val (txt1, aft) = takeskip_until_free (aft, lam i => is_osq i)
+  val txt = skip_while_free (txt1, lam i => is_spc(i))
+  val (expected, aft) = peek_square_list_osq (aft)
+in
+  print_error(err, color);
+
+  free_token(_is);
+  free_token(exp_of);
+  print_toks_free_nonewln(bef);
+
+  print_after_message("");
+
+  print "[ ";
+  simplify_print(exp_sort, color, verbose);
+  print " ]";
+
+  print_after_message("");
+
+  print_toks_free_nonewln(txt);
+
+  print_after_message("");
+
+  print "[ ";
+  simplify_print(expected, color, verbose);
+  print " ]";
+
+  print_toks_free_nonewln(aft);
+
+  print_after_all;
+end
 
 (* ****** ****** *)
 
-(* end of [print_errkind.dats] *)
+(* end of [print_errkind.dats] *)

DATS/simplify_print.dats

@@ -696,18 +696,39 @@ implmnt(*{}*)
 simplify_S2RTbas
 (x0: token, xs0: toks, verbose: bool) : (toks, toks) = let
   // datatype s2rt = | S2RTbas of s2rtbas (* base sort *)
-// old version -- doesnt work really
-  val all = skip_until_in_free(xs0, lam i => is_sco(i))
-  val all = drop_exn_free(all, 0)
-  (* val res = take_until_free2(all, lam i => is_cpr(i)) *)
-  val (res, rest) = takeskip_until_free(all, lam i => is_cpr(i))
-  val rest = drop_exn_free(rest,1)
-  val () = free_token(x0)
-  (* val res = cons_vt(x0, xs0) *)
-  (* val rest = nil_vt() *)
-
+  val knd = get_token_at_unsafe (xs0, 1)
 in
-  (res, rest)
+  ifcase
+  | tok_s2e_eq(knd, "S2RTBASimp") => let
+      val all = skip_until_in_free(xs0, lam i => is_sco(i))
+      val all = drop_exn_free(all, 0)
+      val (res, rest) = takeskip_until_free(all, lam i => is_cpr(i))
+      val rest = drop_exn_free(rest,1)
+      val () = free_token(x0)
+      val () = free_token(knd)
+    in
+      (res, rest)
+    end
+ | tok_s2e_eq(knd, "S2RTBASpre") => let
+      val all = skip_until_in_free(xs0, lam i => is_opr(i))
+      val all = drop_exn_free(all, 0)
+      val (res, rest) = peek_paren_list_opr(all)
+
+      val name = get_token_at_unsafe(res, 1)
+      val () = free_toks (res)
+      val res = cons_vt(name, nil_vt())
+
+      val rest = drop_exn_free(rest, 0)
+      val () = free_token(x0)
+      val () = free_token(knd)
+    in
+      (res, rest)
+    end
+ | (*S2RTBASdef*)_ => (
+    // TODO: handle this case too
+    print_toks(xs0);
+    free_token(x0); free_token(knd); (list_vt_nil(), xs0)
+  )
 end
 
 

Makefile

@@ -26,7 +26,7 @@ all::
 #
 
 all:: ; make -C $(DIR) && printf "$?" && echo "Build Successful" \
-|| printf "\nBuilding acc Failed\n" 
+|| printf "\nBuilding acc Failed\n"
 all:: ; [ -f "./DATS/acc" ] && mv ./DATS/acc .
 
 #
@@ -66,7 +66,7 @@ testrun:: ; @printf "\e[33mbuilding...\e[0m\n"
 testrun:: test0
 testrun:: ; @printf "\e[36mrunning tests... \e[0m\n" && printf "\e[36m>>>\e[0m\n"
 testrun:: ; @printf "Each test will output the current error message (with patscc) and the corresponding pretty-printed message (with acc)\n"
-testrun:: ; -@sh ./TEST/tests.sh
+testrun:: ; -@bash ./TEST/tests.sh
 
 ######
 

SATS/errkind.sats

@@ -23,6 +23,8 @@ datavtype errkind =
   | ERRlast   of toktup // the summary i.e. "exit(ATS): ..."
   | ERRunit   of () 
 //(*
+  | ERRssort of toks   // the static expression [...] is expected to be of functional sort but it is assigned the sort [...]
+                       // the static expression [...] is of the sort [...] but it is expected to be of the sort [...]
   | ERRsimpre of toks  // the static expression needs to be impredicative 
                          // but it is assigned the sort [...].
 //*)

SATS/errkind_util.sats

@@ -82,6 +82,9 @@ print_unit((* *)): void
 fun{}
 print_last(xs: toktup, color: bool, verbose: bool): void
 
+fun{}
+print_ssort(xs: toks, color: bool, verbose: bool): void
+
 //(*
 fun{}
 print_simpre(xs: toks, color: bool, verbose: bool): void
@@ -106,4 +109,4 @@ fn
 free_errtups
 (xs: errtups): void 
 
-(* ****** ****** *)
+(* ****** ****** *)

TEST/s2e_funsort.dats

@@ -0,0 +1,10 @@
+// thanks to @chantisnake for providing this sample
+
+// Part D: formulate and prove the associativity of or, namely
+// that (X || Y) || Z and X || (Y || Z) are equivalent / the same
+absprop PEQ (A: prop, B: prop)
+propdef <->(A: prop, B: prop) = PEQ(A, B) 
+
+extern praxi peq_intro {A, B: prop}: (A ->> B) && (B ->> A) -> (A <-> B)
+extern praxi peq_elim_from_right {A, B: prop}: (A <-> B) -> B -> A 
+extern praxi peq_elim_from_left {A, B: prop}: (A <-> B) -> A -> B

TEST/tests.sh

@@ -5,6 +5,7 @@ files=( "./TEST/cfail.dats"
 	# "./TEST/fail2.dats"
 	"./TEST/list0_tests.dats"
 	"./TEST/show6.dats"
+        "./TEST/s2e_funsort.dats"
       )
 
 ESC_CODE="\e["
@@ -127,20 +128,20 @@ valgrind_message_patscc="
 ==20540== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
 ==20540== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
 ==20540== Command: patscc -tcats ./TEST/failure.dats
-==20540== 
-==20540== 
+==20540==
+==20540==
 ==20540== HEAP SUMMARY:
 ==20540==     in use at exit: 95 bytes in 6 blocks
 ==20540==   total heap usage: 12 allocs, 6 frees, 1,199 bytes allocated
-==20540== 
+==20540==
 ==20540== LEAK SUMMARY:
 ==20540==    definitely lost: 15 bytes in 1 blocks
 ==20540==    indirectly lost: 0 bytes in 0 blocks
 ==20540==      possibly lost: 0 bytes in 0 blocks
 ==20540==    still reachable: 80 bytes in 5 blocks
 ==20540==         suppressed: 0 bytes in 0 blocks
 ==20540== Rerun with --leak-check=full to see details of leaked memory
-==20540== 
+==20540==
 ==20540== For counts of detected and suppressed errors, rerun with: -v
 ==20540== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
 "
@@ -150,14 +151,14 @@ valgrind_message_acc="
 ==20543== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
 ==20543== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
 ==20543== Command: ./acc -tcats ./TEST/failure.dats
-==20543== 
-==20543== 
+==20543==
+==20543==
 ==20543== HEAP SUMMARY:
 ==20543==     in use at exit: 0 bytes in 0 blocks
 ==20543==   total heap usage: 1,140 allocs, 1,140 frees, 35,594 bytes allocated
-==20543== 
+==20543==
 ==20543== All heap blocks were freed -- no leaks are possible
-==20543== 
+==20543==
 ==20543== For counts of detected and suppressed errors, rerun with: -v
 ==20543== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
 "
@@ -171,7 +172,7 @@ show_valgrind_test() {
 
     if [ "$(get_status "valgrind")" -eq "0" ]; then
 	# if valgrind command exists
-	
+
 	print_two_colors "$BOLD" "$LIGHTMAGENTA"
 	printf "patscc"
 	print_color_close
@@ -195,7 +196,7 @@ show_valgrind_test() {
 
 	valgrind ./acc -tcats "$errs" | grep --color=none "^=="
 
-	echo 
+	echo
     else
 	echo "valgrind is not installed"
 	echo "the output would be similar to below"
@@ -216,7 +217,7 @@ show_valgrind_test() {
 	echo "$valgrind_message_acc"
     fi
     print_test_end "4"
-    echo "$valgrind_message"    
+    echo "$valgrind_message"
 }
 
 
@@ -231,8 +232,8 @@ print_end_all_test() {
 
 show_patscc_vs_acc_tests() {
     c=0
-    for (( c=0; c<=3; c++ ))
-    do  
+    for (( c=0; c<=4; c++ ))
+    do
 	print_test "$c"
 	echo
 	# echo "File: ${files[$c]}"