X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=856c9a58622480d6f938cbeb0e8a25c1ce913473;hb=975ad45cc779a6bee3d450a006347cc23ca3977e;hp=d10e177d02d61b3aa783353a5582fa134f06dad4;hpb=70c533b5592b0bb91f544fec275213b866bf33ea;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index d10e177d0..856c9a586 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -78,8 +78,10 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) + | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg) | Sys.Break -> raise exn - | _ -> assert false in + | _ -> prerr_endline (Printexc.to_string exn); assert false + in let loc = try Cic.CicHash.find localization_tbl t @@ -136,9 +138,9 @@ let is_a_double_coercion t = let imp = Cic.Implicit None in let dummyres = false,imp, imp,imp,imp in match t with - | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> + | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + | 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])]) @@ -324,18 +326,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t 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 = - match c with - C.Appl l2 -> C.Appl (l2@[t]) - | _ -> C.Appl [c;t] + let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) = + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last t ugraph in try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context coerced ugraph - in let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt coercion_tgt + avoid_double_coercion context subst metasenv ugraph coerced + coercion_tgt in Some (newt, tty, subst, metasenv, ugraph) with @@ -426,7 +424,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl te' ~f:(fun _ -> - lazy ("The term " ^ + lazy ("(3)The term " ^ CicMetaSubst.ppterm_in_context metasenv'' subst'' te' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty @@ -452,14 +450,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | term -> let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt + CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt in (match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl t (RefineFailure - (lazy ("The term " ^ + (lazy ("(4)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -467,7 +466,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotMetaClosed -> enrich localization_tbl t (Uncertain - (lazy ("The term " ^ + (lazy ("(5)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -475,8 +474,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (try_coercion - t subst metasenv context ugraph coercion_tgt) + (try_coercion t subst context ugraph coercion_tgt) candidates in match selected with @@ -484,7 +482,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | None -> enrich localization_tbl t (RefineFailure - (lazy ("The term " ^ + (lazy ("(6)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ @@ -514,7 +512,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 | C.Lambda (n,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let s',sort1,subst',metasenv',ugraph1 = @@ -526,14 +523,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | coercion_src -> let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt + CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt in match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl s' (RefineFailure - (lazy ("The term " ^ + (lazy ("(7)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -541,7 +539,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.NotMetaClosed -> enrich localization_tbl s' (Uncertain - (lazy ("The term " ^ + (lazy ("(8)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -549,16 +547,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (try_coercion - s' subst' metasenv' context ugraph1 coercion_tgt) - candidates + (try_coercion s' subst' context ugraph1 coercion_tgt) + candidates in match selected with | Some x -> x | None -> enrich localization_tbl s' (RefineFailure - (lazy ("The term " ^ + (lazy ("(9)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context ~metasenv @@ -688,9 +685,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t expected_type' actual_type ugraph2 with exn -> + prerr_endline (CicMetaSubst.ppmetasenv subst metasenv); + prerr_endline (CicMetaSubst.ppsubst subst ~metasenv); enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(10)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type @@ -711,8 +710,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* TODO: check if the sort elimination * is allowed: [(I q1 ... qr)|B] *) let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = - List.fold_left - (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p -> + List.fold_right + (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) -> let constructor = if left_args = [] then (C.MutConstruct (uri,i,j,exp_named_subst)) @@ -727,12 +726,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context constructor ugraph1 in let outtypeinstance,subst,metasenv,ugraph3 = - check_branch 0 context metasenv subst no_left_params - actual_type constructor' expected_type ugraph2 + try + check_branch 0 context metasenv subst + no_left_params actual_type constructor' expected_type + ugraph2 + with + exn -> + enrich localization_tbl constructor' + ~f:(fun _ -> + lazy ("(11)The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst p' + 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)) exn in - (pl @ [p'],j+1, - outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) - ([],1,[],subst,metasenv,ugraph3) pl + (p'::pl,j-1, + outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) + pl ([],List.length pl,[],subst,metasenv,ugraph3) in (* we are left to check that the outype matches his instances. @@ -910,7 +922,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(12)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' @@ -925,17 +937,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (C.Appl(outtype::right_args@[term]))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1,len = List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> + (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl ty')) :: types, ugraph - ) ([],subst,metasenv,[],ugraph) fl + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) + :: types, ugraph, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl in - let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left @@ -951,7 +963,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(13)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -978,17 +990,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Fix (i,fl''),ty,subst,metasenv,ugraph2 | C.CoFix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1,len = List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> + (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl ty')) :: types, ugraph1 - ) ([],subst,metasenv,[],ugraph) fl + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) :: + types, ugraph1, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl in - let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left @@ -1004,7 +1016,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(14)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1204,29 +1216,27 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il if b then let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in - (match CoercGraph.look_for_coercion source_carr tgt_carr + (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr with | CoercGraph.SomeCoercion candidates -> - let selected = + let selected = HExtlib.list_findopt - (function + (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 -> - let newt = - match c with - | Cic.Appl l -> Cic.Appl (l @ [head]) - | _ -> Cic.Appl [c;head] - in - debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last head ugraph in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); (try debug_print (lazy ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c)); let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in + type_of_aux subst metasenv context c ugraph in debug_print (lazy "tipa..."); let subst, metasenv, ugraph = (* COME MAI C'ERA UN IF su !pack_coercions ??? *) @@ -1340,27 +1350,34 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il he in let x,xty,subst,metasenv,ugraph = - type_of_aux subst metasenv context x ugraph + (*CSC: here unsharing is necessary to avoid an unwanted + relocalization. However, this also shows a great source of + inefficiency: "x" is refined twice (once now and once in the + subsequent eat_prods_and_args). Morevoer, how is divergence avoided? + *) + type_of_aux subst metasenv context (Unshare.unshare x) ugraph in let carr_src = CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) in let carr_tgt = CoercDb.Fun 0 in - match CoercGraph.look_for_coercion' carr_src carr_tgt with + match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt - (fun coerc -> - let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t)); + (fun (metasenv,last,coerc) -> + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last x ugraph in + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) let t,tty,subst,metasenv,ugraph = - type_of_aux subst metasenv context t ugraph + type_of_aux subst metasenv context coerc ugraph in try let metasenv, hetype' = @@ -1386,8 +1403,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None - with Uncertain _ | RefineFailure _ -> None - | exn -> assert false) (* ritornare None, e' un localized *) + with + Uncertain _ + | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) (* ritornare None, e' un localized *) candidates with | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> @@ -1425,14 +1446,15 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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, c_s + CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s in (match coer with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl hete exn ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(15)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1442,7 +1464,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NotMetaClosed -> enrich localization_tbl hete exn ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(16)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1452,12 +1474,14 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (fun c -> + (fun (metasenv,last,c) -> try - let t = Cic.Appl[c;hete] in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last hete + ugraph in let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context - t ugraph + c ugraph in let newt, newty, subst, metasenv, ugraph = avoid_double_coercion context subst metasenv @@ -1476,7 +1500,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | None -> enrich localization_tbl hete ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(1)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1486,7 +1510,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | exn -> enrich localization_tbl hete ~f:(fun _ -> - (lazy ("The term " ^ + (lazy ("(2)The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst hety @@ -1712,6 +1736,7 @@ let typecheck metasenv uri obj ~localization_tbl = let con_context = List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in (* second phase: we fix only the constructors *) + let saved_menv = metasenv in let metasenv,ugraph,tys = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> @@ -1724,7 +1749,7 @@ let typecheck metasenv uri obj ~localization_tbl = let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in - metasenv,ugraph,(name,ty')::res + metasenv@saved_menv,ugraph,(name,ty')::res ) cl (metasenv,ugraph,[]) in metasenv,ugraph,(name,b,ty,cl')::res @@ -1759,7 +1784,7 @@ let pack_coercion metasenv ctx t = | C.LetIn (name,so,dest) -> let _,ty,metasenv,ugraph = pack_coercions := false; - type_of_aux' metasenv ctx so CicUniv.empty_ugraph in + 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) @@ -1769,7 +1794,7 @@ let pack_coercion metasenv ctx t = let b,_,_,_,_ = is_a_double_coercion t in (* prerr_endline "CANDIDATO!!!!"; *) if b then - let ugraph = CicUniv.empty_ugraph in + let ugraph = CicUniv.oblivion_ugraph in let old_insert_coercions = !insert_coercions in insert_coercions := false; let newt, _, menv, _ =