| 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)))
};
}
;;
if sort = `Prop then
let inductive_types =
(let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
in
match o with
| Cic.InductiveDefinition (l,_,_,_) -> l
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) ->
(try coercion
- seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try rewrite
seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
else raise Not_a_proof
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let inductive_types,noparams =
- (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
let ind_str = (prefix ^ ".ind") in
let ind_uri = UriManager.uri_of_string ind_str in
let inductive_types,noparams =
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
match o with
| Cic.InductiveDefinition (l,_,n,_) -> (l,n)
| _ -> assert false
}
| _ -> raise NotApplicable
-and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts =
match li with
| ((Cic.AConst _) as he)::tl
| ((Cic.AMutInd _) as he)::tl
| ((Cic.AMutConstruct _) as he)::tl when
- CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
- !hide_coercions ->
- let rec last =
- function
- [] -> assert false
- | [t] -> t
- | _::tl -> last tl
+ (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+ && !hide_coercions ->
+ let cpos,sats =
+ match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> assert false
+ | Some (_,_,_,sats,cpos) -> cpos, sats
in
- acic2content
- seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ let x = List.nth tl cpos in
+ let _,rest =
+ try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[]
+ in
+ if rest = [] then
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ x
+ else
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ (Cic.AAppl (id,x::rest))
| _ -> raise NotApplicable
and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
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,
projects / helm.git / blobdiff