Introduced tuples of arbitrary length, tuple datatypes for lengths 2 …

…to 5 are predefined.

definition_processor.sml

@@ -1926,14 +1926,15 @@ fun addFSymDefInfoAndCompile(p,
         | SOME({fsym=f,right_syms=right_syms,left_syms=left_syms,guard_syms=guard_syms',defining_props=defining_props,...}) => 
             if MS.modSymEq(f,Names.mequal_logical_symbol) orelse Data.isFreeStructureConstructor(f) then NONE
             else 
-                let val _ = debugPrint("\nThis is a defining equation. Here is the asserted sentence:\n"^(pprint(0,p))^
+                let val _ = debugPrint("\nThis is a defining equation, for symbol: " ^ (MS.name f)
+				       ^ "\nHere is the asserted sentence:\n"^(pprint(0,p))^
                                        "\nand here are its defining props:\n"^(Basic.printListStr(defining_props,(fn p => pprint(0,p)),"\n"))^
                                        "\nand here are the right_syms: "^(Basic.printListStr(right_syms,MS.name,",")))
 		    val left_syms = Basic.removeEq(f,left_syms,MS.modSymEq)
 		    val mod_names = map Symbol.name mod_path
 		    val mod_path_string_with_dots = Basic.printListStr(mod_names,fn x => x,".")
 		    val _ = debugPrint("\nProper mod path: " ^ mod_path_string_with_dots ^ "\n")
-	            val already_defined = ref(false)
+	            val already_defined = ref(false)                   					    
                     val abort = 
                           (case MS.find(Prop.fsym_def_table,f) of
                               SOME({eval_proc_name=ep_name,guard_syms=gsyms,occurring_syms=osyms,needed_by=nb,obsolete_axioms=obs_axioms,

lib/basic/util.ath

@@ -5002,3 +5002,13 @@ define (make-datatype datatype-name constructor-letter N) :=
        cmd := (join "datatype " datatype-name " := " (separate constructors " | "))}
            (process-input-from-string cmd)
 
+define (define-tuple-datatype n) :=
+  let {n-str := (val->string n);
+       sort-params := (separate (map lambda (i) (join "S" (val->string i))
+                                     (1 to n))
+                                " ");                                      
+       selectors := (separate (map lambda (i) (join n-str "-tuple-" (val->string i) ":S" (val->string i))
+                                   (1 to n))
+                              " ");                                    
+       cmd := (join "datatype (" n-str "-Tuple " sort-params ") := (" n-str "-tuple " selectors ")")}
+    (process-input-from-string cmd)    

repl.sml

@@ -889,6 +889,11 @@ fun init(file_name_option) =
          val _ = auxLoadFiles(top_files, [],Semantics.top_val_env,Semantics.top_val_env,top_loaded_files_ht)
              handle e => (print("\nEvaluation error encountered during the loading of the initial files:\n");
                           handleException(e))
+         val _ = List.app (fn i => let val cmd = "(define-tuple-datatype " ^ i ^ ")"
+                                   in
+                                      processString(cmd,mod_path,env,eval_env)
+                                   end)
+                          ["2", "3", "4", "5"]
 (** Making private the names of all Athena functions that are by default called by SML code: **)         
          val _ = SM.makePrivateLst(["diff*", "evaluate","compile-symbols", "compile-symbols-simple", "compile-symbols-simple-with-default",
 	                            "auto-induction-definition",