From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Aug 2017 19:05:57 +0200 Subject: Making detyping potentially lazy. The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. --- plugins/ssrmatching/ssrmatching.ml4 | 62 ++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 25 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f6300ab7e..2e5522b83 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -134,6 +134,10 @@ let dC t = CastConv t let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> CErrors.anomaly (str"not a CRef.") +let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false +let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) + | _ -> CErrors.anomaly (str "not a GLambda") +let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) @@ -141,10 +145,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 = 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) +let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -980,11 +984,10 @@ let pr_rpattern = pr_pattern 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 - | _,({ v = GRef (VarRef x, _)} ,None) -> Some x +let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with + | _, Some { v = CRef (Ident (_, x), _) } -> Some x + | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x + | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1082,10 +1085,11 @@ 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 - | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) - | { v = GVar id } + try match DAst.get (pf_intern_term ist gl t) with + | GCast(t,CastConv c) when isGHole t && isGLambda c-> + let (x, c) = destGLambda c in + f x (' ',(c,None)) + | GVar id when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1126,19 +1130,27 @@ 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) = let open CAst in match red with - | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) - when let id = Id.to_string id in let len = String.length id in + let red = let rec decode_red (ist,red) = match red with + | T(k,(t,None)) -> + begin match DAst.get t with + | GCast (c,CastConv t) + when isGHole c && + let (id, t) = destGLambda t in + let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> + let (id, t) = destGLambda t in let id = Id.to_string id in let len = String.length id in - (match String.sub id 8 (len - 8), t with - | "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]) } -> + (match String.sub id 8 (len - 8), DAst.get 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]) -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) + | _ -> + decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x) + end | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) @@ -1163,7 +1175,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,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in + | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.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 @@ -1336,10 +1348,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 = ' ', (CAst.make @@ GRef (VarRef id, None), None) +let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef id, None), None) -let is_wildcard : cpattern -> bool = function - | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true +let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with + | _, Some { CAst.v = CHole _ } | GHole _, None -> true | _ -> false (* "ssrpattern" *) -- cgit v1.2.3