New: cache of translated fixpoints (to avoid the generative fix restriction and

to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)

diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile
index 8269534d50f7b12c6a55c2bbf63b06b82e336197..56915b13e6d16e813f56e969e794b3cb2e9dccb0 100644 (file)
--- a/helm/software/components/ng_kernel/Makefile
+++ b/helm/software/components/ng_kernel/Makefile
@@ -4,9 +4,9 @@ PREDICATES =
 INTERFACE_FILES = \
        nUri.mli \
        nReference.mli \
-       oCic2NCic.mli  \
        nCicUtils.mli \
        nCicSubstitution.mli \
+       oCic2NCic.mli  \
        nCicEnvironment.mli \
        nCicPp.mli \
        nCicReduction.mli \

diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt
index 84385385cffd7b9358cdd0588899e7cf380bd830..4692a4f143ee5b80b662007c80d1499118f47916 100644 (file)
--- a/helm/software/components/ng_kernel/alluris.txt
+++ b/helm/software/components/ng_kernel/alluris.txt
@@ -1,3 +1,59 @@
+cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
+cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
+cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/appA.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
+cic:/matita/algebra/CoRN/SetoidFun/UR.con
+cic:/matita/algebra/CoRN/SetoidFun/UQ.con
+cic:/matita/algebra/CoRN/SetoidFun/UP.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
+cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/Inv.con
+cic:/matita/algebra/CoRN/SetoidFun/Fid.con
+cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
+cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
+cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/BR.con
+cic:/matita/algebra/CoRN/SetoidFun/BQ.con
+cic:/matita/algebra/CoRN/SetoidFun/BP.con
+cic:/matita/algebra/CoRN/SetoidFun/Astar.con
+cic:/matita/demo/realisability/correct2.con
+cic:/matita/demo/realisability/correct.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
 cic:/matita/demo/realisability/type_OF_SP.con
 cic:/matita/demo/realisability/true_impl_realized.con
 cic:/matita/demo/realisability/sigma_rect.con
@@ -2057,65 +2113,6 @@ cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
 cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
 cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
 cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
-# -- fine --
-# # the same fix in different contexts has different lamb-lifted counterpart + generative fix
-# cic:/matita/demo/realisability/correct2.con
-# cic:/matita/demo/realisability/correct.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
-# # depending on the previous
-# cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
-# cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
-# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
-# cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
-# cic:/matita/algebra/CoRN/SetoidFun/appA.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
-# cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
-# cic:/matita/algebra/CoRN/SetoidFun/UR.con
-# cic:/matita/algebra/CoRN/SetoidFun/UQ.con
-# cic:/matita/algebra/CoRN/SetoidFun/UP.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
-# cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
-# cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
-# cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
-# cic:/matita/algebra/CoRN/SetoidFun/Inv.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fid.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
-# cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
-# cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
-# cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
-# cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
-# cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
-# cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
-# cic:/matita/algebra/CoRN/SetoidFun/BR.con
-# cic:/matita/algebra/CoRN/SetoidFun/BQ.con
-# cic:/matita/algebra/CoRN/SetoidFun/BP.con
-# cic:/matita/algebra/CoRN/SetoidFun/Astar.con
 # # mutual fix
 # cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
 # # depending on the previous

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 8b6fd7f4588a0bd2c1118245efa51cebd8ecc382..3880e361b9b9cbfbb19028b28022d1795ea396da 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -1,14 +1,67 @@
 module Ref = NReference
 
