implemented normalize (used in new_metasenv_for_apply)

[helm.git] / helm / ocaml / cic_proof_checking / cicReduction.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 35c89ae33e6f5c6fcf96f7247362d276ae830fb9..55ffb8edb99787b69b77fa2218caf8f96b0b21dd 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -513,7 +513,7 @@ if List.mem uri params then debug_print "---- 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 =
@@ -602,6 +602,9 @@ if List.mem uri params then debug_print "---- 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
@@ -762,8 +765,8 @@ if List.mem uri params then debug_print "---- OK2" ;
   ;;
   *)
 
-  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, [])
   ;;
 
   
@@ -1037,3 +1040,48 @@ 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.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
+  
+