X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b5204de02f78baa2a6731d25c5e61bfe7aa11cef;hb=b58b7f9f3fdf8d66522b31828faa5bfa588c31b8;hp=45c2d26eacf619df9aeee3c94ac3f88f6b880981;hpb=267fbbcd1b8c54ce7faafd48cface965d0f6c37b;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 45c2d26ea..b5204de02 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -295,7 +295,6 @@ and type_of_mutual_inductive_constr uri i j ugraph = and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph = let module C = Cic in - (* let module R = CicMetaSubst in *) let module R = CicReduction in match R.whd ~subst context expectedtype with C.MutInd (_,_,_) -> @@ -303,7 +302,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | C.Appl (C.MutInd (_,_,_)::tl) -> let (_,arguments) = split tl left_args_no in (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph - | C.Prod (name,so,de) -> + | C.Prod (_,so,de) -> (* we expect that the actual type of the branch has the due number of Prod *) (match R.whd ~subst context actualtype with @@ -317,7 +316,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* we should also check that the name variable is anonymous in the actual type de' ?? *) check_branch (n+1) - ((Some (name,(C.Decl so)))::context) + ((Some (name',(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1 | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) @@ -583,7 +582,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' + context)) in let rec instantiate_prod t = function @@ -632,7 +632,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci context)) exn in (p'::pl,j-1, - outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) + outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) pl ([],List.length pl,[],subst,metasenv,ugraph3) in @@ -801,7 +801,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci in C.Appl (outtype'::args) in - CicReduction.whd ~subst context appl + CicReduction.head_beta_reduce ~delta:false + ~upto:(List.length args) appl in try fo_unif_subst subst context metasenv instance instance' @@ -817,12 +818,12 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance context))) - (subst,metasenv,ugraph5) pl' outtypeinstances + (subst,metasenv,ugraph5) pl' outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), CicReduction.head_beta_reduce (CicMetaSubst.apply_subst subst - (C.Appl(outtype::right_args@[term]))), + (C.Appl(outtype::right_args@[term']))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> let fl_ty',subst,metasenv,types,ugraph1,len = @@ -857,7 +858,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty - context)) + context')) in fl @ [bo'] , subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') @@ -1064,8 +1065,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci 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) -> + | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> (* different than Coq manual!!! *) C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> @@ -1076,8 +1076,34 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci C.Sort (C.Type t'),subst,metasenv,ugraph2 with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),subst,metasenv,ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),subst,metasenv,ugraph + | (C.Sort _,C.Sort (C.CProp t1)) -> + C.Sort (C.CProp t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we