diff options
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 33 |
1 files changed, 17 insertions, 16 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index c11c9f83b..9a0dfbf1c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -158,10 +158,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args) -let mkRCast rc rt = Loc.tag @@ GCast (rc, dC rt) -let mkRLambda n s t = Loc.tag @@ GLambda (n, Explicit, s, t) +let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) +let mkRCast rc rt = CAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -1022,7 +1022,7 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern let id_of_cpattern = let open CAst in function | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x - | _,((_, GRef (VarRef x, _)) ,None) -> Some x + | _,({ v = GRef (VarRef x, _)} ,None) -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1121,9 +1121,10 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let eAsXInT e x t = E_As_X_In_T(e,x,t) in let mkG ?(k=' ') x = k,(x,None) in let decode ist t ?reccall f g = + let open CAst in try match (pf_intern_term ist gl t) with - | _, GCast((_, GHole _),CastConv((_, GLambda(Name x,_,_,c)))) -> f x (' ',(c,None)) - | _, GVar id + | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) + | { v = GVar id } when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1164,18 +1165,18 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = match red with - | T(k,((_, GCast ((_, GHole _),CastConv((_, GLambda (Name id,_,_,t))))),None)) + let red = let rec decode_red (ist,red) = let open CAst in match red with + | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) when let id = string_of_id id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> let id = string_of_id id in let len = String.length id in (match String.sub id 8 (len - 8), t with - | "In", (_, GApp( _, [t])) -> decodeG t xInT (fun x -> T x) - | "In", (_, GApp( _, [e; t])) -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", (_, GApp( _, [e; t; e_in_t])) -> + | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) + | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", { v = GApp( _, [e; t; e_in_t]) } -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", (_, GApp(_, [e; t])) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT @@ -1201,7 +1202,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn ?loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ?loc) b)) - | None -> a,(Loc.tag ?loc @@ GLetIn (x, Loc.tag ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in + | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t @@ -1374,10 +1375,10 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef id, None), None) +let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef id, None), None) let is_wildcard : cpattern -> bool = function - | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true + | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true | _ -> false (* "ssrpattern" *) |