From c43f710f5e23e940114b1623329f650814e783af Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Jul 2003 17:03:37 +0000 Subject: [PATCH] The Aux argument of conclude is now of type string (used to be int). Case Fixed. --- helm/ocaml/cic_omdoc/cic2content.ml | 82 +++++++++++++++-------------- helm/ocaml/cic_omdoc/content.ml | 2 +- helm/ocaml/cic_omdoc/content.mli | 2 +- helm/ocaml/cic_omdoc/content2cic.ml | 21 +++++++- helm/ocaml/cic_omdoc/contentPp.ml | 2 +- 5 files changed, 66 insertions(+), 43 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 2749708d2..149fd90ec 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -465,46 +465,50 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> + let inductive_types = + (match CicEnvironment.get_obj uri with + Cic.Constant _ -> assert false + | Cic.Variable _ -> assert false + | Cic.CurrentProof _ -> assert false + | Cic.InductiveDefinition (l,_,_) -> l + ) in + let (_,_,_,constructors) = List.nth inductive_types typeno in let teid = get_id te 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 Not_found -> None) - with - Some tety -> (* we must lift up the argument *) + let pp = List.map2 + (fun p (name,_) -> (K.ArgProof (aux ~name p))) + patterns constructors in + let apply_context,term = + (match + (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized + with Not_found -> None) + with + Some tety -> let p = (aux te) in - { 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 Not_found -> None - } - } - | None -> - { 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 Not_found -> None - } - } - ) + (flat seed p, + 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 + }) + | None -> [],K.Term te) in + { K.proof_name = name; + K.proof_id = gen_id seed; + K.proof_context = []; + K.proof_apply_context = apply_context; + K.proof_conclude = + { K.conclude_id = gen_id seed; + K.conclude_aref = id; + K.conclude_method = "Case"; + K.conclude_args = + (K.Aux (UriManager.string_of_uri uri)):: + (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp; + 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 @@ -696,7 +700,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts = K.conclude_aref = id; K.conclude_method = "ByInduction"; K.conclude_args = - K.Aux no_constructors + K.Aux (string_of_int no_constructors) ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) ::method_args@other_method_args; K.conclude_conclusion = diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml index 2f956d7d1..a09e25cf2 100644 --- a/helm/ocaml/cic_omdoc/content.ml +++ b/helm/ocaml/cic_omdoc/content.ml @@ -121,7 +121,7 @@ and 'term conclude_item = } and 'term arg = - Aux of int + Aux of string | Premise of premise | Term of 'term | ArgProof of 'term proof diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli index 864db1800..813a31053 100644 --- a/helm/ocaml/cic_omdoc/content.mli +++ b/helm/ocaml/cic_omdoc/content.mli @@ -112,7 +112,7 @@ and 'term conclude_item = } and 'term arg = - Aux of int + Aux of string | Premise of premise | Term of 'term | ArgProof of 'term proof diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 1d4dcd1ee..d25d79425 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -167,10 +167,29 @@ let proof2cic deannotate p = let cargs = args2cic premise_env args in C.Appl (C.Const(uri,subst)::cargs) | _ -> prerr_endline "6"; assert false) + else if (conclude.Con.conclude_method = "Case") then + (match conclude.Con.conclude_args with + Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns -> + C.MutCase + (UriManager.uri_of_string uri, + int_of_string notype, deannotate ty, + List.assoc prem.Con.premise_xref premise_env, + List.map + (function + Con.ArgProof p -> proof2cic [] p + | _ -> prerr_endline "7a"; assert false) patterns) + | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase + (UriManager.uri_of_string uri, + int_of_string notype, deannotate ty, deannotate te, + List.map + (function + (Con.ArgProof p) -> proof2cic [] p + | _ -> prerr_endline "7a"; assert false) patterns) + | _ -> (prerr_endline "7"; assert false)) else if (conclude.Con.conclude_method = "Apply") then let cargs = (args2cic premise_env conclude.Con.conclude_args) in C.Appl cargs - else (prerr_endline "7"; assert false) + else (prerr_endline "8"; assert false) and args2cic premise_env l = List.map (arg2cic premise_env) l diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml index 3bc8bb306..b51cba99d 100644 --- a/helm/ocaml/cic_omdoc/contentPp.ml +++ b/helm/ocaml/cic_omdoc/contentPp.ml @@ -130,7 +130,7 @@ and pargs args indent = and parg indent = let module Con = Content in function - Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr + Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ n);flush stderr | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr | Con.Term t -> prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t))); -- 2.39.2