Merge pull request #971 from CakeML/candle-parser-bugs

Fix parsing of x.(y) in Candle
CakeML · Aug 28, 2023 · a500b99 · a500b99
2 parents 69cb57a + e9d2602
commit a500b99
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 14 deletions.
diff --git a/compiler/parsing/ocaml/camlPEGScript.sml b/compiler/parsing/ocaml/camlPEGScript.sml
@@ -580,10 +580,10 @@ Definition camlPEG_def[nocompute]:
        seql [try (pnt nPrefixOp); pnt nEBase] (bindNT nEPrefix));
       (* -- Expr14.6 ------------------------------------------------------- *)
       (INL nArrIdx,
-       seql [tokeq DotParenT; pnt nExpr; tokeq RparT]
+       seql [tokeq DotT; tokeq LparT; pnt nExpr; tokeq RparT]
             (bindNT nArrIdx));
       (INL nStrIdx,
-       seql [tokeq DotBrackT; pnt nExpr; tokeq RbrackT]
+       seql [tokeq DotT; tokeq LbrackT; pnt nExpr; tokeq RbrackT]
             (bindNT nStrIdx));
       (INL nEIndex,
        seql [pnt nEPrefix; try (choicel [pnt nStrIdx; pnt nArrIdx])]

diff --git a/compiler/parsing/ocaml/camlPtreeConversionScript.sml b/compiler/parsing/ocaml/camlPtreeConversionScript.sml
@@ -2125,18 +2125,20 @@ Definition ptree_Expr_def:
   (ptree_Index (Nd (nterm,locs) args) =
      if nterm = INL nArrIdx then
        case args of
-         [dotp; expr; rpar] =>
+         [dott; lpar; expr; rpar] =>
            do
-             expect_tok dotp DotParenT;
+             expect_tok dott DotT;
+             expect_tok lpar LparT;
              expect_tok rpar RparT;
              fmap INR $ ptree_Expr nExpr expr
            od
        | _ => fail (locs, «Impossible: nArrIdx»)
      else if nterm = INL nStrIdx then
        case args of
-         [dotb; expr; rbrack] =>
+         [dott; lbrack; expr; rbrack] =>
            do
-             expect_tok dotb DotBrackT;
+             expect_tok dott DotT;
+             expect_tok lbrack LbrackT;
              expect_tok rbrack RbrackT;
              fmap INL $ ptree_Expr nExpr expr
            od

diff --git a/compiler/parsing/ocaml/camlTestsScript.sml b/compiler/parsing/ocaml/camlTestsScript.sml
@@ -1517,5 +1517,20 @@ val _ = parsetest0 “nExpr” “ptree_Expr nExpr”
   (SOME “App Opapp [Var (Long "Int" (Short "~")); Lit (IntLit 1)]”)
   ;
 
+(* 2023-08-25: Parse .( as two tokens and make sure structure projection of
+   parenthesized things works and isn't parsed as array indexing.
+ *)
+
+val _ = parsetest0 “nExpr” “ptree_Expr nExpr”
+  "a . ( i)"
+  (SOME “App Opapp [App Opapp [Var (Long "Array" (Short "sub")); V "a"];
+                               V "i"]”)
+  ;
+
+val _ = parsetest0 “nExpr” “ptree_Expr nExpr”
+  "Double.(-)"
+  (SOME “Var (Long "Double" (Short "-"))”)
+  ;
+
 val _ = export_theory ();
 
diff --git a/compiler/parsing/ocaml/caml_lexScript.sml b/compiler/parsing/ocaml/caml_lexScript.sml
@@ -31,9 +31,9 @@ Datatype:
     | EqualT | TickT | LparT | RparT | HashT | StarT | PlusT | CommaT | MinusT
     | LessT | GreaterT | LbrackT | RbrackT | LbraceT | RbraceT | QuestionT
     | SemiT | SemisT | BarT | OrelseT | AmpT | AndalsoT | NeqT | MinusFT
-    | RarrowT | LarrowT | DotT | DotsT | DotParenT | DotBrackT | DotBraceT
-    | EscapeT | ColonT | ColonsT | UpdateT | SealT | AnyT | BtickT | TildeT
-    | LqbraceT | RqbraceT | LqbrackT | RqbrackT | RrbrackT | LlbrackT | RlbrackT
+    | RarrowT | LarrowT | DotT | DotsT | EscapeT | ColonT | ColonsT | UpdateT
+    | SealT | AnyT | BtickT | TildeT | LqbraceT | RqbraceT | LqbrackT
+    | RqbrackT | RrbrackT | LlbrackT | RlbrackT
     (* special HOL Light tokens (all infixes): *)
     | FuncompT | F_FT
     | THEN_T | THENC_T | THENL_T | THEN_TCL_T
@@ -482,8 +482,6 @@ Definition next_sym_def:
       case skip_comment (TL cs) 0 (next_loc 2 loc) of
       | NONE => SOME (ErrorS, Locs loc (next_loc 2 loc), "")
       | SOME (rest, loc') => next_sym rest loc'
-    else if c = #"." ∧ cs ≠ "" ∧ MEM (HD cs) "([{" then
-      SOME (OtherS (TAKE 2 (c::cs)), Locs loc (next_loc 2 loc), TL cs)
     else if isDelim c then
       SOME (OtherS [c], Locs loc loc, cs)
     else if isSym c then
@@ -612,9 +610,6 @@ Definition get_token_def:
     if s = "<-" then LarrowT else
     if s = "." then DotT else
     if s = ".." then DotsT else
-    if s = ".(" then DotParenT else
-    if s = ".[" then DotBrackT else
-    if s = ".{" then DotBraceT else
     if s = ".~" then EscapeT else
     if s = ":" then ColonT else
     if s = "::" then ColonsT else