X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=54055ebb6478633c47f3e2f952b6f1c11a707c93;hb=69c5a60dfa385a3d0e270ed38eb0d970366792c5;hp=0ef14696c5d46c68075698cde0f36070629f072c;hpb=3cab09fd975e4eb4f60de55edfbf2576032f5527;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 0ef14696c..54055ebb6 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -78,6 +78,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) + | Sys.Break -> raise exn | _ -> assert false in let loc = try @@ -140,7 +141,7 @@ let is_a_double_coercion t = | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> let sib2,head = last_of tl2 in true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl - (c2::sib2@[Cic.Implicit None])]) + (c2::sib2@[imp])]) | _ -> dummyres) | _ -> dummyres @@ -320,8 +321,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = + let module C = Cic in + let module S = CicSubstitution in + let module U = UriManager in let try_coercion t subst metasenv context ugraph coercion_tgt c = - let coerced = Cic.Appl[c;t] in + let coerced = C.Appl[c;t] in try let newt,_,subst,metasenv,ugraph = type_of_aux subst metasenv context coerced ugraph @@ -333,9 +337,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t with | RefineFailure _ | Uncertain _ -> None in - let module C = Cic in - let module S = CicSubstitution in - let module U = UriManager in let (t',_,_,_,_) as res = match t with (* function *) @@ -357,9 +358,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> + Failure _ -> enrich localization_tbl t - (RefineFailure (lazy "Not a close term"))) + (RefineFailure (lazy "Not a closed term"))) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst @@ -578,8 +579,9 @@ 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'),CicSubstitution.subst s' inferredty, - subst'',metasenv'',ugraph2 + C.LetIn (n,s',t'), + CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, + subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph @@ -1059,6 +1061,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | Some t,Some (_,C.Def (ct,_)) -> 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 subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in @@ -1174,6 +1177,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicPp.ppterm t2'')))) and avoid_double_coercion context subst metasenv ugraph t ty = + if not !pack_coercions then + t,ty,subst,metasenv,ugraph + else let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in if b then let source_carr = CoercGraph.source_of c2 in @@ -1214,11 +1220,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | RefineFailure s | Uncertain s -> debug_print s;debug_print (lazy "goon\n"); try + let old_pack_coercions = !pack_coercions in pack_coercions := false; (* to avoid diverging *) let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = type_of_aux subst metasenv context c1_c2_implicit ugraph in - pack_coercions := true; + pack_coercions := old_pack_coercions; let b, _, _, _, _ = is_a_double_coercion refined_c1_c2_implicit in @@ -1463,8 +1470,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context ^ - "\nReason: " ^ Printexc.to_string exn))) exn + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Printexc.to_string exn*)))) exn (* }}} end coercion stuff *) in eat_prods_and_args pristinemenv metasenv subst context pristinehe he @@ -1492,7 +1499,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst,metasenv,ugraph,hetype,he,args_bo_and_ty else (* this (says CSC) is also useful to infer dependent types *) - fix_arity metasenv context subst he hetype args_bo_and_ty ugraph + try + fix_arity metasenv context subst he hetype args_bo_and_ty ugraph + with RefineFailure _ | Uncertain _ as exn -> + (* unable to fix arity *) + more_args_than_expected localization_tbl + subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph = eat_prods_and_args @@ -1724,7 +1736,11 @@ let pack_coercion metasenv ctx t = 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 ctx' = Some (name,(C.Def (so,None)))::ctx in + let _,ty,metasenv,ugraph = + pack_coercions := false; + type_of_aux' metasenv ctx so CicUniv.empty_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.Appl l -> let l = List.map (merge_coercions ctx) l in @@ -1739,7 +1755,6 @@ let pack_coercion metasenv ctx t = try type_of_aux' metasenv ctx t ugraph with RefineFailure _ | Uncertain _ -> - prerr_endline (CicPp.ppterm t); t, t, [], ugraph in insert_coercions := old_insert_coercions;