Merge branch 'master' of gitlab.aliens-lyon.fr:savrillo/pieuvre

.gitignore

@@ -1,5 +1,6 @@
 _build
 pieuvre
 main.native
+log.8pus
 
 *.kate-swp

README.md

@@ -43,8 +43,11 @@ L'option `alpha` vérifie si deux lambda-termes sont alpha-équivalents. Elle s'
 - Partie interactive
 
 ### Samy
-Introduction du README
+- Introduction du README
-Fonctions de manipulation des λ-termes (pieuvre.ml)
+- Fonctions de manipulation des λ-termes (`pieuvre.ml`)
-Typecheck
+- Typecheck
-Erreurs lors des tactiques.
+- Erreurs lors des tactiques.
-\/ et /\
+- `\/` et `/\`
+- Parsing des λ-termes
+- `True` et `exact`
+- Option `-computetype`

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 }
 

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
 

parser.mly

@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> 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) }

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 *)

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;;

tactic.ml

@@ -8,4 +8,5 @@ type tactic =
   | Cut of ty
   | Split
   | Left
-  | Right;;
+  | Right
+  | Exact of lam;;

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.