| C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
| C.Cast (te,ty) -> (occur uri te)
| C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
- | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
+ | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t)
| C.Appl l ->
List.fold_left
(fun b a ->
| C.AProd (id,_,_,_) -> id
| C.ACast (id,_,_) -> id
| C.ALambda (id,_,_,_) -> id
- | C.ALetIn (id,_,_,_) -> id
+ | C.ALetIn (id,_,_,_,_) -> id
| C.AAppl (id,_) -> id
| C.AConst (id,_,_) -> id
| C.AMutInd (id,_,_,_) -> id
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
true;
with Not_found -> false)
- | C.ALetIn (id,_,_,_) ->
+ | C.ALetIn (id,_,_,_,_) ->
(try
ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
true;
}
;;
-let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
+let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types =
let module C2A = Cic2acic in
let module C = Cic in
let module K = Content in
(match inner_proof.K.proof_conclude.K.conclude_conclusion with
None -> None
| Some t ->
- if is_intro then Some (C.AProd ("gen"^id,n,s,t))
- else Some (C.ALetIn ("gen"^id,n,s,t)))
+ match ty with
+ None -> Some (C.AProd ("gen"^id,n,s,t))
+ | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t)))
};
}
;;
(n <> Cic.Anonymous && fstorder src, t) ::
aux (CicSubstitution.subst
(Deannotate.deannotate_term t) tgt) tl
- | _ -> assert false
+ | _ -> List.map (fun s -> false,s) (t::tl)
in
(false, he) :: aux hety tl
with CicTypeChecker.TypeCheckerFailure _ -> assert false
and
-build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types =
let module K = Content in
try
let sort = Hashtbl.find ids_to_inner_sorts id in
{ K.def_name = name_of n;
K.def_id = gen_id definition_prefix seed;
K.def_aref = id;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
}
with
Not_found -> assert false
proof'.K.proof_context
}
in
- generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
+ generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types
else
raise Not_a_proof
- | C.ALetIn (id,n,s,t) ->
+ | C.ALetIn (id,n,s,ty,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = (* XXX TIPAMI!!! *)
- aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t
+ let proof =
+ aux
+ ((Some (n,
+ Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t
in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
{ proof' with
K.proof_name = None;
K.proof_context =
- ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
+ ((build_def_item seed context metasenv (get_id s) n s ty 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
+ generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types
else
raise Not_a_proof
| C.AAppl (id,li) ->
K.dec_aref = get_id t;
K.dec_type = t
})
- | (id,Some (name,Cic.ADef t)) ->
+ | (id,Some (name,Cic.ADef (t,ty))) ->
Some
(* We should call build_def_item, but we have not computed *)
(* the inner-types ==> we always produce a declaration *)
{ K.def_name = name_of name;
K.def_id = gen_id definition_prefix seed;
K.def_aref = get_id t;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
})
) context
in
K.dec_aref = get_id t;
K.dec_type = t
})
- | (id,Some (name,Cic.ADef t)) ->
+ | (id,Some (name,Cic.ADef (t,ty))) ->
Some
(* We should call build_def_item, but we have not computed *)
(* the inner-types ==> we always produce a declaration *)
{ K.def_name = name_of name;
K.def_id = id;
K.def_aref = get_id t;
- K.def_term = t
+ K.def_term = t;
+ K.def_type = ty
})
) context
in
`Def (K.Const,ty,
build_def_item
seed [] (Deannotate.deannotate_conjectures conjectures)
- (get_id bo) (C.Name n) bo
+ (get_id bo) (C.Name n) bo ty
~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 ty
~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 ty
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AVariable (id,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,