X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=9fb3548d6e4362d8a621b50939f55f85763b5b18;hb=0f76dec7bd31a5914c27c38fb28bf2279a7cdbc1;hp=10563186461a2601c30d4799d7c6657db8231da0;hpb=9c5446cc2a792812df63965d323f71636194bf75;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 105631864..9fb3548d6 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -32,8 +32,36 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; let insert_coercions = ref true +let pack_coercions = ref true -let debug_print = fun _ -> () +let debug = false;; + +let debug_print = + if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());; + +let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" + +let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods2.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + +let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods" + +let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; let profiler = HExtlib.profile "CicRefine.fo_unif" @@ -52,7 +80,10 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) - | _ -> assert false in + | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg) + | Sys.Break -> raise exn + | _ -> prerr_endline (Printexc.to_string exn); assert false + in let loc = try Cic.CicHash.find localization_tbl t @@ -99,24 +130,81 @@ let exp_impl metasenv subst context = let is_a_double_coercion t = let last_of l = - let rec aux = function - | x::[] -> x - | x::tl -> aux tl + let rec aux acc = function + | x::[] -> acc,x + | x::tl -> aux (acc@[x]) tl | [] -> assert false in - aux l - in - let dummyres = - false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None + aux [] l in + 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 - | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> - let head = last_of tl2 in - true, c1, c2, head + | 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])]) | _ -> dummyres) | _ -> dummyres + +let more_args_than_expected + localization_tbl metasenv subst he context hetype' tlbody_and_type exn += + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ + " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ + ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected") + in + enrich localization_tbl he ~f:(fun _-> msg) exn +;; + +let mk_prod_of_metas metasenv context' subst args = + let rec mk_prod metasenv context' = function + | [] -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + metasenv,Cic.Meta (idx, irl) + | (_,argty)::tl -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + let meta = Cic.Meta (idx,irl) in + let name = + (* The name must be fresh for context. *) + (* Nevertheless, argty is well-typed only in context. *) + (* Thus I generate a name (name_hint) in context and *) + (* then I generate a name --- using the hint name_hint *) + (* --- that is fresh in context'. *) + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context') + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) + in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context' name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = + mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl + in + metasenv,Cic.Prod (name,meta,target) + in + mk_prod metasenv context' args +;; let rec type_of_constant uri ugraph = let module C = Cic in @@ -261,9 +349,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 @@ -298,8 +386,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst', metasenv',ugraph1) | C.Sort (C.Type tno) -> let tno' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt tno' tno ugraph in - t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + (try + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph | C.Implicit infos -> @@ -312,77 +403,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - (try - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty' ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - exn -> - enrich localization_tbl te' - ~f:(fun _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst'' te' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst'' inferredty - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst'' ty' context)) exn - ) - | C.Prod (name,s,t) -> - let carr t subst context = CicMetaSubst.apply_subst subst t in - let coerce_to_sort in_source tgt_sort t type_to_coerce - subst context metasenv uragph - = - if not !insert_coercions then - t,type_to_coerce,subst,metasenv,ugraph - else - let coercion_src = carr type_to_coerce subst context in - match coercion_src with - | Cic.Sort _ -> - t,type_to_coerce,subst,metasenv,ugraph - | Cic.Meta _ as meta -> - t, meta, subst, metasenv, ugraph - | Cic.Cast _ as cast -> - t, cast, subst, metasenv, ugraph - | term -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt - in - (match boh with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl t - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl t - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.SomeCoercion c -> - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context (Cic.Appl[c;t]) - ugraph in - let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph - newt coercion_tgt - in - newt, tty, subst, metasenv, ugraph) + let (te', ty'), subst''',metasenv''',ugraph3 = + coerce_to_something true localization_tbl te' inferredty ty' + subst'' metasenv'' context ugraph2 in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let s',sort1,subst', metasenv',ugraph1 = - coerce_to_sort true (Cic.Type(CicUniv.fresh())) + coerce_to_sort localization_tbl s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (name,(C.Decl s')))::context) in @@ -391,56 +422,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context_for_t t ugraph1 in let t',sort2,subst'',metasenv'',ugraph2 = - coerce_to_sort false (Cic.Type(CicUniv.fresh())) + coerce_to_sort localization_tbl t' sort2 subst'' context_for_t metasenv'' ugraph2 in let sop,subst''',metasenv''',ugraph3 = - sort_of_prod subst'' metasenv'' - context (name,s') (sort1,sort2) ugraph2 + sort_of_prod localization_tbl subst'' metasenv'' + context (name,s') t' (sort1,sort2) ugraph2 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 + type_of_aux subst metasenv context s ugraph + in let s',sort1,subst',metasenv',ugraph1 = - if not !insert_coercions then - s',sort1, subst', metasenv', ugraph1 - else - match CicReduction.whd ~subst:subst' context sort1 with - | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 - | coercion_src -> - let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt - in - match boh with - | CoercGraph.SomeCoercion c -> - let newt,_,subst',metasenv',ugraph1 = - type_of_aux subst' metasenv' context (Cic.Appl[c;s']) - ugraph1 in - let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion context subst' metasenv' - ugraph1 newt coercion_tgt - in - newt, tty, subst', metasenv', ugraph1 - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl s' - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl s' - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ - " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context - subst coercion_src context ^ " that is not a sort"))) + coerce_to_sort localization_tbl + s' sort1 subst' context metasenv' ugraph1 in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -463,27 +459,23 @@ 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 in let tlbody_and_type,subst'',metasenv'',ugraph2 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) tl ([],subst',metasenv',ugraph1) + typeof_list subst' metasenv' context ugraph1 tl in - let tl',applty,subst''',metasenv''',ugraph3 = + let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 = eat_prods true subst'' metasenv'' context he' hetype tlbody_and_type ugraph2 in - avoid_double_coercion context - subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty + let newappl = (C.Appl (coerced_he::coerced_args)) in + avoid_double_coercion + context subst''' metasenv''' ugraph3 newappl applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -571,12 +563,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst term' + lazy ("(10)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst actual_type + CicMetaSubst.ppterm_in_context ~metasenv subst actual_type context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_type' context)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) in let rec instantiate_prod t = function @@ -592,8 +584,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)) @@ -608,12 +600,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. @@ -721,8 +726,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t candidate_oty,ugraph,metasenv,subst with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> + | RefineFailure _ | Uncertain _ -> None,ugraph,metasenv,subst ) (Some instance',ugraph4,metasenv,subst) tl in @@ -760,15 +764,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst,metasenv,ugraph) | _ -> (* easy case *) let tlbody_and_type,subst,metasenv,ugraph4 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + typeof_list subst metasenv context ugraph4 (right_args @ [term']) in - let _,_,subst,metasenv,ugraph4 = + let _,_,_,subst,metasenv,ugraph4 = eat_prods false subst metasenv context outtype outtypety tlbody_and_type ugraph4 in @@ -797,12 +795,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst p + lazy ("(12)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst instance' + CicMetaSubst.ppterm_in_context ~metasenv subst instance' context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst instance + CicMetaSubst.ppterm_in_context ~metasenv subst instance context))) (subst,metasenv,ugraph5) pl' outtypeinstances in @@ -812,17 +810,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 @@ -838,12 +836,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + lazy ("(13)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'] , subst',metasenv',ugraph' @@ -865,17 +863,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 @@ -891,12 +889,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + lazy ("(14)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'],subst',metasenv',ugraph' @@ -955,8 +953,9 @@ 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)))))) + 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)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -967,19 +966,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context)))) + (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext ~metasenv subst canonical_context)))) and check_exp_named_subst metasubst metasenv context tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = @@ -1012,9 +1011,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t with _ -> raise (RefineFailure (lazy ("Wrong Explicit Named Substitution: " ^ - CicMetaSubst.ppterm metasubst' typeoft ^ + CicMetaSubst.ppterm metasenv' metasubst' typeoft ^ " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar))) + CicMetaSubst.ppterm metasenv' metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -1026,7 +1025,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t check_exp_named_subst_aux metasubst metasenv [] tl ugraph - and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph = + and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2) + ugraph + = let module C = Cic in let context_for_t2 = (Some (name,C.Decl s))::context in let t1'' = CicReduction.whd ~subst context t1 in @@ -1038,9 +1039,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t C.Sort s2,subst,metasenv,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 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 + (try + 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 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph @@ -1059,203 +1063,628 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t with _ -> assert false (* unification against a metavariable *) in t2'',subst,metasenv,ugraph1 + | (C.Sort _,_) + | (C.Meta _,_) -> + enrich localization_tbl s + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst t context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)))) | _,_ -> - raise - (RefineFailure - (lazy - (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'')))) + enrich localization_tbl t + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst s context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)))) and avoid_double_coercion context subst metasenv ugraph t ty = - let b, c1, c2, head = is_a_double_coercion t in + 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 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 c -> - let newt = - match c with - Cic.Appl l -> Cic.Appl (l @ [head]) - | _ -> Cic.Appl [c;head] + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (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 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 c)); + let newt,_,subst,metasenv,ugraph = + 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 ??? *) + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print (lazy "unifica..."); + Some (newt, ty, subst, metasenv, ugraph) + with + | RefineFailure s | Uncertain s when not !pack_coercions-> + debug_print s; debug_print (lazy "stop\n");None + | 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 := old_pack_coercions; + let b, _, _, _, _ = + is_a_double_coercion refined_c1_c2_implicit + in + if b then + None + else + let head' = + match refined_c1_c2_implicit with + | Cic.Appl l -> HExtlib.list_last l + | _ -> assert false + in + let subst, metasenv, ugraph = + try fo_unif_subst subst context metasenv + head head' ugraph + with RefineFailure s| Uncertain s-> + debug_print s;assert false + in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv + refined_c1_c2_implicit t ugraph + in + Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph) + with + | RefineFailure s | Uncertain s -> + pack_coercions := true;debug_print s;None + | exn -> pack_coercions := true; raise exn)) + candidates in - (try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in - debug_print - (lazy - ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); - newt, ty, subst, metasenv, ugraph - with - RefineFailure _ -> - prerr_endline ("#### Coercion not packed (Refine_failure): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); - assert false - | Uncertain _ -> - prerr_endline ("#### Coercion not packed (Uncerctain case): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); - assert false) - | _ -> assert false) (* the composite coercion must exist *) + (match selected with + | Some x -> x + | None -> + debug_print + (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); + t, ty, subst, metasenv, ugraph) + | _ -> t, ty, subst, metasenv, ugraph) else t, ty, subst, metasenv, ugraph + and typeof_list subst metasenv context ugraph l = + let tlbody_and_type,subst,metasenv,ugraph = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) l ([],subst,metasenv,ugraph) + in + tlbody_and_type,subst,metasenv,ugraph + and eat_prods - allow_coercions subst metasenv context he hetype tlbody_and_type ugraph + allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = - let rec mk_prod metasenv context' = + (* given he:hety, gives beack all (c he) such that (c e):?->? *) + let fix_arity exn metasenv context subst he hetype ugraph = + let hetype = CicMetaSubst.apply_subst subst hetype in + let src = CoercDb.coerc_carr_of_term hetype in + let tgt = CoercDb.Fun 0 in + match CoercGraph.look_for_coercion' metasenv subst context src tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotMetaClosed + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates + | CoercGraph.SomeCoercion candidates -> + HExtlib.filter_map + (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 t,tty,subst,metasenv,ugraph = + type_of_aux subst metasenv context coerc ugraph in + (*{{{*)debug_print (lazy (" refined: "^ pp t)); + debug_print (lazy (" has type: "^ pp tty));(*}}}*) + Some (t,tty,subst,metasenv,ugraph) + with + | Uncertain _ | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) + candidates + in + (* aux function to process the type of the head and the args in parallel *) + let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs = function - [] -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - let meta = Cic.Meta (idx,irl) in - let name = - (* The name must be fresh for context. *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in context'. *) - let name_hint = - (* Cic.Name "pippo" *) - FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - ~typ:(CicMetaSubst.apply_subst subst argty) + | [] -> newargs,subst,metasenv,he,hetype,ugraph + | (hete, hety)::tl as args -> + match (CicReduction.whd ~subst context hetype) with + | Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph = + coerce_to_something allow_coercions localization_tbl + hete hety s subst metasenv context ugraph in + eat_prods_and_args + metasenv subst context he (CicSubstitution.subst (fst arg) t) + ugraph (newargs@[arg]) tl + | _ -> + let he = + match he, newargs with + | _, [] -> he + | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs) + | _ -> Cic.Appl (he::List.map fst newargs) in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name ~subst - [] context' name_hint ~typ:(Cic.Sort Cic.Prop) - in - let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl - in - metasenv,Cic.Prod (name,meta,target) + (*{{{*) debug_print (lazy + let pp x = + CicMetaSubst.ppterm_in_context ~metasenv subst x context in + "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^ + "\n but is applyed to: " ^ String.concat ";" + (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*) + let exn = RefineFailure (lazy ("more args than expected")) in + let possible_fixes = + fix_arity exn metasenv context subst he hetype ugraph in + match + HExtlib.list_findopt + (fun (he,hetype,subst,metasenv,ugraph) -> + (* {{{ *)debug_print (lazy ("Try fix: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context)); + debug_print (lazy (" of type: "^ + CicMetaSubst.ppterm_in_context + ~metasenv subst hetype context)); (* }}} *) + try + Some (eat_prods_and_args + metasenv subst context he hetype ugraph [] args) + with RefineFailure _ | Uncertain _ -> None) + possible_fixes + with + | Some x -> x + | None -> + more_args_than_expected localization_tbl metasenv + subst he context hetype args_bo_and_ty exn in - let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in - let (subst, metasenv,ugraph1) = - try - fo_unif_subst subst context metasenv hetype hetype' ugraph - with exn -> - enrich localization_tbl he - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he - context ^ " (that has type " ^ - CicMetaSubst.ppterm_in_context subst hetype - context ^ ") is here applied to " ^ - string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected" - (* "\nReason: " ^ Lazy.force exn*)))) exn + (* first we check if we are in the simple case of a meta closed term *) + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then + (* this optimization is to postpone fix_arity (the most common case)*) + subst,metasenv,ugraph,hetype,he,args_bo_and_ty + else + (* this (says CSC) is also useful to infer dependent types *) + let pristinemenv = metasenv in + let metasenv,hetype' = + mk_prod_of_metas metasenv context subst args_bo_and_ty + in + try + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph + in + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + with RefineFailure _ | Uncertain _ -> + subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty in - let rec eat_prods metasenv subst context hetype ugraph = - function - | [] -> [],metasenv,subst,hetype,ugraph - | (hete, hety)::tl -> - (match hetype with - Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph1 = - try - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv hety s ugraph - in - hete,subst,metasenv,ugraph1 - with exn when allow_coercions && !insert_coercions -> - (* we search a coercion from hety to s *) - let coer, tgt_carr = - 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, c_s + let coerced_args,subst,metasenv,he,t,ugraph = + eat_prods_and_args + metasenv subst context he hetype' ugraph1 [] args_bo_and_ty + in + he,(List.map fst coerced_args),t,subst,metasenv,ugraph + + and coerce_to_something + allow_coercions localization_tbl t infty expty subst metasenv context ugraph + = + let module CS = CicSubstitution in + let module CR = CicReduction in + let cs_subst = CS.subst ~avoid_beta_redexes:true in + let coerce_atom_to_something t infty expty subst metasenv context ugraph = + debug_print (lazy ("COERCE_ATOM_TO_SOMETHING")); + let coer = + CoercGraph.look_for_coercion metasenv subst context infty expty + in + match coer with + | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy + "coerce_atom_to_something fails since not meta closed")) + | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ + | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + "coerce_atom_to_something fails since no coercions found")) + | CoercGraph.SomeCoercion candidates -> + debug_print (lazy (string_of_int (List.length candidates) ^ + " candidates found")); + let uncertain = ref false in + let selected = + let posibilities = + HExtlib.filter_map + (fun (metasenv,last,c) -> + try + (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ + " <==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last t ugraph + in + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context c ugraph in + let newt, newty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv ugraph newt expty + in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv newhety expty ugraph in + Some ((newt,newty), subst, metasenv, ugraph) + with + | Uncertain _ -> uncertain := true; None + | RefineFailure _ -> None) + candidates + in + match + List.fast_sort + (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2) + posibilities + with + | [] -> None + | x::_ -> Some x + in + match selected with + | Some x -> x + | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails")) + | None -> raise (RefineFailure (lazy "coerce_atom fails")) + in + let rec coerce_to_something_aux + t infty expty subst metasenv context ugraph + = + try + let subst, metasenv, ugraph = + 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 + 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 + let expty = clean expty subst context in + let t = clean t subst context in + (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*) + let (coerced,_),subst,metasenv,_ as result = + match infty, expty, t with + | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) -> + (*{{{*) debug_print (lazy "FIX"); + (match fl with + [name,i,_(* infty *),bo] -> + let context_bo = + Some (Cic.Name name,Cic.Decl expty)::context in + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux (Cic.Rel 1) + (CS.lift 1 expty) (CS.lift 1 infty) subst + metasenv context_bo ugraph in + let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in + let (bo,_), subst, metasenv, ugraph = + coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1 + expty) subst + metasenv context_bo ugraph + in + (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph + | _ -> assert false (* not implemented yet *)) (*}}}*) + | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> + (*{{{*) debug_print (lazy "CASE"); + (* {{{ helper functions *) + let get_cl_and_left_p uri tyno outty ugraph = + match CicEnvironment.get_obj ugraph uri with + | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> + let count_pis t = + let rec aux ctx t = + match CicReduction.whd ~delta:false ctx t with + | Cic.Prod (name,src,tgt) -> + let ctx = Some (name, Cic.Decl src) :: ctx in + 1 + aux ctx tgt + | _ -> 0 in - (match coer with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl hete - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion c -> - try - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - (Cic.Appl[c;hete]) ugraph in - let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt tgt_carr in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - newt, subst, metasenv, ugraph - with _ -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn) - | exn -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn + aux [] t + in + let rec skip_lambda_delifting t n = + match t,n with + | _,0 -> t + | Cic.Lambda (_,_,t),n -> + skip_lambda_delifting + (CS.subst (Cic.Implicit None) t) (n - 1) + | _ -> assert false + in + let get_l_r_p n = function + | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] + | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> + HExtlib.split_nth n args + | _ -> assert false + in + let _, _, ty, cl = List.nth tl tyno in + let pis = count_pis ty in + let rno = pis - leftno in + let t = skip_lambda_delifting outty rno in + let left_p, _ = get_l_r_p leftno t in + let instantiale_with_left cl = + List.map + (fun ty -> + List.fold_left + (fun t p -> match t with + | Cic.Prod (_,_,t) -> + cs_subst p t + | _-> assert false) + ty left_p) + cl + in + let cl = instantiale_with_left (List.map snd cl) in + cl, left_p, leftno, rno, ugraph + | _ -> raise exn + in + let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = + match t,n with + | _,0 -> + let rec mkr n = function + | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl in - let coerced_args,metasenv',subst',t',ugraph2 = - eat_prods metasenv subst context - (CicSubstitution.subst arg t) ugraph1 tl + let bo = + CicReplace.replace_lifting + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:ctx + ~what:(matched::right_p) + ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) + ~where:bo in - arg::coerced_args,metasenv',subst',t',ugraph2 - | _ -> assert false - ) - in - let coerced_args,metasenv,subst,t,ugraph2 = - eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type + bo + | Cic.Lambda (name, src, tgt),_ -> + Cic.Lambda (name, src, + keep_lambdas_and_put_expty + (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo) + (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1)) + | _ -> assert false + in + let eq_uri, eq, eq_refl = + match LibraryObjects.eq_URI () with + | None -> HLog.warn "no default equality"; raise exn + | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) + in + let add_params + metasenv subst context uri tyno cty outty mty m leftno i + = + let rec aux context outty par k mty m = function + | Cic.Prod (name, src, tgt) -> + let t,k = + aux + (Some (name, Cic.Decl src) :: context) + (CS.lift 1 outty) (Cic.Rel k::par) (k+1) + (CS.lift 1 mty) (CS.lift 1 m) tgt + in + Cic.Prod (name, src, t), k + | Cic.MutInd _ -> + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + if par <> [] then Cic.Appl (k::par) else k + in + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl [outty;k])))),k + | Cic.Appl (Cic.MutInd _::pl) -> + let left_p,right_p = HExtlib.split_nth leftno pl in + let has_rights = right_p <> [] in + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + Cic.Appl (k::left_p@par) + in + let right_p = + try match + CicTypeChecker.type_of_aux' ~subst metasenv context k + CicUniv.oblivion_ugraph + with + | Cic.Appl (Cic.MutInd _::args),_ -> + snd (HExtlib.split_nth leftno args) + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _-> assert false + in + if has_rights then + CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k])),k + else + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k]))))),k + | _ -> assert false + in + aux context outty [] 1 mty m cty + in + let add_lambda_for_refl_m pbo rno mty m k cty = + (* k lives in the right context *) + if rno <> 0 then pbo else + let rec aux mty m = function + | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> + Cic.Lambda (name,src, + (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) + | t,_ -> + Cic.Lambda (Cic.Name "p", + Cic.Appl [eq; mty; m; k],CS.lift 1 t) + in + aux mty m (pbo,cty) + in + let add_pi_for_refl_m new_outty mty m rno = + if rno <> 0 then new_outty else + let rec aux m mty = function + | Cic.Lambda (name, src, tgt) -> + Cic.Lambda (name, src, + aux (CS.lift 1 m) (CS.lift 1 mty) tgt) + | t -> + Cic.Prod + (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], + CS.lift 1 t) + in + aux m mty new_outty + in (* }}} end helper functions *) + (* constructors types with left params already instantiated *) + let outty = CicMetaSubst.apply_subst subst outty in + let cl, left_p, leftno,rno,ugraph = + get_cl_and_left_p uri tyno outty ugraph + in + let right_p, mty = + try + match + CicTypeChecker.type_of_aux' ~subst metasenv context m + CicUniv.oblivion_ugraph + with + | Cic.MutInd _ as mty,_ -> [], mty + | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + snd (HExtlib.split_nth leftno args), mty + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _ -> assert false + in + let new_outty = + keep_lambdas_and_put_expty context outty expty right_p m (rno+1) + in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let _,pl,subst,metasenv,ugraph = + List.fold_right2 + (fun cty pbo (i, acc, s, menv, ugraph) -> + (* Pi k_par, (Pi H:m=(K_i left_par k_par)), + * (new_)outty right_par (K_i left_par k_par) *) + let infty_pbo, _ = + add_params menv s context uri tyno + cty outty mty m leftno i in + debug_print + (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context + ~metasenv subst infty_pbo context)); + let expty_pbo, k = (* k is (K_i left_par k_par) *) + add_params menv s context uri tyno + cty new_outty mty m leftno i in + debug_print + (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context + ~metasenv subst expty_pbo context)); + let pbo = add_lambda_for_refl_m pbo rno mty m k cty in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + let (pbo, _), subst, metasenv, ugraph = + coerce_to_something_aux pbo infty_pbo expty_pbo + s menv context ugraph + in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + (i-1, pbo::acc, subst, metasenv, ugraph)) + cl pl (List.length pl, [], subst, metasenv, ugraph) + in + let new_outty = add_pi_for_refl_m new_outty mty m rno in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let t = + if rno = 0 then + let refl_m=Cic.Appl[eq_refl;mty;m]in + Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] + else + Cic.MutCase(uri,tyno,new_outty,m,pl) + in + (t, expty), subst, metasenv, ugraph (*}}}*) + | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> + (*{{{*) debug_print (lazy "LAM"); + let name_con = + FreshNamesGenerator.mk_fresh_name + ~subst metasenv context ~typ:src2 Cic.Anonymous + in + let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in + (* contravariant part: the argument of f:src->ty *) + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux + (Cic.Rel 1) (CS.lift 1 src2) + (CS.lift 1 src) subst metasenv context_src2 ugraph + in + (* covariant part: the result of f(c x); x:src2; (c x):src *) + let name_t, bo = + match t with + | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo) + | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] + in + (* we fix the possible dependency problem in the source ty *) + let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in + let (bo, _), subst, metasenv, ugraph = + coerce_to_something_aux + bo ty ty2 subst metasenv context_src2 ugraph + in + let coerced = Cic.Lambda (name_t,src2, bo) in + (coerced, expty), subst, metasenv, ugraph (*}}}*) + | _ -> + (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context + ~metasenv subst infty context ^ " ==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); + coerce_atom_to_something + t infty expty subst metasenv context ugraph (*}}}*) + in + debug_print (lazy ("COERCE TO SOMETHING END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst coerced context)); + result in - coerced_args,t,subst,metasenv,ugraph2 + try + coerce_to_something_aux t infty expty subst metasenv context ugraph + with Uncertain _ | RefineFailure _ as exn -> + let f _ = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst t context ^ + " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst + infty context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context metasenv subst expty context) + in + enrich localization_tbl ~f t exn + + and coerce_to_sort localization_tbl t infty subst context metasenv uragph = + match CicReduction.whd ~delta:false ~subst context infty with + | Cic.Meta _ | Cic.Sort _ -> + t,infty, subst, metasenv, ugraph + | src -> + debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context + ~metasenv subst src context)); + let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in + try + let (t, ty_t), subst, metasenv, ugraph = + coerce_to_something true + localization_tbl t src tgt subst metasenv context ugraph + in + debug_print (lazy ("COERCE TO SORT END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + t, ty_t, subst, metasenv, ugraph + with HExtlib.Localized (_, exn) -> + let f _ = + lazy ("(7)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context + ^ " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst src context + ^ " that is not a sort") + in + enrich localization_tbl ~f t exn in (* eat prods ends here! *) @@ -1305,12 +1734,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; -let type_of_aux' ?localization_tbl metasenv context term ugraph = - try - type_of_aux' ?localization_tbl metasenv context term ugraph - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) - let undebrujin uri typesno tys t = snd (List.fold_right @@ -1442,6 +1865,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) -> @@ -1454,7 +1878,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 @@ -1487,34 +1911,33 @@ 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.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.Appl l as t -> - let b,_,_,_ = is_a_double_coercion t in - (* prerr_endline "CANDIDATO!!!!"; *) - let newt = - if b then - let ugraph = CicUniv.empty_ugraph in - let old_insert_coercions = !insert_coercions in - insert_coercions := false; - let newt, _, menv, _ = - 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; - if metasenv <> [] || menv = [] then - newt - else - (prerr_endline "PUO' SUCCEDERE!!!!!";t) - else - t - in - (match newt with - | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l) - | _ -> assert false) + | C.Appl l -> + let l = List.map (merge_coercions ctx) l in + let t = C.Appl l in + let b,_,_,_,_ = is_a_double_coercion t in + if b then + let ugraph = CicUniv.oblivion_ugraph in + let old_insert_coercions = !insert_coercions in + insert_coercions := false; + let newt, _, menv, _ = + try + type_of_aux' metasenv ctx t ugraph + with RefineFailure _ | Uncertain _ -> + t, t, [], ugraph + in + insert_coercions := old_insert_coercions; + if metasenv <> [] || menv = [] then + newt + else + (prerr_endline "PUO' SUCCEDERE!!!!!";t) + else + t | C.Var (uri,exp_named_subst) -> let exp_named_subst = List.map aux exp_named_subst in C.Var (uri, exp_named_subst) @@ -1560,6 +1983,31 @@ let pack_coercion metasenv ctx t = merge_coercions ctx t ;; +let pack_coercion_metasenv conjectures = + let module C = Cic in + List.map + (fun (i, ctx, ty) -> + let ctx = + List.fold_right + (fun item ctx -> + let item' = + match item with + Some (name, C.Decl t) -> + Some (name, C.Decl (pack_coercion conjectures ctx t)) + | Some (name, C.Def (t,None)) -> + Some (name,C.Def (pack_coercion conjectures ctx t,None)) + | Some (name, C.Def (t,Some ty)) -> + Some (name, C.Def (pack_coercion conjectures ctx t, + Some (pack_coercion conjectures ctx ty))) + | None -> None + in + item'::ctx + ) ctx [] + in + ((i,ctx,pack_coercion conjectures ctx ty)) + ) conjectures +;; + let pack_coercion_obj obj = let module C = Cic in match obj with @@ -1580,29 +2028,7 @@ let pack_coercion_obj obj = let ty = pack_coercion [] [] ty in C.Variable (name, body, ty, params, attrs) | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> - let conjectures = - List.map - (fun (i, ctx, ty) -> - let ctx = - List.fold_right - (fun item ctx -> - let item' = - match item with - Some (name, C.Decl t) -> - Some (name, C.Decl (pack_coercion conjectures ctx t)) - | Some (name, C.Def (t,None)) -> - Some (name,C.Def (pack_coercion conjectures ctx t,None)) - | Some (name, C.Def (t,Some ty)) -> - Some (name, C.Def (pack_coercion conjectures ctx t, - Some (pack_coercion conjectures ctx ty))) - | None -> None - in - item'::ctx - ) ctx [] - in - ((i,ctx,pack_coercion conjectures ctx ty)) - ) conjectures - in + let conjectures = pack_coercion_metasenv conjectures in let body = pack_coercion conjectures [] body in let ty = pack_coercion conjectures [] ty in C.CurrentProof (name, conjectures, body, ty, params, attrs) @@ -1648,3 +2074,6 @@ let type_of_aux' ?localization_tbl metasenv context term ugraph = let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj + +let _ = DoubleTypeInference.pack_coercion := pack_coercion;; +(* vim:set foldmethod=marker: *)