generated.
there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.
code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.
potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.
=
let module CS = CicSubstitution in
let module CR = CicReduction in
=
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
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 =
| CoercGraph.SomeCoercion candidates ->
let uncertain = ref false in
let selected =
+(* HExtlib.list_findopt *)
+ let posibilities =
+ HExtlib.filter_map
(fun (metasenv,last,c) ->
try
let subst,metasenv,ugraph =
(fun (metasenv,last,c) ->
try
let subst,metasenv,ugraph =
| Uncertain _ -> uncertain := true; None
| RefineFailure _ -> None)
candidates
| 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
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
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
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
| _ -> 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
| Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
HExtlib.split_nth n args
| _ -> assert false
List.map
(fun ty ->
List.fold_left
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)
(List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
| _ -> assert false
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 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,
| 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 =
| Cic.MutInd _ ->
let par = mytl par in
let k =
CR.head_beta_reduce ~delta:false
(Cic.Appl [outty;k])
| Cic.Appl (Cic.MutInd _::pl) ->
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 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
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
(* constructors types with left params already instantiated *)
let outty = CicMetaSubst.apply_subst subst outty in
in
let _,pl,subst,metasenv,ugraph =
List.fold_right2
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
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
(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 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 =
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
(* 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 *)
| _ -> 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
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
| _ ->
coerce_atom_to_something t infty expty subst metasenv context ugraph
in
theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
in
aux
: nat → ∃n. 1 ≤ n);
in
aux
: nat → ∃n. 1 ≤ n);
-[ cases (aux name_con); simplify; ] autobatch;
+[ cases (aux n1); simplify; ] autobatch;
qed.
inductive NN (A:Type) : nat -> Type ≝
qed.
inductive NN (A:Type) : nat -> Type ≝
theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
intros 1;
theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
intros 1;
-(* MANCA UN LIFT forse NEL FIX *)
-apply (
let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
match n in NN return λx.λm:NN A x.NN A (S x) with
[ NO ⇒ NS A ? (NO A)
let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
match n in NN return λx.λm:NN A x.NN A (S x) with
[ NO ⇒ NS A ? (NO A)
-: ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
-[ cases (aux name_con); simplify; ] autobatch;
+: ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m); [3: apply xxx];
+unfold PN in aux ⊢ %; [cases (aux n2 n3)] autobatch
qed.
(* guarded troppo debole
qed.
(* guarded troppo debole