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.ml4121
1 files changed, 60 insertions, 61 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e7d4684b..22dc427b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -1,26 +1,23 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id: g_constr.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Pcoq
open Constr
open Prim
-open Rawterm
+open Glob_term
open Term
open Names
open Libnames
open Topconstr
-
open Util
+open Tok
+open Compat
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
@@ -28,15 +25,20 @@ let constr_kw =
"Prop"; "Set"; "Type"; ".("; "_"; "..";
"`{"; "`("; "{|"; "|}" ]
-let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
+let _ = List.iter Lexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
| (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
+let binders_of_names l =
+ List.map (fun (loc, na) ->
+ LocalRawAssum ([loc, na], Default Explicit,
+ CHole (loc, Some (Evd.BinderType na)))) l
+
let binders_of_lidents l =
List.map (fun (loc, id) ->
- LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
+ LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
CHole (loc, Some (Evd.BinderType (Name id))))) l
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -66,60 +68,55 @@ let mk_fix(loc,kw,id,dcls) =
let mk_single_fix (loc,kw,dcl) =
let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+let err () = raise Stream.Failure
+
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let lpar_id_coloneq =
Gram.Entry.of_parser "test_lpar_id_coloneq"
(fun strm ->
- match Stream.npeek 1 strm with
- | [("","(")] ->
- (match Stream.npeek 2 strm with
- | [_; ("IDENT",s)] ->
- (match Stream.npeek 3 strm with
- | [_; _; ("", ":=")] ->
- Stream.junk strm; Stream.junk strm; Stream.junk strm;
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "(" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT s ->
+ (match get_tok (stream_nth 2 strm) with
+ | KEYWORD ":=" ->
+ stream_njunk 3 strm;
Names.id_of_string s
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
let impl_ident_head =
Gram.Entry.of_parser "impl_ident_head"
(fun strm ->
- match Stream.npeek 1 strm with
- | [(_,"{")] ->
- (match Stream.npeek 2 strm with
- | [_;("IDENT",("wf"|"struct"|"measure"))] ->
- raise Stream.Failure
- | [_;("IDENT",s)] ->
- Stream.junk strm; Stream.junk strm;
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "{" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT ("wf"|"struct"|"measure") -> err ()
+ | IDENT s ->
+ stream_njunk 2 strm;
Names.id_of_string s
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ | _ -> err ())
+ | _ -> err ())
-let ident_colon =
- Gram.Entry.of_parser "ident_colon"
+let name_colon =
+ Gram.Entry.of_parser "name_colon"
(fun strm ->
- match Stream.npeek 1 strm with
- | [("IDENT",s)] ->
- (match Stream.npeek 2 strm with
- | [_; ("", ":")] ->
- Stream.junk strm; Stream.junk strm;
- Names.id_of_string s
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
-
-let ident_with =
- Gram.Entry.of_parser "ident_with"
- (fun strm ->
- match Stream.npeek 1 strm with
- | [("IDENT",s)] ->
- (match Stream.npeek 2 strm with
- | [_; ("", "with")] ->
- Stream.junk strm; Stream.junk strm;
- Names.id_of_string s
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ match get_tok (stream_nth 0 strm) with
+ | IDENT s ->
+ (match get_tok (stream_nth 1 strm) with
+ | KEYWORD ":" ->
+ stream_njunk 2 strm;
+ Name (Names.id_of_string s)
+ | _ -> err ())
+ | KEYWORD "_" ->
+ (match get_tok (stream_nth 1 strm) with
+ | KEYWORD ":" ->
+ stream_njunk 2 strm;
+ Anonymous
+ | _ -> err ())
+ | _ -> err ())
let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
@@ -147,9 +144,9 @@ GEXTEND Gram
[ [ c = lconstr -> c ] ]
;
sort:
- [ [ "Set" -> RProp Pos
- | "Prop" -> RProp Null
- | "Type" -> RType None ] ]
+ [ [ "Set" -> GProp Pos
+ | "Prop" -> GProp Null
+ | "Type" -> GType None ] ]
;
lconstr:
[ [ c = operconstr LEVEL "200" -> c ] ]
@@ -215,7 +212,7 @@ GEXTEND Gram
[ [ "fun" -> () ] ]
;
record_declaration:
- [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+ [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
(* CRecord (loc, Some c, fs) *)
] ]
@@ -227,7 +224,7 @@ GEXTEND Gram
binder_constr:
[ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
- | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
+ | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
mkCLambdaN loc bl c
| "let"; id=name; bl = binders; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
@@ -334,14 +331,17 @@ GEXTEND Gram
[ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ]
| "99" RIGHTA [ ]
| "10" LEFTA
+ [ p = pattern; "as"; id = ident ->
+ CPatAlias (loc, p, id) ]
+ | "9" RIGHTA
[ p = pattern; lp = LIST1 NEXT ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
| _ -> Util.user_err_loc
(cases_pattern_expr_loc p, "compound_pattern",
Pp.str "Constructor expected."))
- | p = pattern; "as"; id = ident ->
- CPatAlias (loc, p, id) ]
+ |"@"; r = Prim.reference; lp = LIST1 NEXT ->
+ CPatCstrExpl (loc, r, lp) ]
| "1" LEFTA
[ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
| "0"
@@ -389,8 +389,7 @@ GEXTEND Gram
[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
+ binders_of_names (id::idl) @ bl
| id1 = name; ".."; id2 = name ->
[LocalRawAssum ([id1;(loc,Name ldots_var);id2],
Default Explicit,CHole (loc,None))]
@@ -432,8 +431,8 @@ GEXTEND Gram
[ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
| "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
id, expl, c
- | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
- (loc, Name iid), expl, c
+ | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
+ (loc, iid), expl, c
| c = operconstr LEVEL "200" ->
(loc, Anonymous), false, c
] ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 17:28:52 +0000