From e23bc37c0a5e552395e499e7b8cee8d610b8e4f4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Jul 2003 12:10:58 +0000 Subject: [PATCH] ** UNTESTED ** Fix and CoFix are now handled "correctly" ;-) --- helm/ocaml/cic_omdoc/cic2content.ml | 80 +++++++---------------------- helm/ocaml/cic_omdoc/content.ml | 2 +- helm/ocaml/cic_omdoc/content.mli | 2 +- helm/ocaml/cic_omdoc/content2cic.ml | 45 +++++++++++++++- 4 files changed, 63 insertions(+), 66 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 7996f927a..12b806162 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -342,7 +342,7 @@ let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = try 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 { K.def_name = name_of n; @@ -357,8 +357,8 @@ let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = Prop. For debugging purposes this is tested again, possibly raising an Not_a_proof exception *) -and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = - let rec aux ?(name = None) t = +and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = + let rec aux ?name t = let module C = Cic in let module K = Content in let module C2A = Cic2acic in @@ -386,7 +386,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = | C.ALambda (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in if sort = "Prop" then - let proof = aux t ~name:None in + let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with @@ -436,7 +436,7 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let subproofs = match args_to_lift with [_] -> List.map aux args_to_lift - | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + | _ -> List.map (aux ~name:"H") args_to_lift in let args = build_args seed li subproofs ~ids_to_inner_types ~ids_to_inner_sorts in { K.proof_name = name; @@ -506,36 +506,15 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = } } ) - | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { 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; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with Not_found -> None - } - } | C.AFix (id, no, funs) -> let proofs = - List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in + List.map + (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in + let decreasing_args = + List.map (function (_,_,n,_,_) -> n) funs in let jo = { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; + K.joint_kind = `Recursive decreasing_args; K.joint_defs = proofs } in @@ -561,36 +540,13 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = with Not_found -> None } } - | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> - let proof = (aux bo) in (* must be recursive !! *) - { 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; - } - ]; - K.conclude_conclusion = - try Some - (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized - with Not_found -> None - } - } | C.ACoFix (id,no,funs) -> let proofs = - List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in + List.map + (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in let jo = { K.joint_id = gen_id seed; - K.joint_kind = `Recursive; + K.joint_kind = `CoRecursive; K.joint_defs = proofs } in @@ -619,10 +575,10 @@ and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = in let id = get_id t in generate_conversion seed false id t1 ~ids_to_inner_types -in aux ~name:name t +in aux ?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 aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -669,7 +625,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = let subproofs = match args_to_lift with [_] -> List.map aux args_to_lift - | _ -> List.map (aux ~name:(Some "H")) args_to_lift in + | _ -> List.map (aux ~name:"H") args_to_lift in prerr_endline "****** end subproofs *******"; flush stderr; let other_method_args = build_args seed other_args subproofs @@ -721,7 +677,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = ( 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 + | _ , t -> ([],aux t) in bc (ty,arg) in K.ArgProof { bo with @@ -753,7 +709,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = | _ -> 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 aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in let module C2A = Cic2acic in let module K = Content in let module C = Cic in diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml index be46f5961..2f956d7d1 100644 --- a/helm/ocaml/cic_omdoc/content.ml +++ b/helm/ocaml/cic_omdoc/content.ml @@ -34,7 +34,7 @@ type id = string;; type joint_recursion_kind = - [ `Recursive + [ `Recursive of int list | `CoRecursive | `Inductive of int (* paramsno *) | `CoInductive of int (* paramsno *) diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli index b58b84b54..864db1800 100644 --- a/helm/ocaml/cic_omdoc/content.mli +++ b/helm/ocaml/cic_omdoc/content.mli @@ -25,7 +25,7 @@ type id = string;; type joint_recursion_kind = - [ `Recursive + [ `Recursive of int list (* decreasing arguments *) | `CoRecursive | `Inductive of int (* paramsno *) | `CoInductive of int (* paramsno *) diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 7641ad90e..815e0caaa 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -79,8 +79,45 @@ let proof2cic term2cic p = C.LetIn (C.Name s, proof2cic premise_env p, target) | None -> C.LetIn (C.Anonymous, proof2cic premise_env p, target)) - | `Joint ho -> - raise TO_DO + | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> + (match target with + C.Rel n -> + (match kind with + `Recursive l -> + let funs = + List.map2 + (fun n bo -> + match bo with + `Proof bo -> + (match + bo.Con.proof_conclude.Con.conclude_conclusion, + bo.Con.proof_name + with + Some ty, Some name -> + (name,n,term2cic ty,proof2cic premise_env bo) + | _,_ -> assert false) + | _ -> assert false) + l defs in + C.Fix (n, funs) + | `CoRecursive -> + let funs = + List.map + (function bo -> + match bo with + `Proof bo -> + (match + bo.Con.proof_conclude.Con.conclude_conclusion, + bo.Con.proof_name + with + Some ty, Some name -> + (name,term2cic ty,proof2cic premise_env bo) + | _,_ -> assert false) + | _ -> assert false) + defs in + C.CoFix (n, funs) + | _ -> (* no inductive types in local contexts *) + assert false) + | _ -> assert false) and conclude2cic premise_env conclude = let module C = Cic in @@ -100,6 +137,10 @@ let proof2cic term2cic p = else if conclude.Con.conclude_method = "Exact" then (match conclude.Con.conclude_args with [Con.Term t] -> term2cic t + | [Con.Premise prem] -> + (match prem.Con.premise_n with + None -> assert false + | Some n -> C.Rel n) | _ -> prerr_endline "3"; assert false) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with -- 2.39.2