From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/ssr/ssrparser.ml4 | 74 +++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 31 deletions(-) (limited to 'plugins/ssr/ssrparser.ml4') diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5f396744..eb69dca9 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -10,6 +10,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +let _vmcast = Constr.VMcast open Names open Pp open Pcoq @@ -17,18 +18,19 @@ open Ltac_plugin open Genarg open Stdarg open Tacarg -open Term open Libnames open Tactics open Tacmach open Util +open Locus open Tacexpr open Tacinterp open Pltac open Extraargs open Ppconstr -open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -64,7 +66,7 @@ DECLARE PLUGIN "ssreflect_plugin" * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_term.E) +let tacltop = (5,Notation_gram.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg @@ -301,24 +303,24 @@ END let pr_index = function - | Misctypes.ArgVar {CAst.v=id} -> pr_id id - | Misctypes.ArgArg n when n > 0 -> int n + | ArgVar {CAst.v=id} -> pr_id id + | ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index -let noindex = Misctypes.ArgArg 0 +let noindex = ArgArg 0 let check_index ?loc i = if i > 0 then i else CErrors.user_err ?loc (str"Index not positive") let mk_index ?loc = function - | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i) + | ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with - | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar id -> + | ArgArg _ -> idx + | ArgVar id -> let i = try let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in @@ -336,7 +338,7 @@ let interp_index ist gl idx = | None -> raise Not_found end end with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) + ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -410,8 +412,8 @@ let pr_docc = function let pr_ssrdocc _ _ _ = pr_docc ARGUMENT EXTEND ssrdocc TYPED AS ssrclear option * ssrocc PRINTED BY pr_ssrdocc -| [ "{" ne_ssrhyp_list(clr) "}" ] -> [ mkclr clr ] | [ "{" ssrocc(occ) "}" ] -> [ mkocc occ ] +| [ "{" ssrhyp_list(clr) "}" ] -> [ mkclr clr ] END (* Old kinds of terms *) @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -574,9 +576,9 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l) | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) + | IPatDispatch (s,iorpat) -> IPatDispatch (s,List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView v -> IPatView (List.map map_ast_closure_term v) + | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat @@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -641,12 +641,12 @@ let interp_ipat ist gl = check_hyps_uniq [] clr'; IPatClear clr' | IPatCase(iorpat) -> IPatCase(List.map (List.map interp) iorpat) - | IPatDispatch(iorpat) -> - IPatDispatch(List.map (List.map interp) iorpat) + | IPatDispatch(s,iorpat) -> + IPatDispatch(s,List.map (List.map interp) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x | IPatTac _ -> assert false (*internal usage only *) @@ -683,11 +683,17 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats (* TODO | [ "+" ] -> [ [IPatAnon Temporary] ] *) | [ ssrsimpl_ne(sim) ] -> [ [IPatSimpl sim] ] | [ ssrdocc(occ) "->" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, L2R)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)]] | [ ssrdocc(occ) "<-" ] -> [ match occ with + | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)]] + | [ ssrdocc(occ) ssrfwdview(v) ] -> [ match occ with + | Some [], _ -> [IPatView (true,v)] + | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] + | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") ] | [ ssrdocc(occ) ] -> [ match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here")] @@ -705,7 +711,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY pr_ssripats | [ "-/" integer(n) "/=" ] -> [ [IPatNoop;IPatSimpl(SimplCut (n,~-1))] ] | [ "-/" integer(n) "/" integer (m) "=" ] -> [ [IPatNoop;IPatSimpl(SimplCut(n,m))] ] - | [ ssrfwdview(v) ] -> [ [IPatView v] ] + | [ ssrfwdview(v) ] -> [ [IPatView (false,v)] ] | [ "[" ":" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] | [ "[:" ident_list(idl) "]" ] -> [ [IPatAbstractVars idl] ] END @@ -956,6 +962,7 @@ END (* the default simpl and unfold tactics would erase blindly. *) open Ssrmatching_plugin.Ssrmatching +open Ssrmatching_plugin.G_ssrmatching let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id @@ -1064,7 +1071,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> @@ -1093,7 +1100,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1154,7 +1161,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1210,8 +1218,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function @@ -1246,7 +1254,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") @@ -1399,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ @@ -1676,7 +1685,10 @@ let pr_gen (docc, dt) = pr_docc docc ++ pr_cpattern dt let pr_ssrgen _ _ _ = pr_gen ARGUMENT EXTEND ssrgen TYPED AS ssrdocc * cpattern PRINTED BY pr_ssrgen -| [ ssrdocc(docc) cpattern(dt) ] -> [ docc, dt ] +| [ ssrdocc(docc) cpattern(dt) ] -> [ + match docc with + | Some [], _ -> CErrors.user_err ~loc (str"Clear flag {} not allowed here") + | _ -> docc, dt ] | [ cpattern(dt) ] -> [ nodocc, dt ] END @@ -1938,7 +1950,7 @@ END let vmexacttac pf = Goal.nf_enter begin fun gl -> - exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl)) + exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end TACTIC EXTEND ssrexact -- cgit v1.2.3