Fix #295

kernel/basic.ml

@@ -14,6 +14,10 @@ let string_of_mident s = s
 
 let mident_eq = ident_eq
 
+let mident_of_ident = function
+  | s when String.starts_with ~prefix:"{|" s -> String.(sub s 2 (length s - 4))
+  | s -> s
+
 type name = mident * ident
 
 let mk_name md id = (md, id)

kernel/basic.mli

@@ -25,9 +25,12 @@ val mk_mident : string -> mident
 (** [mident_eq md md'] checks if the two modules identifiers [mid] and [mid'] are equals *)
 val mident_eq : mident -> mident -> bool
 
-(** [string_of_ident id] returns a string of the identifier [id] *)
+(** [string_of_mident id] returns a string of the module identifier [id] *)
 val string_of_mident : mident -> string
 
+(** [mident_of_ident id] transform the identifier [id] into a module identifier *)
+val mident_of_ident : ident -> mident
+
 (** type for constant names such as [foo.bar] *)
 type name
 

parsing/lexer.mll

@@ -50,19 +50,19 @@ rule token = parse
   | "injective" { KW_INJ     ( get_loc lexbuf ) }
   | "thm"       { KW_THM     ( get_loc lexbuf ) }
   | "private"   { KW_PRV     ( get_loc lexbuf ) }
-  | "require"   space+ (mident as md) { REQUIRE (get_loc lexbuf , mk_mident md) }
+  | "require"   { REQUIRE    ( get_loc lexbuf ) }
   | "assert"    { ASSERT     ( get_loc lexbuf ) }
-  | "#NAME"     space+ (mident as md) { NAME    (get_loc lexbuf , mk_mident md) }
-  | "#REQUIRE"  space+ (mident as md) { REQUIRE (get_loc lexbuf , mk_mident md) }    
+  | "#NAME"     { NAME       ( get_loc lexbuf ) }
+  | "#REQUIRE"  { REQUIRE    ( get_loc lexbuf ) }
   | "#EVAL"     { EVAL       ( get_loc lexbuf ) }
   | "#INFER"    { INFER      ( get_loc lexbuf ) }
   | "#CHECK"    { CHECK      ( get_loc lexbuf ) }
   | "#CHECKNOT" { CHECKNOT   ( get_loc lexbuf ) }
-  | "#ASSERT"   { ASSERT     ( get_loc lexbuf ) }  
+  | "#ASSERT"   { ASSERT     ( get_loc lexbuf ) }
   | "#ASSERTNOT"{ ASSERTNOT  ( get_loc lexbuf ) }
   | "#PRINT"    { PRINT      ( get_loc lexbuf ) }
   | "#GDT"      { GDT        ( get_loc lexbuf ) }
-  | "#" { pragma [] lexbuf }    
+  | "#" { pragma [] lexbuf }
   | mident as md '.' (ident as id)
   { QID ( get_loc lexbuf , mk_mident md , mk_ident id ) }
   | ident  as id

parsing/menhir_parser.mly

@@ -80,8 +80,8 @@ let make_declaration ~lid ~parameters ~definibility ~ty md =
 %token <Kernel.Basic.loc> ASSERTNOT
 %token <Kernel.Basic.loc> PRINT
 %token <Kernel.Basic.loc> GDT
-%token <Kernel.Basic.loc*Basic.mident> NAME
-%token <Kernel.Basic.loc*Basic.mident> REQUIRE
+%token <Kernel.Basic.loc> NAME
+%token <Kernel.Basic.loc> REQUIRE
 %token <Kernel.Basic.loc> TYPE
 %token <Kernel.Basic.loc> KW_DEF
 %token <Kernel.Basic.loc> KW_DEFAC
@@ -173,8 +173,8 @@ line:
   | PRINT STRING DOT {fun _ -> Print($1, $2)}
   | GDT   ID     DOT {fun _ -> DTree($1, None, snd $2)}
   | GDT   QID    DOT {fun _ -> let (_,m,v) = $2 in DTree($1, Some m, v)}
-  | n=NAME       DOT {fun _ -> Name(fst n, snd n)}
-  | r=REQUIRE    DOT {fun _ -> Require(fst r,snd r)}
+  | NAME  ID    DOT {fun _ -> Name($1, mident_of_ident (snd $2))}
+  | REQUIRE ID  DOT {fun _ -> Require($1, mident_of_ident (snd $2))}
   | PRAGMA {fun _ -> Pragma (fst $1, snd $1) }
   | EOF              {raise End_of_file}
 

parsing/tokens.ml

@@ -11,14 +11,12 @@ type token =
   | RIGHTSQU
   | RIGHTPAR
   | RIGHTBRA
+  | ID of (loc * ident)
   | QID of (loc * mident * ident)
-  | NAME of (loc * mident)
-  | REQUIRE of (loc * mident)
   | LONGARROW
   | LEFTSQU
   | LEFTPAR
   | LEFTBRA
-  | ID of (loc * ident)
   | FATARROW
   | EOF
   | DOT
@@ -27,6 +25,8 @@ type token =
   | COLON
   | EQUAL
   | ARROW
+  | NAME of loc
+  | REQUIRE of loc
   | EVAL of loc
   | INFER of loc
   | CHECK of loc

tests/OK/invalid-name.dk

@@ -0,0 +1 @@
+0 : Type.

tests/OK/require.dk

@@ -1,3 +1,3 @@
-require def.
+require {|def|}.
 
-x : def.A.
+x : def.A.

tests/OK/require_invalid.dk

@@ -0,0 +1,3 @@
+#REQUIRE {|invalid-name|}.
+
+1 : 0.