From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 09:57:58 +0000 (+0000)
Subject: type_of_branch ported and optimized to not lift the outty every Prod, keep the
X-Git-Tag: make_still_working~5459
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=54f3a0239cb6cee6176a475070cc70f309a82819;hp=0fae7e0c93edd15c8e7f9f8330721f94388100ad;p=helm.git

type_of_branch ported and optimized to not lift the outty every Prod, keep the
number of passes binders and lift it just once
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 1760c57e4..920a2078e 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -517,33 +517,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
              args coInductiveTypeURI
          ) fl true
 
-and type_of_branch ~subst context argsno need_dummy outtype term constype =
- let module C = Cic in
- let module R = CicReduction in
-  match R.whd ~subst context constype with
-     C.MutInd (_,_,_) ->
-      if need_dummy then
-       outtype
-      else
-       C.Appl [outtype ; term]
-   | C.Appl (C.MutInd (_,_,_)::tl) ->
-      let (_,arguments) = split tl argsno
-      in
-       if need_dummy && arguments = [] then
-        outtype
-       else
-        C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
-   | C.Prod (name,so,de) ->
-      let term' =
-       match CicSubstitution.lift 1 term with
-          C.Appl l -> C.Appl (l@[C.Rel 1])
-        | t -> C.Appl [t ; C.Rel 1]
-      in
-       C.Prod (name,so,type_of_branch ~subst
-        ((Some (name,(C.Decl so)))::context) argsno need_dummy
-        (CicSubstitution.lift 1 outtype) term' de)
-   | _ -> raise (AssertFailure (lazy "20"))
-
  and returns_a_coinductive ~subst context ty =
   let module C = Cic in
    match CicReduction.whd ~subst context ty with
@@ -830,7 +803,7 @@ let rec typeof ~subst ~metasenv context term =
               let ty_p = typeof_aux context p in
               let ty_cons = typeof_aux context cons in
               let ty_branch = 
-                type_of_branch ~subst context leftno outtype cons ty_cons in
+                type_of_branch ~subst context leftno outtype cons ty_cons 0 in
               j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch 
             else
               j,false
@@ -846,7 +819,22 @@ let rec typeof ~subst ~metasenv context term =
           R.head_beta_reduce (C.Appl res)
     | C.Match _ -> assert false
 
-  and type_of_branch ~subst context leftno outty cons tycons = assert false
+  and type_of_branch ~subst context leftno outty cons tycons liftno = 
+    match R.whd ~subst context tycons with
+    | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
+    | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) ->
+        let _,arguments = HExtlib.split_nth leftno tl in
+        C.Appl (S.lift liftno outty::arguments@[cons])
+    | C.Prod (name,so,de) ->
+        let cons =
+         match S.lift 1 cons with
+         | C.Appl l -> C.Appl (l@[C.Rel 1])
+         | t -> C.Appl [t ; C.Rel 1]
+        in
+         C.Prod (name,so,
+           type_of_branch ~subst ((name,(C.Decl so))::context) 
+            leftno outty cons de (liftno+1))
+    | _ -> raise (AssertFailure (lazy "type_of_branch"))
 
   (* check_metasenv_consistency checks that the "canonical" context of a
      metavariable is consitent - up to relocation via the relocation list l -
@@ -1107,7 +1095,6 @@ and split_prods ~subst context n te =
        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
   | _ -> raise (AssertFailure (lazy "split_prods"))
 
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
 and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
  match R.whd ~subst context te with
  | C.Rel m when List.mem m safes -> true
@@ -1120,6 +1107,7 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
  | C.Appl (he::_) ->
     (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
     (*CSC: solo perche' non abbiamo trovato controesempi            *)
+    (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
     is_really_smaller ~subst k he
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false