diff options
Diffstat (limited to 'plugins')
27 files changed, 395 insertions, 322 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 5a4c52456..fca7d9851 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = - let c = Detyping.detype ~lax:true false [] env sigma c in + let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) + Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); 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 diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 003bb4e30..02ee56ac5 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,36 +10,36 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = CAst.make @@ GRef(ref,None) -let mkGVar id = CAst.make @@ GVar(id) -let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) -let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) -let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = CAst.make @@ GSort(s) -let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) +let mkGRef ref = DAst.make @@ GRef(ref,None) +let mkGVar id = DAst.make @@ GVar(id) +let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = DAst.make @@ GSort(s) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = DAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) let glob_decompose_prod = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args c = match DAst.get c with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod [] let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args rt = match DAst.get rt with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,rt in glob_decompose_prod [] @@ -58,10 +58,10 @@ let glob_decompose_prod_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -70,12 +70,12 @@ let glob_decompose_prod_or_letin_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -83,10 +83,10 @@ let glob_decompose_prod_or_letin_n n = let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) - match rt with - | { CAst.v = GApp(rt,rtl) } -> + match DAst.get rt with + | GApp(rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt - | rt -> rt,List.rev acc + | _ -> rt,List.rev acc in decompose_rapp [] @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map_with_loc (fun ?loc -> function + DAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -191,15 +191,15 @@ let change_vars = let rec alpha_pat excluded pat = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty | PatCstr(constr,patl,na) -> @@ -219,7 +219,7 @@ let rec alpha_pat excluded pat = ([],new_excluded,map) patl in - (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -238,7 +238,7 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = let rec get_pattern_id pat = - match pat.CAst.v with + match DAst.get pat with | PatVar(Anonymous) -> assert false | PatVar(Name id) -> [id] @@ -257,8 +257,8 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let loc = rt.CAst.loc in - let new_rt = CAst.make ?loc @@ - match rt.CAst.v with + let new_rt = DAst.make ?loc @@ + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in @@ -377,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) = [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function + let rec is_free_in x = DAst.with_loc_val (fun ?loc -> function | GRef _ -> false | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false @@ -421,7 +421,7 @@ let is_free_in id = -let rec pattern_to_term pt = CAst.with_val (function +let rec pattern_to_term pt = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar(Name id) -> mkGVar id @@ -448,8 +448,8 @@ let rec pattern_to_term pt = CAst.with_val (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern x = CAst.map (function - | GVar id when Id.compare id x_id == 0 -> term.CAst.v + let rec replace_var_by_pattern x = DAst.map (function + | GVar id when Id.compare id x_id == 0 -> DAst.get term | GRef _ | GVar _ | GEvar _ @@ -522,11 +522,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -545,11 +544,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -569,7 +567,7 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = CAst.with_val (function + let rec ids_of_pat ids = DAst.with_val (function | PatVar Anonymous -> ids | PatVar(Name id) -> Id.Set.add id ids | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl @@ -583,9 +581,9 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc {loc; CAst.v = c} = + let rec ids_of_glob_constr acc c = let idof = id_of_name in - match c with + match DAst.get c with | GVar id -> id::acc | GApp (g,args) -> ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc @@ -610,7 +608,7 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term x = CAst.map (function + let rec zeta_normalize_term x = DAst.map (function | GRef _ | GVar _ | GEvar _ @@ -632,9 +630,9 @@ let zeta_normalize = zeta_normalize_term b ) | GLetIn(Name id,def,typ,b) -> - (zeta_normalize_term (replace_var_by_term id def b)).CAst.v + DAst.get (zeta_normalize_term (replace_var_by_term id def b)) | GLetIn(Anonymous,def,typ,b) -> - (zeta_normalize_term b).CAst.v + DAst.get (zeta_normalize_term b) | GLetTuple(nal,(na,rto),def,b) -> GLetTuple(nal, (na,Option.map zeta_normalize_term rto), @@ -670,19 +668,19 @@ let zeta_normalize = let expand_as = - let rec add_as map ({loc; CAst.v = pat } as rt) = - match pat with + let rec add_as map rt = + match DAst.get rt with | PatVar _ -> map | PatCstr(_,patl,Name id) -> Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map = CAst.map (function + let rec expand_as map = DAst.map (function | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt | GVar id as rt -> begin try - (Id.Map.find id map).CAst.v + DAst.get (Id.Map.find id map) with Not_found -> rt end | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) @@ -723,7 +721,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = - match rt.CAst.v with + match DAst.get rt with | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *) ( try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *) @@ -743,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -765,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8769f5668..dab094f91 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -191,7 +191,7 @@ let error msg = user_err Pp.(str msg) let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names gt = match gt.CAst.v with + let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f4f9ba2bb..5f4d514f3 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -66,7 +66,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -80,7 +80,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3ae922190..96200a98a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -64,8 +64,8 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = - match x with - | { CAst.v = GVar x } -> Id.equal x f + match DAst.get x with + | GVar x -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -491,38 +491,38 @@ exception NoMerge let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) + DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args) | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) + DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -533,16 +533,18 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let rec merge_rec_hyps shift accrec (ltyp:(Name.t * glob_constr option * glob_constr option) list) filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = + let is_app c = match DAst.get c with GApp _ -> true | _ -> false in let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) + | (nme,x,Some ind) when is_app ind -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in + let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in match ltyp with | [] -> [] - | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some t) :: lt when is_app t -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -553,12 +555,13 @@ let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = let find_app (nme:Id.t) ltyp = + let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in try ignore (List.map (fun x -> match x with - | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) + | _,None,Some c when is_app c -> raise (Found 0) | _ -> ()) ltyp); false @@ -617,7 +620,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1.CAst.v with + (match DAst.get t1 with | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> @@ -764,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in + Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -848,8 +851,8 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> let t = EConstr.of_constr t in - let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - CAst.make @@ GProd (nme,Explicit,traw,t2) + let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + DAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d3eccb58d..41a10cba3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -190,15 +190,15 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - CAst.make @@ + DAst.make @@ GCases (RegularStyle,None, - [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], + [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], - CAst.make @@ GVar v_id)]) + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b847aadf2..99e444010 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -626,19 +626,19 @@ END let subst_var_with_hole occ tid t = let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in - let rec substrec = function - | { CAst.v = GVar id } as x -> + let rec substrec x = match DAst.get x with + | GVar id -> if Id.equal id tid then (decr occref; if Int.equal !occref 0 then x else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x - | c -> map_glob_constr_left_to_right substrec c in + | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t in if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' @@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t = let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in - let rec substrec = function - | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> + let rec substrec c = match DAst.get c with + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; - CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) - | c -> map_glob_constr_left_to_right substrec c + | _ -> map_glob_constr_left_to_right substrec c in substrec t @@ -666,8 +666,8 @@ let hResolve id c occ t = let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in - let c_raw = Detyping.detype true env_ids env sigma c in - let t_raw = Detyping.detype true env_ids env sigma t in + let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in + let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = try Pretyping.understand env sigma t_hole diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c874f8d5a..c22e68323 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ END let clsubstitute o c = Proofview.Goal.enter begin fun gl -> - let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cb7d9b9c0..f4e3ba633 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty.CAst.v with + match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 0554d4364..fc6ee6aab 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -106,12 +106,12 @@ let intern_ltac_variable ist = function let intern_constr_reference strict ist = function | Ident (_,id) as r when not strict && find_hyp id ist -> - (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None)) | Ident (_,id) as r when find_var id ist -> - (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) + (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None)) | r -> let loc,_ as lqid = qualid_of_reference r in - CAst.make @@ GRef (locate_global_with_alias lqid,None), + DAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (CAst.make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) @@ -264,9 +264,10 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with - | {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id) - | c -> clear,ElimOnConstr (c,NoBindings) + let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in + match DAst.get c with + | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | _ -> clear,ElimOnConstr ((c, p), NoBindings) else clear,ElimOnIdent (loc,id) @@ -348,7 +349,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = ltac_extra = ist.extra; } in let c = Constrintern.interp_reference sign r in - match c.CAst.v with + match DAst.get c with | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2a1e2b682..8fa95ffb0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) = (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = - try match dest_fun x with - | { CAst.v = GVar id }, _ -> + try match DAst.get (fst (dest_fun x)) with + | GVar id -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0f996c65a..d0fe1f957 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -131,7 +131,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None)); + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index cc0e86684..c29a1fe7c 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -42,10 +42,10 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = | Some ghyps -> let clr' = snd (interp_hyps ist gl ghyps) @ clr in if k <> xNoFlag then clr', rcs' else - let open CAst in - match rc with - | { loc; v = GVar id } when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' - | { loc; v = GRef (VarRef id, _) } when not_section_id id -> + let loc = rc.CAst.loc in + match DAst.get rc with + | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' + | GRef (VarRef id, _) when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' @@ -68,9 +68,8 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) - let open CAst in - let n = match ist, t with - | None, { v = GVar id | GRef (VarRef id,_) } -> pf_nbargs gl (EConstr.mkVar id) + let n = match ist, DAst.get t with + | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 799e969ae..cf5fdf318 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -176,24 +176,26 @@ open Globnames open Misctypes open Decl_kinds -let mkRHole = CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] -let rec isRHoles = function { CAst.v = GHole _ } :: cl -> isRHoles cl | cl -> cl = [] -let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) -let mkRVar id = CAst.make @@ GRef (VarRef id,None) -let mkRltacVar id = CAst.make @@ GVar (id) -let mkRCast rc rt = CAst.make @@ GCast (rc, CastConv rt) -let mkRType = CAst.make @@ GSort (GType []) -let mkRProp = CAst.make @@ GSort (GProp) -let mkRArrow rt1 rt2 = CAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) -let mkRConstruct c = CAst.make @@ GRef (ConstructRef c,None) -let mkRInd mind = CAst.make @@ GRef (IndRef mind,None) -let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) +let rec isRHoles cl = match cl with +| [] -> true +| c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRVar id = DAst.make @@ GRef (VarRef id,None) +let mkRltacVar id = DAst.make @@ GVar (id) +let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) +let mkRType = DAst.make @@ GSort (GType []) +let mkRProp = DAst.make @@ GSort (GProp) +let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) +let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) +let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let rec mkRnat n = - if n <= 0 then CAst.make @@ GRef (Coqlib.glob_O, None) else - mkRApp (CAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] + if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else + mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] let glob_constr ist genv = function | _, Some ce -> @@ -710,7 +712,7 @@ let mkSsrRef name = try locate_reference (ssrqid name) with Not_found -> try locate_reference (ssrtopqid name) with Not_found -> CErrors.user_err (Pp.str "Small scale reflection library not loaded") -let mkSsrRRef name = (CAst.make @@ GRef (mkSsrRef name,None)), None +let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None let mkSsrConst name env sigma = EConstr.fresh_global env sigma (mkSsrRef name) let pf_mkSsrConst name gl = @@ -845,10 +847,10 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = let n_binders = ref 0 in let ty = match ty with | a, (t, None) -> - let rec force_type ty = CAst.(map (function + let rec force_type ty = DAst.(map (function | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t) | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t) - | _ -> (mkRCast ty mkRType).v)) ty in + | _ -> DAst.get (mkRCast ty mkRType))) ty in a, (force_type t, None) | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab6a60f4e..8b69c3435 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl = let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) - (fun ty -> congrtac (arg, Detyping.detype false [] (pf_env gl) (project gl) ty) ist) + (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8e6329a15..d01bdc1b9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -184,9 +184,13 @@ let havetac ist mkt ct, mkt cty, mkt (mkCHole None), loc | _, (_, Some ct) -> mkt ct, mkt (mkCHole None), mkt (mkCHole None), None - | _, ({ loc; v = GCast (ct, CastConv cty) }, None) -> - mkl ct, mkl cty, mkl mkRHole, loc - | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in + | _, (t, None) -> + begin match DAst.get t with + | GCast (ct, CastConv cty) -> + mkl ct, mkl cty, mkl mkRHole, t.CAst.loc + | _ -> mkl t, mkl mkRHole, mkl mkRHole, None + end + in let gl, cut, sol, itac1, itac2 = match fk, namefst, suff with | FwdHave, true, true -> @@ -323,11 +327,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let mkpats = function | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats | _ -> fun x -> x in - let open CAst in let ct = match ct with - | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty) - | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None) - | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" + end + in let cut_implies_goal = not (suff || ghave <> `NoGen) in let c, args, ct, gl = let gens = List.filter (function _, Some _ -> true | _ -> false) gens in @@ -398,11 +409,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in - let open CAst in let c = match c with - | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty) - | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None) - | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in + | (a, (b, Some ct)) -> + begin match ct.CAst.v with + | CCast (_, CastConv cty) -> a, (b, Some cty) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + | (a, (t, None)) -> + begin match DAst.get t with + | GCast (_, CastConv cty) -> a, (cty, None) + | _ -> anomaly "suff: ssr cast hole deleted by typecheck" + end + in let ctac gl = let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in basecuttac "ssr_suff" ty gl in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index db1981228..060225dab 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = | None -> begin match Tacinterp.Value.to_constr v with | Some c -> - let rc = Detyping.detype false [] (pf_env gl) (project gl) c in + let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with | _, Constrexpr.Numeral (s,b) -> let n = int_of_string s in if b then n else -n @@ -1062,32 +1062,32 @@ let rec format_glob_decl h0 d0 = match h0, d0 with Bdef (x, None, v) :: format_glob_decl [] d | _, [] -> [] -let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = GLambda (x, _, _, c) } -> +let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with + | BFvar :: h, GLambda (x, _, _, c) -> let bs, c' = format_glob_constr h c in Bvar x :: bs, c' - | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } -> + | BFdecl 1 :: h, GLambda (x, _, t, c) -> let bs, c' = format_glob_constr h c in Bdecl ([x], t) :: bs, c' - | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 -> + | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 -> begin match format_glob_constr (BFdecl (n - 1) :: h) c with | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c' | _ -> [Bdecl ([x], t)], c end - | BFdef :: h, { v = GLetIn(x, v, oty, c) } -> + | BFdef :: h, GLetIn(x, v, oty, c) -> let bs, c' = format_glob_constr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = GCast (c, CastConv t) } -> + | [BFcast], GCast (c, CastConv t) -> [Bcast t], c - | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) } + | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c) when Array.length c = 1 -> let bs = format_glob_decl h bl.(0) in let bstr = match has_str, f with | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs | _ -> [] in bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0) - | _, c -> - [], c + | _, _ -> + [], c0 (** Forward chaining argument *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 9c59d83d4..507b4631b 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -292,7 +292,7 @@ let interp_search_notation ?loc tag okey = err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function - | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (FirstOrderPatVar x) + | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x) | c -> glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in let _, npat = Patternops.pattern_of_glob_constr (sub () body) in @@ -467,10 +467,10 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref = let open CAst in function - | { v = GApp (f, args) } when isRHoles args -> +let pr_rawhintref c = match DAst.get c with + | GApp (f, args) when isRHoles args -> pr_glob_constr f ++ str "|" ++ int (List.length args) - | c -> pr_glob_constr c + | _ -> pr_glob_constr c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 338ecccc2..61b65e347 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -59,13 +59,13 @@ let glob_view_hints lvh = let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh)) -let interp_view ist si env sigma gv v rid = - let open CAst in - match v with - | { v = GApp ( { v = GHole _ } , rargs); loc } -> - let rv = make ?loc @@ GApp (rid, rargs) in +let interp_view ist si env sigma gv rv rid = + match DAst.get rv with + | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) -> + let loc = rv.CAst.loc in + let rv = DAst.make ?loc @@ GApp (rid, rargs) in snd (interp_open_constr ist (re_sig si sigma) (rv, None)) - | rv -> + | _ -> let interp rc rargs = interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in let rec simple_view rargs n = diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f6300ab7e..2e5522b83 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -134,6 +134,10 @@ let dC t = CastConv t let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> CErrors.anomaly (str"not a CRef.") +let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false +let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) + | _ -> CErrors.anomaly (str "not a GLambda") +let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t) @@ -141,10 +145,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((Loc.tag ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args) -let mkRCast rc rt = CAst.make @@ GCast (rc, dC rt) -let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t) +let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) let combineCG t1 t2 f g = match t1, t2 with @@ -980,11 +984,10 @@ let pr_rpattern = pr_pattern type pattern = Evd.evar_map * (constr, constr) ssrpattern - -let id_of_cpattern = let open CAst in function - | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x - | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x - | _,({ v = GRef (VarRef x, _)} ,None) -> Some x +let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with + | _, Some { v = CRef (Ident (_, x), _) } -> Some x + | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x + | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1082,10 +1085,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = let eAsXInT e x t = E_As_X_In_T(e,x,t) in let mkG ?(k=' ') x = k,(x,None) in let decode ist t ?reccall f g = - let open CAst in - try match (pf_intern_term ist gl t) with - | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None)) - | { v = GVar id } + try match DAst.get (pf_intern_term ist gl t) with + | GCast(t,CastConv c) when isGHole t && isGLambda c-> + let (x, c) = destGLambda c in + f x (' ',(c,None)) + | GVar id when Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> @@ -1126,19 +1130,27 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = let open CAst in match red with - | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) - when let id = Id.to_string id in let len = String.length id in + let red = let rec decode_red (ist,red) = match red with + | T(k,(t,None)) -> + begin match DAst.get t with + | GCast (c,CastConv t) + when isGHole c && + let (id, t) = destGLambda t in + let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> + let (id, t) = destGLambda t in let id = Id.to_string id in let len = String.length id in - (match String.sub id 8 (len - 8), t with - | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) - | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", { v = GApp( _, [e; t; e_in_t]) } -> + (match String.sub id 8 (len - 8), DAst.get t with + | "In", GApp( _, [t]) -> decodeG t xInT (fun x -> T x) + | "In", GApp( _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", GApp( _, [e; t; e_in_t]) -> decodeG t (eInXInT (mkG e)) (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) | _ -> bad_enc id ()) + | _ -> + decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x) + end | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) | In_T t -> decode ist t inXInT inT | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) @@ -1163,7 +1175,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn ?loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)) - | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in + | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t @@ -1336,10 +1348,10 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef id, None), None) +let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef id, None), None) -let is_wildcard : cpattern -> bool = function - | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true +let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with + | _, Some { CAst.v = CHole _ } | GHole _, None -> true | _ -> false (* "ssrpattern" *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index c41ec39cb..b299ff853 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -25,6 +25,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -42,9 +46,9 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) :: (aux (n-1) (p/2)) in - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) let interp_ascii_string ?loc s = let p = @@ -60,12 +64,12 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try - let aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + let aux c = match DAst.get c with + | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -75,10 +79,10 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index af64b1479..0dff047a3 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -23,6 +23,10 @@ open Glob_term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let make_mind mp id = Names.MutInd.make2 mp (Label.make id) let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = @@ -49,9 +53,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint ?loc n = - let ref_construct = CAst.make ?loc (GRef (int31_construct, None)) in - let ref_0 = CAst.make ?loc (GRef (int31_0, None)) in - let ref_1 = CAst.make ?loc (GRef (int31_1, None)) in + let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in + let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in + let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in let rec args counter n = if counter <= 0 then [] @@ -59,7 +63,7 @@ let int31_of_pos_bigint ?loc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) + DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") @@ -76,15 +80,15 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur) + | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in - function - | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero + fun c -> match DAst.get c with + | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero | _ -> raise Non_closed -let uninterp_int31 i = +let uninterp_int31 (AnyGlobConstr i) = try Some (bigint_of_int31 i) with Non_closed -> @@ -94,6 +98,6 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([CAst.make (GRef (int31_construct, None))], + ([DAst.make (GRef (int31_construct, None))], uninterp_int31, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 524a5c522..2f9870cf9 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -37,11 +37,11 @@ let warn_large_nat = let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in + let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -56,13 +56,17 @@ let nat_of_int ?loc n = exception Non_closed_number -let rec int_of_nat x = CAst.with_val (function - | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) +let rec int_of_nat x = DAst.with_val (function + | GApp (r, [a]) -> + begin match DAst.get r with + | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number ) x -let uninterp_nat p = +let uninterp_nat (AnyGlobConstr p) = try Some (int_of_nat p) with @@ -75,4 +79,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true) + ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 06117de79..88ff38c6d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -27,6 +27,10 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + let positive_path = make_path binnums "positive" (* TODO: temporary hack *) @@ -42,13 +46,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make @@ GRef (glob_xI, None) in - let ref_xH = CAst.make @@ GRef (glob_xH, None) in - let ref_xO = CAst.make @@ GRef (glob_xO, None) in + let ref_xI = DAst.make @@ GRef (glob_xI, None) in + let ref_xH = DAst.make @@ GRef (glob_xH, None) in + let ref_xO = DAst.make @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -57,10 +61,10 @@ let pos_of_bignat ?loc x = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one +let rec bignat_of_pos c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -81,18 +85,18 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - CAst.make @@ GRef (glob_ZERO, None) + DAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero +let bigint_of_z c = match DAst.get c with + | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -108,18 +112,18 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int ?loc z = - CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) + DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bigint_of_r = function - | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> +let bigint_of_r c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_IZR -> bigint_of_z a | _ -> raise Non_closed_number -let uninterp_r p = +let uninterp_r (AnyGlobConstr p) = try Some (bigint_of_r p) with Non_closed_number -> @@ -128,6 +132,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([CAst.make @@ GRef (glob_IZR, None)], + ([DAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index b7f13b040..cc82fc94c 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -31,25 +31,29 @@ let make_reference id = find_reference "String interpretation" string_module id let glob_String = lazy (make_reference "String") let glob_EmptyString = lazy (make_reference "EmptyString") +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + open Lazy let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), + if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 -let uninterp_string r = +let uninterp_string (AnyGlobConstr r) = try let b = Buffer.create 16 in - let rec aux = function - | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) -> + let rec aux c = match DAst.get c with + | GApp (k,[a;s]) when is_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -61,6 +65,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([CAst.make @@ GRef (static_glob_String,None); - CAst.make @@ GRef (static_glob_EmptyString,None)], + ([DAst.make @@ GRef (static_glob_String,None); + DAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index af3df2889..0d743a2b5 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in + let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in + let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in let rec pos_of x = match div2_with_rest x with - | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) + | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) | (q,true) -> ref_xH in pos_of x @@ -68,14 +68,18 @@ let interp_positive ?loc n = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos x = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + +let rec bignat_of_pos x = DAst.with_val (function + | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number ) x -let uninterp_positive p = +let uninterp_positive (AnyGlobConstr p) = try Some (bignat_of_pos p) with Non_closed_number -> @@ -88,9 +92,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([CAst.make @@ GRef (glob_xI, None); - CAst.make @@ GRef (glob_xO, None); - CAst.make @@ GRef (glob_xH, None)], + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -107,9 +111,9 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else GRef(glob_N0, None) @@ -124,13 +128,13 @@ let n_of_int ?loc n = (* Printing N via scopes *) (**********************************************************************) -let bignat_of_n = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a +let bignat_of_n n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number - ) + ) n -let uninterp_n p = +let uninterp_n (AnyGlobConstr p) = try Some (bignat_of_n p) with Non_closed_number -> None @@ -140,8 +144,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([CAst.make @@ GRef (glob_N0, None); - CAst.make @@ GRef (glob_Npos, None)], + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -163,22 +167,22 @@ let z_of_int ?loc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) + DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - CAst.make ?loc @@ GRef(glob_ZERO, None) + DAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) +let bigint_of_z z = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number - ) + ) z -let uninterp_z p = +let uninterp_z (AnyGlobConstr p) = try Some (bigint_of_z p) with Non_closed_number -> None @@ -189,8 +193,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([CAst.make @@ GRef (glob_ZERO, None); - CAst.make @@ GRef (glob_POS, None); - CAst.make @@ GRef (glob_NEG, None)], + ([DAst.make @@ GRef (glob_ZERO, None); + DAst.make @@ GRef (glob_POS, None); + DAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) |