X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=12b806162b45abb816a90f3e7d9bca0f7225bc4f;hb=e23bc37c0a5e552395e499e7b8cee8d610b8e4f4;hp=82f0005f5eaf08af13187c769ba2323da61205e0;hpb=9e781c8957ff049e7bba65e1d611e5f007b02fb5;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 82f0005f5..12b806162 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -114,49 +114,49 @@ let test_for_lifting ~ids_to_inner_types = (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.ALambda (id,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.ALetIn (id,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.AAppl (id,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.AConst (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.AMutInd (id,_,_,_) -> false | C.AMutConstruct (id,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) (* oppure: false *) | C.AMutCase (id,_,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.AFix (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) | C.ACoFix (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; - with notfound -> false) + with Not_found -> false) ;; let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = @@ -184,7 +184,7 @@ let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = C.ARel (idr,idref,n,b) -> let sort = (try Hashtbl.find ids_to_inner_sorts idr - with notfound -> "Type") in + with Not_found -> "Type") in if sort ="Prop" then K.Premise { K.premise_id = gen_id seed; @@ -282,7 +282,7 @@ let generate_exact seed t id name ~ids_to_inner_types = K.conclude_args = [K.Term t]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None }; } ;; @@ -303,7 +303,7 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> + with Not_found -> (match inner_proof.K.proof_conclude.K.conclude_conclusion with None -> None | Some t -> @@ -315,44 +315,50 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ let build_decl_item seed id n s ~ids_to_inner_sorts = let module K = Content in - let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in - if sort = "Prop" then - `Hypothesis - { K.dec_name = name_of n; - K.dec_id = gen_id seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } - else - `Declaration - { K.dec_name = name_of n; - K.dec_id = gen_id seed; - K.dec_inductive = false; - K.dec_aref = id; - K.dec_type = s - } + try + let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in + if sort = "Prop" then + `Hypothesis + { K.dec_name = name_of n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } + else + `Declaration + { K.dec_name = name_of n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s + } + with + Not_found -> assert false ;; let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in - let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then - `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) - else - `Definition - { K.def_name = name_of n; - K.def_id = gen_id seed; - K.def_aref = id; - K.def_term = t - } + try + let sort = Hashtbl.find ids_to_inner_sorts id in + if sort = "Prop" then + `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + else + `Definition + { K.def_name = name_of n; + K.def_id = gen_id seed; + K.def_aref = id; + K.def_term = t + } + with + Not_found -> assert false (* the following function must be called with an object of sort Prop. For debugging purposes this is tested again, possibly raising an Not_a_proof exception *) -and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = - let rec aux ?(name = None) t = +and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = + let rec aux ?name t = let module C = Cic in let module K = Content in let module C2A = Cic2acic in @@ -380,7 +386,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = | C.ALambda (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = "Prop" then - let proof = aux t ~name:None in + let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with @@ -430,7 +436,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let subproofs = match args_to_lift with [_] -> List.map aux args_to_lift - | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + | _ -> List.map (aux ~name:"H") args_to_lift in let args = build_args seed li subproofs ~ids_to_inner_types ~ids_to_inner_sorts in { K.proof_name = name; @@ -445,7 +451,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None }; }) | C.AConst (id,uri,exp_named_subst) as t -> @@ -464,7 +470,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in (match (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized - with notfound -> None) + with Not_found -> None) with Some tety -> (* we must lift up the argument *) let p = (aux te) in @@ -480,7 +486,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None } } | None -> @@ -496,40 +502,19 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None } } ) - | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Proof proof]; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Exact"; - K.conclude_args = - [ K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = proof.K.proof_id; - K.premise_binder = proof.K.proof_name; - K.premise_n = Some 1; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } | C.AFix (id, no, funs) -> let proofs = - List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in + List.map + (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in + let decreasing_args = + List.map (function (_,_,n,_,_) -> n) funs in let jo = { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; + K.joint_kind = `Recursive decreasing_args; K.joint_defs = proofs } in @@ -552,39 +537,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None - } - } - | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { K.proof_name = name; - K.proof_id = gen_id seed; - K.proof_context = [`Proof proof]; - K.proof_apply_context = []; - K.proof_conclude = - { K.conclude_id = gen_id seed; - K.conclude_aref = id; - K.conclude_method = "Exact"; - K.conclude_args = - [ K.Premise - { K.premise_id = gen_id seed; - K.premise_xref = proof.K.proof_id; - K.premise_binder = proof.K.proof_name; - K.premise_n = Some 1; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None } } | C.ACoFix (id,no,funs) -> let proofs = - List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in + List.map + (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in let jo = { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; + K.joint_kind = `CoRecursive; K.joint_defs = proofs } in @@ -607,16 +569,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None }; } in let id = get_id t in generate_conversion seed false id t1 ~ids_to_inner_types -in aux ~name:name t +in aux ?name t and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = - let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in + let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -663,7 +625,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = let subproofs = match args_to_lift with [_] -> List.map aux args_to_lift - | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + | _ -> List.map (aux ~name:"H") args_to_lift in prerr_endline "****** end subproofs *******"; flush stderr; let other_method_args = build_args seed other_args subproofs @@ -715,7 +677,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = ( 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 ~name:None) in + | _ , t -> ([],aux t) in bc (ty,arg) in K.ArgProof { bo with @@ -741,13 +703,13 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None } } | _ -> raise NotApplicable and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = - let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in + let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -791,7 +753,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with notfound -> None + with Not_found -> None } } else raise NotApplicable @@ -801,6 +763,7 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = let map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) = + let module K = Content in let context' = List.map (function @@ -808,13 +771,26 @@ let map_conjectures | (id,Some (name,Cic.ADecl t)) -> id, Some - (build_decl_item seed (get_id t) name t - ~ids_to_inner_sorts) + (* 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 seed; + K.dec_inductive = false; + K.dec_aref = get_id t; + K.dec_type = t + }) | (id,Some (name,Cic.ADef t)) -> id, Some - (build_def_item seed (get_id t) name t - ~ids_to_inner_sorts ~ids_to_inner_types) + (* 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 seed; + K.def_aref = get_id t; + K.def_term = t + }) ) context in (id,n,context',ty)