diff options
| -rw-r--r-- | dev/doc/changes.txt | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 4 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 1 | ||||
| -rw-r--r-- | pretyping/typing.ml | 154 | ||||
| -rw-r--r-- | pretyping/typing.mli | 11 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 6 |
10 files changed, 111 insertions, 77 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7c5b03457..ad1ee8630 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,10 @@ = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= +** Obsolete functions in typing.ml + +For mtype_of, msort_of, mcheck, now use type_of, sort_of, check + ** Renaming functions renamed concrete_name -> compute_displayed_name_in diff --git a/dev/printers.mllib b/dev/printers.mllib index 78903b8df..e8ec10c5c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -76,11 +76,11 @@ Inductiveops Retyping Cbv Pretype_errors -Typing Evarutil Term_dnet Recordops Evarconv +Typing Pattern Matching Tacred diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 370904a68..b43e6e999 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -17,8 +17,6 @@ open Reduction open Reductionops open Termops open Environ -open Typing -open Classops open Recordops open Evarutil open Libnames diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index e847894a5..cea33c1e9 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -7,15 +7,15 @@ Inductiveops Retyping Cbv Pretype_errors -Typing Evarutil Term_dnet Recordops +Evarconv +Typing Rawterm Pattern Matching Tacred -Evarconv Typeclasses_errors Typeclasses Classops diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 13f2aef26..d94da115a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -18,7 +18,6 @@ open Termops open Typeops open Libobject open Library -open Classops open Mod_subst open Reductionops diff --git a/pretyping/typing.ml b/pretyping/typing.ml index f4d032bf1..831787a06 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -35,54 +35,93 @@ let inductive_type_knowing_parameters env ind jl = let paramstyp = Array.map (fun j -> j.uj_type) jl in Inductive.type_of_inductive_knowing_parameters env mip paramstyp +let e_judge_of_apply env evdref funj argjv = + let rec apply_rec n typ = function + | [] -> + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } + | hj::restjl -> + match kind_of_term (whd_betadeltaiota env !evdref typ) with + | Prod (_,c1,c2) -> + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv + | _ -> + error_cant_apply_not_functional env funj argjv + in + apply_rec 1 funj.uj_type (Array.to_list argjv) + +let check_branch_types env evdref cj (lfj,explft) = + if Array.length lfj <> Array.length explft then + error_number_branches env cj (Array.length explft); + for i = 0 to Array.length explft - 1 do + if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then + error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i) + done + +let e_judge_of_case env evdref ci pj cj lfj = + let indspec = + try find_mrectype env !evdref cj.uj_type + with Not_found -> error_case_not_inductive env cj in + let _ = check_case_info env (fst indspec) ci in + let (bty,rslty,univ) = type_case_branches env indspec pj cj.uj_val in + check_branch_types env evdref cj (lfj,bty); + { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty } + +let e_judge_of_cast env evdref cj k tj = + let expected_type = tj.utj_val in + if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then + error_actual_type env cj expected_type; + { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } + (* The typing machine without information, without universes but with existential variables. *) (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) -let rec execute env evd cstr = +let rec execute env evdref cstr = match kind_of_term cstr with | Meta n -> - { uj_val = cstr; uj_type = nf_evar evd (meta_type evd n) } + { uj_val = cstr; uj_type = meta_type !evdref n } | Evar ev -> - let sigma = evd in - let ty = Evd.existential_type sigma ev in - let jty = execute env evd (nf_evar evd ty) in + let ty = Evd.existential_type !evdref ev in + let jty = execute env evdref (whd_evar !evdref ty) in let jty = assumption_of_judgment env jty in { uj_val = cstr; uj_type = jty } | Rel n -> - j_nf_evar evd (judge_of_relative env n) + judge_of_relative env n | Var id -> - j_nf_evar evd (judge_of_variable env id) + judge_of_variable env id | Const c -> - make_judge cstr (nf_evar evd (type_of_constant env c)) + make_judge cstr (type_of_constant env c) | Ind ind -> - make_judge cstr (nf_evar evd (type_of_inductive env ind)) + make_judge cstr (type_of_inductive env ind) | Construct cstruct -> - make_judge cstr - (nf_evar evd (type_of_constructor env cstruct)) + make_judge cstr (type_of_constructor env cstruct) | Case (ci,p,c,lf) -> - let cj = execute env evd c in - let pj = execute env evd p in - let lfj = execute_array env evd lf in - let (j,_) = judge_of_case env ci pj cj lfj in - j + let cj = execute env evdref c in + let pj = execute env evdref p in + let lfj = execute_array env evdref lf in + e_judge_of_case env evdref ci pj cj lfj | Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evd recdef in + let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in check_fix env fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env evd recdef in + let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) @@ -94,96 +133,93 @@ let rec execute env evd cstr = judge_of_type u | App (f,args) -> - let jl = execute_array env evd args in + let jl = execute_array env evdref args in let j = match kind_of_term f with | Ind ind -> (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind - (jv_nf_evar evd jl)) + (jv_nf_evar !evdref jl)) | Const cst -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst - (jv_nf_evar evd jl)) + (jv_nf_evar !evdref jl)) | _ -> - execute env evd f + execute env evdref f in - fst (judge_of_apply env j jl) + e_judge_of_apply env evdref j jl | Lambda (name,c1,c2) -> - let j = execute env evd c1 in + let j = execute env evdref c1 in let var = type_judgment env j in let env1 = push_rel (name,None,var.utj_val) env in - let j' = execute env1 evd c2 in + let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute env evd c1 in + let j = execute env evdref c1 in let varj = type_judgment env j in let env1 = push_rel (name,None,varj.utj_val) env in - let j' = execute env1 evd c2 in + let j' = execute env1 evdref c2 in let varj' = type_judgment env1 j' in judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute env evd c1 in - let j2 = execute env evd c2 in + let j1 = execute env evdref c1 in + let j2 = execute env evdref c2 in let j2 = type_judgment env j2 in let _ = judge_of_cast env j1 DEFAULTcast j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in - let j3 = execute env1 evd c3 in + let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 | Cast (c,k,t) -> - let cj = execute env evd c in - let tj = execute env evd t in + let cj = execute env evdref c in + let tj = execute env evdref t in let tj = type_judgment env tj in - let j, _ = judge_of_cast env cj k tj in - j + e_judge_of_cast env evdref cj k tj -and execute_recdef env evd (names,lar,vdef) = - let larj = execute_array env evd lar in +and execute_recdef env evdref (names,lar,vdef) = + let larj = execute_array env evdref lar in let lara = Array.map (assumption_of_judgment env) larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 evd vdef in + let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in let _ = type_fixpoint env1 names lara vdefj in (names,lara,vdefv) -and execute_array env evd = Array.map (execute env evd) +and execute_array env evdref = Array.map (execute env evdref) -and execute_list env evd = List.map (execute env evd) +and execute_list env evdref = List.map (execute env evdref) -let mcheck env evd c t = - let sigma = evd in - let j = execute env evd (nf_evar sigma c) in - if not (is_conv_leq env sigma j.uj_type t) then - error_actual_type env j (nf_evar sigma t) +let check env evd c t = + let evdref = ref evd in + let j = execute env evdref c in + if not (Evarconv.e_cumul env evdref j.uj_type t) then + error_actual_type env j (nf_evar evd t) (* Type of a constr *) -let mtype_of env evd c = - let j = execute env evd (nf_evar evd c) in +let type_of env evd c = + let j = execute env (ref evd) c in (* We are outside the kernel: we take fresh universes *) (* to avoid tactics and co to refresh universes themselves *) Termops.refresh_universes j.uj_type -let msort_of env evd c = - let j = execute env evd (nf_evar evd c) in +(* Sort of a type *) + +let sort_of env evd c = + let j = execute env (ref evd) c in let a = type_judgment env j in a.utj_type -let type_of env sigma c = - mtype_of env (Evd.create_evar_defs sigma) c -let sort_of env sigma c = - msort_of env (Evd.create_evar_defs sigma) c -let check env sigma c = - mcheck env (Evd.create_evar_defs sigma) c - -(* The typed type of a judgment. *) +(* Try to solve the existential variables by typing *) -let mtype_of_type env evd constr = - let j = execute env evd (nf_evar evd constr) in - assumption_of_judgment env j +let solve_evars env evd c = + let evdref = ref evd in + let c = (execute env evdref c).uj_val in + (* side-effect on evdref *) + nf_evar !evdref c + diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 9a40d01ec..e3b3e9482 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -21,14 +21,11 @@ open Evd val type_of : env -> evar_map -> constr -> types (* Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> sorts -(* Typecheck a term has a given type (assuming the type is OK *) +(* Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> unit -(* The same but with metas... *) -val mtype_of : env -> evar_map -> constr -> types -val msort_of : env -> evar_map -> types -> sorts -val mcheck : env -> evar_map -> constr -> types -> unit +(* Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types -(* unused typing function... *) -val mtype_of_type : env -> evar_map -> types -> types +(* Solve existential variables using typing *) +val solve_evars : env -> evar_map -> constr -> constr diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ea491b9da..648dcee0c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -61,7 +61,7 @@ let abstract_list_all env evd typ c l = let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in try - if is_conv_leq env evd (Typing.mtype_of env evd p) typ then p + if is_conv_leq env evd (Typing.type_of env evd p) typ then p else error "abstract_list_all" with UserError _ | Type_errors.TypeError _ -> error_cannot_find_well_typed_abstraction env evd p l diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 8495b623f..b0645744b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -269,7 +269,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 + Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 95b34b8d9..e08e5e9ed 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -268,7 +268,7 @@ let decompose_applied_relation env sigma c left2right = | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 + Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 in if not (evd_convertible env eqclause.evd ty1 ty2) then None else @@ -352,8 +352,8 @@ let unify_eqn env sigma hypinfo t = let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel and prf = nf (Clenv.clenv_value env') in - let ty1 = Typing.mtype_of env'.env env'.evd c1 - and ty2 = Typing.mtype_of env'.env env'.evd c2 + let ty1 = Typing.type_of env'.env env'.evd c1 + and ty2 = Typing.type_of env'.env env'.evd c2 in if convertible env env'.evd ty1 ty2 then ( if occur_meta prf then |