Lecture d'une formule à prouver

lexer.mll

@@ -0,0 +1,13 @@
+{
+    open Parser
+}
+
+rule token = parse
+  (* Sauter les espaces et les tabulations  *)
+  | [' ' '\t' '\n']             { token lexbuf }
+  | '('                         { LPAREN }
+  | ')'                         { RPAREN }
+  | "->"                        { RARROW }
+  | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
+  | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
+  | eof                         { EOF }

main.ml

@@ -1,4 +1,52 @@
-open Structs
+open Structs;;
-open Pieuvre
+open Pieuvre;;
 
-let _ = print_string (string_of_ty (TImpl(TSimple("A"),TFalse)));;
+(* Parsage des arguments*)
+let filename = ref "" in
+let reduce = ref false in
+let alpha = ref false in
+let typecheck = ref false in
+
+Arg.parse
+    [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
+     ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
+     ("-typecheck", Arg.Set typecheck, "Check if a lambda term has a given type")]
+    (fun s -> filename := s)
+    "The available options are:";
+
+(* Ouverture éventuelle du fichier *)
+let file = match !filename with
+  | "" -> None
+  | fn -> Some (open_in fn)
+in
+
+let readline () = match file with
+  | None -> (
+        Printf.printf ">>> ";
+        flush stdout;
+        let line = ref "" in
+        Scanf.scanf "%s" (fun s -> line := s);
+        !line
+    )
+  | Some f -> input_line f
+in
+
+(* Show a message only if the input is read from stdin *)
+let show s = match file with
+  | None -> Printf.printf "%s" s
+  | _ -> ()
+in
+
+show "Please type the formula to prove\n";
+
+let ty =
+    try
+        let lexbuf = Lexing.from_string (readline ()) in
+        Parser.main_type Lexer.token lexbuf
+    with e -> (
+        Printf.printf "Can't parse type\n";
+        raise e
+    )
+in
+
+Printf.printf "%s\n" (string_of_ty ty);;

parser.mly

@@ -0,0 +1,26 @@
+%{
+    open Structs;;
+%}
+
+/* Description des lexèmes définis dans lexer.mll */
+%token LPAREN RPAREN RARROW
+%token <string> VAR_NAME
+%token <string> TYPE_NAME
+%token ENDL EOF
+
+/* L'ordre de définition définit la priorité */
+%left RARROW
+
+%start main_type
+%type <Structs.ty> main_type
+
+/* Définition des règles de grammaire */
+%%
+
+main_type:
+  | ty EOF                                { $1 }
+
+ty:
+  | LPAREN ty RPAREN                      { $2 }
+  | ty RARROW ty                          { TImpl ($1, $3) }
+  | TYPE_NAME                             { TSimple $1 }

structs.ml

@@ -1,25 +1,28 @@
 (* Variables des λ-termes *)
 type var = string;;
 let varRegex = Str.regexp "^([a-z]+)([0-9]*)$";;
+
 (* Variable des types simples *)
-type tvar = string;;
+type type_var = string;;
+type tvar = type_var;; (* TODEL *)
+
 let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)$";;
 
 (* Type complexe *)
 type ty =
-    | TSimple of tvar
+    | TSimple of type_var
     | TImpl of ty * ty
     | TFalse;;
 
 (* λ-terme *)
-type lam = 
+type lam =
     | LFun of var * ty * lam
     | LApp of lam * lam
     | LVar of var
     | LExf of lam * ty;;
 
 (* Environnement de typage *)
-type gam = (tvar * ty) list;;
+type gam = (type_var * ty) list;;
 
 (* λ-terme avec des trous *)
 type lho = (lam list) -> lam;;