]> matita.cs.unibo.it Git - helm.git/commitdiff
many changes:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 13 Jun 2007 13:01:32 +0000 (13:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 13 Jun 2007 13:01:32 +0000 (13:01 +0000)
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

26 files changed:
components/acic_content/acic2content.ml
components/acic_content/content.ml
components/acic_content/content.mli
components/acic_content/content2cic.ml
components/cic/deannotate.ml
components/cic/deannotate.mli
components/content_pres/cicNotationLexer.ml
components/content_pres/content2pres.ml
components/content_pres/content2pres.mli
components/library/libraryClean.ml
components/library/libraryDb.ml
components/metadata/metadataDb.ml
components/metadata/metadataDeps.ml
components/metadata/sqlStatements.ml
components/tactics/auto.ml
components/tactics/auto.mli
components/tactics/declarative.ml
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/saturation.mli
components/tactics/tactics.ml
components/tactics/tactics.mli
components/whelp/whelp.ml
matita/applyTransformation.ml
matita/applyTransformation.mli
matita/matitaScript.ml

index eddee38b1a51ed2c985df789006c574ae21604e0..99bab2de44f122fc7d099ba331982bdbe7304409 100644 (file)
@@ -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,
index 22733dcaa33248a7c03477653025ce9d34a21e9b..c8b22f497e713cd0186d99e720ebdd93739fad5c 100644 (file)
@@ -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 (* ???? *)
 
index c1122b8f2b2627d67dccd9ccd3fd4a4e0643af16..546000330da51b7b4eaf63d5b6e8c21e63f57753 100644 (file)
@@ -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 (* ???? *)
 
index 9acea81fa903b8455c830763b5a4c26fef365b66..dcec61d84a478018a003a1623227ed8249b79dac 100644 (file)
@@ -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
 
index f04f5aa10e1197ea61c8338e3a39a01968083346..b7c7d1113cdbd6fea17bb96ad90742b21436b3bc 100644 (file)
@@ -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) ->
index 89b18d2d6faca057879068950560fed48f5df0a8..1e29b5b648ded189030f098707b2496156b7573d 100644 (file)
@@ -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
index 749731bdafcf9038923c213757f652b896c0d56c..f157af40696876a7f38b65946cb6c72acc588590 100644 (file)
@@ -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
index b9c46917c236c32006f0759a1b4fbc7b8c7c7dfa..a41ccc99158a73562218887d2d786e57d903121e 100644 (file)
@@ -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
 
index 6dd0fd8aacb3960a2915df99f8ed15b685fbc452..8d3753d8662e59c16c21a6862ec3889505b6bfc0 100644 (file)
@@ -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
index 46e2dd18cc2c8d56ca72fa56d2bb52082eba3675..0a19d8d5603451fa1e7ccd63e6e4a6170327ebd9 100644 (file)
@@ -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
index 83bc3f6e67ace89cb334b86fa754d4d812d43d05..db8a8a50627d9cb570bfa0a241a8a25730189e8c 100644 (file)
@@ -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
index 6358df5b04718f634defe679c0af44cb8cfcc04d..9480484c00d0f9e879d4f5747cf011f86400ed9b 100644 (file)
@@ -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
index 7454663400a32db88db5e1113a5764b25eedde10..bf1dc49e0ec2d8213577f31a275aa27e4e2ad1f2 100644 (file)
@@ -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
index ddc494c4abfaf89ed93ce0e61487c0dacd26b2df..5ba5429b71199b96b6b8e25d712a1b4a5ccd7508 100644 (file)
@@ -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\";"
index b439b6cfc6efa2c383b0389a09532fa808dc3ef0..0827b7ebcab8b6372c7f487b42077a063edf21d3 100644 (file)
@@ -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 = 
index 57bb26b60ca52a5e2ad6d7f2118fd4fbfc58c16c..cfb31a8c4c15a7f62d0b5405e89143ea7139dfe7 100644 (file)
@@ -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 *)
index 0e063d82b6f60b728b4608715e8a80e75957cd05..24801542dabcb76f57a6684a6d60fccaef31a488 100644 (file)
@@ -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
index e453d95c12c968a3cd696b157db950a6f87408e7..4e14964ff3dc26016818fecd566e83ced817214c 100644 (file)
@@ -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 () = "" ;;
index 340a1eddbc0acf0369ec36b29036d876a295a951..7f464d2485af2c7f0b034172073e205bf1f5ee73 100644 (file)
@@ -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
index 0c9a75e62478dff464ea8ee5b5451b662939a1a4..20b564f4bc7590ca05c0f581cb4ff652415adde0 100644 (file)
@@ -71,4 +71,3 @@ val given_clause:
      ProofEngineTypes.goal list) option * 
     active_table * passive_table * int
 
-
index 1ccd2adcb0ab0d655438ca858d56770ceec76e0b..67a607d1acf16087a7caa65a57ad67bafa88d79d 100644 (file)
@@ -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
index 16c668266987e31378f64737531ba32c16ba2017..e9c265c8e3e451a3b45bccc699dc2c3ad97e77d9 100644 (file)
@@ -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
index e1d8306cce105c1d75b5636bfec377311e056d88..eb1f2b6301c239611b7fa88eb7021ffe78333612 100644 (file)
@@ -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
index 3cfaff52637177e736ff14ea6a8a99ac84f94ae5..5d81d922496e28be36697bb59b77dd74af9f94f1 100644 (file)
@@ -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" 
index 170980cb0e2f95c87c39a02d58150b7f22ec1453..9307f1e18ef2aef63c9efe87537c722393a59e42 100644 (file)
@@ -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
index a615e6f9f01f08bafd6b893436e90e5110d26dde..844d2f01eb3c73d42767c0b7b68b26fd69056152 100644 (file)
@@ -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