+type ctx = 
+  | Ce of NCic.hypothesis * NCic.obj list
+  | Fix of Ref.reference * string * NCic.term
+
+(***** A function to restrict the context of a term getting rid of unsed
+       variables *******)
+
+let restrict octx ctx ot =
+ let odummy = Cic.Implicit None in
+ let dummy = NCic.Meta (~-1,(0,NCic.Irl 0)) in
+ let rec aux m acc ot t =
+  function
+     [],[] -> (ot,t),acc
+   | ohe::otl as octx,he::tl ->
+      if CicTypeChecker.does_not_occur octx 0 1 ot then
+       aux (m+1) acc (CicSubstitution.subst odummy ot)
+        (NCicSubstitution.subst dummy t) (otl,tl)
+      else
+       (match ohe,he with
+           None,_ -> assert false
+         | Some (name,Cic.Decl oty),Ce ((name', NCic.Decl ty),objs) ->
+            aux (m+1) ((m+1,objs,None)::acc) (Cic.Lambda (name,oty,ot))
+             (NCic.Lambda (name',ty,t)) (otl,tl)
+         | Some (name,Cic.Decl oty),Fix (ref,name',ty) ->
+            aux (m+1) ((m+1,[],Some ref)::acc) (Cic.Lambda (name,oty,ot))
+             (NCic.Lambda (name',ty,t)) (otl,tl)
+         | Some (name,Cic.Def (obo,oty)),Ce ((name', NCic.Def (bo,ty)),objs) ->
+            aux (m+1) ((m+1,objs,None)::acc) (Cic.LetIn (name,obo,oty,ot))
+             (NCic.LetIn (name',bo,ty,t)) (otl,tl)
+         | _,_ -> assert false)
+   | _,_ -> assert false in
+ let rec split_lambdas_and_letins octx ctx infos (ote,te) =
+  match infos, ote, te with
+     ([], _, _) -> octx,ctx,ote
+   | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) ->
+       split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
+        (Ce ((name',NCic.Decl so),objs)::ctx) tl (ota,ta)
+   | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
+       split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
+        (Fix (r,name',so)::ctx) tl (ota,ta)
+   | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))->
+       split_lambdas_and_letins ((Some (name,(Cic.Def (obo,oty))))::octx)
+        (Ce ((nam',NCic.Def (bo,ty)),objs)::ctx) tl (ota,ta)
+   | (_, _, _) -> assert false
+ in
+  let long_t,infos = aux 0 [] ot dummy (octx,ctx) in
+  let clean_octx,clean_ctx,clean_ot= split_lambdas_and_letins [] [] infos long_t
+  in
+(*prerr_endline ("RESTRICT PRIMA: " ^ CicPp.pp ot (List.map (function None -> None | Some (name,_) -> Some name) octx));
+prerr_endline ("RESTRICT DOPO: " ^ CicPp.pp clean_ot (List.map (function None -> None | Some (name,_) -> Some name) clean_octx));
+*)
+   clean_octx,clean_ctx,clean_ot, List.map (fun (rel,_,_) -> rel) infos
+;;
+
+
+(**** The translation itself ****)
+
 let cn_to_s = function
   | Cic.Anonymous -> "_"
   | Cic.Name s -> s
 ;;
 
-type ctx = 
-  | Ce of NCic.hypothesis * NCic.obj list
-  | Fix of Ref.reference * string * NCic.term
-
 let splat mk_pi ctx t =
   List.fold_left
     (fun (t,l) c -> 
@@ -35,38 +88,47 @@ let context_tassonomy ctx =
       split true 0 1 ctx
 ;;
 
-let splat_args_for_rel ctx t = 
+let splat_args_for_rel ctx t ?rels n_fix =
+  let rels =
+   match rels with
+      Some rels -> rels
+    | None ->
+       let rec mk_irl = function 0 -> [] | n -> n::mk_irl (n - 1) in
+        mk_irl (List.length ctx)
+  in
   let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in
   if free = 0 then t 
   else
     let rec aux = function
-      | 0 -> []
-      | n -> 
-         match List.nth ctx (n+bound) with
-         | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix ->
-            NCic.Const refe :: aux (n-1)
-         | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (n+bound)::aux (n-1)
-         | Ce ((_, NCic.Def _),_) -> aux (n-1)
+      | n,_ when n = bound + n_fix -> []
+      | n,he::tl -> 
+         (match List.nth ctx (n-1) with
+          | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+             NCic.Const refe :: aux (n-1,tl)
+          | Fix _ | Ce ((_, NCic.Decl _),_)-> NCic.Rel (he - n_fix)::aux(n-1,tl)
+          | Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
+      | _,_ -> assert false
     in
-    NCic.Appl (t:: aux free)
+    NCic.Appl (t:: aux (List.length ctx,rels))
 ;;
 
-let splat_args ctx t n_fix = 
+let splat_args ctx t n_fix rels =
   let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in
   if ctx = [] then t
   else
    let rec aux = function
-     | 0 -> []
-     | n -> 
+     | 0,[] -> []
+     | n,he::tl -> 
         (match List.nth ctx (n-1) with
-         | Ce ((_, NCic.Decl _),_) when n <= bound -> NCic.Rel n:: aux (n-1)
+         | Ce ((_, NCic.Decl _),_) when n <= bound -> NCic.Rel he:: aux (n-1,tl)
          | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
-            splat_args_for_rel ctx (NCic.Const refe):: aux (n-1)
-         | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (n - n_fix):: aux (n-1)
-         | Ce ((_, NCic.Def _),_) -> aux (n - 1)
+            splat_args_for_rel ctx (NCic.Const refe) ~rels n_fix :: aux (n-1,tl)
+         | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (he - n_fix)::aux(n-1,tl)
+         | Ce ((_, NCic.Def _),_) -> aux (n - 1,tl)
         ) 
+     | _,_ -> assert false
    in
-   NCic.Appl (t:: aux (List.length ctx))
+   NCic.Appl (t:: aux ((List.length ctx,rels)))
 ;;
 
 exception Nothing_to_do;;
@@ -210,6 +272,44 @@ let get_fresh,reset_seed =
   (function () -> seed := 0)
 ;;
 
+exception Found of NReference.reference;;
+let cache = Hashtbl.create 313;; 
+let same_obj =
+ function
+    (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty1,_],_)),
+    (_,_,_,_,NCic.Fixpoint (_,[_,_,_,ty2,_],_))
+     when ty1 = ty2 -> true
+  | _ -> false
+;;
+let find_in_cache name obj ref =
+ try
+  List.iter
+   (function (ref',obj') ->
+     let recno =
+      match ref with
+         NReference.Ref (_,_,NReference.Fix (_,recno)) -> recno
+       | _ -> assert false in
+     let recno' =
+      match ref' with
+         NReference.Ref (_,_,NReference.Fix (_,recno)) -> recno
+       | _ -> assert false in
+     if recno = recno' && same_obj (obj,obj') then
+(*(prerr_endline "!!!!!!!!!!! CACHE HIT !!!!!!!!!!";*)
+       raise (Found ref')
+(*);*)
+(*
+     else
+(prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==> " ^ NReference.string_of_reference ref');
+      raise Not_found
+)
+*)
+  ) (Hashtbl.find_all cache name);
+(*prerr_endline "<<< CACHE MISS >>>";*)
+  Hashtbl.add cache name (ref,obj);
+  None
+ with Found ref -> Some ref
+;;
+
 (* we are lambda-lifting also variables that do not occur *)
 (* ctx does not distinguish successive blocks of cofix, since there may be no
  *   lambda separating them *)
@@ -259,9 +359,12 @@ let convert_term uri t =
         in
         splat_args ctx 
          (NCic.Const (Ref.reference_of_ouri buri (Ref.CoFix cofixno)))
-         n_fix,
+         n_fix (assert false),
         fixpoints @ [obj]
-    | Cic.Fix (fixno, fl) ->
+    | Cic.Fix _ as fix ->
+        let octx,ctx,fix,rels = restrict octx ctx fix in
+        let fixno,fl =
+         match fix with Cic.Fix (fixno,fl) -> fixno,fl | _ -> assert false in
         let buri = 
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
@@ -307,18 +410,20 @@ let convert_term uri t =
         in
         let obj = 
           NUri.nuri_of_ouri buri,max_int,[],[],
-            NCic.Fixpoint (true, fl, (`Generated, `Definition)) 
+            NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
+        let r = Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in
+        let obj,r =
+         let _,name,_,_,_ = List.hd fl in
+         match find_in_cache name obj r with
+            Some r' -> [],r'
+          | None -> [obj],r
         in
-        splat_args ctx
-          (NCic.Const 
-            (Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno))))
-          n_fix,
-        fixpoints @ [obj]
+        splat_args ctx (NCic.Const r) n_fix rels, fixpoints @ obj
     | Cic.Rel n ->
         let bound, _, _, primo_ce_dopo_fix = context_tassonomy ctx in
         (match List.nth ctx (n-1) with
         | Fix (r,_,_) when n < primo_ce_dopo_fix -> 
-            splat_args_for_rel ctx (NCic.Const r), []
+            splat_args_for_rel ctx (NCic.Const r) n_fix, []
         | Ce _ when n <= bound -> NCic.Rel n, []
         | Fix _ when n <= bound -> assert false
         | Fix _ | Ce _ when k = true -> NCic.Rel n, []