aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-09 15:33:45 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-09 15:33:45 +0200
commitd5534aab708e5d3bd6c3633dc9d028016eeb3076 (patch)
treeb74bcffce9869dc8aaec115e4614fb7e89ac5a3d /pretyping
parent73a858469479651cc4baf631a45a9ff1d69d0c66 (diff)
parentd19e8bafe6cc18cc47bbb3e3f7aa0d2d719014c0 (diff)
Merge PR #1109: Handle some misc todos
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/nativenorm.ml50
-rw-r--r--pretyping/retyping.ml1
2 files changed, 4 insertions, 47 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 39c2ceeba..1038945c1 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -5,13 +5,11 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open CErrors
open Term
open Vars
open Environ
open Reduction
-open Univ
open Declarations
open Names
open Inductive
@@ -20,8 +18,6 @@ open Nativecode
open Nativevalues
open Context.Rel.Declaration
-module RelDecl = Context.Rel.Declaration
-
(** This module implements normalization by evaluation to OCaml code *)
exception Find_at of int
@@ -177,44 +173,6 @@ let build_case_type dep p realargs c =
if dep then mkApp(mkApp(p, realargs), [|c|])
else mkApp(p, realargs)
-(* TODO move this function *)
-let type_of_rel env n =
- env |> lookup_rel n |> RelDecl.get_type |> lift n
-
-let type_of_prop = mkSort type1_sort
-
-let type_of_sort s =
- match s with
- | Prop _ -> type_of_prop
- | Type u -> mkType (Univ.super u)
-
-let type_of_var env id =
- let open Context.Named.Declaration in
- try env |> lookup_named id |> get_type
- with Not_found ->
- anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")
-
-let sort_of_product env domsort rangsort =
- match (domsort, rangsort) with
- (* Product rule (s,Prop,Prop) *)
- | (_, Prop Null) -> rangsort
- (* Product rule (Prop/Set,Set,Set) *)
- | (Prop _, Prop Pos) -> rangsort
- (* Product rule (Type,Set,?) *)
- | (Type u1, Prop Pos) ->
- if is_impredicative_set env then
- (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
- rangsort
- else
- (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
- Type (sup u1 type0_univ)
- (* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Pos, Type u2) -> Type (sup type0_univ u2)
- (* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Null, Type _) -> rangsort
- (* Product rule (Type_i,Type_i,Type_i) *)
- | (Type u1, Type u2) -> Type (sup u1 u2)
-
(* normalisation of values *)
let branch_of_switch lvl ans bs =
@@ -328,15 +286,15 @@ and nf_atom_type env sigma atom =
match atom with
| Arel i ->
let n = (nb_rel env - i) in
- mkRel n, type_of_rel env n
+ mkRel n, Typeops.type_of_relative env n
| Aconstant cst ->
mkConstU cst, Typeops.type_of_constant_in env cst
| Aind ind ->
mkIndU ind, Inductiveops.type_of_inductive env ind
| Asort s ->
- mkSort s, type_of_sort s
+ mkSort s, Typeops.type_of_sort s
| Avar id ->
- mkVar id, type_of_var env id
+ mkVar id, Typeops.type_of_variable env id
| Acase(ans,accu,p,bs) ->
let a,ta = nf_accu_type env sigma accu in
let ((mind,_),u as ind),allargs = find_rectype_a env ta in
@@ -387,7 +345,7 @@ and nf_atom_type env sigma atom =
let vn = mk_rel_accu (nb_rel env) in
let env = push_rel (LocalAssum (n,dom)) env in
let codom,s2 = nf_type_sort env sigma (codom vn) in
- mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+ mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
| Aevar(ev,ty) ->
let ty = nf_type env sigma ty in
mkEvar ev, ty
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 079524f34..56f8b33e0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -214,7 +214,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty
| Const (cst, u) ->
let t = constant_type_in env (cst, EInstance.kind sigma u) in
- (* TODO *)
sigma, EConstr.of_constr t
| Var id -> sigma, type_of_var env id
| Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))