X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=2c51fe7f80331d23c800fdab42fa9dc78e073bd2;hb=79d584e8f049226ec9cf68e9e06880ed0d95af51;hp=23d6447863a9f9335f101d240e1edfa51ca885dd;hpb=bdf989481462c1185c9cbbfdd4b31d13aa4352b3;p=helm.git diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 23d644786..2c51fe7f8 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -118,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; @@ -262,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 @@ -322,18 +326,59 @@ 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 + | _ -> assert false + 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 = function [] -> [],[] - | t::l1 -> + | (dep, t)::l1 -> let subproofs,args = aux l1 in if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then let new_subproof = acic2content - seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in + seed context metasenv + ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in let new_arg = K.Premise { K.premise_id = gen_id premise_prefix seed; @@ -357,7 +402,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 @@ -369,7 +414,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 @@ -395,11 +440,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 (infer_dependent ~headless context metasenv l)) with [p],args -> [{p with K.proof_name = None}], List.map @@ -411,13 +456,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 @@ -434,8 +479,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 @@ -459,11 +504,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 @@ -479,11 +526,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 @@ -494,29 +544,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 coercion - seed li ~ids_to_inner_types ~ids_to_inner_sorts + seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts with NotApplicable -> try rewrite - 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 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 + 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 @@ -572,12 +623,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 @@ -586,8 +638,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 @@ -601,7 +653,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 @@ -609,9 +661,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 @@ -646,9 +705,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; @@ -680,10 +746,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 @@ -730,8 +798,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 @@ -744,15 +812,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; @@ -762,21 +840,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 @@ -790,7 +868,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 @@ -800,12 +878,12 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = } | _ -> raise NotApplicable -and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts = +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 - CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && + CoercDb.is_a_coercion' (Deannotate.deannotate_term he) && !hide_coercions -> let rec last = function @@ -813,11 +891,14 @@ and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts = | [t] -> t | _::tl -> last tl in - acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl) + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl) | _ -> 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 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 @@ -830,7 +911,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 @@ -845,8 +927,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; @@ -856,9 +938,13 @@ 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 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 @@ -868,7 +954,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 @@ -890,13 +978,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 @@ -905,7 +993,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 @@ -918,11 +1006,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)] ;; @@ -1010,12 +1100,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, @@ -1025,7 +1117,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,