diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 429e740403..61317f3ef2 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -65,6 +65,18 @@ let test_name_colon = let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None +let test_array_opening = + let open Pcoq.Lookahead in + to_entry "test_array_opening" begin + lk_kw "[" >> lk_kw "|" >> check_no_space + end + +let test_array_closing = + let open Pcoq.Lookahead in + to_entry "test_array_closing" begin + lk_kw "|" >> lk_kw "]" >> check_no_space + end + } GRAMMAR EXTEND Gram @@ -172,9 +184,17 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } + | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance -> + { let t = Array.make (List.length ls) def in + List.iteri (fun i e -> t.(i) <- e) ls; + CAst.make ~loc @@ CArray(u, t, def, ty) + } | "`("; c = operconstr LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; + array_elems: + [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]] + ; record_declaration: [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ] ; |