Standard.hop

!!! ---------------------------------------------------- !!!
!!!                                                      !!!
!!! Hope default environment (adapted/reorganized).      !!!
!!! Standard.hop original by Professor Ross Paterson     !!!
!!!                                                      !!!
!!! Augusto Manzano (2022) - www.canal.manzano.pro.br    !!!
!!!                                                      !!!
!!!                Version 2.1.0 - 2026                  !!!
!!!                                                      !!!
!!! This file should be used instead of the original     !!!
!!! Hope language file on your system.                   !!!
!!!                                                      !!!
!!! This is free software an experimental programming    !!!
!!! language. There is none guarantee that this tool     !!!
!!! will lead you to the expected results, nor for       !!!
!!! commercialization or suitability for a certain       !!!
!!! purpose. Its original author and the developers who  !!!
!!! continue the work cannot or may at any time be held  !!!
!!! responsible.                                         !!!
!!!                                                      !!!
!!! Tested only on Windows Operating System with an      !!!
!!! interpreter coded by Marcos Alfaro.                  !!!
!!! http://hopelang.blogspot.com/                        !!!
!!!                                                      !!!
!!! ---------------------------------------------------- !!!


!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!! >>> infix/infixr operators                       <<< !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

infixr ->, o, /\, || : 2;
infixr #, X, U       : 4;
infixr ::, <>, &     : 5; 
infixr **, ^         : 7; 

infix or               : 1;
infix and              : 2; 
infix =, /=            : 3;
infix <, =<, >, >=, .. : 4;
infix +, -             : 5;
infix *, /, div, mod   : 6;
infix ., @             : 9;


!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! 
!!! >>> Type variables and other resources           <<< !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

typevar alpha, beta, gamma, delta, epsilon, dzeta, eta, teta, iota, apa;

abstype char;  
abstype neg -> pos;
abstype pos # pos;
abstype set pos;

data list alpha == nil ++ alpha :: list alpha;
data num        == succ num;
data ordering   == LT ++ EQ ++ GT; 
data relation   == LESS ++ EQUAL ++ GREATER;
data sorting    == ascending ++ descending;   
data truval     == false ++ true;  
data void       == Nothing;  
 
type alpha X beta == alpha # beta;
type set alpha    == list alpha;


!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!! >>> Math constants                               <<< !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

!!! C++ style

dec m_1_sqrt_2        : num; 
dec m_2_sqrt_pi       : num; 
dec m_epsilon         : num;
dec m_eulerMascheroni : num;
dec m_huge            : num;
dec m_ln_sqrt_2_pi    : num; 
dec m_max_exp         : num;
dec m_max_log         : num;
dec m_min_log         : num;
dec m_sqrt_2          : num; 
dec m_sqrt_2_pi       : num; 
dec m_sqrt_eps        : num; 
dec m_tiny            : num;

!!! Other constants - general use

dec e       : num;
dec deg     : num;
dec pi      : num;
dec rad     : num;
dec sqrt_pi : num;
dec tau     : num;


!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!! >>> General operators / functions                <<< !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

!!! Operators
    
dec **, ^               : num # num -> num;
dec .                   : alpha # (alpha -> beta) -> beta;
dec ..                  : num # num -> list num;
dec /\                  : (alpha -> beta) # (alpha -> beta') -> alpha -> beta # beta';
dec @                   : list alpha # num -> alpha;
dec +, -, *, /          : num # num -> num;
dec <>                  : list alpha # list alpha -> list alpha;
dec =, /=, <, =<, >, >= : alpha # alpha -> truval;
dec o                   : (beta -> gamma) # (alpha -> beta) -> alpha -> gamma; 
dec ||                  : list (alpha) # list (beta) -> list (alpha # beta);


!!! Various functions - general use

