renommage des tactiques, implémentation de la tactique try, suppression des tokens inutiles, etc..
This commit is contained in:
Marwan
parent
b1ccb0ad71
commit
d3dcebdb88
@ -15,9 +15,6 @@ rule token = parse
|
||||
| [' ' '\t' '\n'] { token lexbuf }
|
||||
| '.' { DOT }
|
||||
| ',' { COMMA }
|
||||
| '+' { PLUS }
|
||||
| '*' { TIMES }
|
||||
| "True" { TOP }
|
||||
| "False" { BOT }
|
||||
| '(' { LPAREN }
|
||||
| ')' { RPAREN }
|
||||
@ -37,7 +34,6 @@ rule token = parse
|
||||
| "Qed" { QED }
|
||||
| "exact" { EXACT }
|
||||
| "assumption" { ASSUMPTION }
|
||||
| "destruct" { DESTRUCT }
|
||||
| "intros" { INTROS }
|
||||
| "intro" { INTRO }
|
||||
| "cut" { CUT }
|
||||
@ -45,6 +41,7 @@ rule token = parse
|
||||
| "left" { LEFT }
|
||||
| "right" { RIGHT }
|
||||
| "split" { SPLIT }
|
||||
| "try" { TRY }
|
||||
|
||||
| var_id as s { VARID(s) }
|
||||
| ty_id as s { TYID(s) }
|
||||
|
||||
64
main.ml
64
main.ml
@ -5,7 +5,7 @@ open Types
|
||||
open Hlam
|
||||
|
||||
type entry =
|
||||
Simple of (unit -> cmd)
|
||||
Simple of (unit -> instr)
|
||||
| Reduce of Lam.lam
|
||||
| AlphaEquiv of Lam.lam * Lam.lam
|
||||
|
||||
@ -14,11 +14,11 @@ type interactive_state = (hlam * ty) option * proof
|
||||
let parse_lam t =
|
||||
match Parser.main Lexer.token t with
|
||||
| Lam l -> l
|
||||
| Cmd _ -> failwith "entry must be a lam"
|
||||
| Instr _ -> failwith "entry must be a lam"
|
||||
|
||||
let parse_cmd t =
|
||||
match Parser.main Lexer.token t with
|
||||
| Cmd c -> c
|
||||
| Instr is -> is
|
||||
| Lam _ -> failwith "entry must be a cmd"
|
||||
|
||||
let show_beta_reduction e =
|
||||
@ -60,7 +60,7 @@ let alpha_get_lam where_from =
|
||||
- g, gs : next goals
|
||||
- sq : previous states of the interactive loop
|
||||
*)
|
||||
let rec interactive (get_cmd : unit -> cmd) (sl : (interactive_state) list) : proof =
|
||||
let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list) : proof =
|
||||
let (cg, (g, gs)), sq = match sl with
|
||||
[] -> (None, (None, [])), []
|
||||
| s::sq -> s, sq
|
||||
@ -72,38 +72,40 @@ let rec interactive (get_cmd : unit -> cmd) (sl : (interactive_state) list) : pr
|
||||
in
|
||||
|
||||
try
|
||||
match get_cmd () with
|
||||
Goal ty ->
|
||||
let rh = Ref (ref Hole) in
|
||||
[Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_cmd
|
||||
| Undo -> interactive get_cmd sq
|
||||
| Qed -> begin match cg with
|
||||
None ->
|
||||
print_error "No current goal" "";
|
||||
(cg, (g, gs))::sq |> interactive get_cmd
|
||||
| Some (h, t) ->
|
||||
let l = lam_of_hlam h
|
||||
|> beta_reduce in
|
||||
if Typing.typecheck [] l t then begin
|
||||
print_string "Ok";
|
||||
[None, (None, [])] |> interactive get_cmd
|
||||
end else begin
|
||||
print_error "Typing failed" "";
|
||||
print_expr l;
|
||||
print_newline ();
|
||||
print_ty t;
|
||||
(cg, (g, gs))::sq |> interactive get_cmd
|
||||
end
|
||||
match get_instr () with
|
||||
Cmd c -> begin match c with
|
||||
Goal ty ->
|
||||
let rh = Ref (ref Hole) in
|
||||
[Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
|
||||
| Undo -> interactive get_instr sq
|
||||
| Qed -> begin match cg with
|
||||
None ->
|
||||
print_error "No current goal" "";
|
||||
(cg, (g, gs))::sq |> interactive get_instr
|
||||
| Some (h, t) ->
|
||||
let l = lam_of_hlam h
|
||||
|> beta_reduce in
|
||||
if Typing.typecheck [] l t then begin
|
||||
print_string "Ok";
|
||||
[None, (None, [])] |> interactive get_instr
|
||||
end else begin
|
||||
print_error "Typing failed" "";
|
||||
print_expr l;
|
||||
print_newline ();
|
||||
print_ty t;
|
||||
(cg, (g, gs))::sq |> interactive get_instr
|
||||
end
|
||||
end
|
||||
end
|
||||
| Tact t ->
|
||||
(cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_cmd
|
||||
(cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_instr
|
||||
with
|
||||
Parser.Error ->
|
||||
print_error "Invalid input" "";
|
||||
(cg, (g, gs))::sq |> interactive get_cmd
|
||||
(cg, (g, gs))::sq |> interactive get_instr
|
||||
| TacticFailed arg ->
|
||||
print_error "Tactic failed" arg;
|
||||
(cg, (g, gs))::sq |> interactive get_cmd
|
||||
(cg, (g, gs))::sq |> interactive get_instr
|
||||
| End_of_file | Lexer.Eof ->
|
||||
print_string "Bye!\n";
|
||||
(g, gs)
|
||||
@ -176,8 +178,8 @@ let recupere_entree () =
|
||||
let run () =
|
||||
try
|
||||
match recupere_entree () with
|
||||
Simple get_cmd ->
|
||||
let _ = interactive get_cmd [None, (None, [])] in ()
|
||||
Simple get_instr ->
|
||||
let _ = interactive get_instr [None, (None, [])] in ()
|
||||
| Reduce l ->
|
||||
let _ = show_beta_reduction l in ()
|
||||
| AlphaEquiv (l1, l2) -> begin
|
||||
|
||||
34
parser.mly
34
parser.mly
@ -8,8 +8,7 @@ open Parser_entry
|
||||
%token EOF
|
||||
|
||||
%token DOT COMMA
|
||||
%token PLUS TIMES
|
||||
%token TOP BOT EXFALSO TILDE
|
||||
%token BOT EXFALSO TILDE
|
||||
%token LPAREN RPAREN
|
||||
%token FUN ARR COLON TARR
|
||||
%token AND OR
|
||||
@ -18,7 +17,7 @@ open Parser_entry
|
||||
|
||||
%token GOAL UNDO QED
|
||||
%token EXACT ASSUMPTION INTRO INTROS CUT APPLY
|
||||
%token LEFT RIGHT SPLIT DESTRUCT
|
||||
%token LEFT RIGHT SPLIT TRY
|
||||
%token L R
|
||||
|
||||
%right TARR
|
||||
@ -33,26 +32,29 @@ open Parser_entry
|
||||
%%
|
||||
main:
|
||||
| e=expression EOF { Lam e }
|
||||
| ts=nonempty_list(tactic) EOF { Cmd ts }
|
||||
| ts=nonempty_list(instr) EOF { Instr ts }
|
||||
|
||||
tactic:
|
||||
| c=command DOT { c }
|
||||
instr:
|
||||
| c=command DOT { Cmd c }
|
||||
| t=tactic DOT { Tact t }
|
||||
|
||||
command:
|
||||
| GOAL t=ty { Goal t }
|
||||
| UNDO { Undo }
|
||||
| QED { Qed }
|
||||
| EXACT e=expression { Tact (Exact_term e) }
|
||||
| EXACT s=TYID { Tact (Exact_proof s) }
|
||||
| ASSUMPTION { Tact (Assumption) }
|
||||
| INTROS { Tact (Intros) }
|
||||
| INTRO { Tact (Intro) }
|
||||
| SPLIT { Tact (Split) }
|
||||
| RIGHT { Tact (Right) }
|
||||
| LEFT { Tact (Left) }
|
||||
| CUT t=ty { Tact (Cut t) }
|
||||
| APPLY s=TYID { Tact (Apply s) }
|
||||
|
||||
tactic:
|
||||
| EXACT e=expression { TExact_term e }
|
||||
| EXACT s=TYID { TExact_proof s }
|
||||
| ASSUMPTION { TAssumption }
|
||||
| INTROS { TIntros }
|
||||
| INTRO { TIntro }
|
||||
| SPLIT { TSplit }
|
||||
| RIGHT { TRight }
|
||||
| LEFT { TLeft }
|
||||
| CUT t=ty { TCut t }
|
||||
| APPLY s=TYID { TApply s }
|
||||
| TRY t=tactic { TTry t }
|
||||
|
||||
ty_annot:
|
||||
| id=VARID COLON t=ty { (id, t) }
|
||||
|
||||
@ -3,11 +3,14 @@ open Types
|
||||
open Proof
|
||||
|
||||
type cmd =
|
||||
| Goal of ty
|
||||
Goal of ty
|
||||
| Undo
|
||||
| Qed
|
||||
|
||||
type instr =
|
||||
Cmd of cmd
|
||||
| Tact of tactic
|
||||
|
||||
type parser_entry =
|
||||
| Lam of lam
|
||||
| Cmd of cmd list
|
||||
| Instr of instr list
|
||||
|
||||
44
proof.ml
44
proof.ml
@ -7,16 +7,17 @@ type goal = hlam * Types.ty * context
|
||||
type proof = goal option * goal list
|
||||
|
||||
type tactic =
|
||||
Exact_term of lam
|
||||
| Exact_proof of id
|
||||
| Assumption
|
||||
| Intros
|
||||
| Intro
|
||||
| Cut of ty
|
||||
| Apply of id
|
||||
| Split
|
||||
| Right
|
||||
| Left
|
||||
TExact_term of lam
|
||||
| TExact_proof of id
|
||||
| TAssumption
|
||||
| TIntros
|
||||
| TIntro
|
||||
| TCut of ty
|
||||
| TApply of id
|
||||
| TSplit
|
||||
| TRight
|
||||
| TLeft
|
||||
| TTry of tactic
|
||||
|
||||
let hyp_count = ref 0
|
||||
let get_fresh_hyp () =
|
||||
@ -216,18 +217,19 @@ let tact_left ((g, gs) : proof) : proof =
|
||||
Some (new_h, t_l, cs), gs
|
||||
| _ -> raise (TacticFailed "Not a disjunction")
|
||||
|
||||
let apply_tactic (p : proof) (t : tactic) : proof =
|
||||
let rec apply_tactic (p : proof) (t : tactic) : proof =
|
||||
match t with
|
||||
Exact_term e -> tact_exact_term p e
|
||||
| Exact_proof hyp -> tact_exact_proof p hyp
|
||||
| Intros -> tact_intros p
|
||||
| Intro -> tact_intro p
|
||||
| Assumption -> tact_assumption p
|
||||
| Cut t -> tact_cut p t
|
||||
| Apply h -> tact_apply p h
|
||||
| Split -> tact_split p
|
||||
| Right -> tact_right p
|
||||
| Left -> tact_left p
|
||||
TExact_term e -> tact_exact_term p e
|
||||
| TExact_proof hyp -> tact_exact_proof p hyp
|
||||
| TIntros -> tact_intros p
|
||||
| TIntro -> tact_intro p
|
||||
| TAssumption -> tact_assumption p
|
||||
| TCut t -> tact_cut p t
|
||||
| TApply h -> tact_apply p h
|
||||
| TSplit -> tact_split p
|
||||
| TRight -> tact_right p
|
||||
| TLeft -> tact_left p
|
||||
| TTry t -> try apply_tactic p t with TacticFailed _ -> p
|
||||
|
||||
|
||||
let tact_try (p : proof) (t : tactic) : proof =
|
||||
|
||||
Loading…
Reference in New Issue
Block a user