PR to update Dk lexer when Dk 2.8 is released

src/parsing/dkLexer.mll

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

tests/OK/FO.dk

@@ -60,19 +60,19 @@ def conj_elim_2 : A:Prop -> B:Prop -> prf (conj A B) -> prf B
 := A:Prop => B:Prop => p:prf (conj A B) => p B (_: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 -> 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 -> 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 => imp (P x) Q)) -> prf Q
-:= P:(Term->Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x => imp (P x) Q))
+def exists_elim: P:(Term -> Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x => imp (P x) Q)) -> prf Q
+:= P:(Term -> Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x => imp (P x) Q))
 	=> p1 Q p2.
 
 (; Equality ;)

tests/OK/domainfree.dk

@@ -1,3 +1,3 @@
 A:Type.
-F:(A->A)->A.
-def f := F (x=>x).
+F:(A -> A) -> A.
+def f := F (x => x).

tests/OK/dotpat.dk

@@ -1,13 +1,13 @@
 N: Type.
 Z: N.
-S: N->N.
+S: N -> N.
 
-def plus: N->N->N.
+def plus: N -> N -> N.
 [y] plus Z     y --> y
 [x,y] plus (S x) y --> S (plus x y).
 
 
-V:   N->Type.
+V:   N -> Type.
 Nil: V Z.
 Con: n:N -> V n -> N -> V (S n).
 

tests/OK/emptySet.dk

@@ -1,10 +1,10 @@
 Set:Type.
 Prop:Type.
 
-def prf:Prop->Type.
+def prf:Prop -> Type.
 
-forall:(Set->Prop)->Prop.
-imp:Prop->Prop->Prop.
+forall:(Set -> Prop) -> Prop.
+imp:Prop -> Prop -> Prop.
 [f] prf (forall f) --> x:Set -> prf (f x)
 
 [A,B] prf (imp A B) --> prf A -> prf B.

tests/OK/firstOrder.dk

@@ -43,6 +43,6 @@ DeMorgan2 : A:Prop -> B:Prop -> prf (imp (or A B) (not (and (not A) (not B)))).
 
 U:Type.
 
-forall       : (U->Prop) -> Prop.
-forall_intro : P:(U->Prop) -> (x:U -> prf (P x)) -> prf (forall P).
-forall_elim  : P:(U->Prop) -> prf (forall P) -> x:U -> prf (P x).
+forall       : (U -> Prop) -> Prop.
+forall_intro : P:(U -> Prop) -> (x:U -> prf (P x)) -> prf (forall P).
+forall_elim  : P:(U -> Prop) -> prf (forall P) -> x:U -> prf (P x).

tests/OK/firstOrder_v2.dk

@@ -58,16 +58,16 @@ def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B
 	lem B B (q:prf B => q) (q:prf (not B) => false_elim B (p (x:prf A => q))).
 
 (; 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) => q:prf (forall (u:Term => not (P u))) => q t p.
 
 e: (Term -> Prop) -> Term. (;Hilbert operator;)
-exists_elim: P:(Term->Prop) -> prf (exists P) -> prf (P (e P)).
+exists_elim: P:(Term -> Prop) -> prf (exists P) -> prf (P (e P)).
 

tests/OK/nonlin.dk

@@ -8,7 +8,7 @@ S : Nat -> Nat.
 def plus : Nat -> Nat -> Nat.
 [n] plus 0 n --> n
 [m, n] plus (S m) n --> S (plus m n)
-[n] plus n 0--> n
+[n] plus n 0 --> n
 [m, n] plus m (S n) --> S (plus m n).
 
 def eq : (Nat -> Nat) -> (Nat -> Nat) -> Nat.

tests/OK/surjective.dk

@@ -1,8 +1,8 @@
 T:Type.
 Pairs:Type.
-def p1:Pairs->T.
-def p2:Pairs->T.
-def mk:T->T->Pairs.
+def p1:Pairs -> T.
+def p2:Pairs -> T.
+def mk:T -> T -> Pairs.
 
 [a] p1 (mk a _) --> a.
 [b] p2 (mk _ b) --> b.

tests/OK/tuto.dk

@@ -132,7 +132,7 @@ def pred : Nat -> Nat.
 def plus : Nat -> Nat -> Nat.
 [n] plus 0 n --> n
 [m, n] plus (S m) n --> S (plus m n)
-[n] plus n 0--> n
+[n] plus n 0 --> n
 [m, n] plus m (S n) --> S (plus m n).
 
 def plus_rec_term : Nat -> Nat -> Nat.