--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(**************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Andrea Asperti <asperti@cs.unibo.it> *)
+(* 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
+generasse sempre prove con contesto vuoto *)
+
+let gen_id seed =
+ let res = "p" ^ string_of_int !seed in
+ incr seed ;
+ res
+;;
+
+let name_of = function
+ Cic.Anonymous -> None
+ | Cic.Name b -> Some b;;
+
+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 *)
+
+let rec occur uri =
+ let module C = Cic in
+ function
+ C.Rel _ -> false
+ | C.Var _ -> false
+ | C.Meta _ -> false
+ | C.Sort _ -> false
+ | C.Implicit -> raise NotImplemented
+ | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
+ | C.Cast (te,ty) -> (occur uri te)
+ | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
+ | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
+ | C.Appl l ->
+ List.fold_left
+ (fun b a ->
+ if b then b
+ else (occur uri a)) false l
+ | C.Const (_,_) -> false
+ | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
+ | C.MutConstruct (_,_,_,_) -> false
+ | C.MutCase _ -> false (* presuming too much?? *)
+ | C.Fix _ -> false (* presuming too much?? *)
+ | C.CoFix (_,_) -> false (* presuming too much?? *)
+;;
+
+let get_id =
+ let module C = Cic in
+ function
+ C.ARel (id,_,_,_) -> id
+ | C.AVar (id,_,_) -> id
+ | C.AMeta (id,_,_) -> id
+ | C.ASort (id,_) -> id
+ | C.AImplicit _ -> raise NotImplemented
+ | C.AProd (id,_,_,_) -> id
+ | C.ACast (id,_,_) -> id
+ | C.ALambda (id,_,_,_) -> id
+ | C.ALetIn (id,_,_,_) -> id
+ | C.AAppl (id,_) -> id
+ | C.AConst (id,_,_) -> id
+ | C.AMutInd (id,_,_,_) -> id
+ | C.AMutConstruct (id,_,_,_,_) -> id
+ | C.AMutCase (id,_,_,_,_,_) -> id
+ | C.AFix (id,_,_) -> id
+ | C.ACoFix (id,_,_) -> id
+;;
+
+let test_for_lifting ~ids_to_inner_types =
+ let module C = Cic in
+ let module C2A = Cic2acic in
+ (* atomic terms are never lifted, according to my policy *)
+ function
+ C.ARel (id,_,_,_) -> false
+ | C.AVar (id,_,_) -> false
+ | C.AMeta (id,_,_) -> false
+ | C.ASort (id,_) -> false
+ | C.AImplicit _ -> raise NotImplemented
+ | C.AProd (id,_,_,_) -> false
+ | C.ACast (id,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.ALambda (id,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.ALetIn (id,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.AAppl (id,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.AConst (id,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.AMutInd (id,_,_,_) -> false
+ | C.AMutConstruct (id,_,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ (* oppure: false *)
+ | C.AMutCase (id,_,_,_,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.AFix (id,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+ | C.ACoFix (id,_,_) ->
+ (try
+ ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+ true;
+ with notfound -> false)
+;;
+
+let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
+ let module C = Cic in
+ let rec aux l subrpoofs =
+ match l with
+ [] -> []
+ | t::l1 ->
+ if (test_for_lifting t ~ids_to_inner_types) then
+ (match subproofs with
+ [] -> 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
+ }
+ in new_arg::(aux l1 tl))
+ else
+ let hd =
+ (match t with
+ C.ARel (idr,idref,n,b) ->
+ let sort =
+ (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
+ }
+ else (Term t)
+ | _ -> (Term t)) in
+ hd::(aux l1 subproofs)
+ in aux l subproofs
+;;
+
+(* transform a proof p into a proof list, concatenating the last
+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]
+ 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;
+ } in
+ p.proof_apply_context@[p1]
+ else
+ [p]
+;;
+
+let rec serialize seed =
+ function
+ [] -> []
+ | p::tl -> (flat seed p)@(serialize seed tl);;
+
+(* 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 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
+ };
+ }
+ 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
+ }
+ ];
+ 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 =
+ try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with notfound -> None
+ };
+ }
+;;
+
+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 =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with notfound ->
+ (match inner_proof.proof_conclude.conclude_conclusion with
+ None -> None
+ | Some t ->
+ if is_intro then Some (C.AProd ("gen"^id,n,s,t))
+ else Some (C.ALetIn ("gen"^id,n,s,t)))
+ };
+ }
+;;
+
+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
+ { dec_name = name_of n;
+ dec_id = gen_id seed;
+ dec_inductive = false;
+ dec_aref = id;
+ dec_type = s
+ }
+ else
+ Declaration
+ { dec_name = name_of n;
+ dec_id = gen_id seed;
+ dec_inductive = false;
+ dec_aref = id;
+ dec_type = s
+ }
+;;
+
+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)
+ else
+ Definition
+ { def_name = name_of n;
+ def_id = gen_id seed;
+ def_aref = id;
+ def_term = t
+ }
+
+(* the following function must be called with an object of sort
+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 =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+ let module C2A = Cic2acic in
+ let t1 =
+ match t with
+ C.ARel (id,idref,n,b) as t ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ if sort = "Prop" then
+ generate_exact seed t id name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.AVar (id,uri,exp_named_subst) as t ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ if sort = "Prop" then
+ generate_exact seed t id name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.AMeta (id,n,l) as t ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ if sort = "Prop" then
+ generate_exact seed t id name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.ASort (id,s) -> raise Not_a_proof
+ | C.AImplicit _ -> raise NotImplemented
+ | C.AProd (_,_,_,_) -> raise Not_a_proof
+ | C.ACast (id,v,t) -> aux v
+ | 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' =
+ if proof.proof_conclude.conclude_method = "Intros+LetTac" then
+ match proof.proof_conclude.conclude_args with
+ [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 =
+ (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;
+ }
+ in
+ generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.ALetIn (id,n,s,t) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ 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
+ | _ -> 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;
+ }
+ in
+ generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.AAppl (id,li) ->
+ (try rewrite
+ seed name id li ids_to_inner_types ids_to_inner_sorts
+ with NotApplicable ->
+ try inductive
+ seed name id li ids_to_inner_types ids_to_inner_sorts
+ with NotApplicable ->
+ let args_to_lift =
+ List.filter (test_for_lifting ~ids_to_inner_types) li in
+ let subproofs =
+ match args_to_lift with
+ [_] -> List.map aux args_to_lift
+ | _ -> 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 =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with notfound -> None
+ };
+ })
+ | C.AConst (id,uri,exp_named_subst) as t ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ if sort = "Prop" then
+ generate_exact seed t id name ~ids_to_inner_types
+ else raise Not_a_proof
+ | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
+ | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ if sort = "Prop" then
+ generate_exact seed t id name ~ids_to_inner_types
+ 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
+ (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 =
+ 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 =
+ 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;
+ }
+ ];
+ 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
+ }
+ 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;
+ }
+ ];
+ 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;
+ }
+ ];
+ 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
+ }
+ 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;
+ }
+ ];
+ conclude_conclusion =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with notfound -> None
+ };
+ }
+ in
+ let id = get_id t in
+ generate_conversion seed false id t1 ~ids_to_inner_types
+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 C = Cic in
+ match li with
+ C.AConst (idc,uri,exp_named_subst)::args ->
+ let uri_str = UriManager.string_of_uri uri in
+ let suffix = Str.regexp_string "_ind.con" in
+ let len = String.length uri_str in
+ let n = (try (Str.search_backward suffix uri_str len)
+ with Not_found -> -1) in
+ if n<0 then raise NotApplicable
+ else
+ let prefix = String.sub uri_str 0 n in
+ let ind_str = (prefix ^ ".ind") in
+ let ind_uri = UriManager.uri_of_string ind_str in
+ let inductive_types,noparams =
+ (match CicEnvironment.get_obj ind_uri with
+ Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,n) -> (l,n)
+ ) in
+ let rec split n l =
+ if n = 0 then ([],l) else
+ let p,a = split (n-1) (List.tl l) in
+ ((List.hd l::p),a) in
+ let params_and_IP,tail_args = split (noparams+1) args in
+ let constructors =
+ (match inductive_types with
+ [(_,_,_,l)] -> l
+ | _ -> raise NotApplicable) (* don't care for mutual ind *) in
+ let constructors1 =
+ let rec clean_up n t =
+ if n = 0 then t else
+ (match t with
+ (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
+ | _ -> assert false) in
+ List.map (clean_up noparams) constructors in
+ let no_constructors= List.length constructors in
+ let args_for_cases, other_args =
+ split no_constructors tail_args in
+ let args_to_lift =
+ List.filter (test_for_lifting ~ids_to_inner_types) other_args in
+ let subproofs =
+ match args_to_lift with
+ [_] -> List.map aux args_to_lift
+ | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
+ prerr_endline "****** end subproofs *******"; flush stderr;
+ let other_method_args =
+ build_args seed other_args subproofs
+ ~ids_to_inner_types ~ids_to_inner_sorts in
+(*
+ let rparams,inductive_arg =
+ let rec aux =
+ function
+ [] -> assert false
+ | [ia] -> [],ia
+ | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
+ aux other_method_args in
+*)
+ prerr_endline "****** end other *******"; flush stderr;
+ let method_args=
+ let rec build_method_args =
+ function
+ [],_-> [] (* extra args are ignored ???? *)
+ | (name,ty)::tlc,arg::tla ->
+ let idarg = get_id arg in
+ let sortarg =
+ (try (Hashtbl.find ids_to_inner_sorts idarg)
+ with Not_found -> "Type") in
+ let hdarg =
+ if sortarg = "Prop" then
+ let (co,bo) =
+ let rec bc =
+ function
+ Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
+ let ce =
+ build_decl_item
+ seed idl n s1 ~ids_to_inner_sorts in
+ if (occur ind_uri s) then
+ ( prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
+ 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
+ } in
+ let (context,body) = bc (t,t2) in
+ (ce::inductive_hyp::context,body)
+ | _ -> 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;
+ };
+ 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 =
+ { 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))
+ ::method_args@other_method_args;
+ 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 C = Cic in
+ match li with
+ C.AConst (sid,uri,exp_named_subst)::args ->
+ let uri_str = UriManager.string_of_uri uri in
+ if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
+ uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then
+ let subproof = aux (List.nth args 3) in
+ let method_args =
+ let rec ma_aux n = function
+ [] -> []
+ | 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
+ }
+ 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
+ (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 =
+ try Some
+ (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+ with notfound -> None
+ };
+ }
+ else raise NotApplicable
+ | _ -> raise NotApplicable
+;;
+
+let 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)
+
+(*
+and 'term cinductiveType =
+ id * string * bool * 'term * (* typename, inductive, arity *)
+ 'term cconstructor list (* constructors *)
+
+and 'term cconstructor =
+ string * 'term
+*)
+
projects / helm.git / blobdiff