fixed check, if 0 constructors then no List.nth is allowed

[helm.git] / helm / software / components / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml
index a30a036cb42dc7726c1720906d706f903b0fcf30..ba2c8f723146308b65967e5f69ac9c0f13cbe183 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicSubstitution.ml
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml
@@ -32,7 +32,13 @@ exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let debug_print = fun _ -> ()
+let debug = false
+let debug_print =
+ if debug then
+  fun m  -> prerr_endline (Lazy.force m)
+ else
+  fun _  -> ()
+;;
 
 let lift_from k n =
  let rec liftaux k =
@@ -62,7 +68,8 @@ let lift_from k n =
     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
     | C.Appl l -> C.Appl (List.map (liftaux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = 
@@ -108,7 +115,12 @@ let lift n t =
    lift_from 1 n t
 ;;
 
-let subst arg =
+(* subst t1 t2                                                         *)
+(* substitutes [t1] for [Rel 1] in [t2]                                *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes  *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true.                          *)
+let rec subst ?(avoid_beta_redexes=false) arg =
  let rec substaux k =
   let module C = Cic in
    function
@@ -137,13 +149,20 @@ let subst arg =
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k) tl in
         begin
          match substaux k he with
             C.Appl l -> C.Appl (l@tl')
+            (* Experimental *)
+          | C.Lambda (_,_,bo) when avoid_beta_redexes ->
+             (match tl' with
+                 [] -> assert false
+               | [he] -> subst ~avoid_beta_redexes he bo
+               | he::tl -> C.Appl (subst he bo::tl))
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false
@@ -217,19 +236,9 @@ debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
           in
-(*
-debug_print (lazy "\n\n---- BEGIN ") ;
-debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
-debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
-debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
-*)
            let exp_named_subst'' =
             substaux_in_exp_named_subst uri k exp_named_subst' params
            in
-(*
-debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
-debug_print (lazy "---- END\n\n ") ;
-*)
             C.Var (uri,exp_named_subst'')
        )
     | C.Meta (i, l) -> 
@@ -246,7 +255,8 @@ debug_print (lazy "---- END\n\n ") ;
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k) tl in
@@ -297,6 +307,14 @@ debug_print (lazy "---- END\n\n ") ;
         let exp_named_subst'' =
          substaux_in_exp_named_subst uri k exp_named_subst' params
         in
+if (List.map fst exp_named_subst'' <> List.map fst (List.filter (fun (uri,_) -> List.mem uri params) exp_named_subst) @ List.map fst exp_named_subst') then (
+debug_print (lazy "\n\n---- BEGIN ") ;
+debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
+debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
+debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
+debug_print (lazy "---- END\n\n ") ;
+);
          C.MutConstruct (uri,typeno,consno,exp_named_subst'')
     | C.MutCase (sp,i,outt,t,pl) ->
        C.MutCase (sp,i,substaux k outt, substaux k t,
@@ -318,8 +336,6 @@ debug_print (lazy "---- END\n\n ") ;
        in
         C.CoFix (i, substitutedfl)
  and substaux_in_exp_named_subst uri k exp_named_subst' params =
-(*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
-(*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
   let rec filter_and_lift =
    function
       [] -> []
@@ -331,18 +347,24 @@ debug_print (lazy "---- END\n\n ") ;
        ->
         (uri,lift (k-1) t)::(filter_and_lift tl)
     | _::tl -> filter_and_lift tl
-(*
-    | (uri,_)::tl ->
-debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
-exp_named_subst' then debug_print (lazy "---- OK1") ;
-debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
-if List.mem uri params then debug_print (lazy "---- OK2") ;
-        filter_and_lift tl
-*)
   in
-   List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
-    (filter_and_lift exp_named_subst)
+   let res =
+    List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
+     (filter_and_lift exp_named_subst)
+   in
+    let rec reorder =
+     function
+        [] -> []
+      | uri::tl ->
+         let he =
+          try
+           [uri,List.assoc uri res]
+          with
+           Not_found -> []
+         in
+          he@reorder tl
+    in
+     reorder params
  in
   if exp_named_subst = [] then t
   else substaux 1 t
@@ -387,7 +409,7 @@ let subst_meta l t =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
@@ -426,3 +448,4 @@ let subst_meta l t =
   aux 0 t          
 ;;
 
+Deannotate.lift := lift;;