X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=69287243918419218848f810371f5c0c1843fa83;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=362422cac59fa61509a66f76d5ce2fda950702c8;hpb=854ab91c9da5a87346c28a25d9a410f5dc85d15d;p=helm.git diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 362422cac..692872439 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -31,6 +31,22 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception ListTooShort;; exception RelToHiddenHypothesis;; +let syntactic_equality_add_time = ref 0.0;; +let type_of_aux'_add_time = ref 0.0;; +let number_new_type_of_aux'_double_work = ref 0;; +let number_new_type_of_aux' = ref 0;; +let number_new_type_of_aux'_prop = ref 0;; + +let double_work = ref 0;; + +let xxx_type_of_aux' m c t = + let t1 = Sys.time () in + let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in + let t2 = Sys.time () in + type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; + res +;; + type types = {synthesized : Cic.term ; expected : Cic.term option};; (* does_not_occur n te *) @@ -42,7 +58,7 @@ let rec does_not_occur n = | C.Rel _ | C.Meta _ | C.Sort _ - | C.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> does_not_occur n te && does_not_occur n ty | C.Prod (name,so,dest) -> @@ -89,64 +105,64 @@ let rec does_not_occur n = ) fl true ;; -(*CSC: potrebbe creare applicazioni di applicazioni *) -(*CSC: ora non e' piu' head, ma completa!!! *) -let rec head_beta_reduce = +let rec beta_reduce = let module S = CicSubstitution in let module C = Cic in function 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 + List.map (function (i,t) -> i, beta_reduce t) exp_named_subst in C.Var (uri,exp_named_subst) | C.Meta (n,l) -> C.Meta (n, List.map - (function None -> None | Some t -> Some (head_beta_reduce t)) l + (function None -> None | Some t -> Some (beta_reduce t)) l ) | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Cast (te,ty) -> - C.Cast (head_beta_reduce te, head_beta_reduce ty) + C.Cast (beta_reduce te, beta_reduce ty) | C.Prod (n,s,t) -> - C.Prod (n, head_beta_reduce s, head_beta_reduce t) + C.Prod (n, beta_reduce s, beta_reduce t) | C.Lambda (n,s,t) -> - C.Lambda (n, head_beta_reduce s, head_beta_reduce t) + C.Lambda (n, beta_reduce s, beta_reduce t) | C.LetIn (n,s,t) -> - C.LetIn (n, head_beta_reduce s, head_beta_reduce t) + C.LetIn (n, beta_reduce s, 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' + beta_reduce he' else - head_beta_reduce (C.Appl (he'::tl)) + (match he' with + C.Appl l -> beta_reduce (C.Appl (l@tl)) + | _ -> beta_reduce (C.Appl (he'::tl))) | C.Appl l -> - C.Appl (List.map head_beta_reduce l) + C.Appl (List.map beta_reduce l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, 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 + List.map (function (i,t) -> i, 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 + List.map (function (i,t) -> i, 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.MutCase (sp,i,beta_reduce outt,beta_reduce t, + List.map 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 + name,i,beta_reduce ty,beta_reduce bo ) fl in C.Fix (i,fl') @@ -154,14 +170,13 @@ let rec head_beta_reduce = let fl' = List.map (function (name,ty,bo) -> - name,head_beta_reduce ty,head_beta_reduce bo + name,beta_reduce ty,beta_reduce bo ) fl in C.CoFix (i,fl') ;; -(* syntactic_equality up to cookingsno for uris *) -(* (which is often syntactically irrilevant), *) +(* syntactic_equality up to the *) (* distinction between fake dependent products *) (* and non-dependent products, alfa-conversion *) (*CSC: must alfa-conversion be considered or not? *) @@ -230,6 +245,15 @@ let syntactic_equality t t' = _ -> false ;; +let xxx_syntactic_equality t t' = + let t1 = Sys.time () in + let res = syntactic_equality t t' in + let t2 = Sys.time () in + syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ; + res +;; + + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -242,14 +266,14 @@ let type_of_constant uri = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked constant") in match cobj with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty + C.Constant (_,_,ty,_,_) -> ty + | C.CurrentProof (_,_,_,ty,_,_) -> ty | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) ;; @@ -257,8 +281,8 @@ let type_of_variable uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty + match CicEnvironment.is_type_checked CicUniv.empty_ugraph 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)) @@ -269,13 +293,13 @@ let type_of_mutual_inductive_defs uri i = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked inductive type") in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -286,13 +310,13 @@ let type_of_mutual_inductive_constr uri i j = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with - CicEnvironment.CheckedObj cobj -> cobj + match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with + CicEnvironment.CheckedObj (cobj,_) -> cobj | CicEnvironment.UncheckedObj uobj -> raise (NotWellTyped "Reference to an unchecked constructor") in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty @@ -300,12 +324,17 @@ let type_of_mutual_inductive_constr uri i j = ;; module CicHash = - Hashtbl.Make - (struct - type t = Cic.term - let equal = (==) - let hash = Hashtbl.hash - end) + struct + module Tmp = + Hashtbl.Make + (struct + type t = Cic.term + let equal = (==) + let hash = Hashtbl.hash + end) + include Tmp + let empty () = Tmp.create 1 + end ;; (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -325,8 +354,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (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 + | Some (_,C.Def (_,Some ty)) -> S.lift n ty + | Some (_,C.Def (bo,None)) -> + type_of_aux context (S.lift n bo) expectedty + | None -> raise RelToHiddenHypothesis with _ -> raise (NotWellTyped "Not a close term") ) @@ -335,18 +366,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in + let (_,canonical_context,_) = CicUtil.lookup_meta n 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) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def (t,None)))::tl -> + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None))):: + (aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) + | (Some (_,C.Def (_,Some _)))::_ -> assert false in aux 1 canonical_context in @@ -355,10 +386,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (fun t ct -> match t,ct with _,None -> () - | Some t,Some (_,C.Def ct) -> + | Some t,Some (_,C.Def (ct,_)) -> let expected_type = R.whd context - (CicTypeChecker.type_of_aux' metasenv context ct) + (xxx_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 *) @@ -370,16 +401,16 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | _,_ -> 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 + let (_,canonical_context,ty) = CicUtil.lookup_meta n 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) + CicSubstitution.subst_meta l ty + | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *) + C.Sort (C.Type (CicUniv.fresh())) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *) + | 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 te (Some (beta_reduce ty)) in let _ = type_of_aux context ty None in (* Checks suppressed *) ty @@ -389,7 +420,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 _ = type_of_aux context s None in let expected_target_type = match expectedty with None -> None @@ -397,11 +428,11 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let ty = match R.whd context expectedty' with C.Prod (_,_,expected_target_type) -> - head_beta_reduce expected_target_type + beta_reduce expected_target_type | _ -> assert false in Some ty - in + in let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type in @@ -411,35 +442,47 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (*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 + let ty = type_of_aux context s None in let t_typ = (* Checks suppressed *) - type_of_aux ((Some (n,(C.Def s)))::context) t None - in + type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None + in (* CicSubstitution.subst s t_typ *) 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 + CicSubstitution.subst (C.Implicit None) 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. *) - (head_beta_reduce - (R.whd context (CicTypeChecker.type_of_aux' metasenv context he))) - in - let hetype = type_of_aux context he (Some expected_hetype) in + (* of no other solution. *) + (beta_reduce + (R.whd context (xxx_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))):: + (he, type_of_aux context he (Some (beta_reduce s))):: (aux (R.whd context (S.subst he t), tl)) | _ -> assert false in - aux (expected_hetype, tl) + aux (expected_hetype, tl) *) + let hetype = R.whd context (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 (beta_reduce s))):: + (aux (R.whd context (S.subst he t), tl)) + | _ -> assert false + in + aux (hetype, tl) in eat_prods context hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") @@ -479,11 +522,11 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in let (parameters, arguments,exp_named_subst) = let type_of_term = - CicTypeChecker.type_of_aux' metasenv context term + xxx_type_of_aux' metasenv context term in match R.whd context (type_of_aux context term - (Some (head_beta_reduce type_of_term))) + (Some (beta_reduce type_of_term))) with (*CSC manca il caso dei CAST *) C.MutInd (uri',i',exp_named_subst) -> @@ -499,8 +542,13 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Checks suppressed *) (* Let's visit all the subterms that will not be visited later *) let (cl,parsno) = - match CicEnvironment.get_cooked_obj uri with - C.InductiveDefinition (tl,_,parsno) -> + let obj,_ = + try + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + with Not_found -> assert false + in + match obj with + C.InductiveDefinition (tl,_,parsno,_) -> let (_,_,_,cl) = List.nth tl i in (cl,parsno) | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -516,10 +564,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in let expectedtype = type_of_branch context parsno need_dummy outtype cons - (CicTypeChecker.type_of_aux' metasenv context cons) + (xxx_type_of_aux' metasenv context cons) in ignore (type_of_aux context p - (Some (head_beta_reduce expectedtype))) ; + (Some (beta_reduce expectedtype))) ; j+1 ) 1 (List.combine pl cl) in @@ -545,7 +593,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = List.iter (fun (_,_,ty,bo) -> let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + beta_reduce (CicSubstitution.lift (List.length fl) ty) in ignore (type_of_aux context' bo (Some expectedty)) ) fl @@ -569,7 +617,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = List.iter (fun (_,ty,bo) -> let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + beta_reduce (CicSubstitution.lift (List.length fl) ty) in ignore (type_of_aux context' bo (Some expectedty)) ) fl @@ -578,13 +626,13 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (_,ty,_) = List.nth fl i in ty in - let synthesized' = head_beta_reduce synthesized in + let synthesized' = 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 -> + | Some ty when xxx_syntactic_equality synthesized' ty -> (* The expected type is synthactically equal to *) (* the synthesized type. Let's forget it. *) {synthesized = synthesized' ; expected = None}, synthesized @@ -592,22 +640,29 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = {synthesized = synthesized' ; expected = Some expectedty'}, expectedty' in + assert (not (CicHash.mem subterms_to_types t)); 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 + let obj,_ = + try + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + with Not_found -> assert false + in + let params = CicUtil.params_of_obj obj in + List.map + (function uri -> + let obj,_ = + try + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + with Not_found -> assert false + in + match obj 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 @@ -628,10 +683,19 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 _, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different from Coq manual!!! *) C.Sort s2 - | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + C.Sort (C.Type (CicUniv.fresh())) + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *) + C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *) + | (C.Meta _, C.Sort _) -> t2' + | (C.Meta _, (C.Meta (_,_) as t)) + | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> + t2' | (_,_) -> raise (NotWellTyped