From 43f61eedd2a1f499166de33a98af00b767dcc117 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 11:05:12 +0000 Subject: [PATCH] Cic2content split into Content and Cic2content. --- helm/gTopLevel/content2cic.ml | 8 +- helm/gTopLevel/content2cic.mli | 9 +- helm/ocaml/cic_transformations/.depend | 24 +- helm/ocaml/cic_transformations/Makefile | 10 +- helm/ocaml/cic_transformations/cic2content.ml | 662 +++++++----------- .../ocaml/cic_transformations/cic2content.mli | 128 +--- helm/ocaml/cic_transformations/content.ml | 159 +++++ helm/ocaml/cic_transformations/content.mli | 150 ++++ .../ocaml/cic_transformations/content2pres.ml | 20 +- .../cic_transformations/content2pres.mli | 2 +- helm/ocaml/cic_transformations/contentPp.ml | 10 +- helm/ocaml/cic_transformations/contentPp.mli | 2 +- 12 files changed, 621 insertions(+), 563 deletions(-) create mode 100644 helm/ocaml/cic_transformations/content.ml create mode 100644 helm/ocaml/cic_transformations/content.mli diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml index a4f8cd1ae..e8a95fc89 100644 --- a/helm/gTopLevel/content2cic.ml +++ b/helm/gTopLevel/content2cic.ml @@ -37,7 +37,7 @@ exception TO_DO;; let proof2cic term2cic p = let rec proof2cic premise_env p = let module C = Cic in - let module Con = Cic2content in + let module Con = Content in let rec extend_premise_env current_env = function [] -> current_env @@ -53,7 +53,7 @@ let proof2cic term2cic p = and ce2cic premise_env ce target = let module C = Cic in - let module Con = Cic2content in + let module Con = Content in match ce with `Declaration d -> (match d.Con.dec_name with @@ -84,7 +84,7 @@ let proof2cic term2cic p = and conclude2cic premise_env conclude = let module C = Cic in - let module Con = Cic2content in + let module Con = Content in if conclude.Con.conclude_method = "TD_Conversion" then (match conclude.Con.conclude_args with [Con.ArgProof p] -> proof2cic [] p (* empty! *) @@ -133,7 +133,7 @@ let proof2cic term2cic p = and arg2cic premise_env = let module C = Cic in - let module Con = Cic2content in + let module Con = Content in function Con.Aux n -> prerr_endline "8"; assert false | Con.Premise prem -> diff --git a/helm/gTopLevel/content2cic.mli b/helm/gTopLevel/content2cic.mli index 75f14dd7b..74d530182 100644 --- a/helm/gTopLevel/content2cic.mli +++ b/helm/gTopLevel/content2cic.mli @@ -34,11 +34,4 @@ val proof2cic : (Cic.annterm -> Cic.term) -> - Cic.annterm Cic2content.proof -> Cic.term - - - - - - - + Cic.annterm Content.proof -> Cic.term diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 11e89e6cb..8dee5ae2b 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,30 +1,32 @@ cic2Xml.cmi: cic2acic.cmi -cic2content.cmi: cic2acic.cmi -contentPp.cmi: cic2content.cmi +cic2content.cmi: cic2acic.cmi content.cmi +contentPp.cmi: content.cmi cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi -content2pres.cmi: cic2content.cmi mpresentation.cmi +content2pres.cmi: content.cmi mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi applyStylesheets.cmi: cic2acic.cmi doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +content.cmo: content.cmi +content.cmx: content.cmi cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi -cic2content.cmo: cic2acic.cmi cic2content.cmi -cic2content.cmx: cic2acic.cmx cic2content.cmi +cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi +cic2content.cmx: cic2acic.cmx content.cmx cic2content.cmi content_expressions.cmo: cic2acic.cmi content_expressions.cmi content_expressions.cmx: cic2acic.cmx content_expressions.cmi -contentPp.cmo: cic2content.cmi contentPp.cmi -contentPp.cmx: cic2content.cmx contentPp.cmi +contentPp.cmo: content.cmi contentPp.cmi +contentPp.cmx: content.cmx contentPp.cmi mpresentation.cmo: mpresentation.cmi mpresentation.cmx: mpresentation.cmi cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi -content2pres.cmo: cexpr2pres.cmi cic2content.cmi mpresentation.cmi \ - content2pres.cmi -content2pres.cmx: cexpr2pres.cmx cic2content.cmx mpresentation.cmx \ - content2pres.cmi +content2pres.cmo: cexpr2pres.cmi content.cmi content_expressions.cmi \ + mpresentation.cmi content2pres.cmi +content2pres.cmx: cexpr2pres.cmx content.cmx content_expressions.cmx \ + mpresentation.cmx content2pres.cmi cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \ mpresentation.cmi cexpr2pres_hashtbl.cmi cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \ diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 76470873b..126e250ba 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -2,11 +2,11 @@ PACKAGE = cic_transformations REQUIRES = helm-xml helm-cic_proof_checking gdome2-xslt PREDICATES = -INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli cic2Xml.mli \ - cic2content.mli content_expressions.mli contentPp.mli \ - mpresentation.mli cexpr2pres.mli content2pres.mli \ - cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli \ - sequentPp.mli applyStylesheets.mli +INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ + cic2Xml.mli cic2content.mli content_expressions.mli \ + contentPp.mli mpresentation.mli cexpr2pres.mli \ + content2pres.mli cexpr2pres_hashtbl.mli misc.mli \ + xml2Gdome.mli sequentPp.mli applyStylesheets.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_transformations/cic2content.ml index 464c4c5be..3fd8422cc 100644 --- a/helm/ocaml/cic_transformations/cic2content.ml +++ b/helm/ocaml/cic_transformations/cic2content.ml @@ -32,134 +32,6 @@ (* *) (**************************************************************************) -type id = string;; -type joint_recursion_kind = - [ `Recursive - | `CoRecursive - | `Inductive of int (* paramsno *) - | `CoInductive of int (* paramsno *) - ] -;; - -type var_or_const = Var | Const;; - -type 'term declaration = - { dec_name : string option; - dec_id : string ; - dec_inductive : bool; - dec_aref : string; - dec_type : 'term - } -;; - -type 'term definition = - { def_name : string option; - def_id : string ; - def_aref : string ; - def_term : 'term - } -;; - -type 'term inductive = - { inductive_id : string ; - inductive_kind : bool; - inductive_type : 'term; - inductive_constructors : 'term declaration list - } -;; - -type 'term decl_context_element = - [ `Declaration of 'term declaration - | `Hypothesis of 'term declaration - ] -;; - -type ('term,'proof) def_context_element = - [ `Proof of 'proof - | `Definition of 'term definition - ] -;; - -type ('term,'proof) in_joint_context_element = - [ `Inductive of 'term inductive - | 'term decl_context_element - | ('term,'proof) def_context_element - ] -;; - -type ('term,'proof) joint = - { joint_id : string ; - joint_kind : joint_recursion_kind ; - joint_defs : ('term,'proof) in_joint_context_element list - } -;; - -type ('term,'proof) joint_context_element = - [ `Joint of ('term,'proof) joint ] -;; - -type 'term proof = - { proof_name : string option; - proof_id : string ; - proof_context : 'term in_proof_context_element list ; - proof_apply_context: 'term proof list; - proof_conclude : 'term conclude_item - } - -and 'term in_proof_context_element = - [ 'term decl_context_element - | ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] - -and 'term conclude_item = - { conclude_id :string; - conclude_aref : string; - conclude_method : string; - conclude_args : ('term arg) list ; - conclude_conclusion : 'term option - } - -and 'term arg = - Aux of int - | Premise of premise - | Term of 'term - | ArgProof of 'term proof - | ArgMethod of string (* ???? *) - -and premise = - { premise_id: string; - premise_xref : string ; - premise_binder : string option; - premise_n : int option; - } -;; - -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 -;; - -type 'term in_object_context_element = - [ `Decl of var_or_const * 'term decl_context_element - | `Def of var_or_const * 'term * ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] -;; - -type 'term cobj = - id * (* id *) - UriManager.uri list * (* params *) - 'term conjecture list option * (* optional metasenv *) - 'term in_object_context_element (* actual object *) -;; - - - (* e se mettessi la conversione di BY nell'apply_context ? *) (* sarebbe carino avere l'invariante che la proof2pres generasse sempre prove con contesto vuoto *) @@ -289,6 +161,7 @@ let test_for_lifting ~ids_to_inner_types = let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = let module C = Cic in + let module K = Content in let rec aux l subrpoofs = match l with [] -> [] @@ -298,11 +171,11 @@ let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = [] -> assert false | p::tl -> let new_arg = - Premise - { premise_id = gen_id seed; - premise_xref = p.proof_id; - premise_binder = p.proof_name; - premise_n = None + K.Premise + { K.premise_id = gen_id seed; + K.premise_xref = p.K.proof_id; + K.premise_binder = p.K.proof_name; + K.premise_n = None } in new_arg::(aux l1 tl)) else @@ -313,14 +186,14 @@ let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts = (try Hashtbl.find ids_to_inner_sorts idr with notfound -> "Type") in if sort ="Prop" then - Premise - { premise_id = gen_id seed; - premise_xref = idr; - premise_binder = Some b; - premise_n = Some n + K.Premise + { K.premise_id = gen_id seed; + K.premise_xref = idr; + K.premise_binder = Some b; + K.premise_n = Some n } - else (Term t) - | _ -> (Term t)) in + else (K.Term t) + | _ -> (K.Term t)) in hd::(aux l1 subproofs) in aux l subproofs ;; @@ -330,17 +203,17 @@ conclude element to the apply_context list, in case context is empty. Otherwise, it just returns [p] *) let flat seed p = - if (p.proof_context = []) then - if p.proof_apply_context = [] then [p] + let module K = Content in + if (p.K.proof_context = []) then + if p.K.proof_apply_context = [] then [p] else let p1 = - { proof_name = p.proof_name; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = []; - proof_conclude = p.proof_conclude; + { p with + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = [] } in - p.proof_apply_context@[p1] + p.K.proof_apply_context@[p1] else [p] ;; @@ -353,59 +226,61 @@ let rec serialize seed = (* top_down = true if the term is a LAMBDA or a decl *) let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = let module C2A = Cic2acic in + let module K = Content in let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected) with Not_found -> None) in match exp with None -> inner_proof | Some expty -> - if inner_proof.proof_conclude.conclude_method = "Intros+LetTac" then - { proof_name = None ; - proof_id = gen_id seed; - proof_context = [] ; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "TD_Conversion"; - conclude_args = [ArgProof inner_proof]; - conclude_conclusion = Some expty + if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then + { K.proof_name = None ; + K.proof_id = gen_id seed; + K.proof_context = [] ; + K.proof_apply_context = []; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "TD_Conversion"; + K.conclude_args = [K.ArgProof inner_proof]; + K.conclude_conclusion = Some expty }; } else - { proof_name = None ; - proof_id = gen_id seed; - proof_context = [] ; - proof_apply_context = [inner_proof]; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "BU_Conversion"; - conclude_args = - [Premise - { premise_id = gen_id seed; - premise_xref = inner_proof.proof_id; - premise_binder = None; - premise_n = None + { K.proof_name = None ; + K.proof_id = gen_id seed; + K.proof_context = [] ; + K.proof_apply_context = [inner_proof]; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "BU_Conversion"; + K.conclude_args = + [K.Premise + { K.premise_id = gen_id seed; + K.premise_xref = inner_proof.K.proof_id; + K.premise_binder = None; + K.premise_n = None } ]; - conclude_conclusion = Some expty + K.conclude_conclusion = Some expty }; } ;; let generate_exact seed t id name ~ids_to_inner_types = let module C2A = Cic2acic in - { proof_name = name; - proof_id = id ; - proof_context = [] ; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Exact"; - conclude_args = [Term t]; - conclude_conclusion = + let module K = Content in + { K.proof_name = name; + K.proof_id = id ; + K.proof_context = [] ; + 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.Term t]; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None }; @@ -415,20 +290,21 @@ let generate_exact seed t id name ~ids_to_inner_types = let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types = let module C2A = Cic2acic in let module C = Cic in - { proof_name = name; - proof_id = id ; - proof_context = [] ; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Intros+LetTac"; - conclude_args = [ArgProof inner_proof]; - conclude_conclusion = + let module K = Content in + { K.proof_name = name; + K.proof_id = id ; + K.proof_context = [] ; + K.proof_apply_context = []; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Intros+LetTac"; + K.conclude_args = [K.ArgProof inner_proof]; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> - (match inner_proof.proof_conclude.conclude_conclusion with + (match inner_proof.K.proof_conclude.K.conclude_conclusion with None -> None | Some t -> if is_intro then Some (C.AProd ("gen"^id,n,s,t)) @@ -438,35 +314,37 @@ 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 - { dec_name = name_of n; - dec_id = gen_id seed; - dec_inductive = false; - dec_aref = id; - dec_type = s + { 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 - { dec_name = name_of n; - dec_id = gen_id seed; - dec_inductive = false; - dec_aref = id; - dec_type = s + { K.dec_name = name_of n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s } ;; 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 - { def_name = name_of n; - def_id = gen_id seed; - def_aref = id; - def_term = t + { K.def_name = name_of n; + K.def_id = gen_id seed; + K.def_aref = id; + K.def_term = t } (* the following function must be called with an object of sort @@ -477,6 +355,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let rec aux ?(name = None) t = let module C = Cic in let module X = Xml in + let module K = Content in let module U = UriManager in let module C2A = Cic2acic in let t1 = @@ -505,19 +384,17 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = if sort = "Prop" then let proof = aux t ~name:None in let proof' = - if proof.proof_conclude.conclude_method = "Intros+LetTac" then - match proof.proof_conclude.conclude_args with - [ArgProof p] -> p + if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then + match proof.K.proof_conclude.K.conclude_args with + [K.ArgProof p] -> p | _ -> assert false else proof in let proof'' = - { proof_name = None; - proof_id = proof'.proof_id; - proof_context = + { proof' with + K.proof_name = None; + K.proof_context = (build_decl_item seed id n s ids_to_inner_sorts):: - proof'.proof_context; - proof_apply_context = proof'.proof_apply_context; - proof_conclude = proof'.proof_conclude; + proof'.K.proof_context } in generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types @@ -527,18 +404,18 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = if sort = "Prop" then let proof = aux t in let proof' = - if proof.proof_conclude.conclude_method = "Intros+LetTac" then - match proof.proof_conclude.conclude_args with - [ArgProof p] -> p + if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then + match proof.K.proof_conclude.K.conclude_args with + [K.ArgProof p] -> p | _ -> assert false else proof in let proof'' = { proof' with - proof_name = name; - proof_context = + K.proof_name = name; + K.proof_context = ((build_def_item seed id n s ids_to_inner_sorts - ids_to_inner_types) :> Cic.annterm in_proof_context_element) - ::proof'.proof_context; + ids_to_inner_types):> Cic.annterm K.in_proof_context_element) + ::proof'.K.proof_context; } in generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types @@ -558,16 +435,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = | _ -> List.map (aux ~name:(Some "H")) args_to_lift in let args = build_args seed li subproofs ~ids_to_inner_types ~ids_to_inner_sorts in - { proof_name = name; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = serialize seed subproofs; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Apply"; - conclude_args = args; - conclude_conclusion = + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = serialize seed subproofs; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Apply"; + K.conclude_args = args; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None @@ -586,150 +463,150 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let teid = get_id te in - let pp = List.map (function p -> (ArgProof (aux p))) patterns in + 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 Some tety -> (* we must lift up the argument *) let p = (aux te) in - { proof_name = Some "name"; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = flat seed p; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Case"; - conclude_args = (Term ty)::(Term te)::pp; - conclude_conclusion = + { K.proof_name = Some "name"; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = flat seed p; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Case"; + K.conclude_args = (K.Term ty)::(K.Term te)::pp; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None - }; + } } | None -> - { proof_name = name; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Case"; - conclude_args = (Term ty)::(Term te)::pp; - conclude_conclusion = + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = []; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Case"; + K.conclude_args = (K.Term ty)::(K.Term te)::pp; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None - }; + } } ) | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> let proof = (aux bo) in (* must be recursive !! *) - { proof_name = name; - proof_id = gen_id seed; - proof_context = [`Proof proof]; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Exact"; - conclude_args = - [ Premise - { premise_id = gen_id seed; - premise_xref = proof.proof_id; - premise_binder = proof.proof_name; - premise_n = Some 1; + { 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; } ]; - conclude_conclusion = + 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 let jo = - { joint_id = gen_id seed; - joint_kind = `Recursive; - joint_defs = proofs + { K.joint_id = gen_id seed; + K.joint_kind = `Recursive; + K.joint_defs = proofs } in - { proof_name = name; - proof_id = gen_id seed; - proof_context = [`Joint jo]; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Exact"; - conclude_args = - [ Premise - { premise_id = gen_id seed; - premise_xref = jo.joint_id; - premise_binder = Some "tiralo fuori"; - premise_n = Some no; + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = [`Joint jo]; + 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 = jo.K.joint_id; + K.premise_binder = Some "tiralo fuori"; + K.premise_n = Some no; } ]; - conclude_conclusion = + 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 !! *) - { proof_name = name; - proof_id = gen_id seed; - proof_context = [`Proof proof]; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Exact"; - conclude_args = - [ Premise - { premise_id = gen_id seed; - premise_xref = proof.proof_id; - premise_binder = proof.proof_name; - premise_n = Some 1; + { 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; } ]; - conclude_conclusion = + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None - }; + } } | C.ACoFix (id,no,funs) -> let proofs = List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in let jo = - { joint_id = gen_id seed; - joint_kind = `Recursive; - joint_defs = proofs + { K.joint_id = gen_id seed; + K.joint_kind = `Recursive; + K.joint_defs = proofs } in - { proof_name = name; - proof_id = gen_id seed; - proof_context = [`Joint jo]; - proof_apply_context = []; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Exact"; - conclude_args = - [ Premise - { premise_id = gen_id seed; - premise_xref = jo.joint_id; - premise_binder = Some "tiralo fuori"; - premise_n = Some no; + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = [`Joint jo]; + 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 = jo.K.joint_id; + K.premise_binder = Some "tiralo fuori"; + K.premise_n = Some no; } ]; - conclude_conclusion = + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None @@ -743,6 +620,7 @@ in aux ~name: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 module C2A = Cic2acic in + let module K = Content in let module C = Cic in match li with C.AConst (idc,uri,exp_named_subst)::args -> @@ -826,11 +704,11 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = Cic.ALambda(id2,n2,s2,t2) -> let inductive_hyp = `Hypothesis - { dec_name = name_of n2; - dec_id = gen_id seed; - dec_inductive = true; - dec_aref = id2; - dec_type = s2 + { K.dec_name = name_of n2; + K.dec_id = gen_id seed; + K.dec_inductive = true; + K.dec_aref = id2; + K.dec_type = s2 } in let (context,body) = bc (t,t2) in (ce::inductive_hyp::context,body) @@ -841,40 +719,39 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = (ce::context,body)) | _ , t -> ([],aux t ~name:None) in bc (ty,arg) in - ArgProof - { proof_name = Some name; - proof_id = bo.proof_id; - proof_context = co; - proof_apply_context = bo.proof_apply_context; - proof_conclude = bo.proof_conclude; + K.ArgProof + { bo with + K.proof_name = Some name; + K.proof_context = co; }; - else (Term arg) in + else (K.Term arg) in hdarg::(build_method_args (tlc,tla)) | _ -> assert false in build_method_args (constructors1,args_for_cases) in - { proof_name = None; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = subproofs; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "ByInduction"; - conclude_args = - Aux no_constructors - ::Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) + { K.proof_name = None; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = subproofs; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "ByInduction"; + K.conclude_args = + K.Aux no_constructors + ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) ::method_args@other_method_args; - conclude_conclusion = + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> 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 module C2A = Cic2acic in + let module K = Content in let module C = Cic in match li with C.AConst (sid,uri,exp_named_subst)::args -> @@ -888,36 +765,36 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = | a::tl -> let hd = if n = 0 then - Premise - { premise_id = gen_id seed; - premise_xref = subproof.proof_id; - premise_binder = None; - premise_n = None + K.Premise + { K.premise_id = gen_id seed; + K.premise_xref = subproof.K.proof_id; + K.premise_binder = None; + K.premise_n = None } else let aid = get_id a in let asort = (try (Hashtbl.find ids_to_inner_sorts aid) with Not_found -> "Type") in if asort = "Prop" then - ArgProof (aux a) - else Term a in + K.ArgProof (aux a) + else K.Term a in hd::(ma_aux (n-1) tl) in (ma_aux 3 args) in - { proof_name = None; - proof_id = gen_id seed; - proof_context = []; - proof_apply_context = [subproof]; - proof_conclude = - { conclude_id = gen_id seed; - conclude_aref = id; - conclude_method = "Rewrite"; - conclude_args = - Term (C.AConst (sid,uri,exp_named_subst))::method_args; - conclude_conclusion = + { K.proof_name = None; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = [subproof]; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Rewrite"; + K.conclude_args = + K.Term (C.AConst (sid,uri,exp_named_subst))::method_args; + K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with notfound -> None - }; + } } else raise NotApplicable | _ -> raise NotApplicable @@ -947,6 +824,7 @@ let map_conjectures let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = let module C = Cic in + let module K = Content in let module C2A = Cic2acic in let seed = ref 0 in function @@ -956,57 +834,59 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = (List.map (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types) conjectures), - `Def (Const,ty, + `Def (K.Const,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (_,_,n,Some bo,ty,params) -> (gen_id seed, params, None, - `Def (Const,ty, + `Def (K.Const,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (id,_,n,None,ty,params) -> (gen_id seed, params, None, - `Decl (Const, + `Decl (K.Const, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) | C.AVariable (_,n,Some bo,ty,params) -> (gen_id seed, params, None, - `Def (Var,ty, + `Def (K.Var,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AVariable (id,n,None,ty,params) -> (gen_id seed, params, None, - `Decl (Var, + `Decl (K.Var, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) | C.AInductiveDefinition (id,l,params,nparams) -> (gen_id seed, params, None, `Joint - { joint_id = gen_id seed; - joint_kind = `Inductive nparams; - joint_defs = List.map (build_inductive seed) l + { K.joint_id = gen_id seed; + K.joint_kind = `Inductive nparams; + K.joint_defs = List.map (build_inductive seed) l }) and build_inductive seed = + let module K = Content in fun (_,n,b,ty,l) -> `Inductive - { inductive_id = gen_id seed; - inductive_kind = b; - inductive_type = ty; - inductive_constructors = build_constructors seed l + { K.inductive_id = gen_id seed; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed l } and build_constructors seed l = - List.map - (fun (n,t) -> - { dec_name = Some n; - dec_id = gen_id seed; - dec_inductive = false; - dec_aref = ""; - dec_type = t - }) l + let module K = Content in + List.map + (fun (n,t) -> + { K.dec_name = Some n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = t + }) l ;; (* diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_transformations/cic2content.mli index f3a38be50..16eb5333f 100644 --- a/helm/ocaml/cic_transformations/cic2content.mli +++ b/helm/ocaml/cic_transformations/cic2content.mli @@ -23,134 +23,8 @@ * http://cs.unibo.it/helm/. *) -type id = string;; -type joint_recursion_kind = - [ `Recursive - | `CoRecursive - | `Inductive of int (* paramsno *) - | `CoInductive of int (* paramsno *) - ] -;; - -type var_or_const = Var | Const;; - -type 'term declaration = - { dec_name : string option; - dec_id : string ; - dec_inductive : bool; - dec_aref : string; - dec_type : 'term - } -;; - -type 'term definition = - { def_name : string option; - def_id : string ; - def_aref : string ; - def_term : 'term - } -;; - -type 'term inductive = - { inductive_id : string ; - inductive_kind : bool; - inductive_type : 'term; - inductive_constructors : 'term declaration list - } -;; - -type 'term decl_context_element = - [ `Declaration of 'term declaration - | `Hypothesis of 'term declaration - ] -;; - -type ('term,'proof) def_context_element = - [ `Proof of 'proof - | `Definition of 'term definition - ] -;; - -type ('term,'proof) in_joint_context_element = - [ `Inductive of 'term inductive - | 'term decl_context_element - | ('term,'proof) def_context_element - ] -;; - -type ('term,'proof) joint = - { joint_id : string ; - joint_kind : joint_recursion_kind ; - joint_defs : ('term,'proof) in_joint_context_element list - } -;; - -type ('term,'proof) joint_context_element = - [ `Joint of ('term,'proof) joint ] -;; - -type 'term proof = - { proof_name : string option; - proof_id : string ; - proof_context : 'term in_proof_context_element list ; - proof_apply_context: 'term proof list; - proof_conclude : 'term conclude_item - } - -and 'term in_proof_context_element = - [ 'term decl_context_element - | ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] - -and 'term conclude_item = - { conclude_id :string; - conclude_aref : string; - conclude_method : string; - conclude_args : ('term arg) list ; - conclude_conclusion : 'term option - } - -and 'term arg = - Aux of int - | Premise of premise - | Term of 'term - | ArgProof of 'term proof - | ArgMethod of string (* ???? *) - -and premise = - { premise_id: string; - premise_xref : string ; - premise_binder : string option; - premise_n : int option; - } -;; - -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 -;; - -type 'term in_object_context_element = - [ `Decl of var_or_const * 'term decl_context_element - | `Def of var_or_const * 'term * ('term,'term proof) def_context_element - | ('term,'term proof) joint_context_element - ] -;; - -type 'term cobj = - id * (* id *) - UriManager.uri list * (* params *) - 'term conjecture list option * (* optional metasenv *) - 'term in_object_context_element (* actual object *) -;; - val annobj2content : ids_to_inner_sorts:(string, string) Hashtbl.t -> ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> Cic.annobj -> - Cic.annterm cobj + Cic.annterm Content.cobj diff --git a/helm/ocaml/cic_transformations/content.ml b/helm/ocaml/cic_transformations/content.ml new file mode 100644 index 000000000..be46f5961 --- /dev/null +++ b/helm/ocaml/cic_transformations/content.ml @@ -0,0 +1,159 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(**************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 16/62003 *) +(* *) +(**************************************************************************) + +type id = string;; +type joint_recursion_kind = + [ `Recursive + | `CoRecursive + | `Inductive of int (* paramsno *) + | `CoInductive of int (* paramsno *) + ] +;; + +type var_or_const = Var | Const;; + +type 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +;; + +type 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +;; + +type 'term inductive = + { inductive_id : string ; + inductive_kind : bool; + inductive_type : 'term; + inductive_constructors : 'term declaration list + } +;; + +type 'term decl_context_element = + [ `Declaration of 'term declaration + | `Hypothesis of 'term declaration + ] +;; + +type ('term,'proof) def_context_element = + [ `Proof of 'proof + | `Definition of 'term definition + ] +;; + +type ('term,'proof) in_joint_context_element = + [ `Inductive of 'term inductive + | 'term decl_context_element + | ('term,'proof) def_context_element + ] +;; + +type ('term,'proof) joint = + { joint_id : string ; + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list + } +;; + +type ('term,'proof) joint_context_element = + [ `Joint of ('term,'proof) joint ] +;; + +type 'term proof = + { proof_name : string option; + proof_id : string ; + proof_context : 'term in_proof_context_element list ; + proof_apply_context: 'term proof list; + proof_conclude : 'term conclude_item + } + +and 'term in_proof_context_element = + [ 'term decl_context_element + | ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] + +and 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } + +and 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) + +and premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + +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 +;; + +type 'term in_object_context_element = + [ `Decl of var_or_const * 'term decl_context_element + | `Def of var_or_const * 'term * ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] +;; + +type 'term cobj = + id * (* id *) + UriManager.uri list * (* params *) + 'term conjecture list option * (* optional metasenv *) + 'term in_object_context_element (* actual object *) +;; diff --git a/helm/ocaml/cic_transformations/content.mli b/helm/ocaml/cic_transformations/content.mli new file mode 100644 index 000000000..b58b84b54 --- /dev/null +++ b/helm/ocaml/cic_transformations/content.mli @@ -0,0 +1,150 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type id = string;; +type joint_recursion_kind = + [ `Recursive + | `CoRecursive + | `Inductive of int (* paramsno *) + | `CoInductive of int (* paramsno *) + ] +;; + +type var_or_const = Var | Const;; + +type 'term declaration = + { dec_name : string option; + dec_id : string ; + dec_inductive : bool; + dec_aref : string; + dec_type : 'term + } +;; + +type 'term definition = + { def_name : string option; + def_id : string ; + def_aref : string ; + def_term : 'term + } +;; + +type 'term inductive = + { inductive_id : string ; + inductive_kind : bool; + inductive_type : 'term; + inductive_constructors : 'term declaration list + } +;; + +type 'term decl_context_element = + [ `Declaration of 'term declaration + | `Hypothesis of 'term declaration + ] +;; + +type ('term,'proof) def_context_element = + [ `Proof of 'proof + | `Definition of 'term definition + ] +;; + +type ('term,'proof) in_joint_context_element = + [ `Inductive of 'term inductive + | 'term decl_context_element + | ('term,'proof) def_context_element + ] +;; + +type ('term,'proof) joint = + { joint_id : string ; + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list + } +;; + +type ('term,'proof) joint_context_element = + [ `Joint of ('term,'proof) joint ] +;; + +type 'term proof = + { proof_name : string option; + proof_id : string ; + proof_context : 'term in_proof_context_element list ; + proof_apply_context: 'term proof list; + proof_conclude : 'term conclude_item + } + +and 'term in_proof_context_element = + [ 'term decl_context_element + | ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] + +and 'term conclude_item = + { conclude_id :string; + conclude_aref : string; + conclude_method : string; + conclude_args : ('term arg) list ; + conclude_conclusion : 'term option + } + +and 'term arg = + Aux of int + | Premise of premise + | Term of 'term + | ArgProof of 'term proof + | ArgMethod of string (* ???? *) + +and premise = + { premise_id: string; + premise_xref : string ; + premise_binder : string option; + premise_n : int option; + } +;; + +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 +;; + +type 'term in_object_context_element = + [ `Decl of var_or_const * 'term decl_context_element + | `Def of var_or_const * 'term * ('term,'term proof) def_context_element + | ('term,'term proof) joint_context_element + ] +;; + +type 'term cobj = + id * (* id *) + UriManager.uri list * (* params *) + 'term conjecture list option * (* optional metasenv *) + 'term in_object_context_element (* actual object *) +;; diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index c2d10e519..46585f14c 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -42,7 +42,7 @@ let rec split n l = let is_big_general countterm p = let maxsize = Cexpr2pres.maxsize in - let module Con = Cic2content in + let module Con = Content in let rec countp current_size p = if current_size > maxsize then current_size else @@ -143,7 +143,7 @@ let make_concl verb concl = ;; let make_args_for_apply term2pres args = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let rec make_arg_for_apply is_first arg row = (match arg with @@ -168,7 +168,7 @@ let make_args_for_apply term2pres args = | _ -> assert false;; let rec justification term2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or ((p.Con.proof_context = []) & @@ -183,7 +183,7 @@ let rec justification term2pres p = and proof2pres term2pres p = let rec proof2pres p = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in let indent = let is_decl e = @@ -239,7 +239,7 @@ and proof2pres term2pres p = and ce2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function `Declaration d -> (match d.Con.dec_name with @@ -322,7 +322,7 @@ and proof2pres term2pres p = [P.Mtd ([], conclude_aux conclude)]) and conclude_aux conclude = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in if conclude.Con.conclude_method = "TD_Conversion" then let expected = @@ -446,7 +446,7 @@ and proof2pres term2pres p = and arg2pres = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.Aux n -> P.Mtext ([],"aux " ^ string_of_int n) @@ -461,7 +461,7 @@ and proof2pres term2pres p = and byinduction conclude = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"No conclusion???") @@ -507,7 +507,7 @@ and proof2pres term2pres p = and make_case = let module P = Mpresentation in - let module Con = Cic2content in + let module Con = Content in function Con.ArgProof p -> let name = @@ -591,7 +591,7 @@ proof2pres p exception ToDo;; let content2pres term2pres (id,params,metasenv,obj) = - let module Con = Cic2content in + let module Con = Content in let module P = Mpresentation in match obj with `Def (Con.Const,thesis,`Proof p) -> diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 45d652c11..9b7411685 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -34,4 +34,4 @@ val content2pres : ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> - Cic.annterm Cic2content.cobj -> Mpresentation.mpres + Cic.annterm Content.cobj -> Mpresentation.mpres diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml index e42c98790..3bc8bb306 100644 --- a/helm/ocaml/cic_transformations/contentPp.ml +++ b/helm/ocaml/cic_transformations/contentPp.ml @@ -58,8 +58,8 @@ let rec blanks n = if n = 0 then "" else (" " ^ (blanks (n-1)));; -let rec pproof (p: Cic.annterm Cic2content.proof) indent = - let module Con = Cic2content in +let rec pproof (p: Cic.annterm Content.proof) indent = + let module Con = Content in let new_indent = (match p.Con.proof_name with Some s -> @@ -77,7 +77,7 @@ and pcontext c indent = List.iter (pcontext_element indent) c and pcontext_element indent = - let module Con = Cic2content in + let module Con = Content in function `Declaration d -> (match d.Con.dec_name with @@ -117,7 +117,7 @@ and papply_context ac indent = List.iter(function p -> (pproof p indent)) ac and pconclude concl indent = - let module Con = Cic2content in + let module Con = Content in prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr; pargs concl.Con.conclude_args indent; match concl.Con.conclude_conclusion with @@ -128,7 +128,7 @@ and pargs args indent = List.iter (parg indent) args and parg indent = - let module Con = Cic2content in + let module Con = Content in function Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr diff --git a/helm/ocaml/cic_transformations/contentPp.mli b/helm/ocaml/cic_transformations/contentPp.mli index ddaf76b23..85ce238f3 100644 --- a/helm/ocaml/cic_transformations/contentPp.mli +++ b/helm/ocaml/cic_transformations/contentPp.mli @@ -23,6 +23,6 @@ * http://cs.unibo.it/helm/. *) -val print_proof: Cic.annterm Cic2content.proof -> unit +val print_proof: Cic.annterm Content.proof -> unit -- 2.39.2