X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;fp=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=0000000000000000000000000000000000000000;hp=b06619c4ddf74d98929420761a7d3a61e34119c5;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml deleted file mode 100644 index b06619c4d..000000000 --- a/helm/gTopLevel/doubleTypeInference.ml +++ /dev/null @@ -1,567 +0,0 @@ -(* 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 option};; - -(*CSC: potrebbe creare applicazioni di applicazioni *) -(*CSC: ora non e' piu' head, ma completa!!! *) -let rec head_beta_reduce = - let module S = CicSubstitution in - let module C = Cic in - function - C.Rel _ - | C.Var _ as t -> t - | C.Meta (n,l) -> - C.Meta (n, - List.map - (function None -> None | Some t -> Some (head_beta_reduce t)) l - ) - | C.Sort _ as t -> t - | C.Implicit -> assert false - | C.Cast (te,ty) -> - C.Cast (head_beta_reduce te, head_beta_reduce ty) - | C.Prod (n,s,t) -> - C.Prod (n, head_beta_reduce s, head_beta_reduce t) - | C.Lambda (n,s,t) -> - C.Lambda (n, head_beta_reduce s, head_beta_reduce t) - | C.LetIn (n,s,t) -> - C.LetIn (n, head_beta_reduce s, head_beta_reduce t) - | C.Appl ((C.Lambda (name,s,t))::he::tl) -> - let he' = S.subst he t in - if tl = [] then - head_beta_reduce he' - else - head_beta_reduce (C.Appl (he'::tl)) - | C.Appl l -> - C.Appl (List.map head_beta_reduce l) - | C.Const _ as t -> t - | C.MutInd _ - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cno,i,outt,t,pl) -> - C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t, - List.map head_beta_reduce pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (function (name,i,ty,bo) -> - name,i,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.Fix (i,fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (function (name,ty,bo) -> - name,head_beta_reduce ty,head_beta_reduce bo - ) fl - in - C.CoFix (i,fl') -;; - -(* syntactic_equality up to cookingsno for uris *) -(* (which is often syntactically irrilevant), *) -(* distinction between fake dependent products *) -(* and non-dependent products, alfa-conversion *) -(*CSC: must alfa-conversion be considered or not? *) -let syntactic_equality t t' = - let module C = Cic in - let rec syntactic_equality t t' = - if t = t' then true - else - match t, t' with - C.Rel _, C.Rel _ - | C.Var _, C.Var _ - | C.Meta _, C.Meta _ - | C.Sort _, C.Sort _ - | C.Implicit, C.Implicit -> false (* we already know that t != t' *) - | C.Cast (te,ty), C.Cast (te',ty') -> - syntactic_equality te te' && - syntactic_equality ty ty' - | C.Prod (_,s,t), C.Prod (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Lambda (_,s,t), C.Lambda (_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.LetIn (_,s,t), C.LetIn(_,s',t') -> - syntactic_equality s s' && - syntactic_equality t t' - | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' - | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' - | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> - UriManager.eq uri uri' && i = i' - | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') -> - UriManager.eq uri uri' && i = i' && j = j' - | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') -> - UriManager.eq sp sp' && i = i' && - syntactic_equality outt outt' && - syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' - | C.Fix (i,fl), C.Fix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,i,ty,bo) (_,i',ty',bo') -> - b && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | C.CoFix (i,fl), C.CoFix (i',fl') -> - i = i' && - List.fold_left2 - (fun b (_,ty,bo) (_,ty',bo') -> - b && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' - | _,_ -> false - in - try - syntactic_equality t t' - with - _ -> false -;; - -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 expectedty = - (* 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 expectedty = - 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) expectedty - | 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 (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let lifted_canonical_context = - let rec aux i = - function - [] -> [] - | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def t))::tl -> - (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | None::tl -> None::(aux (i+1) tl) - in - aux 1 canonical_context - in - let _ = - List.iter2 - (fun t ct -> - match t,ct with - _,None -> () - | Some t,Some (_,C.Def ct) -> - let expected_type = - R.whd context - (CicTypeChecker.type_of_aux' metasenv context ct) - in - (* Maybe I am a bit too paranoid, because *) - (* if the term is well-typed than t and ct *) - (* are convertible. Nevertheless, I compute *) - (* the expected type. *) - ignore (type_of_aux context t (Some expected_type)) - | Some t,Some (_,C.Decl ct) -> - ignore (type_of_aux context t (Some ct)) - | _,_ -> assert false (* the term is not well typed!!! *) - ) l lifted_canonical_context - 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 (Some (head_beta_reduce ty)) in - let _ = type_of_aux context ty None in - (* Checks suppressed *) - ty - | C.Prod (name,s,t) -> - let sort1 = type_of_aux context s None - and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None 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 None in - let expected_target_type = - match expectedty with - None -> None - | Some expectedty' -> - let ty = - match R.whd context expectedty' with - C.Prod (_,_,expected_target_type) -> - head_beta_reduce expected_target_type - | _ -> assert false - in - Some ty - in - let type2 = - type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type - in - (* Checks suppressed *) - C.Prod (n,s,type2) - | C.LetIn (n,s,t) -> -(*CSC: What are the right expected types for the source and *) -(*CSC: target of a LetIn? None used. *) - (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s None in - (* Checks suppressed *) - C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None) - | C.Appl (he::tl) when List.length tl > 0 -> - let expected_hetype = - (* Inefficient, the head is computed twice. But I know *) - (* of no other solution. *) - R.whd context (CicTypeChecker.type_of_aux' metasenv context he) - in - let hetype = type_of_aux context he (Some expected_hetype) in - let tlbody_and_type = - let rec aux = - function - _,[] -> [] - | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: - (aux (R.whd context (S.subst he t), tl)) - | _ -> assert false - in - aux (expected_hetype, 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.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 outsort = type_of_aux context outtype None 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 - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) - in - let (parameters, arguments) = - let type_of_term = - CicTypeChecker.type_of_aux' metasenv context term - in - match - R.whd context (type_of_aux context term - (Some (head_beta_reduce type_of_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 *) - (* Let's visit all the subterms that will not be visited later *) - let (cl,parsno) = - match CicEnvironment.get_cooked_obj uri cookingsno with - C.InductiveDefinition (tl,_,parsno) -> - let (_,_,_,cl) = List.nth tl i in (cl,parsno) - | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) - in - let _ = - List.fold_left - (fun j (p,(_,c,_)) -> - let cons = - if parameters = [] then - (C.MutConstruct (uri,cookingsno,i,j)) - else - (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) - in - let expectedtype = - type_of_branch context parsno need_dummy outtype cons - (CicTypeChecker.type_of_aux' metasenv context cons) - in - ignore (type_of_aux context p - (Some (head_beta_reduce expectedtype))) ; - j+1 - ) 1 (List.combine pl cl) - in - 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 None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - 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 None in - (Some (C.Name n,(C.Decl ty))) - ) fl - ) @ - context - in - let _ = - List.iter - (fun (_,ty,bo) -> - let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) - in - ignore (type_of_aux context' bo (Some expectedty)) - ) fl - in - (* Checks suppressed *) - let (_,ty,_) = List.nth fl i in - ty - in - let synthesized' = head_beta_reduce synthesized in - let types,res = - match expectedty with - None -> - (* No expected type *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some ty when syntactic_equality synthesized' ty -> - (* The expected type is synthactically equal to *) - (* the synthesized type. Let's forget it. *) - {synthesized = synthesized' ; expected = None}, synthesized - | Some expectedty' -> - {synthesized = synthesized' ; expected = Some expectedty'}, - expectedty' - in - CicHash.add subterms_to_types t types ; - res - - 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") - ) - -and type_of_branch context argsno need_dummy outtype term constype = - let module C = Cic in - let module R = CicReduction in - match R.whd context constype with - C.MutInd (_,_,_) -> - if need_dummy then - outtype - else - C.Appl [outtype ; term] - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl argsno - in - if need_dummy && arguments = [] then - outtype - else - C.Appl (outtype::arguments@(if need_dummy then [] else [term])) - | C.Prod (name,so,de) -> - let term' = - match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1] - in - C.Prod (C.Anonimous,so,type_of_branch - ((Some (name,(C.Decl so)))::context) argsno need_dummy - (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (Impossible 20) - - in - type_of_aux context t expectedty -;; - -let double_type_of metasenv context t expectedty = - let subterms_to_types = CicHash.create 503 in - ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ; - subterms_to_types -;;