allow more letters in identifiers (#333)

- allow ' as first letter in an identifier (fix #328) 
- allow more letters in identifiers: + * ~ & ^ @ = $ % / < | \ - >

The main modifs are in parsing/lexer.mll and parsing/menhir_parser.mly.
Spaces are added in test files (e.g. writing A -> A instead of A->A).
The error code for tests/KO/nsteps1.dk (`#EVAL[-1]`) is changed in tests/main.ml from lexing error to scoping error because '-' is now allowed in identifiers but the argument of `#EVAL` must be a non-negative integer.

libraries/theories/fol.dk

@@ -61,19 +61,19 @@ def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B
 := A:Prop => B:Prop => p:prf (and A B) => p B (a:prf A => b:prf B => b).
 
 (; Universal quantificator ;)
-def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P)
-:= P:(Term->Prop) => p:(t:Term -> prf (P t)) => p.
+def forall_intro: P:(Term -> Prop) -> (t:Term -> prf (P t)) -> prf (forall P)
+:= P:(Term -> Prop) => p:(t:Term -> prf (P t)) => p.
 
-def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t)
-:= P:(Term->Prop) => t:Term => p:prf (forall P) => p t.
+def forall_elim: P:(Term -> Prop) -> t:Term -> p:prf (forall P) -> prf (P t)
+:= P:(Term -> Prop) => t:Term => p:prf (forall P) => p t.
 
 (; Existential quantificator ;)
-def exists_intro: P:(Term->Prop) -> t:Term -> prf (P t) -> prf (exists P)
+def exists_intro: P:(Term -> Prop) -> t:Term -> prf (P t) -> prf (exists P)
 := P:(Term -> Prop) => t:Term => p:prf (P t) =>
 	A:Prop => f:(x:Term -> prf (P x) -> prf A) => f t p.
 
-def exists_elim: P:(Term->Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x : Term => imp (P x) Q)) -> prf Q
-:= P:(Term->Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x : Term => imp (P x) Q))
+def exists_elim: P:(Term -> Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x : Term => imp (P x) Q)) -> prf Q
+:= P:(Term -> Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x : Term => imp (P x) Q))
 	=> p1 Q p2.
 
 

libraries/theories/ott.dk

@@ -177,7 +177,7 @@ coh : A : type -> B : type -> Q : Proof (EQ A B) -> a : term A ->
    b1 a1 (a0 a1 Qa) (Qb a1 (a0 a1 Qa) (H a1 Qa)) (x (a0 a1 Qa)))
   (fst (proof (EQ A1 A0))
        (__ : Proof (EQ A1 A0) =>
-        proof (all A1 (x1 : term A1=> all A0 (x0 : term A0 =>
+        proof (all A1 (x1 : term A1 => all A0 (x0 : term A0 =>
                imp (eq A1 x1 A0 x0) (EQ (B0 x0) (B1 x1))))))
        Q)
   (a1 : term A1 => Q : Proof (EQ A1 A0) => coe A1 A0 Q a1)

parsing/lexer.mll

@@ -21,9 +21,9 @@
 }
 
 let space   = [' ' '\t' '\r']
+let letter = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' '+' '*' '~' '&' '^' '@' '=' '$' '%' '/' '<' '|' '-' '\\' '>']
 let mident = ['a'-'z' 'A'-'Z' '0'-'9' '_']+
-let ident   = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?']['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' ]*
-let capital = ['A'-'Z']+
+let ident = letter+
 
 rule token = parse
   | space       { token lexbuf  }

parsing/menhir_parser.mly

@@ -27,7 +27,9 @@ let mk_config loc lid =
     | "CBN"  when !strat    = None -> strat    := Some ByName
     | "CBV"  when !strat    = None -> strat    := Some ByValue
     | "CBSV" when !strat    = None -> strat    := Some ByStrongValue
-    | i      when !nb_steps = None -> nb_steps := Some (int_of_string i)
+    | i      when !nb_steps = None ->
+       let n = int_of_string i in
+       if n < 0 then raise Exit else nb_steps := Some n
     | _ -> raise Exit in
   try
     List.iter proc lid;

tests/KO/SR_unsat_1.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must* or *may* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a)) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t y      ) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a)) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t y      ) --> A.

