(**************************************************************************) (* *) (* Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, *) (* Kim Nguyen, Laurent Sartre *) (* *) (* Informatique - MP2I/MPI - CPGE 1re et 2e années. *) (* Cours et exercices corrigés. Éditions Ellipses, 2022. *) (* *) (* https://www.informatique-mpi.fr/ *) (* *) (**************************************************************************) open Prop (* Analyse syntaxique de formules strictes F = True | False | ~ F | ( B ) B = F O F O = \/ | /\ | -> *) (* On modélise l'entrée par une liste de lexèmes, du type suivant. *) type token = TRUE | FALSE | VAR of int | NOT | LPAR | RPAR | OR | AND | IMP | EOF (* Principe de l'analyse : - une fonction par non terminal ; - chacune reçoit en argument une liste de lexèmes, reconnaît un préfixe et renvoie le suffixe non consommé ; - en cas d'erreur syntaxique, on lève `Error`. *) exception Error (* Validation pure *) let rec validateF = function | (TRUE | FALSE | VAR _) :: l -> l | NOT :: l -> validateF l | LPAR :: l -> (match validateB l with | RPAR :: l -> l | _ -> raise Error) | _ -> raise Error and validateB l = match validateF l with | (OR | AND | IMP) :: l -> validateF l | _ -> raise Error (* Attention : pour reconnaître l'entrée, il faut bien vérifier qu'il reste un unique lexème, `Eof`. *) let validate l = try validateF l = [EOF] with Error -> false (* Tests, avec lex réduit *) let of_string s = let char = function | 'T' -> TRUE | 'L' -> FALSE | '0' -> VAR 0 | '~' -> NOT | '&' -> AND | '|' -> OR | '>' -> IMP | '(' -> LPAR | ')' -> RPAR | _ -> invalid_arg "of_string" in let rec build acc i = if i = String.length s then List.rev (EOF :: acc) else build (char s.[i] :: acc) (i + 1) in build [] 0 let accepts s = assert (validate (of_string s)) let rejects s = assert (not (validate (of_string s))) let () = rejects "" let () = rejects "~" let () = accepts "~T" let () = rejects "T|T" let () = accepts "(T&T)" let () = accepts "~((T|~T)|~(~T&T))" let () = rejects "((T&T)" let () = rejects "(T&T))" let () = rejects "(T|(T&))" (* V2 : construction de l'AST *) let rec parseS l = match parseF l with f, [ EOF ] -> f | _ -> raise Error and parseF l = match l with | TRUE :: l -> True, l | FALSE :: l -> False, l | VAR x :: l -> Var x, l | NOT :: l -> let f, l = parseF l in Not f, l | LPAR :: l -> (match parseB l with | f, RPAR :: l -> f, l | _ -> raise Error) | _ -> raise Error and parseB l = let f1, l = parseF l in let op, l = parseO l in let f2, l = parseF l in Bin(op, f1, f2), l and parseO l = match l with | AND :: l -> And, l | OR :: l -> Or, l | IMP :: l -> Imp, l | _ -> raise Error let parse l = try Some (parseS l) with Error -> None (* Tests de l'AST, avec toujours lex réduit *) let parse_accepts s f = assert (parse (of_string s) = Some f) let parse_rejects s = assert (parse (of_string s) = None) let () = parse_rejects "" let () = parse_rejects "~" let () = parse_accepts "~T" (Not True) let () = parse_rejects "T|T" let () = parse_accepts "(T&T)" (Bin (And, True, True)) let () = parse_accepts "~((T|~T)|~(~T&T))" (Not (Bin (Or, Bin (Or, True, Not True), Not (Bin (And, Not True, True))))) let () = parse_rejects "((T&T)" let () = parse_rejects "(T&T))" let () = parse_rejects "(T|(T&))" (* Lex plus intéressant *) (* limitation de cette version : n'accepte pas un blanc final *) let of_string s = (* renvoie symbole et indice de son dernier caractère *) let n = String.length s in let rec token i = match s.[i] with | '(' -> LPAR, i | ')' -> RPAR, i | '~' -> NOT, i | 'V' -> TRUE, i | 'F' -> FALSE, i | '/' -> tand (i + 1) | '\\' -> tor (i + 1) | '-' -> timp (i + 1) | c when '0' <= c && c <= '9' -> tvar i (i + 1) | ' ' -> token (i + 1) | _ -> raise Error and tand i = if i < n && s.[i] = '\\' then AND, i else raise Error and tor i = if i < n && s.[i] = '/' then OR, i else raise Error and timp i = if i < n && s.[i] = '>' then IMP, i else raise Error and tvar i j = if j < n && '0' <= s.[j] && s.[j] <= '9' then tvar i (j + 1) else VAR (int_of_string (String.sub s i (j - i))), j - 1 in let rec build acc i = if i = String.length s then List.rev (EOF :: acc) else let t, i = token i in build (t :: acc) (i + 1) in build [] 0 (* variante qui accepte un blanc final, et qui nomme les variables xN *) let of_string s = let n = String.length s in let rec q_0 i = if i = n then EOF,i else match s.[i] with | '(' -> LPAR, i | ')' -> RPAR, i | '~' -> NOT, i | 'V' -> TRUE, i | 'F' -> FALSE, i | '/' -> q_and (i + 1) | '\\' -> q_or (i + 1) | '-' -> q_imp (i + 1) | 'x' -> q_var (i + 1) (i + 1) | ' ' -> q_0 (i+1) | _ -> raise Error and q_and i = if i < n && s.[i] = '\\' then AND, i else raise Error and q_or i = if i < n && s.[i] = '/' then OR, i else raise Error and q_imp i = if i < n && s.[i] = '>' then IMP, i else raise Error and q_var i j = if j < n && '0' <= s.[j] && s.[j] <= '9' then q_var i (j + 1) else if i = j then raise Error else VAR (int_of_string (String.sub s i (j - i))), j - 1 in let rec build acc i = match q_0 i with EOF, _ -> List.rev (EOF::acc) | token, i -> build (token :: acc) (i+1) in build [] 0 let lex_accepts s l = assert (try of_string s = l with Error -> false) let lex_rejects s = assert (try let _ = of_string s in false with Error -> true) let () = lex_accepts "(" [LPAR; EOF] let () = lex_accepts "()" [LPAR; RPAR; EOF] let () = lex_accepts "(V->F)" [LPAR; TRUE; IMP; FALSE; RPAR; EOF] let () = lex_accepts "V /\\ (F \\/ V)" [TRUE; AND; LPAR; FALSE; OR; TRUE; RPAR; EOF] let () = lex_accepts "x0" [VAR 0; EOF] let () = lex_accepts "~x124" [NOT; VAR 124; EOF] let () = lex_accepts "(x3/\\~x42 )" [LPAR; VAR 3; AND; NOT; VAR 42; RPAR; EOF] let () = lex_accepts "(x12/\\F)" [LPAR; VAR 12; AND; FALSE; RPAR; EOF] let () = lex_accepts "V " [TRUE; EOF] let () = lex_rejects "x" let parse_accepts s f = assert (try parse (of_string s) = Some f with Error -> false) let parse_rejects s = assert (try parse (of_string s) = None with Error -> true) let () = parse_rejects "" let () = parse_rejects "~" let () = parse_accepts "~V" (Not True) let () = parse_rejects "V \\/ V" let () = parse_accepts "(x12/\\F)" (Bin (And, Var 12, False)) let () = parse_accepts "~( (x0\\/~ x42 )\\/ ~(~V /\\F))" (Not (Bin (Or, Bin (Or, Var 0, Not (Var 42)), Not (Bin (And, Not True, False))))) let () = parse_rejects "((V/\\V)" let () = parse_rejects "(V/\\V))" let () = parse_rejects "(V\\/(V/\\))"