diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 4 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 14 | ||||
| -rw-r--r-- | parsing/g_obligations.ml4 | 135 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 18 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 6 |
6 files changed, 161 insertions, 18 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 3245c642fa..e2b78d725c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -47,7 +47,7 @@ open Egramml let constr_expr_of_name (loc,na) = match na with | Anonymous -> CHole (loc,None,None) - | Name id -> CRef (Ident (loc,id)) + | Name id -> CRef (Ident (loc,id), None) let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) @@ -76,7 +76,7 @@ let make_constr_action make (v :: constrs, constrlists, binders) tl) | ETReference -> Gram.action (fun (v:reference) -> - make (CRef v :: constrs, constrlists, binders) tl) + make (CRef (v,None) :: constrs, constrlists, binders) tl) | ETName -> Gram.action (fun (na:Loc.t * Name.t) -> make (constr_expr_of_name na :: constrs, constrlists, binders) tl) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index cdaa809d28..499e7b0531 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -159,7 +159,7 @@ GEXTEND Gram ; constr: [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global -> CAppExpl(!@loc,(None,f),[]) ] ] + | "@"; f=global -> CAppExpl(!@loc,(None,f,None),[]) ] ] ; operconstr: [ "200" RIGHTA @@ -183,20 +183,20 @@ GEXTEND Gram | "90" RIGHTA [ ] | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f),args) + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,None),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> - let args = List.map (fun x -> CRef (Ident x), None) args in + let args = List.map (fun x -> CRef (Ident x,None), None) args in CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAppExpl (!@loc,(None,Ident (!@loc,ldots_var)),[c]) ] + CAppExpl (!@loc,(None,Ident (!@loc,ldots_var),None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - CApp(!@loc,(Some (List.length args+1),CRef f),args@[c,None]) + CApp(!@loc,(Some (List.length args+1),CRef (f,None)),args@[c,None]) | c=operconstr; ".("; "@"; f=global; args=LIST0 (operconstr LEVEL "9"); ")" -> - CAppExpl(!@loc,(Some (List.length args+1),f),args@[c]) + CAppExpl(!@loc,(Some (List.length args+1),f,None),args@[c]) | c=operconstr; "%"; key=IDENT -> CDelimiters (!@loc,key,c) ] | "0" [ c=atomic_constr -> c @@ -277,7 +277,7 @@ GEXTEND Gram | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: - [ [ g=global -> CRef g + [ [ g=global -> CRef (g,None) | s=sort -> CSort (!@loc,s) | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 new file mode 100644 index 0000000000..2354aa3325 --- /dev/null +++ b/parsing/g_obligations.ml4 @@ -0,0 +1,135 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 camlp4deps: "grammar/grammar.cma" i*) + +(* + Syntax for the subtac terms and types. + Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) + + +open Libnames +open Constrexpr +open Constrexpr_ops + +(* We define new entries for programs, with the use of this module + * Subtac. These entries are named Subtac.<foo> + *) + +module Gram = Pcoq.Gram +module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic + +open Pcoq + +let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) + +type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type + +let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = + Genarg.create_arg None "withtac" + +let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac) + +GEXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> Some t + | -> None ] ] + ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [LocalRawAssum ([id], default_binder_kind, typ)] + ] ]; + + END + +open Obligations + +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater) + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl +| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> + [ obligation (num, Some name, Some t) tac ] +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> + [ obligation (num, Some name, None) tac ] +| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> + [ obligation (num, None, Some t) tac ] +| [ "Obligation" integer(num) withtac(tac) ] -> + [ obligation (num, None, None) tac ] +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> + [ next_obligation (Some name) tac ] +| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] +END + +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF +| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> + [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] +END + +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> + [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" "with" tactic(t) ] -> + [ try_solve_obligations None (Some (Tacinterp.interp t)) ] +| [ "Solve" "Obligations" ] -> + [ try_solve_obligations None None ] +END + +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> + [ solve_all_obligations (Some (Tacinterp.interp t)) ] +| [ "Solve" "All" "Obligations" ] -> + [ solve_all_obligations None ] +END + +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF +| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] +| [ "Admit" "Obligations" ] -> [ admit_obligations None ] +END + +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ + set_default_tactic + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) + (Tacintern.glob_tactic t) ] +END + +open Pp + +VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY +| [ "Show" "Obligation" "Tactic" ] -> [ + msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] +END + +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY +| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] +| [ "Obligations" ] -> [ show_obligations None ] +END + +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY +| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] +| [ "Preterm" ] -> [ msg_info (show_term None) ] +END + +open Pp + +(* Declare a printer for the content of Program tactics *) +let () = + let printer _ _ _ = function + | None -> mt () + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac + in + (* should not happen *) + let dummy _ _ _ expr = assert false in + Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 6b989b6baf..65e046fb86 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -146,7 +146,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [ElimOnIdent id,(None,None)],None,None -> - TacCase (with_evar,(CRef (Ident id),NoBindings)) + TacCase (with_evar,(CRef (Ident id,None),NoBindings)) | ic -> if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic) then diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 73b26b02d3..df3c18d10d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -72,8 +72,9 @@ GEXTEND Gram [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v - | IDENT "Local"; v = vernac_aux -> VernacLocal (true, v) - | IDENT "Global"; v = vernac_aux -> VernacLocal (false, v) + + | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) + | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument @@ -85,7 +86,13 @@ GEXTEND Gram | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_aux -> v ] + | v = vernac_poly -> v ] + ] + ; + vernac_poly: + [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | v = vernac_aux -> v ] ] ; vernac_aux: @@ -171,8 +178,8 @@ GEXTEND Gram [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = identref; bl = binders; ":"; c = lconstr -> - (Some id,(bl,c,None)) ] -> - VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false) + (Some id,(bl,c,None)) ] -> + VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> @@ -203,6 +210,7 @@ GEXTEND Gram VernacRegister(id, RegisterInline) ] ] ; + gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; ps = binders; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 820d44392b..99cfa70838 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -179,7 +179,7 @@ let rec interp_xml_constr = function | XmlTag (loc,"META",al,xl) -> GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl)) | XmlTag (loc,"CONST",al,[]) -> - GRef (loc, ConstRef (get_xml_constant 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 @@ -192,9 +192,9 @@ let rec interp_xml_constr = function 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)) + GRef (loc, IndRef (get_xml_inductive al), None) | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> - GRef (loc, ConstructRef (get_xml_constructor 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 |