X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=5aa96944d4e50295cac8094e69210f75e5cff99b;hb=ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a;hp=970d3e05f70b2c4deb33a993fbdf9ceaf0cbb6fa;hpb=14139694d817bd900f7f0fb412c69cf431baaad9;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 970d3e05f..5aa96944d 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -337,15 +337,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 +438,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 +470,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)) -> @@ -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 ( @@ -939,13 +949,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 +966,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) -> @@ -1736,11 +1761,7 @@ 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 @@ -1826,7 +1847,7 @@ 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 @@ -1856,10 +1877,13 @@ let typecheck metasenv uri obj ~localization_tbl = " but is here used with type " ^ CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) in - match exn with - RefineFailure _ -> raise (HExtlib.Localized (loc exn,RefineFailure msg)) - | Uncertain _ -> raise (HExtlib.Localized (loc exn,Uncertain msg)) - | _ -> assert false + 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 @@ -1918,7 +1942,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 @@ -1954,13 +1978,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