%% examples.pvs
%% General examples
%% Release PVSio-2.d (11/09/05)

examples : THEORY
BEGIN

  %% PVSio is useful for

  %% printing to stdout 
  hello_world : void =
    println("+"+pad(50,"-")+"+") &
    println("|"+center(50,"Hello World")+"|")&
    println("+"+pad(50,"-")+"+") 

  %% reading from stdin and assert the input
  hello_you : void =
     LET s = query_line("What is your name?") IN
     println("Hola "+s) &
     LET r = query_real(s+", give me a non-negative real number:") IN
     assert(r>=0,"Sorry, "+r+" is < 0") &
     println("The sqrt of "+r+" is: "+SQRT(r))

  %% catching exceptions
  hello_catch : void = 
    catch(NotARealNumber,
          hello_you,
          LAMBDA(e:Exception[string]):println(tag(e)+": "+val(e)))

  %% reading files (the imperative way)
  cat : void =
    let f=fopenin("examples.pvs") in
    while(not eof?(f),println(fread_line(f))) &
    fclose(f)

  %% reading files (the functional way)
  more(n:nat) : void =
    let f = fopenin("examples.pvs") in
    try(forall(i:below(n)):
        if not eof?(f) then 
          println(fread_line(f)) 
        else 
          fail
        endif,
        fclose(f))

  %% iterating a function on a file 
  copy : void =
    let f  = fopenout(create,"examples.bak") in
    let nf = fmap_line(fopenin("examples.pvs"),
                       1,
                       lambda(s:string,l:nat):
                         prog(fprintf(f,"[~3,'0d]~a~%",(l,s)),l+1)) in
    println("*** Check the content of examples.bak in the working directory") &
    fclose(f)

  %% defining mutable variables
  woow(x:int) : void =
    let lvar = ref[int](3) in
    set[int](lvar,x) &
    println("The value of lvar is: "+val(lvar))

  %% declaring global variables
  gvar : Global[int,1]
    
  WOOW(x:int) : void =
    set[int](gvar,x) &
    println("The value of gvar is: "+val(gvar))

  %% catching exceptions
  mysqrt(r:real):real = 
    catch(NotARealNumber,
          SQRT(r),
          0)

  %% throwing and catching exceptions 
  int_aux : int =
    let i = query_int("Enter a number less than 10") in
    if i > 10 then throw("GreaterThan10")
    else i
    endif

  readupto10 : int =  
    catch[int]((:NotAnInteger,"GreaterThan10":),
	       int_aux,0)

  %% PVS parsing and printing

  Point : TYPE = [# x : real, y: real #]

  zero : Point = str2pvs("(# x := 0, y:= 0#)")
   
  rec2str(p:Point):string = pvs2str(p)

  %% ... and many other things.
  % But, semantic attachments may produce surprising results:

  paradox: bool =
    (RANDOM=RANDOM) % often evaluates to FALSE!

  noparadox: bool =
    LET r = RANDOM IN
      r = r         % evaluates to TRUE

  thefact : LEMMA 
    RANDOM = RANDOM % is trivially TRUE!

  %%% Welcome message printed by make examples
  welcome : void =
    println("+"+pad(50,"-")+"+") &
    println("|"+center(50,pvsio_version)+"|")&
    println("|"+center(50,date)+"|")&
    println("+"+pad(50,"-")+"+") 
    

END examples