dec argv           : list (list char);
dec cbrt           : num -> num;
dec ceiling        : num -> num;
dec choose         : set alpha -> alpha # set alpha;
dec const          : alpha # beta -> alpha;
dec div, mod       : num # num -> num;
dec divMod         : num # num -> num # num;
dec dup            : alpha -> alpha # alpha;
dec empty          : set alpha;
dec error          : list char -> alpha;
dec flip           : (alpha # alpha') # (beta # beta') -> (alpha # beta) # (alpha' # beta');
dec from           : num -> list num;
dec fst            : alpha # beta -> alpha;
dec id             : alpha -> alpha;
dec mkpair         : alpha -> beta -> alpha # beta;
dec negate         : num -> num;
dec recip          : num -> num;
dec posAlpha       : char -> num;
dec pred           : num -> num; 
dec properFraction : num -> num # num;
dec quot           : num # num -> num; 
dec quotRem        : num # num -> (num # num);
dec read           : list char -> list char;
dec rem            : num # num -> num;
dec round          : num -> num;
dec round'         : num # num -> num;
dec seq            : alpha # beta -> beta;
dec sign           : num -> num; 
dec signum         : num -> num; 
dec snd            : alpha # beta -> beta;
dec succ           : num -> num; 
dec truncate       : num -> num;
dec Ycurry         : (alpha -> alpha) -> alpha;
dec Yturing        : (alpha -> alpha) -> alpha; 

!!! Data conversion functions

dec chr     : num -> char;
dec num2str : num -> list char;
dec ord     : char -> num;
dec str2num : list char -> num;    

!!! Logic functions - general use
 
dec and          : truval # truval -> truval;  
dec bool         : alpha -> alpha -> truval -> alpha;
dec cmp_pair     : (alpha # beta) # (alpha # beta) -> relation;
dec comp         : list alpha # (alpha -> truval) -> list alpha;
dec compare      : alpha # alpha -> relation;
dec compare_cond : relation -> alpha -> alpha -> alpha -> alpha;
dec even         : num -> truval;
dec if_then_else : truval -> alpha -> alpha -> alpha;
dec not          : truval -> truval;
dec odd          : num -> truval;
dec or           : truval # truval -> truval;
dec sorted       : list alpha -> sorting;
dec xor          : truval # truval -> truval;

!!! Character conversion

dec toLower, toUpper : char -> char; 
dec digitToInt       : char -> num;    
dec intToDigit       : num -> char;    

!!! Logic functions - classification functions

dec isAlnum,    isAlpha, isAscii,    isCtrl  : char -> truval;
dec isDigit,    isGraph, isHexDigit, isLower : char -> truval;
dec isOctDigit, isPunct, isSpace,    isUpper : char -> truval;
dec isXdigit                                 : char -> truval;  

!!! Basic functions
  
dec abs, ceil, fact, floor    : num -> num;
dec erf, erfc, erfcx, normcdf : num -> num;  
dec exp, log, log10, sqrt     : num -> num;
dec normal, normalc, sum      : num -> num;
dec gcd, lcm, pow, logBase    : num # num -> num;
dec max, min                  : alpha # alpha -> alpha;

!!! Trigonometric functions (radians)

dec cos, csc, cot, sec, sin, tan, acos, asin, atan   : num -> num;
dec cosh, sinh, tanh, toDeg, toRad, acot, acsc, asec : num -> num;
dec acosh, asinh, atanh, acsch, asech, acoth         : num -> num;
dec coth, csch, sech                                 : num -> num;
dec atan2, hypot                                     : num # num -> num;


!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!! >>> Protected code - private tunneling           <<< !!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

private;

!!! Math functions: C++ style

--- m_1_sqrt_2 <= 0.707106781186548;

--- m_2_sqrt_pi <= 1.12837916709551;

--- m_epsilon <= 2.22044604925031;

--- m_sqrt_2 <= 1.4142135623731;

--- m_sqrt_2_pi <= 2.506628274631;

--- m_sqrt_eps <= 1.49011611938476;

--- m_ln_sqrt_2_pi <= 0.918938533204673;

--- m_eulerMascheroni <= 0.577215664901533;

--- m_huge <= 1.79769313486232;

--- m_tiny <= 2.2250738585072;

--- m_max_exp <= 1024;

--- m_max_log <= 709.782712893384;

--- m_min_log <= 0 - 708.3964185322641;

!!! Math functions: general

--- e  <= exp 1;

--- pi <= acos 0 * 2;

--- deg <= 57.2957795130823208767981548;

--- rad <=  0.0174532925199432957692369076848;

--- sqrt_pi <= 1.772453850905516027298167483341;

--- tau <= 2 * pi;

!!! General functions

--- (x :: xs) @ 0 <= x;
--- (x :: xs) @ succ n <= xs @ n;

--- x . f <= f(x);

--- xor (x, y) <= x /= y;

--- n .. m <= if n > m 
              then [] 
              else if m > 140000
                   then error ("Limite permitido: 140000.")
                   else n :: (succ n .. m);
                 
--- (a # b) (x, y) <= (a x, b y);

--- (a -> b) f <= b o f o a;
    
--- (f o g) x <= f (g x);

--- [] <> ys <= ys;

--- (x::xs) <> ys <= x :: (xs <> ys);

--- (**) <= pow;

--- (^) <= pow;

--- (f /\ g) x <= (f x, g x);

--- [] || ys <= [];
--- xs || [] <= [];
--- x::xs || y::ys <= (x, y) :: (xs || ys);

--- acosh (x) <= log (x + sqrt (pow (x, 2) - 1));

--- asinh (x) <= log (x + sqrt (pow (x, 2) + 1));

--- atanh (x) <= log ((1 + x) / (1 - x)) / 2;

--- acsch (x) <= log (sqrt (1 + (1 / pow (x, 2))) + 1 / x);

--- asech (x) <= log (sqrt (1 / x - 1) * sqrt (1 / x + 1) + 1 / x);

--- acoth (x) <= log ((x + 1) / (x - 1)) / 2;

--- acot (x) <= atan (1 / x);

--- acsc (x) <= asin (1 / x);

--- asec (x) <= acos (1 / x);

--- bool f _ false <= f;
--- bool _ t true  <= t;

--- choose (x :: xs) <= (x, xs);

--- comp ([], f) <= [];
--- comp (x :: xs, f) <= if f x 
                         then x :: comp (xs, f)
                         else comp (xs, f);

--- cbrt (x) <= pow (x, 1 / 3);

--- ceiling n <= ceil n;

--- char x <= x;

--- const (x, _) <= x;

--- coth (x) <= exp(0 - x) / (exp (x) - exp (0 - x)) * 2 + 1;

--- csch (x) <= 2 / (exp (x) - exp (0 - x));

--- sech (x) <= 2 / (exp (x) + exp (0 - x));

--- cmp_pair ((x1, y1), (x2, y2)) <=
	compare_cond (compare (x1, x2)) LESS (compare (y1, y2)) GREATER;
	
--- compare_cond LESS    l e g <= l;
--- compare_cond EQUAL   l e g <= e;
--- compare_cond GREATER l e g <= g;

--- csc x <= 1 / sin x;

--- cot x <= 1 / tan x;

--- divMod (n, d) <= (quot (n, d), rem (n, d));

--- digitToInt c <= if isAlnum c and ord c > 47 and ord c < 58
                    then ord c - 48
                    else if ord (toUpper c) > 64 and ord (toUpper c) < 71
                         then ord (toUpper c) - 55
                         else error("not a digit");
                      
--- dup x <= (x, x);

--- empty <= [];

--- even n <= n mod 2 = 0;

dec erfcFracAux : num # num # num -> num;
--- erfcFracAux (0, x, acc) <= acc;
--- erfcFracAux (n, x, acc) <= erfcFracAux (n - 1, x, (n / 2) / (x + acc));

dec erfGrande : num -> num;
--- erfGrande x <=
        let exponen == exp(0 - (x * x)) in
        let fracao  == 1 / (x + erfcFracAux(50, x, 0)) in
        1 - ((exponen / sqrt_pi) * fracao);

dec erfTaylorAux : num # num # num # num -> num;
--- erfTaylorAux (termo, n, x2, soma) <=
        if termo = 0
        then soma
        else erfTaylorAux (
                termo * (0 - x2) * (2 * n + 1) / ((n + 1) * (2 * n + 3)),
                n + 1,
                x2,
                soma + termo
             );

dec erfPequeno : num -> num;
--- erfPequeno x <= (2 / sqrt_pi) * erfTaylorAux (x, 0, x * x, 0);

--- erf x <=
        if x < 0 
        then 0 - erf(0 - x) 
        else if x =< 1.5 
        then erfPequeno x   
        else erfGrande x;  
        
--- erfc (0) <= 1;
--- erfc (x) <= 1 - erf x;   

--- erfcx (x) <= exp (pow (x, 2)) * erfc x;

--- fact 0 <= 1;
--- fact(succ n) <= succ n * fact n;

--- flip ((x, x'), (y, y')) <= ((x, y), (x', y'));

--- from n <= if n > 140000
              then error ("Limite maximo de simulacao de infinito: 140000.")
              else n .. 140000;

--- fst (x, _) <= x;

--- gcd (0, n) <= n;
--- gcd (m, n) <= gcd (floor n mod floor m, m);

--- intToDigit n <= if n >= 0 and n < 10
                    then chr (n + 48)
                    else if n > 9 and n < 16
                         then chr (n + 55)
                         else error("not a digit");
                         
--- isAlnum c <= isAlpha c or isDigit c;

--- isAlpha c <= isUpper c or isLower c;

--- isAscii c <= ord c < 128;

--- isCtrl c <= isAscii c and not (isGraph c);

--- isDigit c <= '0' =< c and c =< '9';

--- isHexDigit c <= if isAlnum c and ord c > 47 and ord c < 58
                    then true
                    else if ord (toUpper c) > 64 and ord (toUpper c) < 71
                         then true
                         else false;
                         
--- isGraph c <= ' ' =< c and c =< '~';

--- isLower c <= 'a' =< c and c =< 'z';

--- isPunct c <= isGraph c and c /= ' ' and not(isAlnum c);

--- isOctDigit c <= isAlnum c and ord c > 47 and ord c < 56;

--- isSpace c <= c = ' ' or c = '\t' or c = '\n';

--- isUpper c <= 'A' =< c and c =< 'Z';

--- isXdigit c <= isDigit c or 'a' =< c and c =< 'f' or 'A' =< c and c =< 'F';

--- lcm (_, 0) <= 0;
--- lcm (0, _) <= 0;
--- lcm (x, y) <= x * y div gcd (x, y);

--- logBase (x, y) <= log y / log x;

--- max (x, y) <= if x > y then x else y;

--- min (x, y) <= if x < y then x else y;

--- mkpair x y <= (x, y);

--- negate (x) <= 0 - x;

--- normal x <= erf(x/sqrt 2);

--- normalc x <= erfc(x/sqrt 2);

--- normcdf (x) <= erfc (0 - x / sqrt 2) / 2;

--- not true  <= false;
--- not false <= true;

--- odd n <= n mod 2 /= 0;

--- posAlpha ch <= if isLower ch
                   then ord ch - ord 'a'
                   else ord ch - ord 'A';
              
--- pred 0       <= 0;
--- pred (n + 1) <= n;

--- properFraction x <= (n, r) where n == floor x 
                               where r == x - floor x; 

--- quot (n, d) <= n div d;

--- quotRem (a, b) <= (a div b, a mod b);

--- sum 0 <= 0;
--- sum (succ n) <= succ n + sum n;

--- sec x <= 1 / cos x;

--- succ n <= n + 1;

--- false and p <= false;
--- true  and p <= p;

--- true  or p <= true;
--- false or p <= p;

--- if true  then x else y <= x;
--- if false then x else y <= y;

--- id x <= x;

--- x =  y <= (\ EQUAL   => true  | _ => false) (compare(x, y));
--- x /= y <= (\ EQUAL   => false | _ => true)  (compare(x, y));
--- x <  y <= (\ LESS    => true  | _ => false) (compare(x, y));
--- x >= y <= (\ LESS    => false | _ => true)  (compare(x, y));
--- x >  y <= (\ GREATER => true  | _ => false) (compare(x, y));
--- x =< y <= (\ GREATER => false | _ => true)  (compare(x, y));

dec print : alpha -> beta;	
!!! print x <= return;		

--- recip (x) <= 1 / x;
--- x / y <= x * recip y;

--- rem (n, d) <= n mod d;

dec return : alpha;		

--- round x <= if compare (half_down, 0.0) = LESS    then n else 
               if compare (half_down, 0.0) = EQUAL   then if even n then n else m else
               if compare (half_down, 0.0) = GREATER then m else 0.0
                  where half_down == abs r - 0.5  
                  where m         == if r < 0.0 then n - 1 else n + 1    
                  where (n, r)    == properFraction x;
                  
--- round' (n, d) <= if d < 0
                     then error ("Second argument must be positive number.")
                     else ceil (n * pow (10, d)) / pow (10, d);  

--- seq (_, y) <= y;    
                   
--- sign n <= if n < 0 then 0 - 1 else
              if n = 0 then 0 else 1;

--- signum n <= if n < 0 then 0 - 1 else  
                if n = 0 then 0 else 1;
                
--- sorted [] <= ascending;
--- sorted [x] <= ascending;
--- sorted (x :: y :: xs) <= if x =< y
                             then sorted (y :: xs)
                             else descending; 
                                
--- snd (_, y) <= y;              

--- tan x <= sin x / cos x;

--- toDeg r <= r * deg;

--- toLower c <= if isUpper c then chr(ord c + 32) else c;

--- toRad r <= r * rad;

--- toUpper c <= if isLower c then chr(ord c - 32) else c;

--- truncate x <= if x < 0 
                  then floor (x) + 1
                  else floor (x);
              
dec write_element : alpha -> list alpha -> beta; 
!!! write_element x <= write_list;	

dec write_list : list alpha -> beta;
--- write_list []     <= return;
--- write_list(x::xs) <= write_element x xs;

--- Ycurry f <= Z Z where Z == \ z => f(z z);

--- Yturing <= Z Z where Z == \ z => \ f => f(z z f);