X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=7b3e4179c47b77f65d2939d5fead0e2bea3914f9;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=14c69a4571900d956f041581595c55071def654d;hpb=9a56298c7e6cfd34830ab40393b880f5a678e98d;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 14c69a457..7b3e4179c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -107,8 +107,9 @@ and type_of_mutual_inductive_constr uri i j = and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in - let module R = CicMetaSubst in - match R.whd subst context expectedtype with + (* let module R = CicMetaSubst in *) + let module R = CicReduction in + match R.whd ~subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv | C.Appl (C.MutInd (_,_,_)::tl) -> @@ -117,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | C.Prod (name,so,de) -> (* we expect that the actual type of the branch has the due number of Prod *) - (match R.whd subst context actualtype with + (match R.whd ~subst context actualtype with C.Prod (name',so',de') -> let subst, metasenv = fo_unif_subst subst context metasenv so so' in @@ -132,11 +133,12 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t = - let rec type_of_aux subst metasenv context = + let rec type_of_aux subst metasenv context t = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - function + match t with +(* function *) C.Rel n -> (try match List.nth context (n - 1) with @@ -156,14 +158,29 @@ and type_of_aux' metasenv context t = in ty,subst',metasenv' | C.Meta (n,l) -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - let subst',metasenv' = - check_metasenv_consistency n subst metasenv context canonical_context l - in - CicSubstitution.lift_meta l ty, subst', metasenv' - | C.Sort s -> - C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) - subst,metasenv + (try + let (canonical_context, term) = CicUtil.lookup_subst n subst in + let subst,metasenv = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + type_of_aux subst metasenv context (CicSubstitution.lift_meta l term) + with CicUtil.Subst_not_found _ -> + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in + let subst,metasenv = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + CicSubstitution.lift_meta l ty, subst, metasenv) + (* TASSI: CONSTRAINT *) + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t'),subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let _,subst',metasenv' = @@ -186,7 +203,7 @@ and type_of_aux' metasenv context t = sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in - (match CicMetaSubst.whd subst' context sort1 with + (match CicReduction.whd ~subst:subst' context sort1 with C.Meta _ | C.Sort _ -> () | _ -> @@ -208,7 +225,7 @@ and type_of_aux' metasenv context t = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) CicSubstitution.subst s inferredty,subst',metasenv' - | C.Appl (he::tl) when List.length tl > 0 -> + | C.Appl (he::((_::_) as tl)) -> let hetype,subst',metasenv' = type_of_aux subst metasenv context he in let tlbody_and_type,subst'',metasenv'' = List.fold_right @@ -255,19 +272,19 @@ and type_of_aux' metasenv context t = (RefineFailure ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in let rec count_prod t = - match CicMetaSubst.whd subst context t with + match CicReduction.whd ~subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let no_args = count_prod arity in (* now, create a "generic" MutInd *) let metasenv,left_args = - CicMkImplicit.n_fresh_metas metasenv context no_left_params in + CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in let metasenv,right_args = let no_right_params = no_args - no_left_params in if no_right_params < 0 then assert false - else CicMkImplicit.n_fresh_metas metasenv context no_right_params in + else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in let metasenv,exp_named_subst = - CicMkImplicit.fresh_subst metasenv context expl_params in + CicMkImplicit.fresh_subst metasenv subst context expl_params in let expected_type = if no_args = 0 then C.MutInd (uri,i,exp_named_subst) @@ -280,7 +297,7 @@ and type_of_aux' metasenv context t = let _, subst, metasenv = type_of_aux subst metasenv context expected_type in - let actual_type = CicMetaSubst.whd subst context actual_type in + let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv = fo_unif_subst subst context metasenv expected_type actual_type in @@ -331,11 +348,21 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context appl in *) - CicMetaSubst.whd subst context appl + (* DEBUG + let prova1 = CicMetaSubst.whd subst context appl in + let prova2 = CicReduction.whd ~subst context appl in + if not (prova1 = prova2) then + begin + prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1)); + prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2)); + end; + *) + (* CicMetaSubst.whd subst context appl *) + CicReduction.whd ~subst context appl in fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in - CicMetaSubst.whd subst + CicReduction.whd ~subst context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix (i,fl) -> let subst,metasenv,types = @@ -354,7 +381,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift subst len ty) + ty_of_bo (CicSubstitution.lift len ty) ) (subst,metasenv) fl in let (_,_,ty,_) = List.nth fl i in ty,subst,metasenv @@ -375,7 +402,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context' bo in fo_unif_subst subst context' metasenv - ty_of_bo (CicMetaSubst.lift subst len ty) + ty_of_bo (CicSubstitution.lift len ty) ) (subst,metasenv) fl in let (_,ty,_) = List.nth fl i in @@ -404,7 +431,7 @@ and type_of_aux' metasenv context t = C.Def ((S.lift_meta l (S.lift i t)), Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl) in - aux 1 canonical_context + aux 1 canonical_context in try List.fold_left2 @@ -446,6 +473,7 @@ and type_of_aux' metasenv context t = | ((uri,t) as subst)::tl -> let typeofvar = CicSubstitution.subst_vars substs (type_of_variable uri) in +(* CSC: why was this code here? it is wrong (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise @@ -457,31 +485,40 @@ and type_of_aux' metasenv context t = (RefineFailure ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; +*) let typeoft,metasubst',metasenv' = type_of_aux metasubst metasenv context t in - try - let metasubst'',metasenv'' = + let metasubst'',metasenv'' = + try fo_unif_subst metasubst' context metasenv' typeoft typeofvar - in - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl - with _ -> - raise (RefineFailure "Wrong Explicit Named Substitution") + with _ -> + raise (RefineFailure + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) + in + check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl in check_exp_named_subst_aux metasubst metasenv [] and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in let context_for_t2 = (Some (name,C.Decl s))::context in - let t1'' = CicMetaSubst.whd subst context t1 in - let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in + let t1'' = CicReduction.whd ~subst context t1 in + let t2'' = CicReduction.whd ~subst context_for_t2 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 than Coq manual!!! *) C.Sort s2,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst,metasenv + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t'),subst,metasenv + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + C.Sort (C.Type t1),subst,metasenv | (C.Meta _, C.Sort _) -> t2'',subst,metasenv | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we @@ -490,7 +527,7 @@ and type_of_aux' metasenv context t = * likely to know the exact value of the result e.g. if the rhs is a * Sort (Prop | Set | CProp) then the result is the rhs *) let (metasenv,idx) = - CicMkImplicit.mk_implicit_sort metasenv in + CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv) = fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' in @@ -505,13 +542,13 @@ and type_of_aux' metasenv context t = let rec mk_prod metasenv context = function [] -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv,Cic.Meta (idx, irl) | (_,argty)::tl -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -522,21 +559,22 @@ and type_of_aux' metasenv context t = (* Thus I generate a name (name_hint) in context and *) (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in (context'@context). *) - let name_hint = - FreshNamesGenerator.mk_fresh_name - (CicMetaSubst.apply_subst_metasenv subst metasenv) + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name metasenv +(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous - (CicMetaSubst.apply_subst subst argty) + (CicMetaSubst.apply_subst subst argty) in (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name [] context name_hint (Cic.Sort Cic.Prop) in let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl + mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl in - metasenv,Cic.Prod (name,meta,target) + metasenv,Cic.Prod (name,meta,target) in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv) = @@ -549,10 +587,31 @@ and type_of_aux' metasenv context t = (match hetype with Cic.Prod (n,s,t) -> let subst,metasenv = - fo_unif_subst subst context metasenv hety s + fo_unif_subst subst context metasenv hety s +(* + try + fo_unif_subst subst context metasenv hety s + with _ -> + prerr_endline("senza subst fallisce"); + let hety = CicMetaSubst.apply_subst subst hety in + let s = CicMetaSubst.apply_subst subst s in + prerr_endline ("unifico = " ^(CicPp.ppterm hety)); + prerr_endline ("con = " ^(CicPp.ppterm s)); + fo_unif_subst subst context metasenv hety s *) in - eat_prods metasenv subst context - (CicMetaSubst.subst subst hete t) tl + (* DEBUG + let t1 = CicMetaSubst.subst subst hete t in + let t2 = CicSubstitution.subst hete t in + prerr_endline ("con subst = " ^(CicPp.ppterm t1)); + prerr_endline ("senza subst = " ^(CicPp.ppterm t2)); + prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^ + (CicMetaSubst.ppmetasenv metasenv subst)); + prerr_endline("++++++++++subst prima di eat_prods:\n" ^ + (CicMetaSubst.ppsubst subst)); + *) + eat_prods metasenv subst context + (* (CicMetaSubst.subst subst hete t) tl *) + (CicSubstitution.subst hete t) tl | _ -> assert false ) in @@ -608,15 +667,20 @@ and type_of_aux' metasenv context t = in aux [] [] (hetype,subst,metasenv) tlbody_and_type *) - in + in let ty,subst',metasenv' = type_of_aux [] metasenv context t in let substituted_t = CicMetaSubst.apply_subst subst' t in let substituted_ty = CicMetaSubst.apply_subst subst' ty in - let substituted_metasenv = - CicMetaSubst.apply_subst_metasenv subst' metasenv' - in +(* Andrea: ho rimesso qui l'applicazione della subst al +metasenv dopo che ho droppato l'invariante che il metsaenv +e' sempre istanziato *) + let substituted_metasenv = + CicMetaSubst.apply_subst_metasenv subst' metasenv' in + (* metasenv' *) +(* substituted_t,substituted_ty,substituted_metasenv *) +(* ANDREA: spostare tutta questa robaccia da un altra parte *) let cleaned_t = FreshNamesGenerator.clean_dummy_dependent_types substituted_t in let cleaned_ty = @@ -646,20 +710,20 @@ and type_of_aux' metasenv context t = (n,context',ty') ) substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv) - + (cleaned_t,cleaned_ty,cleaned_metasenv) ;; -(* DEBUGGING ONLY *) + + +(* DEBUGGING ONLY let type_of_aux' metasenv context term = try - let (t,ty,m) = type_of_aux' metasenv context term in - debug_print - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); -(* + let (t,ty,m) = + type_of_aux' metasenv context term in + debug_print + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); debug_print - ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s); -*) + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []); (t,ty,m) with | RefineFailure msg as e -> @@ -668,4 +732,4 @@ let type_of_aux' metasenv context term = | Uncertain msg as e -> debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e -;; +;; *)