diff options
Diffstat (limited to 'plugins/ssr')
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 8 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 60 | ||||
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 24 |
3 files changed, 48 insertions, 44 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 499154d50..4ae746288 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -268,7 +268,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl (loc, id) in + let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' @@ -835,9 +835,9 @@ let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t) + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ - CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t) + CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] @@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function | CProdN (abs, t) -> - n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs)); + n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs)); CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 211cad3f5..0d8044f19 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id @@ -316,7 +316,7 @@ END let pr_index = function - | Misctypes.ArgVar (_, id) -> pr_id id + | Misctypes.ArgVar {CAst.v=id} -> pr_id id | Misctypes.ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index @@ -330,13 +330,13 @@ let mk_index ?loc = function | iv -> iv let interp_index ist gl idx = - Tacmach.project gl, + Tacmach.project gl, match idx with | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar (loc, id) -> + | Misctypes.ArgVar id -> let i = try - let v = Id.Map.find id ist.Tacinterp.lfun in + let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in begin match Tacinterp.Value.to_int v with | Some i -> i | None -> @@ -350,8 +350,8 @@ let interp_index ist gl idx = end | None -> raise Not_found end end - with _ -> CErrors.user_err ?loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc i) + with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in + Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -1014,22 +1014,22 @@ let rec mkBstruct i = function | [] -> [] let rec format_local_binders h0 bl0 = match h0, bl0 with - | BFvar :: h, CLocalAssum ([_, x], _, _) :: bl -> + | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _) :: bl -> Bvar x :: format_local_binders h bl | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl -> - Bdecl (List.map snd lxs, t) :: format_local_binders h bl - | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl + | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl -> Bdef (x, oty, v) :: format_local_binders h bl | _ -> [] let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } -> + | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } -> let bs, c' = format_constr_expr h c in - Bdecl (List.map snd lxs, t) :: bs, c' - | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c' + | 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) } -> @@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> let bs = format_local_binders h bl in - let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in + let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } -> format_local_binders h bl @ (if has_cast then [Bcast t] else []), c @@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id - | { loc = loc } -> Loc.tag ?loc Anonymous + | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id + | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ")" ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> @@ -1191,7 +1191,7 @@ GEXTEND Gram [ ["of" | "&"]; c = operconstr LEVEL "99" -> let loc = !@loc in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] ]; END @@ -1250,13 +1250,13 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id + | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] -> - [ let (_, id) as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd let lb = fix_binders bs in let has_struct, i = let rec loop = function - (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id') - | [l', Name id'] when sid = None -> false, (l', id') + | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') -> + true, CAst.make ?loc:l' id' + | [{CAst.loc=l';v=Name id'}] when sid = None -> + false, CAst.make ?loc:l' id' | _ :: bn -> loop bn | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in @@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] -> - [ let _, id as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1323,7 +1325,7 @@ END let intro_id_to_binder = List.map (function | IPatId id -> - let xloc, _ as x = bvar_lname (mkCVar id) in + let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], mkCHole None) @@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> - List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids - | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id] - | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One] + List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids + | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id] + | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One] | _ -> anomaly "ssrbinder is not a binder")) let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = @@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ - [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id) + [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id) | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n) ] ]; ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]]; diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 25d1472f1..8e6e0347f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -79,9 +79,9 @@ let aliasvar = function let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in let mk_rtype t = Some t in -let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in +let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in let mk_let ?loc rt ct mp c1 = - CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in + CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; @@ -94,14 +94,16 @@ GEXTEND Gram ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; + ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in - let b1, b2 = - let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in + let b1, b2 = let open CAst in + let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in + (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) + in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1 @@ -118,7 +120,7 @@ GEXTEND Gram GLOBAL: closed_binder; closed_binder: [ [ ["of" | "&"]; c = operconstr LEVEL "99" -> - [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)] + [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)] ] ]; END (* }}} *) @@ -553,7 +555,7 @@ GEXTEND Gram let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag (Name s)),None), d) + ((CAst.make (Name s)),None), d) ]]; END @@ -584,10 +586,10 @@ END GEXTEND Gram GLOBAL: hloc; hloc: [ - [ "in"; "("; "Type"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypTypeOnly) - | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypValueOnly) + [ "in"; "("; "Type"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly) + | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly) ] ]; END |