From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- plugins/extraction/extraction.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f53..85cacecdbb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast c) + Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) (*S Generation of flags and signatures. *) @@ -887,7 +887,7 @@ 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 body in + and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in if n <= m then decompose_lam_n n body else let s,s' = List.chop m s in -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- plugins/extraction/extraction.ml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 85cacecdbb..6ca34036af 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -74,7 +74,7 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_all env none t in + let t = whd_all env none (EConstr.of_constr t) in match kind_of_term 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) @@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*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 none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -135,7 +135,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 none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -143,7 +143,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -214,7 +214,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta Evd.empty c) with + match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -297,7 +297,7 @@ and extract_type_app env 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 (type_of env c))) in + let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in let db = iterate (fun l -> 0 :: l) p db in (extract_type_scheme env db c p) :: a else a) @@ -316,12 +316,12 @@ and extract_type_app env db (r,s) args = 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 Evd.empty c in + let c = whd_betaiotazeta none (EConstr.of_constr c) in match kind_of_term c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> - let rels = fst (splay_prod env none (type_of env c)) in + let rels = fst (splay_prod env none (EConstr.of_constr (type_of env 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 @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env none c) with + match kind_of_term (whd_all env none (EConstr.of_constr 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 @@ -846,7 +846,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = 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 t) in + 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,c)) rels in let rels',c = decompose_lam c in let d = n - m in -- cgit v1.2.3 From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- plugins/extraction/extraction.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6ca34036af..42a8cac69b 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) let sort_of env 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 none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) (*S Generation of flags and signatures. *) @@ -595,7 +595,7 @@ let rec extract_term env mle mlt c args = | Construct (cp,_) -> extract_cons_app env mle mlt cp args | Proj (p, c) -> - let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in extract_term env mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) -- cgit v1.2.3 From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Nov 2016 11:39:27 +0100 Subject: Unification API using EConstr. --- plugins/extraction/extraction.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 42a8cac69b..0c4fa70555 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -99,6 +99,9 @@ let is_info_scheme env t = match flag_of_type env t with | (Info, TypeScheme) -> true | _ -> false +let push_rel_assum (n, t) env = + Environ.push_rel (LocalAssum (n, t)) env + (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = -- cgit v1.2.3 From 536026f3e20f761e8ef366ed732da7d3b626ac5e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 15:39:01 +0100 Subject: Cleaning up opening of the EConstr module in pretyping folder. --- plugins/extraction/extraction.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0c4fa70555..6559aeb082 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -599,6 +599,7 @@ let rec extract_term env mle mlt c args = extract_cons_app env 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 | Rel n -> (* As soon as the expected [mlt] for the head is known, *) -- cgit v1.2.3 From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:07:35 +0100 Subject: Inv API using EConstr. --- plugins/extraction/extraction.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6559aeb082..e9fd407225 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -325,6 +325,7 @@ and extract_type_scheme env db c p = extract_type_scheme (push_rel_assum (n,t) env) 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 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 -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- plugins/extraction/extraction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e9fd407225..4601571306 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) (*S Generation of flags and signatures. *) -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- plugins/extraction/extraction.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4601571306..61547f96d9 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -70,11 +70,17 @@ 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 none (EConstr.of_constr t) in + let t = whd_all env t in match kind_of_term 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) @@ -105,14 +111,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 none (EConstr.of_constr c)) with + match kind_of_term (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 none (EConstr.of_constr c)) with + match kind_of_term (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 @@ -138,7 +144,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 none (EConstr.of_constr c)) with + match kind_of_term (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 @@ -146,7 +152,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_all env none (EConstr.of_constr c)) with + match kind_of_term (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 @@ -217,7 +223,7 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = - match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with + match kind_of_term (whd_betaiotazeta c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -319,7 +325,7 @@ and extract_type_app env db (r,s) args = 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 none (EConstr.of_constr c) in + let c = whd_betaiotazeta c in match kind_of_term c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) @@ -492,7 +498,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_all env none (EConstr.of_constr c)) with + match kind_of_term (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 -- cgit v1.2.3 From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 61547f96d9..7b7e746f20 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,7 +42,7 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) let sort_of env c = let polyprop = (lang() == Haskell) in -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7b7e746f20..8744eacd3f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -858,7 +858,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = 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,c)) rels 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 d = n - m in (* we'd better keep rels' as long as possible. *) -- cgit v1.2.3