exception AssertFailure of string Lazy.t;;
let insert_coercions = ref true
+let pack_coercions = ref true
-let debug_print = fun _ -> ()
+let debug_print = fun _ -> ();;
+(*let debug_print x = prerr_endline (Lazy.force x);;*)
+
+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"
Cic.CicHash.find localization_tbl t
with Not_found ->
prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
- assert false
+ raise exn'
in
raise (HExtlib.Localized (loc,exn'))
let exp_impl metasenv subst context =
function
| Some `Type ->
- 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)
+ 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)
| Some `Closed ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+ metasenv', Cic.Meta (idx, [])
| None ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
| _ -> assert false
;;
+let is_a_double_coercion t =
+ let last_of l =
+ let rec aux acc = function
+ | x::[] -> acc,x
+ | x::tl -> aux (acc@[x]) tl
+ | [] -> assert false
+ in
+ 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 ->
+ (match last_of tl with
+ | 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])])
+ | _ -> dummyres)
+ | _ -> dummyres
+
+let more_args_than_expected
+ localization_tbl subst he context hetype' tlbody_and_type exn
+=
+ let msg =
+ 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")
+ 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
let module R = CicReduction in
| C.CurrentProof (_,_,_,ty,_,_) -> ty,u
| _ ->
raise
- (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
+ (RefineFailure
+ (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
and type_of_variable uri ugraph =
let module C = Cic in
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
+ let try_coercion t subst metasenv context ugraph coercion_tgt c =
+ let coerced = Cic.Appl[c;t] 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
+ in
+ Some (newt, tty, subst, metasenv, ugraph)
+ with
+ | RefineFailure _ | Uncertain _ -> None
+ in
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
t, cast, subst, metasenv, ugraph
| term ->
let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
+ let boh =
+ CoercGraph.look_for_coercion coercion_src coercion_tgt
+ in
(match boh with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
" 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, tty, subst, metasenv, ugraph =
- avoid_double_coercion
- subst metasenv ugraph
- (Cic.Appl[c;t]) coercion_tgt
- in
- newt, tty, subst, metasenv, ugraph)
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (try_coercion
+ t subst metasenv context ugraph coercion_tgt)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None ->
+ 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"))))
in
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
| C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
| coercion_src ->
let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
+ let boh =
+ CoercGraph.look_for_coercion coercion_src coercion_tgt
+ in
match boh with
- | CoercGraph.SomeCoercion c ->
- let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion
- subst' metasenv' ugraph1
- (Cic.Appl[c;s']) coercion_tgt
- in
- newt, tty, subst', metasenv', ugraph1
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
enrich localization_tbl s'
" is not a type since it has type " ^
CicMetaSubst.ppterm_in_context
subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (try_coercion
+ s' subst' metasenv' context ugraph1 coercion_tgt)
+ candidates
+ in
+ match selected with
+ | Some x -> x
+ | None ->
+ 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")))
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
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
- hetype tlbody_and_type ugraph2
+ he' hetype tlbody_and_type ugraph2
in
- avoid_double_coercion
- 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 =
| None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
| Some candidate ->
let subst,metasenv,ugraph =
+ try
fo_unif_subst subst context metasenv
candidate outtype ugraph5
+ with
+ exn -> assert false(* unification against a metavariable *)
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
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
- outtypety tlbody_and_type ugraph4
+ outtype outtypety tlbody_and_type ugraph4
in
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(C.Appl ((outtype :: right_args) @ [term'])) ugraph4
in
let (subst,metasenv,ugraph6) =
- List.fold_left
+ List.fold_left2
(fun (subst,metasenv,ugraph)
- (constructor_args_no,context,instance,args) ->
+ p (constructor_args_no,context,instance,args)
+ ->
let instance' =
let appl =
let outtype' =
in
CicReduction.whd ~subst context appl
in
- fo_unif_subst subst context metasenv
- instance instance' ugraph)
- (subst,metasenv,ugraph5) outtypeinstances
+ try
+ fo_unif_subst subst context metasenv instance instance'
+ ugraph
+ with
+ exn ->
+ enrich localization_tbl p exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst p
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst instance'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst instance
+ context)))
+ (subst,metasenv,ugraph5) pl' outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph
- in
+ type_of_aux subst metasenv context' bo ugraph in
+ let expected_ty = CicSubstitution.lift len ty in
let subst',metasenv',ugraph' =
+ try
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ty_of_bo expected_ty ugraph1
+ with
+ exn ->
+ enrich localization_tbl bo exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_ty
+ context))
in
fl @ [bo'] , subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph
- in
+ type_of_aux subst metasenv context' bo ugraph in
+ let expected_ty = CicSubstitution.lift len ty in
let subst',metasenv',ugraph' =
+ try
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ty_of_bo expected_ty ugraph1
+ with
+ exn ->
+ enrich localization_tbl bo exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_ty
+ context))
in
fl @ [bo'],subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
relocalize localization_tbl t t';
res
- and avoid_double_coercion subst metasenv ugraph t ty =
- match t with
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- 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
- with
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
- | _ -> assert false) (* the composite coercion must exist *)
- | _ -> t, ty, subst, metasenv, ugraph
-
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
| (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 *)
+ * break 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 *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv,ugraph1) =
+ try
fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2'' ugraph
+ with _ -> assert false (* unification against a metavariable *)
in
t2'',subst,metasenv,ugraph1
| _,_ ->
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2''))))
+ and avoid_double_coercion context subst metasenv ugraph t ty =
+ 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
+ with
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (function
+ | 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));
+ (try
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt 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
+ 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;
+ 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
+ (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 hetype tlbody_and_type ugraph
+ allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
=
- 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
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv,ugraph1) =
+ (* aux function to add coercions to funclass *)
+ let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+ (* {{{ body *)
+ let pristinemenv = metasenv in
+ let metasenv,hetype' =
+ mk_prod_of_metas metasenv context subst args_bo_and_ty
+ in
try
- fo_unif_subst subst context metasenv hetype hetype' ugraph
- with exn ->
- 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)));
- raise exn
-
+ 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 s | Uncertain s as exn
+ when allow_coercions && !insert_coercions ->
+ (* {{{ we search a coercion of the head (saturated) to funclass *)
+ let metasenv = pristinemenv in
+ debug_print (lazy
+ ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
+ " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype'
+ (* ^ " cause: " ^ Lazy.force s *)));
+ let how_many_args_are_needed =
+ let rec aux n = function
+ | Cic.Prod(_,_,t) -> aux (n+1) t
+ | _ -> n
+ in
+ aux 0 (CicMetaSubst.apply_subst subst hetype)
+ in
+ let args, remainder =
+ HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
+ in
+ let args = List.map fst args in
+ let x =
+ if args <> [] then
+ match he with
+ | Cic.Appl l -> Cic.Appl (l@args)
+ | _ -> Cic.Appl (he::args)
+ else
+ he
+ in
+ let x,xty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context 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
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotMetaClosed
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ match
+ HExtlib.list_findopt
+ (fun coerc ->
+ let t = Cic.Appl [coerc;x] in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+ 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
+ in
+ try
+ let metasenv, hetype' =
+ mk_prod_of_metas metasenv context subst remainder
+ in
+ debug_print (lazy
+ (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
+ CicMetaSubst.ppterm subst hetype'));
+ let subst,metasenv,ugraph =
+ fo_unif_subst_eat_prods
+ subst context metasenv tty hetype' ugraph
+ in
+ debug_print (lazy " success!");
+ Some (subst,metasenv,ugraph,tty,t,remainder)
+ with
+ | Uncertain _ | RefineFailure _
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ try
+ let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
+ fix_arity
+ metasenv context subst t tty remainder ugraph
+ in
+ Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
+ with Uncertain _ | RefineFailure _ -> None
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ with
+ | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ | None ->
+ more_args_than_expected localization_tbl
+ subst he context hetype args_bo_and_ty exn
+ (* }}} end coercion to funclass stuff *)
+ (* }}} end fix_arity *)
in
- let rec eat_prods metasenv subst context hetype ugraph =
+ (* aux function to process the type of the head and the args in parallel *)
+ let rec eat_prods_and_args
+ pristinemenv metasenv subst context pristinehe he hetype ugraph newargs
+ =
+ (* {{{ body *)
function
- | [] -> [],metasenv,subst,hetype,ugraph
+ | [] -> newargs,subst,metasenv,he,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
- 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 ->
- let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion
- subst metasenv ugraph
- (Cic.Appl[c;hete]) tgt_carr in
- try
- let newty,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- newt, subst, metasenv, ugraph
- with 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)
- | exn ->
+ match (CicReduction.whd ~subst context hetype) with
+ | Cic.Prod (n,s,t) ->
+ let arg,subst,metasenv,ugraph1 =
+ try
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst_eat_prods2
+ subst context metasenv hety s ugraph
+ in
+ (hete,hety),subst,metasenv,ugraph1
+ (* {{{ we search a coercion from hety to s if fails *)
+ with RefineFailure _ | Uncertain _ as exn
+ when allow_coercions && !insert_coercions ->
+ let coer, tgt_carr =
+ let carr t subst context =
+ CicReduction.whd ~delta:false
+ 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
+ in
+ (match coer with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
enrich localization_tbl hete
- ~f:(fun _ ->
+ (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*)))) exn
- in
- let coerced_args,metasenv',subst',t',ugraph2 =
- eat_prods metasenv subst context
- (CicSubstitution.subst arg t) ugraph1 tl
- in
- arg::coerced_args,metasenv',subst',t',ugraph2
- | _ -> assert false
- )
+ (* "\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 candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ try
+ let t = Cic.Appl[c;hete] in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ t ugraph
+ in
+ let newt, newty, 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
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ (match selected with
+ | Some x -> x
+ | None ->
+ 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: " ^ Printexc.to_string exn))) exn
+ (* }}} end coercion stuff *)
+ in
+ eat_prods_and_args pristinemenv metasenv subst context pristinehe he
+ (CicSubstitution.subst (fst arg) t)
+ ugraph1 (newargs@[arg]) tl
+ | _ ->
+ try
+ let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+ fix_arity
+ pristinemenv context subst he hetype
+ (newargs@[hete,hety]@tl) ugraph
+ in
+ eat_prods_and_args metasenv
+ metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+ 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
+ (* 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 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 *)
+ 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,metasenv,subst,t,ugraph2 =
- eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
+ let coerced_args,subst,metasenv,he,t,ugraph =
+ eat_prods_and_args
+ metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
in
- coerced_args,t,subst,metasenv,ugraph2
+ he,(List.map fst coerced_args),t,subst,metasenv,ugraph
in
(* eat prods ends here! *)
(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
are_all_occurrences_positive metasenv ugraph uri tys paramsno
in
Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+;;
+
+(* sara' piu' veloce che raffinare da zero? mah.... *)
+let pack_coercion metasenv ctx t =
+ let module C = Cic in
+ let rec merge_coercions ctx =
+ let aux = (fun (u,t) -> u,merge_coercions ctx t) in
+ function
+ | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
+ | C.Meta (n,subst) ->
+ let subst' =
+ List.map
+ (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
+ in
+ C.Meta (n,subst')
+ | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
+ | C.Prod (name,so,dest) ->
+ let ctx' = (Some (name,C.Decl so))::ctx in
+ C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | 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 ctx' = Some (name,(C.Def (so,None)))::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
+ let t = C.Appl l in
+ let b,_,_,_,_ = is_a_double_coercion t in
+ (* prerr_endline "CANDIDATO!!!!"; *)
+ 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
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Var (uri, exp_named_subst)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Const (uri, exp_named_subst)
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutInd (uri,tyno,exp_named_subst)
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst)
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ let pl = List.map (merge_coercions ctx) pl in
+ C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
+ | C.Fix (fno, fl) ->
+ let ctx' =
+ List.fold_left
+ (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,idx,ty,bo) ->
+ (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
+ fl
+ in
+ C.Fix (fno, fl)
+ | C.CoFix (fno, fl) ->
+ let ctx' =
+ List.fold_left
+ (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, merge_coercions ctx ty, merge_coercions ctx' bo))
+ fl
+ in
+ C.CoFix (fno, fl)
+ in
+ merge_coercions ctx t
+;;
+
+let pack_coercion_obj obj =
+ let module C = Cic in
+ match obj with
+ | C.Constant (id, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] [] body)
+ in
+ let ty = pack_coercion [] [] ty in
+ C.Constant (id, body, ty, params, attrs)
+ | C.Variable (name, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] [] body)
+ in
+ 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 body = pack_coercion conjectures [] body in
+ let ty = pack_coercion conjectures [] ty in
+ C.CurrentProof (name, conjectures, body, ty, params, attrs)
+ | C.InductiveDefinition (indtys, params, leftno, attrs) ->
+ let indtys =
+ List.map
+ (fun (name, ind, arity, cl) ->
+ let arity = pack_coercion [] [] arity in
+ let cl =
+ List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
+ in
+ (name, ind, arity, cl))
+ indtys
+ in
+ C.InductiveDefinition (indtys, params, leftno, attrs)
+;;
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
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: *)