% LIB.ML %


% General %

syntax prefix Do 0;  let Do _ = ();
let I a = a;
let K a b = a;


% Unit %

syntax nonfix printdot 86 1; let rec printdot(x:unit):unit = printdot x;


% Function %

syntax infix 1400 o 1400 76 2; 
   let rec (x:('b -> 'c)) o (y:('a -> 'b)):('a -> 'c) = x o y;
   % This is also defined by InitEnv! %
syntax infix 400 & 400;  let f & g = g o f;
syntax infix 400 # 400;  let #(f,g)(a,b) = (f(a),g(b));



% Boolean %

syntax prefix Not 600 30 1; let rec Not(x:bool):bool = Not(x);
syntax infix 500 And 500 31 2; let rec (x:bool) And (y:bool):bool = x And y;
syntax infix 400 Or  400 32 2; let rec (x:bool) Or  (y:bool):bool = x Or y;
syntax nonfix printbool 87 1; let rec printbool(x:bool):unit = printbool x;



% Integer %

syntax prefix ~ 1100 33 1; let rec ~(x:int):int = ~ x;
syntax infix 900 * 900 36 2; let rec (x:int) * (y:int):int = x * y;
syntax infix 900 / 900 37 2; let rec (x:int) / (y:int):int = x / y;
syntax infix 900 div 900 38 2; let rec (x:int) div (y:int):int = x div y;
syntax infix 900 mod 900 39 2; let rec (x:int) mod (y:int):int = x mod y;
syntax infix 800 + 800 34 2; let rec (x:int) + (y:int):int = x + y;
syntax infix 800 - 800 35 2; let rec (x:int) - (y:int):int = x - y;
syntax infix 700 > 700 44 2; let rec (x:int) > (y:int):bool = x > y;
syntax infix 700 < 700 45 2; let rec (x:int) < (y:int):bool = x < y;
syntax infix 700 >= 700 46 2; let rec (x:int) >= (y:int):bool = x >= y;
syntax infix 700 <= 700 47 2; let rec (x:int) <= (y:int):bool = x <= y;
let min(a:int,b:int) = if a<b then a else b;
let max(a:int,b:int) = if a>b then a else b;
let rec AppInt'(f,i,j) = if i>j then () else ( f(i); AppInt'(f,i+1,j) );
let AppInt f (i,j) = AppInt'(f,i,j);
syntax nonfix printint 88 1; let rec printint(x:int):unit = printint x;



% Real %

syntax nonfix realofstring 198 1;
    let rec realofstring(x:string):real = realofstring x;
syntax nonfix tokofreal 197 1; let rec tokofreal(x:real):string = tokofreal x;
syntax nonfix printreal 199 1; let rec printreal(x:real):unit = printreal x;


% Reference %

