diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 99 |
1 files changed, 59 insertions, 40 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3a0c6648cf..44aacd62d8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -407,6 +407,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 @@ -441,27 +471,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 @@ -477,7 +489,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) -> @@ -500,10 +512,14 @@ 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 + 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 @@ -520,10 +536,14 @@ 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 + 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 @@ -746,7 +766,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 -> @@ -766,8 +786,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 @@ -1211,24 +1233,21 @@ 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 - | None when nallargs > 0 -> + 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 | 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 - | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = |