From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Aug 2017 19:05:57 +0200 Subject: Making detyping potentially lazy. The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. --- interp/constrextern.ml | 95 +++++++++++++++++++++++++++++++------------------- 1 file changed, 59 insertions(+), 36 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e85415bed..f5eff693f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -298,7 +298,7 @@ let add_patt_for_params ind l = let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -376,6 +376,10 @@ 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 lift f c = + let loc = c.CAst.loc in + CAst.make ?loc (f ?loc (DAst.get c)) + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try @@ -392,7 +396,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> - CAst.map_with_loc (fun ?loc -> function + lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> @@ -482,7 +486,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in - match t.v with + match DAst.get t with | PatCstr (cstr,_,na) -> let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in @@ -645,8 +649,12 @@ let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in List.map map args -let match_coercion_app = function - | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args) +let match_coercion_app c = match DAst.get c with + | GApp (r, args) -> + begin match DAst.get r with + | GRef (r,_) -> Some (c.CAst.loc, r, 0, args) + | _ -> None + end | _ -> None let rec remove_coercions inctx c = @@ -668,14 +676,20 @@ let rec remove_coercions inctx c = been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if List.is_empty l then a' else CAst.make ?loc @@ GApp (a',l) + if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l) | _ -> c with Not_found -> c) | _ -> c -let rec flatten_application = function - | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l)) - | a -> a +let rec flatten_application c = match DAst.get c with + | GApp (f, l) -> + begin match DAst.get f with + | GApp(a,l') -> + let loc = c.CAst.loc in + flatten_application (DAst.make ?loc @@ GApp (a,l'@l)) + | _ -> c + end + | a -> c (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) @@ -702,10 +716,12 @@ let extern_optimal_prim_token scopes r r' = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) - | (p,bk,Some x, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None) - | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t) + | (p,bk,Some x, t) -> + match DAst.get t with + | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | _ -> GLocalDef (p,bk,x,Some t) -let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u) +let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -730,7 +746,7 @@ let rec extern inctx scopes vars r = let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation scopes vars r'' (uninterp_notations r'') - with No_match -> CAst.map_with_loc (fun ?loc -> function + with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference ?loc vars ref) (extern_universes us) @@ -749,8 +765,9 @@ let rec extern inctx scopes vars r = | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) | GApp (f,args) -> - (match f with - | {loc = rloc; v = GRef (ref,us) } -> + (match DAst.get f with + | GRef (ref,us) -> + let rloc = f.CAst.loc in let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes (snd scopes) in begin @@ -825,8 +842,8 @@ let rec extern inctx scopes vars r = (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> - let na' = match na,tm with - | Anonymous, { v = GVar id } -> + let na' = match na, DAst.get tm with + | Anonymous, GVar id -> begin match rtntypopt with | None -> None | Some ntn -> @@ -835,12 +852,12 @@ let rec extern inctx scopes vars r = else None end | Anonymous, _ -> None - | Name id, { v = GVar id' } when Id.equal id id' -> None + | Name id, GVar id' when Id.equal id id' -> None | Name _, _ -> Some (Loc.tag na) in (sub_extern false scopes vars tm, na', Option.map (fun (loc,(ind,nal)) -> - let args = List.map (fun x -> CAst.make @@ PatVar x) nal in + let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) @@ -931,14 +948,16 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | { v = GLocalDef (na,bk,bd,ty)}::l -> + | b :: l -> + match DAst.get b with + | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) - | { v = GLocalAssum (na,bk,ty)}::l -> + | GLocalAssum (na,bk,ty) -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) @@ -951,7 +970,7 @@ and extern_local_binder scopes vars = function (na::assums,na::ids, CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) - | { v = GLocalPattern ((p,_),_,bk,ty)}::l -> + | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in @@ -969,12 +988,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function try if is_inactive_rule keyrule then raise No_match; (* Adjusts to the number of arguments expected by the notation *) - let (t,args,argsscopes,argsimpls) = match t.v ,n with + let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with | GApp (f,args), Some n when List.length args >= n -> let args1, args2 = List.chop n args in let subscopes, impls = - match f.v with + match DAst.get f with | GRef (ref,us) -> let subscopes = try List.skipn n (find_arguments_scope ref) @@ -987,15 +1006,19 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)), + (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), args2, subscopes, impls - | GApp ({ v = GRef (ref,us) } as f, args), None -> + | GApp (f, args), None -> + begin match DAst.get f with + | GRef (ref,us) -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef (ref,us), Some 0 -> CAst.make @@ GApp (t,[]), [], [], [] + | _ -> t, [], [], [] + end + | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -1065,7 +1088,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in + let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in extern false (scopt,[]) vars r @@ -1077,7 +1100,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = let extern_type goal_concl_style env sigma t = let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype goal_concl_style avoid env sigma t in + let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) @@ -1095,9 +1118,9 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) -let rec glob_of_pat env sigma pat = CAst.make @@ match pat with +let rec glob_of_pat env sigma pat = DAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1117,12 +1140,12 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) - | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), + | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), + GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) @@ -1154,15 +1177,15 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) - | PCoFix c -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))).v + | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) + | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) | PSort s -> GSort s let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = - let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in + let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (None,[]) vars a) -- cgit v1.2.3