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

Intros

Browse Source
This commit is contained in:
Adrien Vannson 2022-05-18 16:36:02 +02:00
parent 2de70d29a7
commit d631cd3e93
No known key found for this signature in database
GPG Key ID: FE2E66FD978C1A55
5 changed files with 54 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
lexer.mll
View File

@ -15,6 +15,7 @@ rule token = parse
| ',' { COMMA } | ',' { COMMA }
| "intro" { INTRO } | "intro" { INTRO }
| "intros" { INTROS }
| "assumption" { ASSUMPTION } | "assumption" { ASSUMPTION }
| "apply" { APPLY } | "apply" { APPLY }
| "elim" { ELIM } | "elim" { ELIM }

62
main.ml
View File

@ -162,28 +162,17 @@ let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in
let fill_holes = ref (fun holes -> List.hd holes) in let fill_holes = ref (fun holes -> List.hd holes) in
while !subgoals <> [] do while !subgoals <> [] do
let (ty, hyps) = List.hd !subgoals in
subgoals := List.tl !subgoals;
let find_hyp (var: var_lambda) : ty option =
let rec explore = function
| [] -> None
| (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
| _ :: hyps -> explore hyps
in
explore hyps
in
if is_interactive then ( if is_interactive then (
(* Nettoyage du terminal *) (* Nettoyage du terminal *)
let _ = Sys.command("clear -x") in let _ = Sys.command("clear -x") in
(* Affichage des hypothèses *) (* Affichage des hypothèses *)
List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps; List.iter
(fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h))
(snd (List.hd !subgoals));
(* Affichage des sous-buts *) (* Affichage des sous-buts *)
Printf.printf "================\n"; Printf.printf "================\n";
Printf.printf "%s\n" (string_of_ty ty);
List.iter (fun (ty, _) -> List.iter (fun (ty, _) ->
Printf.printf "%s\n" (string_of_ty ty) Printf.printf "%s\n" (string_of_ty ty)
) !subgoals; ) !subgoals;
@ -199,23 +188,40 @@ while !subgoals <> [] do
with e -> raise TacticParseException with e -> raise TacticParseException
in in
let applyTactic tactic = let rec applyTactic tactic = (
begin let (ty, hyps) = List.hd !subgoals in
let find_hyp (var: var_lambda) : ty option =
let rec explore = function
| [] -> None
| (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
| _ :: hyps -> explore hyps
in
explore hyps
in
let f = !fill_holes in let f = !fill_holes in
match tactic with match tactic with
| Intro var -> ( | Intro var -> (
match ty with match ty with
| TImpl (ty1, ty2) -> ( | TImpl (ty1, ty2) -> (
subgoals := List.tl !subgoals;
subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals; subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| h :: hs -> f (LFun (var, ty1, h) :: hs) | h :: hs -> f (LFun (var, ty1, h) :: hs)
| _ -> raise TrouException | _ -> raise TrouException
) )
| _ -> raise (TacticException(tactic,"Cannot intro when the goal is no implication.")) | _ -> raise (TacticException(tactic, "Cannot intro when the goal is no implication."))
) )
| Intros [] -> ()
| Intros (t :: ts) -> (
applyTactic (Intro t);
applyTactic (Intros ts)
)
| Assumption -> ( | Assumption -> (
let rec explore = function let rec explore = function
| (var, hyp) :: _ when hyp = ty -> ( | (var, hyp) :: _ when hyp = ty -> (
subgoals := List.tl !subgoals;
fill_holes := fun holes -> f ((LVar var) :: holes) fill_holes := fun holes -> f ((LVar var) :: holes)
) )
| [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal.")) | [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal."))
@ -226,6 +232,7 @@ while !subgoals <> [] do
| Apply var -> ( | Apply var -> (
match find_hyp var with match find_hyp var with
| Some (TImpl (t1, t2)) when t2 = ty -> ( | Some (TImpl (t1, t2)) when t2 = ty -> (
subgoals := List.tl !subgoals;
subgoals := (t1, hyps) :: !subgoals; subgoals := (t1, hyps) :: !subgoals;
fill_holes := function fill_holes := function
| hole :: holes -> f ((LApp (LVar var, hole)) :: holes) | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
@ -236,14 +243,19 @@ while !subgoals <> [] do
) )
| Elim var -> ( | Elim var -> (
match find_hyp var with match find_hyp var with
| Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes) | Some TFalse -> (
subgoals := List.tl !subgoals;
fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
)
| Some TAnd(tl,tr) -> ( | Some TAnd(tl,tr) -> (
subgoals := List.tl !subgoals;
subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals; subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r) | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r)
| _ -> raise TrouException | _ -> raise TrouException
) )
| Some TOr(tl,tr) -> ( | Some TOr(tl,tr) -> (
subgoals := List.tl !subgoals;
subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals; subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| hl::hr::r -> f (LCase(LVar(var),hl,hr)::r) | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r)
@ -254,6 +266,7 @@ while !subgoals <> [] do
) )
(* Pour montrer A, on montre B -> A et B *) (* Pour montrer A, on montre B -> A et B *)
| Cut tint -> ( | Cut tint -> (
subgoals := List.tl !subgoals;
subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals; subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
fill_holes := function fill_holes := function
| pf :: px :: s -> f ((LApp (pf, px)) :: s) | pf :: px :: s -> f ((LApp (pf, px)) :: s)
@ -263,6 +276,7 @@ while !subgoals <> [] do
| Split -> ( | Split -> (
match ty with match ty with
| TAnd(t1,t2) -> ( | TAnd(t1,t2) -> (
subgoals := List.tl !subgoals;
subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals; subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs) | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
@ -273,6 +287,7 @@ while !subgoals <> [] do
| Left -> ( | Left -> (
match ty with match ty with
| TOr(tl,tr) -> ( | TOr(tl,tr) -> (
subgoals := List.tl !subgoals;
subgoals := (tl, hyps) :: !subgoals; subgoals := (tl, hyps) :: !subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| hl :: hs -> f (LIg(hl,tr) :: hs) | hl :: hs -> f (LIg(hl,tr) :: hs)
@ -283,6 +298,7 @@ while !subgoals <> [] do
| Right -> ( | Right -> (
match ty with match ty with
| TOr(tl,tr) -> ( | TOr(tl,tr) -> (
subgoals := List.tl !subgoals;
subgoals := (tr, hyps) :: !subgoals; subgoals := (tr, hyps) :: !subgoals;
fill_holes := fun holes -> match holes with fill_holes := fun holes -> match holes with
| hr :: hs -> f (LId(hr,tl) :: hs) | hr :: hs -> f (LId(hr,tl) :: hs)
@ -291,10 +307,14 @@ while !subgoals <> [] do
| _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause")) | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause"))
) )
| Exact l -> ( | Exact l -> (
if not (typecheck hyps l ty) then raise (TacticException(tactic,"λ-term "^(string_of_lam l)^" cannot be typed with "^(string_of_ty ty)^" as its type is "^(match (computeType [] l) with None -> "None" | Some t -> string_of_ty t))) if not (typecheck hyps l ty) then
else fill_holes := fun holes -> f (l::holes) raise (TacticException(tactic,"λ-term "^(string_of_lam l)^" cannot be typed with "^(string_of_ty ty)^" as its type is "^(match (computeType [] l) with None -> "None" | Some t -> string_of_ty t)))
else (
subgoals := List.tl !subgoals;
fill_holes := fun holes -> f (l::holes)
)
) )
end )
in in
let rec applyUntilWorking () = let rec applyUntilWorking () =

9
parser.mly
View File

@ -10,7 +10,7 @@
%token <string> VAR_NAME %token <string> VAR_NAME
%token <string> TYPE_NAME %token <string> TYPE_NAME
%token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I %token DOT INTRO INTROS ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I
%token FUN MAPS_TO COLON EXF %token FUN MAPS_TO COLON EXF
%token AMPERSAND %token AMPERSAND
@ -63,9 +63,14 @@ ty:
| FALSE { TFalse } | FALSE { TFalse }
| TRUE { TTrue } | TRUE { TTrue }
var_list:
| VAR_NAME { [$1] }
| VAR_NAME var_list { $1 :: $2 }
/* Tactiques */ /* Tactiques */
tactic: tactic:
| INTRO VAR_NAME DOT { Intro $2 } | INTRO VAR_NAME DOT { Intro $2 }
| INTROS var_list DOT { Intros $2 }
| ASSUMPTION DOT { Assumption } | ASSUMPTION DOT { Assumption }
| APPLY VAR_NAME DOT { Apply $2 } | APPLY VAR_NAME DOT { Apply $2 }
| ELIM VAR_NAME DOT { Elim $2 } | ELIM VAR_NAME DOT { Elim $2 }
@ -83,7 +88,7 @@ lambda_arg: /* Expression pouvant être en argument d'une fonction */
| SND LPAREN lambda RPAREN { LSnd ($3) } | SND LPAREN lambda RPAREN { LSnd ($3) }
| IG LPAREN lambda COMMA ty RPAREN { LIg ($3, $5) } | IG LPAREN lambda COMMA ty RPAREN { LIg ($3, $5) }
| ID LPAREN lambda COMMA ty RPAREN { LId ($3, $5) } | ID LPAREN lambda COMMA ty RPAREN { LId ($3, $5) }
| CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN | CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN
{ LCase ($3, $5,$7) } { LCase ($3, $5,$7) }
| I { LI } | I { LI }
| LPAREN lambda COMMA lambda RPAREN { LCouple($2, $4) } | LPAREN lambda COMMA lambda RPAREN { LCouple($2, $4) }

1
tactic.ml
View File

@ -2,6 +2,7 @@ open Structs;;
type tactic = type tactic =
| Intro of var_lambda | Intro of var_lambda
| Intros of var_lambda list
| Assumption | Assumption
| Apply of var_lambda | Apply of var_lambda
| Elim of var_lambda | Elim of var_lambda

4
tests/intros.8pus Normal file
View File

@ -0,0 +1,4 @@
A -> (A -> B) -> B
intros a f.
apply f.
assumption.