From 5fa47f1258408541150e2e4c26d60ff694e7c1bc Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:37 +0000 Subject: locus.mli for occurrences+clauses, misctypes.mli for various little things Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_constr.ml4 | 20 +++++++------- parsing/g_ltac.ml4 | 3 ++- parsing/g_prim.ml4 | 4 +-- parsing/g_proofs.ml4 | 3 ++- parsing/g_tactic.ml4 | 49 ++++++++++++++++++---------------- parsing/g_vernac.ml4 | 9 ++++--- parsing/g_xml.ml4 | 8 +++--- parsing/grammar.mllib | 2 ++ parsing/pcoq.mli | 3 ++- parsing/ppconstr.ml | 33 +++++++++++++---------- parsing/ppconstr.mli | 3 ++- parsing/pptactic.ml | 23 +++++++++------- parsing/pptactic.mli | 1 + parsing/prettyp.ml | 9 ++++--- parsing/prettyp.mli | 2 +- parsing/q_constr.ml4 | 11 ++++---- parsing/q_coqast.ml4 | 74 ++++++++++++++++++++++++++++----------------------- 17 files changed, 144 insertions(+), 113 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 06d922a7c..c8ca6cbab 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -18,6 +18,8 @@ open Topconstr open Util open Tok open Compat +open Misctypes +open Decl_kinds let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; @@ -29,7 +31,7 @@ let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty) let binders_of_names l = List.map (fun (loc, na) -> @@ -38,7 +40,7 @@ let binders_of_names l = let binders_of_lidents l = List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, + LocalRawAssum ([loc, Name id], Default Explicit, CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -144,8 +146,8 @@ GEXTEND Gram [ [ c = lconstr -> c ] ] ; sort: - [ [ "Set" -> GProp Pos - | "Prop" -> GProp Null + [ [ "Set" -> GSet + | "Prop" -> GProp | "Type" -> GType None ] ] ; lconstr: @@ -160,13 +162,13 @@ GEXTEND Gram [ c = binder_constr -> c ] | "100" RIGHTA [ c1 = operconstr; "<:"; c2 = binder_constr -> - CCast(loc,c1, CastConv (VMcast,c2)) + CCast(loc,c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> - CCast(loc,c1, CastConv (VMcast,c2)) + CCast(loc,c1, CastVM c2) | c1 = operconstr; ":";c2 = binder_constr -> - CCast(loc,c1, CastConv (DEFAULTcast,c2)) + CCast(loc,c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv (DEFAULTcast,c2)) + CCast(loc,c1, CastConv c2) | c1 = operconstr; ":>" -> CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] @@ -410,7 +412,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] + [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))] | "{"; id=name; "}" -> [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index bf0e13e02..e2edbb096 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -17,6 +17,7 @@ open Pcoq open Prim open Tactic open Tok +open Misctypes let fail_default_value = ArgArg 0 @@ -177,7 +178,7 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) + | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index fd6fc7dd8..d6b2d8380 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -86,8 +86,8 @@ GEXTEND Gram [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ] ; smart_global: - [ [ c = reference -> Genarg.AN c - | ntn = by_notation -> Genarg.ByNotation ntn ] ] + [ [ c = reference -> Misctypes.AN c + | ntn = by_notation -> Misctypes.ByNotation ntn ] ] ; qualid: [ [ qid = basequalid -> loc, qid ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 5f44a9e9c..6edb0bfc1 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -17,6 +17,7 @@ open Locality open Prim open Constr open Tok +open Misctypes let thm_token = G_vernac.thm_token @@ -113,6 +114,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8b72a5e93..7cbcd584c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -18,6 +18,9 @@ open Libnames open Termops open Tok open Compat +open Misctypes +open Locus +open Decl_kinds let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] @@ -166,17 +169,17 @@ let mkCLambdaN_simple bl c = let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) let map_int_or_var f = function - | Glob_term.ArgArg x -> Glob_term.ArgArg (f x) - | Glob_term.ArgVar _ as y -> y + | ArgArg x -> ArgArg (f x) + | ArgVar _ as y -> y -let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr } +let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } let has_no_specified_occs cl = (cl.onhyps = None || - List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr) + List.for_all (fun ((occs,_),_) -> occs = AllOccurrences) (Option.get cl.onhyps)) - && (cl.concl_occs = all_occurrences_expr - || cl.concl_occs = no_occurrences_expr) + && (cl.concl_occs = AllOccurrences + || cl.concl_occs = NoOccurrences) let merge_occurrences loc cl = function | None -> @@ -185,11 +188,11 @@ let merge_occurrences loc cl = function user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.") | Some (occs,p) -> (Some p, - if occs = all_occurrences_expr then cl + if occs = AllOccurrences then cl else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs } else match cl.onhyps with | Some [(occs',id),l] when - occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr -> + occs' = AllOccurrences && cl.concl_occs = NoOccurrences -> { cl with onhyps=Some[(occs,id),l] } | _ -> if has_no_specified_occs cl then @@ -205,12 +208,12 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Glob_term.ArgArg n - | id = identref -> Glob_term.ArgVar id ] ] + [ [ n = integer -> ArgArg n + | id = identref -> ArgVar id ] ] ; nat_or_var: - [ [ n = natural -> Glob_term.ArgArg n - | id = identref -> Glob_term.ArgVar id ] ] + [ [ n = natural -> ArgArg n + | id = identref -> ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -236,18 +239,18 @@ GEXTEND Gram ; conversion: [ [ c = constr -> (None, c) - | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2) + | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2) | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> (Some (occs,c1), c2) ] ] ; occs_nums: - [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl + [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl | "-"; n = nat_or_var; nl = LIST0 int_or_var -> (* have used int_or_var instead of nat_or_var for compatibility *) - all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ] + AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ] ; occs: - [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ] + [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ] ; pattern_occ: [ [ c = constr; nl = occs -> (nl,c) ] ] @@ -374,7 +377,7 @@ GEXTEND Gram | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> {onhyps=Some hl; concl_occs=occs} | hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ] + {onhyps=Some hl; concl_occs=NoOccurrences} ] ] ; clause_dft_concl: [ [ "in"; cl = in_clause -> cl @@ -383,14 +386,14 @@ GEXTEND Gram ; clause_dft_all: [ [ "in"; cl = in_clause -> cl - | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ] + | -> {onhyps=None; concl_occs=AllOccurrences} ] ] ; opt_clause: [ [ "in"; cl = in_clause -> Some cl | -> None ] ] ; concl_occ: [ [ "*"; occs = occs -> occs - | -> no_occurrences_expr ] ] + | -> NoOccurrences ] ] ; in_hyp_list: [ [ "in"; idl = LIST1 id_or_meta -> idl @@ -546,9 +549,9 @@ GEXTEND Gram TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacLetTac (Names.Name id,b,nowhere,true) + TacLetTac (Names.Name id,b,Locusops.nowhere,true) | IDENT "pose"; b = constr; na = as_name -> - TacLetTac (na,b,nowhere,true) + TacLetTac (na,b,Locusops.nowhere,true) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> TacLetTac (Names.Name id,c,p,true) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> @@ -572,9 +575,9 @@ GEXTEND Gram | IDENT "cut"; c = constr -> TacCut c | IDENT "generalize"; c = constr -> - TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)] + TacGeneralize [((AllOccurrences,c),Names.Anonymous)] | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in + let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in TacGeneralize (List.map gen_everywhere (c::l)) | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; na = as_name; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f684b9a0d..34e0d9532 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -23,6 +23,7 @@ open Genarg open Ppextend open Goptions open Declaremods +open Misctypes open Prim open Constr @@ -240,7 +241,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -343,7 +344,7 @@ GEXTEND Gram (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, Glob_term.CastConv (_, t)) -> + | CCast(_,b, (CastConv t|CastVM t)) -> (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) | _ -> (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ] @@ -568,7 +569,7 @@ GEXTEND Gram VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> Some r | ":="; c = lconstr -> Some c | -> None ] -> @@ -714,7 +715,7 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> VernacInstance (true, not (use_section_locality ()), snd namesup, (fst namesup, expl, t), diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 3cb553437..7c26ac124 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -20,6 +20,8 @@ open Libnames open Nametab open Detyping open Tok +open Misctypes +open Decl_kinds (* Generic xml parser without raw data *) @@ -96,8 +98,8 @@ let inductive_of_cdata a = match global_of_cdata a with let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) let sort_of_cdata (loc,a) = match a with - | "Prop" -> GProp Null - | "Set" -> GProp Pos + | "Prop" -> GProp + | "Set" -> GSet | "Type" -> GType None | _ -> user_err_loc (loc,"",str "sort expected.") @@ -191,7 +193,7 @@ let rec interp_xml_constr = function 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 (DEFAULTcast, interp_xml_type 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,_,_) -> diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 39fd88506..cae4b13d6 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -56,11 +56,13 @@ Lib Goptions Decl_kinds Global +Locusops Termops Namegen Evd Reductionops Inductiveops +Miscops Glob_term Detyping Pattern diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ebcc53264..5bc6bddd9 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -17,6 +17,7 @@ open Topconstr open Tacexpr open Libnames open Compat +open Misctypes (** The parser of Coq *) @@ -220,7 +221,7 @@ module Tactic : val int_or_var : int or_var Gram.entry val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_atomic_tactic_expr Gram.entry - val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry + val simple_intropattern : intro_pattern_expr located Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 98ed6883e..45ea77d13 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -21,6 +21,9 @@ open Pattern open Glob_term open Constrextern open Termops +open Decl_kinds +open Misctypes +open Locus (*i*) let sep_v = fun _ -> str"," ++ spc() @@ -110,8 +113,8 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_universe = Univ.pr_uni let pr_glob_sort = function - | GProp Term.Null -> str "Prop" - | GProp Term.Pos -> str "Set" + | GProp -> str "Prop" + | GSet -> str "Set" | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u) let pr_id = pr_id @@ -253,7 +256,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,k,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c, CastConv (_,t)) -> c, t + | CCast(_,c, (CastConv t|CastVM t)) -> c, t | _ -> c, CHole (dummy_loc, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) @@ -530,13 +533,12 @@ let pr pr sep inherited a = | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_glob_sort s, latom - | CCast (_,a,CastConv (k,b)) -> - let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in - hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b), - lcast - | CCast (_,a,CastCoerce) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), - lcast + | CCast (_,a,b) -> + hv 0 (pr mt (lcast,L) a ++ cut () ++ + match b with + | CastConv b -> str ":" ++ pr mt (-lcast,E) b + | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastCoerce -> str ":>"), lcast | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> @@ -581,12 +583,15 @@ let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders spc (pr ltop) -let pr_with_occurrences pr occs = +let pr_with_occurrences pr (occs,c) = match occs with - ((false,[]),c) -> pr c - | ((nowhere_except_in,nl),c) -> + | AllOccurrences -> pr c + | NoOccurrences -> failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> hov 1 (pr c ++ spc() ++ str"at " ++ - (if nowhere_except_in then mt() else str "- ") ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc() ++ str"at - " ++ hov 0 (prlist_with_sep spc (pr_or_var int) nl)) let pr_red_flag pr r = diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index c61d4c206..1497c90e7 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -16,7 +16,8 @@ open Topconstr open Names open Errors open Util -open Genarg +open Misctypes +open Locus val extract_lam_binders : constr_expr -> local_binder list * constr_expr diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 513034194..c50ab9fcd 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -20,6 +20,9 @@ open Pattern open Ppextend open Ppconstr open Printer +open Misctypes +open Locus +open Decl_kinds let pr_global x = Nametab.pr_global_env Idset.empty x @@ -384,11 +387,11 @@ let pr_by_tactic prt = function | tac -> spc() ++ str "by " ++ prt tac let pr_hyp_location pr_id = function - | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs - | occs, Termops.InHypTypeOnly -> + | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, InHypTypeOnly -> spc () ++ pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs - | occs, Termops.InHypValueOnly -> + | occs, InHypValueOnly -> spc () ++ pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs @@ -403,17 +406,17 @@ let pr_in_hyp_as pr_id = function | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat let pr_clauses default_is_concl pr_id = function - | { onhyps=Some []; concl_occs=occs } - when occs = all_occurrences_expr & default_is_concl = Some true -> mt () - | { onhyps=None; concl_occs=occs } - when occs = all_occurrences_expr & default_is_concl = Some false -> mt () + | { onhyps=Some []; concl_occs=AllOccurrences } + when default_is_concl = Some true -> mt () + | { onhyps=None; concl_occs=AllOccurrences } + when default_is_concl = Some false -> mt () | { onhyps=None; concl_occs=occs } -> - if occs = no_occurrences_expr then pr_in (str " * |-") + if occs = NoOccurrences then pr_in (str " * |-") else pr_in (pr_with_occurrences (fun () -> str " *") (occs,())) | { onhyps=Some l; concl_occs=occs } -> pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ - (if occs = no_occurrences_expr then mt () + (if occs = NoOccurrences then mt () else pr_with_occurrences (fun () -> str" |- *") (occs,()))) let pr_orient b = if b then mt () else str " <-" @@ -690,7 +693,7 @@ and pr_atom1 = function | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg c) - | TacLetTac (na,c,cl,true) when cl = nowhere -> + | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere -> hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c) | TacLetTac (na,c,cl,b) -> hov 1 ((if b then str "set" else str "remember") ++ diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index d85f1ec3f..afcc83c68 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -17,6 +17,7 @@ open Pattern open Ppextend open Environ open Evd +open Misctypes val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index fad4e879e..5dbef1fe5 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -31,6 +31,7 @@ open Printmod open Libnames open Nametab open Recordops +open Misctypes type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -644,11 +645,11 @@ let print_any_name = function "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_name = function - | Genarg.ByNotation (loc,ntn,sc) -> + | ByNotation (loc,ntn,sc) -> print_any_name (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) - | Genarg.AN ref -> + | AN ref -> print_any_name (locate_any_name ref) let print_opaque_name qid = @@ -686,11 +687,11 @@ let print_about_any k = hov 0 (pr_located_qualid k) ++ fnl() let print_about = function - | Genarg.ByNotation (loc,ntn,sc) -> + | ByNotation (loc,ntn,sc) -> print_about_any (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) - | Genarg.AN ref -> + | AN ref -> print_about_any (locate_any_name ref) (* for debug *) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 40ba7f047..b3271d141 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -16,7 +16,7 @@ open Environ open Reductionops open Libnames open Nametab -open Genarg +open Misctypes (** A Pretty-Printer for the Calculus of Inductive Constructions. *) diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index f5225feb3..543240a82 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -17,6 +17,7 @@ open Pp open Compat open Pcaml open PcamlSig +open Misctypes let loc = dummy_loc let dloc = <:expr< Pp.dummy_loc >> @@ -33,8 +34,8 @@ EXTEND <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> GProp Pos - | "Prop" -> GProp Null + [ [ "Set" -> GSet + | "Prop" -> GProp | "Type" -> GType None ] ] ; ident: @@ -49,9 +50,9 @@ EXTEND constr: [ "200" RIGHTA [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> - <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> - <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >> + <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >> | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> (* fix todo *) @@ -61,7 +62,7 @@ EXTEND <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA [ c1 = constr; "->"; c2 = SELF -> - <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ] + <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index f36465207..6ef7ba1d8 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -51,18 +51,18 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> let mlexpr_of_loc loc = <:expr< $dloc$ >> let mlexpr_of_by_notation f = function - | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> - | Genarg.ByNotation (loc,s,sco) -> - <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> + | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >> + | Misctypes.ByNotation (loc,s,sco) -> + <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> let mlexpr_of_intro_pattern = function - | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> - | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >> - | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >> - | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> - | Genarg.IntroIdentifier id -> - <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> - | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ -> + | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >> + | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >> + | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >> + | Misctypes.IntroIdentifier id -> + <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >> + | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ -> failwith "mlexpr_of_intro_pattern: TODO" let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) @@ -72,34 +72,40 @@ let mlexpr_of_or_metaid f = function | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >> let mlexpr_of_quantified_hypothesis = function - | Glob_term.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> - | Glob_term.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> + | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >> + | Misctypes.NamedHyp id -> <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >> let mlexpr_of_or_var f = function - | Glob_term.ArgArg x -> <:expr< Glob_term.ArgArg $f x$ >> - | Glob_term.ArgVar id -> <:expr< Glob_term.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> + | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >> + | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) -let mlexpr_of_occs = - mlexpr_of_pair - mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)) +let mlexpr_of_occs = function + | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >> + | Locus.AllOccurrencesBut l -> + <:expr< Locus.AllOccurrencesBut + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> + | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >> + | Locus.OnlyOccurrences l -> + <:expr< Locus.OnlyOccurrences + $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >> let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f let mlexpr_of_hyp_location = function - | occs, Termops.InHyp -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >> - | occs, Termops.InHypTypeOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >> - | occs, Termops.InHypValueOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >> + | occs, Locus.InHyp -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >> + | occs, Locus.InHypTypeOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >> + | occs, Locus.InHypValueOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >> let mlexpr_of_clause cl = - <:expr< {Tacexpr.onhyps= + <:expr< {Locus.onhyps= $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) - cl.Tacexpr.onhyps$; - Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >> + cl.Locus.onhyps$; + Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >> let mlexpr_of_red_flags { Glob_term.rBeta = bb; @@ -120,8 +126,8 @@ let mlexpr_of_explicitation = function | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >> let mlexpr_of_binding_kind = function - | Glob_term.Implicit -> <:expr< Glob_term.Implicit >> - | Glob_term.Explicit -> <:expr< Glob_term.Explicit >> + | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >> + | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >> let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> @@ -215,14 +221,14 @@ let rec mlexpr_of_may_eval f = function <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >> let mlexpr_of_binding_kind = function - | Glob_term.ExplicitBindings l -> + | Misctypes.ExplicitBindings l -> let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in - <:expr< Glob_term.ExplicitBindings $l$ >> - | Glob_term.ImplicitBindings l -> + <:expr< Misctypes.ExplicitBindings $l$ >> + | Misctypes.ImplicitBindings l -> let l = mlexpr_of_list mlexpr_of_constr l in - <:expr< Glob_term.ImplicitBindings $l$ >> - | Glob_term.NoBindings -> - <:expr< Glob_term.NoBindings >> + <:expr< Misctypes.ImplicitBindings $l$ >> + | Misctypes.NoBindings -> + <:expr< Misctypes.NoBindings >> let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr -- cgit v1.2.3