]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed in handling of explicit named substitutions: it could happen that
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 May 2008 21:31:45 +0000 (21:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 May 2008 21:31:45 +0000 (21:31 +0000)
explicit named substitution are merged not in the expected order. This happens
comparing the case of an instantiation inside and outside a (nested) section.
Thus I have added back the re-ordering of the explicit named substitution in
CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have
added to CicTypechecker.type_of_aux' the check that verifies if an explicit
named substitution is ordered.

helm/software/components/cic_proof_checking/cicReduction.ml
helm/software/components/cic_proof_checking/cicSubstitution.ml
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/ng_kernel/TEST

index 11fd5123560b1f411bd8a77832c30a6db7150f01..5e02fdbaaa391d00705586a0df49d61d60b79a2a 100644 (file)
@@ -523,31 +523,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,
           in
            C.CoFix (i, substitutedfl)
      and substaux_in_exp_named_subst params exp_named_subst' m  =
-  (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
-      let ens' =
-       List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
-  (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
-        List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
-      in
-      let rec filter_and_lift =
-       function
-          [] -> []
-        | uri::tl ->
-           let r = filter_and_lift tl in
-            (try
-              (uri,(List.assq uri ens'))::r
-             with
-              Not_found -> r
-            )
-      in
-       filter_and_lift params
-  *)
-  
-  (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
-  (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
-  
-  (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
-  (*CSC: codice altamente inefficiente *)
+     (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
       let rec filter_and_lift already_instantiated =
        function
           [] -> []
@@ -562,18 +538,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,
             (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) ::
              (filter_and_lift (uri::already_instantiated) tl)
         | _::tl -> filter_and_lift already_instantiated 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, unwind_aux m t) exp_named_subst' @
-        (filter_and_lift [] (List.rev ens))
+       let res =
+        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
+         (filter_and_lift [] (List.rev ens))
+       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
       unwind_aux m t          
   
index 8d1dad9e2c2af09ccded670260c3b9c0b8971927..ba2c8f723146308b65967e5f69ac9c0f13cbe183 100644 (file)
@@ -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 =
@@ -230,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) -> 
@@ -311,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,
@@ -332,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
       [] -> []
@@ -345,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
index 35015e541202d36fe82a245ddd167e7322fc2c1c..88219ee37d2e9a95a05894db3fce055db3c156af 100644 (file)
@@ -1328,7 +1328,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-         check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+         check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph 
        in 
        let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
        let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
@@ -1441,7 +1441,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.Const (uri,exp_named_subst) ->
        incr fdebug ;
        let ugraph1 = 
-        check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger ~subst  context exp_named_subst ugraph 
        in
        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
        let cty1 =
@@ -1452,11 +1452,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.MutInd (uri,i,exp_named_subst) ->
       incr fdebug ;
        let ugraph1 = 
-        check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger  ~subst context exp_named_subst ugraph 
        in
-        (* TASSI: da me c'era anche questa, ma in CVS no *)
        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
-        (* fine parte dubbia *)
        let cty =
         CicSubstitution.subst_vars exp_named_subst mty
        in
@@ -1464,9 +1462,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
         cty,ugraph2
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let ugraph1 = 
-        check_exp_named_subst ~logger ~subst context exp_named_subst ugraph 
+        check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
        in
-        (* TASSI: idem come sopra *)
        let mty,ugraph2 = 
         type_of_mutual_inductive_constr ~logger uri i j ugraph1 
        in
@@ -1773,7 +1770,24 @@ end;
        let (_,ty,_) = List.nth fl i in
         ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context =
+ and check_exp_named_subst uri ~logger ~subst context ens ugraph =
+   let params =
+    let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    (match obj with
+        Cic.Constant (_,_,_,params,_) -> params
+      | Cic.Variable (_,_,_,params,_) -> params
+      | Cic.CurrentProof (_,_,_,_,params,_) -> params
+      | Cic.InductiveDefinition (_,params,_,_) -> params
+    ) in
+   let rec check_same_order params ens =
+    match params,ens with
+     | _,[] -> ()
+     | [],_::_ ->
+        raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
+     | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
+        check_same_order tl tl'
+     | _::tl,l -> check_same_order tl l
+   in
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
         [] -> ugraph
@@ -1799,7 +1813,8 @@ end;
                 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger []
+    check_same_order params ens ;
+    check_exp_named_subst_aux ~logger [] ens ugraph
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in
index 933460b8d976b6774eff10da64a4feb43ed3e11e..6f3d571a1c8468d4069443146dd6b8fb909f3186 100644 (file)
@@ -29,18 +29,18 @@ Rocq/COC: type-checking vecchio nucleo troppo lento
 nijmegen: type-checking vecchio nucleo troppo lento
 Sophia-Antipolis/Float: vecchio nucleo troppo lento
 Sophia-Antipolis/geometry: vecchio nucleo troppo lento
+Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo troppo lento
 
 matita/tests: nuovo nucleo problema con universi!!!
 
+cic:/Rocq/ALGEBRA/CATEGORY_THEORY/LIMITS/FunForget_UA/UA_FM.con: 15.17s vs 0.14s vecchio nucleo!
 coq: nuovo nucleo mooooolto lento in guarded by: cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
 orsay: nuovo nucleo diverge (vedi sopra)
 Sophia-Antipolis/Buchberger: nuovo nucleo diverge
 matita/freescale: nuovo nucleo diverge
 
-Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo: ???
-  cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con
-Sophia-Antipolis/Algebra: vecchio nucleo variabili
-lyon/PROCESSES: vecchio nucleo, variabili
+Sophia-Antipolis/Algebra: nuovo nucleo?
+lyon/PROCESSES: nuovo nucleo?
 
 lannion: nuovo nucleo impredicative set
 rocq.higman: nuovo nucleo impredicative set