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. --- printing/prettyp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b19f8376c0..ab0ce7e56e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,7 @@ let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in @@ -594,7 +594,7 @@ let gallina_print_context with_values = prec let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma trm in + let ntrm = red_fun env sigma (EConstr.of_constr trm) in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) -- 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. --- printing/prettyp.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index ab0ce7e56e..e66d3aafed 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,7 +73,8 @@ let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in + let ccl = EConstr.Unsafe.to_constr ccl in it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in @@ -595,6 +596,7 @@ let gallina_print_context with_values = let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = let ntrm = red_fun env sigma (EConstr.of_constr trm) in + let ntrm = EConstr.Unsafe.to_constr ntrm in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) -- cgit v1.2.3 From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- printing/prettyp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e66d3aafed..e2c0f55f8f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -75,7 +75,7 @@ let print_ref reduce ref = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in let ccl = EConstr.Unsafe.to_constr ccl - in it_mkProd_or_LetIn ccl ctx + in Term.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in -- cgit v1.2.3 From 778e863b77bcafc8ed339dd02226e85e5fee2532 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 11:36:09 +0100 Subject: Removing compatibility layers related to printing. --- printing/prettyp.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e2c0f55f8f..93970512da 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -42,8 +42,8 @@ type object_pr = { print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds; } let gallina_print_module = print_module @@ -433,8 +433,8 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_lconstr_env env sigma trm ++ fnl () ++ - str " : " ++ pr_ltype_env env sigma typ) + (pr_leconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that @@ -595,8 +595,7 @@ let gallina_print_context with_values = prec let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma (EConstr.of_constr trm) in - let ntrm = EConstr.Unsafe.to_constr ntrm in + let ntrm = red_fun env sigma trm in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) @@ -643,6 +642,8 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} = let print_safe_judgment env sigma j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in + let trm = EConstr.of_constr trm in + let typ = EConstr.of_constr typ in print_typed_value_in_env env sigma (trm, typ) (*********************) @@ -762,7 +763,9 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> + let open EConstr in let ty = Universes.unsafe_type_of_global gr in + let ty = EConstr.of_constr ty in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl -- 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. --- printing/prettyp.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 93970512da..64c7c0ba5e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,11 +71,11 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in + let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in - let ccl = EConstr.Unsafe.to_constr ccl - in Term.it_mkProd_or_LetIn ccl ctx + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in @@ -85,7 +85,7 @@ let print_ref reduce ref = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_universe_ctx sigma univs) (********************************) -- cgit v1.2.3