a non necessary but morally required change. The matched term in

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

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 32ae57a4709a18ebd35690fbed84564238468ac2..6e34360850caf0f2f5f48f85cee3c65e060833c7 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -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          
   
@@ -887,19 +869,16 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
 *)
                aux test_equality_only context t1 term' ugraph
             with  CicUtil.Subst_not_found _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-            (try
-              true,(CicUniv.add_eq t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-            (try
-              true,(CicUniv.add_ge t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-          (* TASSI: CONSTRAINTS *)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) 
+          when test_equality_only ->
+            (try true,(CicUniv.add_eq t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2))
+          when not test_equality_only ->
+            (try true,(CicUniv.add_ge t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort s1, C.Sort (C.Type _))
+        | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph
         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
             let b',ugraph' = aux true context s1 s2 ugraph in
@@ -909,7 +888,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+           let b',ugraph' = aux true context s1 s2 ugraph in
            if b' then
              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
                t1 t2 ugraph'
@@ -927,13 +906,18 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
            else
              false,ugraph
         | (C.Appl l1, C.Appl l2) ->
+           let b, ugraph = 
+             aux test_equality_only context (List.hd l1) (List.hd l2) ugraph
+           in
+           if not b then false, ugraph
+           else
            (try
              List.fold_right2
                (fun  x y (b,ugraph) -> 
                  if b then
-                   aux test_equality_only context x y ugraph
+                   aux true context x y ugraph
                  else
-                   false,ugraph) l1 l2 (true,ugraph)
+                   false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph)
             with
              Invalid_argument _ -> false,ugraph
            )
@@ -996,7 +980,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
              let b'',ugraph''=aux test_equality_only context 
                  outtype1 outtype2 ugraph in
              if b'' then 
-               let b''',ugraph'''= aux test_equality_only context 
+               let b''',ugraph'''= aux true context 
                    term1 term2 ugraph'' in
                List.fold_right2
                  (fun x y (b,ugraph) -> 
@@ -1081,7 +1065,7 @@ prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
 *)
-let rec convert_machines ugraph =
+let rec convert_machines test_equality_only ugraph =
  function
     [] -> true,ugraph
   | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
@@ -1106,11 +1090,11 @@ let rec convert_machines ugraph =
        in
         match problems with
            None -> false,ugraph
-         | Some problems -> convert_machines ugraph problems
+         | Some problems -> convert_machines true ugraph problems
       else
        res
 in
- convert_machines ugraph
+ convert_machines test_equality_only ugraph
   [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
    R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)