=
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 =
let coer =
CoercGraph.look_for_coercion metasenv subst context infty expty
| CoercGraph.SomeCoercion candidates ->
let uncertain = ref false in
let selected =
- HExtlib.list_findopt
+(* HExtlib.list_findopt *)
+ let posibilities =
+ HExtlib.filter_map
(fun (metasenv,last,c) ->
try
let subst,metasenv,ugraph =
| 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
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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
- 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
| _ -> assert false
in
let get_l_r_p n = function
- | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+ | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
| Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
HExtlib.split_nth n args
| _ -> assert false
List.map
(fun ty ->
List.fold_left
- (fun t p -> CS.subst ~avoid_beta_redexes:true p t)
+ (fun t p -> match t with
+ | Cic.Prod (_,_,t) ->
+ cs_subst p t
+ | _-> assert false)
ty left_p)
cl
in
(List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
| _ -> assert false
in
- let add_params uri tyno cty outty leftno i =
+ let add_params
+ metasenv subst context uri tyno cty outty leftno i
+ =
let mytl = function [] -> [] | _::tl -> tl in
- let rec aux outty par k = function
+ let rec aux context outty par k = function
| Cic.Prod (name, src, tgt) ->
Cic.Prod (name, src,
- aux (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
+ aux
+ (Some (name, Cic.Decl src) :: context)
+ (CS.lift 1 outty) (Cic.Rel k::par) (k+1) tgt)
| Cic.MutInd _ ->
let par = mytl par in
let k =
CR.head_beta_reduce ~delta:false
(Cic.Appl [outty;k])
| Cic.Appl (Cic.MutInd _::pl) ->
- let par = mytl par in
- let left_p,right_p = HExtlib.split_nth leftno pl in
+ let left_p,_ = HExtlib.split_nth leftno pl 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
CR.head_beta_reduce ~delta:false
(Cic.Appl (outty ::right_p @ [k]))
| _ -> assert false
in
- aux outty [] 1 cty
- in
- let rec add_params2 expty = function
- | Cic.Prod (name, src, tgt) ->
- Cic.Prod (name, src, add_params2 (CS.lift 1 expty) tgt)
- | Cic.MutInd _ | Cic.Appl (Cic.MutInd _::_) -> expty
- | _ -> assert false
+ aux context outty [] 1 cty
in
(* constructors types with left params already instantiated *)
let outty = CicMetaSubst.apply_subst subst outty in
in
let _,pl,subst,metasenv,ugraph =
List.fold_right2
- (fun cty pbo (i, acc, subst, metasenv, ugraph) ->
- (* Pi k_par, outty right_par (K_i left_par k_par)*)
- let infty_pbo = add_params uri tyno cty outty leftno i in
- (* Pi k_par, expty *)
- let expty_pbo = add_params2 expty cty in
+ (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
let (pbo, _), subst, metasenv, ugraph =
coerce_to_something_aux pbo infty_pbo expty_pbo
- subst metasenv context ugraph
+ s m context ugraph
in
(i-1, pbo::acc, subst, metasenv, ugraph))
cl pl (List.length pl, [], subst, metasenv, ugraph)
let t = Cic.MutCase(uri, tyno, new_outty, m, pl) in
(t, expty), subst, metasenv, ugraph
| Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
- let name_con = Cic.Name "name_con" in
+ let name_con =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst metasenv context Cic.Anonymous ~typ:src2
+ 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 =
(* 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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 bo)
+ | 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 ~avoid_beta_redexes:true rel1 (CS.lift_from 2 1 ty) in
+ 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 ("coerced: "^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst coerced context)(;
+ (coerced, expty), subst, metasenv, ugraph
| _ ->
coerce_atom_to_something t infty expty subst metasenv context ugraph
in
projects / helm.git / blobdiff