adding parameters to auto to tune some builtin constants

+ a not working "Filename.chop_extension" removed. It does not understand our uri fragments
+ the "debug" flag enables auto debug_print that produces stack overflow sometimes :(

.gitignore

@@ -1,3 +1,5 @@
+*.exe
+_build
 matita/broken_contribs/lambdadelta/bin/*/_build
 matita/broken_contribs/lambdadelta/.depend
 matita/broken_contribs/lambdadelta/bin/recomm/srcs

components/ng_kernel/nUri.ml

@@ -47,7 +47,7 @@ fun s ->
 ;;
 
 let eq = (==);;
-let compare (n1,_) (n2,_) = n2 - n1;;
+let compare (n1,_) (n2,_) = n2 - n1;; (* we compare by age *)
 let hash (n,_) = n;;
 
 module HT = struct

components/ng_paramodulation/nCicParamod.ml

@@ -1,12 +1,12 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
@@ -16,12 +16,14 @@ NCicBlob.set_default_eqP()
 NCicProof.set_default_sig()
 ;;
 
+let time = ref 300.0
+
 let noprint _ = ();;
-let print s = prerr_endline (Lazy.force s);; 
-let debug = noprint;; 
+let print s = prerr_endline (Lazy.force s);;
+let debug = noprint;;
 
-module B(C : NCicBlob.NCicContext): Orderings.Blob 
-  with type t = NCic.term and type input = NCic.term 
+module B(C : NCicBlob.NCicContext): Orderings.Blob
+  with type t = NCic.term and type input = NCic.term
   = Orderings.LPO(NCicBlob.NCicBlob(C))
 
 module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
@@ -30,32 +32,32 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 (*
   List.iter (fun x ->
      print_endline (Pp.pp_unit_clause ~margin:max_int
-     (fst(Terms.M.find x bag)))) l; 
+     (fst(Terms.M.find x bag)))) l;
 *)
   (* let stamp = Unix.gettimeofday () in *)
   let proofterm,prooftype = NCicProof.mk_proof status ~demod bag i fo_subst l in
   (* debug (lazy (Printf.sprintf "Got proof term in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
 (*
-  let metasenv, proofterm = 
+  let metasenv, proofterm =
     let rec aux k metasenv = function
       | NCic.Meta _ as t -> metasenv, t
-      | NCic.Implicit _ -> 
+      | NCic.Implicit _ ->
           let metasenv, i, _, _ =
-            NCicMetaSubst.mk_meta metasenv context `IsTerm 
+            NCicMetaSubst.mk_meta metasenv context `IsTerm
           in
             metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
-      | t -> NCicUntrusted.map_term_fold_a 
+      | t -> NCicUntrusted.map_term_fold_a
           (fun _ k -> k+1) k aux metasenv t
     in
       aux 0 metasenv proofterm
   in *)
   debug (lazy (status#ppterm ~metasenv ~subst ~context proofterm));
 (*
   let stamp = Unix.gettimeofday () in
-  let metasenv, subst, proofterm, _prooftype = 
-    NCicRefiner.typeof 
-      (status#set_coerc_db NCicCoercion.empty_db) 
+  let metasenv, subst, proofterm, _prooftype =
+    NCicRefiner.typeof
+      (status#set_coerc_db NCicCoercion.empty_db)
       metasenv subst context proofterm None
   in
     print (lazy (Printf.sprintf "Refined in %fs"
@@ -65,32 +67,32 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
 
 let nparamod status metasenv subst context t table =
   let module C =
-    struct 
+    struct
       let metasenv = metasenv
       let subst = subst
-      let context = context 
-    end 
+      let context = context
+    end
   in
   (*let module B = B(C) in*)
   let module P = NCicParamod(C) in
   (*let module Pp = Pp.Pp(B) in*)
   let bag, maxvar = Terms.empty_bag, 0 in
-  let (bag,maxvar), goals = 
+  let (bag,maxvar), goals =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
-  let (bag,maxvar), passives = 
+  let (bag,maxvar), passives =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
   in
-  match 
-    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
-      ~g_passives:goals ~passives (bag,maxvar) 
-  with 
+  match
+    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. !time)
+      ~g_passives:goals ~passives (bag,maxvar)
+  with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       List.map (readback status metasenv subst context) solutions
 ;;
-  
-module EmptyC = 
+
+module EmptyC =
   struct
     let metasenv = []
     let subst = []
@@ -103,7 +105,17 @@ module P = NCicParamod(EmptyC)
 type state = P.state
 let empty_state = P.empty_state
 
-exception NotEmbeddable 
+let pp_state s =
+  let module Pp = Pp.Pp(CB) in
+  let str () =
+    let bag, _ = P.bag_of_state s in
+    Pp.pp_bag bag
+  in
+  debug (lazy "EQ CACHE BEGINS");
+  debug (lazy (str ()));
+  debug (lazy "EQ CACHE ENDS")
+
+exception NotEmbeddable
 
 let not_embeddable status subst context ty =
   let rec aux = function
@@ -112,12 +124,12 @@ let not_embeddable status subst context ty =
     | NCic.Rel _
     | NCic.Sort _ -> ()
     | NCic.Appl l -> List.iter aux l
-    | t -> 
+    | t ->
         (* cannot embed a blob term containing metas *)
         if (NCicUntrusted.metas_of_term status subst context t = [])
-        then () 
+        then ()
         else raise NotEmbeddable
-  in 
+  in
   try aux ty; noprint (lazy ("Embeddable")); false
   with NotEmbeddable -> debug (lazy ("Not embeddable")); true
 ;;
@@ -130,12 +142,12 @@ let tooflex (_,l,_,_) =
        | _, (Terms.Var _ | Terms.Node (Terms.Var _::_)),(Terms.Incomparable | Terms.Invertible) -> true
        | _ -> false)
     | _ -> false
-;;  
+;;
 
 let forward_infer_step0 status metasenv subst context s t ty =
   let bag = P.bag_of_state s in
   let not_embed =
-    let sty,_,_ = 
+    let sty,_,_ =
       NCicMetaSubst.saturate status ~delta:0  metasenv subst context ty 0 in
       not_embeddable status subst context sty in
   if not_embed then (debug (lazy "theorem not embeddable"); s,None)
@@ -171,7 +183,7 @@ let demod status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
   match P.demod s goal with
     | P.Error _ | P.GaveUp | P.Timeout _ -> []
-    | P.Unsatisfiable solutions -> 
+    | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback ~demod:true status metasenv subst context) solutions
@@ -180,30 +192,31 @@ let demod status metasenv subst context s goal =
 let paramod status metasenv subst context s goal =
   if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
-  match P.nparamod ~useage:true ~max_steps:max_int 
-    ~timeout:(Unix.gettimeofday () +. 300.0) s goal with
+  match P.nparamod ~useage:true ~max_steps:max_int
+    ~timeout:(Unix.gettimeofday () +. !time) s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions
 ;;
 
 let fast_eq_check status metasenv subst context s goal =
+  pp_state s;
   if not_embeddable status subst context (snd goal) then [] else
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions
 ;;
 
 let is_equation status metasenv subst context ty =
-  let hty, _, _ = 
+  let hty, _, _ =
     NCicMetaSubst.saturate status ~delta:0 metasenv subst context
-      ty 0 
+      ty 0
   in match hty with
     | NCic.Appl (eq ::_) when eq = CB.eqP -> true
     | _ -> false
@@ -214,7 +227,7 @@ let demodulate status metasenv subst context s goal =
   (* let stamp = Unix.gettimeofday () in *)
   match P.fast_eq_check s goal with
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
-  | P.Unsatisfiable solutions -> 
+  | P.Unsatisfiable solutions ->
       (* print (lazy (Printf.sprintf "Got solutions in %fs"
 		     (Unix.gettimeofday() -. stamp))); *)
       List.map (readback status metasenv subst context) solutions

components/ng_paramodulation/nCicParamod.mli

@@ -1,47 +1,50 @@
 (*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.      
-     \ /   This software is distributed as is, NO WARRANTY.     
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department, University of Bologna, Italy.
+    ||I||
+    ||T||  HELM is free software; you can redistribute it and/or
+    ||A||  modify it under the terms of the GNU General Public License
+    \   /  version 2 or (at your option) any later version.
+     \ /   This software is distributed as is, NO WARRANTY.
       V_______________________________________________________________ *)
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+(* FG: this was 300.0 hard coded *)
+val time: float ref
+
 val nparamod :
   #NCicCoercion.status ->
-  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+  NCic.metasenv -> NCic.substitution -> NCic.context ->
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
      (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
 
-type state 
+type state
 val empty_state: state
-val forward_infer_step: 
+val forward_infer_step:
   #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   state -> NCic.term -> NCic.term -> state
 val index_obj:
  #NCic.status -> state -> NUri.uri -> state * NCic.term Terms.unit_clause option
 val is_equation:
  #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> bool
-val paramod : 
+val paramod :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val fast_eq_check : 
+val fast_eq_check :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val demod : 
+val demod :
   #NCicCoercion.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context ->
-  state -> 
-  (NCic.term * NCic.term) -> 
+  state ->
+  (NCic.term * NCic.term) ->
   (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list