X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=71422ced12d6190d09b2829d2f80d1fcffaef6c5;hb=70f855932359e26ca89deb11c22f9c9d26154827;hp=024f49ebf6732ca6bf4ad6e82d5011007c1012b7;hpb=528294d5228f65f4b3fbd3ebe00a5cd9a8f3b929;p=helm.git diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml index 024f49ebf..71422ced1 100644 --- a/helm/gTopLevel/doubleTypeInference.ml +++ b/helm/gTopLevel/doubleTypeInference.ml @@ -33,14 +33,74 @@ exception RelToHiddenHypothesis;; type types = {synthesized : Cic.term ; expected : Cic.term option};; +(* does_not_occur n te *) +(* returns [true] if [Rel n] does not occur in [te] *) +let rec does_not_occur n = + let module C = Cic in + function + C.Rel m when m = n -> false + | C.Rel _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> true + | C.Cast (te,ty) -> + does_not_occur n te && does_not_occur n ty + | C.Prod (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.Lambda (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.LetIn (name,so,dest) -> + does_not_occur n so && + does_not_occur (n + 1) dest + | C.Appl l -> + List.fold_right (fun x i -> i && does_not_occur n x) l true + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_right (fun (_,x) i -> i && does_not_occur n x) + exp_named_subst true + | C.MutCase (_,_,out,te,pl) -> + does_not_occur n out && does_not_occur n te && + List.fold_right (fun x i -> i && does_not_occur n x) pl true + | C.Fix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let tys = + List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in + List.fold_right + (fun (_,_,ty,bo) i -> + i && does_not_occur n ty && + does_not_occur n_plus_len bo + ) fl true + | C.CoFix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let tys = + List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + in + List.fold_right + (fun (_,ty,bo) i -> + i && does_not_occur n ty && + does_not_occur n_plus_len bo + ) fl true +;; + (*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.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.Var (uri,exp_named_subst) | C.Meta (n,l) -> C.Meta (n, List.map @@ -64,11 +124,23 @@ let rec head_beta_reduce = 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, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst' = + List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t, List.map head_beta_reduce pl) | C.Fix (i,fl) -> let fl' = @@ -99,11 +171,9 @@ let 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.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') -> + UriManager.eq uri uri' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' | C.Cast (te,ty), C.Cast (te',ty') -> syntactic_equality te te' && syntactic_equality ty ty' @@ -118,12 +188,17 @@ let syntactic_equality t t' = 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') -> + | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') -> + UriManager.eq uri uri' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') -> + UriManager.eq uri uri' && i = i' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | C.MutConstruct (uri,i,j,exp_named_subst), + C.MutConstruct (uri',i',j',exp_named_subst') -> + UriManager.eq uri uri' && i = i' && j = j' && + syntactic_equality_exp_named_subst exp_named_subst exp_named_subst' + | 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' && @@ -143,7 +218,11 @@ let syntactic_equality t t' = b && syntactic_equality ty ty' && syntactic_equality bo bo') true fl fl' - | _,_ -> false + | _, _ -> false (* we already know that t != t' *) + and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 = + List.fold_left2 + (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true + exp_named_subst1 exp_named_subst2 in try syntactic_equality t t' @@ -158,20 +237,19 @@ let rec split l n = | (_,_) -> raise ListTooShort ;; -let cooked_type_of_constant uri cookingsno = +let type_of_constant uri = 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 + match CicEnvironment.is_type_checked uri 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 + C.Constant (_,_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty,_) -> ty | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) ;; @@ -179,20 +257,19 @@ 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 + match CicEnvironment.is_type_checked uri 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 type_of_mutual_inductive_defs uri 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 + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked inductive type") @@ -204,12 +281,12 @@ let cooked_type_of_mutual_inductive_defs uri cookingsno i = | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ;; -let cooked_type_of_mutual_inductive_constr uri cookingsno i j = +let type_of_mutual_inductive_constr uri 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 + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked constructor") @@ -217,7 +294,7 @@ let cooked_type_of_mutual_inductive_constr uri cookingsno i j = match cobj with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cl) = List.nth dl i in - let (_,ty,_) = List.nth cl (j-1) in + let (_,ty) = List.nth cl (j-1) in ty | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ;; @@ -253,21 +330,51 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = with _ -> raise (NotWellTyped "Not a close term") ) - | C.Var uri -> type_of_variable uri + | C.Var (uri,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst (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 None) - ) l + let (_,canonical_context,_) = + List.find (function (m,_,_) -> n = m) metasenv in - let (_,canonical_context,ty) = - List.find (function (m,_,_) -> n = m) metasenv + 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 - (* Checks suppressed *) - CicSubstitution.lift_meta l ty + 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) -> @@ -305,31 +412,48 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (*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 hetype = type_of_aux context he None 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 + let t_typ = + (* Checks suppressed *) + type_of_aux ((Some (n,(C.Def s)))::context) t None in - aux (R.whd context hetype, tl) + if does_not_occur 1 t_typ then + (* since [Rel 1] does not occur in typ, substituting any term *) + (* in place of [Rel 1] is equivalent to delifting once *) + CicSubstitution.subst C.Implicit t_typ + else + C.LetIn (n,s,t_typ) + | 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 - eat_prods context hetype tlbody_and_type + 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) -> + | C.Const (uri,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + | C.MutInd (uri,i,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_defs uri i) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + visit_exp_named_subst context uri exp_named_subst ; + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_constr uri i j) + | C.MutCase (uri,i,outtype,term,pl) -> let outsort = type_of_aux context outtype None in let (need_dummy, k) = let rec guess_args context t = @@ -340,10 +464,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 -> + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> (false, 1) - | C.Appl ((C.MutInd (uri',_,i')) :: _) + | C.Appl ((C.MutInd (uri',i',_)) :: _) when U.eq uri' uri && i' = i -> (false, 1) | _ -> (true, 1) else @@ -353,7 +476,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (b, k) = guess_args context outsort in if not b then (b, k - 1) else (b, k) in - let (parameters, arguments) = + let (parameters, arguments,exp_named_subst) = let type_of_term = CicTypeChecker.type_of_aux' metasenv context term in @@ -362,18 +485,20 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (Some (head_beta_reduce type_of_term))) with (*CSC manca il caso dei CAST *) - C.MutInd (uri',_,i') -> + C.MutInd (uri',i',exp_named_subst) -> (* Checks suppressed *) - [],[] - | C.Appl (C.MutInd (uri',_,i') :: tl) -> + [],[],exp_named_subst + | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) -> + let params,args = split tl (List.length tl - k) + in params,args,exp_named_subst | _ -> 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 + match CicEnvironment.get_cooked_obj uri with C.InductiveDefinition (tl,_,parsno) -> let (_,_,_,cl) = List.nth tl i in (cl,parsno) | _ -> @@ -381,12 +506,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in let _ = List.fold_left - (fun j (p,(_,c,_)) -> + (fun j (p,(_,c)) -> let cons = if parameters = [] then - (C.MutConstruct (uri,cookingsno,i,j)) + (C.MutConstruct (uri,i,j,exp_named_subst)) else - (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) + (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in let expectedtype = type_of_branch context parsno need_dummy outtype cons @@ -469,6 +594,34 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = CicHash.add subterms_to_types t types ; res + and visit_exp_named_subst context uri exp_named_subst = + let uris_and_types = + match CicEnvironment.get_cooked_obj uri with + Cic.Constant (_,_,_,params) + | Cic.CurrentProof (_,_,_,_,params) + | Cic.Variable (_,_,_,params) + | Cic.InductiveDefinition (_,params,_) -> + List.map + (function uri -> + match CicEnvironment.get_cooked_obj uri with + Cic.Variable (_,None,ty,_) -> uri,ty + | _ -> assert false (* the theorem is well-typed *) + ) params + in + let rec check uris_and_types subst = + match uris_and_types,subst with + _,[] -> [] + | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' -> + ignore (type_of_aux context t (Some ty)) ; + let tytl' = + List.map + (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl + in + check tytl' substtl + | _,_ -> assert false (* the theorem is well-typed *) + in + check uris_and_types exp_named_subst + and sort_of_prod context (name,s) (t1, t2) = let module C = Cic in let t1' = CicReduction.whd context t1 in @@ -518,7 +671,7 @@ and type_of_branch context argsno need_dummy outtype term constype = 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 + C.Prod (C.Anonymous,so,type_of_branch ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) | _ -> raise (Impossible 20)