X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=c8ff783c3eafab71d645e5bc13005682259a62ae;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=57b8502bb3ac4e35029178490e0726766b94f1de;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index 57b8502bb..c8ff783c3 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/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 *) @@ -76,7 +78,7 @@ let rec occur uri = | 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.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t) | C.Appl l -> List.fold_left (fun b a -> @@ -101,7 +103,7 @@ let get_id = | C.AProd (id,_,_,_) -> id | C.ACast (id,_,_) -> id | C.ALambda (id,_,_,_) -> id - | C.ALetIn (id,_,_,_) -> id + | C.ALetIn (id,_,_,_,_) -> id | C.AAppl (id,_) -> id | C.AConst (id,_,_) -> id | C.AMutInd (id,_,_,_) -> id @@ -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; @@ -139,7 +145,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; with Not_found -> false) - | C.ALetIn (id,_,_,_) -> + | C.ALetIn (id,_,_,_,_) -> (try ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized; true; @@ -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 @@ -268,7 +274,7 @@ let generate_exact seed t id name ~ids_to_inner_types = } ;; -let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types = +let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types = let module C2A = Cic2acic in let module C = Cic in let module K = Content in @@ -288,8 +294,9 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_ (match inner_proof.K.proof_conclude.K.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))) + match ty with + None -> Some (C.AProd ("gen"^id,n,s,t)) + | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t))) }; } ;; @@ -320,18 +327,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 +406,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 +418,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 @@ -376,7 +427,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts if sort = `Prop then let inductive_types = (let o,_ = - CicEnvironment.get_obj CicUniv.empty_ugraph uri + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with | Cic.InductiveDefinition (l,_,_,_) -> l @@ -393,11 +444,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 +460,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 ty ~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 @@ -423,7 +474,8 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = { K.def_name = name_of n; K.def_id = gen_id definition_prefix seed; K.def_aref = id; - K.def_term = t + K.def_term = t; + K.def_type = ty } with Not_found -> assert false @@ -432,8 +484,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 +509,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 @@ -476,12 +530,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = proof'.K.proof_context } 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) -> + generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types + else + raise Not_a_proof + | C.ALetIn (id,n,s,ty,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.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::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,23 +551,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 ty 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 + generate_intros_let_tac seed id n s (Some ty) 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 + (try coercion + seed context metasenv id 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 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 @@ -546,7 +612,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let inductive_types,noparams = - (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false @@ -564,12 +630,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 @@ -578,8 +645,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 @@ -593,7 +660,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 @@ -601,9 +668,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 @@ -638,9 +712,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; @@ -672,10 +753,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 @@ -697,7 +780,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let ind_str = (prefix ^ ".ind") in let ind_uri = UriManager.uri_of_string ind_str in let inductive_types,noparams = - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in + (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in match o with | Cic.InductiveDefinition (l,_,n,_) -> (l,n) | _ -> assert false @@ -722,8 +805,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 @@ -736,15 +819,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; @@ -754,21 +847,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 @@ -782,7 +875,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 @@ -792,8 +885,37 @@ 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 id 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 + (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with + | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl) + && !hide_coercions -> + let cpos,sats = + match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with + | None -> assert false + | Some (_,_,_,sats,cpos) -> cpos, sats + in + let x = List.nth tl cpos in + let _,rest = + try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] + in + if rest = [] then + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + x + else + acic2content + seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts + (Cic.AAppl (id,x::rest)) + | _ -> 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 @@ -806,7 +928,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 @@ -821,8 +944,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; @@ -832,9 +955,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 @@ -843,8 +971,70 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = } else raise NotApplicable | _ -> raise NotApplicable + +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 + match li with + | C.AConst (sid,uri,exp_named_subst)::args + when LibraryObjects.is_trans_eq_URI uri -> + let exp_args = List.map snd exp_named_subst in + let t1,t2,t3,p1,p2 = + match exp_args@args with + | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2 + | _ -> raise NotApplicable + in + { K.proof_name = name; + K.proof_id = gen_id proof_prefix seed; + K.proof_context = []; + K.proof_apply_context = []; + K.proof_conclude = + { K.conclude_id = gen_id conclude_prefix seed; + K.conclude_aref = id; + K.conclude_method = "Eq_chain"; + K.conclude_args = + K.Term (false,t1):: + (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.Term (false,t3)]; + K.conclude_conclusion = + try Some + (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized + with Not_found -> None + } + } + | _ -> raise NotApplicable + +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 + match t with + | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args) + when LibraryObjects.is_trans_eq_URI uri -> + let exp_args = List.map snd exp_named_subst in + let t1,t2,t3,p1,p2 = + match exp_args@args with + | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2 + | _ -> raise NotApplicable + in + (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 context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)] + ;; + let map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty) = @@ -864,7 +1054,7 @@ let map_conjectures K.dec_aref = get_id t; K.dec_type = t }) - | (id,Some (name,Cic.ADef t)) -> + | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) @@ -872,7 +1062,8 @@ let map_conjectures { K.def_name = name_of name; K.def_id = gen_id definition_prefix seed; K.def_aref = get_id t; - K.def_term = t + K.def_term = t; + K.def_type = ty }) ) context in @@ -900,7 +1091,7 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) = K.dec_aref = get_id t; K.dec_type = t }) - | (id,Some (name,Cic.ADef t)) -> + | (id,Some (name,Cic.ADef (t,ty))) -> Some (* We should call build_def_item, but we have not computed *) (* the inner-types ==> we always produce a declaration *) @@ -908,7 +1099,8 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) = { K.def_name = name_of name; K.def_id = id; K.def_aref = get_id t; - K.def_term = t + K.def_term = t; + K.def_type = ty }) ) context in @@ -928,12 +1120,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 ty ~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 ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AConstant (id,_,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, @@ -943,7 +1137,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 ty ~ids_to_inner_sorts ~ids_to_inner_types)) | C.AVariable (id,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None,