X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2content.ml;h=464c4c5bec92e6fc90bf7be7f8a21134bfea12ff;hb=4a01e6197e070d3eff7a3fe02180597136d81eba;hp=d4b729606b778c55ada75b7a9fada6d38f641b42;hpb=62820aacb94856be5cd2e125032669245ca1408d;p=helm.git 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 *) +