Mysaa/pieuvre
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Ajout du cut, un peu buggé pour l'instant.

Browse Source
This commit is contained in:
Mysaa 2022-05-10 14:17:35 +02:00
parent ed4471da44
commit a1276102a7
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
5 changed files with 19 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
lexer.mll
View File

@ -2,22 +2,21 @@
open Parser
}
rule token_ty = parse
| [' ' '\t' '\n'] { token_ty lexbuf }
rule token = parse
| [' ' '\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 }
| "cut" { CUT }
| "False" { FALSE }
| ['A'-'Z']+['0'-'9']* as s { TYPE_NAME s }
| ['a'-'z']+['0'-'9']* as s { VAR_NAME s }
| '.' { DOT }

10
main.ml
View File

@ -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
@ -132,6 +132,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

3
parser.mly
View File

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

2
pieuvre.ml
View File

@ -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)^")"
;;

3
tactic.ml
View File

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