head_beta_reduce used to create applications of applications. Fixed.

head_beta_reduce renamed to beta_reduce (since it performs full beta reduction).

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 6bfced57e2ad69ed44982773a8bdb85961372ff1..7f09da68918ed5b886cfc2532abf405371db55dc 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -105,64 +105,64 @@ let rec does_not_occur n =
          ) fl true
 ;;
 
-(*CSC: potrebbe creare applicazioni di applicazioni *)
-(*CSC: ora non e' piu' head, ma completa!!! *)
-let rec head_beta_reduce =
+let rec beta_reduce =
  let module S = CicSubstitution in
  let module C = Cic in
   function
       C.Rel _ as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.Var (uri,exp_named_subst)
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
-         (function None -> None | Some t -> Some (head_beta_reduce t)) l
+         (function None -> None | Some t -> Some (beta_reduce t)) l
        )
     | C.Sort _ as t -> t
     | C.Implicit _ -> assert false
     | C.Cast (te,ty) ->
-       C.Cast (head_beta_reduce te, head_beta_reduce ty)
+       C.Cast (beta_reduce te, beta_reduce ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+       C.Prod (n, beta_reduce s, beta_reduce t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+       C.Lambda (n, beta_reduce s, beta_reduce t)
     | C.LetIn (n,s,t) ->
-       C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+       C.LetIn (n, beta_reduce s, beta_reduce t)
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
-         head_beta_reduce he'
+         beta_reduce he'
         else
-         head_beta_reduce (C.Appl (he'::tl))
+         (match he' with
+             C.Appl l -> beta_reduce (C.Appl (l@tl))
+           | _ -> beta_reduce (C.Appl (he'::tl)))
     | C.Appl l ->
-       C.Appl (List.map head_beta_reduce l)
+       C.Appl (List.map beta_reduce l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri,i,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.MutInd (uri,i,exp_named_subst')
     | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.MutConstruct (uri,i,j,exp_named_subst')
     | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
-        List.map head_beta_reduce pl)
+       C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
+        List.map beta_reduce pl)
     | C.Fix (i,fl) ->
        let fl' =
         List.map
          (function (name,i,ty,bo) ->
-           name,i,head_beta_reduce ty,head_beta_reduce bo
+           name,i,beta_reduce ty,beta_reduce bo
          ) fl
        in
         C.Fix (i,fl')
@@ -170,7 +170,7 @@ let rec head_beta_reduce =
        let fl' =
         List.map
          (function (name,ty,bo) ->
-           name,head_beta_reduce ty,head_beta_reduce bo
+           name,beta_reduce ty,beta_reduce bo
          ) fl
        in
         C.CoFix (i,fl')
@@ -405,7 +405,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
      | C.Implicit _ -> raise (Impossible 21)
      | C.Cast (te,ty) ->
         (* Let's visit all the subterms that will not be visited later *)
-        let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
+        let _ = type_of_aux context te (Some (beta_reduce ty)) in
         let _ = type_of_aux context ty None in
          (* Checks suppressed *)
          ty
@@ -423,7 +423,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               let ty =
                match R.whd context expectedty' with
                   C.Prod (_,_,expected_target_type) ->
-                   head_beta_reduce expected_target_type
+                   beta_reduce expected_target_type
                 | _ -> assert false
               in
                Some ty
@@ -453,7 +453,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         let expected_hetype =
          (* Inefficient, the head is computed twice. But I know *)
          (* of no other solution. *)                               
-         (head_beta_reduce
+         (beta_reduce
           (R.whd context (xxx_type_of_aux' metasenv context he)))
         in 
          let hetype = type_of_aux context he (Some expected_hetype) in 
@@ -462,7 +462,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               _,[] -> []
             | C.Prod (n,s,t),he::tl ->
-               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+               (he, type_of_aux context he (Some (beta_reduce s)))::
                 (aux (R.whd context (S.subst he t), tl))
             | _ -> assert false
           in
@@ -473,7 +473,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               _,[] -> []
             | C.Prod (n,s,t),he::tl ->
-               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+               (he, type_of_aux context he (Some (beta_reduce s)))::
                 (aux (R.whd context (S.subst he t), tl))
             | _ -> assert false
           in
@@ -521,7 +521,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          in
           match
            R.whd context (type_of_aux context term
-            (Some (head_beta_reduce type_of_term)))
+            (Some (beta_reduce type_of_term)))
           with
              (*CSC manca il caso dei CAST *)
              C.MutInd (uri',i',exp_named_subst) ->
@@ -562,7 +562,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                   (xxx_type_of_aux' metasenv context cons)
                in
                 ignore (type_of_aux context p
-                 (Some (head_beta_reduce expectedtype))) ;
+                 (Some (beta_reduce expectedtype))) ;
                 j+1
             ) 1 (List.combine pl cl)
           in
@@ -588,7 +588,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           List.iter
            (fun (_,_,ty,bo) ->
              let expectedty =
-              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+              beta_reduce (CicSubstitution.lift (List.length fl) ty)
              in
               ignore (type_of_aux context' bo (Some expectedty))
            ) fl
@@ -612,7 +612,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           List.iter
            (fun (_,ty,bo) ->
              let expectedty =
-              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+              beta_reduce (CicSubstitution.lift (List.length fl) ty)
              in
               ignore (type_of_aux context' bo (Some expectedty))
            ) fl
@@ -621,7 +621,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           let (_,ty,_) = List.nth fl i in
            ty
    in
-    let synthesized' = head_beta_reduce synthesized in
+    let synthesized' = beta_reduce synthesized in
      let types,res =
       match expectedty with
          None ->