From d6467c2fea8a29634ca649850784c95ed5b9d4f4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 13:17:12 +0100 Subject: Fixing anomaly from #11091 (incompatible printing with notation and imp. args). We fix also an index error in deciding when to explicit print a non-inferable implicit argument. --- interp/constrextern.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 38dc10a9b3..82ba559406 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -742,7 +742,7 @@ let extern_applied_ref inctx impl (cf,f) us args = let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = try let syndefargs = List.map (fun a -> (a,None)) syndefargs in - let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in + let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in let args = syndefargs @ extraargs in if args = [] then cf else CApp ((None, CAst.make cf), args) with Expl -> @@ -762,8 +762,10 @@ let extern_applied_notation n impl f args = if List.is_empty args then f.CAst.v else - let args = adjust_implicit_arguments false (List.length args) 1 args impl in + try + let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in mkFlattenedCApp (f,args) + with Expl -> raise No_match let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in -- cgit v1.2.3 From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 07:19:27 +0100 Subject: Fixing a notation printing bug (missing a @ to reflect absence of imp. args). When a non-applied reference was matching a notation to the same reference, implicit arguments were lost. --- interp/constrextern.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 82ba559406..5098b2a00c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1216,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), args2, args2scopes, args2impls - | None when nallargs > 0 -> + | None -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] @@ -1226,7 +1226,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules = | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] | _ -> t, [], [], [] end - | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = -- cgit v1.2.3 From 67e16fdeef26455d0afa357e31de8f7b3f772034 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 07:30:05 +0100 Subject: Fixing printing of notations bound to an expression of the form "@f". The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[]) encoding of @f was lost. It remains to let printing match parsing wrt the deactivation of implicit arguments and argument scopes in such case. See next commit. --- interp/constrextern.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5098b2a00c..681d6ba541 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1209,23 +1209,17 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n && nallargs > 0 -> + | Some n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in let args2impls = try List.skipn n argsimpls with Failure _ -> [] in (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) - (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), - args2, args2scopes, args2impls + DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls | None -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | Some 0 when nallargs = 0 -> - begin match DAst.get f with - | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] - | _ -> t, [], [], [] - end | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = -- cgit v1.2.3 From 556e9dde62b6822db20bd5c7e6e6a67bc717c408 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 07:31:37 +0100 Subject: Deactivate implicit arguments in printing notations bound to "@f". This is to match the parsing policy (see #11091). In particular, we deactivate also argument scopes, consistently with what is done at parsing time. --- interp/constrextern.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 681d6ba541..362fe83ffa 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1211,9 +1211,14 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let (t,args,argsscopes,argsimpls) = match n with | Some n when nallargs >= n -> let args1, args2 = List.chop n args in - let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in - let args2impls = try List.skipn n argsimpls with Failure _ -> [] in - (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) + let args2scopes = + if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in + let args2impls = + if n = 0 then + (* Note: NApp(NRef f,[]), hence n=0, encodes @f and + conventionally deactivates implicit arguments *) + [] + else try List.skipn n argsimpls with Failure _ -> [] in DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls | None -> begin match DAst.get f with -- cgit v1.2.3 From 04b9870f0ebe79fde789551c8e172aad1e7cfc5c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 08:52:01 +0100 Subject: Inherit argument scopes in notations to expressions of the form @f. This is a change of semantics. --- interp/constrextern.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 362fe83ffa..7f5f03610b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1211,8 +1211,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let (t,args,argsscopes,argsimpls) = match n with | Some n when nallargs >= n -> let args1, args2 = List.chop n args in - let args2scopes = - if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in + let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in let args2impls = if n = 0 then (* Note: NApp(NRef f,[]), hence n=0, encodes @f and -- cgit v1.2.3 From ba52fd0dff4dcf06621fb91ff4902a060a0b222d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 11:36:51 +0100 Subject: Use auxiliary function for externing record patterns. Also apply the same conditions for printing constructors as record instances in both terms and patterns. --- interp/constrextern.ml | 54 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 33 insertions(+), 21 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7f5f03610b..c68a60fc93 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -403,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args) ) impl_st +let extern_record_pattern cstrsp args = + try + if !Flags.raw_print then raise Exit; + let projs = Recordops.lookup_projections (fst cstrsp) in + if PrintingRecord.active (fst cstrsp) then + () + else if PrintingConstructor.active (fst cstrsp) then + raise Exit + else if not (get_record_print ()) then + raise Exit; + let rec ip projs args acc = + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, { CAst.v = CPatAtom None } -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + let loc = pat.CAst.loc in + (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc + | _ -> raise No_match in + ip q tail acc + | _ -> assert false + in + Some (List.rev (ip projs args [])) + with + Not_found | No_match | Exit -> None + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try @@ -437,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in let p = - try - if !Flags.raw_print then raise Exit; - let projs = Recordops.lookup_projections (fst cstrsp) in - let rec ip projs args acc = - match projs, args with - | [], [] -> acc - | proj :: q, pat :: tail -> - let acc = - match proj, pat with - | _, { CAst.v = CPatAtom None } -> - (* we don't want to have 'x := _' in our patterns *) - acc - | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc) - | _ -> raise No_match in - ip q tail acc - | _ -> assert false - in - CPatRecord(List.rev (ip projs args [])) - with - Not_found | No_match | Exit -> + match extern_record_pattern cstrsp args with + | Some l -> CPatRecord l + | None -> let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp -- cgit v1.2.3 From 3eea1e383e23ea76fcd49a7b302f31b2e3f6ef2a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 12:14:37 +0100 Subject: Fix inheritance of argument scopes when printing notations in patterns. --- interp/constrextern.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c68a60fc93..008e84cd9c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -508,7 +508,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let subscope = (subentry,(scopt,scl@scopes')) in List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with @@ -528,7 +531,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in - let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in + let subscopes = find_arguments_scope gr in + let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in + let more_args = fill_arg_scopes more_args more_args_scopes allscopes in + let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with -- cgit v1.2.3 From 32467acf285629c28cbda27d27a8cf248150f2bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 12:44:44 +0100 Subject: Fix index bug in computing implicit signature of abbrev. in pattern printing. --- interp/constrextern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 008e84cd9c..b05ca8e5a6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -537,7 +537,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else - match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in -- cgit v1.2.3 From 9da7715108554a5105c012685e90b2fa563abf08 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 14 Nov 2019 13:41:00 +0100 Subject: In printing patterns, distinguish the case of a notation to @id. This is a case which conventionally deactivates implicit arguments. --- interp/constrextern.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b05ca8e5a6..4ec9f17c71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -485,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = in insert_pat_coercion coercion pat -and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) +and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args)) (custom, (tmp_scope, scopes) as allscopes) vars = function | NotationRule (_,ntn as specific_ntn) -> @@ -514,7 +514,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else - match drop_implicits_in_patt gr nb_to_drop l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in @@ -537,7 +538,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in let l2' = if Constrintern.get_asymmetric_patterns () then l2 else - match drop_implicits_in_patt gr nb_to_drop l2 with + if no_implicit then l2 else + match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args |None -> raise No_match in -- cgit v1.2.3