diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 44 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 12 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 66 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 115 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 290 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 10 |
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] |