diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/xml/doubleTypeInference.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/xml/doubleTypeInference.ml')
-rw-r--r-- | plugins/xml/doubleTypeInference.ml | 272 |
1 files changed, 272 insertions, 0 deletions
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml new file mode 100644 index 00000000..f8921aec --- /dev/null +++ b/plugins/xml/doubleTypeInference.ml @@ -0,0 +1,272 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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 = Rawterm 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 _ -> (* 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) +;; |