X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b5204de02f78baa2a6731d25c5e61bfe7aa11cef;hb=6719c0e318b312b51b089fea3d69d1b7103245ea;hp=49c85a72eea1b0fc09efb2d805f988040f12d4e4;hpb=4a2768c670a6904975fe6098c5bf7ea80ddb49e8;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 49c85a72e..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,12 +316,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 = @@ -337,15 +336,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match List.nth context (n - 1) with Some (_,C.Decl ty) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (_,Some ty)) -> + | Some (_,C.Def (_,ty)) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (bo,None)) -> - let ty,ugraph = - (* if it is in the context it must be already well-typed*) - CicTypeChecker.type_of_aux' ~subst metasenv context - (S.lift n bo) ugraph - in - t,ty,subst,metasenv,ugraph | None -> enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) @@ -445,12 +437,29 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 - | C.LetIn (n,s,t) -> - (* only to check if s is well-typed *) - let s',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in + | C.LetIn (n,s,ty,t) -> + (* only to check if s is well-typed *) + let s',ty',subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph in + let ty,_,subst',metasenv',ugraph1 = + type_of_aux subst' metasenv' context ty ugraph1 in + let subst',metasenv',ugraph1 = + try + fo_unif_subst subst' context metasenv' + ty ty' ugraph1 + with + exn -> + enrich localization_tbl s' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty + context)) + in + let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in let t',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' @@ -460,7 +469,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t * Even faster than the previous solution. * Moreover the inferred type is closer to the expected one. *) - C.LetIn (n,s',t'), + C.LetIn (n,s',ty,t'), CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> @@ -568,12 +577,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("(10)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' 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 @@ -613,7 +623,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("(11)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -622,7 +632,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 @@ -639,7 +649,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (let candidate,ugraph5,metasenv,subst = let exp_name_subst, metasenv = let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in List.fold_right ( @@ -791,7 +801,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' @@ -800,19 +811,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("(12)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' 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 = @@ -841,13 +852,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(13)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ 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') @@ -894,7 +905,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(14)The term " ^ + lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -939,13 +950,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n, - C.Def ((S.subst_meta l (S.lift i t)), - Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some + (n, + C.Def + (S.subst_meta l (S.lift i t), + S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl) in aux 1 canonical_context in @@ -956,12 +967,27 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t _,None -> l @ [None],subst,metasenv,ugraph | Some t,Some (_,C.Def (ct,_)) -> + (*CSC: the following optimization is to avoid a possibly + expensive reduction that can be easily avoided and + that is quite frequent. However, this is better + handled using levels to control reduction *) + let optimized_t = + match t with + Cic.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with + Failure _ -> t) + | _ -> t + in let subst',metasenv',ugraph' = (try (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*) - fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + fo_unif_subst subst context metasenv optimized_t ct ugraph + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -1039,8 +1065,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)) -> @@ -1051,8 +1076,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 @@ -1204,14 +1255,16 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (fun (metasenv,last,coerc) -> let pp t = CicMetaSubst.ppterm_in_context ~metasenv subst t context in - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last he ugraph in - debug_print (lazy ("New head: "^ pp coerc)); try + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last he ugraph in + debug_print (lazy ("New head: "^ pp coerc)); let tty,ugraph = - CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in - debug_print (lazy (" has type: "^ pp tty)); - Some (coerc,tty,subst,metasenv,ugraph) + CicTypeChecker.type_of_aux' ~subst metasenv context coerc + ugraph + in + debug_print (lazy (" has type: "^ pp tty)); + Some (coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1373,10 +1426,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fo_unif_subst subst context metasenv infty expty ugraph in (t, expty), subst, metasenv, ugraph - with Uncertain _ | RefineFailure _ as exn -> - if not allow_coercions || not !insert_coercions then - enrich localization_tbl t exn - else + with (Uncertain _ | RefineFailure _ as exn) + when allow_coercions && !insert_coercions -> let whd = CicReduction.whd ~delta:false in let clean t s c = whd c (CicMetaSubst.apply_subst s t) in let infty = clean infty subst context in @@ -1720,10 +1771,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 @@ -1736,17 +1792,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) | Some (n, Cic.Def (bo,ty)) -> let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in - let ty' = - match ty with - None -> None - | Some ty -> - Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in Some (n, Cic.Def (bo',ty')) ) context in (n,context',ty') ) substituted_metasenv + else + substituted_metasenv in (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; @@ -1826,14 +1880,44 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno = metasenv,ugraph,substituted_tys let typecheck metasenv uri obj ~localization_tbl = - let ugraph = CicUniv.empty_ugraph in + let ugraph = CicUniv.oblivion_ugraph in match obj with Cic.Constant (name,Some bo,ty,args,attrs) -> + (* CSC: ugly code. Here I need to retrieve in advance the loc of bo + since type_of_aux' destroys localization information (which are + preserved by type_of_aux *) + let loc exn' = + try + Cic.CicHash.find localization_tbl bo + with Not_found -> + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo); + raise exn' in let bo',boty,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] bo ugraph in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let subst,metasenv,ugraph = + try + fo_unif_subst [] [] metasenv boty ty' ugraph + with + RefineFailure _ + | Uncertain _ as exn -> + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ + " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ + " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) + in + let exn' = + match exn with + RefineFailure _ -> RefineFailure msg + | Uncertain _ -> Uncertain msg + | _ -> assert false + in + raise (HExtlib.Localized (loc exn',exn')) + in let bo' = CicMetaSubst.apply_subst subst bo' in let ty' = CicMetaSubst.apply_subst subst ty' in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in @@ -1875,7 +1959,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 @@ -1891,7 +1980,7 @@ let typecheck metasenv uri obj ~localization_tbl = (fun (name,ty) (metasenv,ugraph,res) -> let ty = CicTypeChecker.debrujin_constructor - ~cb:(relocalize localization_tbl) uri typesno ty in + ~cb:(relocalize localization_tbl) uri typesno [] ty in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in @@ -1927,13 +2016,11 @@ let pack_coercion metasenv ctx t = | C.Lambda (name,so,dest) -> let ctx' = (Some (name,C.Decl so))::ctx in C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) - | C.LetIn (name,so,dest) -> - let _,ty,metasenv,ugraph = - pack_coercions := false; - type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in - pack_coercions := true; - let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in - C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.LetIn (name,so,ty,dest) -> + let ctx' = Some (name,(C.Def (so,ty)))::ctx in + C.LetIn + (name, merge_coercions ctx so, merge_coercions ctx ty, + merge_coercions ctx' dest) | C.Appl l -> let l = List.map (merge_coercions ctx) l in let t = C.Appl l in