From fc7317b2d06e9e87b7e757972cfe99e19fd453d8 Mon Sep 17 00:00:00 2001
From: Adrien Vannson <adrien.vannson@protonmail.com>
Date: Sun, 8 May 2022 20:03:29 +0200
Subject: [PATCH] Parse tactics

---
 lexer.mll  | 14 ++++++++++----
 main.ml    | 18 ++++++++++++++++--
 parser.mly | 17 ++++++++++++++---
 structs.ml | 15 ++++++++-------
 4 files changed, 48 insertions(+), 16 deletions(-)

diff --git a/lexer.mll b/lexer.mll
index 75dc89a..e8bfc32 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -2,14 +2,20 @@
     open Parser
 }
 
-rule token = parse
-  (* Sauter les espaces et les tabulations  *)
-  | [' ' '\t' '\n']             { token lexbuf }
+rule token_ty = parse
+  | [' ' '\t' '\n']             { token_ty lexbuf }
+  | eof                         { EOF }
+
   | '('                         { LPAREN }
   | ')'                         { RPAREN }
   | "->"                        { RARROW }
   | '~'                         { TILDE }
   | "False"                     { FALSE }
-  | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
+
+and token_tactic = parse
+  | [' ' '\t' '\n']             { token_tactic lexbuf }
   | eof                         { EOF }
+  | "intro"                     { INTRO }
+  | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
+  | '.'                         { DOT }
diff --git a/main.ml b/main.ml
index 2a9f946..4d15231 100644
--- a/main.ml
+++ b/main.ml
@@ -45,7 +45,7 @@ show "Please type the formula to prove\n";
 let ty =
     try
         let lexbuf = Lexing.from_string (readline ()) in
-        Parser.main_type Lexer.token lexbuf
+        Parser.main_type Lexer.token_ty lexbuf
     with e -> (
         Printf.printf "Can't parse type\n";
         raise e
@@ -66,7 +66,21 @@ while true do
         (* Lecture d'une tactique *)
         Printf.printf "What do you want to do?\n";
 
-        let line = read_line () in
+        let tactic =
+            let rec read_tactic () =
+                try
+                    let lexbuf = Lexing.from_string (readline ()) in
+                    Parser.main_tactic Lexer.token_tactic lexbuf
+                with e -> (
+                    Printf.printf "Can't parse tactic\n";
+                    if is_interactive then
+                        read_tactic ()
+                    else
+                        raise e
+                )
+            in
+            read_tactic ()
+        in
         ()
     )
 done;
diff --git a/parser.mly b/parser.mly
index c4a1129..7c23383 100644
--- a/parser.mly
+++ b/parser.mly
@@ -1,12 +1,16 @@
 %{
     open Structs;;
+    open Tactic;;
 %}
 
 /* Description des lexèmes définis dans lexer.mll */
 %token LPAREN RPAREN RARROW TILDE FALSE
+%token EOF
+
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
-%token ENDL EOF
+
+%token DOT INTRO
 
 /* L'ordre de définition définit la priorité */
 %left RARROW
@@ -15,9 +19,10 @@
 %start main_type
 %type <Structs.ty> main_type
 
-/* Définition des règles de grammaire */
-%%
+%start main_tactic
+%type <Tactic.tactic> main_tactic
 
+%%
 main_type:
   | ty EOF                                { $1 }
 
@@ -27,3 +32,9 @@ ty:
   | TYPE_NAME                             { TSimple $1 }
   | TILDE ty                              { TImpl ($2, TFalse) }
   | FALSE                                 { TFalse }
+
+main_tactic:
+  | tactic EOF                            { $1 }
+
+tactic:
+  | INTRO VAR_NAME DOT                    { Intro $2 }
diff --git a/structs.ml b/structs.ml
index 570c406..5b14ed0 100644
--- a/structs.ml
+++ b/structs.ml
@@ -1,28 +1,29 @@
 (* Variables des λ-termes *)
-type var = string;;
+type var_lambda = string;;
+type var = var_lambda;; (* TODEL *)
 let varRegex = Str.regexp "^([a-z]+)([0-9]*)$";;
 
 (* Variable des types simples *)
-type type_var = string;;
-type tvar = type_var;; (* TODEL *)
+type var_type = string;;
+type tvar = var_type;; (* TODEL *)
 
 let tvarRegex = Str.regexp "^([A-Z]+)([0-9]*)$";;
 
 (* Type complexe *)
 type ty =
-    | TSimple of type_var
+    | TSimple of var_type
     | TImpl of ty * ty
     | TFalse;;
 
 (* λ-terme *)
 type lam =
-    | LFun of var * ty * lam
+    | LFun of var_lambda * ty * lam
     | LApp of lam * lam
-    | LVar of var
+    | LVar of var_lambda
     | LExf of lam * ty;;
 
 (* Environnement de typage *)
-type gam = (type_var * ty) list;;
+type gam = (var_type * ty) list;;
 
 (* λ-terme avec des trous *)
 type lho = (lam list) -> lam;;