parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_acic / doubleTypeInference.ml

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 1671b98d25321ca6492f8565715ba99d5ddfedba..4ca88d4b96a411318a6be88d2c6c1ef4d9e6302c 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -97,64 +97,72 @@ let rec does_not_occur n =
          ) fl true
 ;;
 
-let rec beta_reduce =
+(* FG: if ~clean:true, unreferenced letins are removed *)
+(*     (beta-reducttion can cause unreferenced letins) *)
+let rec beta_reduce ?(clean=false)=
  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, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean 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 (beta_reduce t)) l
+         (function None -> None | Some t -> Some (beta_reduce ~clean t)) l
        )
     | C.Sort _ as t -> t
     | C.Implicit _ -> assert false
     | C.Cast (te,ty) ->
-       C.Cast (beta_reduce te, beta_reduce ty)
+       C.Cast (beta_reduce ~clean te, beta_reduce ~clean ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, beta_reduce s, beta_reduce t)
+       C.Prod (n, beta_reduce ~clean s, beta_reduce ~clean t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, beta_reduce s, beta_reduce t)
+       C.Lambda (n, beta_reduce ~clean s, beta_reduce ~clean t)
     | C.LetIn (n,s,ty,t) ->
-       C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
+       let t' = beta_reduce ~clean t in
+       if clean && does_not_occur 1 t' then
+         (* since [Rel 1] does not occur in typ, substituting any term *)
+          (* in place of [Rel 1] is equivalent to delifting once        *)
+          CicSubstitution.subst (C.Implicit None) t'
+       else
+          C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t')
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
-         beta_reduce he'
+         beta_reduce ~clean he'
         else
          (match he' with
-             C.Appl l -> beta_reduce (C.Appl (l@tl))
-           | _ -> beta_reduce (C.Appl (he'::tl)))
+             C.Appl l -> beta_reduce ~clean (C.Appl (l@tl))
+           | _ -> beta_reduce ~clean (C.Appl (he'::tl)))
     | C.Appl l ->
-       C.Appl (List.map beta_reduce l)
+       C.Appl (List.map (beta_reduce ~clean) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean 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, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean 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, beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst
        in
         C.MutConstruct (uri,i,j,exp_named_subst')
     | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
-        List.map beta_reduce pl)
+       C.MutCase (sp,i,beta_reduce ~clean outt,beta_reduce ~clean t,
+        List.map (beta_reduce ~clean) pl)
     | C.Fix (i,fl) ->
        let fl' =
         List.map
          (function (name,i,ty,bo) ->
-           name,i,beta_reduce ty,beta_reduce bo
+           name,i,beta_reduce ~clean ty,beta_reduce ~clean bo
          ) fl
        in
         C.Fix (i,fl')
@@ -162,7 +170,7 @@ let rec beta_reduce =
        let fl' =
         List.map
          (function (name,ty,bo) ->
-           name,beta_reduce ty,beta_reduce bo
+           name,beta_reduce ~clean ty,beta_reduce ~clean bo
          ) fl
        in
         C.CoFix (i,fl')
@@ -339,17 +347,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
      | C.Lambda (n,s,t) ->
         (* Let's visit all the subterms that will not be visited later *)
          let _ = type_of_aux context s None in 
-         let expected_target_type =
+         let n, expected_target_type =
           match expectedty with
-             None -> None
+           | None -> n, None
            | Some expectedty' ->
-              let ty =
+              let n, ty =
                match R.whd context expectedty' with
-                  C.Prod (_,_,expected_target_type) ->
-                   beta_reduce expected_target_type
+                | C.Prod (n',_,expected_target_type) ->
+                   let xtt = beta_reduce expected_target_type in
+                  if n <> C.Anonymous then n, xtt else n', xtt
                 | _ -> assert false
               in
-               Some ty
+               n, Some ty
          in 
           let type2 =
            type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
@@ -366,8 +375,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           (* Checks suppressed *)
           type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
          in  (* CicSubstitution.subst s t_typ *)
-          if does_not_occur 1 t_typ then
-           (* since [Rel 1] does not occur in typ, substituting any term *)
+         if does_not_occur 1 t_typ then
+          (* since [Rel 1] does not occur in typ, substituting any term *)
            (* in place of [Rel 1] is equivalent to delifting once        *)
            CicSubstitution.subst (C.Implicit None) t_typ
           else
@@ -550,7 +559,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           let (_,ty,_) = List.nth fl i in
            ty
    in
-    let synthesized' = beta_reduce synthesized in
+(* FG: beta-reduction can cause unreferenced letins *)
+    let synthesized' = beta_reduce ~clean:true synthesized in
     let synthesized' = !pack_coercion metasenv context synthesized' in
      let types,res =
       match expectedty with