summaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml444
-rw-r--r--parsing/g_proofs.ml412
-rw-r--r--parsing/g_tactic.ml466
-rw-r--r--parsing/g_vernac.ml4115
-rw-r--r--parsing/g_xml.ml4290
-rw-r--r--parsing/lexer.ml42
-rw-r--r--parsing/pcoq.ml410
7 files changed, 154 insertions, 385 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3bb029a8..e2e6795f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,12 +153,12 @@ GEXTEND Gram
[ [ "Set" -> GSet
| "Prop" -> GProp
| "Type" -> GType []
- | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+ | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
] ]
;
universe:
- [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
- | id = ident -> [id]
+ [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
+ | id = identref -> [id]
] ]
;
lconstr:
@@ -223,26 +223,29 @@ GEXTEND Gram
CHole (!@loc, None, IntroAnonymous, Some arg)
] ]
;
- forall:
- [ [ "forall" -> () ] ]
- ;
- lambda:
- [ [ "fun" -> () ] ]
- ;
record_declaration:
- [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
+ [ [ fs = record_fields -> CRecord (!@loc, None, fs)
(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
(* CRecord (!@loc, Some c, fs) *)
] ]
;
+
+ record_fields:
+ [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
+ | f = record_field_declaration; ";" -> [f]
+ | f = record_field_declaration -> [f]
+ | -> []
+ ] ]
+ ;
+
record_field_declaration:
[ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
(id, abstract_constr_expr c (binders_of_lidents params)) ] ]
;
binder_constr:
- [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+ [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
mkCProdN (!@loc) bl c
- | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+ | "fun"; 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" ->
@@ -308,7 +311,7 @@ GEXTEND Gram
[ [ "Set" -> GSet
| "Prop" -> GProp
| "Type" -> GType None
- | id = ident -> GType (Some (Id.to_string id))
+ | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
] ]
;
fix_constr:
@@ -362,18 +365,25 @@ GEXTEND Gram
[ [ pll = LIST1 mult_pattern SEP "|";
"=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
;
- recordpattern:
+ record_pattern:
[ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
;
+ record_patterns:
+ [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
+ | p = record_pattern; ";" -> [p]
+ | p = record_pattern-> [p]
+ | -> []
+ ] ]
+ ;
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
[ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
| "99" RIGHTA [ ]
- | "10" LEFTA
+ | "11" LEFTA
[ p = pattern; "as"; id = ident ->
CPatAlias (!@loc, p, id) ]
- | "9" RIGHTA
+ | "10" RIGHTA
[ p = pattern; lp = LIST1 NEXT ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
@@ -388,7 +398,7 @@ GEXTEND Gram
[ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
| "0"
[ r = Prim.reference -> CPatAtom (!@loc,Some r)
- | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+ | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
| "_" -> CPatAtom (!@loc,None)
| "("; p = pattern LEVEL "200"; ")" ->
(match p with
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1e254c16..017f0ea5 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -37,12 +37,12 @@ GEXTEND Gram
command:
[ [ IDENT "Goal"; c = lconstr -> VernacGoal c
| IDENT "Proof" ->
- VernacProof (None,hint_proof_using G_vernac.section_subset_descr None)
+ VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; "with"; ta = tactic;
- l = OPT [ "using"; l = G_vernac.section_subset_descr -> l ] ->
- VernacProof (Some ta,hint_proof_using G_vernac.section_subset_descr l)
- | IDENT "Proof"; "using"; l = G_vernac.section_subset_descr;
+ l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+ VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l)
+ | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
ta = OPT [ "with"; ta = tactic -> ta ] ->
VernacProof (ta,Some l)
| IDENT "Proof"; c = lconstr -> VernacExactProof c
@@ -73,8 +73,10 @@ GEXTEND Gram
| IDENT "Unfocused" -> VernacUnfocused
| IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
| IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
+ | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
+ | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
| IDENT "Show"; IDENT "Goal"; n = string ->
- VernacShow (ShowGoal (GoalId n))
+ VernacShow (ShowGoal (GoalUid n))
| IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
VernacShow (ShowGoalImplicitly n)
| IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 69593f99..c94ac846 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -339,21 +339,6 @@ GEXTEND Gram
| d = delta_flag -> all_with d
] ]
;
- red_tactic:
- [ [ IDENT "red" -> Red false
- | IDENT "hnf" -> Hnf
- | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
- | IDENT "cbv"; s = strategy_flag -> Cbv s
- | IDENT "cbn"; s = strategy_flag -> Cbn s
- | IDENT "lazy"; s = strategy_flag -> Lazy s
- | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
- | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
- | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
- | IDENT "fold"; cl = LIST1 constr -> Fold cl
- | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
- ;
- (* This is [red_tactic] including possible extensions *)
red_expr:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
@@ -452,16 +437,6 @@ GEXTEND Gram
[ [ "using"; l = LIST1 constr SEP "," -> l
| -> [] ] ]
;
- trivial:
- [ [ IDENT "trivial" -> Off
- | IDENT "info_trivial" -> Info
- | IDENT "debug"; IDENT "trivial" -> Debug ] ]
- ;
- auto:
- [ [ IDENT "auto" -> Off
- | IDENT "info_auto" -> Info
- | IDENT "debug"; IDENT "auto" -> Debug ] ]
- ;
eliminator:
[ [ "using"; el = constr_with_bindings -> el ] ]
;
@@ -627,9 +602,18 @@ GEXTEND Gram
TacAtom (!@loc, TacInductionDestruct(false,true,icl))
(* Automation tactic *)
- | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
- | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacAuto (d,n,lems,db))
+ | IDENT "trivial"; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacTrivial (Off, lems, db))
+ | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacTrivial (Info, lems, db))
+ | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacTrivial (Debug, lems, db))
+ | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacAuto (Off, n, lems, db))
+ | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacAuto (Info, n, lems, db))
+ | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+ TacAtom (!@loc, TacAuto (Debug, n, lems, db))
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
@@ -677,7 +661,31 @@ GEXTEND Gram
TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
(* Conversion *)
- | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
+ | IDENT "red"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Red false, cl))
+ | IDENT "hnf"; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Hnf, cl))
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+ | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv s, cl))
+ | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbn s, cl))
+ | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Lazy s, cl))
+ | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+ | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvVm po, cl))
+ | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (CbvNative po, cl))
+ | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Unfold ul, cl))
+ | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Fold l, cl))
+ | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+ TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
(* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
| IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
let p,cl = merge_occurrences (!@loc) cl oc in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cf7f6af2..1f9f57f6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field"
let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_descr = Gram.entry_create "vernac:section_subset_descr"
+let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
let command_entry = ref noedit_mode
let set_command_entry e = command_entry := e
@@ -71,6 +71,17 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+ Gram.Entry.of_parser "test_bracket_ident"
+ (fun strm ->
+ match get_tok (stream_nth 0 strm) with
+ | KEYWORD "[" ->
+ (match get_tok (stream_nth 1 strm) with
+ | IDENT _ -> ()
+ | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
+
let default_command_entry =
Gram.Entry.of_parser "command_entry"
(fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -79,6 +90,7 @@ GEXTEND Gram
GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
vernac: FIRST
[ [ IDENT "Time"; l = vernac_list -> VernacTime l
+ | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l)
| IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac -> VernacFail v
@@ -95,12 +107,12 @@ GEXTEND Gram
| IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
| IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
- | v = vernac_poly -> v ]
+ | v = vernac_poly -> v ]
]
;
- vernac_poly:
+ vernac_poly:
[ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v)
- | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
+ | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
| v = vernac_aux -> v ]
]
;
@@ -128,7 +140,7 @@ GEXTEND Gram
selector:
[ [ n=natural; ":" -> SelectNth n
- | "["; id = ident; "]"; ":" -> SelectId id
+ | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
| IDENT "all" ; ":" -> SelectAll
| IDENT "par" ; ":" -> SelectAllParallel ] ]
;
@@ -145,7 +157,7 @@ GEXTEND Gram
] ]
;
- subgoal_command:
+ subgoal_command:
[ [ c = query_command; "." ->
begin function
| Some (SelectNth g) -> c (Some g)
@@ -184,9 +196,9 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
+ [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
l = LIST0
- [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
+ [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
(Some id,(bl,c,None)) ] ->
VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
| stre = assumption_token; nl = inline; bl = assum_list ->
@@ -194,10 +206,10 @@ GEXTEND Gram
| stre = assumptions_token; nl = inline; bl = assum_list ->
test_plurial_form bl;
VernacAssumption (stre, nl, bl)
- | d = def_token; id = identref; b = def_body ->
+ | d = def_token; id = pidentref; b = def_body ->
VernacDefinition (d, id, b)
| IDENT "Let"; id = identref; b = def_body ->
- VernacDefinition ((Some Discharge, Definition), id, b)
+ VernacDefinition ((Some Discharge, Definition), (id, None), b)
(* Gallina inductive declarations *)
| priv = private_token; f = finite_token;
indl = LIST1 inductive_definition SEP "with" ->
@@ -248,13 +260,17 @@ GEXTEND Gram
[ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
| IDENT "Variables" -> (Some Discharge, Definitional)
| IDENT "Axioms" -> (None, Logical)
- | IDENT "Parameters" -> (None, Definitional) ] ]
+ | IDENT "Parameters" -> (None, Definitional)
+ | IDENT "Conjectures" -> (None, Conjectural) ] ]
;
inline:
[ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
| IDENT "Inline" -> DefaultInline
| -> NoInline] ]
;
+ pidentref:
+ [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ]
+ ;
univ_constraint:
[ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ];
r = identref -> (l, ord, r) ] ]
@@ -299,7 +315,7 @@ GEXTEND Gram
| -> RecordDecl (None, []) ] ]
;
inductive_definition:
- [ [ oc = opt_coercion; id = identref; indpar = binders;
+ [ [ oc = opt_coercion; id = pidentref; indpar = binders;
c = OPT [ ":"; c = lconstr -> c ];
lc=opt_constructors_or_fields; ntn = decl_notation ->
(((oc,id),indpar,c,lc),ntn) ] ]
@@ -309,9 +325,9 @@ GEXTEND Gram
| id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
Constructors ((c id)::l)
| id = identref ; c = constructor_type -> Constructors [ c id ]
- | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+ | cstr = identref; "{"; fs = record_fields; "}" ->
RecordDecl (Some cstr,fs)
- | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+ | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
| -> Constructors [] ] ]
;
(*
@@ -325,14 +341,14 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = identref;
+ [ [ id = pidentref;
bl = binders_fixannot;
ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = identref; bl = binders; ty = type_cstr;
+ [ [ id = pidentref; bl = binders; ty = type_cstr;
def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -373,6 +389,13 @@ GEXTEND Gram
[ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
ntn = decl_notation -> (bd,pri),ntn ] ]
;
+ record_fields:
+ [ [ f = record_field; ";"; fs = record_fields -> f :: fs
+ | f = record_field; ";" -> [f]
+ | f = record_field -> [f]
+ | -> []
+ ] ]
+ ;
record_binder_body:
[ [ l = binders; oc = of_type_with_opt_coercion;
t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
@@ -397,7 +420,7 @@ GEXTEND Gram
[ [ "("; a = simple_assum_coe; ")" -> a ] ]
;
simple_assum_coe:
- [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
+ [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr ->
(not (Option.is_empty oc),(idl,c)) ] ]
;
@@ -424,20 +447,24 @@ GEXTEND Gram
;
END
-let only_identrefs =
- Gram.Entry.of_parser "test_only_identrefs"
+let only_starredidentrefs =
+ Gram.Entry.of_parser "test_only_starredidentrefs"
(fun strm ->
let rec aux n =
match get_tok (Util.stream_nth n strm) with
| KEYWORD "." -> ()
| KEYWORD ")" -> ()
- | IDENT _ -> aux (n+1)
+ | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
| _ -> raise Stream.Failure in
aux 0)
+let starredidentreflist_to_expr l =
+ match l with
+ | [] -> SsEmpty
+ | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
(* Modules and Sections *)
GEXTEND Gram
- GLOBAL: gallina_ext module_expr module_type section_subset_descr;
+ GLOBAL: gallina_ext module_expr module_type section_subset_expr;
gallina_ext:
[ [ (* Interactive module declaration *)
@@ -460,7 +487,7 @@ GEXTEND Gram
| IDENT "End"; id = identref -> VernacEndSegment id
(* Naming a set of section hyps *)
- | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr ->
+ | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
VernacNameSectionHypSet (id, expr)
(* Requiring an already compiled module *)
@@ -551,22 +578,32 @@ GEXTEND Gram
CMwith (!@loc,mty,decl)
] ]
;
- section_subset_descr:
- [ [ IDENT "All" -> SsAll
- | "Type" -> SsType
- | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l)
- | e = section_subset_expr -> SsExpr e ] ]
- ;
+ (* Proof using *)
section_subset_expr:
+ [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+ starredidentreflist_to_expr l
+ | e = ssexpr -> e ]]
+ ;
+ starredidentref:
+ [ [ i = identref -> SsSingl i
+ | i = identref; "*" -> SsFwdClose(SsSingl i)
+ | "Type" -> SsSingl (!@loc, Id.of_string "Type")
+ | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+ ;
+ ssexpr:
[ "35"
- [ "-"; e = section_subset_expr -> SsCompl e ]
+ [ "-"; e = ssexpr -> SsCompl e ]
| "50"
- [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2)
- | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)]
+ [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2)
+ | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)]
| "0"
- [ i = identref -> SsSet [i]
- | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l
- | "("; e = section_subset_expr; ")"-> e ] ]
+ [ i = starredidentref -> i
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+ starredidentreflist_to_expr l
+ | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+ SsFwdClose(starredidentreflist_to_expr l)
+ | "("; e = ssexpr; ")"-> e
+ | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ]
;
END
@@ -592,15 +629,15 @@ GEXTEND Gram
d = def_body ->
let s = coerce_reference_to_id qid in
VernacDefinition
- ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
+ ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
+ VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d)
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (true, f, s, t)
@@ -1041,7 +1078,9 @@ GEXTEND Gram
VernacOpenCloseScope (local,(false,sc))
| IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
- VernacDelimiters (sc,key)
+ VernacDelimiters (sc, Some key)
+ | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
+ VernacDelimiters (sc, None)
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
refl = LIST1 smart_global -> VernacBindScope (sc,refl)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
deleted file mode 100644
index 84e4a573..00000000
--- a/parsing/g_xml.ml4
+++ /dev/null
@@ -1,290 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Compat
-open Pp
-open Errors
-open Util
-open Names
-open Pcoq
-open Glob_term
-open Tacexpr
-open Libnames
-open Globnames
-open Detyping
-open Misctypes
-open Decl_kinds
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-(* Generic xml parser without raw data *)
-
-type attribute = string * (Loc.t * string)
-type xml = XmlTag of Loc.t * string * attribute list * xml list
-
-let check_tags loc otag ctag =
- if not (String.equal otag ctag) then
- user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
- str "does not match open xml tag " ++ str otag ++ str ".")
-
-let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
-
-GEXTEND Gram
- GLOBAL: xml_eoi;
-
- xml_eoi:
- [ [ x = xml; EOI -> x ] ]
- ;
- xml:
- [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
- "<"; "/"; ctag = IDENT; ">" ->
- check_tags (!@loc) otag ctag;
- XmlTag (!@loc,ctag,attrs,l)
- | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
- XmlTag (!@loc,tag,attrs,[])
- ] ]
- ;
- attr:
- [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
- ;
-END
-
-(* Errors *)
-
-let error_bad_arity loc n =
- let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
- user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^")."))
-
-(* Interpreting attributes *)
-
-let nmtoken (loc,a) =
- try int_of_string a
- with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-
-let get_xml_attr s al =
- try String.List.assoc s al
- with Not_found -> error ("No attribute "^s)
-
-(* Interpreting specific attributes *)
-
-let ident_of_cdata (loc,a) = Id.of_string a
-
-let uri_of_data s =
- try
- let n = String.index s ':' in
- let p = String.index s '.' in
- let s = String.sub s (n+2) (p-n-2) in
- for i = 0 to String.length s - 1 do
- match s.[i] with
- | '/' -> s.[i] <- '.'
- | _ -> ()
- done;
- qualid_of_string s
- with Not_found | Invalid_argument _ ->
- error ("Malformed URI \""^s^"\"")
-
-let constant_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate_constant q
- with Not_found -> error ("No such constant "^string_of_qualid q)
-
-let global_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate q
- with Not_found -> error ("No such global "^string_of_qualid q)
-
-let inductive_of_cdata a = match global_of_cdata a with
- | IndRef (kn,_) -> kn
- | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive")
-
-let ltacref_of_cdata (loc,a) =
- let q = uri_of_data a in
- try (loc,Nametab.locate_tactic q)
- with Not_found -> error ("No such ltac "^string_of_qualid q)
-
-let sort_of_cdata (loc,a) = match a with
- | "Prop" -> GProp
- | "Set" -> GSet
- | "Type" -> GType None
- | _ -> user_err_loc (loc,"",str "sort expected.")
-
-let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
-
-let get_xml_inductive_kn al =
- inductive_of_cdata (* uriType apparent synonym of uri *)
- (try get_xml_attr "uri" al
- with UserError _ -> get_xml_attr "uriType" al)
-
-let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
-
-let get_xml_inductive al =
- (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al))
-
-let get_xml_constructor al =
- (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-
-let get_xml_binder al =
- try Name (ident_of_cdata (String.List.assoc "binder" al))
- with Not_found -> Anonymous
-
-let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
-
-let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
-
-let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
-
-let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al))
-
-(* A leak in the xml dtd: arities of constructor need to know global env *)
-
-let compute_branches_lengths ind =
- let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
- mip.Declarations.mind_consnrealdecls
-
-let compute_inductive_ndecls ind =
- Inductiveops.inductive_nrealdecls ind
-
-(* Interpreting constr as a glob_constr *)
-
-let rec interp_xml_constr = function
- | XmlTag (loc,"REL",al,[]) ->
- GVar (loc, get_xml_ident al)
- | XmlTag (loc,"VAR",al,[]) ->
- error "XML parser: unable to interp free variables"
- | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
- let body,defs = List.sep_last xl in
- let ctx = List.map interp_xml_def defs in
- List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"APPLY",_,x::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
- | XmlTag (loc,"instantiate",_,
- (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
- | XmlTag (loc,"META",al,xl) ->
- GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl))
- | XmlTag (loc,"CONST",al,[]) ->
- GRef (loc, ConstRef (get_xml_constant al), None)
- | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
- let ind = get_xml_inductive al in
- let p = interp_xml_patternsType x in
- let tm = interp_xml_inductiveTerm y in
- let vars = compute_branches_lengths ind in
- let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
- in
- let mat = simple_cases_matrix_of_branches ind brs in
- let n = compute_inductive_ndecls ind in
- let nal,rtn = return_type_of_predicate ind n p in
- GCases (loc,RegularStyle,rtn,[tm,nal],mat)
- | XmlTag (loc,"MUTIND",al,[]) ->
- GRef (loc, IndRef (get_xml_inductive al), None)
- | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- GRef (loc, ConstructRef (get_xml_constructor al), None)
- | XmlTag (loc,"FIX",al,xl) ->
- let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
- let ln,lc,lt = List.split3 lnct in
- let lctx = List.map (fun _ -> []) ln in
- GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"COFIX",al,xl) ->
- let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
- GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"CAST",al,[x1;x2]) ->
- GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
- | XmlTag (loc,"SORT",al,[]) ->
- GSort (loc, get_xml_sort al)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-and interp_xml_tag s = function
- | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
- | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
- str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
-
-and interp_xml_constr_alias s x =
- match interp_xml_tag s x with
- | (_,_,[x]) -> interp_xml_constr x
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_term x = interp_xml_constr_alias "term" x
-and interp_xml_type x = interp_xml_constr_alias "type" x
-and interp_xml_target x = interp_xml_constr_alias "target" x
-and interp_xml_body x = interp_xml_constr_alias "body" x
-and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
-and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
-and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
-and interp_xml_arg x = interp_xml_constr_alias "arg" x
-and interp_xml_substitution x =
- match interp_xml_tag "substitution" x with
- _, al, [x] -> get_xml_name al, interp_xml_constr x
- | loc, _, _ -> error_bad_arity loc 1
- (* no support for empty substitution from official dtd *)
-
-and interp_xml_decl_alias s x =
- match interp_xml_tag s x with
- | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_def x = interp_xml_decl_alias "def" x
-and interp_xml_decl x = interp_xml_decl_alias "decl" x
-
-and interp_xml_recursionOrder x =
- let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
- let (locs, s) = get_xml_attr "type" al in
- match s, l with
- | "Structural", [] -> GStructRec
- | "Structural", _ -> error_bad_arity loc 0
- | "WellFounded", [c] -> GWfRec (interp_xml_type c)
- | "WellFounded", _ -> error_bad_arity loc 1
- | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
- | "Measure", _ -> error_bad_arity loc 2
- | _ -> user_err_loc (locs,"",str "Invalid recursion order.")
-
-and interp_xml_FixFunction x =
- match interp_xml_tag "FixFunction" x with
- | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
- ((Some (nmtoken (get_xml_attr "recIndex" al)),
- interp_xml_recursionOrder x1),
- (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
- | (loc,al,[x1;x2]) ->
- ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-and interp_xml_CoFixFunction x =
- match interp_xml_tag "CoFixFunction" x with
- | (loc,al,[x1;x2]) ->
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-(* Interpreting tactic argument *)
-
-let rec interp_xml_tactic_arg = function
- | XmlTag (loc,"TERM",[],[x]) ->
- ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
- | XmlTag (loc,"CALL",al,xl) ->
- let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
- TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-let parse_tactic_arg ch =
- interp_xml_tactic_arg
- (Pcoq.Gram.entry_parse xml_eoi
- (Pcoq.Gram.parsable (Stream.of_channel ch)))
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 8e839296..c6d5f3b9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -70,7 +70,7 @@ let ttree_remove ttree str =
remove ttree 0
-(* Errors occuring while lexing (explained as "Lexer error: ...") *)
+(* Errors occurring while lexing (explained as "Lexer error: ...") *)
module Error = struct
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 54edbb2c..2e47e07a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -298,7 +298,7 @@ module Prim =
struct
let gec_gen x = make_gen_entry uprim x
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic or vernac extensions *)
let preident = gec_gen (rawwit wit_pre_ident) "preident"
let ident = gec_gen (rawwit wit_ident) "ident"
@@ -334,7 +334,7 @@ module Constr =
struct
let gec_constr = make_gen_entry uconstr (rawwit wit_constr)
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
let constr = gec_constr "constr"
let operconstr = gec_constr "operconstr"
let constr_eoi = eoi_entry constr
@@ -367,7 +367,7 @@ module Tactic =
(* Main entry for extensions *)
let simple_tactic = Gram.entry_create "tactic:simple_tactic"
- (* Entries that can be refered via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic (rawwit wit_open_constr) "open_constr"
@@ -459,8 +459,8 @@ let default_pattern_levels =
[200,Extend.RightA,true;
100,Extend.RightA,false;
99,Extend.RightA,true;
- 10,Extend.LeftA,false;
- 9,Extend.RightA,false;
+ 11,Extend.LeftA,false;
+ 10,Extend.RightA,false;
1,Extend.LeftA,false;
0,Extend.RightA,false]