(* ===================================================== *)
(* Apprentissage de la programmation avec OCaml *)
(* Catherine Dubois & Valérie Ménissier-Morain *)
(* Éditions Hermès Sciences *)
(* Mars 2004 *)
(* ===================================================== *)
(* Fichier MLSRC/assistant.ml *)
(* ===================================================== *)
type tformule =
Toujours_vrai
| Toujours_faux
| Var of string
| Non of tformule
| Et of tformule * tformule
| Ou of tformule * tformule
| Implique of tformule * tformule
| Est_équivalent of tformule * tformule;;
(*****************************************
* analyse syntaxique *
*****************************************)
let non_significatif c =
match c with
| ' ' | '\n' | '\t' -> true
| _ -> false;;
(* n doit être la longueur de s *)
let début_mot s n pos =
let i = ref pos in
while (!i)<n && non_significatif s.[!i] do
i := !i +1
done;
!i;;
(* n doit être la longueur de s *)
let fin_chaîne s n pos =
début_mot s n pos = n;;
exception Erreur_syntaxe;;
let alpha c =
let petit_c = Char.lowercase c in
'a' <= petit_c && petit_c <= 'z';;
let digit c = '0' <= c && c <= '9';;
let possible c = (alpha c) || (digit c) || c='_';;
let reconnaître_ident s n pos =
(* à la position pos, on doit avoir le début d'un mot*)
(* n = longueur de s*)
if pos = n || not(possible s.[pos])
then raise Erreur_syntaxe
else
let j = ref 1 in
while (pos + !j)<n && possible s.[pos + !j] do
j := !j +1 done;
let lg_mot = !j in
while (pos+(!j))<n &&
non_significatif s.[pos+(!j)] do
j := !j +1 done;
((String.sub s pos lg_mot),pos+(!j));;
let reconnaître_var s n pos =
let (ch, pos1) = reconnaître_ident s n pos in
(Var ch, pos1);;
let reconnaître_mot_clé motclé s n pos =
let lg = String.length motclé in
try (if (String.sub s pos lg) = motclé
then début_mot s n (pos+lg)
else raise Erreur_syntaxe)
with Invalid_argument "String.sub"
-> raise Erreur_syntaxe;;
let reconnaître_par_ouv s n pos = reconnaître_mot_clé "(" s n pos;;
let reconnaître_par_ferm s n pos = reconnaître_mot_clé ")" s n pos;;
let reconnaître_et s n pos = reconnaître_mot_clé "/\\" s n pos;;
let reconnaître_ou s n pos = reconnaître_mot_clé "\/" s n pos;;
let reconnaître_not s n pos = reconnaître_mot_clé "~" s n pos;;
let reconnaître_imp s n pos = reconnaître_mot_clé "==>" s n pos;;
let reconnaître_équiv s n pos = reconnaître_mot_clé "<==>" s n pos;;
let reconnaître_vrai_faux s n pos =
try
(match (let lg_formules_base = 13
in String.sub s pos lg_formules_base) with
"Toujours_vrai" -> (Toujours_vrai, début_mot s n pos+13)
| "Toujours_faux" -> (Toujours_faux, début_mot s n pos+13)
| _ -> raise Erreur_syntaxe)
with Invalid_argument _ -> raise Erreur_syntaxe;;
let rec reconnaître_form0 s n pos =
let (f1, pos1) = reconnaître_form1 s n pos in
try (let pos2 = reconnaître_équiv s n pos1 in
let (f2, pos3) = reconnaître_form0 s n pos2 in
(Est_équivalent (f1, f2), pos3))
with Erreur_syntaxe -> (f1, pos1)
and reconnaître_form1 s n pos =
let (f1, pos1) = reconnaître_form2 s n pos in
try (let pos2 = reconnaître_imp s n pos1 in
let (f2, pos3) = reconnaître_form1 s n pos2 in
(Implique (f1, f2), pos3))
with Erreur_syntaxe -> (f1, pos1)
and reconnaître_form2 s n pos =
let (f1, pos1) = reconnaître_form3 s n pos in
try (let pos2 = reconnaître_ou s n pos1 in
let f2, pos3 = reconnaître_form2 s n pos2 in
(Ou (f1, f2), pos3))
with Erreur_syntaxe -> (f1, pos1)
and reconnaître_form3 s n pos =
let (f1, pos1) = reconnaître_form4 s n pos in
try (let pos2 = reconnaître_et s n pos1 in
let f2, pos3 = reconnaître_form3 s n pos2 in
(Et (f1, f2), pos3))
with Erreur_syntaxe -> (f1, pos1)
and reconnaître_form4 s n pos =
try (let pos1 = reconnaître_not s n pos in
let (f, pos2) = reconnaître_form4 s n pos1 in
(Non f, pos2))
with Erreur_syntaxe -> reconnaître_form5 s n pos
and reconnaître_form_parenth s n pos =
let pos1 = reconnaître_par_ouv s n pos in
let f, pos2 = reconnaître_form0 s n pos1 in
let pos3 = reconnaître_par_ferm s n pos2 in
(f, pos3)
and reconnaître_form5 s n pos =
try reconnaître_form_parenth s n pos
with Erreur_syntaxe ->
(try (reconnaître_vrai_faux s n pos)
with Erreur_syntaxe -> reconnaître_var s n pos);;
let analyser_prop s =
let n = String.length s in
let (f, pos) = reconnaître_form0 s n (début_mot s n 0) in
if (fin_chaîne s n pos) then f
else raise Erreur_syntaxe;;
(*Exemples
analyser_prop "P1 ";;
analyser_prop " _S";;
analyser_prop " (E) ";;
analyser_prop "~E";;
analyser_prop "~~E";;
analyser_prop "~(~E)";;
analyser_prop "P1 \n /\ Q";;
analyser_prop " (~E/\P)";;
analyser_prop " P/\Q\/ S";;
analyser_prop " P /\ Q /\ S";;
analyser_prop " P \/ Q /\ S";;
analyser_prop " (P \/ Q) /\ S";;
analyser_prop " (P/\Q)/\ S";;
analyser_prop "P /\ Q ==> R" ;;
analyser_prop "P /\ Q = R" ;;
analyser_prop "P ==> R ==> Q" ;;
analyser_prop "(P ==> R) ==> Q" ;;
analyser_prop "P1<==>Q";;
analyser_prop "~P <==> Q ==> R";;
analyser_prop "P ==> Q <==> ~P \/ Q";;
*)
(**************************************
* Assistant à la preuve *
**************************************)
type ident = string;;
type tactique = Exact of ident | Split
| Decompose of ident | Case of ident
| Left | Right
| Intro of ident | Intros of ident list
| Apply of ident | Absurd of tformule ;;
type but = {contexte : (ident*tformule) list ;
formule : tformule};;
(**************************************
* Affichage *
**************************************)
let priorité f = match f with
| Est_équivalent (f1, f2) -> 1
| Implique (f1, f2) -> 2
| Ou (f1, f2) -> 3
| Et (f1, f2) -> 4
| Non f1 -> 5
| _ -> 6;;
let rec parenthéser_afficher f p assoc =
let ouv = "(" and ferm = ")" in
if (priorité f < p) || (priorité f=p && assoc)
then (print_string ouv ;
afficher_formule f ;
print_string ferm)
else afficher_formule f
and
afficher_formule f =
let p = priorité f in
match f with
| Et (f1, f2) ->
parenthéser_afficher f1 p true; print_string "/\\" ;
parenthéser_afficher f2 p false
| Ou (f1, f2) ->
parenthéser_afficher f1 p true; print_string "\/" ;
parenthéser_afficher f2 p false
| Implique (f1, f2)->
parenthéser_afficher f1 p true; print_string "==>" ;
parenthéser_afficher f2 p false
| Est_équivalent (f1, f2)->
parenthéser_afficher f1 p true; print_string "<==>" ;
parenthéser_afficher f2 p false
| Non f1 ->
print_string "~"; parenthéser_afficher f1 p false
| Var x -> print_string x
| Toujours_faux -> print_string "Toujours_faux"
| Toujours_vrai -> print_string "Toujours_vrai";;
let afficher_hyp (nom,formule) =
print_string nom; print_string ": ";
afficher_formule formule;
print_newline();;
let afficher_contexte c = List.iter afficher_hyp c;;
let rec afficher_but c =
print_newline();
afficher_contexte c.contexte ;
print_string "====================================\n";
afficher_formule c.formule;
print_newline();;
(*Exemple
let théo = analyser_prop "(Q ==> R) ==> R";;
afficher_but
{formule = théo;
contexte = [("H", Implique(Var"P", Var "Q")); ("Hp", (Var "P"))]};;
*)
exception Ident_non_valide;;
exception Pb_tactique;;
let ident_frais =
let prefixe="_hyp" and compteur = ref 0 in
function () ->
compteur := !compteur + 1; prefixe^(string_of_int (!compteur));;
let valide_ident id c =
try not(List.mem_assoc id c)
with Not_found -> raise Ident_non_valide;;
let rec introduire hyps c f = match (hyps, f) with
[], _ -> (c,f)
| hyp::r, Implique(f1, f2) ->
if (valide_ident hyp c)
then introduire r ((hyp, f1)::c) f2
else raise Ident_non_valide
| _ -> raise Pb_tactique;;
(*Exemples
introduire ["H1"] []
(Implique (Implique (Var "P", Var "Q"),
Implique (Var "P", Var "R")));;
introduire ["H1"; "H2"] []
(Implique (Implique (Var "P", Var "Q"), Var "R"));;
*)
let rec conditions_apply phi f =
match phi with
Implique (f1, f2) -> if f2=f then [f1]
else f1::(conditions_apply f2 f)
| _ -> raise Pb_tactique;;
(* Exemple
conditions_apply
(Implique (Var "P", Implique (Var "Q", Var "R")))
(Var "R");;
*)
let appliquer_tactique tac but =
match (tac, but.formule) with
(Exact hyp_ident, f) ->
(try (if List.assoc hyp_ident but.contexte = f
then []
else raise Pb_tactique)
with Not_found -> raise Ident_non_valide)
| (Split, Et (f1,f2)) -> [{contexte = but.contexte; formule = f1};
{contexte = but.contexte; formule = f2}]
| (Split, Est_équivalent (f1,f2)) ->
[{contexte = but.contexte; formule = Implique(f1, f2)};
{contexte = but.contexte; formule = Implique(f2, f1)}]
| (Case hyp_ident, f) ->
(try (match List.assoc hyp_ident but.contexte with
Ou (phi1, phi2) ->
let n1=ident_frais () and n2=ident_frais () in
[{contexte = (n1,phi1)::but.contexte; formule = f} ;
{contexte = (n2,phi2)::but.contexte; formule = f}]
| _ -> raise Pb_tactique)
with Not_found -> raise Ident_non_valide)
| (Decompose hyp_ident, f) ->
(try (match List.assoc hyp_ident but.contexte with
Et (phi1, phi2) ->
let n1=ident_frais () and n2=ident_frais () in
[{contexte = (n1,phi1)::(n2,phi2)::but.contexte;
formule = f}]
| _ -> raise Pb_tactique)
with Not_found -> raise Ident_non_valide)
| (Left, Ou(f1,_)) -> [{contexte = but.contexte; formule = f1}]
| (Right, Ou(_,f2)) -> [{contexte = but.contexte; formule = f2}]
| (Intro h, Implique(f1,f2)) ->
if not(valide_ident h but.contexte)
then raise Ident_non_valide
else [{contexte = (h,f1)::but.contexte; formule = f2}]
| (Intros ((_::_) as nvs), Implique(f1,f2)) ->
let (nv_c, phi)= introduire nvs but.contexte but.formule in
[{contexte = nv_c ; formule = phi}]
| (Apply hyp_ident, f) ->
(try (let phi = List.assoc hyp_ident but.contexte in
List.map
(function f -> {contexte= but.contexte; formule=f})
(conditions_apply phi f))
with Not_found -> raise Ident_non_valide)
| (Absurd f1, f) -> [{contexte = but.contexte; formule = f1} ;
{contexte = but.contexte; formule = Non f1}]
| _ -> raise Pb_tactique;;
(* Exemples
let afficher_buts = List.iter afficher_but;;
let théo2 = analyser_prop ("(P ==> Q ==> R) ==> Q ==> P ==> R") in
afficher_buts (appliquer_tactique (Intros ["h1";"h2";"h3"])
{formule=théo2 ; contexte=[]});;
afficher_buts (appliquer_tactique (Decompose "h1")
{formule=Var "R" ;
contexte=[("h1", Et (Var "Q", Var "R"))]});;
appliquer_tactique (Decompose "h1") {formule=Var "R" ; contexte=[]};;
afficher_buts(appliquer_tactique (Apply "h1")
{formule=Var "R" ;
contexte=[("h1", analyser_prop("P ==> (Q ==> R)"))]});;
appliquer_tactique (Apply "h1")
{formule=Var "P" ;
contexte=[("h1", analyser_prop("P ==> (Q ==> R)"))]};;
*)
(************************************
* Analyse syntaxique des tactiques *
************************************)
let reconnaître_virgule s n pos =
reconnaître_mot_clé "," s n pos;;
let reconnaître_hypo_util s n pos =
let (ch, pos1) = reconnaître_ident s n pos in
if ch.[0] = '_'
then raise Erreur_syntaxe
else (ch, pos1);;
let rec reconnaître_hypos s n pos =
let h, pos1 = reconnaître_hypo_util s n pos in
try let pos2 = reconnaître_virgule s n pos1 in
let (hs, pos3) = reconnaître_hypos s n pos2 in
(h::hs, pos3)
with Erreur_syntaxe -> [h], pos1;;
exception Fin;;
let reconnaître_tactique s n pos =
let (ch, pos1) = reconnaître_ident s n pos in
match ch with
"Split" -> (Split, pos1)
| "Left" -> (Left, pos1)
| "Right" -> (Right, pos1)
| "Intro" ->
let (h,pos2) = reconnaître_hypo_util s n pos1 in
(Intro h, pos2)
| "Exact" ->
let (h,pos2) = reconnaître_ident s n pos1 in
(Exact h, pos2)
| "Case" ->
let (h,pos2) = reconnaître_ident s n pos1 in
(Case h, pos2)
| "Decompose" ->
let (h,pos2) = reconnaître_ident s n pos1 in
(Decompose h, pos2)
| "Apply" ->
let (h,pos2) = reconnaître_ident s n pos1 in
(Apply h, pos2)
| "Intros" ->
let hs, pos2 = reconnaître_hypos s n pos1 in
(Intros hs, pos2)
| "Absurd" ->
let (f,pos2) = reconnaître_form0 s n pos1 in
(Absurd f, pos2)
| "Quit" -> raise Fin
| _ -> raise Erreur_syntaxe;;
let analyser_tactique s =
let n = String.length s in
let (t, pos) = reconnaître_tactique s n (début_mot s n 0) in
if (fin_chaîne s n pos) then t
else raise Erreur_syntaxe;;
(* Exemples
analyser_tactique "Intros hyp1, hyp2 ";;
analyser_tactique "Intro _hyp1";;
(* un nom d'hypothèse choisi par l'utilisateur ne peut
commencer par \_*)
analyser_tactique "Exact _hyp1";;
analyser_tactique "Absurd P==> Q";;
analyser_tactique "Split P";;
(* Split n'est suivi de rien *)
analyser_tactique "Quit";;
*)
let rec une_étape but =
try (print_string "\n> ";
let tac = analyser_tactique(read_line()) in
appliquer_tactique tac but)
with
Pb_tactique -> print_string "tactique non valide";
une_étape but
| Erreur_syntaxe -> print_string "erreur de syntaxe";
une_étape but
| Ident_non_valide -> print_string "ident. non valide";
une_étape but;;
let rec boucle_interactive buts = match buts with
[] -> ()
| but::r -> afficher_but but;
boucle_interactive ((une_étape but)@r);;
let vérif () =
print_string "formule ? ";
try let f = analyser_prop (read_line()) in
begin boucle_interactive [{formule=f ; contexte=[]}];
print_string "qed\n"
end
with | Fin -> print_string "bye\n"
| Erreur_syntaxe -> print_string "formule incorrecte\n";;
vérif();;
(*pour compiler : ocamlc -o assistant assistant.ml
pour lancer l'exécution : ocamlrun assistant *)
Ce document a été traduit de LATEX par
HEVEA.