diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 60 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 7 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 482 | ||||
| -rw-r--r-- | plugins/extraction/extraction.mli | 12 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 6 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/g_eqdecide.ml4 | 1 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 76 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 19 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 135 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 12 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 98 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 8 | ||||
| -rw-r--r-- | plugins/nsatz/g_nsatz.ml4 | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 |
18 files changed, 583 insertions, 351 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 722b3990cb..a4e8c44cd0 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,22 +137,25 @@ let check_arity env cb = let t = cb.const_type in if Reduction.is_arity env t then raise Impossible -let check_fix env cb i = +let get_body lbody = + EConstr.of_constr (Mod_subst.force_constr lbody) + +let check_fix env sg cb i = match cb.const_body with | Def lbody -> - (match Constr.kind (Mod_subst.force_constr lbody) with - | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) + (match EConstr.kind sg (get_body lbody) with + | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) | Undef _ | OpaqueDef _ -> raise Impossible -let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = +let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ca1 ca2 && - Array.equal Constr.equal ta1 ta2 + Array.equal (EConstr.eq_constr sg) ca1 ca2 && + Array.equal (EConstr.eq_constr sg) ta1 ta2 -let factor_fix env l cb msb = - let _,recd as check = check_fix env cb 0 in +let factor_fix env sg l cb msb = + let _,recd as check = check_fix env sg cb 0 in let n = Array.length (let fi,_,_ = recd in fi) in if Int.equal n 1 then [|l|], recd, msb else begin @@ -163,9 +166,9 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - let check' = check_fix env cb' (j+1) in - if not ((fst check : bool) == (fst check') && - prec_declaration_equal (snd check) (snd check')) + let check' = check_fix env sg cb' (j+1) in + if not ((fst check : bool) == (fst check') && + prec_declaration_equal sg (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; @@ -248,7 +251,9 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in let env' = env_for_mtb_with_def env mp1 me_struct delta idl in let mt = extract_mexpr_spec env mp1 (None,me') in - (match extract_with_type env' c with (* cb may contain some kn *) + let sg = Evd.from_env env in + (match extract_with_type env' sg (EConstr.of_constr c) with + (* cb may contain some kn *) | None -> mt | Some (vl,typ) -> type_iter_references Visit.add_ref typ; @@ -299,12 +304,13 @@ let rec extract_structure env mp reso ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try - let vl,recd,struc = factor_fix env l cb struc in + let sg = Evd.from_env env in + let vl,recd,struc = factor_fix env sg l cb struc in let vc = Array.map (make_cst reso mp) vl in let ms = extract_structure env mp reso ~all struc in let b = Array.exists Visit.needed_cst vc in if all || b then - let d = extract_fixpoint env vc recd in + let d = extract_fixpoint env sg vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -572,8 +578,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init ?(compute=false) modular library = - check_inside_section (); check_inside_module (); +let init ?(compute=false) ?(inner=false) modular library = + if not inner then (check_inside_section (); check_inside_module ()); set_keywords (descr ()).keywords; set_modular modular; set_library library; @@ -701,10 +707,9 @@ let flatten_structure struc = and flatten_elems l = List.flatten (List.map flatten_elem l) in flatten_elems (List.flatten (List.map snd struc)) -let structure_for_compute c = +let structure_for_compute env sg c = init false false ~compute:true; - let env = Global.env () in - let ast, mlt = Extraction.extract_constr env c in + let ast, mlt = Extraction.extract_constr env sg c in let ast = Mlutil.normalize ast in let refs = ref Refset.empty in let add_ref r = refs := Refset.add r !refs in @@ -744,3 +749,20 @@ let extract_and_compile l = let base = Filename.chop_suffix f ".ml" in let () = remove (base^".cmo"); remove (base^".cmi") in Feedback.msg_notice (str "Extracted code successfully compiled") + +(* Show the extraction of the current ongoing proof *) + +let show_extraction () = + init ~inner:true false false; + let prf = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let trms = Proof.partial_proof prf in + let extr_term t = + let ast, ty = extract_constr env sigma t in + let mp = Lib.current_mp () in + let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let fake_ref = ConstRef (Constant.make2 mp l) in + let decl = Dterm (fake_ref, ast, ty) in + print_one_decl [] mp decl + in + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 464f109be2..591d3bb86e 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -36,4 +36,9 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Environ.env -> Evd.evar_map -> EConstr.t -> + Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type + +(* Show the extraction of the current ongoing proof *) + +val show_extraction : unit -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ce49700561..f25f636249 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Vars open Declarations open Declareops open Environ @@ -36,20 +35,18 @@ exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : Constant.t list) -let none = Evd.empty - (* NB: In OCaml, [type_of] and [get_of] might raise [SingletonInductiveBecomeProp]. This exception will be caught in late wrappers around the exported functions of this file, in order to display the location of the issue. *) -let type_of env c = +let type_of env sg c = let polyprop = (lang() == Haskell) in - EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env sg (strip_outer_cast sg c) -let sort_of env c = +let sort_of env sg c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_sort_family_of ~polyprop env sg (strip_outer_cast sg c) (*S Generation of flags and signatures. *) @@ -73,61 +70,91 @@ type scheme = TypeScheme | Default type flag = info * scheme -let whd_all env t = - EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t)) - -let whd_betaiotazeta t = - EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t)) - (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) -let rec flag_of_type env t : flag = - let t = whd_all env t in - match Constr.kind t with - | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c - | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) +let rec flag_of_type env sg t : flag = + let t = whd_all env sg t in + match EConstr.kind sg t with + | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c + | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) + | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) (*s Two particular cases of [flag_of_type]. *) -let is_default env t = match flag_of_type env t with +let is_default env sg t = match flag_of_type env sg t with | (Info, Default) -> true | _ -> false exception NotDefault of kill_reason -let check_default env t = - match flag_of_type env t with +let check_default env sg t = + match flag_of_type env sg t with | _,TypeScheme -> raise (NotDefault Ktype) | Logic,_ -> raise (NotDefault Kprop) | _ -> () -let is_info_scheme env t = match flag_of_type env t with +let is_info_scheme env sg t = match flag_of_type env sg t with | (Info, TypeScheme) -> true | _ -> false let push_rel_assum (n, t) env = - Environ.push_rel (LocalAssum (n, t)) env + EConstr.push_rel (LocalAssum (n, t)) env + +let push_rels_assum assums = + EConstr.push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums) + +let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) + +let get_opaque env c = + EConstr.of_constr + (Opaqueproof.force_proof (Environ.opaque_tables env) c) + +let applistc c args = EConstr.mkApp (c, Array.of_list args) + +(* Same as [Environ.push_rec_types], but for [EConstr.t] *) +let push_rec_types (lna,typarray,_) env = + let ctxt = + Array.map2_i + (fun i na t -> LocalAssum (na, EConstr.Vars.lift i t)) lna typarray + in + Array.fold_left (fun e assum -> EConstr.push_rel assum e) env ctxt + +(* Same as [Termops.nb_lam], but for [EConstr.t] *) +let nb_lam sg c = List.length (fst (EConstr.decompose_lam sg c)) + +(* Same as [Term.decompose_lam_n] but for [EConstr.t] *) +let decompose_lam_n sg n = + let rec lamdec_rec l n c = + if n <= 0 then l,c + else match EConstr.kind sg c with + | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | _ -> raise Not_found + in + lamdec_rec [] n (*s [type_sign] gernerates a signature aimed at treating a type application. *) -let rec type_sign env c = - match Constr.kind (whd_all env c) with +let rec type_sign env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kprop) - :: (type_sign (push_rel_assum (n,t) env) d) + (if is_info_scheme env sg t then Keep else Kill Kprop) + :: (type_sign (push_rel_assum (n,t) env) sg d) | _ -> [] -let rec type_scheme_nb_args env c = - match Constr.kind (whd_all env c) with +let rec type_scheme_nb_args env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in - if is_info_scheme env t then n+1 else n + let n = type_scheme_nb_args (push_rel_assum (n,t) env) sg d in + if is_info_scheme env sg t then n+1 else n | _ -> 0 -let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args +let type_scheme_nb_args' env c = + type_scheme_nb_args env (Evd.from_env env) (EConstr.of_constr c) + +let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args' (*s [type_sign_vl] does the same, plus a type var list. *) @@ -147,19 +174,19 @@ let make_typvar n vl = let vl = Id.Set.of_list vl in next_ident_away id' vl -let rec type_sign_vl env c = - match Constr.kind (whd_all env c) with +let rec type_sign_vl env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kprop::s, vl - else Keep::s, (make_typvar n vl) :: vl + let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in + if not (is_info_scheme env sg t) then Kill Kprop::s, vl + else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] -let rec nb_default_params env c = - match Constr.kind (whd_all env c) with +let rec nb_default_params env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = nb_default_params (push_rel_assum (n,t) env) d in - if is_default env t then n+1 else n + let n = nb_default_params (push_rel_assum (n,t) env) sg d in + if is_default env sg t then n+1 else n | _ -> 0 (* Enriching a signature with implicit information *) @@ -226,62 +253,62 @@ let parse_ind_args si args relmax = generate ML type var anymore (in subterms for example). *) -let rec extract_type env db j c args = - match Constr.kind (whd_betaiotazeta c) with +let rec extract_type env sg db j c args = + match EConstr.kind sg (whd_betaiotazeta sg c) with | App (d, args') -> - (* We just accumulate the arguments. *) - extract_type env db j d (Array.to_list args' @ args) + (* We just accumulate the arguments. *) + extract_type env sg db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> (match args with | [] -> assert false (* A lambda cannot be a type. *) - | a :: args -> extract_type env db j (subst1 a d) args) + | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args) | Prod (n,t,d) -> assert (List.is_empty args); let env' = push_rel_assum (n,t) env in - (match flag_of_type env t with + (match flag_of_type env sg t with | (Info, Default) -> (* Standard case: two [extract_type] ... *) - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d - | _ -> Tarr (extract_type env db 0 t [], mld)) + | _ -> Tarr (extract_type env sg db 0 t [], mld)) | (Info, TypeScheme) when j > 0 -> (* A new type var. *) - let mld = extract_type env' (j::db) (j+1) d [] in + let mld = extract_type env' sg (j::db) (j+1) d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> Tarr (Tdummy Ktype, mld)) | _,lvl -> - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applistc c args) == InProp -> Tdummy Kprop + | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop | Rel n -> - (match lookup_rel n env with - | LocalDef (_,t,_) -> extract_type env db j (lift n t) args + (match EConstr.lookup_rel n env with + | LocalDef (_,t,_) -> + extract_type env sg db j (EConstr.Vars.lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') - | Const (kn,u as c) -> - let r = ConstRef kn in - let cb = lookup_constant kn env in - let typ = Typeops.type_of_constant_in env c in - (match flag_of_type env typ with + | Const (kn,u) -> + let r = ConstRef kn in + let typ = type_of env sg (EConstr.mkConstU (kn,u)) in + (match flag_of_type env sg typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> - let mlt = extract_type_app env db (r, type_sign env typ) args in - (match cb.const_body with + let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> mlt - | Def _ when is_custom r -> mlt + | Def _ when is_custom (ConstRef kn) -> mlt | Def lbody -> - let newc = applistc (Mod_subst.force_constr lbody) args in - let mlt' = extract_type env db j newc [] in + let newc = applistc (get_body lbody) args in + let mlt' = extract_type env sg db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) (* The more precise is [mlt'], extracted after reduction *) @@ -290,36 +317,51 @@ let rec extract_type env db j c args = if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt') | (Info, Default) -> (* Not an ML type, for example [(c:forall X, X->X) Type nat] *) - (match cb.const_body with + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applistc (Mod_subst.force_constr lbody) args in - extract_type env db j newc [])) + let newc = applistc (get_body lbody) args in + extract_type env sg db j newc [])) | Ind ((kn,i),u) -> - let s = (extract_ind env kn).ind_packets.(i).ip_sign in - extract_type_app env db (IndRef (kn,i),s) args + let s = (extract_ind env kn).ind_packets.(i).ip_sign in + extract_type_app env sg db (IndRef (kn,i),s) args | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown - else extract_type env db j (mkProj (Projection.unfold p, t)) args + else + extract_type env sg db j (EConstr.mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false + | Evar _ | Meta _ -> Taxiom (* only possible during Show Extraction *) + | Var v -> + (* For Show Extraction *) + let open Context.Named.Declaration in + (match EConstr.lookup_named v env with + | LocalDef (_,body,_) -> + extract_type env sg db j (EConstr.applist (body,args)) [] + | LocalAssum (_,ty) -> + let r = VarRef v in + (match flag_of_type env sg ty with + | (Logic,_) -> assert false (* Cf. logical cases above *) + | (Info, TypeScheme) -> + extract_type_app env sg db (r, type_sign env sg ty) args + | (Info, Default) -> Tunknown)) + | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) -and extract_type_app env db (r,s) args = +and extract_type_app env sg db (r,s) args = let ml_args = List.fold_right (fun (b,c) a -> if b == Keep then - let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in + let p = List.length (fst (splay_prod env sg (type_of env sg c))) in let db = iterate (fun l -> 0 :: l) p db in - (extract_type_scheme env db c p) :: a + (extract_type_scheme env sg db c p) :: a else a) (List.combine s args) [] - in Tglob (r, ml_args) + in Tglob (r, ml_args) (*S Extraction of a type scheme. *) @@ -330,19 +372,18 @@ and extract_type_app env db (r,s) args = (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) -and extract_type_scheme env db c p = - if Int.equal p 0 then extract_type env db 0 c [] +and extract_type_scheme env sg db c p = + if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta c in - match Constr.kind c with + let c = whd_betaiotazeta sg c in + match EConstr.kind sg c with | Lambda (n,t,d) -> - extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) + extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) | _ -> - let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in - let rels = List.map (on_snd EConstr.Unsafe.to_constr) rels in + let rels = fst (splay_prod env sg (type_of env sg c)) in let env = push_rels_assum rels env in - let eta_args = List.rev_map mkRel (List.interval 1 p) in - extract_type env db 0 (lift p c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 p) in + extract_type env sg db 0 (EConstr.Vars.lift p c) eta_args (*S Extraction of an inductive type. *) @@ -384,6 +425,7 @@ and extract_really_ind env kn mib = let mip0 = mib.mind_packets.(0) in let npar = mib.mind_nparams in let epar = push_rel_context mib.mind_params_ctxt env in + let sg = Evd.from_env env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -391,8 +433,9 @@ and extract_really_ind env kn mib = (fun i mip -> let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in - let info = (fst (flag_of_type env ar) = Info) in - let s,v = if info then type_sign_vl env ar else [],[] in + let ar = EConstr.of_constr ar in + let info = (fst (flag_of_type env sg ar) = Info) in + let s,v = if info then type_sign_vl env sg ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; ip_consnames = mip.mind_consnames; @@ -424,7 +467,8 @@ and extract_really_ind env kn mib = in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in let db = db_from_ind dbmap npar in - p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1) + p.ip_types.(j) <- + extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1) done done; (* Third pass: we determine special cases. *) @@ -477,10 +521,9 @@ and extract_really_ind env kn mib = (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env - (Inductive.type_of_inductive env ((mib,mip0),u)) - in - let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip + let ty = Inductive.type_of_inductive env ((mib,mip0),u) in + let n = nb_default_params env sg (EConstr.of_constr ty) in + let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in List.iter (Option.iter check_proj) (lookup_projections ip) with Not_found -> () @@ -505,13 +548,13 @@ and extract_really_ind env kn mib = - [i] is the rank of the current product (initially [params_nb+1]) *) -and extract_type_cons env db dbmap c i = - match Constr.kind (whd_all env c) with +and extract_type_cons env sg db dbmap c i = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in - let l = extract_type_cons env' db' dbmap d (i+1) in - (extract_type env db 0 t []) :: l + let l = extract_type_cons env' sg db' dbmap d (i+1) in + (extract_type env sg db 0 t []) :: l | _ -> [] (*s Recording the ML type abbreviation of a Coq type scheme constant. *) @@ -526,16 +569,17 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = cb.const_type + let sg = Evd.from_env env in + let typ = EConstr.of_constr cb.const_type (* FIXME not sure if we should instantiate univs here *) in - match flag_of_type env typ with - | Info,TypeScheme -> - let body = Mod_subst.force_constr l_body in - let s = type_sign env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) - in add_typedef kn cb t; Some t - | _ -> None + match flag_of_type env sg typ with + | Info,TypeScheme -> + let body = get_body l_body in + let s = type_sign env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db body (List.length s) + in add_typedef kn cb t; Some t + | _ -> None and expand env = type_expand (mlt_env env) and type2signature env = type_to_signature (mlt_env env) @@ -545,16 +589,16 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) (*s Extraction of the type of a constant. *) -let record_constant_type env kn opt_typ = +let record_constant_type env sg kn opt_typ = let cb = lookup_constant kn env in match lookup_cst_type kn cb with | Some schema -> schema | None -> let typ = match opt_typ with - | None -> cb.const_type + | None -> EConstr.of_constr cb.const_type | Some typ -> typ in - let mlt = extract_type env [] 1 typ [] in + let mlt = extract_type env sg [] 1 typ [] in let schema = (type_maxvar mlt, mlt) in let () = add_cst_type kn cb schema in schema @@ -566,75 +610,86 @@ let record_constant_type env kn opt_typ = (* [mle] is a ML environment [Mlenv.t]. *) (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) -let rec extract_term env mle mlt c args = - match Constr.kind c with +let rec extract_term env sg mle mlt c args = + match EConstr.kind sg c with | App (f,a) -> - extract_term env mle mlt f (Array.to_list a @ args) + extract_term env sg mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> let id = id_of_name n in (match args with | a :: l -> (* We make as many [LetIn] as possible. *) - let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l)) - in extract_term env mle mlt d' [] + let l' = List.map (EConstr.Vars.lift 1) l in + let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in + extract_term env sg mle mlt d' [] | [] -> let env' = push_rel_assum (Name id, t) env in let id, a = - try check_default env t; Id id, new_meta() - with NotDefault d -> Dummy, Tdummy d + try check_default env sg t; Id id, new_meta() + with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in (* If [mlt] cannot be unified with an arrow type, then magic! *) let magic = needs_magic (mlt, Tarr (a, b)) in - let d' = extract_term env' (Mlenv.push_type mle a) b d [] in + let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (LocalDef (Name id, c1, t1)) env in + let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) - let args' = List.map (lift 1) args in + let args' = List.map (EConstr.Vars.lift 1) args in (try - check_default env t1; + check_default env sg t1; let a = new_meta () in - let c1' = extract_term env mle a c1 [] in + let c1' = extract_term env sg mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = if generalizable c1' then Mlenv.push_gen mle a else Mlenv.push_type mle a in - MLletin (Id id, c1', extract_term env' mle' mlt c2 args') + MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in - ast_pop (extract_term env' mle' mlt c2 args')) + ast_pop (extract_term env' sg mle' mlt c2 args')) | Const (kn,_) -> - extract_cst_app env mle mlt kn args + extract_cst_app env sg mle mlt kn args | Construct (cp,_) -> - extract_cons_app env mle mlt cp args + extract_cons_app env sg mle mlt cp args | Proj (p, c) -> - let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in - let term = EConstr.Unsafe.to_constr term in - extract_term env mle mlt term args + let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + extract_term env sg mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) - in extract_app env mle mlt extract_rel args + in extract_app env sg mle mlt extract_rel args | Case ({ci_ind=ip},_,c0,br) -> - extract_app env mle mlt (extract_case env mle (ip,c0,br)) args + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args + extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c,_,_) -> extract_term env mle mlt c args - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false + extract_app env sg mle mlt (extract_fix env sg mle i recd) args + | Cast (c,_,_) -> extract_term env sg mle mlt c args + | Evar _ | Meta _ -> MLaxiom + | Var v -> + (* Only during Show Extraction *) + let open Context.Named.Declaration in + let ty = match EConstr.lookup_named v env with + | LocalAssum (_,ty) -> ty + | LocalDef (_,_,ty) -> ty + in + let vty = extract_type env sg [] 0 ty [] in + let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + extract_app env sg mle mlt extract_var args + | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) -and extract_maybe_term env mle mlt c = - try check_default env (type_of env c); - extract_term env mle mlt c [] +and extract_maybe_term env sg mle mlt c = + try check_default env sg (type_of env sg c); + extract_term env sg mle mlt c [] with NotDefault d -> put_magic (mlt, Tdummy d) (MLdummy d) @@ -644,28 +699,28 @@ and extract_maybe_term env mle mlt c = This gives us the expected type of the head. Then we use the [mk_head] to produce the ML head from this type. *) -and extract_app env mle mlt mk_head args = +and extract_app env sg mle mlt mk_head args = let metas = List.map new_meta args in let type_head = type_recomp (metas, mlt) in - let mlargs = List.map2 (extract_maybe_term env mle) metas args in + let mlargs = List.map2 (extract_maybe_term env sg mle) metas args in mlapp (mk_head type_head) mlargs (*s Auxiliary function used to extract arguments of constant or constructor. *) -and make_mlargs env e s args typs = +and make_mlargs env sg e s args typs = let rec f = function | [], [], _ -> [] - | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[])) - | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s)) + | a::la, t::lt, [] -> extract_maybe_term env sg e t a :: (f (la,lt,[])) + | a::la, t::lt, Keep::s -> extract_maybe_term env sg e t a :: (f (la,lt,s)) | _::la, _::lt, _::s -> f (la,lt,s) | _ -> assert false in f (args,typs,s) (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn args = +and extract_cst_app env sg mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) - let nb,t = record_constant_type env kn None in + let nb,t = record_constant_type env sg kn None in let schema = nb, expand env t in (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) @@ -691,7 +746,7 @@ and extract_cst_app env mle mlt kn args = let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) - let mla = make_mlargs env mle s args metas in + let mla = make_mlargs env sg mle s args metas in let mla = if magic1 || lang () != Ocaml then mla else @@ -736,7 +791,7 @@ and extract_cst_app env mle mlt kn args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = +and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -777,7 +832,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = put_magic_if magic2 (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)) else - let mla = make_mlargs env mle s args' metas in + let mla = make_mlargs env sg mle s args' metas in if Int.equal la (ls + params_nb) then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) @@ -788,7 +843,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (*S Extraction of a case. *) -and extract_case env mle ((kn,i) as ip,c,br) mlt = +and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) let ni = constructors_nrealargs_env env ip in @@ -799,9 +854,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = MLexn "absurd case" end else (* [c] has an inductive type, and is not a type scheme type. *) - let t = type_of env c in + let t = type_of env sg c in (* The only non-informative case: [c] is of sort [Prop] *) - if (sort_of env t) == InProp then + if (sort_of env sg t) == InProp then begin add_recursors env kn; (* May have passed unseen if logical ... *) (* Logical singleton case: *) @@ -809,7 +864,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = assert (Int.equal br_size 1); let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in - let e = extract_maybe_term env mle mlt br.(0) in + let e = extract_maybe_term env sg mle mlt br.(0) in snd (case_expunge s e) end else @@ -818,7 +873,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) let type_head = Tglob (IndRef ip, Array.to_list metas) in - let a = extract_term env mle type_head c [] in + let a = extract_term env sg mle type_head c [] in (* The extraction of each branch. *) let extract_branch i = let r = ConstructRef (ip,i+1) in @@ -829,7 +884,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let s = List.map (type2sign env) oi.ip_types.(i) in let s = sign_with_implicits r s mi.ind_nparams in (* Extraction of the branch (in functional form). *) - let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in + let e = extract_maybe_term env sg mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in (List.rev ids, Pusual r, e) @@ -851,12 +906,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (*s Extraction of a (co)-fixpoint. *) -and extract_fix env mle i (fi,ti,ci as recd) mlt = +and extract_fix env sg mle i (fi,ti,ci as recd) mlt = let env = push_rec_types recd env in let metas = Array.map new_meta fi in metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in - let ei = Array.map2 (extract_maybe_term env mle) metas ci in + let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -864,34 +919,34 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) -let decomp_lams_eta_n n m env c t = - let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in - let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,EConstr.Unsafe.to_constr c)) rels in - let rels',c = decompose_lam c in +let decomp_lams_eta_n n m env sg c t = + let rels = fst (splay_prod_n env sg n t) in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in + let rels',c = EConstr.decompose_lam sg c in let d = n - m in (* we'd better keep rels' as long as possible. *) let rels = (List.firstn d rels) @ rels' in - let eta_args = List.rev_map mkRel (List.interval 1 d) in - rels, applistc (lift d c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 d) in + rels, applistc (EConstr.Vars.lift d c) eta_args (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match Constr.kind c with +let rec gentypvar_ok sg c = match EConstr.kind sg c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will disappear after extraction (see [empty_s] below) *) - Array.for_all isRel v && gentypvar_ok c - | Cast (c,_,_) -> gentypvar_ok c + Array.for_all (EConstr.isRel sg) v && gentypvar_ok sg c + | Cast (c,_,_) -> gentypvar_ok sg c | _ -> false (*s From a constant to a ML declaration. *) -let extract_std_constant env kn body typ = +let extract_std_constant env sg kn body typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,t' = type_decomp (expand env (var2var' t)) in @@ -906,14 +961,14 @@ let extract_std_constant env kn body typ = break user's clever let-ins and partial applications). *) let rels, c = let n = List.length s - and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in - if n <= m then decompose_lam_n n body + and m = nb_lam sg body in + if n <= m then decompose_lam_n sg n body else let s,s' = List.chop m s in if List.for_all ((==) Keep) s' && (lang () == Haskell || sign_kind s != UnsafeLogicalSig) - then decompose_lam_n m body - else decomp_lams_eta_n n m env body typ + then decompose_lam_n sg m body + else decomp_lams_eta_n n m env sg body typ in (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = @@ -921,9 +976,9 @@ let extract_std_constant env kn body typ = let s,s' = List.chop n s in let k = sign_kind s in let empty_s = (k == EmptySig || k == SafeLogicalSig) in - if lang () == Ocaml && empty_s && not (gentypvar_ok c) + if lang () == Ocaml && empty_s && not (gentypvar_ok sg c) && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0) - then decomp_lams_eta_n (n+1) n env body typ + then decomp_lams_eta_n (n+1) n env sg body typ else rels,c in let n = List.length rels in @@ -937,16 +992,16 @@ let extract_std_constant env kn body typ = (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) - let e = extract_term env mle t' c [] in + let e = extract_term env sg mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) -let extract_axiom env kn typ = +let extract_axiom env sg kn typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,_ = type_decomp (expand env (var2var' t)) in @@ -955,18 +1010,19 @@ let extract_axiom env kn typ = let s = sign_with_implicits (ConstRef kn) s 0 in type_expunge_from_sign env s t -let extract_fixpoint env vkn (fi,ti,ci) = +let extract_fixpoint env sg vkn (fi,ti,ci) = let n = Array.length vkn in let types = Array.make n (Tdummy Kprop) and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) - let sub = List.rev_map mkConst kns in + let sub = List.rev_map EConstr.mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then + if sort_of env sg ti.(i) != InProp then try - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + let e,t = extract_std_constant env sg vkn.(i) + (EConstr.Vars.substl sub ci.(i)) ti.(i) in terms.(i) <- e; types.(i) <- t; with SingletonInductiveBecomesProp id -> @@ -976,32 +1032,33 @@ let extract_fixpoint env vkn (fi,ti,ci) = Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) let extract_constant env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in let mk_typ_ax () = - let n = type_scheme_nb_args env typ in + let n = type_scheme_nb_args env sg typ in let ids = iterate (fun l -> anonymous_name::l) n [] in Dtype (r, ids, Taxiom) in let mk_typ c = - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) + let t = extract_type_scheme env sg db c (List.length s) in Dtype (r, vl, t) in let mk_ax () = - let t = extract_axiom env kn typ in + let t = extract_axiom env sg kn typ in Dterm (r, MLaxiom, t) in let mk_def c = - let e,t = extract_std_constant env kn c typ in + let e,t = extract_std_constant env sg kn c typ in Dterm (r,e,t) in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> @@ -1009,73 +1066,72 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (Mod_subst.force_constr c) - | Some pb -> mk_typ pb.proj_body) + | None -> mk_typ (get_body c) + | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_typ (get_opaque env c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (Mod_subst.force_constr c) - | Some pb -> mk_def pb.proj_body) + | None -> mk_def (get_body c) + | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_def (get_opaque env c) else mk_ax ()) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in (match cb.const_body with | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let body = Mod_subst.force_constr body in - let t = extract_type_scheme env db body (List.length s) - in Stype (r, vl, Some t)) + let body = get_body body in + let t = extract_type_scheme env sg db body (List.length s) + in Stype (r, vl, Some t)) | (Info, Default) -> - let t = snd (record_constant_type env kn (Some typ)) in - Sval (r, type_expunge env t) + let t = snd (record_constant_type env sg kn (Some typ)) in + Sval (r, type_expunge env t) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) -let extract_with_type env c = +let extract_with_type env sg c = try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) in - Some (vl, t) + let s,vl = type_sign_vl env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db c (List.length s) in + Some (vl, t) | _ -> None with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None -let extract_constr env c = +let extract_constr env sg c = reset_meta_count (); try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> - let mlt = extract_type env [] 1 typ [] in - extract_term env Mlenv.empty mlt c [], mlt + let mlt = extract_type env sg [] 1 typ [] in + extract_term env sg Mlenv.empty mlt c [], mlt with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index a0f2885a42..d27c79cb62 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -11,9 +11,9 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Constr open Declarations open Environ +open Evd open Miniml val extract_constant : env -> Constant.t -> constant_body -> ml_decl @@ -22,16 +22,18 @@ val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) -val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option +val extract_with_type : + env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl + env -> evar_map -> Constant.t array -> + (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) -val extract_constr : env -> constr -> ml_ast * ml_type +val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type (*s Is a [ml_decl] or a [ml_spec] logical ? *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 468f2fe8ca..93909f3e64 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -160,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> [ show_extraction () ] +END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 0bcda69d4d..6c421491fc 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -38,14 +38,13 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstRef _ | VarRef _ -> false let repr_of_r = function | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr3 kn - | VarRef _ -> assert false + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -279,7 +278,7 @@ let safe_basename_of_global r = | ConstructRef ((kn,i),j) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) - | VarRef _ -> assert false + | VarRef v -> v let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index b3bcc99840..2251a66204 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -15,6 +15,7 @@ (************************************************************************) open Eqdecide +open Stdarg DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b46413..e0368153e5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4665ff9ed3..2c7ebb7458 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -16,6 +16,7 @@ open Misctypes open Genarg open Stdarg open Geninterp +open Pp exception CannotCoerceTo of string @@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v let to_pair v = prj Val.typ_pair v +let cast_error wit v = + let pr_v = Pptactic.pr_value Pptactic.ltop v in + let Val.Dyn (tag, _) = v in + let tag = Val.pr tag in + CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + ++ str " while type " ++ Val.pr wit ++ str " was expected.") + +let unbox wit v ans = match ans with +| None -> cast_error wit v +| Some x -> x + +let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with +| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) +| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) +| Val.Pair (tag1, tag2) -> + let (x, y) = unbox Val.typ_pair v (to_pair v) in + (prj tag1 x, prj tag2 y) +| Val.Base t -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> cast_error t v + | Some Refl -> x +let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with +| ExtraArg _ -> Geninterp.val_tag (topwit wit) +| ListArg t -> Val.List (tag_of_arg t) +| OptArg t -> Val.Opt (tag_of_arg t) +| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) + +let val_cast arg v = prj (tag_of_arg arg) v + +let cast (Topwit wit) v = val_cast wit v + end let is_variable env id = @@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v = | Some l -> let map n = ArgArg (coerce_to_int n) in List.map map l + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +(* Values for interpretation *) +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in + wit + +let pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Val.pr tag + +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) + +(* Displays a value *) +let pr_value env v = + let pr_with_env pr = + match env with + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) + +let error_ltac_variable ?loc id env v s = + CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index ce05d70e88..1fa5e3c076 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -42,6 +42,7 @@ sig val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** {5 Coercion functions} *) @@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type + +val error_ltac_variable : ?loc:Loc.t -> Id.t -> + (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type + +val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 42f2abd73c..566fc28733 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,3 +554,138 @@ let () = AnyEntry Pltac.tactic_arg; ] in register_grammars_by_name "tactic" entries + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu -> + match tu with + | TUlist1 l -> Ulist1(untype_user_symbol l) + | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s) + | TUlist0 l -> Ulist0(untype_user_symbol l) + | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s) + | TUopt(o) -> Uopt(untype_user_symbol o) + | TUentry a -> Uentry (Genarg.ArgT.Any a) + | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i) + +let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = + fun sign -> match sign with + | TyNil -> [] + | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' + | TyArg ((loc,(a,id)),sig') -> + TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg ((loc,a),sig') -> + TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + +let clause_of_ty_ml = function + | TyML (t,_) -> clause_of_sign t + +let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function + | TUentry a -> ExtraArg a + | TUentryl (a,l) -> ExtraArg a + | TUopt(o) -> OptArg (prj o) + | TUlist1 l -> ListArg (prj l) + | TUlist1sep (l,_) -> ListArg (prj l) + | TUlist0 l -> ListArg (prj l) + | TUlist0sep (l,_) -> ListArg (prj l) + +let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = + fun sign tac -> + match sign with + | TyNil -> + begin fun vals ist -> match vals with + | [] -> tac ist + | _ :: _ -> assert false + end + | TyIdent (s, sig') -> eval_sign sig' tac + | TyArg ((_loc,(a,id)), sig') -> + let f = eval_sign sig' in + begin fun tac vals ist -> match vals with + | [] -> assert false + | v :: vals -> + let v' = Taccoerce.Value.cast (topwit (prj a)) v in + f (tac v') vals ist + end tac + | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + +let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function + | TyML (t,tac) -> eval_sign t tac + +let is_constr_entry = function +| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr +| _ -> false + +let rec only_constr : type a. a ty_sig -> bool = function +| TyNil -> true +| TyIdent(_,_) -> false +| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false + +let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function +| TyNil -> [] +| TyIdent (_,s) -> mk_sign_vars s +| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s +| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let map = function + | Anonymous -> None + | Name id -> + let c = Id.Map.find id ist.Geninterp.lfun in + try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c) + with Taccoerce.CannotCoerceTo ty -> + Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac + +let tactic_extend plugin_name tacname ~level sign = + let open Tacexpr in + let ml_tactic_name = + { mltac_tactic = tacname; + mltac_plugin = plugin_name } + in + match sign with + | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> + (** The extension is only made of a name followed by constr entries: we do not + add any grammar nor printing rule and add it as a true Ltac definition. *) + (* + let patt = make_patt rem in + let vars = List.map make_var rem in + let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in + *) + let vars = mk_sign_vars s in + let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in + let tac = match s with + | TyNil -> eval ml_tac + (** Special handling of tactics without arguments: such tactics do not do + a Proofview.Goal.nf_enter to compute their arguments. It matters for some + whole-prof tactics like [shelve_unifiable]. *) + | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) + in + (** Arguments are not passed directly to the ML tactic in the TacML node, + the ML tactic retrieves its arguments in the [ist] environment instead. + This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true false id body in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin_name + | _ -> + let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); + Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 02e2f0f60e..3f804ee8d1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -67,3 +67,15 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.reference -> unit (** Display the absolute name of a tactic. *) + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cd9d9bac2c..991afe9c60 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -79,9 +79,6 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) -let base_val_typ wit = - match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") - let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -93,11 +90,6 @@ let safe_msgnl s = type value = Val.t -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Val.t list) list - (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl @@ -121,19 +113,6 @@ let combine_appl appl1 appl2 = | UnnamedAppl,a | a,UnnamedAppl -> a | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1) -(* Values for interpretation *) -type tacvalue = - | VFun of appl*ltac_trace * value Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of value Id.Map.t ref * glob_tactic_expr - -let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - let wit = Genarg.create_arg "tacvalue" in - let () = register_val0 wit None in - let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in - wit - let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v @@ -169,39 +148,6 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure - let cast_error wit v = - let pr_v = Pptactic.pr_value Pptactic.ltop v in - let Val.Dyn (tag, _) = v in - let tag = Val.pr tag in - user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag - ++ str " while type " ++ Val.pr wit ++ str " was expected.") - - let unbox wit v ans = match ans with - | None -> cast_error wit v - | Some x -> x - - let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with - | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) - | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) - | Val.Pair (tag1, tag2) -> - let (x, y) = unbox Val.typ_pair v (to_pair v) in - (prj tag1 x, prj tag2 y) - | Val.Base t -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> cast_error t v - | Some Refl -> x - - let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with - | ExtraArg _ -> val_tag wit - | ListArg t -> Val.List (tag_of_arg t) - | OptArg t -> Val.Opt (tag_of_arg t) - | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - - let val_cast arg v = prj (tag_of_arg arg) v - - let cast (Topwit wit) v = val_cast wit v - end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with | None -> DebugOff | Some level -> level -(** TODO: unify printing of generic Ltac values in case of coercion failure. *) - -(* Displays a value *) -let pr_value env v = - let pr_with_env pr = - match env with - | Some (env,sigma) -> pr env sigma - | None -> str "a value of type" ++ spc () ++ pr_argument_type v in - let open Genprint in - match generic_val_print v with - | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr_with_env pr - | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> - pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) - let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in @@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) -let error_ltac_variable ?loc id env v s = - user_err ?loc (str "Ltac variable " ++ Id.print id ++ - strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s ++ str".") - (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in - try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s + try coerce v with CannotCoerceTo s -> + Taccoerce.error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid @@ -2090,27 +2017,6 @@ let _ = in Pretyping.register_constr_interp0 wit_tactic eval -(** Used in tactic extension **) - -let dummy_id = Id.of_string "_" - -let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let map = function - | Anonymous -> None - | Name id -> - let c = Id.Map.find id ist.lfun in - try Some (coerce_to_closed_constr env c) - with CannotCoerceTo ty -> - error_ltac_variable dummy_id (Some (env,sigma)) c ty - in - let args = List.map_filter map vars in - tac args ist - end in - tac - let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 3f3b8e5558..bd44bdbea4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : ?loc:Loc.t -> Id.t -> - (Environ.env * Evd.evar_map) option -> value -> string -> 'a - -(** Transforms a constr-expecting tactic into a tactic finding its arguments in - the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Name.t list -> - (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic - val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index c8112eaa99..4ac49adb90 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Ltac_plugin +open Stdarg DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 43c29a08a8..f049963f1c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1193,7 +1193,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in - let ucst = Evd.union_evar_universe_context ucst ucst' in + let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else let gl, pty = pfe_type_of gl p in false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 859513d5cd..57635edac4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -216,7 +216,7 @@ let same_proj sigma t1 t2 = let all_ok _ _ = true let fake_pmatcher_end () = - mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp) + mkProp, L2R, (Evd.empty, UState.empty, mkProp) let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 62c35d6dfa..33b18001c9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -361,7 +361,7 @@ let unif_end env sigma0 ise0 pt ok = if ise2 == ise1 then (s, uc, t) else let s, uc', t = nf_open_term sigma0 ise2 t in - s, Evd.union_evar_universe_context uc uc', t + s, UState.union uc uc', t let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in @@ -1268,7 +1268,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context + | None -> do_subst env0 concl0 concl0 1, UState.empty | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in |