summaryrefslogtreecommitdiff
path: root/parsing/g_constr.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_constr.ml4')
-rw-r--r--parsing/g_constr.ml4137
1 files changed, 66 insertions, 71 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bba3d0d6..76b761b1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id$ *)
+(* $Id: g_constr.ml4 13359 2010-07-30 08:46:55Z herbelin $ *)
open Pp
open Pcoq
@@ -34,11 +34,6 @@ let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
-let loc_of_binder_let = function
- | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
- | LocalRawDef ((loc,_),_)::_ -> loc
- | _ -> dummy_loc
-
let binders_of_lidents l =
List.map (fun (loc, id) ->
LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
@@ -88,8 +83,8 @@ let lpar_id_coloneq =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-let impl_ident =
- Gram.Entry.of_parser "impl_ident"
+let impl_ident_head =
+ Gram.Entry.of_parser "impl_ident_head"
(fun strm ->
match Stream.npeek 1 strm with
| [(_,"{")] ->
@@ -126,13 +121,13 @@ let ident_with =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
-let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
+let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
constr_pattern lconstr_pattern Constr.ident
- binder binder_let binders_let record_declaration
- binders_let_fixannot typeclass_constraint pattern appl_arg;
+ closed_binder open_binders binder binders binders_fixannot
+ record_declaration typeclass_constraint pattern appl_arg;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -204,7 +199,7 @@ GEXTEND Gram
| "("; c = operconstr LEVEL "200"; ")" ->
(match c with
CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
- CNotation(loc,"( _ )",([c],[]))
+ CNotation(loc,"( _ )",([c],[],[]))
| _ -> c)
| "{|"; c = record_declaration; "|}" -> c
| "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -214,14 +209,10 @@ GEXTEND Gram
] ]
;
forall:
- [ [ "forall" -> ()
- | IDENT "Π" -> ()
- ] ]
+ [ [ "forall" -> () ] ]
;
lambda:
- [ [ "fun" -> ()
- | IDENT "λ" -> ()
- ] ]
+ [ [ "fun" -> () ] ]
;
record_declaration:
[ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
@@ -234,13 +225,13 @@ GEXTEND Gram
(id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
;
binder_constr:
- [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+ [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
- | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
+ | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
mkCLambdaN loc bl c
- | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
+ | "let"; id=name; bl = binders; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
- let loc1 = loc_of_binder_let bl in
+ let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in
CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
| "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
let fixp = mk_single_fix fx in
@@ -253,7 +244,7 @@ GEXTEND Gram
po = return_type;
":="; c1 = operconstr LEVEL "200"; "in";
c2 = operconstr LEVEL "200" ->
- CLetTuple (loc,List.map snd lb,po,c1,c2)
+ CLetTuple (loc,lb,po,c1,c2)
| "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
@@ -298,7 +289,7 @@ GEXTEND Gram
| "cofix" -> false ] ]
;
fix_decl:
- [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
+ [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
c=operconstr LEVEL "200" ->
(id,fst bl,snd bl,c,ty) ] ]
;
@@ -310,14 +301,14 @@ GEXTEND Gram
[ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
;
pred_pattern:
- [ [ ona = OPT ["as"; id=name -> snd id];
+ [ [ ona = OPT ["as"; id=name -> id];
ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ]
;
case_type:
[ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
;
return_type:
- [ [ a = OPT [ na = OPT["as"; id=name -> snd id];
+ [ [ a = OPT [ na = OPT["as"; na=name -> na];
ty = case_type -> (na,ty) ] ->
match a with
| None -> None, None
@@ -365,15 +356,7 @@ GEXTEND Gram
| n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
| s = string -> CPatPrim (loc, String s) ] ]
;
- binder_list:
- [ [ idl=LIST1 name; bl=binders_let ->
- LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
- | idl=LIST1 name; ":"; c=lconstr ->
- [LocalRawAssum (idl,Default Explicit,c)]
- | cl = binders_let -> cl
- ] ]
- ;
- binder_assum:
+ impl_ident_tail:
[ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
| idl=LIST1 name; ":"; c=lconstr; "}" ->
(fun id -> LocalRawAssum (id::idl,Default Implicit,c))
@@ -390,47 +373,59 @@ GEXTEND Gram
rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
] ]
;
- binders_let_fixannot:
- [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
- (assum (loc, Name id) :: fst bl), snd bl
- | f = fixannot -> [], f
- | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
- | -> [], (None, CStructRec)
+ binders_fixannot:
+ [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot ->
+ (assum (loc, Name id) :: fst bl), snd bl
+ | f = fixannot -> [], f
+ | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
+ | -> [], (None, CStructRec)
] ]
;
- binders_let:
- [ [ b = binder_let; bl = binders_let -> b @ bl
- | -> [] ] ]
- ;
- binder_let:
- [ [ id=name ->
- [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
- | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
- [LocalRawAssum (id::idl,Default Explicit,c)]
- | "("; id=name; ":"; c=lconstr; ")" ->
- [LocalRawAssum ([id],Default Explicit,c)]
- | "("; id=name; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,c)]
- | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
- | "{"; id=name; "}" ->
- [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
- | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
- [LocalRawAssum (id::idl,Default Implicit,c)]
- | "{"; id=name; ":"; c=lconstr; "}" ->
- [LocalRawAssum ([id],Default Implicit,c)]
- | "{"; id=name; idl=LIST1 name; "}" ->
- List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
- | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
- | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+ open_binders:
+ (* Same as binders but parentheses around a closed binder are optional if
+ the latter is unique *)
+ [ [ (* open binder *)
+ id = name; idl = LIST0 name; ":"; c = lconstr ->
+ [LocalRawAssum (id::idl,Default Explicit,c)]
+ (* binders factorized with open binder *)
+ | id = name; idl = LIST0 name; bl = binders ->
+ let t = CHole (loc, Some (Evd.BinderType (snd id))) in
+ LocalRawAssum (id::idl,Default Explicit,t)::bl
+ | id1 = name; ".."; id2 = name ->
+ [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
+ Default Explicit,CHole (loc,None))]
+ | bl = closed_binder; bl' = binders ->
+ bl@bl'
] ]
;
+ binders:
+ [ [ l = LIST0 binder -> List.flatten l ] ]
+ ;
binder:
- [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
- | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
- | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
+ [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+ | bl = closed_binder -> bl ] ]
+ ;
+ closed_binder:
+ [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum (id::idl,Default Explicit,c)]
+ | "("; id=name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum ([id],Default Explicit,c)]
+ | "("; id=name; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,c)]
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+ | "{"; id=name; "}" ->
+ [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum (id::idl,Default Implicit,c)]
+ | "{"; id=name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum ([id],Default Implicit,c)]
+ | "{"; id=name; idl=LIST1 name; "}" ->
+ List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+ | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+ | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
] ]
;
typeclass_constraint:
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 18:15:10 +0000