diff options
Diffstat (limited to 'plugins/xml/doubleTypeInference.ml')
| -rw-r--r-- | plugins/xml/doubleTypeInference.ml | 273 |
1 files changed, 0 insertions, 273 deletions
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml deleted file mode 100644 index c22c16f0..00000000 --- a/plugins/xml/doubleTypeInference.ml +++ /dev/null @@ -1,273 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * The HELM Project / The EU MoWGLI Project *) -(* * University of Bologna *) -(************************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(* *) -(* Copyright (C) 2000-2004, HELM Team. *) -(* http://helm.cs.unibo.it *) -(************************************************************************) - -(*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *) -type types = {synthesized : Term.types ; expected : Term.types option};; - -let prerr_endline _ = ();; - -let cprop = - let module N = Names in - N.make_con - (N.MPfile - (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.make_dirpath []) - (N.mk_label "CProp") -;; - -let whd_betadeltaiotacprop env _evar_map ty = - let module R = Glob_term in - let module C = Closure in - let module CR = C.RedFlags in - (*** CProp is made Opaque ***) - let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in - C.whd_val (C.create_clos_infos flags env) (C.inject ty) -;; - - -(* Code similar to the code in the Typing module, but: *) -(* - the term is already assumed to be well typed *) -(* - some checks have been removed *) -(* - both the synthesized and expected types of every *) -(* node are computed (Coscoy's double type inference) *) - -let assumption_of_judgment env sigma j = - Typeops.assumption_of_judgment env (Evarutil.j_nf_evar sigma j) -;; - -let type_judgment env sigma j = - Typeops.type_judgment env (Evarutil.j_nf_evar sigma j) -;; - -let type_judgment_cprop env sigma j = - match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with - | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s } - | _ -> None (* None means the CProp constant *) -;; - -let double_type_of env sigma cstr expectedty subterms_to_types = - (*CSC: the code is inefficient because judgments are created just to be *) - (*CSC: destroyed using Environ.j_type. Moreover I am pretty sure that the *) - (*CSC: functions used do checks that we do not need *) - let rec execute env sigma cstr expectedty = - let module T = Term in - let module E = Environ in - (* the type part is the synthesized type *) - let judgement = - match T.kind_of_term cstr with - T.Meta n -> - Util.error - "DoubleTypeInference.double_type_of: found a non-instanciated goal" - - | T.Evar ((n,l) as ev) -> - let ty = Unshare.unshare (Evd.existential_type sigma ev) in - let jty = execute env sigma ty None in - let jty = assumption_of_judgment env sigma jty in - let evar_context = - E.named_context_of_val (Evd.find sigma n).Evd.evar_hyps in - let rec iter actual_args evar_context = - match actual_args,evar_context with - [],[] -> () - | he1::tl1,(n,_,ty)::tl2 -> - (* for side-effects *) - let _ = execute env sigma he1 (Some ty) in - let tl2' = - List.map - (function (m,bo,ty) -> - (* Warning: the substitution should be performed also on bo *) - (* This is not done since bo is not used later yet *) - (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty)) - ) tl2 - in - iter tl1 tl2' - | _,_ -> assert false - in - (* for side effects only *) - iter (List.rev (Array.to_list l)) (List.rev evar_context) ; - E.make_judge cstr jty - - | T.Rel n -> - Typeops.judge_of_relative env n - - | T.Var id -> - Typeops.judge_of_variable env id - - | T.Const c -> - E.make_judge cstr (Typeops.type_of_constant env c) - - | T.Ind ind -> - E.make_judge cstr (Inductiveops.type_of_inductive env ind) - - | T.Construct cstruct -> - E.make_judge cstr (Inductiveops.type_of_constructor env cstruct) - - | T.Case (ci,p,c,lf) -> - let expectedtype = - Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in - let cj = execute env sigma c (Some expectedtype) in - let pj = execute env sigma p None in - let (expectedtypes,_,_) = - let indspec = Inductive.find_rectype env cj.Environ.uj_type in - Inductive.type_case_branches env indspec pj cj.Environ.uj_val - in - let lfj = - execute_array env sigma lf - (Array.map (function x -> Some x) expectedtypes) in - let (j,_) = Typeops.judge_of_case env ci pj cj lfj in - j - - | T.Fix ((vn,i as vni),recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in - E.make_judge (T.mkFix fix) tys.(i) - - | T.CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let cofix = (i,recdef') in - E.make_judge (T.mkCoFix cofix) tys.(i) - - | T.Sort (T.Prop c) -> - Typeops.judge_of_prop_contents c - - | T.Sort (T.Type u) -> -(*CSC: In case of need, I refresh the universe. But exportation of the *) -(*CSC: right universe level information is destroyed. It must be changed *) -(*CSC: again once Judicael will introduce his non-bugged algebraic *) -(*CSC: universes. *) -(try - Typeops.judge_of_type u - with e when e <> Sys.Break -> - (* Successor of a non universe-variable universe anomaly *) - (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ; - Typeops.judge_of_type (Termops.new_univ ()) -) - - | T.App (f,args) -> - let expected_head = - Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma f) in - let j = execute env sigma f (Some expected_head) in - let expected_args = - let rec aux typ = - function - [] -> [] - | hj::restjl -> - match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with - T.Prod (_,c1,c2) -> - (Some (Reductionops.nf_beta sigma c1)) :: - (aux (T.subst1 hj c2) restjl) - | _ -> assert false - in - Array.of_list (aux j.Environ.uj_type (Array.to_list args)) - in - let jl = execute_array env sigma args expected_args in - let (j,_) = Typeops.judge_of_apply env j jl in - j - - | T.Lambda (name,c1,c2) -> - let j = execute env sigma c1 None in - let var = type_judgment env sigma j in - let env1 = E.push_rel (name,None,var.E.utj_val) env in - let expectedc2type = - match expectedty with - None -> None - | Some ety -> - match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with - T.Prod (_,_,expected_target_type) -> - Some (Reductionops.nf_beta sigma expected_target_type) - | _ -> assert false - in - let j' = execute env1 sigma c2 expectedc2type in - Typeops.judge_of_abstraction env1 name var j' - - | T.Prod (name,c1,c2) -> - let j = execute env sigma c1 None in - let varj = type_judgment env sigma j in - let env1 = E.push_rel (name,None,varj.E.utj_val) env in - let j' = execute env1 sigma c2 None in - (match type_judgment_cprop env1 sigma j' with - Some varj' -> Typeops.judge_of_product env name varj varj' - | None -> - (* CProp found *) - { Environ.uj_val = T.mkProd (name, j.Environ.uj_val, j'.Environ.uj_val); - Environ.uj_type = T.mkConst cprop }) - - | T.LetIn (name,c1,c2,c3) -> -(*CSC: What are the right expected types for the source and *) -(*CSC: target of a LetIn? None used. *) - let j1 = execute env sigma c1 None in - let j2 = execute env sigma c2 None in - let j2 = type_judgment env sigma j2 in - let env1 = - E.push_rel (name,Some j1.E.uj_val,j2.E.utj_val) env - in - let j3 = execute env1 sigma c3 None in - Typeops.judge_of_letin env name j1 j2 j3 - - | T.Cast (c,k,t) -> - let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in - let tj = execute env sigma t None in - let tj = type_judgment env sigma tj in - let j, _ = Typeops.judge_of_cast env cj k tj in - j - in - let synthesized = E.j_type judgement in - let synthesized' = Reductionops.nf_beta sigma synthesized in - let types,res = - match expectedty with - None -> - (* No expected type *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when Term.eq_constr synthesized' ty -> - (* The expected type is synthactically equal to the *) - (* synthesized type. Let's forget it. *) - (* Note: since eq_constr is up to casts, it is better *) - (* to keep the expected type, since it can bears casts *) - (* that change the innersort to CProp *) - {synthesized = ty ; expected = None}, ty - | Some expectedty' -> - {synthesized = synthesized' ; expected = Some expectedty'}, - expectedty' - in -(*CSC: debugging stuff to be removed *) -if Acic.CicHash.mem subterms_to_types cstr then - (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ; - Acic.CicHash.add subterms_to_types cstr types ; - E.make_judge cstr res - - - and execute_recdef env sigma (names,lar,vdef) = - let length = Array.length lar in - let larj = - execute_array env sigma lar (Array.make length None) in - let lara = Array.map (assumption_of_judgment env sigma) larj in - let env1 = Environ.push_rec_types (names,lara,vdef) env in - let expectedtypes = - Array.map (function i -> Some (Term.lift length i)) lar - in - let vdefj = execute_array env1 sigma vdef expectedtypes in - let vdefv = Array.map Environ.j_val vdefj in - (names,lara,vdefv) - - and execute_array env sigma v expectedtypes = - let jl = - execute_list env sigma (Array.to_list v) (Array.to_list expectedtypes) - in - Array.of_list jl - - and execute_list env sigma = - List.map2 (execute env sigma) - -in - ignore (execute env sigma cstr expectedty) -;; |