home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / demonstr / demo.ml < prev    next >
Encoding:
Text File  |  1995-06-01  |  1.1 KB  |  37 lines  |  [TEXT/MPS ]
  1. #open "prop";;
  2. #open "asynt";;
  3.  
  4. let examine chaîne =
  5.     let proposition = analyse_proposition chaîne in
  6.     let variables = variables_libres proposition in
  7.     try
  8.       vérifie_tautologie proposition variables;
  9.       begin match variables with
  10.         [] ->
  11.           print_string "Théorème: "
  12.       | [var] ->
  13.           print_string ("Théorème: pour toute proposition "^var^", ")
  14.       | _ ->
  15.           print_string "Théorème: pour toutes propositions ";
  16.           do_list (function var -> print_string (var^", ")) variables
  17.       end;
  18.       print_string chaîne;
  19.       print_newline()
  20.     with Réfutation liaisons ->
  21.       print_string (chaîne ^ " n'est pas un théorème,\n");
  22.       print_string "car la proposition est fausse quand\n";
  23.       do_list
  24.        (function (var, b) ->
  25.          print_string (var ^ " est ");
  26.          print_string (if b then "vraie" else "fausse");
  27.          print_newline ())
  28.        liaisons;;
  29. let boucle () =
  30.   try
  31.     while true do
  32.       print_string ">>> "; examine(read_line())
  33.     done
  34.   with End_of_file -> ();;
  35.  
  36. if sys__interactive then () else begin boucle(); exit 0 end;;
  37.