From 6aa58955515dff338ea85d59073dfc0d0c7648ab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 15:41:11 +0200 Subject: Move type_scope into user space, fix some output logs --- interp/constrintern.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8c56d0ccfe..d572508a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -298,7 +298,7 @@ let set_var_scope loc id istermvar env ntnvars = (* Not in a notation *) () -let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} +let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()} let reset_tmp_scope env = {env with tmp_scope = None} @@ -449,12 +449,15 @@ let intern_generalization intern env lvar loc bk ak c = | Some AbsPi -> true | Some _ -> false | None -> - let is_type_scope = match env.tmp_scope with + match Notation.current_type_scope_name () with + | Some type_scope -> + let is_type_scope = match env.tmp_scope with + | None -> false + | Some sc -> String.equal sc type_scope + in + is_type_scope || + String.List.mem type_scope env.scopes | None -> false - | Some sc -> String.equal sc Notation.type_scope - in - is_type_scope || - String.List.mem Notation.type_scope env.scopes in if pi then (fun (id, loc') acc -> @@ -1755,7 +1758,7 @@ let extract_ids env = Id.Set.empty let scope_of_type_kind = function - | IsType -> Some Notation.type_scope + | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None -- cgit v1.2.3 From 6af9f644b64acf485c1628247f5435d09b990b79 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 16 Sep 2015 06:41:04 +0200 Subject: Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #4268) --- interp/constrintern.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ecaf2b8c13..c754f1910c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in begin match sorted_fields with | None -> RCPatAtom (loc, None) - | Some (_, head, pl) -> + | Some (n, head, pl) -> + let pl = + if !oldfashion_patterns then pl else + let pars = List.make n (CPatAtom (loc, None)) in + List.rev_append pars pl in match drop_syndef top env head pl with |Some (a,b,c) -> RCPatCstr(loc, a, b, c) |None -> raise (InternalizationError (loc,NotAConstructor head)) -- cgit v1.2.3 From 701a69732ef2abfc7384296e090a3e9bd7604bbd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 Nov 2015 18:45:32 +0100 Subject: Fixing bug #3554: Anomaly: Anonymous implicit argument. We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c754f1910c..8afe630ec5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -317,7 +317,7 @@ let rec it_mkGLambda loc2 env body = let build_impls = function |Implicit -> (function |Name id -> Some (id, Impargs.Manual, (true,true)) - |Anonymous -> anomaly (Pp.str "Anonymous implicit argument")) + |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true))) |Explicit -> fun _ -> None let impls_type_list ?(args = []) = -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- interp/constrintern.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8afe630ec5..8a86d30220 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1506,7 +1506,7 @@ let internalize globalenv env allow_patvar lvar c = intern env app end | CCases (loc, sty, rtnpo, tms, eqns) -> - let as_in_vars = List.fold_left (fun acc (_,(na,inb)) -> + let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x) (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na) inb) Id.Set.empty tms in @@ -1542,7 +1542,7 @@ let internalize globalenv env allow_patvar lvar c = | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in (* "in" is None so no match to add *) - let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in + let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.ghost,na') in @@ -1551,7 +1551,7 @@ let internalize globalenv env allow_patvar lvar c = intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in - let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *) + let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.ghost,na') in @@ -1628,7 +1628,7 @@ let internalize globalenv env allow_patvar lvar c = let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll - and intern_case_item env forbidden_names_for_gen (tm,(na,t)) = + and intern_case_item env forbidden_names_for_gen (tm,na,t) = (*the "match" part *) let tm' = intern env tm in (* the "as" part *) -- cgit v1.2.3 From 1a157442dff4bfa127af467c49280e79889acde7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 26 Dec 2015 10:07:19 +0100 Subject: Do not compose List.length with List.filter. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d30220..d4cb797759 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1386,7 +1386,7 @@ let internalize globalenv env allow_patvar lvar c = let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in + let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- interp/constrintern.ml | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d4cb797759..f9de8c4663 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -698,19 +698,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = (* [id] a goal variable *) GVar (loc,id), [], [], [] -let proj_impls r impls = - let env = Global.env () in - let f (x, l) = x, projection_implicits env r l in - List.map f impls - -let proj_scopes n scopes = - List.skipn_at_least n scopes - -let proj_impls_scopes p impls scopes = - match p with - | Some (r, n) -> proj_impls r impls, proj_scopes n scopes - | None -> impls, scopes - let find_appl_head_data c = match c with | GRef (loc,ref,_) as x -> -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- interp/constrintern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d30220..918b75b0c1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -101,7 +101,7 @@ let global_reference id = let construct_reference ctx id = try - Term.mkVar (let _ = Context.lookup_named id ctx in id) + Term.mkVar (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id @@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) - let _ = Context.lookup_named id namedctx in + let _ = Context.Named.lookup id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68bc0b1092..c0203b0666 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1479,7 +1479,7 @@ let internalize globalenv env allow_patvar lvar c = apply_impargs c env impargs args_scopes (merge_impargs l args) loc - | CRecord (loc, _, fs) -> + | CRecord (loc, fs) -> let cargs = sort_fields true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8afe630ec5..a7b1bb4128 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- interp/constrintern.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 964ed05140..70802d5cba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -29,6 +29,7 @@ open Nametab open Notation open Inductiveops open Decl_kinds +open Context.Rel.Declaration (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -1645,14 +1646,14 @@ let internalize globalenv env allow_patvar lvar c = |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) - |(_,Some _,_)::t, l when not with_letin -> + | LocalDef _ :: t, l when not with_letin -> canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc) |[],[] -> (add_name match_acc na, var_acc) |_::t,PatVar (loc,x)::tt -> canonize_args t tt forbidden_names (add_name match_acc (loc,x)) ((loc,x)::var_acc) - |(cano_name,_,ty)::t,c::tt -> + | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in canonize_args t tt (fresh::forbidden_names) @@ -1894,7 +1895,7 @@ let interp_rawcontext_evars env evdref k bl = let t' = locate_if_hole (loc_of_glob_constr t) na t in let t = understand_tcc_evars env evdref ~expected_type:IsType t' in - let d = (na,None,t) in + let d = LocalAssum (na,t) in let impls = if k == Implicit then let na = match na with Name n -> Some n | Anonymous -> None in @@ -1904,7 +1905,7 @@ let interp_rawcontext_evars env evdref k bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment_tcc env evdref b in - let d = (na, Some c.uj_val, c.uj_type) in + let d = LocalDef (na, c.uj_val, c.uj_type) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls -- cgit v1.2.3 From 4d25b224b91959b85fcd68c825a307ec684f0bac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 28 Feb 2016 18:28:14 +0100 Subject: Printing notations: Cleaning in anticipation of fixing #4592. - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env. --- interp/constrintern.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 70802d5cba..36f88fc3cc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -275,7 +275,8 @@ let error_expect_binder_notation_type loc id = let set_var_scope loc id istermvar env ntnvars = try - let idscopes,typ = Id.Map.find id ntnvars in + let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in + if istermvar then isonlybinding := false; let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) begin match !idscopes with @@ -629,7 +630,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> match typ with - | NtnTypeConstr -> ((x,scl)::l1,l2,l3) + | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3) | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) @@ -1845,7 +1846,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let interp_notation_constr ?(impls=empty_internalization_env) nenv a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in @@ -1854,7 +1855,8 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a = (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in - let vars = Id.Map.map (fun (sc, typ) -> (out_scope !sc, typ)) vl in + let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> + (!isonlybinding, out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a -- cgit v1.2.3 From 7478ad7cc600753ba2609254657c87cacc27e8fc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Mar 2016 08:03:05 +0100 Subject: A more explicit name to the asymmetric boolean flag. --- interp/constrintern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 36f88fc3cc..f46217dec6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1133,7 +1133,7 @@ let drop_notations_pattern looked_for = | None -> RCPatAtom (loc, None) | Some (n, head, pl) -> let pl = - if !oldfashion_patterns then pl else + if !asymmetric_patterns then pl else let pars = List.make n (CPatAtom (loc, None)) in List.rev_append pars pl in match drop_syndef top env head pl with @@ -1238,7 +1238,7 @@ let rec intern_pat genv aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv aliases' p | RCPatCstr (loc, head, expl_pl, pl) -> - if !oldfashion_patterns then + if !asymmetric_patterns then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- interp/constrintern.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f46217dec6..b62df8dfff 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) -- cgit v1.2.3 From 3366f05ab09aa90dcc96d7432bff09617162c3e4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 17:49:25 +0100 Subject: Adopting the same rules for interpreting @, abbreviations and notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable). --- interp/constrintern.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b62df8dfff..fa38695705 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -918,7 +918,7 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = - let cstr = match ref with + let (ind,_ as cstr) = match ref with | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in @@ -927,15 +927,15 @@ let find_constructor loc add_params ref = let error = str "This reference is not a constructor." in user_err_loc (loc, "find_constructor", error) in - cstr, (function (ind,_ as c) -> match add_params with - |Some nb_args -> + cstr, match add_params with + | Some nb_args -> let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls c) + if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))]) - |None -> []) cstr + | None -> [] let find_pattern_variable = function | Ident (loc,id) -> id @@ -1099,16 +1099,17 @@ let drop_notations_pattern looked_for = let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with | NRef g -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc env) argscs pats) - | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) test_kind top g; let () = assert (List.is_empty vars) in - let (argscs,_) = find_remaining_scopes pats [] g in - Some (g, List.map2 (in_pat_sc env) argscs pats, []) + Some (g, List.map (in_pat false env) pats, []) | NApp (NRef g,args) -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; @@ -1146,12 +1147,18 @@ let drop_notations_pattern looked_for = | Some (a,b,c) -> RCPatCstr(loc, a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, Some expl_pl, pl) -> + | 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) + if expl_pl == [] then + (* Convention: (@r) deactivates all further implicit arguments and scopes *) + RCPatCstr (loc, g, List.map (in_pat false env) pl, []) + else + (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) + (* but not scopes in expl_pl *) + let (argscs1,_) = find_remaining_scopes expl_pl pl g in + RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl @ List.map (in_pat false env) pl, []) | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) when Bigint.is_strictly_pos p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) @@ -1203,8 +1210,8 @@ let drop_notations_pattern looked_for = ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl, - List.map2 (in_pat_sc env) argscs2 args) + List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl @ + List.map (in_pat false env) args, []) | NList (x,_,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); -- cgit v1.2.3