/% input file for pervasives files generation %/ /% section I: pervasive kinds %/ /% number of pervasive kinds %/ KIND 7 /% kind data table %/ /% index name index_name arity %/ /* int */ 0 int int 0 ;; /* real */ 1 real real 0 ;; /* bool */ 2 o bool 0 ;; /* string */ 3 string string 0 ;; /* list type constructor */ 4 list list 1 ;; /* in_stream */ 5 in_stream instream 0 ;; /* out_stream */ 6 out_stream outstream 0 /% section II: pervasive constants and their type skeletons %/ /% section II.I : type skeletion and constant declarations %/ /% number of pervasive constants %/ CONST 94 /% number of type skeletons %/ TYPE SKEL 42 /% type skeleton and constant data table %/ /% type skeleton format: [comments] TYPE index type %/ /% constant format: index name indname tesize neededness typerv redef prec fixity codeinfo %/ /* A */ TYPE 0 #0 /* for unnamed universal constants (Note: tesize should be 0)*/ 85 univ 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* (list A) */ TYPE 1 (@ list 1 [#0]) /* nil */ 89 nil nil 0 1 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* A->(list A)->(list A) */ TYPE 2 #0 -> (@ list 1 [#0]) -> (@ list 1 [#0]) /* cons */ 93 :: cons 0 1 0 TRUE FALSE 140 INFIXR NOCODE ;; /* int */ TYPE 3 int /* integer constant */ 90 intc 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* real */ TYPE 4 real /* real constant */ 91 realc 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* string */ TYPE 5 string /* string constant */ 92 strc 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* o (type of proposition)*/ TYPE 6 bool /* true proposition */ 4 true true 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE /* cut predicate */ 5 ! cut 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE /* fail predicate */ 6 fail fail 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE /* halt the system */ 9 halt halt 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE /* return to top level */ 10 stop stop 0 0 0 TRUE FALSE 0 NOFIXITY NOCODE ;; /* int -> int */ TYPE 7 int -> int /* unary minus on integers */ 56 %i~ intuminus 0 0 0 TRUE FALSE MAX PREFIX NOCODE - /* modulus */ 61 mod mod 0 0 0 TRUE TRUE 160 INFIXL NOCODE /* integer abs */ 63 %iabs iabs 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE abs ;; /* int -> int -> int */ TYPE 8 int -> int -> int /* addition on integers */ 57 %i+ intplus 0 0 0 TRUE FALSE 150 INFIXL NOCODE + /* subtraction on integers */ 58 %i- intminus 0 0 0 TRUE FALSE 150 INFIXL NOCODE - /* mutiplication on integers */ 59 %i* intmult 0 0 0 TRUE FALSE 160 INFIXL NOCODE * /* integer division */ 60 div intdiv 0 0 0 TRUE FALSE 160 INFIXL NOCODE ;; /* int -> int -> o */ TYPE 9 int -> int -> bool /* less than on integers */ 19 %i< intlss 0 0 0 TRUE FALSE 130 INFIX 4 < /* greater than on integers */ 20 %i> intgrt 0 0 0 TRUE FALSE 130 INFIX 5 > /* less than or eq on integers */ 21 %i<= intleq 0 0 0 TRUE FALSE 130 INFIX 6 <= /* greater than or eq on integers*/ 22 %i>= intgeq 0 0 0 TRUE FALSE 130 INFIX 7 >= /* time predicate */ 51 time time 0 0 0 TRUE TRUE 0 NOFIXITY 36 ;; /* int -> real */ TYPE 10 int -> real /* coercion to real */ 62 int_to_real itor 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* real -> int */ TYPE 11 real -> int /* floor function */ 74 floor floor 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* ceiling function */ 75 ceil ceil 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* truncation */ 76 truncate trunc 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* real -> real */ TYPE 12 real -> real /* unary minus on real */ 64 %r~ realuminus 0 0 0 TRUE FALSE MAX PREFIX NOCODE - /* square root */ 69 sqrt sqrt 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* sine */ 70 sin sin 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* cosine */ 71 cos cos 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* arc tan */ 72 arctan arctan 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* natural log */ 73 ln log 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* real abs */ 77 %rabs rabs 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE rabs ;; /* real -> string */ TYPE 13 real -> string /* real to string */ 84 real_to_string rtos 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* real -> real -> real */ TYPE 14 real -> real -> real /* addition on reals */ 65 %r+ realplus 0 0 0 TRUE FALSE 150 INFIXL NOCODE + /* subtraction on reals */ 66 %r- realminus 0 0 0 TRUE FALSE 150 INFIXL NOCODE - /* multiplication on reals */ 67 %r* realmult 0 0 0 TRUE FALSE 160 INFIXL NOCODE * /* division */ 68 / realdiv 0 0 0 TRUE FALSE 160 INFIXL NOCODE ;; /* real -> real -> o */ TYPE 15 real -> real -> bool /* less than in reals */ 23 %r< reallss 0 0 0 TRUE FALSE 130 INFIX 8 < /* greater than on reals */ 24 %r> realgrt 0 0 0 TRUE FALSE 130 INFIX 9 > /* less than or eq on reals */ 25 %r<= realleq 0 0 0 TRUE FALSE 130 INFIX 10 <= /* greater than or eq on reals */ 26 %r>= realgeq 0 0 0 TRUE FALSE 130 INFIX 11 >= ;; /* string -> int */ TYPE 16 string -> int /* string length */ 79 size slen 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* ord function */ 81 string_to_int stoi 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* int -> string */ TYPE 17 int -> string /* chr function */ 80 chr itochr 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* int to string */ 83 int_to_string itostr 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* string -> string -> string */ TYPE 18 string -> string -> string /* string concatination */ 78 ^ scat 0 0 0 TRUE TRUE 150 INFIXL NOCODE ;; /* string -> string -> o */ TYPE 19 string -> string -> bool /* less than on strings */ 27 %s< strlss 0 0 0 TRUE TRUE 130 INFIX 12 < /* greater than on strings */ 28 %s> strgrt 0 0 0 TRUE TRUE 130 INFIX 13 > /* less than or eq on strings */ 29 %s<= strleq 0 0 0 TRUE TRUE 130 INFIX 14 <= /* greater than or eq on strings */ 30 %s>= strgeq 0 0 0 TRUE TRUE 130 INFIX 15 >= /* getenv predicate; needed? */ 49 getenv getenv 0 0 0 TRUE TRUE 0 NOFIXITY 34 ;; /* string -> int -> int -> string */ TYPE 20 string -> int -> int -> string /* substring */ 82 substring substr 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* o -> o -> o */ TYPE 21 bool -> bool -> bool /* logical and */ 0 , and 0 0 0 TRUE FALSE 110 INFIXL NOCODE /* logical or */ 1 ; or 0 0 0 TRUE FALSE 100 INFIXL NOCODE /* another logical and */ 8 & ampand 0 0 0 TRUE FALSE 120 INFIXR NOCODE /* Prolog if; needed? */ 11 :- colondash 0 0 0 TRUE FALSE 0 INFIXL NOCODE /* implication; needed? */ 12 => impl 0 0 0 TRUE FALSE 130 INFIXR NOCODE ;; /* (A -> o) -> o */ TYPE 22 (#0 -> bool) -> bool /* existential quantifier */ 2 sigma some 1 1 1 FALSE FALSE 0 NOFIXITY NOCODE /* universal quantifier */ 3 pi all 1 1 1 FALSE FALSE 0 NOFIXITY NOCODE ;; /* A -> A -> o */ TYPE 23 #0 -> #0 -> bool /* is */ 16 is is 1 1 1 FALSE FALSE 130 INFIX 1 /* equality (unify) predicate */ 18 = eq 1 1 1 FALSE FALSE 130 INFIX 3 ;; /* in_stream */ TYPE 24 instream /* std_in */ 86 std_in stdin 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* out_stream */ TYPE 25 outstream /* std_out */ 87 std_out stdout 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE /* std_err */ 88 std_err stderr 0 0 0 TRUE TRUE 0 NOFIXITY NOCODE ;; /* string -> in_stream -> o */ TYPE 26 string -> instream -> bool /* open_in */ 31 open_in openin 0 0 0 TRUE TRUE 0 NOFIXITY 16 /* open_string */ 36 open_string openstr 0 0 0 TRUE TRUE 0 NOFIXITY 21 ;; /* string -> out_stream -> o */ TYPE 27 string -> outstream -> bool /* open_out */ 32 open_out openout 0 0 0 TRUE TRUE 0 NOFIXITY 17 /* open_append */ 33 open_append openapp 0 0 0 TRUE TRUE 0 NOFIXITY 18 ;; /* in_stream -> o */ TYPE 28 instream -> bool /* close_in */ 34 close_in closein 0 0 0 TRUE TRUE 0 NOFIXITY 19 /* eof */ 41 eof eof 0 0 0 TRUE TRUE 0 NOFIXITY 26 ;; /* out_stream -> o */ TYPE 29 outstream -> bool /* close_out */ 35 close_out closeout 0 0 0 TRUE TRUE 0 NOFIXITY 20 /* flush */ 42 flush flush 0 0 0 TRUE TRUE 0 NOFIXITY 27 ;; /* A -> string -> o */ TYPE 30 #0 -> string -> bool /* term_to_string */ 46 term_to_string termtostr 1 1 0 FALSE TRUE 0 NOFIXITY 31 ;; /* string -> A -> o */ TYPE 31 string -> #0 -> bool /* string_to_term */ 47 string_to_term strtoterm 1 1 1 FALSE TRUE 0 NOFIXITY 32 ;; /* out_stream -> string -> o */ TYPE 32 outstream -> string -> bool /* output */ 38 output output 0 0 0 TRUE TRUE 0 NOFIXITY 23 ;; /* in_stream -> int -> string -> o */ TYPE 33 instream -> int -> string -> bool /* input */ 37 input input 0 0 0 TRUE TRUE 0 NOFIXITY 22 ;; /* in_stream -> string -> o */ TYPE 34 instream -> string -> bool /* input_line */ 39 input_line inputline 0 0 0 TRUE TRUE 0 NOFIXITY 24 /* lookahead */ 40 lookahead lookahead 0 0 0 TRUE TRUE 0 NOFIXITY 25 ;; /* string -> o */ TYPE 35 string -> bool /* print */ 43 print print 0 0 0 TRUE TRUE 0 NOFIXITY 28 ;; /* A -> o */ TYPE 36 #0 -> bool /* read */ 44 read read 1 1 1 FALSE TRUE 0 NOFIXITY 29 ;; /* out_stream -> A -> o */ TYPE 37 outstream -> #0 -> bool /* printterm */ 45 printterm printterm 1 1 0 FALSE TRUE 0 NOFIXITY 30 ;; /* in_stream -> A -> o */ TYPE 38 instream -> #0 -> bool /* readterm */ 48 readterm readterm 1 1 1 FALSE TRUE 0 NOFIXITY 33 ;; /* o -> o */ TYPE 39 bool -> bool /* solve; used by code generator */ 15 solve solve 0 0 0 TRUE FALSE 0 NOFIXITY 0 /* not */ 17 not not 0 0 0 TRUE FALSE 0 NOFIXITY 2 ;; /* string -> int -> in_stream -> out_stream -> o */ TYPE 40 string -> int -> instream -> outstream -> bool /* open_socket predicate */ 50 open_socket opensocket 0 0 0 FALSE TRUE 0 NOFIXITY 35 ;; /* string -> int -> o */ TYPE 41 string -> int -> bool /* system predicate */ 52 system system 0 0 0 FALSE TRUE 0 NOFIXITY 37 /% pervasive constant classification %/ LOGIC SYMBOL 11 LS_START and LS_END stop /% logic symbol types %/ 0 and 1 or 2 some 3 all 4 l_true 5 cut 6 fail 7 eq 8 ampand 9 halt 10 stop PRED SYMBOL 37 PRED_START solve PRED_END system REGCL solve not getenv strtoterm readterm read is lookahead input inputline BACKTRACK eq