let module C2A = Cic2acic in
let module K = Content in
{ K.proof_name = name;
- K.proof_id = proof_prefix ^ id ;
+ K.proof_id = gen_id proof_prefix seed ;
K.proof_context = [] ;
K.proof_apply_context = [];
K.proof_conclude =
let module C = Cic in
let module K = Content in
{ K.proof_name = name;
- K.proof_id = proof_prefix ^ id ;
+ K.proof_id = gen_id proof_prefix seed ;
K.proof_context = [] ;
K.proof_apply_context = [];
K.proof_conclude =
let module K = Content in
try
let sort = Hashtbl.find ids_to_inner_sorts id in
- (match name_of n with
- Some "w" -> prerr_endline ("build_def: " ^ sort );
- | _ -> ());
if sort = "Prop" then
- (prerr_endline ("entro");
- let p =
+ (let p =
(acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
in
- (match p.K.proof_name with
- Some "w" -> prerr_endline ("TUTTO BENE:");
- | Some s -> prerr_endline ("mi chiamo " ^ s);
- | _ -> prerr_endline ("ho perso il nome"););
- prerr_endline ("esco"); `Proof p;)
+ `Proof p;)
else
- (prerr_endline ("siamo qui???");
`Definition
{ K.def_name = name_of n;
K.def_id = gen_id definition_prefix seed;
K.def_aref = id;
K.def_term = t
- })
+ }
with
Not_found -> assert false
let subproofs,other_method_args =
build_subproofs_and_args seed other_args
~ids_to_inner_types ~ids_to_inner_sorts in
- prerr_endline "****** end other *******"; flush stderr;
let method_args=
let rec build_method_args =
function
build_decl_item
seed idl n s1 ~ids_to_inner_sorts in
if (occur ind_uri s) then
- ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
- match t1 with
+ ( match t1 with
Cic.ALambda(id2,n2,s2,t2) ->
let inductive_hyp =
`Hypothesis
(ce::inductive_hyp::context,body)
| _ -> assert false)
else
- ( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
+ (
let (context,body) = bc (t,t1) in
(ce::context,body))
| _ , t -> ([],aux t) 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 (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
::method_args@other_method_args;
K.conclude_conclusion =
try Some
let context' =
List.map
(function
- (id,None) as item -> item
+ (id,None) -> None
| (id,Some (name,Cic.ADecl t)) ->
- id,
- Some
- (* We should call build_decl_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Declaration
- { K.dec_name = name_of name;
- K.dec_id = gen_id declaration_prefix seed;
- K.dec_inductive = false;
- K.dec_aref = get_id t;
- K.dec_type = t
- })
+ Some
+ (* We should call build_decl_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Declaration
+ { K.dec_name = name_of name;
+ K.dec_id = gen_id declaration_prefix seed;
+ K.dec_inductive = false;
+ K.dec_aref = get_id t;
+ K.dec_type = t
+ })
| (id,Some (name,Cic.ADef t)) ->
- id,
- Some
- (* We should call build_def_item, but we have not computed *)
- (* the inner-types ==> we always produce a declaration *)
- (`Definition
- { K.def_name = name_of name;
- K.def_id = gen_id definition_prefix seed;
- K.def_aref = get_id t;
- K.def_term = t
- })
+ Some
+ (* We should call build_def_item, but we have not computed *)
+ (* the inner-types ==> we always produce a declaration *)
+ (`Definition
+ { K.def_name = name_of name;
+ K.def_id = gen_id definition_prefix seed;
+ K.def_aref = get_id t;
+ K.def_term = t
+ })
) context
in
(id,n,context',ty)