syntax prefix ! 1100 54 1; let rec ! (x: 'a ref): 'a = ! x;
syntax infix 50 := 50 55 2;
    let rec (x: 'a ref) := (y: 'a) = (x := y): unit; %JJS%
let deref = !;


% String %

syntax nonfix explode 48 1; let rec explode(x:string):string list = explode x;
syntax nonfix implode 49 1; let rec implode(x:string list):string = implode x;
syntax nonfix explodeascii 50 1; 
   let rec explodeascii(x:string):int list = explodeascii x;
syntax nonfix implodeascii 51 1; 
   let rec implodeascii(x:int list):string = implodeascii x;
syntax nonfix tokofint 52 1; let rec tokofint(x:int):string = tokofint x;
syntax nonfix intoftok 53 1; let rec intoftok(x:string):int = intoftok x;
syntax nonfix LengthTok 100 1; let rec LengthTok(x:string):int = LengthTok x;
syntax nonfix substring 101 3; 
   let rec substring(x:string, y:int, z:int):string = substring(x,y,z);
syntax infix 700 #<= 700 107 2; let rec (a:string) #<= (b:string) = a#<=b: bool;
syntax infix 700 #< 700 108 2; let rec (a:string) #< (b:string) = a#<b: bool;
syntax infix 700 #>= 700 109 2; let rec (a:string) #>= (b:string) = a#>=b: bool;
syntax infix 700 #> 700 110 2; let rec (a:string) #> (b:string) = a#>b: bool;
syntax infix 300 #@ 300;  let t1 #@ t2 = implode([t1;t2]);
   %let t1 #@ t2 = implode(explode(t1) @ explode(t2));%
syntax nonfix tokhash 126 2; let rec tokhash(x:string,n:int):int = tokhash(x,n);
syntax nonfix ScanTokUntilIn 161 4;
   let rec ScanTokUntilIn(set: string, t: string, start: int, n: int ): int = 
      ScanTokUntilIn(set, t, start, n);
syntax nonfix ScanTokWhileIn 162 4;
   let rec ScanTokWhileIn(set: string, t: string, start: int, n: int ): int = 
      ScanTokWhileIn(set, t, start, n);
syntax nonfix outstring 90 1; let rec outstring(x:string):unit = outstring x;
let outtok = outstring;
syntax nonfix flush 231 0; let rec flush():unit = flush();

%{--- Functions to provide fixed-width printing ---}%
let lineterm = ref `/L`;

let type fixed_width_stream <=> (|linelength: int; lengthleft: int ref |)
with
    init_fixed_width_stream(maxwidth) = 
      absfixed_width_stream(|linelength=maxwidth; lengthleft = ref maxwidth|)
enc
    fws = init_fixed_width_stream(79)
ins {
    newline(n) =
      let (|linelength; lengthleft|) = repfixed_width_stream(fws) 
      enc rec outlinefeed(n) = if n <= 0 then () else
                               (outtok(! lineterm); outlinefeed(n-1))
       in if n = 0 then ()
          else if !lengthleft = linelength then outlinefeed(n-1)
          else (lengthleft := linelength; outlinefeed(n) )
enc 
   checkminimum(min:int) =
      let (|linelength; lengthleft|) = repfixed_width_stream(fws) 
       in if !lengthleft < min then newline(1) else ()

enc rec { output(string) =
      let (|linelength; lengthleft|) = repfixed_width_stream(fws) 
      enc left = !lengthleft in
      if LengthTok(string) < left
      then (lengthleft := left - LengthTok(string); outtok(string))
      else if LengthTok(string) >= linelength
      then (outtok(substring(string,1,left)); 
            lengthleft := linelength; outtok(! lineterm);
            outputlongstring(string,left+1))
      else (newline(1); output(string))
    and outputlongstring(string,pos) =
      let (|linelength; lengthleft|) = repfixed_width_stream(fws) in
      if (LengthTok(string) - pos + 1) < linelength
      then output(substring(string,pos,(LengthTok(string) - pos + 1)))
      else (outtok(substring(string,pos,linelength)); outtok(! lineterm);
            outputlongstring(string,pos+linelength))
    } }
;

let output_string_fn = ref output;
let newline_fn = ref newline;
let check_minimum_fn = ref checkminimum;
let flush_fn = ref flush;

let outtok(x) = (!output_string_fn)(x);
let outstring(x) = (!output_string_fn)(x);
let printstring(x) = ((!check_minimum_fn)(LengthTok(x)+2);
                      (!output_string_fn)(`"`); 
                      (!output_string_fn)(x); 
                      (!output_string_fn)(`"`));
let printtok(x) = ((!check_minimum_fn)(LengthTok(x)+2);
                   (!output_string_fn)(`"`); 
                   (!output_string_fn)(x); 
                   (!output_string_fn)(`"`));
let printint(x) = (!output_string_fn)(tokofint(x));
let printreal(x) = (!output_string_fn)(tokofreal(x));
let printdot() = (!output_string_fn)(`()`);
let printbool(x) = if x then (!output_string_fn)(`true`) 
                   else (!output_string_fn)(`false`);
let newline(n) = (!newline_fn)(n);
let flush() = (!flush_fn)();


% Pair (i.e. Tuple of size 2) %

syntax nonfix fst 15 1; let rec fst(x:('a # 'b)): 'a = fst x;
syntax nonfix snd 16 1; let rec snd(x:('a # 'b)): 'b = snd x;
let pair a b = (a,b);



% Disjoint sum %

syntax nonfix outl 20 1; let rec outl(x:('a + 'b)): 'a = outl x;
syntax nonfix outr 21 1; let rec outr(x:('a + 'b)): 'b = outr x;
syntax nonfix isl 22 1; let rec isl(x:('a + 'b)):bool = isl x;
syntax nonfix isr 23 1; let rec isr(x:('a + 'b)):bool = isr x;



% List %

let cons = ::;
syntax nonfix hd 17 1; let rec hd(x: 'a list): 'a = hd x;
syntax nonfix tl 18 1; let rec tl(x: 'a list): 'a list = tl x;
syntax nonfix null 19 1; let rec null(x: 'a list):bool = null x;
syntax nonfix LengthList 115 1;
   let rec LengthList(l: 'a list):int = LengthList(l);
let length = LengthList;
syntax infix 300 @ 300;
   let rec a@b = if null a then b else (hd a)::((tl a)@b);
syntax nonfix rev 179 1;
   let rec rev(l: 'a list): 'a list = rev(l);
let { rec rev'(r,l) = if null l then r else rev'(hd(l)::r,tl(l)) }
ins append(k,l) = rev'(l,rev k);  % Tail-recursive but slower than "@" %
let reverse = rev;
let rec MapList'(f,a) = if null a then [] else f(hd(a))::MapList'(f,tl(a));
let MapList f a = MapList'(f,a);
let map' = MapList';
let map = MapList;
let rec AppList'(f,a) = if null a then () else ( f(hd(a)); AppList'(f,tl(a)) );
   % Could make f: 'a -> 'b by adding "Do" %
let rec RevAppList'(f:('a -> unit),l) =
        if null(l) then () else (RevAppList'(f,tl l); f(hd l));
let AppList f l = AppList'(f,l);
let app' = AppList';
let app = AppList;
let aplist = AppList';
let revaplist = RevAppList';
syntax nonfix nth 178 2;
   let rec nth(l: 'a list, n:int): 'a = nth(l,n);
let rec LftReduceList f l x =
    if null l then x else f (hd l) (LftReduceList f (tl l) x);
let rec RhtReduceList f l x =
    if null l then x else RhtReduceList f (tl l) (f (hd l) x);
let itlist = LftReduceList;
let revitlist = RhtReduceList;

% RH: the original version has type annotations that don't make sense! %
%let ReduceList %
%        (down:('x # 'a) -> ('b # 's), bottom: 'b -> 'c, up:('x # 's # 'c) -> 'c) %
%            (l: 'x list)  (starter: 'a) : 'c = %
%    let rec traverse(l, sofar) = %
%       if null(l) then bottom(sofar) %
%       else let (passdown, state) = down(hd(l),sofar) in %
%            up(hd(l), state, traverse(tl(l), passdown)) %
% in traverse(l,starter); %

let ReduceList
        (down, bottom, up)
            (l)  (starter) =
    let rec traverse(l, sofar) =
       if null(l) then bottom(sofar)
       else let (passdown, state) = down(hd(l),sofar) in
            up(hd(l), state, traverse(tl(l), passdown))
 in traverse(l,starter);

let rec exists(f,l) =
    if null(l) then false
    else if f(hd l) then true
    else exists(f,tl l);

let rec split(l, m, n) =
  if m=0 then if length(l)=n then ([],l) else failwith `split`
         else if null(l) then failwith `split`
         else ( let (a,b) = split(tl(l),m-1,n) in (hd(l)::a,b));

let rec sum(f,l) = if null(l) then 0 else f(hd l) + sum(f,tl l);

let rec listprint(Args:('a list), Print:('a -> unit), Sep): unit =
  if null(Args) then ()
  else ( Print(hd Args);
         if null(tl Args) then () else outtok(Sep);
         listprint(tl Args, Print, Sep));



% List of String %

let rec MemberTok(x:string,l) =
    if null l then false else if x=hd l then true else MemberTok(x,tl l);



% Array %

syntax nonfix array 103 2;
   let rec array(n:int, init: '_weak): '_weak array = array(n,init);
syntax nonfix LengthArray 104 1; 
   let rec LengthArray(x: 'a array):int = LengthArray(x);
syntax infix 50 sub 50 105 2;
   let rec (x: 'a array) sub (y:int) = (x sub y): 'a;
syntax nonfix update 106 3; 
   let rec update(x: 'a array, y:int, z: 'a):unit = update(x,y,z);
syntax nonfix arrayoflist 121 1;
   let rec arrayoflist(x: '_weak list): '_weak array = arrayoflist(x);
let AppArray'(f,a) = AppInt'( (\i. f(a sub i)), 1, LengthArray(a));
let AppArray f a = AppArray'(f,a);

let ArrayOfFn(n,f) =
    if n=0 then arrayoflist[]
    else
        let a = array(n,f(1))
        enc rec maparr i = if i>n then a else ( update(a,i,f(i)); maparr(i+1) )
        in maparr(2);

let IterArray(a,f) =
    let n = LengthArray(a) in
    if n=0 then ()
    else
        let rec maparr i = if i>n then () 
        else ( update(a,i,f(a sub i)); maparr(i+1) )
        in maparr(1);

let MapArray f a = 
   let n = LengthArray(a) in
      if n=0 then arrayoflist[]
      else
         let a' = array(n,f(1,(a sub 1)))
         enc rec maparr(i) = 
            if i>n then a' else ( update(a',i,f(i,(a sub i))); maparr(i+1) )
         in maparr(2);

let RhtReduceArray f a x =
  let {length = LengthArray(a)
  enc  rec maparr(x,n) = 
       if (n > length) then x 
       else maparr((f (a sub n) x), n+1) } in
  maparr(x,1);



% ML System and Operating System %

syntax nonfix system 92 1; let rec system(x:string): int = system(x);
let ie(file) = (system(implode(explode `ie ` @ (explode file))); file);

syntax nonfix collect 85 1; let rec collect(x: 'a): 'a = collect(x);
syntax nonfix chdir 176 1;  let rec chdir(x: string): unit = chdir(x);
syntax nonfix CpuTime 163 0;  let rec CpuTime():int = CpuTime();
