let module C2A = Cic2acic in
(* atomic terms are never lifted, according to my policy *)
function
- C.ARel (id,_,_,_) -> false
+ C.ARel (id,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with Not_found -> false)
| C.AVar (id,_,_) ->
(try
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
{ K.conclude_id = gen_id conclude_prefix seed;
K.conclude_aref = id;
K.conclude_method = "Exact";
- K.conclude_args = [K.Term t];
+ K.conclude_args = [K.Term (false, t)];
K.conclude_conclusion =
try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
with Not_found -> None
}
;;
-let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
+let infer_dependent ~headless context metasenv = function
+ | [] -> assert false
+ | [t] -> [false, t]
+ | he::tl as l ->
+ if headless then
+ List.map (function s -> false,s) l
+ else
+ try
+ let hety,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv context (Deannotate.deannotate_term he)
+ CicUniv.oblivion_ugraph
+ in
+ let fstorder t =
+ match CicReduction.whd context t with
+ | Cic.Prod _ -> false
+ | _ -> true
+ in
+ let rec dummify_last_tgt t =
+ match CicReduction.whd context t with
+ | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt)
+ | _ -> Cic.Implicit None
+ in
+ let rec aux ty = function
+ | [] -> []
+ | t::tl ->
+ match
+ FreshNamesGenerator.clean_dummy_dependent_types
+ (dummify_last_tgt ty)
+ with
+ | Cic.Prod (n,src,tgt) ->
+ (n <> Cic.Anonymous && fstorder src, t) ::
+ aux (CicSubstitution.subst
+ (Deannotate.deannotate_term t) tgt) tl
+ | _ -> List.map (fun s -> false,s) (t::tl)
+ in
+ (false, he) :: aux hety tl
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+;;
+
+let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
let module C = Cic in
let module K = Content in
- let rec aux =
+ let rec aux n =
function
[] -> [],[]
- | t::l1 ->
- let subproofs,args = aux l1 in
- if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+ | (dep, t)::l1 ->
+ let need_lifting =
+ test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in
+ let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in
+ if need_lifting then
let new_subproof =
acic2content
- seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+ seed context metasenv
+ ~name:("H" ^ string_of_int n) ~ids_to_inner_types
+ ~ids_to_inner_sorts t in
let new_arg =
K.Premise
{ K.premise_id = gen_id premise_prefix seed;
K.premise_binder = Some b;
K.premise_n = Some n
}
- else (K.Term t)
+ else (K.Term (dep,t))
| C.AConst(id,uri,[]) ->
let sort =
(try
K.lemma_name = UriManager.name_of_uri uri;
K.lemma_uri = UriManager.string_of_uri uri
}
- else (K.Term t)
+ else (K.Term (dep,t))
| C.AMutConstruct(id,uri,tyno,consno,[]) ->
let sort =
(try
string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
")"
}
- else (K.Term t)
- | _ -> (K.Term t)) in
+ else (K.Term (dep,t))
+ | _ -> (K.Term (dep,t))) in
subproofs,hd::args
in
- match (aux l) with
+ match (aux 1 (infer_dependent ~headless context metasenv l)) with
[p],args ->
[{p with K.proof_name = None}],
List.map
and
-build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
let module K = Content in
try
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
(let p =
- (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
+ (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
in
`Proof p;)
else
Prop. For debugging purposes this is tested again, possibly raising an
Not_a_proof exception *)
-and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
- let rec aux ?name t =
+and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
+ let rec aux ?name context t =
let module C = Cic in
let module K = Content in
let module C2A = Cic2acic in
| C.ASort (id,s) -> raise Not_a_proof
| C.AImplicit _ -> raise NotImplemented
| C.AProd (_,_,_,_) -> raise Not_a_proof
- | C.ACast (id,v,t) -> aux v
+ | C.ACast (id,v,t) -> aux context v
| C.ALambda (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = aux t in
+ let proof =
+ aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t
+ in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
match proof.K.proof_conclude.K.conclude_args with
}
in
generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ else
+ raise Not_a_proof
| C.ALetIn (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = aux t in
+ let proof = (* XXX TIPAMI!!! *)
+ aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t
+ in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
match proof.K.proof_conclude.K.conclude_args with
{ proof' with
K.proof_name = None;
K.proof_context =
- ((build_def_item seed id n s ids_to_inner_sorts
+ ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
::proof'.K.proof_context;
}
in
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ else
+ raise Not_a_proof
| C.AAppl (id,li) ->
(try coercion
- seed li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try rewrite
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try inductive
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try transitivity
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
let subproofs, args =
build_subproofs_and_args
- seed li ~ids_to_inner_types ~ids_to_inner_sorts in
+ seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in
(*
let args_to_lift =
List.filter (test_for_lifting ~ids_to_inner_types) li in
let pp =
let build_proof p (name,arity) =
let rec make_context_and_body c p n =
- if n = 0 then c,(aux p)
+ if n = 0 then c,(aux context p)
else
(match p with
Cic.ALambda(idl,vname,s1,t1) ->
let ce =
- build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
+ build_decl_item
+ seed idl vname s1 ~ids_to_inner_sorts in
make_context_and_body (ce::c) t1 (n-1)
| _ -> assert false) in
let context,body = make_context_and_body [] p arity in
List.map2 build_proof patterns name_and_arities in
let context,term =
(match
- build_subproofs_and_args
- seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
+ build_subproofs_and_args ~headless:true
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te]
with
l,[t] -> l,t
| _ -> assert false) in
K.conclude_method = "Case";
K.conclude_args =
(K.Aux (UriManager.string_of_uri uri))::
- (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+ (K.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp;
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
}
}
| C.AFix (id, no, funs) ->
+ let context' =
+ List.fold_left
+ (fun ctx (_,n,_,ty,_) ->
+ let ty = Deannotate.deannotate_term ty in
+ Some (Cic.Name n,Cic.Decl ty) :: ctx)
+ [] funs @ context
+ in
let proofs =
List.map
- (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+ (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in
let fun_name =
List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no
in
}
}
| C.ACoFix (id,no,funs) ->
+ let context' =
+ List.fold_left
+ (fun ctx (_,n,ty,_) ->
+ let ty = Deannotate.deannotate_term ty in
+ Some (Cic.Name n,Cic.Decl ty) :: ctx)
+ [] funs @ context
+ in
let proofs =
List.map
- (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
+ (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in
let jo =
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind = `CoRecursive;
in
let id = get_id t in
generate_conversion seed false id t1 ~ids_to_inner_types
-in aux ?name t
+in aux ?name context t
-and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
- let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
+and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+ let aux context ?name =
+ acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
let args_for_cases, other_args =
split no_constructors tail_args in
let subproofs,other_method_args =
- build_subproofs_and_args seed other_args
- ~ids_to_inner_types ~ids_to_inner_sorts in
+ build_subproofs_and_args ~headless:true seed context metasenv
+ other_args ~ids_to_inner_types ~ids_to_inner_sorts in
let method_args=
let rec build_method_args =
function
let hdarg =
if sortarg = `Prop then
let (co,bo) =
- let rec bc =
+ let rec bc context =
function
Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
+ let context' =
+ Some (n,Cic.Decl(Deannotate.deannotate_term s1))
+ ::context
+ in
let ce =
build_decl_item
seed idl n s1 ~ids_to_inner_sorts in
if (occur ind_uri s) then
( match t1 with
Cic.ALambda(id2,n2,s2,t2) ->
+ let context'' =
+ Some
+ (n2,Cic.Decl
+ (Deannotate.deannotate_term s2))
+ ::context'
+ in
let inductive_hyp =
`Hypothesis
{ K.dec_name = name_of n2;
K.dec_aref = id2;
K.dec_type = s2
} in
- let (context,body) = bc (t,t2) in
+ let (context,body) = bc context'' (t,t2) in
(ce::inductive_hyp::context,body)
| _ -> assert false)
else
(
- let (context,body) = bc (t,t1) in
+ let (context,body) = bc context' (t,t1) in
(ce::context,body))
- | _ , t -> ([],aux t) in
- bc (ty,arg) in
+ | _ , t -> ([],aux context t) in
+ bc context (ty,arg) in
K.ArgProof
{ bo with
K.proof_name = Some name;
K.proof_context = co;
};
- else (K.Term arg) in
+ else (K.Term (false,arg)) in
hdarg::(build_method_args (tlc,tla))
| _ -> assert false in
build_method_args (constructors1,args_for_cases) in
K.conclude_method = method_name;
K.conclude_args =
K.Aux (string_of_int no_constructors)
- ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
+ ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))))
::method_args@other_method_args;
K.conclude_conclusion =
try Some
}
| _ -> raise NotApplicable
-and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
match li with
| ((Cic.AConst _) as he)::tl
| ((Cic.AMutInd _) as he)::tl
| [t] -> t
| _::tl -> last tl
in
- acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
| _ -> raise NotApplicable
-and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
- let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
+and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+ let aux context ?name =
+ acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
let subproofs,arg =
(match
build_subproofs_and_args
- seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
+ seed context metasenv
+ ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
with
l,[p] -> l,p
| _,_ -> assert false) in
let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
with Not_found -> `Type (CicUniv.fresh())) in
if asort = `Prop then
- K.ArgProof (aux a)
- else K.Term a in
+ K.ArgProof (aux context a)
+ else K.Term (false,a) in
hd::(ma_aux (n-1) tl) in
(ma_aux 3 args) in
{ K.proof_name = name;
K.proof_conclude =
{ K.conclude_id = gen_id conclude_prefix seed;
K.conclude_aref = id;
- K.conclude_method = "Rewrite";
+ K.conclude_method =
+ if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+ || LibraryObjects.is_eq_ind_URI uri then
+ "RewriteLR"
+ else
+ "RewriteRL";
K.conclude_args =
- K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
+ K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
else raise NotApplicable
| _ -> raise NotApplicable
-and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+and transitivity
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
+=
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
K.conclude_aref = id;
K.conclude_method = "Eq_chain";
K.conclude_args =
- K.Term t1::
+ K.Term (false,t1)::
(transitivity_aux
- seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
- [K.Term t2]@
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @ [K.Term (false,t2)]@
(transitivity_aux
- seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
- [K.Term t3];
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ @ [K.Term (false,t3)];
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
}
| _ -> raise NotApplicable
-and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
+and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t =
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
| [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
| _ -> raise NotApplicable
in
- (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
- @[K.Term t2]
- @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ (transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @[K.Term (false,t2)]
+ @(transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
| _ -> [K.ArgProof
- (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
+ (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)]
;;
(map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
conjectures),
`Def (K.Const,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item
+ seed [] (Deannotate.deannotate_conjectures conjectures)
+ (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (_,_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Const,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (id,_,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
| C.AVariable (_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Var,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AVariable (id,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
projects / helm.git / blobdiff