X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=4dcf01c53b1a43f2793cf29ca374e456cbdba62c;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=655c8f17a06708990d5fcff0a9441a41073a04e0;hpb=0bd584a839bae570f44c4a5f8a06cdbc55fe0726;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 655c8f17a..4dcf01c53 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -22,14 +22,23 @@ let map_term_fold_a g k f a = function
  | C.Rel _ as t -> a,t
  | C.Appl [] | C.Appl [_] -> assert false
  | C.Appl l as orig ->
-    let a,l = 
+    let fire_beta, upto = 
+      match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 
+    in
+    let a,l1 = 
       (* sharing fold? *)
-      List.fold_right (fun t (a,l) -> let a,t = f k a t in a, t :: l) l (a,[])
+      List.fold_right 
+        (fun t (a,l) -> let a,t = f k a t in a, t :: l) 
+        l (a,[])
     in
-    a, (match l with
-       | C.Appl l :: tl -> C.Appl (l@tl)
-       | l1 when l == l1 -> orig
-       | l1 -> C.Appl l1)
+    a, if l1 == l then orig else 
+       let t =
+        match l1 with
+         | C.Appl l :: tl -> C.Appl (l@tl)
+         | _ -> C.Appl l1
+       in
+        if fire_beta then NCicReduction.head_beta_reduce ~upto t
+        else t
  | C.Prod (n,s,t) as orig ->
      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
      a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
@@ -71,3 +80,18 @@ let metas_of_term subst context term =
     HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
 ;;
 
+module NCicHash =
+ Hashtbl.Make
+  (struct
+    type t = C.term
+    let equal = (==)
+    let hash = Hashtbl.hash_param 100 1000 
+   end)
+;;
+
+let mk_appl he args = 
+  if args = [] then he else
+  match he with
+  | NCic.Appl l -> NCic.Appl (l@args)
+  | _ -> NCic.Appl (he::args)
+;;