From d9b059cc6ee460f5a0b0c606fd70241be49f0125 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Jul 2003 10:34:39 +0000 Subject: [PATCH] We do not compute inner-types for the metasenv ==> we handle it in a particular way, always generating `Declaration and `Definition (instead of `Hypothesis and `Proof when the sort is Prop). --- helm/ocaml/cic_omdoc/cic2content.ml | 126 ++++++++++++++++------------ 1 file changed, 73 insertions(+), 53 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 82f0005f5..7996f927a 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,37 +315,43 @@ 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 @@ -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,7 +502,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 } } ) @@ -521,7 +527,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.AFix (id, no, funs) -> @@ -552,7 +558,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.ACoFix (id,no,[(id1,n,ty,bo)]) -> @@ -576,7 +582,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.ACoFix (id,no,funs) -> @@ -607,7 +613,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 }; } in @@ -741,7 +747,7 @@ 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 @@ -791,7 +797,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 +807,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 +815,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) -- 2.39.2