From d8f791328d9394aec2cda22958fc001c47adf39e Mon Sep 17 00:00:00 2001 From: Mysaa Date: Wed, 18 May 2022 00:53:01 +0200 Subject: [PATCH] Ajout de True et de la tactique exact. --- .gitignore | 1 + README.md | 12 ++++++++---- lexer.mll | 3 +++ main.ml | 30 +++++++++++++++++++++++++++++- parser.mly | 13 +++++++++++-- pieuvre.ml | 9 +++++++-- structs.ml | 3 ++- tactic.ml | 3 ++- tests/vrai-pas-faux.8pus | 8 ++++++++ 9 files changed, 71 insertions(+), 11 deletions(-) create mode 100644 tests/vrai-pas-faux.8pus diff --git a/.gitignore b/.gitignore index 93424b3..2061421 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ _build pieuvre main.native +log.8pus *.kate-swp diff --git a/README.md b/README.md index d6f9798..d299a25 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,11 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s' - Option `typecheck` ### Samy -Fonctions de manipulation des λ-termes (pieuvre.ml) -Typecheck -Erreurs lors des tactiques. -\/ et /\ +- Fonctions de manipulation des λ-termes (`pieuvre.ml`) +- Typecheck +- Erreurs lors des tactiques. +- `\/` et `/\` +- Parsing des λ-termes +- `True` et `exact` +- Option `-computetype` + diff --git a/lexer.mll b/lexer.mll index c68d9bf..50d8ad5 100644 --- a/lexer.mll +++ b/lexer.mll @@ -22,8 +22,10 @@ rule token = parse | "split" { SPLIT } | "left" { LEFT } | "right" { RIGHT } + | "exact" { EXACT } | "False" { FALSE } + | "True" { TRUE } | "fun" { FUN } | "=>" { MAPS_TO } @@ -34,6 +36,7 @@ rule token = parse | "ig" { IG } | "id" { ID } | "case" { CASE } + | 'I' { I } | '&' { AMPERSAND } diff --git a/main.ml b/main.ml index 2819cb1..2fd67c4 100644 --- a/main.ml +++ b/main.ml @@ -16,11 +16,13 @@ let filename = ref "" in let reduce_option = ref false in let alpha_option = ref false in let typecheck_option = ref false in +let computetype_option = ref false in Arg.parse [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term"); ("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible"); - ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")] + ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type"); + ("-computetype", Arg.Set computetype_option, "Computes the type of the input λ-term")] (fun s -> filename := s) "The available options are:"; @@ -96,6 +98,28 @@ if !typecheck_option then ( exit 0 ); +if !computetype_option then ( + let lexbuf = Lexing.from_channel (match file with + | None -> stdin + | Some file -> file + ) + in + let lambda_term = + try + Parser.main_lambda Lexer.token lexbuf + with e -> ( + Printf.printf "Can't read lambda term\n"; + raise e + ) + in + begin + match (computeType [] lambda_term) with + | Some t -> Printf.printf "The type of %s is %s\n" (string_of_lam lambda_term) (string_of_ty t) + | None -> Printf.printf "λ-term %s cannot be typed ! (Therfore, it has to be either wrong or not closed)\n" (string_of_lam lambda_term) + end; + exit 0 +); + (* Affiche un message si l'entrée est lue sur stdin *) let show s = match file with | None -> Printf.printf "%s" s @@ -266,6 +290,10 @@ while !subgoals <> [] do ) | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause")) ) + | 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))) + else fill_holes := fun holes -> f (l::holes) + ) end in diff --git a/parser.mly b/parser.mly index 14ed0e3..c6381f1 100644 --- a/parser.mly +++ b/parser.mly @@ -10,7 +10,7 @@ %token VAR_NAME %token TYPE_NAME -%token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT FST SND IG ID CASE +%token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT EXACT FST SND IG ID CASE I %token FUN MAPS_TO COLON EXF %token AMPERSAND @@ -73,10 +73,20 @@ tactic: | SPLIT DOT { Split } | LEFT DOT { Left } | RIGHT DOT { Right } + | EXACT lambda DOT { Exact $2 } /* Lambda-termes */ lambda_arg: /* Expression pouvant être en argument d'une fonction */ | VAR_NAME { LVar $1 } + | EXF LPAREN lambda COLON ty RPAREN { LExf ($3, $5) } + | FST LPAREN lambda RPAREN { LFst ($3) } + | SND LPAREN lambda RPAREN { LSnd ($3) } + | IG LPAREN lambda COMMA ty RPAREN { LIg ($3, $5) } + | ID LPAREN lambda COMMA ty RPAREN { LId ($3, $5) } + | CASE LPAREN lambda COMMA lambda COMMA lambda RPAREN + { LCase ($3, $5,$7) } + | I { LI } + | LPAREN lambda COMMA lambda RPAREN { LCouple($2, $4) } | LPAREN lambda RPAREN { $2 } /* Application d'une fonction */ @@ -89,4 +99,3 @@ lambda: | FUN VAR_NAME COLON ty MAPS_TO lambda { LFun ($2, $4, $6) } | FUN LPAREN VAR_NAME COLON ty RPAREN MAPS_TO lambda { LFun ($3, $5, $8) } - | EXF LPAREN VAR_NAME COLON ty RPAREN { LExf (LVar $3, $5) } diff --git a/pieuvre.ml b/pieuvre.ml index 45d040a..29ee56c 100644 --- a/pieuvre.ml +++ b/pieuvre.ml @@ -25,7 +25,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') + | LFun(v,t,l') -> "(fun "^v^":"^(string_of_ty t)^" => "^(string_of_lam l')^")" | 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)^")" @@ -35,6 +35,7 @@ let rec string_of_lam (l: lam) : string = match l with | LIg(ll,t) -> "ig("^(string_of_lam ll)^","^(string_of_ty t)^")" | LId(ll,t) -> "id("^(string_of_lam ll)^","^(string_of_ty t)^")" | LCase(ll,lg,ld) -> "case("^(string_of_lam ll)^","^(string_of_lam lg)^","^(string_of_lam ld)^")" + | LI -> "I" ;; let split, tsplit = @@ -64,6 +65,7 @@ let findFreeName (l: lam) (x: var) = | LIg(l',t) -> finder l' | LId(l',t) -> finder l' | LCase(ll,lg,ld) -> (finder ll; finder lg; finder ld) + | LI -> () in finder l; @@ -121,6 +123,7 @@ let rec replace (l: lam) (x: var) (s: lam) = match l with | LIg(l',t) -> LIg(replace l' x s, t) | LId(l',t) -> LId(replace l' x s, t) | LCase(l',lg,ld) -> LCase(replace l' x s, replace lg x s, replace ld x s) + | LI -> LI ;; @@ -140,6 +143,7 @@ let rec alpha (l1: lam) (l2: lam) : bool = | (LIg(l1,t1),LIg(l2,t2)) -> t1=t2 && alpha l1 l2 | (LId(l1,t1),LId(l2,t2)) -> t1=t2 && alpha l1 l2 | (LCase(l1,lg1,ld1),LCase(l2,lg2,ld2)) -> (alpha l1 l2) && (alpha lg1 lg2) && (alpha ld1 ld2) + | (LI,LI) -> true | _ -> false (* Les deux formules n'ont pas la même structure *) ;; @@ -183,6 +187,7 @@ let rec betastep (l: lam) : lam option = match l with | (LId(_,_),None) -> Some ld | (_,None) -> None end + | LI -> None ;; @@ -230,7 +235,7 @@ let rec computeType (env: gam) (l: lam) : ty option = | (Some TOr(t1a,t1b),Some TImpl(t2a,t2c),Some TImpl(t3b,t3c)) when t1a=t2a && t1b=t3b && t2c=t3c -> Some t3c | _ -> None end - + | LI -> Some TTrue ;; (* Vérifie que le λ-terme l sous l'environnement env a bien le type t *) diff --git a/structs.ml b/structs.ml index 676bf18..293aae9 100644 --- a/structs.ml +++ b/structs.ml @@ -29,7 +29,8 @@ type lam = | LSnd of lam | LIg of lam * ty | LId of lam * ty - | LCase of lam * lam * lam;; + | LCase of lam * lam * lam + | LI;; (* Environnement de typage *) type gam = (var_type * ty) list;; diff --git a/tactic.ml b/tactic.ml index 4afcb6f..1aa4aaa 100644 --- a/tactic.ml +++ b/tactic.ml @@ -8,4 +8,5 @@ type tactic = | Cut of ty | Split | Left - | Right;; + | Right + | Exact of lam;; diff --git a/tests/vrai-pas-faux.8pus b/tests/vrai-pas-faux.8pus new file mode 100644 index 0000000..9d8bfd1 --- /dev/null +++ b/tests/vrai-pas-faux.8pus @@ -0,0 +1,8 @@ +(True \/ False) /\ (~(False /\ True)) +split. +left. +exact I. +intro x. +elim x. +intro a. +elim a.