X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=14b858491d8c55c8e4c9010ecb5781836e796845;hb=ed9af5a10b66343f817a1f9eac3add29e4b2baae;hp=687a46549a5455f2253b085c4f83b49a552fd55d;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 687a46549..14b858491 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -33,6 +33,8 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let debug_print = fun _ -> ()
+
 let fdebug = ref 1;;
 let debug t env s =
  let rec debug_aux t i =
@@ -41,7 +43,7 @@ let debug t env s =
    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
-   prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+   debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
 ;;
 
 module type Strategy =
@@ -347,7 +349,7 @@ module Reduction(RS : Strategy) =
             )
        | C.Var (uri,exp_named_subst) ->
 (*
-prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
 *)
          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
@@ -493,10 +495,11 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
         | _::tl -> filter_and_lift already_instantiated tl
 (*
         | (uri,_)::tl ->
-prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
-if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ;
-prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then prerr_endline "---- OK2" ;
+debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
+exp_named_subst' then debug_print "---- OK1" ;
+debug_print ("++++ 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 "---- OK2" ;
         filter_and_lift tl
 *)
       in
@@ -510,7 +513,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
    unwind' 0 
   ;;
   
-  let reduce ?(subst = []) context : config -> Cic.term = 
+  let reduce ~delta ?(subst = []) context : config -> Cic.term = 
    let module C = Cic in
    let module S = CicSubstitution in 
    let rec reduce =
@@ -599,6 +602,9 @@ if List.mem uri params then prerr_endline "---- OK2" ;
      | (k, e, ens, C.Appl l, s) ->
          C.Appl (List.append (List.map (unwind k e ens) l) s)
   *)
+     | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
+           let t' = unwind k e ens t in
+           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
         (let o,_ = 
 	   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
@@ -754,13 +760,13 @@ if List.mem uri params then prerr_endline "---- OK2" ;
     try 
       reduce context (0, [], [], t, [])
     with Not_found -> 
-      prerr_endline (CicPp.ppterm t) ; 
+      debug_print (CicPp.ppterm t) ; 
       raise Not_found
   ;;
   *)
 
-  let rec whd ?(subst=[]) context t = 
-    reduce ~subst context (0, [], [], t, [])
+  let rec whd ?(delta=true) ?(subst=[]) context t = 
+    reduce ~delta ~subst context (0, [], [], t, [])
   ;;
 
   
@@ -770,11 +776,11 @@ let whd context t =
  let rescsc = CicReductionNaif.whd context t in
   if not (CicReductionNaif.are_convertible context res rescsc) then
    begin
-    prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ;
+    debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
     flush stderr ;
-    prerr_endline ("DOPO: " ^ CicPp.ppterm res) ;
+    debug_print ("DOPO: " ^ CicPp.ppterm res) ;
     flush stderr ;
-    prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ;
+    debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
     flush stderr ;
 CicReductionNaif.fdebug := 0 ;
 let _ =  CicReductionNaif.are_convertible context res rescsc in
@@ -1020,10 +1026,10 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
      (* 
      (match t1 with 
 	 Cic.Meta _ -> 
-	   prerr_endline (CicPp.ppterm t1);
-	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
-	   prerr_endline (CicPp.ppterm t2);
-	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
+	   debug_print (CicPp.ppterm t1);
+	   debug_print (CicPp.ppterm (whd ~subst context t1));
+	   debug_print (CicPp.ppterm t2);
+	   debug_print (CicPp.ppterm (whd ~subst context t2))
        | _ -> ()); *)
      let t1' = whd ~subst context t1 in
      let t2' = whd ~subst context t2 in
@@ -1034,3 +1040,65 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
   aux false (*c t1 t2 ugraph *)
 ;;
 
+
+let rec normalize ?(delta=true) ?(subst=[]) ctx term =
+  let module C = Cic in
+  let t = whd ~delta ~subst ctx term in
+  let aux = normalize ~delta ~subst in
+  let decl name t = Some (name, C.Decl t) in
+  let def  name t = Some (name, C.Def (t,None)) in
+  match t with
+  | C.Rel n -> t
+  | C.Var (uri,exp_named_subst) ->
+      C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+  | C.Meta (i,l) -> 
+      C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
+  | C.Sort _ -> t
+  | C.Implicit _ -> t
+  | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
+  | C.Prod (n,s,t) -> 
+      let s' = aux ctx s in
+      C.Prod (n, s', aux ((decl n s')::ctx) t)
+  | C.Lambda (n,s,t) -> 
+      let s' = aux ctx s in
+      C.Lambda (n, s', aux ((decl n s')::ctx) t)
+  | C.LetIn (n,s,t) ->
+      let s' = aux ctx s in
+      C.LetIn (n, s, aux ((def n s')::ctx) t)
+  | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
+  | C.Appl [] -> assert false
+  | C.Const (uri,exp_named_subst) ->
+      C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+  | C.MutInd (uri,typeno,exp_named_subst) ->
+      C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+  | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+      C.MutConstruct (uri, typeno, consno, 
+        List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
+  | C.MutCase (sp,i,outt,t,pl) ->
+      C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+  | C.Fix _ -> t 
+  | C.CoFix _ -> t
+
+let normalize ?delta ?subst ctx term =  
+(*  prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
+  let t = normalize ?delta ?subst ctx term in
+(*  prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
+  t
+  
+  
+(* performs an head beta/cast reduction *)
+let rec head_beta_reduce =
+ function
+    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+      let he'' = CicSubstitution.subst he' t in
+       if tl' = [] then
+        he''
+       else
+        let he''' =
+         match he'' with
+            Cic.Appl l -> Cic.Appl (l@tl')
+          | _ -> Cic.Appl (he''::tl')
+        in
+         head_beta_reduce he'''
+  | Cic.Cast (te,_) -> head_beta_reduce te
+  | t -> t