(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

DECLARE GLOBAL PLUGIN

{

open Names
open Constr
open Libnames
open Glob_term
open Constrexpr
open Constrexpr_ops
open Util

open Pcoq
open Pcoq.Prim
open Pcoq.Constr

(* TODO: avoid this redefinition without an extra dep to Notation_ops *)
let ldots_var = Id.of_string ".."

let binder_of_name expl { CAst.loc = loc; v = na } =
  CLocalAssum ([CAst.make ?loc na], None, Default expl,
    CAst.make ?loc @@ CHole (Some (GBinderType na)))

let binders_of_names l =
  List.map (binder_of_name Explicit) l

let pat_of_name CAst.{loc;v} = match v with
| Anonymous -> CAst.make ?loc @@ CPatAtom None
| Name id -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident id))

(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_coloneq" begin
    lk_kw "(" >> lk_ident >> lk_kw ":="
  end

(* Hack to parse "(n:=t)" as an explicit argument without conflicts with the *)
(* syntax "(n t)" *)
let test_lpar_nat_coloneq =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_coloneq" begin
    lk_kw "(" >> lk_nat >> lk_kw ":="
  end

let ensure_fixannot =
  let open Pcoq.Lookahead in
  to_entry "check_fixannot" begin
    lk_kw "{" >> lk_kws ["wf"; "struct"; "measure"]
  end

let test_name_colon =
  let open Pcoq.Lookahead in
  to_entry "test_name_colon" begin
    lk_name >> lk_kw ":"
  end

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

let test_sort_qvar =
  let open Pcoq.Lookahead in
  to_entry "test_sort_qvar" begin
    lk_ident >> lk_list lk_field >> lk_kw "|"
  end

type univ_level_or_quality =
  | SProp | Prop | Set | Type | Anon of Loc.t | Global of Libnames.qualid

let force_univ_level ?loc = function
  | SProp -> UNamed CSProp
  | Prop -> UNamed CProp
  | Set -> UNamed CSet
  | Type -> UAnonymous {rigid=UnivRigid}
  | Anon _ -> UAnonymous {rigid=UnivFlexible false}
  | Global qid -> UNamed (CType qid)

let force_quality ?loc = function
  | SProp -> CQConstant QSProp
  | Prop -> CQConstant QProp
  | Set -> CErrors.user_err ?loc Pp.(str "Universe levels cannot be Set.")
  | Type -> CQConstant QType
  | Anon loc -> CQualVar (CQAnon (Some loc))
  | Global qid -> CQualVar (CQVar qid)

}

GRAMMAR EXTEND Gram
  GLOBAL: binder_constr lconstr constr term
  universe_name sort sort_family
  global constr_pattern cpattern Constr.ident
  closed_binder open_binders binder binders binders_fixannot
  record_declaration typeclass_constraint pattern arg type_cstr
  one_closed_binder one_open_binder;
  Constr.ident:
    [ [ id = Prim.ident -> { id } ] ]
  ;
  Prim.name: TOP
    [ [ "_" -> { CAst.make ~loc Anonymous } ] ]
  ;
  global:
    [ [ r = Prim.reference -> { r } ] ]
  ;
  constr_pattern:
    [ [ c = constr -> { c } ] ]
  ;
  cpattern:
    [ [ c = lconstr -> { c } ] ]
  ;
  sort:
    [ [ "Set"  -> { None, UNamed [CSet, 0] }
      | "Prop" -> { None, UNamed [CProp, 0] }
      | "SProp" -> { None, UNamed [CSProp, 0] }
      | "Type" -> { None, UAnonymous {rigid=UnivRigid} }
      | "Type"; "@{"; "_"; "}" -> { None, UAnonymous {rigid=UnivFlexible false} }
      | "Type"; "@{"; test_sort_qvar; q = reference; "|"; u = universe; "}" ->
        { Some (CQVar q), u }
      | "Type"; "@{"; u = universe; "}" -> { None, u } ] ]
  ;
  sort_family:
    [ [ "Set"  -> { Sorts.InSet }
      | "Prop" -> { Sorts.InProp }
      | "SProp" -> { Sorts.InSProp }
      | "Type" -> { Sorts.InType } ] ]
  ;
  universe_increment:
    [ [ "+"; n = natural -> { n }
      | -> { 0 } ] ]
  ;
  universe_name:
    [ [ id = global -> { CType id }
      | "Set"  -> { CSet }
      | "Prop" -> { CProp } ] ]
  ;
  universe_expr:
    [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
  ;
  universe:
    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
      | "_" -> { UAnonymous { rigid = UnivFlexible false } }
      | u = universe_expr -> { UNamed [u] } ] ]
  ;
  lconstr:
    [ [ c = term LEVEL "200" -> { c } ] ]
  ;
  constr:
    [ [ c = term LEVEL "8" -> { c }
      | "@"; f=global; i = univ_annot -> { CAst.make ~loc @@ CAppExpl((f,i),[]) } ] ]
  ;
  term:
    [ "200" RIGHTA [ ]
    | "100" RIGHTA
      [ c1 = term; "<:"; c2 = term LEVEL "200" ->
                 { CAst.make ~loc @@ CCast(c1, Some VMcast, c2) }
      | c1 = term; "<<:"; c2 = term LEVEL "200" ->
                 { CAst.make ~loc @@ CCast(c1, Some NATIVEcast, c2) }
      | c1 = term; ":>"; c2 = term LEVEL "200" ->
                 { CAst.make ~loc @@ CCast(c1, None, c2) }
      | c1 = term; ":"; c2 = term LEVEL "200" ->
                 { CAst.make ~loc @@ CCast(c1, Some DEFAULTcast, c2) } ]
    | "99" RIGHTA [ ]
    | "90" RIGHTA [ ]
    | "10" LEFTA
      [ f = term; args = LIST1 arg -> { CAst.make ~loc @@ CApp(f,args) }
      | "@"; f = global; i = univ_annot; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((f,i),args) }
      | "@"; lid = pattern_ident; args = LIST1 identref ->
        { let { CAst.loc = locid; v = id } = lid in
          let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
          CAst.make ~loc @@ CApp(CAst.make ?loc:locid @@ CPatVar id,args) }
      | c = binder_constr -> { c } ]
    | "9"
      [ ".."; c = term LEVEL "0"; ".." ->
        { CAst.make ~loc @@ CAppExpl ((qualid_of_ident ~loc ldots_var, None),[c]) } ]
    | "8" [ ]
    | "1" LEFTA
      [ c = term; ".("; f = global; i = univ_annot; args = LIST0 arg; ")" ->
        { CAst.make ~loc @@ CProj(false, (f,i), args, c) }
      | c = term; ".("; "@"; f = global; i = univ_annot;
        args = LIST0 (term LEVEL "9"); ")" ->
        { CAst.make ~loc @@ CProj(true, (f,i), List.map (fun a -> (a,None)) args, c) }
      | c = term; "%"; key = IDENT ->
        { CAst.make ~loc @@ CDelimiters (DelimUnboundedScope,key,c) }
      | c = term; "%_"; key = IDENT ->
        { CAst.make ~loc @@ CDelimiters (DelimOnlyTmpScope,key,c) } ]
    | "0"
      [ c = atomic_constr -> { c }
      | c = term_match -> { c }
      | id = ident; f = Prim.fields; i = univ_annot ->
        { let (l,id') = f in CAst.make ~loc @@ CRef (make_qualid ~loc (DirPath.make (l@[id])) id', i) }
      | id = ident; i = univ_annot ->
        { CAst.make ~loc @@ CRef (qualid_of_ident ~loc id, i) }
      | n = NUMBER-> { CAst.make ~loc @@ CPrim (Number (NumTok.SPlus,n)) }
      | s = string -> { CAst.make ~loc @@ CPrim (String s) }
      | "("; c = term LEVEL "200"; ")" ->
        { (* Preserve parentheses around numbers so that constrintern does not
             collapse -(3) into the number -3. *)
          (match c.CAst.v with
            | CPrim (Number (NumTok.SPlus,n)) ->
                CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[]))
            | _ -> c) }
      | "{|"; c = record_declaration; bar_cbrace -> { c }
      | "`{"; c = term LEVEL "200"; "}" ->
        { CAst.make ~loc @@ CGeneralization (MaxImplicit, c) }
      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_annot ->
        { 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 = term LEVEL "200"; ")" ->
        { CAst.make ~loc @@ CGeneralization (Explicit, c) } ] ]
  ;
  array_elems:
    [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]]
  ;
  record_declaration:
    [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ]
  ;
  fields_def:
    [ [ f = field_def; ";"; fs = fields_def -> { f :: fs }
      | f = field_def -> { [f] }
      | -> { [] } ] ]
  ;
  field_def:
    [ [ id = global; bl = binders; ":="; c = lconstr ->
        { (id, mkLambdaCN ~loc bl c) } ] ]
  ;
  binder_constr:
    [ [ "forall"; bl = open_binders; ","; c = term LEVEL "200" ->
        { mkProdCN ~loc bl c }
      | "fun"; bl = open_binders; "=>"; c = term LEVEL "200" ->
        { mkLambdaCN ~loc bl c }
      | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
        c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
        { let ty,c1 = match ty, c1 with
          | (_,None), { CAst.v = CCast(c, Some DEFAULTcast, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
          | _, _ -> ty, c1 in
          CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                 Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
      | "let"; "fix"; fx = fix_decl; "in"; c = term LEVEL "200" ->
        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_,_ as dcl)} = fx in
          let fix = CAst.make ?loc:locf @@ CFix (lid,[dcl]) in
          CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fix,None,c) }
      | "let"; "cofix"; fx = cofix_body; "in"; c = term LEVEL "200" ->
        { let {CAst.loc=locf;CAst.v=({CAst.loc=li;CAst.v=id} as lid,_,_,_,_ as dcl)} = fx in
          let cofix = CAst.make ?loc:locf @@ CCoFix (lid,[dcl]) in
          CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,cofix,None,c) }
      | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
        po = as_return_type; ":="; c1 = term LEVEL "200"; "in";
        c2 = term LEVEL "200" ->
        { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
        "in"; c2 = term LEVEL "200" ->
        { CAst.make ~loc @@
          CCases (LetPatternStyle, None,    [c1, None, None],       [CAst.make ~loc ([[p]], c2)]) }
      | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = term LEVEL "200";
        rt = case_type; "in"; c2 = term LEVEL "200" ->
        { CAst.make ~loc @@
          CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
      | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200";
        ":="; c1 = term LEVEL "200"; rt = case_type;
        "in"; c2 = term LEVEL "200" ->
        { CAst.make ~loc @@
          CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
      | "if"; c = term LEVEL "200"; po = as_return_type;
        "then"; b1 = term LEVEL "200";
        "else"; b2 = term LEVEL "200" ->
        { CAst.make ~loc @@ CIf (c, po, b1, b2) }
      | "fix"; c = fix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CFix (id,dcls) }
      | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
  ;
  arg:
    [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) }
      | test_lpar_nat_coloneq; "("; n = natural; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByPos n)) }
      | c=term LEVEL "9" -> { (c,None) } ] ]
  ;
  atomic_constr:
    [ [ s = sort   -> { CAst.make ~loc @@ CSort s }
      | "_"      -> { CAst.make ~loc @@ CHole (None) }
      | "?"; "["; id = identref; "]"  -> { CAst.make ~loc @@  CHole (Some (GNamedHole (false, id.CAst.v))) }
      | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (Some (GNamedHole (true, id.CAst.v))) }
      | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
  ;
  inst:
    [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ]
  ;
  evar_instance:
    [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
      | -> { [] } ] ]
  ;
  univ_annot:
    [ [ "@{"; l = LIST0 univ_level_or_quality; l' = OPT [ "|"; l' = LIST0 univ_level_or_quality -> { l' } ]; "}" ->
        {
          let l, l' = match l' with
            | None -> [], List.map (force_univ_level ~loc) l
            | Some l' -> List.map (force_quality ~loc) l, List.map (force_univ_level ~loc) l'
          in
          Some (l,l')
        }
      | -> { None } ] ]
  ;
  univ_level_or_quality:
    [ [ "Set" -> { Set }
      | "SProp" -> { SProp }
      | "Prop" -> { Prop }
      | "Type" -> { Type }
      | "_" -> { Anon loc }
      | id = global -> { Global id } ] ]
  ;
  fix_decls:
    [ [ dcl = fix_decl -> { let (id,_,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
      | dcl = fix_decl; "with"; dcls = LIST1 fix_decl SEP "with"; "for"; id = identref ->
        { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
  ;
  cofix_decls:
    [ [ dcl = cofix_body -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
      | dcl = cofix_body; "with"; dcls = LIST1 cofix_body SEP "with"; "for"; id = identref ->
        { (id,List.map (fun x -> x.CAst.v) (dcl::dcls)) } ] ]
  ;
  fix_decl:
    [ [ id = identref; bl = binders_fixannot; ty = type_cstr; ":=";
        c = term LEVEL "200" ->
        { CAst.make ~loc (id,None,snd bl,fst bl,ty,c) } ] ]
  ;
  cofix_body:
    [ [ id = identref; bl = binders; ty = type_cstr; ":=";
        c = term LEVEL "200" ->
        { CAst.make ~loc (id,None,bl,ty,c) } ] ]
  ;
  term_match:
    [ [ "match"; ci = LIST1 case_item SEP ","; ty = OPT case_type; "with";
        br = branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
  ;
  case_item:
    [ [ c = term LEVEL "100";
        ona = OPT ["as"; id = name -> { id } ];
        ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] ->
        { (c,ona,ty) } ] ]
  ;
  case_type:
    [ [ "return"; ty = term LEVEL "100" -> { ty } ] ]
  ;
  as_return_type:
    [ [ a = OPT [ na = OPT ["as"; na = name -> { na } ];
                  ty = case_type -> { (na,ty) } ] ->
        { match a with
          | None -> None, None
          | Some (na,t) -> (na, Some t) } ] ]
  ;
  branches:
    [ [ OPT"|"; br = LIST0 eqn SEP "|" -> { br } ] ]
  ;
  mult_pattern:
    [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ]
  ;
  eqn:
    [ [ pll = LIST1 mult_pattern SEP "|";
        "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ]
  ;
  record_pattern:
    [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ]
  ;
  record_patterns:
    [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
      | p = record_pattern-> { [p] }
      | -> { [] } ] ]
  ;
  pattern:
    [ "200" RIGHTA [ ]
    | "100" RIGHTA
      [ p = pattern; ":"; ty = term LEVEL "200" ->
        { CAst.make ~loc @@ CPatCast (p, ty) } ]
    | "99" RIGHTA [ ]
    | "90" RIGHTA [ ]
    | "10" LEFTA
      [ p = pattern; "as"; na = name ->
        { CAst.make ~loc @@ CPatAlias (p, na) }
      | p = pattern; lp = LIST1 NEXT -> { mkAppPattern ~loc p lp }
      | "@"; r = Prim.reference; lp = LIST0 NEXT ->
        { CAst.make ~loc @@ CPatCstr (r, Some lp, []) } ]
    | "1" LEFTA
      [ c = pattern; "%"; key = IDENT ->
        { CAst.make ~loc @@ CPatDelimiters (DelimUnboundedScope,key,c) }
      | c = pattern; "%_"; key = IDENT ->
        { CAst.make ~loc @@ CPatDelimiters (DelimOnlyTmpScope,key,c) } ]
    | "0"
      [ r = Prim.reference                -> { CAst.make ~loc @@ CPatAtom (Some r) }
      | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat }
      | "_" -> { CAst.make ~loc @@ CPatAtom None }
      | "("; p = pattern LEVEL "200"; ")" ->
        { (* Preserve parentheses around numbers so that constrintern does not
             collapse -(3) into the number -3. *)
          match p.CAst.v with
          | CPatPrim (Number (NumTok.SPlus,n)) ->
              CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[],[]),[])
          | _ -> p }
      | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
        { CAst.make ~loc @@ CPatOr (p::pl) }
      | n = NUMBER-> { CAst.make ~loc @@ CPatPrim (Number (NumTok.SPlus,n)) }
      | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
  ;
  fixannot:
    [ [ "{"; IDENT "struct"; id = identref; "}" -> { CAst.make ~loc @@ CStructRec id }
      | "{"; IDENT "wf"; rel = constr; id = identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) }
      | "{"; IDENT "measure"; m = constr; id = OPT identref; rel = OPT constr; "}" ->
        { CAst.make ~loc @@ CMeasureRec (id,m,rel) } ] ]
  ;
  binders_fixannot:
    [ [ ensure_fixannot; f = fixannot -> { [], Some f }
      | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
      | -> { [], None } ] ]
  ;
  open_binders:
    (* Same as binders but parentheses around a closed binder are optional if
       the latter is unique *)
    [ [ id = name; idl = LIST0 name; ":"; c = lconstr ->
        { [CLocalAssum (id::idl,None,Default Explicit,c)] }
        (* binders factorized with open binder *)
      | id = name; idl = LIST0 name; bl = binders ->
        { binders_of_names (id::idl) @ bl }
      | id1 = name; ".."; id2 = name ->
        { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2],
                        None, Default Explicit, CAst.make ~loc @@ CHole (None))] }
      | bl = closed_binder; bl' = binders ->
        { bl@bl' } ] ]
  ;
  binders:
    [ [ l = LIST0 binder -> { List.flatten l } ] ]
  ;
  binder:
    [ [ id = name -> { [CLocalAssum ([id], None, Default Explicit, CAst.make ~loc @@ CHole (None))] }
      | bl = closed_binder -> { bl } ] ]
  ;
  closed_binder:
    [ [ "("; id = name; idl = LIST1 name; ":"; c = lconstr; ")" ->
        { [CLocalAssum (id::idl,None,Default Explicit,c)] }
      | "("; id = name; ":"; c = lconstr; ")" ->
        { [CLocalAssum ([id],None,Default Explicit,c)] }
      | "("; id = name; ":="; c = lconstr; ")" ->
        { match c.CAst.v with
          | CCast(c, Some DEFAULTcast, t) -> [CLocalDef (id,None,c,Some t)]
          | _ -> [CLocalDef (id,None,c,None)] }
      | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
        { [CLocalDef (id,None,c,Some t)] }
      | "{"; id = name; "}" ->
        { [CLocalAssum ([id], None, Default MaxImplicit, CAst.make ~loc @@ CHole (None))] }
      | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" ->
        { [CLocalAssum (id::idl,None,Default MaxImplicit,c)] }
      | "{"; id = name; ":"; c = lconstr; "}" ->
        { [CLocalAssum ([id],None,Default MaxImplicit,c)] }
      | "{"; id = name; idl = LIST1 name; "}" ->
        { List.map (fun id -> CLocalAssum ([id], None, Default MaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
      | "["; id = name; "]" ->
        { [CLocalAssum ([id], None, Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))] }
      | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" ->
        { [CLocalAssum (id::idl,None,Default NonMaxImplicit,c)] }
      | "["; id = name; ":"; c = lconstr; "]" ->
        { [CLocalAssum ([id],None, Default NonMaxImplicit,c)] }
      | "["; id = name; idl = LIST1 name; "]" ->
        { List.map (fun id -> CLocalAssum ([id], None, Default NonMaxImplicit, CAst.make ~loc @@ CHole (None))) (id::idl) }
      | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (Explicit, b), t)) tc }
      | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (MaxImplicit, b), t)) tc }
      | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
        { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (NonMaxImplicit, b), t)) tc }
      | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
  ;
  one_open_binder:
    [ [ na = name -> { (pat_of_name na, Explicit) }
      | na = name; ":"; t = lconstr -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
      | b = one_closed_binder -> { b } ] ]
  ;
  one_closed_binder:
    [ [ "("; na = name; ":"; t = lconstr; ")" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
      | "{"; na = name; "}" -> { (pat_of_name na, MaxImplicit) }
      | "{"; na = name; ":"; t = lconstr; "}" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), MaxImplicit) }
      | "["; na = name; "]" -> { (pat_of_name na, NonMaxImplicit) }
      | "["; na = name; ":"; t = lconstr; "]" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), NonMaxImplicit) }
      | "'"; p = pattern LEVEL "0" -> { (p, Explicit) } ] ]
  ;
  typeclass_constraint:
    [ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
      | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
          { id, expl, c }
      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = term LEVEL "200" ->
          { iid, expl, c }
      | c = term LEVEL "200" ->
          { (CAst.make ~loc Anonymous), false, c } ] ]
  ;
  type_cstr:
    [ [ ":"; c = lconstr -> { c }
      | -> { CAst.make ~loc @@ CHole (None) } ] ]
  ;
  let_type_cstr:
    [ [ c = OPT [":"; c = lconstr -> { c } ] -> { Loc.tag ~loc c } ] ]
  ;
  END