let insert_coercions = ref true
let pack_coercions = ref true
-let debug_print = fun _ -> ();;
-(*let debug_print x = prerr_endline (Lazy.force x);;*)
+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"
allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
=
(* aux function to add coercions to funclass *)
- let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+ let rec fix_arity metasenv context subst he hetype eaten args_bo_and_ty ugraph =
(* {{{ body *)
let pristinemenv = metasenv in
let metasenv,hetype' =
let args, remainder =
HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
in
- let args = List.map fst args in
+ let args = List.map fst (eaten@args) in
let x =
if args <> [] then
match he with
match
HExtlib.list_findopt
(fun (metasenv,last,coerc) ->
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
+ debug_print (lazy ("Last " ^ CicMetaSubst.ppterm ~metasenv subst last));
+ debug_print (lazy ("x " ^ CicMetaSubst.ppterm ~metasenv subst x));
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. *)
try
let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
fix_arity
- metasenv context subst t tty remainder ugraph
+ metasenv context subst t tty [] remainder ugraph
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
with Uncertain _ | RefineFailure _ -> None
(* {{{ body *)
function
| [] -> newargs,subst,metasenv,he,hetype,ugraph
- | (hete, hety)::tl ->
+ | (hete, hety)::tl as rest ->
match (CicReduction.whd ~subst context hetype) with
| Cic.Prod (n,s,t) ->
let arg,subst,metasenv,ugraph =
let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
fix_arity
pristinemenv context subst he hetype
- (newargs@[hete,hety]@tl) ugraph
+ newargs rest ugraph
in
eat_prods_and_args metasenv
metasenv subst context pristinehe he hetype'
else
(* this (says CSC) is also useful to infer dependent types *)
try
- fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ 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 metasenv
| 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 =
(* HExtlib.list_findopt *)
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
+ 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 =
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));
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 =
(Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
| _ -> assert false (* not implemented yet *))
| _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
- (* move this stuff away *)
+ 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 ->
(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 leftno i
+ metasenv subst context uri tyno cty outty mty m leftno i
=
- let mytl = function [] -> [] | _::tl -> tl in
- let rec aux context outty par k = function
+ let rec aux context outty par k mty m = function
| Cic.Prod (name, src, tgt) ->
- Cic.Prod (name, src,
+ let t,k =
aux
(Some (name, Cic.Decl src) :: context)
- (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+ (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 par = mytl par in
let k =
let k = Cic.MutConstruct (uri,tyno,i,[]) in
if par <> [] then Cic.Appl (k::par) else k
in
- CR.head_beta_reduce ~delta:false
- (Cic.Appl [outty;k])
+ 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,_ = HExtlib.split_nth leftno pl in
+ 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)
| _ -> assert false
with CicTypeChecker.TypeCheckerFailure _ -> assert false
in
- CR.head_beta_reduce ~delta:false
- (Cic.Appl (outty ::right_p @ [k]))
+ 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 cty
+ 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 =
+ let right_p, mty =
try
match
CicTypeChecker.type_of_aux' ~subst metasenv context m
CicUniv.oblivion_ugraph
with
- | Cic.MutInd _,_ -> []
- | Cic.Appl (Cic.MutInd _::args),_ ->
- snd (HExtlib.split_nth leftno args)
+ | Cic.MutInd _ as mty,_ -> [], mty
+ | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+ snd (HExtlib.split_nth leftno args), mty
| _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _ ->
- let rec foo =
- function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
- in
- foo rno
+ 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, m, ugraph) ->
- (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
- let infty_pbo =
- add_params m s context uri tyno cty outty leftno i in
- let expty_pbo =
- add_params m s context uri tyno cty new_outty leftno i in
+ (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 m context ugraph
+ 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 t = Cic.MutCase(uri, tyno, new_outty, m, pl) 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 Cic.Anonymous ~typ:src2
+ ~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 *)
~metasenv subst coerced context));
(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
try