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