Experimental commit: definitions are now allowed in contexts. As a consequence,

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 52f07e4dc2411d8b8aa63a75fcb290c3ebefe044..94e5b353de3534df42cba3016327de56abffdd6c 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -59,7 +59,11 @@ let replace ~what ~with_what ~where =
     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-    | C.Appl l -> C.Appl (List.map aux l)
+    | C.Appl l ->
+       (* Invariant enforced: no application of an application *)
+       (match List.map aux l with
+           (C.Appl l')::tl -> C.Appl (l'@tl)
+         | l' -> C.Appl l')
     | C.Const _ as t -> t
     | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
@@ -87,7 +91,7 @@ let replace ~what ~with_what ~where =
 
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
-let reduce =
+let reduce context =
  let rec reduceaux l =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -242,10 +246,7 @@ let reduce =
        in
         if l = [] then t' else C.Appl (t'::l)
  in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
   reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
 ;;
 
 exception WrongShape;;
@@ -273,7 +274,7 @@ exception WhatShouldIDo;;
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
 (*CSC: It does not perform simplification in a Case *)
-let simpl =
+let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (*reduce, but for the const case.                             *) 
  (**** Step 1 ****)
@@ -336,7 +337,7 @@ let simpl =
                       with
                        _ -> raise AlreadySimplified
                      in
-                      (match CicReduction.whd recparam with
+                      (match CicReduction.whd context recparam with
                           C.MutConstruct _
                         | C.Appl ((C.MutConstruct _)::_) ->
                            let body' =
@@ -361,7 +362,7 @@ let simpl =
                    [] -> C.Const (uri,cookingsno)
                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
                in
-                let reduced_term_to_fold = reduce term_to_fold in
+                let reduced_term_to_fold = reduce context term_to_fold in
 prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
 prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
                  replace reduced_term_to_fold term_to_fold res