X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2content.ml;h=3fd8422cc30540e4c2a0f905ffcc2fe9b611b03f;hb=43f61eedd2a1f499166de33a98af00b767dcc117;hp=d4b729606b778c55ada75b7a9fada6d38f641b42;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_transformations/cic2content.ml index d4b729606..3fd8422cc 100644 --- a/helm/ocaml/cic_transformations/cic2content.ml +++ b/helm/ocaml/cic_transformations/cic2content.ml @@ -31,96 +31,6 @@ (* 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 *) - -and 'term cconstructor = - string * 'term (* id, type *) - -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 = - { dec_name : string option; - dec_id : string ; - dec_inductive : bool; - dec_aref : string; - dec_type : 'term - } -and - 'term definition = - { def_name : string option; - def_id : string ; - def_aref : string ; - def_term : 'term - } -and - 'term joint = - { joint_id : string ; - joint_kind : recursion_kind ; - joint_defs : 'term context_element list - } -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; - } -;; - (* e se mettessi la conversione di BY nell'apply_context ? *) (* sarebbe carino avere l'invariante che la proof2pres @@ -139,7 +49,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 *) @@ -252,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 [] -> [] @@ -261,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 @@ -276,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 ;; @@ -293,18 +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_kind = NoRecursive; - 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] ;; @@ -317,62 +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_kind = NoRecursive; - 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_kind = NoRecursive; - 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_kind = NoRecursive; - 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 }; @@ -382,21 +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_kind = NoRecursive; - 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)) @@ -406,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 + `Hypothesis + { K.dec_name = name_of n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s } else - Declaration - { dec_name = name_of n; - dec_id = gen_id seed; - dec_inductive = false; - dec_aref = id; - dec_type = s + `Declaration + { K.dec_name = name_of n; + K.dec_id = gen_id seed; + K.dec_inductive = false; + K.dec_aref = id; + K.dec_type = s } ;; 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) + `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 + `Definition + { 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 @@ -445,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 = @@ -473,20 +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_kind = proof'.proof_kind ; - 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 @@ -496,20 +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_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 + K.proof_name = name; + K.proof_context = + ((build_def_item seed id n s ids_to_inner_sorts + 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 @@ -529,17 +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_kind = NoRecursive; - 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 @@ -558,156 +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_kind = NoRecursive; - 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_kind = NoRecursive; - 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_kind = NoRecursive; - 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 + 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_kind = NoRecursive; - 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_kind = NoRecursive; - 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 + 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_kind = NoRecursive; - 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 @@ -721,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 -> @@ -803,58 +703,55 @@ 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 - { dec_name = name_of n2; - dec_id = gen_id seed; - dec_inductive = true; - dec_aref = id2; - dec_type = s2 + `Hypothesis + { 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) - | _ -> 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 (ce::context,body)) | _ , t -> ([],aux t ~name:None) in bc (ty,arg) in - 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; + 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_kind = NoRecursive; - 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 -> @@ -868,71 +765,130 @@ 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) + 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 + 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_kind = NoRecursive; - 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 +;; + +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 K = Content 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 (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 (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 (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 (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 (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 + { 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 + { 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 = + 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 +;; + (* and 'term cinductiveType = id * string * bool * 'term * (* typename, inductive, arity *) @@ -942,3 +898,4 @@ and 'term cconstructor = string * 'term *) +