diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 511 |
1 files changed, 284 insertions, 227 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 717d509e8..10f6d67b7 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -10,6 +10,10 @@ open Pp open Util +open Ast +open Genarg +open Tacexpr +open Vernacexpr (* The lexer of Coq *) @@ -43,9 +47,62 @@ let grammar_delete e rls = List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) (List.rev rls) -type typed_entry = - | Ast of Coqast.t G.Entry.e - | ListAst of Coqast.t list G.Entry.e +module type Gramobj = +sig + type grammar_object + type 'a entry + + val in_entry : 'a -> 'b G.Entry.e -> 'a entry + val object_of_entry : 'a entry -> grammar_object G.Entry.e + val type_of_entry : 'a entry -> 'a +end + +module Gramobj : Gramobj = +struct + type grammar_object = Obj.t + type 'a entry = 'a * grammar_object G.Entry.e + + let in_entry t e = (t,Obj.magic e) + let object_of_entry (t,e) = e + let type_of_entry (t,e) = t +end + +type grammar_object = Gramobj.grammar_object +let in_typed_entry = Gramobj.in_entry +let type_of_typed_entry = Gramobj.type_of_entry +let object_of_typed_entry = Gramobj.object_of_entry +type typed_entry = entry_type Gramobj.entry + +module type Gramtypes = +sig + val inAstListType : Coqast.t list G.Entry.e -> typed_entry + val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry + val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry + val inDynamicAstType : typed_ast G.Entry.e -> typed_entry + val inReferenceAstType : reference_expr G.Entry.e -> typed_entry + val inPureAstType : constr_ast G.Entry.e -> typed_entry + val inGenAstType : 'a raw_abstract_argument_type -> + 'a G.Entry.e -> typed_entry + val outGenAstType : 'a raw_abstract_argument_type -> typed_entry -> 'a G.Entry.e +end + +module Gramtypes : Gramtypes = +struct + let inAstListType = in_typed_entry AstListType + let inTacticAtomAstType = in_typed_entry TacticAtomAstType + let inThmTokenAstType = in_typed_entry ThmTokenAstType + let inDynamicAstType = in_typed_entry DynamicAstType + let inReferenceAstType = in_typed_entry ReferenceAstType + let inPureAstType = in_typed_entry (GenAstType ConstrArgType) + let inGenAstType rawwit = in_typed_entry (GenAstType (unquote rawwit)) + + let outGenAstType (a:'a raw_abstract_argument_type) o = + if type_of_typed_entry o <> GenAstType (unquote a) + then anomaly "outGenAstType: wrong type"; + Obj.magic (object_of_typed_entry o) +end + +open Gramtypes type ext_kind = | ByGrammar of @@ -81,22 +138,21 @@ module Gram = let grammar_extend te pos rls = camlp4_state := ByGrammar (te,pos,rls) :: !camlp4_state; - match te with - | Ast e -> G.extend e pos rls - | ListAst e -> G.extend e pos rls + let a = !Gramext.warning_verbose in + Gramext.warning_verbose := Options.is_verbose (); + G.extend (object_of_typed_entry te) pos rls; + Gramext.warning_verbose := a (* n is the number of extended entries (not the number of Grammar commands!) to remove. *) +let remove_grammar rls te = grammar_delete (object_of_typed_entry te) rls + let rec remove_grammars n = if n>0 then (match !camlp4_state with | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove" - | ByGrammar(Ast e,_,rls)::t -> - grammar_delete e rls; - camlp4_state := t; - remove_grammars (n-1) - | ByGrammar(ListAst e,_,rls)::t -> - grammar_delete e rls; + | ByGrammar(g,_,rls)::t -> + remove_grammar rls g; camlp4_state := t; remove_grammars (n-1) | ByGEXTEND (undo,redo)::t -> @@ -129,44 +185,28 @@ let map_entry f en = let parse_string f x = let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm) +(* let slam_ast (_,fin) id ast = match id with | Coqast.Nvar (loc, s) -> Coqast.Slam (loc, Some s, ast) | Coqast.Nmeta (loc, s) -> Coqast.Smetalam (loc, s, ast) | _ -> invalid_arg "Ast.slam_ast" +*) -(* This is to interpret the macro $ABSTRACT used in binders *) -(* $ABSTRACT should occur in this configuration : *) -(* ($ABSTRACT name (s1 a1 ($LIST l1)) ... (s2 an ($LIST ln)) b) *) -(* where li is id11::...::id1p1 and it produces the ast *) -(* (s1' a1 [id11]...[id1p1](... (sn' an [idn1]...[idnpn]b)...)) *) -(* where s1' is overwritten by name if s1 is $BINDER otherwise s1 *) - -let abstract_binder_ast (_,fin as loc) name a b = - match a with - | Coqast.Node((deb,_),s,d::l) -> - let s' = if s="BINDER" then name else s in - Coqast.Node((deb,fin),s', [d; List.fold_right (slam_ast loc) l b]) - | _ -> invalid_arg "Bad usage of $ABSTRACT macro" - -let abstract_binders_ast loc name a b = - match a with - | Coqast.Node(_,"BINDERS",l) -> - List.fold_right (abstract_binder_ast loc name) l b - | _ -> invalid_arg "Bad usage of $ABSTRACT macro" - -type entry_type = ETast | ETastl - +(* let entry_type ast = match ast with | Coqast.Id (_, "LIST") -> ETastl | Coqast.Id (_, "AST") -> ETast | _ -> invalid_arg "Ast.entry_type" +*) -let type_of_entry e = - match e with - | Ast _ -> ETast - | ListAst _ -> ETastl +(* +let entry_type ast = + match ast with + | AstListType -> ETastl + | _ -> ETast +*) type gram_universe = (string, typed_entry) Hashtbl.t @@ -177,35 +217,61 @@ let trace = ref false let univ_tab = Hashtbl.create 7 -let get_univ s = - try - Hashtbl.find univ_tab s - with Not_found -> +let create_univ s = + let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u + +let uprim = create_univ "prim" +let uconstr = create_univ "constr" +let utactic = create_univ "tactic" +let uvernac = create_univ "vernac" + +let create_univ_if_new s = + (* compatibilite *) + let s = if s = "command" then (warning "'command' grammar universe is obsolete; use name 'constr' instead"; "constr") else s in + try + Hashtbl.find univ_tab s + with Not_found -> if !trace then begin Printf.eprintf "[Creating univ %s]\n" s; flush stderr; () end; let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u - + +let get_univ = create_univ_if_new + let get_entry (u, utab) s = - try + try Hashtbl.find utab s with Not_found -> errorlabstrm "Pcoq.get_entry" (str "unknown grammar entry " ++ str u ++ str ":" ++ str s) - + let new_entry etyp (u, utab) s = let ename = u ^ ":" ^ s in - let e = - match etyp with - | ETast -> Ast (Gram.Entry.create ename) - | ETastl -> ListAst (Gram.Entry.create ename) - in + let e = in_typed_entry etyp (Gram.Entry.create ename) in Hashtbl.add utab s e; e - + +let entry_type (u, utab) s = + try + let e = Hashtbl.find utab s in + Some (type_of_typed_entry e) + with Not_found -> None + +let get_entry_type (u,n) = type_of_typed_entry (get_entry (get_univ u) n) + +let create_entry_if_new (u, utab) s etyp = + try + if type_of_typed_entry (Hashtbl.find utab s) <> etyp then + failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type") + with Not_found -> + if !trace then begin + Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () + end; + let _ = new_entry etyp (u, utab) s in () + let create_entry (u, utab) s etyp = try let e = Hashtbl.find utab s in - if type_of_entry e <> etyp then + if type_of_typed_entry e <> etyp then failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); e with Not_found -> @@ -213,11 +279,46 @@ let create_entry (u, utab) s etyp = Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () end; new_entry etyp (u, utab) s - + +let create_constr_entry u s = + outGenAstType rawwit_constr (create_entry u s (GenAstType ConstrArgType)) + +let create_generic_entry s wit = + let (u,utab) = utactic in + let etyp = unquote wit in + try + let e = Hashtbl.find utab s in + if type_of_typed_entry e <> GenAstType etyp then + failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); + outGenAstType wit e + with Not_found -> + if !trace then begin + Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; () + end; + let e = Gram.Entry.create s in + Hashtbl.add utab s (inGenAstType wit e); e + +let get_generic_entry s = + let (u,utab) = utactic in + try + object_of_typed_entry (Hashtbl.find utab s) + with Not_found -> + error ("unknown grammar entry "^u^":"^s) + +let get_generic_entry_type (u,utab) s = + try + match type_of_typed_entry (Hashtbl.find utab s) with + | GenAstType t -> t + | _ -> error "Not a generic type" + with Not_found -> + error ("unknown grammar entry "^u^":"^s) + let force_entry_type (u, utab) s etyp = try let entry = Hashtbl.find utab s in - let extyp = type_of_entry entry in + let extyp = type_of_typed_entry entry in + if etyp = PureAstType && extyp = GenAstType ConstrArgType then + entry else if etyp = extyp then entry else begin @@ -232,190 +333,110 @@ let force_entry_type (u, utab) s etyp = (* Grammar entries *) +let make_entry (u,univ) in_fun s = + let e = Gram.Entry.create (u ^ ":" ^ s) in + Hashtbl.add univ s (in_fun e); e + +let make_gen_entry u rawwit = make_entry u (inGenAstType rawwit) + +module Prim = + struct + let gec_gen x = make_gen_entry uprim x + let gec = make_entry uprim inPureAstType + let gec_list = make_entry uprim inAstListType + + let preident = gec_gen rawwit_pre_ident "preident" + let ident = gec_gen rawwit_ident "ident" + let rawident = Gram.Entry.create "Prim.rawident" + let natural = gec_gen rawwit_int "natural" + let integer = gec_gen rawwit_int "integer" + let string = gec_gen rawwit_string "string" + let qualid = gec_gen rawwit_qualid "qualid" + let reference = make_entry uprim inReferenceAstType "reference" + let dirpath = Gram.Entry.create "Prim.dirpath" + let astpat = make_entry uprim inDynamicAstType "astpat" + let ast = gec "ast" + let astlist = gec_list "astlist" + let ast_eoi = eoi_entry ast + let astact = gec "astact" + let metaident = gec "metaident" + let numarg = gec "numarg" + let var = gec "var" + end + + module Constr = struct - let uconstr = snd (get_univ "constr") - let gec s = - let e = Gram.Entry.create ("Constr." ^ s) in - Hashtbl.add uconstr s (Ast e); e - - let gec_list s = - let e = Gram.Entry.create ("Constr." ^ s) in - Hashtbl.add uconstr s (ListAst e); e - - let constr = gec "constr" - let constr0 = gec "constr0" - let constr1 = gec "constr1" - let constr2 = gec "constr2" - let constr3 = gec "constr3" - let lassoc_constr4 = gec "lassoc_constr4" - let constr5 = gec "constr5" - let constr6 = gec "constr6" - let constr7 = gec "constr7" - let constr8 = gec "constr8" - let constr9 = gec "constr9" - let constr91 = gec "constr91" - let constr10 = gec "constr10" + let gec = make_entry uconstr inPureAstType + let gec_constr = make_gen_entry uconstr rawwit_constr + let gec_list = make_entry uconstr inAstListType + + let constr = gec_constr "constr" + let constr0 = gec_constr "constr0" + let constr1 = gec_constr "constr1" + let constr2 = gec_constr "constr2" + let constr3 = gec_constr "constr3" + let lassoc_constr4 = gec_constr "lassoc_constr4" + let constr5 = gec_constr "constr5" + let constr6 = gec_constr "constr6" + let constr7 = gec_constr "constr7" + let constr8 = gec_constr "constr8" + let constr9 = gec_constr "constr9" + let constr91 = gec_constr "constr91" + let constr10 = gec_constr "constr10" let constr_eoi = eoi_entry constr - let lconstr = gec "lconstr" + let lconstr = gec_constr "lconstr" let ident = gec "ident" - let qualid = gec_list "qualid" + let qualid = gec "qualid" let global = gec "global" let ne_ident_comma_list = gec_list "ne_ident_comma_list" let ne_constr_list = gec_list "ne_constr_list" - let sort = gec "sort" + let sort = gec_constr "sort" let pattern = gec "pattern" + let constr_pattern = gec "constr_pattern" let ne_binders_list = gec_list "ne_binders_list" - - let uconstr = snd (get_univ "constr") end module Tactic = struct - let utactic = snd (get_univ "tactic") - let gec s = - let e = Gram.Entry.create ("Tactic." ^ s) in - Hashtbl.add utactic s (Ast e); e - - let gec_list s = - let e = Gram.Entry.create ("Tactic." ^ s) in - Hashtbl.add utactic s (ListAst e); e - - let autoargs = gec_list "autoargs" - let binding_list = gec "binding_list" - let castedopenconstrarg = gec "castedopenconstrarg" - let castedconstrarg = gec "castedconstrarg" - let com_binding_list = gec_list "com_binding_list" - let constrarg = gec "constrarg" - let constrarg_binding_list = gec_list "constrarg_binding_list" - let numarg_binding_list = gec_list "numarg_binding_list" - let lconstrarg_binding_list = gec_list "lconstrarg_binding_list" - let constrarg_list = gec_list "constrarg_list" - let ne_constrarg_list = gec_list "ne_constrarg_list" - let ident_or_numarg = gec "ident_or_numarg" - let ident_or_constrarg = gec "ident_or_constrarg" - let identarg = gec "identarg" - let hypident = gec "hypident" - let idmeta_arg = gec "idmeta_arg" - let idmetahyp = gec "idmetahyp" - let qualidarg = gec "qualidarg" - let input_fun = gec "input_fun" - let lconstrarg = gec "lconstrarg" - let let_clause = gec "let_clause" - let letcut_clause = gec "letcut_clause" - let clausearg = gec "clausearg" - let match_context_rule = gec "match_context_rule" - let match_hyps = gec "match_hyps" - let match_pattern = gec "match_pattern" - let match_context_list = gec_list "match_context_list" - let match_rule = gec "match_rule" - let match_list = gec_list "match_list" - let ne_identarg_list = gec_list "ne_identarg_list" - let ne_hyp_list = gec_list "ne_hyp_list" - let ne_idmetahyp_list = gec_list "ne_idmetahyp_list" - let ne_qualidarg_list = gec_list "ne_qualidarg_list" - let ne_pattern_list = gec_list "ne_pattern_list" - let clause_pattern = gec "clause_pattern" - let one_intropattern = gec "one_intropattern" - let intropattern = gec "intropattern" - let ne_intropattern = gec "ne_intropattern" - let simple_intropattern = gec "simple_intropattern" - let ne_unfold_occ_list = gec_list "ne_unfold_occ_list" - let rec_clause = gec "rec_clause" - let red_tactic = gec "red_tactic" - let red_flag = gec "red_flag" - let numarg = gec "numarg" - let pattern_occ = gec "pattern_occ" - let pattern_occ_hyp = gec "pattern_occ_hyp" - let pure_numarg = gec "pure_numarg" - let simple_binding = gec "simple_binding" - let simple_binding_list = gec_list "simple_binding_list" - let simple_tactic = gec "simple_tactic" - let tactic = gec "tactic" - let tactic_arg = gec "tactic_arg" - let tactic_atom0 = gec "tactic_atom0" - let tactic_atom = gec "tactic_atom" - let tactic_expr = gec "tactic_expr" - let tactic_expr_par = gec "tactic_expr_par" - let unfold_occ = gec "unfold_occ" - let with_binding_list = gec "with_binding_list" - let fixdecl = gec_list "fixdecl" - let cofixdecl = gec_list "cofixdecl" - let tacarg_list = gec_list "tacarg_list" + let gec = make_entry utactic inPureAstType + let gec_list = make_entry utactic inAstListType + let castedopenconstr = + make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr" + let constr_with_bindings = + make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" + let constrarg = make_gen_entry utactic rawwit_constr_may_eval "constrarg" + let quantified_hypothesis = + make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis" + let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var" + let red_tactic = make_gen_entry utactic rawwit_red_expr "red_tactic" + let simple_tactic = make_entry utactic inTacticAtomAstType "simple_tactic" + let tactic_arg = Gram.Entry.create "tactic:tactic_arg" + let tactic = make_gen_entry utactic rawwit_tactic "tactic" let tactic_eoi = eoi_entry tactic end module Vernac_ = struct - let uvernac = snd (get_univ "vernac") - let gec s = - let e = Gram.Entry.create ("Vernac." ^ s) in - Hashtbl.add uvernac s (Ast e); e - - let gec_list s = - let e = Gram.Entry.create ("Vernac." ^ s) in - Hashtbl.add uvernac s (ListAst e); e - - let identarg = gec "identarg" - let ne_identarg_list = gec_list "ne_identarg_list" - let qualidarg = gec "qualidarg" - let commentarg = gec "commentarg" - let commentarg_list = gec_list "commentarg_list" - let ne_qualidarg_list = gec_list "ne_qualidarg_list" - let numarg = gec "numarg" - let numarg_list = gec_list "numarg_list" - let ne_numarg_list = gec_list "ne_numarg_list" - let stringarg = gec "stringarg" - let ne_stringarg_list = gec_list "ne_stringarg_list" - let constrarg = gec "constrarg" - let ne_constrarg_list = gec_list "ne_constrarg_list" - let tacarg = gec "tacarg" - let reduce = gec_list "reduce" - let sortarg = gec "sortarg" - let theorem_body = gec "theorem_body" - let thm_tok = gec "thm_tok" - - let gallina = gec "gallina" - let gallina_ext = gec "gallina_ext" - let command = gec "command" - let syntax = gec "syntax_command" - let vernac = gec "vernac" + let thm_token = make_entry uvernac inThmTokenAstType "thm_token" + let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" + let gec_vernac s = Gram.Entry.create ("vernac:" ^ s) + let gallina = gec_vernac "gallina" + let gallina_ext = gec_vernac "gallina_ext" + let command = gec_vernac "command" + let syntax = gec_vernac "syntax_command" + let vernac = gec_vernac "Vernac_.vernac" let vernac_eoi = eoi_entry vernac end -module Prim = - struct - let uprim = snd (get_univ "prim") - let gec s = - let e = Gram.Entry.create ("Prim." ^ s) in - Hashtbl.add uprim s (Ast e); e - let ast = gec "ast" - let ast_eoi = eoi_entry ast - let astact = gec "astact" - let astpat = gec "astpat" - let entry_type = gec "entry_type" - let grammar_entry = gec "grammar_entry" - let grammar_entry_eoi = eoi_entry grammar_entry - let ident = gec "ident" - let metaident = gec "metaident" - let number = gec "number" - let path = gec "path" - let string = gec "string" - let syntax_entry = gec "syntax_entry" - let syntax_entry_eoi = eoi_entry syntax_entry - let uprim = snd (get_univ "prim") - let var = gec "var" - end - - let main_entry = Gram.Entry.create "vernac" GEXTEND Gram main_entry: - [ [ a = Vernac_.vernac -> Some a | EOI -> None ] ] + [ [ a = Vernac_.vernac -> Some (loc,a) | EOI -> None ] ] ; END @@ -439,13 +460,13 @@ let define_quotation default s e = *) END); (GEXTEND Gram - GLOBAL: ast constr vernac tactic; + GLOBAL: ast constr command tactic; ast: [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ]; (* Uncomment this to keep compatibility with old grammar syntax constr: [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ]; - vernac: + command: [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ]; tactic: [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ]; @@ -454,31 +475,67 @@ let define_quotation default s e = let _ = define_quotation false "ast" ast in () -let constr_parser = ref Constr.constr -let tactic_parser = ref Tactic.tactic -let vernac_parser = ref Vernac_.vernac +let gecdyn s = + let e = Gram.Entry.create ("Dyn." ^ s) in + Hashtbl.add (snd uconstr) s (inDynamicAstType e); e + +let dynconstr = gecdyn "dynconstr" +let dyntactic = gecdyn "dyntactic" +let dynvernac = gecdyn "dynvernac" +let dynastlist = gecdyn "dynastlist" +let dynast = gecdyn "dynast" + +let globalizer = ref (fun x -> x) +let set_globalizer f = globalizer := f -let update_constr_parser p = constr_parser := p -let update_tactic_parser p = tactic_parser := p -let update_vernac_parser p = vernac_parser := p +GEXTEND Gram + dynconstr: [ [ a = Constr.constr -> !globalizer (PureAstNode a) ] ]; +(* + dyntactic: [ [ a = Tactic.tactic -> !globalizer (TacticAstNode a) ] ]; + dynvernac: [ [ a = Vernac_.vernac -> !globalizer(VernacAstNode a) ] ]; +*) + dynastlist: [ [ a = Prim.astlist -> AstListNode a ] ]; + dynast: [ [ a = ast -> PureAstNode a ] ]; +END (**********************************************************************) (* The following is to dynamically set the parser in Grammar actions *) (* and Syntax pattern, according to the universe of the rule defined *) -let default_action_parser_ref = ref ast +type parser_type = + | AstListParser + | AstParser + | ConstrParser + | TacticParser + | VernacParser -let get_default_action_parser () = !default_action_parser_ref +let default_action_parser_ref = ref dynast -let set_default_action_parser f = (default_action_parser_ref := f) +let get_default_action_parser () = !default_action_parser_ref -let set_default_action_parser_by_name = function - | "constr" -> set_default_action_parser !constr_parser - | "tactic" -> set_default_action_parser !tactic_parser - | "vernac" -> set_default_action_parser !vernac_parser - | _ -> set_default_action_parser ast +let entry_type_from_name = function + | "constr" -> GenAstType ConstrArgType + | "tactic" -> failwith "Not supported" + | "vernac" -> failwith "Not supported" + | s -> GenAstType ConstrArgType + +let entry_type_of_parser = function + | AstListParser -> Some AstListType + | _ -> None + +let parser_type_from_name = function + | "constr" -> ConstrParser + | "tactic" -> TacticParser + | "vernac" -> VernacParser + | s -> AstParser + +let set_default_action_parser = function + | AstListParser -> default_action_parser_ref := dynastlist + | AstParser -> default_action_parser_ref := dynast + | ConstrParser -> default_action_parser_ref := dynconstr + | TacticParser -> default_action_parser_ref := dyntactic + | VernacParser -> default_action_parser_ref := dynvernac let default_action_parser = Gram.Entry.of_parser "default_action_parser" (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm) - |