diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /parsing/g_constr.ml4 | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'parsing/g_constr.ml4')
-rw-r--r-- | parsing/g_constr.ml4 | 121 |
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 ] ] |