X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=fc9dc840d1bb5323ff9526ce57d561664b5999ac;hb=4d765cc85e3a1e84c80c348a1e67ea1eed984916;hp=5aa96944d4e50295cac8094e69210f75e5cff99b;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 5aa96944d..fc9dc840d 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -132,25 +132,27 @@ let exp_impl metasenv subst context = ;; let is_a_double_coercion t = - let last_of l = - let rec aux acc = function - | x::[] -> acc,x - | x::tl -> aux (acc@[x]) tl - | [] -> assert false - in - aux [] l + let rec subst_nth n x l = + match n,l with + | _, [] -> [] + | 0, _::tl -> x :: tl + | n, hd::tl -> hd :: subst_nth (n-1) x tl in let imp = Cic.Implicit None in let dummyres = false,imp, imp,imp,imp in match t with - | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> - (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> - let sib2,head = last_of tl2 in - true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl - (c2::sib2@[imp])]) + | Cic.Appl l1 -> + (match CoercGraph.coerced_arg l1 with + | Some (Cic.Appl l2, pos1) -> + (match CoercGraph.coerced_arg l2 with + | Some (x, pos2) -> + true, List.hd l1, List.hd l2, x, + Cic.Appl (subst_nth (pos1 + 1) + (Cic.Appl (subst_nth (pos2+1) imp l2)) l1) + | _ -> dummyres) | _ -> dummyres) | _ -> dummyres +;; let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn = @@ -295,7 +297,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 +304,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,12 +318,12 @@ 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")) -and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t +and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = @@ -385,7 +386,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | C.Sort _ -> + | C.Sort (C.CProp tno) -> + let tno' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | C.Sort (C.Prop|C.Set) -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph | C.Implicit infos -> let metasenv',t' = exp_impl metasenv subst context infos in @@ -583,7 +591,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +641,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +810,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +827,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +867,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +1074,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 +1085,34 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 @@ -1216,12 +1251,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* given he:hety, gives beack all (c he) such that (c e):?->? *) let fix_arity n metasenv context subst he hetype ugraph = let hetype = CicMetaSubst.apply_subst subst hetype in - let src = CoercDb.coerc_carr_of_term hetype in - let tgt = CoercDb.Fun 0 in + let src = CoercDb.coerc_carr_of_term hetype 0 in + let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in match CoercGraph.look_for_coercion' metasenv subst context src tgt with | CoercGraph.NoCoercion -> [] - | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> + | CoercGraph.NotHandled -> raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> @@ -1340,11 +1374,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CoercGraph.look_for_coercion metasenv subst context infty expty in match coer with - | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy - "coerce_atom_to_something fails since not meta closed")) | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy + "coerce_atom_to_something fails since no coercions found")) + | CoercGraph.NotHandled when + not (CicUtil.is_meta_closed infty) || + not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy + "coerce_atom_to_something fails since carriers have metas")) + | CoercGraph.NotHandled -> raise (RefineFailure (lazy "coerce_atom_to_something fails since no coercions found")) | CoercGraph.SomeCoercion candidates -> debug_print (lazy (string_of_int (List.length candidates) ^ @@ -1597,11 +1634,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicTypeChecker.type_of_aux' ~subst metasenv context m CicUniv.oblivion_ugraph with - | Cic.MutInd _ as mty,_ -> [], mty - | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty + | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ -> snd (HExtlib.split_nth leftno args), mty | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> assert false + with CicTypeChecker.TypeCheckerFailure _ -> + raise (AssertFailure(lazy "already ill-typed matched term")) in let new_outty = keep_lambdas_and_put_expty context outty expty right_p m (rno+1) @@ -1745,10 +1783,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* 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 + if clean_dummy_dependent_types then + FreshNamesGenerator.clean_dummy_dependent_types substituted_t + else substituted_t in let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in + if clean_dummy_dependent_types then + FreshNamesGenerator.clean_dummy_dependent_types substituted_ty + else substituted_ty in let cleaned_metasenv = + if clean_dummy_dependent_types then List.map (function (n,context,ty) -> let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in @@ -1768,6 +1811,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in (n,context',ty') ) substituted_metasenv + else + substituted_metasenv in (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; @@ -1926,7 +1971,12 @@ let typecheck metasenv uri obj ~localization_tbl = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> let ty',_,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty ugraph + (* clean_dummy_dependent_types: false to avoid cleaning the names + of the left products, that must be identical to those of the + constructors; however, non-left products should probably be + cleaned *) + type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl + metasenv [] ty ugraph in metasenv,ugraph,(name,b,ty',cl)::res ) tys (metasenv,ugraph,[]) in