From: Andrea Asperti Date: Fri, 18 Jul 2003 18:01:29 +0000 (+0000) Subject: CSC: tentative definition of the ocaml structure that represents X-Git-Tag: LucaOK~61 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4a01e6197e070d3eff7a3fe02180597136d81eba CSC: tentative definition of the ocaml structure that represents OMDoc objects. --- diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml index 17ba99ed8..a4f8cd1ae 100644 --- a/helm/gTopLevel/content2cic.ml +++ b/helm/gTopLevel/content2cic.ml @@ -55,31 +55,31 @@ let proof2cic term2cic p = let module C = Cic in let module Con = Cic2content in match ce with - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> C.Lambda (C.Name s, term2cic d.Con.dec_type, target) | None -> C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target)) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> C.Lambda (C.Name s, term2cic h.Con.dec_type, target) | None -> C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target)) - | Con.Proof p -> + | `Proof p -> (match p.Con.proof_name with Some s -> C.LetIn (C.Name s, proof2cic premise_env p, target) | None -> C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | Con.Definition d -> + | `Definition d -> (match d.Con.def_name with Some s -> C.LetIn (C.Name s, proof2cic premise_env p, target) | None -> C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | Con.Joint ho -> + | `Joint ho -> raise TO_DO and conclude2cic premise_env conclude = diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 5291c3587..a54db659d 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -210,14 +210,9 @@ class proof_viewer obj = Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> let time1 = Sys.time () in let content = - Cic2content.acic2content - (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts ~ids_to_inner_types bo in - let content2pres = - (Content2pres.proof2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p)))) in - let pres = content2pres content in + Cic2content.annobj2content + ~ids_to_inner_sorts ~ids_to_inner_types acic in + let pres = Content2pres.content2pres ~ids_to_inner_sorts content in let time2 = Sys.time () in (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) let xmlpres = Mpresentation.print_mpres pres in diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_transformations/cic2content.ml index d4b729606..464c4c5be 100644 --- a/helm/ocaml/cic_transformations/cic2content.ml +++ b/helm/ocaml/cic_transformations/cic2content.ml @@ -31,95 +31,133 @@ (* 16/62003 *) (* *) (**************************************************************************) -type id = string;; -type recursion_kind = NoRecursive | Recursive | CoRecursive;; - -type 'term cobj = - Def of id * id option * string * (* name, *) - 'term option * 'term * (* body, type, *) - UriManager.uri list (* parameters *) - | Theorem of id * id option * string * (* name, *) - ('term proof) option * 'term * (* body, type, *) - UriManager.uri list (* parameters *) - | Variable of id * - string * 'term option * 'term * (* name, body, type *) - UriManager.uri list -(* (* parameters *) - | CurrentProof of id * id * - string * annmetasenv * (* name, conjectures, *) - 'term proof * 'term * UriManager.uri list (* value,type,parameters *) -*) - | InductiveDefinition of id * - 'term cinductiveType list * (* inductive types , *) - UriManager.uri list * int (* parameters,n ind. pars *) -and 'term cinductiveType = - id * string * bool * 'term * (* typename, inductive, arity *) - 'term cconstructor list (* constructors *) +type id = string;; +type joint_recursion_kind = + [ `Recursive + | `CoRecursive + | `Inductive of int (* paramsno *) + | `CoInductive of int (* paramsno *) + ] +;; -and 'term cconstructor = - string * 'term (* id, type *) +type var_or_const = Var | Const;; -and - 'term proof = - { proof_name : string option; - proof_id : string ; - proof_kind : recursion_kind ; - proof_context : ('term context_element) list ; - proof_apply_context: ('term proof) list; - proof_conclude : 'term conclude_item; - } -and - 'term context_element = - Declaration of 'term declaration - | Hypothesis of 'term declaration - | Proof of 'term proof - | Definition of 'term definition - | Joint of 'term joint -and - 'term declaration = +type 'term declaration = { dec_name : string option; dec_id : string ; dec_inductive : bool; dec_aref : string; dec_type : 'term } -and - 'term definition = +;; + +type 'term definition = { def_name : string option; def_id : string ; def_aref : string ; def_term : 'term } -and - 'term joint = +;; + +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 : recursion_kind ; - joint_defs : 'term context_element list + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list } -and - 'term conclude_item = +;; + +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 = + +and 'term arg = Aux of int | Premise of premise | Term of 'term | ArgProof of 'term proof | ArgMethod of string (* ???? *) -and - premise = + +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 ? *) @@ -139,7 +177,6 @@ let name_of = function exception Not_a_proof;; exception NotImplemented;; exception NotApplicable;; -exception ToDo;; (* we do not care for positivity, here, that in any case is enforced by well typing. Just a brutal search *) @@ -261,8 +298,8 @@ 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 + { premise_id = gen_id seed; premise_xref = p.proof_id; premise_binder = p.proof_name; premise_n = None @@ -299,7 +336,6 @@ let flat seed p = let p1 = { proof_name = p.proof_name; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = []; proof_apply_context = []; proof_conclude = p.proof_conclude; @@ -326,7 +362,6 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = if inner_proof.proof_conclude.conclude_method = "Intros+LetTac" then { proof_name = None ; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = [] ; proof_apply_context = []; proof_conclude = @@ -340,7 +375,6 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types = else { proof_name = None ; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = [] ; proof_apply_context = [inner_proof]; proof_conclude = @@ -364,7 +398,6 @@ let generate_exact seed t id name ~ids_to_inner_types = let module C2A = Cic2acic in { proof_name = name; proof_id = id ; - proof_kind = NoRecursive; proof_context = [] ; proof_apply_context = []; proof_conclude = @@ -384,7 +417,6 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ let module C = Cic in { proof_name = name; proof_id = id ; - proof_kind = NoRecursive; proof_context = [] ; proof_apply_context = []; proof_conclude = @@ -408,7 +440,7 @@ 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 sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in if sort = "Prop" then - Hypothesis + `Hypothesis { dec_name = name_of n; dec_id = gen_id seed; dec_inductive = false; @@ -416,7 +448,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts = dec_type = s } else - Declaration + `Declaration { dec_name = name_of n; dec_id = gen_id seed; dec_inductive = false; @@ -428,9 +460,9 @@ let build_decl_item seed id n s ~ids_to_inner_sorts = let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = 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) + `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) else - Definition + `Definition { def_name = name_of n; def_id = gen_id seed; def_aref = id; @@ -481,7 +513,6 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let proof'' = { proof_name = None; proof_id = proof'.proof_id; - proof_kind = proof'.proof_kind ; proof_context = (build_decl_item seed id n s ids_to_inner_sorts):: proof'.proof_context; @@ -502,14 +533,12 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = | _ -> assert false else proof in let proof'' = - { proof_name = name; - proof_id = proof'.proof_id; - proof_kind = proof'.proof_kind ; - proof_context = - (build_def_item seed id n s ids_to_inner_sorts - ids_to_inner_types)::proof'.proof_context; - proof_apply_context = proof'.proof_apply_context; - proof_conclude = proof'.proof_conclude; + { proof' with + proof_name = name; + 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; } in generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types @@ -531,7 +560,6 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = ~ids_to_inner_types ~ids_to_inner_sorts in { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = []; proof_apply_context = serialize seed subproofs; proof_conclude = @@ -567,7 +595,6 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let p = (aux te) in { proof_name = Some "name"; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = []; proof_apply_context = flat seed p; proof_conclude = @@ -584,7 +611,6 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = | None -> { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = []; proof_apply_context = []; proof_conclude = @@ -603,8 +629,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let proof = (aux bo) in (* must be recursive !! *) { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; - proof_context = [Proof proof]; + proof_context = [`Proof proof]; proof_apply_context = []; proof_conclude = { conclude_id = gen_id seed; @@ -626,17 +651,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = } | C.AFix (id, no, funs) -> let proofs = - List.map (function (id1,n,_,ty,bo) -> (Proof (aux bo))) funs in + List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in let jo = { joint_id = gen_id seed; - joint_kind = Recursive; + joint_kind = `Recursive; joint_defs = proofs } in { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; - proof_context = [Joint jo]; + proof_context = [`Joint jo]; proof_apply_context = []; proof_conclude = { conclude_id = gen_id seed; @@ -660,8 +684,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let proof = (aux bo) in (* must be recursive !! *) { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; - proof_context = [Proof proof]; + proof_context = [`Proof proof]; proof_apply_context = []; proof_conclude = { conclude_id = gen_id seed; @@ -683,17 +706,16 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = } | C.ACoFix (id,no,funs) -> let proofs = - List.map (function (id1,n,ty,bo) -> (Proof (aux bo))) funs in + List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in let jo = { joint_id = gen_id seed; - joint_kind = Recursive; + joint_kind = `Recursive; joint_defs = proofs } in { proof_name = name; proof_id = gen_id seed; - proof_kind = NoRecursive; - proof_context = [Joint jo]; + proof_context = [`Joint jo]; proof_apply_context = []; proof_conclude = { conclude_id = gen_id seed; @@ -803,7 +825,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = match t1 with Cic.ALambda(id2,n2,s2,t2) -> let inductive_hyp = - Hypothesis + `Hypothesis { dec_name = name_of n2; dec_id = gen_id seed; dec_inductive = true; @@ -812,7 +834,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = } in let (context,body) = bc (t,t2) in (ce::inductive_hyp::context,body) - | _ -> assert false) + | _ -> 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 @@ -822,18 +844,16 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = ArgProof { proof_name = Some name; proof_id = bo.proof_id; - proof_kind = NoRecursive; proof_context = co; proof_apply_context = bo.proof_apply_context; proof_conclude = bo.proof_conclude; }; - else (Term arg) in + else (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_kind = NoRecursive; proof_context = []; proof_apply_context = subproofs; proof_conclude = @@ -868,24 +888,23 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = | a::tl -> let hd = if n = 0 then - Premise + Premise { premise_id = gen_id seed; premise_xref = subproof.proof_id; premise_binder = None; premise_n = None } - else - let aid = get_id a in - let asort = (try (Hashtbl.find ids_to_inner_sorts aid) + 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 - hd::(ma_aux (n-1) tl) in + ArgProof (aux a) + else Term a in + hd::(ma_aux (n-1) tl) in (ma_aux 3 args) in { proof_name = None; proof_id = gen_id seed; - proof_kind = NoRecursive; proof_context = []; proof_apply_context = [subproof]; proof_conclude = @@ -902,37 +921,94 @@ and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts = } else raise NotApplicable | _ -> raise NotApplicable +;; + +let map_conjectures + seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) += + let context' = + List.map + (function + (id,None) as item -> item + | (id,Some (name,Cic.ADecl t)) -> + id, + Some + (build_decl_item seed (get_id t) name t + ~ids_to_inner_sorts) + | (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) + ) context + in + (id,n,context',ty) ;; -let annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = +let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = let module C = Cic in let module C2A = Cic2acic in let seed = ref 0 in function - C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - assert false (* TO DO *) - | C.AConstant (id,idbody,n,bo,ty,params) -> - (match idbody with - Some idb -> - let sort = - (try Hashtbl.find ids_to_inner_sorts idb - with notfound -> "Type") in - if sort = "Prop" then - let proof = - (match bo with - Some body -> - acic2content seed ~name:None ~ids_to_inner_sorts - ~ids_to_inner_types body - | None -> assert false) in - Theorem(id,idbody,n,Some proof,ty,params) - else - Def(id,idbody,n,bo,ty,params) - | None -> Def(id,idbody,n,bo,ty,params)) - | C.AVariable (id,n,bo,ty,params) -> - Variable(id,n,bo,ty,params) - | C.AInductiveDefinition (id,tys,params,nparams) -> - InductiveDefinition(id,tys,params,nparams) + C.ACurrentProof (_,_,n,conjectures,bo,ty,params) -> + (gen_id seed, params, + Some + (List.map + (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types) + conjectures), + `Def (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, + 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, + 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, + 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, + 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 + }) + +and + build_inductive seed = + fun (_,n,b,ty,l) -> + `Inductive + { inductive_id = gen_id seed; + inductive_kind = b; + inductive_type = ty; + 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 +;; + (* and 'term cinductiveType = id * string * bool * 'term * (* typename, inductive, arity *) @@ -942,3 +1018,4 @@ and 'term cconstructor = string * 'term *) + diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_transformations/cic2content.mli index 8e26bb897..f3a38be50 100644 --- a/helm/ocaml/cic_transformations/cic2content.mli +++ b/helm/ocaml/cic_transformations/cic2content.mli @@ -23,71 +23,102 @@ * http://cs.unibo.it/helm/. *) -(**************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Andrea Asperti *) -(* 16/62003 *) -(* *) -(**************************************************************************) - -type recursion_kind = NoRecursive | Recursive | CoRecursive;; - -type - 'term proof = - { proof_name : string option; - proof_id : string ; - proof_kind : recursion_kind ; - proof_context : ('term context_element) list ; - proof_apply_context: ('term proof) list; - proof_conclude : 'term conclude_item; - } -and - 'term context_element = - Declaration of 'term declaration - | Hypothesis of 'term declaration - | Proof of 'term proof - | Definition of 'term definition - | Joint of 'term joint -and - 'term declaration = +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 } -and - 'term definition = +;; + +type 'term definition = { def_name : string option; def_id : string ; def_aref : string ; def_term : 'term } -and - 'term joint = +;; + +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 : recursion_kind ; - joint_defs : 'term context_element list + joint_kind : joint_recursion_kind ; + joint_defs : ('term,'proof) in_joint_context_element list } -and - 'term conclude_item = +;; + +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 = + +and 'term arg = Aux of int | Premise of premise | Term of 'term | ArgProof of 'term proof | ArgMethod of string (* ???? *) -and - premise = + +and premise = { premise_id: string; premise_xref : string ; premise_binder : string option; @@ -95,12 +126,31 @@ and } ;; -val acic2content : - int ref -> (* seed *) - ?name:string option -> (* name *) - ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> - (* ids_to_inner_sorts *) - ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - (* ids_to_inner_types *) - Cic.annterm -> (* annotated term *) - Cic.annterm proof +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 diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 5d6923237..c2d10e519 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -62,23 +62,23 @@ let is_big_general countterm p = if current_size > maxsize then maxsize else (match e with - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> current_size + 4 + (String.length s) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> current_size + 4 + (String.length s) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Proof p -> countp current_size p - | Con.Definition d -> + | `Proof p -> countp current_size p + | `Definition d -> (match d.Con.def_name with Some s -> let c1 = (current_size + 4 + (String.length s)) in (countterm c1 d.Con.def_term) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Joint ho -> maxsize + 1) (* we assume is big *) + | `Joint ho -> maxsize + 1) (* we assume is big *) and countapplycontext current_size ac = List.fold_left countp current_size ac @@ -188,8 +188,8 @@ and proof2pres term2pres p = let indent = let is_decl e = (match e with - Con.Declaration _ - | Con.Hypothesis _ -> true + `Declaration _ + | `Hypothesis _ -> true | _ -> false) in ((List.filter is_decl p.Con.proof_context) != []) in let concl = @@ -241,7 +241,7 @@ and proof2pres term2pres p = let module P = Mpresentation in let module Con = Cic2content in function - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> let ty = term2pres d.Con.dec_type in @@ -253,7 +253,7 @@ and proof2pres term2pres p = ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> let ty = term2pres h.Con.dec_type in @@ -267,8 +267,8 @@ and proof2pres term2pres p = ty]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Proof p -> proof2pres p - | Con.Definition d -> + | `Proof p -> proof2pres p + | `Definition d -> (match d.Con.def_name with Some s -> let term = term2pres d.Con.def_term in @@ -279,7 +279,7 @@ and proof2pres term2pres p = term]) | None -> prerr_endline "NO NAME!!"; assert false) - | Con.Joint ho -> + | `Joint ho -> P.Mtext ([],"jointdef") and acontext2pres ac continuation indent = @@ -517,15 +517,15 @@ and proof2pres term2pres p = let indhyps,args = List.partition (function - Con.Hypothesis h -> h.Con.dec_inductive + `Hypothesis h -> h.Con.dec_inductive | _ -> false) p.Con.proof_context in let pattern_aux = List.fold_right (fun e p -> let dec = (match e with - Con.Declaration h - | Con.Hypothesis h -> + `Declaration h + | `Hypothesis h -> let name = (match h.Con.dec_name with None -> "NO NAME???" @@ -557,7 +557,7 @@ and proof2pres term2pres p = (P.Mtext([],"by induction hypothesis we know:")))]) in let make_hyp = function - Con.Hypothesis h -> + `Hypothesis h -> let name = (match h.Con.dec_name with None -> "no name" @@ -588,11 +588,43 @@ and proof2pres term2pres p = proof2pres p ;; -(* -let content2pres = - proof2pres - (function p -> Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr p)) -;; *) - +exception ToDo;; +let content2pres term2pres (id,params,metasenv,obj) = + let module Con = Cic2content in + let module P = Mpresentation in + match obj with + `Def (Con.Const,thesis,`Proof p) -> + P.Mtable + [None,"align","baseline 1"; + None,"equalrows","false"; + None,"columnalign","left"; + None,"helm:xref","id"] + [(*P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ params ^ ")")])] ; +*) + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mtext [] "THESIS:"])] ; + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [P.Mphantom [] + (P.Mtext [] "__") ; + term2pres thesis])] ; + P.Mtr [] + [P.Mtd [] + (P.Mrow [] + [proof2pres term2pres p])]] + | _ -> raise ToDo +;; +let content2pres ~ids_to_inner_sorts = + content2pres + (function p -> + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p))) +;; diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 6a99f1b99..45d652c11 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -32,15 +32,6 @@ (* *) (**************************************************************************) -val proof2pres : - ('a -> Mpresentation.mpres) -> - 'a Cic2content.proof -> - Mpresentation.mpres - -(* val content2pres : Cic.annterm Cic2content.proof -> Mpresentation.mpres *) - - - - - - +val content2pres : + ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> + Cic.annterm Cic2content.cobj -> Mpresentation.mpres diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml index 4206404f5..e42c98790 100644 --- a/helm/ocaml/cic_transformations/contentPp.ml +++ b/helm/ocaml/cic_transformations/contentPp.ml @@ -34,6 +34,7 @@ exception ContentPpInternalError;; exception NotEnoughElements;; +exception TO_DO (* Utility functions *) @@ -57,7 +58,7 @@ let rec blanks n = if n = 0 then "" else (" " ^ (blanks (n-1)));; -let rec pproof p indent = +let rec pproof (p: Cic.annterm Cic2content.proof) indent = let module Con = Cic2content in let new_indent = (match p.Con.proof_name with @@ -78,7 +79,7 @@ and pcontext c indent = and pcontext_element indent = let module Con = Cic2content in function - Con.Declaration d -> + `Declaration d -> (match d.Con.dec_name with Some s -> prerr_endline @@ -88,7 +89,7 @@ and pcontext_element indent = flush stderr | None -> prerr_endline ((blanks indent) ^ "NO NAME!!")) - | Con.Hypothesis h -> + | `Hypothesis h -> (match h.Con.dec_name with Some s -> prerr_endline @@ -98,8 +99,8 @@ and pcontext_element indent = flush stderr | None -> prerr_endline ((blanks indent) ^ "NO NAME!!")) - | Con.Proof p -> pproof p indent - | Con.Definition d -> + | `Proof p -> pproof p indent + | `Definition d -> (match d.Con.def_name with Some s -> prerr_endline @@ -108,7 +109,7 @@ and pcontext_element indent = flush stderr | None -> prerr_endline ((blanks indent) ^ "NO NAME!!")) - | Con.Joint ho -> + | `Joint ho -> prerr_endline ((blanks indent) ^ "Joint Def"); flush stderr @@ -136,9 +137,10 @@ and parg indent = flush stderr | Con.ArgProof p -> pproof p (indent+1) | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr - ;; let print_proof p = pproof p 0; + + diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml index de1172d2a..4dde38a36 100644 --- a/helm/ocaml/cic_transformations/mpresentation.ml +++ b/helm/ocaml/cic_transformations/mpresentation.ml @@ -219,4 +219,5 @@ let print_mpres pres = Some "xmlns","xlink","http://www.w3.org/1999/xlink" ] (print_mpres pres) >] -;; + +