Merge branch 'cut'

lexer.mll

@@ -2,23 +2,22 @@
     open Parser
 }
 
-rule token_ty = parse
+rule token = parse
-  | [' ' '\t' '\n']             { token_ty lexbuf }
+  | [' ' '\t' '\n']             { token lexbuf }
   | eof                         { EOF }
 
   | '('                         { LPAREN }
   | ')'                         { RPAREN }
   | "->"                        { RARROW }
   | '~'                         { TILDE }
-  | "False"                     { FALSE }
-  | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
 
-and token_tactic = parse
-  | [' ' '\t' '\n']             { token_tactic lexbuf }
-  | eof                         { EOF }
   | "intro"                     { INTRO }
   | "assumption"                { ASSUMPTION }
   | "apply"                     { APPLY }
   | "elim"                      { ELIM }
+  | "cut"                       { CUT }
+  | "False"                     { FALSE }
+  
+  | ['A'-'Z']+['0'-'9']* as s   { TYPE_NAME s }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }

main.ml

@@ -48,7 +48,7 @@ show "Please type the formula to prove\n";
 let ty =
     try
         let lexbuf = Lexing.from_string (readline ()) in
-        Parser.main_type Lexer.token_ty lexbuf
+        Parser.main_type Lexer.token lexbuf
     with e -> (
         Printf.printf "Can't parse type\n";
         raise e
@@ -84,7 +84,7 @@ while !subgoals <> [] do
         let rec read_tactic () =
             try
                 let lexbuf = Lexing.from_string (readline ()) in
-                Parser.main_tactic Lexer.token_tactic lexbuf
+                Parser.main_tactic Lexer.token lexbuf
             with e -> (
                   Printf.printf "Can't parse tactic\n";
                   if is_interactive then
@@ -142,6 +142,12 @@ while !subgoals <> [] do
             in
             explore hyps;
         )
+      | Cut tint -> (
+            subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals;
+            fill_holes := function 
+                | (pf::px::s) -> f ((LApp(pf, px))::s)
+                | _ -> fail ()
+        )
 done;
 
 let finalLam = !fill_holes [] in

parser.mly

@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION APPLY ELIM
+%token DOT INTRO ASSUMPTION APPLY ELIM CUT
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -41,3 +41,4 @@ tactic:
   | ASSUMPTION DOT                        { Assumption }
   | APPLY VAR_NAME DOT                    { Apply $2 }
   | ELIM VAR_NAME DOT                     { Elim $2 }
+  | CUT ty DOT                            { Cut $2 }

pieuvre.ml

@@ -16,7 +16,7 @@ let rec string_of_ty (t: ty) : string =
 (* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
 let rec string_of_lam (l: lam) : string = match l with
     | LFun(v,t,l') -> "λ"^v^":"^(string_of_ty t)^" . "^(string_of_lam l')
-    | LApp(l1, l2) -> (string_of_lam l1)^" "^(string_of_lam l2)
+    | LApp(l1, l2) -> "("^(string_of_lam l1)^" "^(string_of_lam l2)^")"
     | LVar(v) -> v
     | LExf(l',t) -> "exf("^(string_of_lam l')^" : "^(string_of_ty t)^")"
 ;;

tactic.ml

@@ -4,4 +4,5 @@ type tactic =
   | Intro of var_lambda
   | Assumption
   | Apply of var_lambda
-  | Elim of var_lambda;;
+  | Elim of var_lambda
+  | Cut of ty;;