From: Enrico Tassi Date: Wed, 13 Jun 2007 13:01:32 +0000 (+0000) Subject: many changes: X-Git-Tag: make_still_working~6248 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=66929b8edb58d468a134b648466f3e9c45ba5c0e;p=helm.git many changes: 1) fixed many bugs and added support for implicit detection in cic -> declarative 2) added a tactic to find a proof rewriting n times with a given universe used instead of auto_paramodulation in the declarative language (here you know that 1 rewriting step with that lemma is enough) 3) added ESCAPE to sql queries using LIKE, to make sqlite and mysql compatible --- diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml index eddee38b1..99bab2de4 100644 --- a/helm/software/components/acic_content/acic2content.ml +++ b/helm/software/components/acic_content/acic2content.ml @@ -262,7 +262,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 +322,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 +398,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 +410,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 +436,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 +452,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 +475,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 +500,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 @@ -484,7 +527,9 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = | 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 @@ -495,7 +540,7 @@ 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 (get_id s) 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; } @@ -505,20 +550,20 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = 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 @@ -574,12 +619,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 @@ -588,8 +634,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 @@ -603,7 +649,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 @@ -611,9 +657,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 @@ -648,9 +701,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; @@ -682,10 +742,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 @@ -732,8 +794,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 @@ -746,15 +808,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; @@ -764,21 +836,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 @@ -792,7 +864,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 @@ -802,7 +874,7 @@ 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 @@ -815,11 +887,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 @@ -832,7 +907,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 @@ -847,8 +923,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; @@ -860,7 +936,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.conclude_aref = id; K.conclude_method = "Rewrite"; 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 @@ -870,7 +946,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 @@ -892,13 +970,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 @@ -907,7 +985,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 @@ -920,11 +998,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)] ;; @@ -1012,12 +1092,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, @@ -1027,7 +1109,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, diff --git a/helm/software/components/acic_content/content.ml b/helm/software/components/acic_content/content.ml index 22733dcaa..c8b22f497 100644 --- a/helm/software/components/acic_content/content.ml +++ b/helm/software/components/acic_content/content.ml @@ -127,7 +127,7 @@ and 'term arg = Aux of string | Premise of premise | Lemma of lemma - | Term of 'term + | Term of bool * 'term | ArgProof of 'term proof | ArgMethod of string (* ???? *) diff --git a/helm/software/components/acic_content/content.mli b/helm/software/components/acic_content/content.mli index c1122b8f2..546000330 100644 --- a/helm/software/components/acic_content/content.mli +++ b/helm/software/components/acic_content/content.mli @@ -116,7 +116,7 @@ and 'term arg = Aux of string | Premise of premise | Lemma of lemma - | Term of 'term + | Term of bool * 'term (* inferrable, term *) | ArgProof of 'term proof | ArgMethod of string (* ???? *) diff --git a/helm/software/components/acic_content/content2cic.ml b/helm/software/components/acic_content/content2cic.ml index 9acea81fa..dcec61d84 100644 --- a/helm/software/components/acic_content/content2cic.ml +++ b/helm/software/components/acic_content/content2cic.ml @@ -141,7 +141,7 @@ let proof2cic deannotate p = | _ -> prerr_endline "2"; assert false) else if conclude.Con.conclude_method = "Exact" then (match conclude.Con.conclude_args with - [Con.Term t] -> deannotate t + [Con.Term (_,t)] -> deannotate t | [Con.Premise prem] -> (match prem.Con.premise_n with None -> assert false @@ -156,7 +156,7 @@ let proof2cic deannotate p = conclude.Con.conclude_method = "Exists" || conclude.Con.conclude_method = "FalseInd") then (match (List.tl conclude.Con.conclude_args) with - Con.Term (C.AAppl ( + Con.Term (_,C.AAppl ( id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args -> let subst = List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in @@ -166,7 +166,7 @@ let proof2cic deannotate p = | _ -> prerr_endline "5"; assert false) else if (conclude.Con.conclude_method = "Rewrite") then (match conclude.Con.conclude_args with - Con.Term (C.AConst (sid,uri,exp_named_subst))::args -> + Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args -> let subst = List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in let cargs = args2cic premise_env args in @@ -174,7 +174,7 @@ let proof2cic deannotate p = | _ -> 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 -> + 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, @@ -183,7 +183,7 @@ let proof2cic deannotate p = (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 + | 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 @@ -214,7 +214,7 @@ let proof2cic deannotate p = raise Not_found)) | Con.Lemma lemma -> CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri) - | Con.Term t -> deannotate t + | Con.Term (_,t) -> deannotate t | Con.ArgProof p -> proof2cic [] p (* empty! *) | Con.ArgMethod s -> raise TO_DO diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml index f04f5aa10..b7c7d1113 100644 --- a/helm/software/components/cic/deannotate.ml +++ b/helm/software/components/cic/deannotate.ml @@ -89,6 +89,22 @@ let deannotate_inductiveType (_, name, isinductive, arity, cons) = List.map (fun (id,ty) -> (id,deannotate_term ty)) cons) ;; +let deannotate_conjectures = + let module C = Cic in + List.map + (function + (_,id,acontext,con) -> + let context = + List.map + (function + | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None))) + | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at))) + | _,None -> None) + acontext + in + (id,context,deannotate_term con)) +;; + let deannotate_obj = let module C = Cic in function @@ -103,21 +119,7 @@ let deannotate_obj = | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) -> C.CurrentProof ( name, - List.map - (function - (_,id,acontext,con) -> - let context = - List.map - (function - _,Some (n,(C.ADef at)) -> - Some (n,(C.Def ((deannotate_term at),None))) - | _,Some (n,(C.ADecl at)) -> - Some (n,(C.Decl (deannotate_term at))) - | _,None -> None - ) acontext - in - (id,context,deannotate_term con) - ) conjs, + deannotate_conjectures conjs, deannotate_term bo,deannotate_term ty, params, attrs ) | C.AInductiveDefinition (_, tys, params, parno, attrs) -> diff --git a/helm/software/components/cic/deannotate.mli b/helm/software/components/cic/deannotate.mli index 89b18d2d6..1e29b5b64 100644 --- a/helm/software/components/cic/deannotate.mli +++ b/helm/software/components/cic/deannotate.mli @@ -33,4 +33,5 @@ (******************************************************************************) val deannotate_term : Cic.annterm -> Cic.term +val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv val deannotate_obj : Cic.annobj -> Cic.obj diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 749731bda..f157af406 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -30,6 +30,7 @@ open Printf exception Error of int * int * string let regexp number = xml_digit+ +let regexp utf8_blank = " " | "\n" | "\t" | [160] (* this is a nbsp *) (* ZACK: breaks unicode's binder followed by an ascii letter without blank *) (* let regexp ident_letter = xml_letter *) @@ -75,7 +76,7 @@ let regexp meta_ident = "$" ident let regexp meta_anonymous = "$_" let regexp qstring = '"' [^ '"']* '"' -let regexp begincomment = "(**" xml_blank +let regexp begincomment = "(**" utf8_blank let regexp beginnote = "(*" let regexp endcomment = "*)" (* let regexp comment_char = [^'*'] | '*'[^')'] @@ -229,7 +230,7 @@ let read_unparsed_group token_name lexbuf = let rec level2_meta_token = lexer - | xml_blank+ -> level2_meta_token lexbuf + | utf8_blank+ -> level2_meta_token lexbuf | ident -> let s = Ulexing.utf8_lexeme lexbuf in begin @@ -279,7 +280,7 @@ let rec ligatures_token k = and level2_ast_token = lexer - | xml_blank+ -> ligatures_token level2_ast_token lexbuf + | utf8_blank+ -> ligatures_token level2_ast_token lexbuf | meta -> let s = Ulexing.utf8_lexeme lexbuf in return lexbuf ("META", String.sub s 1 (String.length s - 1)) @@ -320,7 +321,7 @@ and level2_ast_token = and level1_pattern_token = lexer - | xml_blank+ -> ligatures_token level1_pattern_token lexbuf + | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) | ident -> let s = Ulexing.utf8_lexeme lexbuf in diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index b9c46917c..a41ccc991 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -97,8 +97,8 @@ let make_args_for_apply term2pres args = Some "xlink", "href", lemma.Con.lemma_uri ] in (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row - | Con.Term t -> - if is_first then + | Con.Term (b,t) -> + if is_first || (not b) then (term2pres t)::row else (B.b_object (P.Mi([],"?")))::row | Con.ArgProof _ @@ -135,8 +135,7 @@ let rec justification term2pres p = Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p]) and proof2pres ?skip_initial_lambdas is_top_down term2pres p = - let rec proof2pres ?(skip_initial_lambdas_internal=false) is_top_down p omit_dot = - prerr_endline p.Con.proof_conclude.Con.conclude_method; + let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot = let indent = let is_decl e = (match e with @@ -151,7 +150,13 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | Some t -> Some (term2pres t)) in let body = let presconclude = - conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion + conclude2pres + ?skip_initial_lambdas_internal: + (match skip_initial_lambdas_internal with + Some (`Later s) -> Some (`Now s) + | _ -> None) + is_top_down + p.Con.proof_name p.Con.proof_conclude indent omit_conclusion omit_dot in let presacontext = acontext2pres @@ -161,7 +166,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion") in context2pres - (if skip_initial_lambdas_internal then [] else p.Con.proof_context) + (match skip_initial_lambdas_internal with + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) + | _ -> p.Con.proof_context) presacontext in match p.Con.proof_name with @@ -174,7 +181,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = let concl = make_concl ~attrs:[ Some "helm", "xref", p.Con.proof_id ] "proof of" ac in - B.b_toggle [ concl; body ] + B.b_toggle [ B.H ([], [concl; B.skip ; B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")") ]) ; body ] in B.indent action @@ -260,7 +269,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); continuation])) ac continuation - and conclude2pres ?skip_initial_lambdas_internal is_top_down conclude indent omit_conclusion omit_dot = + and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot = let tconclude_body = match conclude.Con.conclude_conclusion with Some t (*when not omit_conclusion or @@ -273,11 +282,37 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = if conclude.Con.conclude_method = "BU_Conversion" then B.b_hv [] (make_concl "that is equivalent to" concl :: - if is_top_down then [B.b_space ; B.Text([],"done.")] else []) + if is_top_down then [B.b_space ; B.b_kw "done"; + B.Text([],".")] else []) else if conclude.Con.conclude_method = "FalseInd" then (* false ind is in charge to add the conclusion *) falseind conclude else + let prequel = + if + (match skip_initial_lambdas_internal with + None + | Some (`Later _) -> true + | Some (`Now _) -> false) + && conclude.Con.conclude_method = "Intros+LetTac" + then + let name = get_name name in + [B.V ([], + [ B.H([], + let expected = + (match conclude.Con.conclude_conclusion with + None -> B.Text([],"NO EXPECTED!!!") + | Some c -> term2pres c) + in + [make_concl "we need to prove" expected; + B.skip; + B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")"); + B.Text ([],".") + ])])] + else + [] in let conclude_body = conclude_aux ?skip_initial_lambdas_internal conclude in let ann_concl = @@ -286,11 +321,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = || conclude.Con.conclude_method = "TD_Conversion" then B.Text([],"") - else if omit_conclusion then B.Text([],"done.") + else if omit_conclusion then + B.H([], [B.b_kw "done" ; B.Text([],".") ]) else B.b_hv [] - ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else []) + ((if not is_top_down || omit_dot then [make_concl "we proved" + concl; B.Text([],if not is_top_down then "(previous)" else "")] + else [B.b_kw "done"]) @ if not omit_dot then [B.Text([],".")] else []) in - B.V ([], [conclude_body; ann_concl]) + B.V ([], prequel @ [conclude_body; ann_concl]) | _ -> conclude_aux ?skip_initial_lambdas_internal conclude in if indent then @@ -324,7 +362,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = else if conclude.Con.conclude_method = "Exact" then let arg = (match conclude.Con.conclude_args with - [Con.Term t] -> term2pres t + [Con.Term (b,t)] -> assert (not b);term2pres t | [Con.Premise p] -> (match p.Con.premise_binder with | None -> assert false; (* unnamed hypothesis ??? *) @@ -333,12 +371,16 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (match conclude.Con.conclude_conclusion with None -> B.b_h [] [B.b_kw "by"; B.b_space; arg] - | Some c -> let conclusion = term2pres c in + | Some c -> B.b_h [] [B.b_kw "by"; B.b_space; arg] ) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with - [Con.ArgProof p] -> proof2pres ?skip_initial_lambdas_internal true p false + [Con.ArgProof p] -> + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> + proof2pres ?skip_initial_lambdas_internal true p false + | _ -> assert false) | _ -> assert false) (* OLD CODE let conclusion = @@ -372,11 +414,11 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> assert false) in let term1 = (match List.nth conclude.Con.conclude_args 2 with - Con.Term t -> term2pres t + Con.Term (_,t) -> term2pres t | _ -> assert false) in let term2 = (match List.nth conclude.Con.conclude_args 5 with - Con.Term t -> term2pres t + Con.Term (_,t) -> term2pres t | _ -> assert false) in (* B.V ([], @@ -390,16 +432,18 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = *) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"]) else if conclude.Con.conclude_method = "Eq_chain" then let justification p = +(* if skip_initial_lambdas <> None (* cheating *) then [B.b_kw "by _"] else +*) let j1,j2 = justification term2pres p in j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> []) in let rec aux args = match args with | [] -> [] - | (Con.ArgProof p)::(Con.Term t)::tl -> + | (Con.ArgProof p)::(Con.Term (_,t))::tl -> B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p@ (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl) @@ -407,10 +451,10 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = in let hd = match List.hd conclude.Con.conclude_args with - | Con.Term t -> t + | Con.Term (_,t) -> t | _ -> assert false in - B.HOV([],[B.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *) + B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *) B.V ([],aux (List.tl conclude.Con.conclude_args))]) else if conclude.Con.conclude_method = "Apply" then let pres_args = @@ -431,7 +475,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = Con.Aux n -> B.b_kw ("aux " ^ n) | Con.Premise prem -> B.b_kw "premise" | Con.Lemma lemma -> B.b_kw "lemma" - | Con.Term t -> term2pres t + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> proof2pres true p false | Con.ArgMethod s -> B.b_kw "method" @@ -454,7 +498,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) - | Con.Term t -> + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> B.b_kw "a proof???" | Con.ArgMethod s -> B.b_kw "a method???") @@ -485,7 +529,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) - | Con.Term t -> + | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> B.b_kw "a proof???" | Con.ArgMethod s -> B.b_kw "a method???") in @@ -559,7 +603,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = (* let acontext = acontext2pres_old p.Con.proof_apply_context true in *) let body = - conclude2pres true p.Con.proof_conclude true true false in + conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in let presacontext = let acontext_id = match p.Con.proof_apply_context with @@ -640,7 +684,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.skip; term2pres hyp2.Con.dec_type]) in (* let body = proof2pres {proof with Con.proof_context = tl} false in *) - let body= conclude2pres false proof.Con.proof_conclude false true false in + let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -680,7 +724,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = B.skip; term2pres hyp.Con.dec_type]) in (* let body = proof2pres {proof with Con.proof_context = tl} false in *) - let body= conclude2pres false proof.Con.proof_conclude false true false in + let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in let presacontext = acontext2pres false proof.Con.proof_apply_context body false false in @@ -692,7 +736,12 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> assert false in - proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas is_top_down p false + proof2pres + ?skip_initial_lambdas_internal: + (match skip_initial_lambdas with + None -> Some (`Later 0) (* we already printed theorem: *) + | Some n -> Some (`Later n)) + is_top_down p false exception ToDo diff --git a/helm/software/components/content_pres/content2pres.mli b/helm/software/components/content_pres/content2pres.mli index 6dd0fd8aa..8d3753d86 100644 --- a/helm/software/components/content_pres/content2pres.mli +++ b/helm/software/components/content_pres/content2pres.mli @@ -33,7 +33,7 @@ (**************************************************************************) val content2pres: - ?skip_initial_lambdas:bool -> ?skip_thm_and_qed:bool -> + ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.cobj -> CicNotationPres.boxml_markup diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml index 46e2dd18c..0a19d8d56 100644 --- a/helm/software/components/library/libraryClean.ml +++ b/helm/software/components/library/libraryClean.ml @@ -62,7 +62,7 @@ let one_step_depend suri = HLog.debug "Warning SELECT without REGEXP"; sprintf ("SELECT source, h_occurrence FROM %s WHERE " ^^ - "h_occurrence LIKE '%s%%'") + "h_occurrence LIKE '%s%%' ESCAPE \"\\\"") obj_tbl buri*) end in @@ -103,7 +103,7 @@ let db_uris_of_baseuri buri = HLog.debug "Warning SELECT without REGEXP"; sprintf ("SELECT source, h_occurrence FROM %s WHERE " ^^ - "h_occurrence LIKE '%s%%'") + "h_occurrence LIKE '%s%%' ESCAPE \"\\\" ") obj_tbl buri *) end diff --git a/helm/software/components/library/libraryDb.ml b/helm/software/components/library/libraryDb.ml index 83bc3f6e6..db8a8a506 100644 --- a/helm/software/components/library/libraryDb.ml +++ b/helm/software/components/library/libraryDb.ml @@ -164,9 +164,12 @@ let remove_uri uri = let xpointers_of_ind uri = let dbd = instance () in let name_tbl = MetadataTypes.name_tbl () in + let escape s = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s) + in let query = sprintf - "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl - (HSql.escape (UriManager.string_of_uri uri)) + "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' ESCAPE \"\\\" " + name_tbl (escape (UriManager.string_of_uri uri)) in let rc = HSql.exec dbd query in let l = ref [] in diff --git a/helm/software/components/metadata/metadataDb.ml b/helm/software/components/metadata/metadataDb.ml index 6358df5b0..9480484c0 100644 --- a/helm/software/components/metadata/metadataDb.ml +++ b/helm/software/components/metadata/metadataDb.ml @@ -180,8 +180,12 @@ let clean ~(dbd:HSql.dbd) = uris in let del_from tbl = + let escape s = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s) + in let query s = - sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s + sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\" ESCAPE \"\\\" " + (tbl ()) (escape s) in List.iter (fun source_col -> ignore (HSql.exec dbd (query source_col))) @@ -193,8 +197,12 @@ let clean ~(dbd:HSql.dbd) = let unindex ~dbd ~uri = let uri = UriManager.string_of_uri uri in let del_from tbl = + let escape s = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s) + in let query tbl = - sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri + sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\" ESCAPE \"\\\" " + (tbl ()) (escape uri) in ignore (HSql.exec dbd (query tbl)) in diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml index 745466340..bf1dc49e0 100644 --- a/helm/software/components/metadata/metadataDeps.ml +++ b/helm/software/components/metadata/metadataDeps.ml @@ -103,12 +103,13 @@ let topological_sort ~dbd uris = let sorted_uris_of_baseuri ~dbd baseuri = let sql_pat = - Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" baseuri ^ "%" + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%" in let query = Printf.sprintf - ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE source LIKE \"%s\"") + ("SELECT source FROM %s WHERE source LIKE \"%s\" ESCAPE \"\\\" UNION " + ^^ + "SELECT source FROM %s WHERE source LIKE \"%s\" ESCAPE \"\\\"") (MetadataTypes.name_tbl ()) sql_pat MetadataTypes.library_name_tbl sql_pat in diff --git a/helm/software/components/metadata/sqlStatements.ml b/helm/software/components/metadata/sqlStatements.ml index ddc494c4a..5ba5429b7 100644 --- a/helm/software/components/metadata/sqlStatements.ml +++ b/helm/software/components/metadata/sqlStatements.ml @@ -202,10 +202,13 @@ let fill_hits refObj hits = let move_content (name1, tbl1) (name2, tbl2) buri = + let escape s = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s) + in assert (tbl1 = tbl2); sprintf "INSERT INTRO %s SELECT * FROM %s WHERE source LIKE \"%s%%\";" - name2 name1 (HSql.escape buri) + name2 name1 (escape buri) let direct_deps refObj uri = sprintf "SELECT * FROM %s WHERE source = \"%s\";" diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index b439b6cfc..0827b7ebc 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -66,11 +66,11 @@ let naif_closure ?(prefix_name="xxx_") t metasenv context = let lambda_close ?prefix_name t menv ctx = let t = naif_closure ?prefix_name t menv ctx in List.fold_left - (fun t -> function - | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *) - | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t) - | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t)) - t ctx + (fun (t,i) -> function + | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *) + | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1 + | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1) + (t,List.length menv) ctx ;; (* functions for retrieving theorems *) @@ -147,7 +147,9 @@ let is_unit_equation context metasenv oldnewmeta term = args in if propositional_args = [] then - let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + let newmetas = + List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv + in Some (args,metasenv,newmetas,head,newmeta) else None ;; @@ -163,19 +165,21 @@ let get_candidates universe cache t = candidates ;; -let only signature context t = +let only signature context metasenv t = try - let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph + in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in if b then b else - try - let ty' = unfold context ty in - let consts' = MetadataConstraints.constants_of ty' in - MetadataConstraints.UriManagerSet.subset consts' signature - with _-> false - with _ -> false + let ty' = unfold context ty in + let consts' = MetadataConstraints.constants_of ty' in + MetadataConstraints.UriManagerSet.subset consts' signature + with + | CicTypeChecker.TypeCheckerFailure _ -> assert false + | ProofEngineTypes.Fail _ -> false (* unfold may fail *) ;; let not_default_eq_term t = @@ -184,7 +188,7 @@ let not_default_eq_term t = not (LibraryObjects.in_eq_URIs uri) with Invalid_argument _ -> true -let retrieve_equations signature universe cache context= +let retrieve_equations dont_filter signature universe cache context metasenv = match LibraryObjects.eq_URI() with | None -> [] | Some eq_uri -> @@ -192,11 +196,10 @@ let retrieve_equations signature universe cache context= let fake= Cic.Meta(-1,[]) in let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in let candidates = get_candidates universe cache fake_eq in - (* defaults eq uris are built-in in auto *) - let candidates = List.filter not_default_eq_term candidates in - let candidates = List.filter (only signature context) candidates in - List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates; - candidates + if dont_filter then candidates + else + let candidates = List.filter not_default_eq_term candidates in + List.filter (only signature context metasenv) candidates let build_equality bag head args proof newmetas maxmeta = match head with @@ -218,6 +221,14 @@ let build_equality bag head args proof newmetas maxmeta = let partition_unit_equalities context metasenv newmeta bag equations = List.fold_left (fun (units,other,maxmeta)(t,ty) -> + if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then + let _ = + HLog.warn + ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context + ^ " since it is not meta closed") + in + units,(t,ty)::other,maxmeta + else match is_unit_equation context metasenv maxmeta ty with | Some (args,metasenv,newmetas,head,newmeta') -> let maxmeta,equality = @@ -232,50 +243,58 @@ let empty_tables = Saturation.make_passive [], Equality.mk_equality_bag) -let init_cache_and_tables dbd use_library paramod universe (proof, goal) = +let init_cache_and_tables + ?dbd use_library paramod use_context dont_filter universe (proof, goal) += (* the local cache in initially empty *) let cache = AutoCache.cache_empty in let _, metasenv, _subst,_, _, _ = proof in let signature = MetadataQuery.signature_of metasenv goal in let newmeta = CicMkImplicit.new_meta metasenv [] in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let ct = find_context_theorems context metasenv in + let ct = if use_context then find_context_theorems context metasenv else [] in debug_print (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct)))); let lt = - if use_library then - find_library_theorems dbd metasenv goal - else [] in + match use_library, dbd with + | true, Some dbd -> find_library_theorems dbd metasenv goal + | _ -> [] + in debug_print (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt)))); let cache = cache_add_list cache context (ct@lt) in let equations = - retrieve_equations signature universe cache context in + retrieve_equations dont_filter signature universe cache context metasenv + in debug_print (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations)))); let eqs_and_types = HExtlib.filter_map (fun t -> let ty,_ = - CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in - (* retrieve_equations could also return flexible terms *) - if is_an_equality ty then Some(t,ty) - else - try - let ty' = unfold context ty in - if is_an_equality ty' then Some(t,ty') else None - with _ -> None) (* catturare l'eccezione giusta di unfold *) - equations in + CicTypeChecker.type_of_aux' + metasenv context t CicUniv.empty_ugraph + in + (* retrieve_equations could also return flexible terms *) + if is_an_equality ty then Some(t,ty) + else + try + let ty' = unfold context ty in + if is_an_equality ty' then Some(t,ty') else None + with _ -> None) (* catturare l'eccezione giusta di unfold *) + equations + in let bag = Equality.mk_equality_bag () in let units, other_equalities, newmeta = - partition_unit_equalities context metasenv newmeta bag eqs_and_types in - (* let env = (metasenv, context, CicUniv.empty_ugraph) in - let equalities = - let eq_uri = - match LibraryObjects.eq_URI() with - | None ->assert false - | Some eq_uri -> eq_uri in - Saturation.simplify_equalities bag eq_uri env units in *) + partition_unit_equalities context metasenv newmeta bag eqs_and_types + in + (* SIMPLIFICATION STEP + let equalities = + let env = (metasenv, context, CicUniv.empty_ugraph) in + let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in + Saturation.simplify_equalities bag eq_uri env units + in + *) let passive = Saturation.make_passive units in let no = List.length units in let active = Saturation.make_active [] in @@ -380,7 +399,9 @@ let close_more tables maxmeta context status auto universe cache = let proof, goalno = status in let _, metasenv,_subst,_,_, _ = proof in let signature = MetadataQuery.signature_of metasenv goalno in - let equations = retrieve_equations signature universe cache context in + let equations = + retrieve_equations false signature universe cache context metasenv + in let eqs_and_types = HExtlib.filter_map (fun t -> @@ -509,7 +530,7 @@ let new_metasenv_and_unify_and_t in match let (active, passive,bag), cache, maxmeta = - init_cache_and_tables dbd flags.use_library true universe + init_cache_and_tables ~dbd flags.use_library true true false universe (proof'''',newmeta) in Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive @@ -1679,8 +1700,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = (* just for testing *) let use_library = flags.use_library in let tables,cache,newmeta = - init_cache_and_tables dbd use_library flags.use_only_paramod - universe (proof, goal) in + init_cache_and_tables ~dbd use_library flags.use_only_paramod true + false universe (proof, goal) in let tables,cache,newmeta = if flags.close_more then close_more @@ -1722,6 +1743,46 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +(* performs steps of rewrite with the universe, obtaining if possible + * a trivial goal *) +let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= + let _,metasenv,_subst,_,_,_ = proof in + let _,context,ty = CicUtil.lookup_meta goal metasenv in + let eq_uri = eq_of_goal ty in + let (active,passive,bag), cache, maxm = + (* we take the whole universe (no signature filtering) *) + init_cache_and_tables false true false true universe (proof,goal) + in + let initgoal = [], [], ty in + let table = + let equalities = (Saturation.list_of_passive passive) in + (* we demodulate using both actives passives *) + List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities + in + let env = metasenv,context,CicUniv.empty_ugraph in + match Indexing.solve_demodulating bag env table initgoal steps with + | Some (proof, metasenv, newty) -> + let refl = + match newty with + | Cic.Appl[Cic.MutInd _;eq_ty;left;_] -> + Equality.Exact (Equality.refl_proof eq_uri eq_ty left) + | _ -> assert false + in + let proofterm,_ = + Equality.build_goal_proof + bag eq_uri proof refl newty [] context metasenv + in + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) status + | None -> + raise + (ProofEngineTypes.Fail (lazy + ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) +;; +let solve_rewrite_tac ~universe ?steps () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps) +;; + (* DEMODULATE *) let demodulate_tac ~dbd ~universe (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in @@ -1730,7 +1791,9 @@ let demodulate_tac ~dbd ~universe (proof,goal)= let initgoal = [], [], ty in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = - init_cache_and_tables dbd false true universe (proof,goal) in + init_cache_and_tables + ~dbd false true true false universe (proof,goal) + in let equalities = (Saturation.list_of_passive passive) in (* we demodulate using both actives passives *) let table = diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index 57bb26b60..cfb31a8c4 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -42,6 +42,12 @@ val demodulate_tac : universe:Universe.universe -> ProofEngineTypes.tactic +val solve_rewrite_tac: + universe:Universe.universe -> + ?steps:int -> + unit -> + ProofEngineTypes.tactic + type auto_status = Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * (int * Cic.term * int) list * @@ -53,7 +59,8 @@ val give_hint : int -> unit val give_prune_hint : int -> unit val lambda_close : - ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term + ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term * + int val pp_proofterm: Cic.term -> string val revision : string (* svn revision *) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 0e063d82b..24801542d 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -184,7 +184,15 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = Tacticals.first [Tactics.auto ~dbd ~params ~universe ; Tactics.auto ~dbd ~params:params' ~universe] - | `Term just -> Tactics.apply just + | `Term just -> + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context just + CicUniv.empty_ugraph + in + Tactics.solve_rewrite + ~universe:(Universe.index Universe.empty + (Universe.key ty) just) ~steps:1 () + (* Tactics.apply just *) in let plhs,prhs,prepare = match lhs with diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index e453d95c1..4e14964ff 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -294,6 +294,7 @@ let find_matches metasenv context ugraph lift_amount term termty = as above, but finds all the matching equalities, and the matching condition can be either Founif.matching or Inference.unification *) +(* XXX termty unused *) let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in @@ -363,10 +364,12 @@ let find_all_matches (* returns true if target is subsumed by some equality in table *) +(* let print_res l = prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug, ((pos,equation),_)) -> Equality.string_of_equality equation)l)) ;; +*) let subsumption_aux use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in @@ -1093,4 +1096,118 @@ let rec demodulation_goal bag env table goal = | None -> do_right () ;; +type next = L | R +type solved = Yes of Equality.goal | No of Equality.goal list + +(* returns all the 1 step demodulations *) +module C = Cic;; +module S = CicSubstitution;; +let rec demodulation_all_aux + metasenv context ugraph table lift_amount term += + let candidates = + get_candidates ~env:(metasenv,context,ugraph) Matching table term + in + match term with + | C.Meta _ -> [] + | _ -> + let termty, ugraph = C.Implicit None, ugraph in + let res = + find_all_matches + metasenv context ugraph lift_amount term termty candidates + in + match term with + | C.Appl l -> + let res, _, _ = + List.fold_left + (fun (res,l,r) t -> + res @ + List.map + (fun (rel, s, m, ug, c) -> + (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) + (demodulation_all_aux + metasenv context ugraph table lift_amount t), + l@[List.hd r], List.tl r) + (res, [], List.map (S.lift 1) l) l + in + res + | C.Prod (nn, s, t) + | C.Lambda (nn, s, t) -> + let context = (Some (nn, C.Decl s))::context in + let mk s t = + match term with + | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t) + in + res @ + List.map + (fun (rel, subst, m, ug, c) -> + mk (S.lift 1 s) rel, subst, m, ug, c) + (demodulation_all_aux + metasenv context ugraph table (lift_amount+1) t) + (* we could demodulate also in s, but then t may be badly + * typed... *) + | t -> res +;; + +let solve_demodulating bag env table initgoal steps = + let _, context, ugraph = env in + let solved goal res side = + let newg = build_newgoal bag context goal side Equality.Demodulation res in + match newg with + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) + when LibraryObjects.is_eq_URI uri -> + (try + let _ = + Founif.unification m m context left right CicUniv.empty_ugraph + in + Yes newg + with CicUnification.UnificationFailure _ -> No [newg]) + | _ -> No [newg] + in + let solved goal res_list side = + let newg = List.map (fun x -> solved goal x side) res_list in + try + List.find (function Yes _ -> true | _ -> false) newg + with Not_found -> + No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) + in + let rec first f l = + match l with + | [] -> None + | x::tl -> + match f x with + | None -> first f tl + | Some x as ok -> ok + in + let rec aux steps next goal = + if steps = 0 then None else + let goalproof,menv,_,_,left,right = open_goal goal in + let do_step t = + demodulation_all_aux menv context ugraph table 0 t + in + match next with + | L -> + (match do_step left with + | _::_ as res -> + (match solved goal res Utils.Right with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> aux steps R goal) + | Yes newgoal -> Some newgoal) + | [] -> aux steps R goal) + | R -> + (match do_step right with + | _::_ as res -> + (match solved goal res Utils.Left with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> None) + | Yes newgoal -> Some newgoal) + | [] -> None) + in + aux steps L initgoal +;; + let get_stats () = "" ;; diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 340a1eddb..7f464d248 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -99,6 +99,14 @@ val check_target: Equality.equality_bag -> Cic.context -> Equality.equality -> string -> unit +val solve_demodulating: + Equality.equality_bag -> + Cic.metasenv * Cic.context * CicUniv.universe_graph -> + Index.t -> + Equality.goal -> + int -> + Equality.goal option + (** profiling *) val get_stats: unit -> string diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index 0c9a75e62..20b564f4b 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -71,4 +71,3 @@ val given_clause: ProofEngineTypes.goal list) option * active_table * passive_table * int - diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 1ccd2adcb..67a607d1a 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -65,6 +65,7 @@ let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac let simpl = ReductionTactics.simpl_tac +let solve_rewrite = Auto.solve_rewrite_tac let split = IntroductionTactics.split_tac let subst = SubstTactic.subst_tac let symmetry = EqualityTactics.symmetry_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 16c668266..e9c265c8e 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun 4 13:44:18 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 13 14:11:00 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -94,6 +94,8 @@ val rewrite_simpl : val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val solve_rewrite : + universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val subst : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic diff --git a/helm/software/components/whelp/whelp.ml b/helm/software/components/whelp/whelp.ml index e1d8306cc..eb1f2b630 100644 --- a/helm/software/components/whelp/whelp.ml +++ b/helm/software/components/whelp/whelp.ml @@ -43,12 +43,15 @@ let sqlpat_of_shellglob = shellglob))) let locate ~(dbd:HSql.dbd) ?(vars = false) pat = + let escape s = HSql.escape s in let sql_pat = sqlpat_of_shellglob pat in let query = - sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE value LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat + sprintf + ("SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" " + ^^ "UNION " ^^ + "SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" ") + (MetadataTypes.name_tbl ()) (escape sql_pat) + MetadataTypes.library_name_tbl (escape sql_pat) in let result = HSql.exec dbd query in List.filter nonvar diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 3cfaff526..5d81d9224 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -200,7 +200,7 @@ let txt_of_cic_object in String.concat "" (List.map aux script) ^ "\n\n" -let txt_of_inline_macro style suri prefix = +let txt_of_inline_macro ?map_unicode_to_tex style suri prefix = let print_exc = function | ProofEngineHelpers.Bad_pattern s as e -> Printexc.to_string e ^ " " ^ Lazy.force s @@ -209,8 +209,10 @@ let txt_of_inline_macro style suri prefix = let dbd = LibraryDb.instance () in let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in let map uri = - try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *) - (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) + try + txt_of_cic_object + ?map_unicode_to_tex 78 style prefix + (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) with | e -> Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 170980cb0..9307f1e18 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -69,11 +69,12 @@ val txt_of_cic_sequent_conclusion: val txt_of_cic_object: ?map_unicode_to_tex:bool -> ?skip_thm_and_qed:bool -> - ?skip_initial_lambdas:bool -> + ?skip_initial_lambdas:int -> int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string (* presentation_style, uri or baseuri, name prefix *) val txt_of_inline_macro: + ?map_unicode_to_tex:bool -> GrafiteAst.presentation_style -> string -> string -> string diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index a615e6f9f..844d2f01e 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -549,7 +549,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status in let proof_script = if List.exists (fun (s,_) -> s = "paramodulation") params then - let proof_term = + let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc in @@ -566,7 +566,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status ApplyTransformation.txt_of_cic_object ~map_unicode_to_tex:false ~skip_thm_and_qed:true - ~skip_initial_lambdas:true + ~skip_initial_lambdas:how_many_lambdas 80 GrafiteAst.Declarative "" obj else if true then @@ -574,7 +574,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status cic2grafite cc menv proof_term else (* alternative using FG stuff *) - let proof_term = + let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc in @@ -590,7 +590,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status (ApplyTransformation.txt_of_cic_object ~map_unicode_to_tex:false ~skip_thm_and_qed:true - ~skip_initial_lambdas:true + ~skip_initial_lambdas:how_many_lambdas 80 (GrafiteAst.Procedural None) "" obj)) in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in @@ -600,7 +600,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) | TA.Inline (_,style,suri,prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + let str = + ApplyTransformation.txt_of_inline_macro + ~map_unicode_to_tex:false style suri prefix + in [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff