|
(************************************************************************)
(* * The Rocq Prover / The Rocq 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 Procq
open Procq.Prim
open Procq.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 Procq.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 Procq.Lookahead in
to_entry "test_lpar_id_coloneq" begin
lk_kw "(" >> lk_nat >> lk_kw ":="
end
let ensure_fixannot =
let open Procq.Lookahead in
to_entry "check_fixannot" begin
lk_kw "{" >> lk_kws ["wf"; "struct"; "measure"]
end
let test_name_colon =
let open Procq.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 Procq.Lookahead in
to_entry "test_array_opening" begin
lk_kw "[" >> lk_kw "|" >> check_no_space
end
let test_array_closing =
let open Procq.Lookahead in
to_entry "test_array_closing" begin
lk_kw "|" >> lk_kw "]" >> check_no_space
end
let test_old_sort_qvar =
let open Procq.Lookahead in
to_entry "test_old_sort_qvar" begin
lk_ident >> lk_list lk_field >> lk_kw "|"
end
let test_sort_qvar =
let open Procq.Lookahead in
to_entry "test_sort_qvar" begin
lk_ident >> lk_list lk_field >> lk_kw ";"
end
let warn_old_sort_syntax =
CWarnings.create ~name:"deprecated-sort-poly-syntax" ~category:Deprecation.Version.v9_1
Pp.(fun () -> fmt "Separating sorts from universes with \"|\" is deprecated.@ Use \";\" instead.")
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)
(* XXX use registered ref? but currently constrexpr doesn't have a node for registered refs
and we can't do [Rocqlib.lib_ref] at parsing time, it's only available in the interp phase. *)
let sigref loc = Libnames.qualid_of_string ~loc "Corelib.Init.Specif.sig"
}
GRAMMAR EXTEND Gram
GLOBAL: binder_constr lconstr constr term
universe_name sort sort_quality_or_set
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_old_sort_qvar; q = reference; pipe_loc = [ "|" -> { loc } ]; u = universe; "}" -> {
warn_old_sort_syntax ~loc:pipe_loc ();
Some (CQVar q), u
}
| "Type"; "@{"; test_sort_qvar; q = reference; ";"; u = universe; "}" -> {
Some (CQVar q), u
}
| "Type"; "@{"; u = universe; "}" -> { None, u } ] ]
;
sort_quality_or_set:
[ [ "Prop" -> { UnivGen.QualityOrSet.prop }
| "SProp" -> { UnivGen.QualityOrSet.sprop }
| "Set" -> { UnivGen.QualityOrSet.Set }
| "Type" -> { UnivGen.QualityOrSet.qtype } ] ]
;
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 = reference; i = univ_annot ->
{ CAst.make ~loc @@ CRef (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 [ is_pipe = [ "|" -> { Some loc } | ";" -> { None } ]; l' = LIST0 univ_level_or_quality -> { is_pipe, l' } ]; "}" ->
{
let l, l' = match l' with
| None -> [], List.map (force_univ_level ~loc) l
| Some (is_pipe, l') ->
let () = Option.iter (fun loc -> warn_old_sort_syntax ~loc ()) is_pipe in
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; ":"; t=lconstr; "|"; c=lconstr; ")" -> {
let lambda = mkLambdaC ([id], default_binder_kind, t, c) in
let typ = CAst.make ~loc @@ CAppExpl ((sigref loc,None), [CAst.make @@ CHole None; lambda]) in
[CLocalAssum ([id], None, default_binder_kind, typ)] }
| "{"; 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
[ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
]
|
