X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=7b3e4179c47b77f65d2939d5fead0e2bea3914f9;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=c1b70df8d4e6ece7d71de3b8950914efb6d3c5f4;hpb=7ec7262cfa317c1962164350361f82a56c5d1826;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index c1b70df8d..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 @@ -158,13 +159,13 @@ and type_of_aux' metasenv context t = ty,subst',metasenv' | C.Meta (n,l) -> (try - let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in + 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 CicMetaSubst.SubstNotFound _ -> + 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 @@ -202,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 _ -> () | _ -> @@ -271,7 +272,7 @@ 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 @@ -296,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 @@ -347,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 = @@ -370,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 @@ -391,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 @@ -420,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 @@ -493,8 +504,8 @@ and type_of_aux' metasenv context t = 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!!! *) @@ -548,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 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) = @@ -575,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 @@ -634,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 = 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 = @@ -672,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 -> @@ -694,4 +732,4 @@ let type_of_aux' metasenv context term = | Uncertain msg as e -> debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e -;; +;; *)