X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=614848706f5110a6398937d9548a5d305038c8cc;hb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;hp=335296effff7b374a7a4379f3d56a86828bcfff6;hpb=c1f6f44f9acab34668041aa85c6d6fbf7e6f9d55;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 335296eff..614848706 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -251,7 +251,7 @@ let generate_exact seed t id name ~ids_to_inner_types = 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 = @@ -271,7 +271,7 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ 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 = @@ -405,27 +405,18 @@ build_def_item seed 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 - (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 @@ -671,6 +662,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists" else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd" + else if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd" else "ByInduction" in let prefix = String.sub uri_str 0 n in let ind_str = (prefix ^ ".ind") in @@ -687,9 +679,6 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let p,a = split (n-1) (List.tl l) in ((List.hd l::p),a) in let params_and_IP,tail_args = split (noparams+1) args in - if method_name = "Exists" then - (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args)); - prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args))); let constructors = (match inductive_types with [(_,_,_,l)] -> l @@ -707,7 +696,6 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = 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 @@ -727,8 +715,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = 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 @@ -743,7 +730,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = (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 @@ -767,7 +754,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = 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 @@ -836,30 +823,28 @@ let map_conjectures 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)