aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-13 13:18:10 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-13 13:18:54 +0100
commitd868820ad1f00b896c5f44f18678fac2f8e0f720 (patch)
tree2312a62d9fd275d1c70b5e4fabcbe308826d5a05 /interp
parent7478ad7cc600753ba2609254657c87cacc27e8fc (diff)
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml2
-rw-r--r--interp/constrextern.ml18
-rw-r--r--interp/constrintern.ml13
-rw-r--r--interp/topconstr.ml2
4 files changed, 17 insertions, 18 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9c577034e..c5730e626 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
eq_reference c1 c2 &&
- List.equal cases_pattern_expr_eq a1 a2 &&
+ Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(_,r1), CPatAtom(_,r2) ->
Option.equal eq_reference r1 r2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2da8e0f6f..49892bec4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -266,7 +266,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args =
let mkPat loc qid l =
(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
- if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
+ if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -286,7 +286,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+ CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
| _ ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -329,13 +329,13 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
if !Topconstr.asymmetric_patterns then
if pattern_printable_in_both_syntax cstrsp
- then CPatCstr (loc, c, [], args)
- else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+ then CPatCstr (loc, c, None, args)
+ else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
else
let full_args = add_patt_for_params (fst cstrsp) args in
match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
- |Some true_args -> CPatCstr (loc, c, [], true_args)
- |None -> CPatCstr (loc, c, full_args, [])
+ |Some true_args -> CPatCstr (loc, c, None, true_args)
+ |None -> CPatCstr (loc, c, Some full_args, [])
in insert_pat_alias loc p na
and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
(tmp_scope, scopes as allscopes) vars =
@@ -413,7 +413,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
let c = extern_reference Loc.ghost vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
+ CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
else
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -431,8 +431,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
let c = extern_reference Loc.ghost vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
match drop_implicits_in_patt (IndRef ind) 0 args with
- |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args)
- |None -> CPatCstr (Loc.ghost, c, args, [])
+ |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
+ |None -> CPatCstr (Loc.ghost, c, Some args, [])
let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (None,[]) vars p
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f46217dec..b62df8dff 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1095,7 +1095,7 @@ let drop_notations_pattern looked_for =
let (loc,qid) = qualid_of_reference re in
try
match locate_extended qid with
- |SynDef sp ->
+ | SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
| NRef g ->
@@ -1118,7 +1118,7 @@ let drop_notations_pattern looked_for =
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2)
| _ -> raise Not_found)
- |TrueGlobal g ->
+ | TrueGlobal g ->
test_kind top g;
Dumpglob.add_glob loc g;
let (_,argscs) = find_remaining_scopes [] pats g in
@@ -1140,16 +1140,15 @@ let drop_notations_pattern looked_for =
|Some (a,b,c) -> RCPatCstr(loc, a, b, c)
|None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, head, [], pl) ->
+ | CPatCstr (loc, head, None, pl) ->
begin
match drop_syndef top env head pl with
| Some (a,b,c) -> RCPatCstr(loc, a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, r, expl_pl, pl) ->
- let g = try
- (locate (snd (qualid_of_reference r)))
- with Not_found ->
+ | CPatCstr (loc, r, Some expl_pl, pl) ->
+ let g = try locate (snd (qualid_of_reference r))
+ with Not_found ->
raise (InternalizationError (loc,NotAConstructor r)) in
let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in
RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cde72fd93..e569f543b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -52,7 +52,7 @@ let rec cases_pattern_fold_names f a = function
List.fold_left (cases_pattern_fold_names f) a patl
| CPatCstr (_,_,patl1,patl2) ->
List.fold_left (cases_pattern_fold_names f)
- (List.fold_left (cases_pattern_fold_names f) a patl1) patl2
+ (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
| CPatNotation (_,_,(patl,patll),patl') ->
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'