diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 18:32:02 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:05 +0100 |
commit | 398358618bb3eabfe822b79c669703c1c33b67e6 (patch) | |
tree | 967c18294374fe73a51d582cd120ab70eb856936 /interp/constrexpr_ops.ml | |
parent | e21f70cc2b284a3cf489b16e0251492fb864cf1e (diff) |
Adding patterns in the category of binders for notations.
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r-- | interp/constrexpr_ops.ml | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 9fe890e90..83add7a7c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -545,6 +545,45 @@ let coerce_to_name = function | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") +let mkAppPattern ?loc p lp = + let open CAst in + make ?loc @@ (match p.v with + | CPatAtom (Some r) -> CPatCstr (r, None, lp) + | CPatCstr (r, None, l2) -> + CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" + (Pp.str "Nested applications not supported.") + | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp) + | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp) + | _ -> CErrors.user_err + ?loc:p.loc ~hdr:"compound_pattern" + (Pp.str "Such pattern cannot have arguments.")) + +let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function + | CRef (r,None) -> + CPatAtom (Some r) + | CHole (None,Misctypes.IntroAnonymous,None) -> + CPatAtom None + | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> + CPatAlias (coerce_to_cases_pattern_expr b, id) + | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> + (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v + | CAppExpl ((None,r,i),args) -> + CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) + | CNotation (ntn,(c,cl,[])) -> + CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, + List.map (List.map coerce_to_cases_pattern_expr) cl),[]) + | CPrim p -> + CPatPrim p + | CRecord l -> + CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l) + | CDelimiters (s,p) -> + CPatDelimiters (s,coerce_to_cases_pattern_expr p) + | CCast (p,CastConv t) -> + CPatCast (coerce_to_cases_pattern_expr p,t) + | _ -> + CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" + (str "This expression should be coercible to a pattern.")) c + let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optdepr = false; |