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. --- plugins/funind/glob_term_to_relation.ml | 106 ++++++++++++++++++-------------- 1 file changed, 61 insertions(+), 45 deletions(-) (limited to 'plugins/funind/glob_term_to_relation.ml') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8cf5e8442..7087a195e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -34,10 +34,10 @@ type glob_context = (binder_type*glob_constr) list let rec solve_trivial_holes pat_as_term e = - match pat_as_term.CAst.v,e.CAst.v with + match DAst.get pat_as_term, DAst.get e with | GHole _,_ -> e | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> - CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) | _,_ -> pat_as_term (* @@ -361,7 +361,7 @@ let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); - match pat.CAst.v with + match DAst.get pat with | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = @@ -411,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = CAst.with_val (function +let rec pattern_to_term_and_type env typ = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar (Name id) -> mkGVar id @@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) + (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -480,7 +480,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); let open CAst in - match rt.v with + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid @@ -496,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f.v with + match DAst.get f with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> CAst.make @@ - match t.v with + | u::l -> DAst.make @@ + match DAst.get t with | GLambda(na,_,nat,b) -> GLetIn(na,u,None,aux b l) | _ -> @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in - let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in + let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -564,7 +564,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (CAst.make @@ GVar id) + (DAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -626,7 +626,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] + Detyping.detype Detyping.Now false [] env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ_as_constr = EConstr.of_constr typ_as_constr in - let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in + let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in (* removing trivial holes *) let pat_as_term = solve_trivial_holes pat_as_term e in @@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -875,15 +875,23 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve { brl'_res with result = this_branch_res@brl'_res.result } -let is_res id = - try +let is_res r = match DAst.get r with +| GVar id -> + begin try String.equal (String.sub (Id.to_string id) 0 4) "_res" - with Invalid_argument _ -> false + with Invalid_argument _ -> false end +| _ -> false +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false +let is_gvar c = match DAst.get c with +| GVar id -> true +| _ -> false let same_raw_term rt1 rt2 = - match CAst.(rt1.v, rt2.v) with + match DAst.get rt1, DAst.get rt2 with | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false @@ -917,23 +925,24 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); let open Context.Rel.Declaration in let open CAst in - match rt.v with + match DAst.get rt with | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin - match t with - | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> + match DAst.get t with + | GApp(res_rt ,args') when is_res res_rt -> begin - match args' with - | { v = GVar this_relname }::args' -> + let arg = List.hd args' in + match DAst.get arg with + | GVar this_relname -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) let new_t = - mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) + mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in @@ -948,9 +957,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty; id ;rt]) + when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> + let loc1 = rt.CAst.loc in + let loc2 = eq_as_ref.CAst.loc in + let loc3 = id.CAst.loc in + let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try observe (str "computing new type for eq : " ++ pr_glob_constr rt); @@ -985,10 +998,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = CAst.make @@ - GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), + let rt_typ = DAst.make @@ + GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype false [] + (fun p -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr p)) params)@(Array.to_list (Array.make @@ -996,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) + DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in @@ -1015,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype false [] + (id',Detyping.detype Detyping.Now false [] env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false [] env (Evd.from_env env) arg)::acc @@ -1065,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty;rt1;rt2]) + when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try @@ -1077,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1135,14 +1148,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here.") (* We have renamed all the anonymous functions during alpha_renaming phase *) end | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1158,7 +1171,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(nal,(na,rto),t,b) -> @@ -1184,7 +1197,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - CAst.make @@ GLetTuple(nal,(na,None),t,new_b), + DAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1210,12 +1223,15 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params gt = CAst.with_val (function +let rec compute_cst_params relnames params gt = DAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> - compute_cst_params_from_app [] (params,rtl) | GApp(f,args) -> + begin match DAst.get f with + | GVar relname' when Id.Set.mem relname' relnames -> + compute_cst_params_from_app [] (params,args) + | _ -> List.fold_left (compute_cst_params relnames) params (f::args) + end | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b @@ -1232,10 +1248,10 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = + let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' - when Id.compare id id' == 0 -> + | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -- cgit v1.2.3