X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b535b9ebe987677505d7d9b40a2c59731a4c2606;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=87b3f7f42a319f227f06ce9d9c7b3db5bfc85e53;hpb=bbe46eaa76d94ea97c7aa1d60bdcbde9380a2e14;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 87b3f7f42..b535b9ebe 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -131,26 +131,42 @@ let exp_impl metasenv subst context = | _ -> assert false ;; +let unvariant newt = + match newt with + | Cic.Appl (hd::args) -> + let uri = CicUtil.uri_of_term hd in + (match + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + with + | Cic.Constant (_,Some t,_,[],attrs),_ + when List.exists ((=) (`Flavour `Variant)) attrs -> + Cic.Appl (t::args) + | _ -> newt) + | _ -> newt +;; + 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 = @@ -321,8 +337,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t - ugraph +and type_of_aux' ?(clean_dummy_dependent_types=true) + ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph = let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in @@ -384,7 +400,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci 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 @@ -396,6 +419,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 @@ -451,7 +505,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl s' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(2) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' @@ -577,7 +631,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(3) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type @@ -623,7 +677,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("The term " ^ + lazy ("(4) The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -811,7 +865,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(5) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' @@ -852,7 +906,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(7) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -905,7 +959,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(8) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1095,7 +1149,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 @@ -1151,12 +1205,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) -> - match c with - | c when not (CoercGraph.is_composite c) -> - debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); - None - | c -> + (fun (metasenv,last,c) _ -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last head ugraph in debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); @@ -1242,12 +1291,13 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci (* 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 - match CoercGraph.look_for_coercion' metasenv subst context src tgt with + (* instead of a dummy functional type we may create the real product + * using args_bo_and_ty, but since coercions lookup ignores the + * actual ariety we opt for the simple solution *) + let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in + match CoercGraph.look_for_coercion metasenv subst context hetype fty with | CoercGraph.NoCoercion -> [] - | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> + | CoercGraph.NotHandled -> raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> @@ -1264,7 +1314,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci ugraph in debug_print (lazy (" has type: "^ pp tty)); - Some (coerc,tty,subst,metasenv,ugraph) + + Some (unvariant coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1298,12 +1349,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: "^ @@ -1315,14 +1367,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 = @@ -1366,11 +1422,14 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci 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) ^ @@ -1395,11 +1454,21 @@ 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 ~metasenv context infty expty ugraph + in + if b then + Some ((t,infty), subst, metasenv, ugraph) + else + let newt = unvariant newt in + Some ((newt,newty), subst, metasenv, ugraph) with | Uncertain _ -> uncertain := true; None | RefineFailure _ -> None) @@ -1721,7 +1790,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci coerce_to_something_aux t infty expty subst metasenv context ugraph with Uncertain _ | RefineFailure _ as exn -> let f _ = - lazy ("The term " ^ + lazy ("(9) The term " ^ CicMetaSubst.ppterm_in_context metasenv subst t context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst infty context ^ " but is here used with type " ^ @@ -1759,7 +1828,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci (* eat prods ends here! *) let t',ty,subst',metasenv',ugraph1 = - type_of_aux [] metasenv context t ugraph + type_of_aux subst metasenv context t ugraph in let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in @@ -1803,7 +1872,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci else substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) + (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) +;; + +let type_of metasenv subst context t ug = + type_of_aux' metasenv subst context t ug +;; + +let type_of_aux' + ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug += + let t,ty,m,s,ug = + type_of_aux' ?clean_dummy_dependent_types ?localization_tbl + metasenv [] context t ug + in + t,ty,m,ug ;; let undebrujin uri typesno tys t = @@ -1904,7 +1987,7 @@ let typecheck metasenv uri obj ~localization_tbl = RefineFailure _ | Uncertain _ as exn -> let msg = - lazy ("The term " ^ + lazy ("(1) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ @@ -1924,10 +2007,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 *) @@ -1936,7 +2022,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 *)