X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;h=69a1f632dcf3117138c5b421dcfb94f9999adb10;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=e72d466d537fb7724dd91daadbe99f0886dee46f;hpb=9e5abfcf937cb4fa85387cbd2b6503c2bf21a32c;p=helm.git diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index e72d466d5..69a1f632d 100644 --- a/components/acic_content/acic2content.ml +++ b/components/acic_content/acic2content.ml @@ -44,6 +44,8 @@ let conclude_prefix = "concl:";; let premise_prefix = "prem:";; let lemma_prefix = "lemma:";; +let hide_coercions = ref true;; + (* e se mettessi la conversione di BY nell'apply_context ? *) (* sarebbe carino avere l'invariante che la proof2pres generasse sempre prove con contesto vuoto *) @@ -116,7 +118,11 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= let module C2A = Cic2acic in (* atomic terms are never lifted, according to my policy *) function - C.ARel (id,_,_,_) -> false + C.ARel (id,_,_,_) -> + (try + ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; + true; + with Not_found -> false) | C.AVar (id,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; @@ -260,7 +266,7 @@ let generate_exact seed t id name ~ids_to_inner_types = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; K.conclude_method = "Exact"; - K.conclude_args = [K.Term t]; + K.conclude_args = [K.Term (false, t)]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized with Not_found -> None @@ -320,18 +326,62 @@ let build_decl_item seed id n s ~ids_to_inner_sorts = } ;; -let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts = +let infer_dependent ~headless context metasenv = function + | [] -> assert false + | [t] -> [false, t] + | he::tl as l -> + if headless then + List.map (function s -> false,s) l + else + try + let hety,_ = + CicTypeChecker.type_of_aux' + metasenv context (Deannotate.deannotate_term he) + CicUniv.oblivion_ugraph + in + let fstorder t = + match CicReduction.whd context t with + | Cic.Prod _ -> false + | _ -> true + in + let rec dummify_last_tgt t = + match CicReduction.whd context t with + | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt) + | _ -> Cic.Implicit None + in + let rec aux ty = function + | [] -> [] + | t::tl -> + match + FreshNamesGenerator.clean_dummy_dependent_types + (dummify_last_tgt ty) + with + | Cic.Prod (n,src,tgt) -> + (n <> Cic.Anonymous && fstorder src, t) :: + aux (CicSubstitution.subst + (Deannotate.deannotate_term t) tgt) tl + | _ -> List.map (fun s -> false,s) (t::tl) + in + (false, he) :: aux hety tl + with CicTypeChecker.TypeCheckerFailure _ -> assert false +;; + +let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts = let module C = Cic in let module K = Content in - let rec aux = + let rec aux n = function [] -> [],[] - | t::l1 -> - let subproofs,args = aux l1 in - if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then + | (dep, t)::l1 -> + let need_lifting = + test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in + let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in + if need_lifting then let new_subproof = acic2content - seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in + seed context metasenv + ~name:("H" ^ string_of_int n) ~ids_to_inner_types + ~ids_to_inner_sorts t in let new_arg = K.Premise { K.premise_id = gen_id premise_prefix seed; @@ -355,7 +405,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts K.premise_binder = Some b; K.premise_n = Some n } - else (K.Term t) + else (K.Term (dep,t)) | C.AConst(id,uri,[]) -> let sort = (try @@ -367,7 +417,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts K.lemma_name = UriManager.name_of_uri uri; K.lemma_uri = UriManager.string_of_uri uri } - else (K.Term t) + else (K.Term (dep,t)) | C.AMutConstruct(id,uri,tyno,consno,[]) -> let sort = (try @@ -393,11 +443,11 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")" } - else (K.Term t) - | _ -> (K.Term t)) in + else (K.Term (dep,t)) + | _ -> (K.Term (dep,t))) in subproofs,hd::args in - match (aux l) with + match (aux 1 (infer_dependent ~headless context metasenv l)) with [p],args -> [{p with K.proof_name = None}], List.map @@ -409,13 +459,13 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts and -build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = +build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in if sort = `Prop then (let p = - (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) + (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) in `Proof p;) else @@ -432,8 +482,8 @@ 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 ~ids_to_inner_sorts ~ids_to_inner_types t = - let rec aux ?name t = +and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t = + let rec aux ?name context t = let module C = Cic in let module K = Content in let module C2A = Cic2acic in @@ -457,11 +507,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = | 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.ACast (id,v,t) -> aux context 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 in + let proof = + aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t + in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with @@ -477,11 +529,14 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = } in generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types - else raise Not_a_proof + 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 = (* XXX TIPAMI!!! *) + aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t + in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then match proof.K.proof_conclude.K.conclude_args with @@ -492,26 +547,30 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = { proof' with K.proof_name = None; K.proof_context = - ((build_def_item seed id n s ids_to_inner_sorts + ((build_def_item seed context metasenv (get_id s) 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 - else raise Not_a_proof + else + raise Not_a_proof | C.AAppl (id,li) -> - (try rewrite - seed name id li ~ids_to_inner_types ~ids_to_inner_sorts + (try coercion + seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts + with NotApplicable -> + try rewrite + seed context metasenv 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 + seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> - try transitivity - seed name id li ~ids_to_inner_types ~ids_to_inner_sorts + try transitivity + seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> let subproofs, args = build_subproofs_and_args - seed li ~ids_to_inner_types ~ids_to_inner_sorts in + seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in (* let args_to_lift = List.filter (test_for_lifting ~ids_to_inner_types) li in @@ -567,12 +626,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = let pp = let build_proof p (name,arity) = let rec make_context_and_body c p n = - if n = 0 then c,(aux p) + if n = 0 then c,(aux context p) else (match p with Cic.ALambda(idl,vname,s1,t1) -> let ce = - build_decl_item seed idl vname s1 ~ids_to_inner_sorts in + build_decl_item + seed idl vname s1 ~ids_to_inner_sorts in make_context_and_body (ce::c) t1 (n-1) | _ -> assert false) in let context,body = make_context_and_body [] p arity in @@ -581,8 +641,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = List.map2 build_proof patterns name_and_arities in let context,term = (match - build_subproofs_and_args - seed ~ids_to_inner_types ~ids_to_inner_sorts [te] + build_subproofs_and_args ~headless:true + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te] with l,[t] -> l,t | _ -> assert false) in @@ -596,7 +656,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = 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.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized @@ -604,9 +664,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = } } | C.AFix (id, no, funs) -> + let context' = + List.fold_left + (fun ctx (_,n,_,ty,_) -> + let ty = Deannotate.deannotate_term ty in + Some (Cic.Name n,Cic.Decl ty) :: ctx) + [] funs @ context + in let proofs = List.map - (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in + (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in let fun_name = List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no in @@ -641,9 +708,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = } } | C.ACoFix (id,no,funs) -> + let context' = + List.fold_left + (fun ctx (_,n,ty,_) -> + let ty = Deannotate.deannotate_term ty in + Some (Cic.Name n,Cic.Decl ty) :: ctx) + [] funs @ context + in let proofs = List.map - (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in + (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in let jo = { K.joint_id = gen_id joint_prefix seed; K.joint_kind = `CoRecursive; @@ -675,10 +749,12 @@ and acic2content seed ?name ~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 t +in aux ?name context t -and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = - let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in +and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = + let aux context ?name = + acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + in let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -725,8 +801,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let args_for_cases, other_args = split no_constructors tail_args in let subproofs,other_method_args = - build_subproofs_and_args seed other_args - ~ids_to_inner_types ~ids_to_inner_sorts in + build_subproofs_and_args ~headless:true seed context metasenv + other_args ~ids_to_inner_types ~ids_to_inner_sorts in let method_args= let rec build_method_args = function @@ -739,15 +815,25 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let hdarg = if sortarg = `Prop then let (co,bo) = - let rec bc = + let rec bc context = function Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) -> + let context' = + Some (n,Cic.Decl(Deannotate.deannotate_term s1)) + ::context + in let ce = build_decl_item seed idl n s1 ~ids_to_inner_sorts in if (occur ind_uri s) then ( match t1 with Cic.ALambda(id2,n2,s2,t2) -> + let context'' = + Some + (n2,Cic.Decl + (Deannotate.deannotate_term s2)) + ::context' + in let inductive_hyp = `Hypothesis { K.dec_name = name_of n2; @@ -757,21 +843,21 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.dec_aref = id2; K.dec_type = s2 } in - let (context,body) = bc (t,t2) in + let (context,body) = bc context'' (t,t2) in (ce::inductive_hyp::context,body) | _ -> assert false) else ( - let (context,body) = bc (t,t1) in + let (context,body) = bc context' (t,t1) in (ce::context,body)) - | _ , t -> ([],aux t) in - bc (ty,arg) in + | _ , t -> ([],aux context t) in + bc context (ty,arg) in K.ArgProof { bo with K.proof_name = Some name; K.proof_context = co; }; - else (K.Term arg) in + else (K.Term (false,arg)) in hdarg::(build_method_args (tlc,tla)) | _ -> assert false in build_method_args (constructors1,args_for_cases) in @@ -785,7 +871,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.conclude_method = method_name; K.conclude_args = K.Aux (string_of_int no_constructors) - ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))) + ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))) ::method_args@other_method_args; K.conclude_conclusion = try Some @@ -795,8 +881,27 @@ 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 = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in +and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts = + match li with + | ((Cic.AConst _) as he)::tl + | ((Cic.AMutInd _) as he)::tl + | ((Cic.AMutConstruct _) as he)::tl when + CoercDb.is_a_coercion' (Deannotate.deannotate_term he) && + !hide_coercions -> + let rec last = + function + [] -> assert false + | [t] -> t + | _::tl -> last tl + in + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl) + | _ -> raise NotApplicable + +and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts = + let aux context ?name = + acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + in let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -809,7 +914,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let subproofs,arg = (match build_subproofs_and_args - seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3] + seed context metasenv + ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3] with l,[p] -> l,p | _,_ -> assert false) in @@ -824,8 +930,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let asort = (try (Hashtbl.find ids_to_inner_sorts aid) with Not_found -> `Type (CicUniv.fresh())) in if asort = `Prop then - K.ArgProof (aux a) - else K.Term a in + K.ArgProof (aux context a) + else K.Term (false,a) in hd::(ma_aux (n-1) tl) in (ma_aux 3 args) in { K.proof_name = name; @@ -835,9 +941,14 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.proof_conclude = { K.conclude_id = gen_id conclude_prefix seed; K.conclude_aref = id; - K.conclude_method = "Rewrite"; + K.conclude_method = + if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI + || LibraryObjects.is_eq_ind_URI uri then + "RewriteLR" + else + "RewriteRL"; K.conclude_args = - K.Term (C.AConst (sid,uri,exp_named_subst))::method_args; + K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized @@ -847,7 +958,9 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = else raise NotApplicable | _ -> raise NotApplicable -and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = +and transitivity + seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts += let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -869,13 +982,13 @@ and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.conclude_aref = id; K.conclude_method = "Eq_chain"; K.conclude_args = - K.Term t1:: + K.Term (false,t1):: (transitivity_aux - seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@ - [K.Term t2]@ + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1) + @ [K.Term (false,t2)]@ (transitivity_aux - seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@ - [K.Term t3]; + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2) + @ [K.Term (false,t3)]; K.conclude_conclusion = try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized @@ -884,7 +997,7 @@ and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = } | _ -> raise NotApplicable -and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t = +and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t = let module C2A = Cic2acic in let module K = Content in let module C = Cic in @@ -897,11 +1010,13 @@ and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t = | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2 | _ -> raise NotApplicable in - (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1) - @[K.Term t2] - @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2) + (transitivity_aux + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1) + @[K.Term (false,t2)] + @(transitivity_aux + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2) | _ -> [K.ArgProof - (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)] + (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)] ;; @@ -989,12 +1104,14 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = (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 + build_def_item + seed [] (Deannotate.deannotate_conjectures conjectures) + (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (_,_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Const,ty, - build_def_item seed (get_id bo) (C.Name n) bo + 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 object_prefix seed, params, None, @@ -1004,7 +1121,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = | C.AVariable (_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Var,ty, - build_def_item seed (get_id bo) (C.Name n) bo + 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 object_prefix seed, params, None,