allow * in identifiers (#815)

Deducteam · Jan 15, 2022 · efd9e64 · efd9e64
1 parent 089f239
commit efd9e64
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/Logic/Makefile b/Logic/Makefile
@@ -1,7 +1,7 @@
 PKG := TFF U Zenon PTS
 
 .PHONY: default
-default:
+default: clean
 	for p in $(PKG); do $(MAKE) -C $$p; done
 
 %:

diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
@@ -153,7 +153,7 @@ let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
 
 (** Unqualified regular identifiers are any non-empty sequence of characters
    not among: *)
-let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|?/*"]
+let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|/"]
 let regid = [%sedlex.regexp? '/' | '*' | Plus (Compl forbidden_letter)]
 
 let is_regid : string -> bool = fun s ->
@@ -280,7 +280,7 @@ let rec token lb =
   | '_' -> UNDERSCORE
 
   (* identifiers *)
-  | regid -> UID(Utf8.lexeme lb)
+  | '/' | regid -> UID(Utf8.lexeme lb)
   | escid -> UID(remove_useless_escape(Utf8.lexeme lb))
   | '@', regid -> UID_EXPL(remove_first lb)
   | '@', escid -> UID_EXPL(remove_useless_escape(remove_first lb))

diff --git a/tests/OK/identifiers.lp b/tests/OK/identifiers.lp
@@ -0,0 +1,3 @@
+symbol /:TYPE;
+symbol *:TYPE;
+symbol **:TYPE;