From: Claudio Sacerdoti Coen Date: Mon, 10 Jun 2002 17:39:19 +0000 (+0000) Subject: * doubleTypeInference.ml* added. For now, it just computes the synthesized type. X-Git-Tag: V_0_3_0_debian_8~54 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cedc0cfe0ea81f94ac8b88b71d8f855a33329593;p=helm.git * doubleTypeInference.ml* added. For now, it just computes the synthesized type. The expected type is expected soon ;-) * great performance improvement. For example, the rendering of limit_plus is now "only" 30s (was 50s) --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 5a677d73a..7d0186948 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,7 +1,9 @@ proofEngine.cmo: proofEngineReduction.cmo proofEngine.cmx: proofEngineReduction.cmx -cic2acic.cmo: cic2acic.cmi -cic2acic.cmx: cic2acic.cmi +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 44c9887f7..8a9c5e535 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -15,12 +15,13 @@ all: gTopLevel opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ - cic2acic.ml cic2acic.mli logicalOperations.ml sequentPp.ml \ - mquery.mli mquery.ml gTopLevel.ml + doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ + cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \ + mquery.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ - cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \ - mquery.cmo gTopLevel.cmo + cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \ + logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index ffe9dbd4d..7b9511da1 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -53,9 +53,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let module T = CicTypeChecker in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in + let terms_to_types = DoubleTypeInference.double_type_of metasenv context t in let rec aux computeinnertypes father context tt = let fresh_id'' = fresh_id' father tt in - let aux' = aux true (Some fresh_id'') in + (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) + let aux' = aux computeinnertypes (Some fresh_id'') in (* First of all we compute the inner type and the inner sort *) (* of the term. They may be useful in what follows. *) (*CSC: This is a very inefficient way of computing inner types *) @@ -71,11 +73,19 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let ainnertype,innertype,innersort = (*CSC: Here we need the algorithm for Coscoy's double type-inference *) (*CSC: (expected type + inferred type). Just for now we use the usual *) -(*CSC: type-inference, but the result is very poort. As a very weak *) +(*CSC: type-inference, but the result is very poor. As a very weak *) (*CSC: patch, I apply whd to the computed type. Full beta *) (*CSC: reduction would be a much better option. *) let innertype = - CicReduction.whd context (T.type_of_aux' metasenv context tt) + if computeinnertypes then + let {DoubleTypeInference.synthesized = synthesized} = + DoubleTypeInference.CicHash.find terms_to_types tt + in + synthesized + else + (* We are already in an inner-type and Coscoy's double *) + (* type inference algorithm has not been applied. *) + CicReduction.whd context (T.type_of_aux' metasenv context tt) in let innersort = T.type_of_aux' metasenv context innertype in let ainnertype = @@ -203,8 +213,6 @@ let acic_of_cic_context metasenv context t = ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; -exception Found of (Cic.name * Cic.context_entry) list;; - let acic_object_of_cic_object obj = let module C = Cic in let ids_to_terms = Hashtbl.create 503 in diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli index 479a5760c..a2c0497f1 100644 --- a/helm/gTopLevel/cic2acic.mli +++ b/helm/gTopLevel/cic2acic.mli @@ -26,8 +26,6 @@ exception NotImplemented exception NotEnoughElements exception NameExpected -exception Found of (Cic.name * Cic.context_entry) list -exception NotImplemented val acic_of_cic_context' : int ref -> (* seed *) diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml new file mode 100644 index 000000000..50a81c56a --- /dev/null +++ b/helm/gTopLevel/doubleTypeInference.ml @@ -0,0 +1,316 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception Impossible of int;; +exception NotWellTyped of string;; +exception WrongUriToConstant of string;; +exception WrongUriToVariable of string;; +exception WrongUriToMutualInductiveDefinitions of string;; +exception ListTooShort;; +exception RelToHiddenHypothesis;; + +type types = {synthesized : Cic.term ; expected : Cic.term};; + +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> raise ListTooShort +;; + +let cooked_type_of_constant uri cookingsno = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked constant") + in + match cobj with + C.Definition (_,_,ty,_) -> ty + | C.Axiom (_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty) -> ty + | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) +;; + +let type_of_variable uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* 0 because a variable is never cooked => no partial cooking at one level *) + match CicEnvironment.is_type_checked uri 0 with + CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty + | CicEnvironment.UncheckedObj (C.Variable _) -> + raise (NotWellTyped "Reference to an unchecked variable") + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) +;; + +let cooked_type_of_mutual_inductive_defs uri cookingsno i = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked inductive type") + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) +;; + +let cooked_type_of_mutual_inductive_constr uri cookingsno i j = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + raise (NotWellTyped "Reference to an unchecked constructor") + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty,_) = List.nth cl (j-1) in + ty + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) +;; + +module CicHash = + Hashtbl.Make + (struct + type t = Cic.term + let equal = (==) + let hash = Hashtbl.hash + end) +;; + +(* type_of_aux' is just another name (with a different scope) for type_of_aux *) +let rec type_of_aux' subterms_to_types metasenv context t = + (* Coscoy's double type-inference algorithm *) + (* It computes the inner-types of every subterm of [t], *) + (* even when they are not needed to compute the types *) + (* of other terms. *) + let rec type_of_aux context t = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let module U = UriManager in + let synthesized = + match t with + C.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Decl t) -> S.lift n t + | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) + | None -> raise RelToHiddenHypothesis + with + _ -> raise (NotWellTyped "Not a close term") + ) + | C.Var uri -> type_of_variable uri + | C.Meta (n,l) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = + List.iter + (function None -> () | Some t -> ignore (type_of_aux context t)) l + in + let (_,canonical_context,ty) = + List.find (function (m,_,_) -> n = m) metasenv + in + (* Checks suppressed *) + CicSubstitution.lift_meta l ty + | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | C.Implicit -> raise (Impossible 21) + | C.Cast (te,ty) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context te in + let _ = type_of_aux context ty in + (* Checks suppressed *) + ty + | C.Prod (name,s,t) -> + let sort1 = type_of_aux context s + and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in + sort_of_prod context (name,s) (sort1,sort2) + | C.Lambda (n,s,t) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context s in + let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in + (* Checks suppressed *) + C.Prod (n,s,type2) + | C.LetIn (n,s,t) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = type_of_aux context s in + (* Checks suppressed *) + C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t) + | C.Appl (he::tl) when List.length tl > 0 -> + let hetype = type_of_aux context he + and tlbody_and_type = + List.map (fun x -> (x, type_of_aux context x)) tl + in + eat_prods context hetype tlbody_and_type + | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") + | C.Const (uri,cookingsno) -> + cooked_type_of_constant uri cookingsno + | C.Abst _ -> raise (Impossible 22) + | C.MutInd (uri,cookingsno,i) -> + cooked_type_of_mutual_inductive_defs uri cookingsno i + | C.MutConstruct (uri,cookingsno,i,j) -> + let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in + cty + | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> + (* Let's visit all the subterms that will not be visited later *) + let _ = List.map (type_of_aux context) pl in + let outsort = type_of_aux context outtype in + let (need_dummy, k) = + let rec guess_args context t = + match CicReduction.whd context t with + C.Sort _ -> (true, 0) + | C.Prod (name, s, t) -> + let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd context s with + (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) + C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> + (false, 1) + | C.Appl ((C.MutInd (uri',_,i')) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) + | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") + in + (*CSC whd non serve dopo type_of_aux ? *) + let (b, k) = guess_args context outsort in + if not b then (b, k - 1) else (b, k) + in + let (_, arguments) = + match R.whd context (type_of_aux context term) with + (*CSC manca il caso dei CAST *) + C.MutInd (uri',_,i') -> + (* Checks suppressed *) + [],[] + | C.Appl (C.MutInd (uri',_,i') :: tl) -> + split tl (List.length tl - k) + | _ -> + raise (NotWellTyped "MutCase: the term is not an inductive one") + in + (* Checks suppressed *) + if not need_dummy then + C.Appl ((outtype::arguments)@[term]) + else if arguments = [] then + outtype + else + C.Appl (outtype::arguments) + | C.Fix (i,fl) -> + (* Let's visit all the subterms that will not be visited later *) + let context' = + List.rev + (List.map + (fun (n,_,ty,_) -> + let _ = type_of_aux context ty in + (Some (C.Name n,(C.Decl ty))) + ) fl + ) @ + context + in + let _ = + List.iter + (fun (_,_,_,bo) -> ignore (type_of_aux context' bo)) + in + (* Checks suppressed *) + let (_,_,ty,_) = List.nth fl i in + ty + | C.CoFix (i,fl) -> + (* Let's visit all the subterms that will not be visited later *) + let context' = + List.rev + (List.map + (fun (n,ty,_) -> + let _ = type_of_aux context ty in + (Some (C.Name n,(C.Decl ty))) + ) fl + ) @ + context + in + let _ = + List.iter + (fun (_,_,bo) -> ignore (type_of_aux context' bo)) + in + (* Checks suppressed *) + let (_,ty,_) = List.nth fl i in + ty + in + (*CSC: Is whd the right thing to do? Or should full beta *) + (*CSC: reduction be more appropriate? *) +(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *) +(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *) + let synthesized' = CicReduction.whd context synthesized in + CicHash.add subterms_to_types t + {synthesized = synthesized' ; expected = Cic.Implicit} ; + synthesized' + + and sort_of_prod context (name,s) (t1, t2) = + let module C = Cic in + let t1' = CicReduction.whd context t1 in + let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in + match (t1', t2') with + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + C.Sort s2 + | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (_,_) -> + raise + (NotWellTyped + ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) + + and eat_prods context hetype = + (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) + (*CSC: cucinati *) + function + [] -> hetype + | (hete, hety)::tl -> + (match (CicReduction.whd context hetype) with + Cic.Prod (n,s,t) -> + (* Checks suppressed *) + eat_prods context (CicSubstitution.subst hete t) tl + | _ -> raise (NotWellTyped "Appl: wrong Prod-type") + ) + + in + type_of_aux context t +;; + +let double_type_of metasenv context t = + let subterms_to_types = CicHash.create 503 in + ignore (type_of_aux' subterms_to_types metasenv context t) ; + subterms_to_types +;; diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli new file mode 100644 index 000000000..4de5bc00c --- /dev/null +++ b/helm/gTopLevel/doubleTypeInference.mli @@ -0,0 +1,19 @@ +exception Impossible of int +exception NotWellTyped of string +exception WrongUriToConstant of string +exception WrongUriToVariable of string +exception WrongUriToMutualInductiveDefinitions of string +exception ListTooShort +exception RelToHiddenHypothesis + +type types = {synthesized : Cic.term ; expected : Cic.term};; + +module CicHash : + sig + type key = Cic.term + and 'a t + val find : 'a t -> key -> 'a + end + +val double_type_of : + Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t