* (Head) beta reduction functions factorized

* the type inferred for a match both in the kernel and in the refiner
  are now beta reduced

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 63a8f550323a8ac9ad9fd8fd90b609158ef230f4..14b858491d8c55c8e4c9010ecb5781836e796845 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -1086,3 +1086,19 @@ let normalize ?delta ?subst ctx term =
   t
   
   
+(* performs an head beta/cast reduction *)
+let rec head_beta_reduce =
+ function
+    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+      let he'' = CicSubstitution.subst he' t in
+       if tl' = [] then
+        he''
+       else
+        let he''' =
+         match he'' with
+            Cic.Appl l -> Cic.Appl (l@tl')
+          | _ -> Cic.Appl (he''::tl')
+        in
+         head_beta_reduce he'''
+  | Cic.Cast (te,_) -> head_beta_reduce te
+  | t -> t

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli
index cd48a025b9b86937fa6f79e2ee4b25e26d103ac4..e3619053d0d2163add738b5ebe8039f0cc9b1fbe 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.mli
+++ b/helm/ocaml/cic_proof_checking/cicReduction.mli
@@ -38,3 +38,5 @@ val are_convertible :
 val normalize:
   ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
  
+(* performs an head beta/cast reduction *)
+val head_beta_reduce: Cic.term -> Cic.term

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index fbcf25f91450a4beb8ace412ba213dcfc0fa0d6c..6789c4dff8213acdf53d18aef9b286c0bd46744f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1766,12 +1766,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          if not need_dummy then
-            (C.Appl ((outtype::arguments)@[term])),ugraph5
-          else if arguments = [] then
-            outtype,ugraph5
-          else
-            (C.Appl (outtype::arguments)),ugraph5
+          let arguments =
+           if not need_dummy then outtype::arguments@[term]
+           else outtype::arguments in
+          let outtype =
+           if arguments = [] then outtype
+           else CicReduction.head_beta_reduce (C.Appl arguments)
+          in
+           outtype,ugraph5
    | C.Fix (i,fl) ->
       let types_times_kl,ugraph1 =
        (* WAS: list rev list map *)
@@ -2117,9 +2119,9 @@ let typecheck uri ugraph =
 
 (** wrappers which instantiate fresh loggers *)
 
-let type_of_aux' ?(subst = []) metasenv context t =
+let type_of_aux' ?(subst = []) metasenv context t ugraph =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger ~subst metasenv context t
+  type_of_aux' ~logger ~subst metasenv context t ugraph
 
 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
   let logger = new CicLogger.logger in

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 768255a1493db265c087ecad4355b934d8354b19..3b8e4ad221646ba6f0e949eb1250e2ba04e477bb 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -232,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
-(* CSC: old code that never performs beta reduction
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-      begin
-       match um_aux he with
-          Cic.Appl l -> Cic.Appl (l@tl')
-        | he' -> Cic.Appl (he'::tl')
-      end
-  in
-  apply_subst_gen ~appl_fun
-*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -252,18 +241,7 @@ let apply_subst =
     in
      begin
       match he with
-         Cic.Meta (m,_) ->
-          let rec beta_reduce =
-           function
-              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (Cic.Appl(he''::tl'))
-            | t -> t
-          in
-           beta_reduce t'
+         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
        | _ -> t'
      end
   in

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a9593c67fb617782815a6631fcc3cfa18c9b5f06..76642ee3d51e553309d67b6294e4a475761b4613 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -559,7 +559,9 @@ and type_of_aux' metasenv context t ugraph =
                        candidate outtype ugraph5
                    in
                      C.MutCase (uri, i, outtype, term', pl'),
-                       (Cic.Appl (outtype::right_args@[term'])),
+                      CicReduction.head_beta_reduce
+                       (CicMetaSubst.apply_subst subst
+                        (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
              let _,_, subst, metasenv,ugraph5 =
@@ -584,8 +586,9 @@ and type_of_aux' metasenv context t ugraph =
                  (subst,metasenv,ugraph5) outtypeinstances 
              in
                C.MutCase (uri, i, outtype, term', pl'),
-                 CicReduction.whd ~subst       context 
-                   (C.Appl(outtype::right_args@[term])),
+                 CicReduction.head_beta_reduce
+                  (CicMetaSubst.apply_subst subst
+                   (C.Appl(outtype::right_args@[term]))),
                  subst,metasenv,ugraph6)
        | C.Fix (i,fl) ->
            let fl_ty',subst,metasenv,types,ugraph1 =

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 5e2eaba0046fca7544454395852a995acc258ca6..7a67c8248e4e5d72d7986166cd5ec9f5401213cc 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -50,29 +50,6 @@ let type_of_aux' metasenv subst context term ugraph =
 let exists_a_meta l = 
   List.exists (function Cic.Meta _ -> true | _ -> false) l
 
-let rec beta_reduce =
-  function
-      (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-        let he'' = CicSubstitution.subst he' t in
-          if tl' = [] then
-            he''
-          else
-            beta_reduce (Cic.Appl(he''::tl'))
-    | t -> t
-(* 
-let rec deref subst =
-  let snd (_,a,_) = a in
-  function
-      Cic.Meta(n,l) as t -> 
-        (try 
-           deref subst
-             (CicSubstitution.subst_meta 
-                l (snd (CicUtil.lookup_subst n subst))) 
-         with 
-           CicUtil.Subst_not_found _ -> t)
-    | t -> t
-;; *)
-
 let rec deref subst t =
   let snd (_,a,_) = a in
   match t with
@@ -86,10 +63,10 @@ let rec deref subst t =
     | Cic.Appl(Cic.Meta(n,l)::args) ->
         (match deref subst (Cic.Meta(n,l)) with
            | Cic.Lambda _ as t -> 
-               deref subst (beta_reduce (Cic.Appl(t::args)))
+               deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
            | r -> Cic.Appl(r::args))
     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
-           deref subst (beta_reduce (Cic.Appl(t::args)))
+           deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
     | t -> t
 ;; 
 
@@ -481,7 +458,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
               (try 
                  let (_,t,_) = CicUtil.lookup_subst i subst in
                  let lifted = S.subst_meta l t in
-                 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                    fo_unif_subst 
                     test_equality_only 
                      subst context metasenv reduced t2 ugraph
@@ -496,7 +473,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
               (* (try 
                  let (_,t,_) = CicUtil.lookup_subst i subst in
                  let lifted = S.subst_meta l t in
-                 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                    fo_unif_subst 
                      test_equality_only 
                      subst context metasenv t1 reduced ugraph