X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=a2c7707493bb82baafc0561e7f6418a02ea41483;hb=4dfb1305a9c4a7c292f4b1957de1454d46c1ab8a;hp=bde5d63e413978703bf8ef0d58a9908f478d1d34;hpb=70211a10f741fe77945f5a720596df2b686f344d;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index bde5d63e4..a2c770749 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -405,6 +405,37 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in + let rec count_prods context ty = + match CicReduction.whd context ~subst:subst'' ty with + | Cic.Prod (n,s,t) -> + 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + in + let exp_prods = count_prods context ty' in + let inf_prods = count_prods context inferredty in + let te', inferredty, metasenv'', subst'', ugraph2 = + let rec aux t m s ug it = function + | 0 -> t,it,m,s,ug + | n -> + match CicReduction.whd context ~subst:s it with + | Cic.Prod (_,src,tgt) -> + let newmeta, metaty, s, m, ug = + type_of_aux s m context (Cic.Implicit None) ug + in + let s,m,ug = + fo_unif_subst s context m metaty src ug + in + let t = + match t with + | Cic.Appl l -> Cic.Appl (l @ [newmeta]) + | _ -> Cic.Appl [t;newmeta] + in + aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1) + | _ -> t,it,m,s,ug + in + aux te' metasenv'' subst'' ugraph2 inferredty + (max 0 (inf_prods - exp_prods)) + in let (te', ty'), subst''',metasenv''',ugraph3 = coerce_to_something true localization_tbl te' inferredty ty' subst'' metasenv'' context ugraph2 @@ -1104,7 +1135,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci | (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 ugraph1 = CicUniv.add_ge t' t1 ugraph in let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in C.Sort (C.Type t'),subst,metasenv,ugraph2 with @@ -1160,7 +1191,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (function (metasenv,last,c) -> + (fun (metasenv,last,c) _ -> match c with | c when not (CoercGraph.is_composite c) -> debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); @@ -1308,12 +1339,13 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^ "\n but is applyed to: " ^ String.concat ";" (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*) + let error = ref None in let possible_fixes = fix_arity (List.length args) metasenv context subst he hetype ugraph in match HExtlib.list_findopt - (fun (he,hetype,subst,metasenv,ugraph) -> + (fun (he,hetype,subst,metasenv,ugraph) _ -> (* {{{ *)debug_print (lazy ("Try fix: "^ CicMetaSubst.ppterm_in_context ~metasenv subst he context)); debug_print (lazy (" of type: "^ @@ -1325,14 +1357,18 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci with | RefineFailure _ | Uncertain _ | HExtlib.Localized (_,RefineFailure _) - | HExtlib.Localized (_,Uncertain _) -> None) + | HExtlib.Localized (_,Uncertain _) as exn -> + error := Some exn; None) possible_fixes with | Some x -> x | None -> - raise - (MoreArgsThanExpected - (List.length args, RefineFailure (lazy ""))) + match !error with + None -> + raise + (MoreArgsThanExpected + (List.length args, RefineFailure (lazy ""))) + | Some exn -> raise exn in (* first we check if we are in the simple case of a meta closed term *) let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = @@ -1408,11 +1444,19 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt expty + avoid_double_coercion context subst metasenv ugraph newt + expty in let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv newhety expty ugraph in - Some ((newt,newty), subst, metasenv, ugraph) + fo_unif_subst subst context metasenv newhety expty ugraph + in + let b, ugraph = + CicReduction.are_convertible ~subst context infty expty ugraph + in + if b then + Some ((t,infty), subst, metasenv, ugraph) + else + Some ((newt,newty), subst, metasenv, ugraph) with | Uncertain _ -> uncertain := true; None | RefineFailure _ -> None) @@ -1937,10 +1981,13 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph | Cic.Constant (name,None,ty,args,attrs) -> - let ty',_,metasenv,ugraph = + let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + (match CicReduction.whd [] sort with + Cic.Sort _ + | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + | _ -> raise (RefineFailure (lazy ""))) | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> assert (metasenv' = metasenv); (* Here we do not check the metasenv for correctness *) @@ -1949,7 +1996,7 @@ let typecheck metasenv uri obj ~localization_tbl = let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in begin - match sort with + match CicReduction.whd ~delta:true [] sort with Cic.Sort _ (* instead of raising Uncertain, let's hope that the meta will become a sort *)