allow_coercions localization_tbl t infty expty subst metasenv context ugraph
=
let module CS = CicSubstitution in
+ let module CR = CicReduction in
let coerce_atom_to_something t infty expty subst metasenv context ugraph =
let coer =
CoercGraph.look_for_coercion metasenv subst context infty expty
let newt, newty, subst, metasenv, ugraph =
avoid_double_coercion context subst metasenv ugraph newt expty
in
- let subst,metasenv,ugraph1 =
+ let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv newhety expty ugraph in
Some ((newt,newty), subst, metasenv, ugraph)
with
let context_bo =
Some (Cic.Name name,Cic.Decl expty)::context in
let (rel1, _), subst, metasenv, ugraph =
- coerce_to_something_aux (Cic.Rel 1) expty infty subst
+ 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,_), subst, metasenv, ugraph =
- coerce_to_something_aux bo infty expty subst
+ 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 *)
- )
+ | _ -> assert false (* not implemented yet *))
+ | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
+ (* move this stuff away *)
+ 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
+ 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 -> CS.subst ~avoid_beta_redexes:true p t)
+ 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 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
+ 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 add_params uri tyno cty outty leftno i =
+ let mytl = function [] -> [] | _::tl -> tl in
+ let rec aux 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)
+ | 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.Appl (Cic.MutInd _::pl) ->
+ let par = mytl par in
+ let left_p,right_p = HExtlib.split_nth leftno pl in
+ let k =
+ let k = Cic.MutConstruct (uri,tyno,i,[]) in
+ Cic.Appl (k::left_p@par)
+ 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
+ in
+ (* 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 =
+ 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)
+ | _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ ->
+ let rec foo =
+ function 0 -> [] | n -> Cic.Implicit None :: foo (n-1)
+ in
+ foo rno
+ in
+ let new_outty =
+ keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+ 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
+ let (pbo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux pbo infty_pbo expty_pbo
+ subst metasenv context ugraph
+ in
+ (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
+ (t, expty), subst, metasenv, ugraph
| Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
let name_con = Cic.Name "name_con" in
let context_src2 = (Some (name_con, Cic.Decl src2) :: context) 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)
+ | Cic.Lambda (n,_,bo) -> n, CS.subst ~avoid_beta_redexes:true 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 ty = CS.subst ~avoid_beta_redexes:true 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
projects / helm.git / commitdiff