X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=e3392bf05ff949b9778aa96eccbe43d56b598aa7;hb=07151480b04db0ef4e77d09a5b7559ae5ab25ab4;hp=a5221c22976f3d3c337121cbb116e82b7a0bb88c;hpb=e82e30cc9885f2acdf03801c637aaacfd8c81d71;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index a5221c229..e3392bf05 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -40,14 +40,18 @@ exception AssertFailure of string;; let debug_print = fun _ -> () +let profiler = HExtlib.profile "CicRefine.fo_unif" + let fo_unif_subst subst context metasenv t1 t2 ugraph = try +let foo () = CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler.HExtlib.profile foo () with (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; - + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -255,11 +259,61 @@ and type_of_aux' metasenv context t ugraph = type_of_aux subst' metasenv' ((Some (name,(C.Decl s')))::context) t ugraph1 in - let sop,subst''',metasenv''',ugraph3 = - sort_of_prod subst'' metasenv'' - context (name,s') (sort1,sort2) ugraph2 - in - C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 + (try + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod subst'' metasenv'' + context (name,s') (sort1,sort2) ugraph2 + in + C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 + with + | RefineFailure _ as exn -> + (* given [t] of type [type_to_coerce] returns + * a term that has type [tgt_sort] eventually + * derived from (coercion [t]) *) + let refined_target = t' in + let sort_of_refined_target = sort2 in + let carr t subst context = CicMetaSubst.apply_subst subst t in + let coerce_to_sort tgt_sort t type_to_coerce subst ctx = + match type_to_coerce with + | Cic.Sort _ -> t + | term -> + let coercion_src = carr type_to_coerce subst ctx in + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let search = CoercGraph.look_for_coercion in + (match search coercion_src coercion_tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain "Coercions on metas") + | CoercGraph.SomeCoercion c -> Cic.Appl [c;t]) + in + (* this is probably not the best... *) + let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in + let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in + let new_src = + coerce_to_sort tgt_sort_for_pi_source s sort1 subst context + in + let context_with_new_src = + ((Some (name,(C.Decl new_src)))::context) + in + let new_tgt = + coerce_to_sort + tgt_sort_for_pi_target + refined_target sort_of_refined_target + subst context_with_new_src + in + let newprod = C.Prod (name,new_src,new_tgt) in + let _,sort_of_refined_prod,subst,metasenv,ugraph3 = + type_of_aux subst metasenv context newprod ugraph2 + in + (* this if for a coercion on the tail of the arrow *) + let new_target = + match sort_of_refined_target with + | Cic.Sort _ -> refined_target + | _ -> new_tgt + in + C.Prod(name,new_src,new_target), + sort_of_refined_prod,subst,metasenv,ugraph3) | C.Lambda (n,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -796,35 +850,39 @@ and type_of_aux' metasenv context t ugraph = 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) -> (* different than Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different than Coq manual!!! *) C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) let t' = CicUniv.fresh() 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 | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) C.Sort (C.Type 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 * brake the invariant that refine produce only well typed terms *) - (* TODO if we check the non meta term and if it is a sort then we are - * likely to know the exact value of the result e.g. if the rhs is a - * Sort (Prop | Set | CProp) then the result is the rhs *) + (* TODO if we check the non meta term and if it is a sort then we + * are likely to know the exact value of the result e.g. if the rhs + * is a Sort (Prop | Set | CProp) then the result is the rhs *) let (metasenv,idx) = CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv,ugraph1) = - fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph + fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' ugraph in t2'',subst,metasenv,ugraph1 - | (_,_) -> - raise (RefineFailure (Reason (sprintf - "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" - (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2'')))) + | _,_ -> + raise + (RefineFailure + (Reason + (sprintf + ("Two sorts were expected, found %s " ^^ + "(that reduces to %s) and %s (that reduces to %s)") + (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) + (CicPp.ppterm t2'')))) and eat_prods subst metasenv context hetype tlbody_and_type ugraph = let rec mk_prod metasenv context = @@ -873,11 +931,11 @@ and type_of_aux' metasenv context t ugraph = try fo_unif_subst subst context metasenv hetype hetype' ugraph with exn -> - debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" + debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" (CicPp.ppterm hetype) (CicPp.ppterm hetype') (CicMetaSubst.ppmetasenv [] metasenv) - (CicMetaSubst.ppsubst subst)); + (CicMetaSubst.ppsubst subst))); raise exn in @@ -895,13 +953,20 @@ and type_of_aux' metasenv context t ugraph = hete,subst,metasenv,ugraph1 with exn -> (* we search a coercion from hety to s *) - let coer = CoercGraph.look_for_coercion - (CicMetaSubst.apply_subst subst hety) - (CicMetaSubst.apply_subst subst s) + let coer = + let carr t subst context = + CicMetaSubst.apply_subst subst t + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s in match coer with - | None -> raise exn - | Some c -> + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain "Coercions on meta") + | CoercGraph.SomeCoercion c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in let coerced_args,metasenv',subst',t',ugraph2 = @@ -1070,16 +1135,24 @@ let type_of_aux' metasenv context term = try let (t,ty,m) = type_of_aux' metasenv context term in - debug_print - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); - debug_print - ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []); + debug_print (lazy + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty)); + debug_print (lazy + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m [])); (t,ty,m) with | RefineFailure msg as e -> - debug_print ("@@@ REFINE FAILED: " ^ msg); + debug_print (lazy ("@@@ REFINE FAILED: " ^ msg)); raise e | Uncertain msg as e -> - debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); + debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); raise e ;; *) + +let profiler2 = HExtlib.profile "CicRefine" + +let type_of_aux' metasenv context term ugraph = + profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph + +let typecheck metasenv uri obj = + profiler2.HExtlib.profile (typecheck metasenv uri) obj