From 7fd0b9edc6be316b4ef43ca98a6b02f76dd1108e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Jul 2003 15:43:30 +0000 Subject: [PATCH] Unuseful id removed from hypothesis. --- helm/ocaml/cic_omdoc/cic2acic.ml | 6 +++ helm/ocaml/cic_omdoc/cic2content.ml | 42 +++++++++---------- helm/ocaml/cic_omdoc/content.ml | 1 - helm/ocaml/cic_omdoc/content.mli | 1 - helm/ocaml/cic_omdoc/content2cic.ml | 10 ++--- .../ocaml/cic_transformations/content2pres.ml | 10 ++--- 6 files changed, 36 insertions(+), 34 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index b8679dc62..c0e514d37 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -63,9 +63,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let module T = CicTypeChecker in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in +prerr_endline "*************** INIZIO DOUBLE TYPE INFERENCE ************"; let terms_to_types = D.double_type_of metasenv context t expectedty in +prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************"; let rec aux computeinnertypes father context idrefs tt = let fresh_id'' = fresh_id' father tt in (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) @@ -339,6 +341,7 @@ let acic_object_of_cic_object obj = C.AVariable ("mettereaposto",id,abo,aty, params) | C.CurrentProof (id,conjectures,bo,ty,params) -> +prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ; let conjectures' = List.map (function (i,canonical_context,term) -> @@ -354,6 +357,7 @@ let acic_object_of_cic_object obj = (i,canonical_context',term') ) conjectures in +prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ; let aconjectures = List.map (function (i,canonical_context,term) as conjecture -> @@ -400,8 +404,10 @@ let acic_object_of_cic_object obj = in (cid,i,(List.rev revacanonical_context),aterm) ) conjectures' in +prerr_endline "*********** INIZIO ETA FIXING PROVA **********"; let bo' = E.eta_fix conjectures' bo in let ty' = E.eta_fix conjectures' ty in +prerr_endline "*********** INIZIO CIC ==> ACIC PROVA **********"; let abo = acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 58ef34c87..0f23afb56 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -834,30 +834,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) diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml index c3c2295ca..6679cfabb 100644 --- a/helm/ocaml/cic_omdoc/content.ml +++ b/helm/ocaml/cic_omdoc/content.ml @@ -148,7 +148,6 @@ type 'term conjecture = id * int * 'term context * 'term and 'term context = 'term hypothesis list and 'term hypothesis = - id * ['term decl_context_element | ('term,'term proof) def_context_element ] option ;; diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli index a672cd83c..fea233da0 100644 --- a/helm/ocaml/cic_omdoc/content.mli +++ b/helm/ocaml/cic_omdoc/content.mli @@ -138,7 +138,6 @@ type 'term conjecture = id * int * 'term context * 'term and 'term context = 'term hypothesis list and 'term hypothesis = - id * ['term decl_context_element | ('term,'term proof) def_context_element ] option ;; diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 644f55920..29e81bffb 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -238,19 +238,19 @@ let cobj2obj deannotate (id,params,metasenv,obj) = let canonical_context' = List.map (function - _,None -> None - | _,Some (`Declaration d) - | _,Some (`Hypothesis d) -> + None -> None + | Some (`Declaration d) + | Some (`Hypothesis d) -> (match d with {K.dec_name = Some n ; K.dec_type = t} -> Some (Cic.Name n, Cic.Decl (deannotate t)) | _ -> assert false) - | _,Some (`Definition d) -> + | Some (`Definition d) -> (match d with {K.def_name = Some n ; K.def_term = t} -> Some (Cic.Name n, Cic.Def (deannotate t)) | _ -> assert false) - | _,Some (`Proof d) -> + | Some (`Proof d) -> (match d with {K.proof_name = Some n } -> Some (Cic.Name n, Cic.Def (proof2cic deannotate d)) diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 9a5ad74fd..cfa061bfb 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -810,13 +810,13 @@ let content2pres term2pres (id,params,metasenv,obj) = (P.Mrow [Some "helm", "xref", id] (List.map (function - (_,None) -> + None -> P.Mrow [] [ P.Mi [] "_" ; P.Mo [] ":?" ; P.Mi [] "_"] - | (_,Some (`Declaration d)) - | (_,Some (`Hypothesis d)) -> + | Some (`Declaration d) + | Some (`Hypothesis d) -> let { K.dec_name = dec_name ; K.dec_type = ty } = d @@ -828,7 +828,7 @@ let content2pres term2pres (id,params,metasenv,obj) = | Some n -> n) ; P.Mo [] ":" ; term2pres ty] - | (_,Some (`Definition d)) -> + | Some (`Definition d) -> let { K.def_name = def_name ; K.def_term = bo } = d @@ -840,7 +840,7 @@ let content2pres term2pres (id,params,metasenv,obj) = | Some n -> n) ; P.Mo [] ":=" ; term2pres bo] - | (_,Some (`Proof p)) -> + | Some (`Proof p) -> let proof_name = p.K.proof_name in P.Mrow [] [ P.Mi [] -- 2.39.2