]> matita.cs.unibo.it Git - helm.git/commitdiff
toplevel.ml patched but it doesn't compile with open and free variables.
authornatile <??>
Fri, 22 Nov 2002 18:39:19 +0000 (18:39 +0000)
committernatile <??>
Fri, 22 Nov 2002 18:39:19 +0000 (18:39 +0000)
helm/gTopLevel/topLevel/topLevel.ml

index 78aceae26f52ecafd4d53e07055e688bcda95737..d4af37c23e38cd3b16e9791329e5c665d359a558 100644 (file)
@@ -1,4 +1,4 @@
-let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"
+let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
 
 let show_queries = ref false
 
@@ -25,13 +25,13 @@ let get_terms () =
    let lexbuf = Lexing.from_channel stdin in
    try
       while true do
-         match CicTextualParserContext.main  
-           (UriManager.uri_of_string "cic:/dummy") [] []
-           CicTextualLexer.token lexbuf
-           with
-            | None           -> ()
-            | Some (_, expr) -> terms := expr :: ! terms
-      done;
+       let dom,mk_term =
+        CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+       in
+        match dom with
+          [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
+        | _ -> assert false
+      done ;
       ! terms
    with
       CicTextualParser0.Eof -> ! terms
@@ -120,7 +120,7 @@ let mbackward n m l =
            if Mqint.get_stat () then 
               print_string ("? " ^ CicPp.ppterm term ^ nl);
            let t0 = Sys.time () in
-            let r = Gen.backward [] [] term level in
+            let r = Gen.searchPattern [] [] term level in
            let t1 = Sys.time () -. t0 in
            let info = Gen.get_query_info () in
            let num = List.nth info 0 in
@@ -192,7 +192,6 @@ let parse_args () =
 
 let _ =
    let module Gen = MQueryGenerator in
-   CicCooking.init () ; 
    Logger.log_callback :=
       (Logger.log_to_html
       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;