X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=128da869b72a142b8cb914c80f68a02a221952ff;hb=7df065750ec593fb409ae8627f81927397602b9b;hp=8880ff3f4d1dadb43a035a18bbb9a804cad43a64;hpb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 8880ff3f4..128da869b 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -41,7 +41,7 @@ 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 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 @@ -58,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) -> @@ -123,7 +123,7 @@ let rec head_beta_reduce = (function None -> None | Some t -> Some (head_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.Prod (n,s,t) -> @@ -266,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)) ;; @@ -281,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)) @@ -293,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)) @@ -310,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 @@ -361,9 +361,7 @@ 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 @@ -398,13 +396,13 @@ 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) + | 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 @@ -447,7 +445,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 -> @@ -539,8 +537,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)) @@ -637,17 +640,23 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -668,10 +677,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 or s2 = C.CProp) -> (* 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