From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- parsing/g_constr.ml4 | 137 +++++++++++++++++++++++++-------------------------- 1 file changed, 66 insertions(+), 71 deletions(-) (limited to 'parsing/g_constr.ml4') 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: -- cgit v1.2.3