From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- plugins/extraction/extract_env.ml | 8 ++++---- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 31 ++++++++++++++++--------------- plugins/extraction/extraction.mli | 2 +- plugins/extraction/table.mli | 2 +- 5 files changed, 23 insertions(+), 22 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3c46d5c43..bc84df76b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -7,7 +7,7 @@ (************************************************************************) open Miniml -open Term +open Constr open Declarations open Names open ModPath @@ -138,7 +138,7 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with | Def lbody -> - (match kind_of_term (Mod_subst.force_constr lbody) with + (match Constr.kind (Mod_subst.force_constr 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) @@ -146,8 +146,8 @@ let check_fix env cb i = let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal eq_constr ca1 ca2 && - Array.equal eq_constr ta1 ta2 + Array.equal Constr.equal ca1 ca2 && + Array.equal Constr.equal ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7bbb825b1..dd8617738 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,4 +34,4 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Term.constr -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a227478d0..47e812319 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -10,6 +10,7 @@ open Util open Names open Term +open Constr open Vars open Declarations open Declareops @@ -81,7 +82,7 @@ let whd_betaiotazeta t = let rec flag_of_type env t : flag = let t = whd_all env t in - match kind_of_term t with + 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) | Sort _ -> (Info,TypeScheme) @@ -111,14 +112,14 @@ let push_rel_assum (n, t) env = (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env 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) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env 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 @@ -145,7 +146,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env 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 @@ -153,7 +154,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env 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 @@ -207,7 +208,7 @@ let parse_ind_args si args relmax = | [] -> Int.Map.empty | Kill _ :: s -> parse (i+1) j s | Keep :: s -> - (match kind_of_term args.(i-1) with + (match Constr.kind args.(i-1) with | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s) | _ -> parse (i+1) (j+1) s) in parse 1 1 si @@ -224,7 +225,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta c) with + match Constr.kind (whd_betaiotazeta c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -299,7 +300,7 @@ let rec extract_type env db j c 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 (Term.mkProj (Projection.unfold p, t)) args + else extract_type env db j (mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false @@ -331,7 +332,7 @@ and extract_type_scheme env db c p = if Int.equal p 0 then extract_type env db 0 c [] else let c = whd_betaiotazeta c in - match kind_of_term c with + match Constr.kind c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> @@ -415,8 +416,8 @@ and extract_really_ind env kn mib = let t = snd (decompose_prod_n npar types.(j)) in let prods,head = dest_prod epar t in let nprods = List.length prods in - let args = match kind_of_term head with - | App (f,args) -> args (* [kind_of_term f = Ind ip] *) + let args = match Constr.kind head with + | App (f,args) -> args (* [Constr.kind f = Ind ip] *) | _ -> [||] in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in @@ -444,7 +445,7 @@ and extract_really_ind env kn mib = if Option.is_empty mib.mind_record then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) - let rec names_prod t = match kind_of_term t with + let rec names_prod t = match Constr.kind t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t | Cast(t,_,_) -> names_prod t @@ -503,7 +504,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env c) with + match Constr.kind (whd_all env 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 @@ -564,7 +565,7 @@ let record_constant_type env kn opt_typ = (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) let rec extract_term env mle mlt c args = - match kind_of_term c with + match Constr.kind c with | App (f,a) -> extract_term env mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> @@ -874,7 +875,7 @@ let decomp_lams_eta_n n m env c t = (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match kind_of_term c with +let rec gentypvar_ok c = match Constr.kind c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index e1d43f340..b15b88ed2 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -9,7 +9,7 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Term +open Constr open Declarations open Environ open Miniml diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index cc93f294b..e52e419fd 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -180,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) -val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t +val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t val is_custom : global_reference -> bool val is_inline_custom : global_reference -> bool -- cgit v1.2.3