tests/KO/SR_unsat_2.dk

@@ -15,5 +15,5 @@ def b : A -> A -> A.
    See SR_sat.dk for examples of satisfiable constraints.
 ;)
 
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a)) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c a (c a y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A ->  T (b x a)) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c a (c a y))) --> A.

tests/KO/SR_unsat_a1.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must* or *may* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x y)) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (b x x)) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A ->  T (c x y)) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (b x x)) --> A.

tests/KO/SR_unsat_a2.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must* or *may* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x y)) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c x (Y x))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A ->  T (c x y)) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c x (Y x))) --> A.

tests/KO/SR_unsat_a2_2.dk

@@ -19,8 +19,8 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must* or *may* contain y ;)
-def a2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c (c a x) a) (c a y))) -> Type.
-[X,Y] a2  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y x) (Y y))) --> A.
+def a2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (c (c a x) a) (c a y))) -> Type.
+[X,Y] a2  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y x) (Y y))) --> A.
 (; From the following constraints:
     Y x = c (c a x) a
     Y y = c a y

tests/KO/SR_unsat_b1.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must*, *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c y x)) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A ->  T (c x (X (c y y) a))) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c y x)) --> A.

tests/KO/SR_unsat_b2.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must*, *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y y) y)) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a))) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y y) y)) --> A.

tests/KO/SR_unsat_b3.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *must*, *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y y) (b y y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a))) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y y) (b y y))) --> A.

tests/KO/SR_unsat_c1.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x     (b x x))) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y x) (c x y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x     (b x x))) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y x) (c x y))) --> A.

tests/KO/SR_unsat_c2.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must* or *may* contain x
           and *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x     (b x x))) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y y) (b x y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x     (b x x))) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y y) (b x y))) --> A.

tests/KO/SR_unsat_e1.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must*, *may* or *may not* contain x
           and *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a      )) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (Y x) (c a y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a      )) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (Y x) (c a y))) --> A.

tests/KO/SR_unsat_e2.dk

@@ -19,5 +19,5 @@ def b : A -> A -> A.
    are convertible with
    terms that *must*, *may* or *may not* contain x
           and *may* or *may not* contain y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a      )) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c y (c a y))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a      )) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c y (c a y))) --> A.

tests/KO/SR_unsat_f1.dk

@@ -18,5 +18,5 @@ def b : A -> A -> A.
 (; Terms that *may not* contain x or y
    are convertible with
    terms that *may* or *may not* contain x or y ;)
-def   d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b a a)) -> Type.
-[X,Y] d  (x=>y=>X x y)   (y=>Y y)    ( x => y => t (c (c a y) (b a a))) --> A.
+def   d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b a a)) -> Type.
+[X,Y] d  (x => y => X x y)   (y => Y y)    (x => y => t (c (c a y) (b a a))) --> A.

tests/KO/def.dk

@@ -1,3 +1,3 @@
 A : Type.
-P : A->Type.
+P : A -> Type.
 def magic (a1:A) (a2:A) (H:P a1) : P a2 := H.

tests/KO/typing_abstraction.dk

@@ -1,6 +1,6 @@
 A : Type.
 y : A.
-P : A->Type.
+P : A -> Type.
 p : P y.
 id : x:A -> P x -> P x.
 def T : P y.

tests/KO/unsound.dk

@@ -8,8 +8,8 @@ def A:Type.
 [] A --> Nat.
 
 
-g:X->Nat.
-f:Nat->X.
+g:X -> Nat.
+f:Nat -> X.
 
 def l1 := x:Nat => g (f x).
 def l2 := y:A => l1 y.