]> matita.cs.unibo.it Git - helm.git/commitdiff
new are_convertible and head_beta_reduce
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Mar 2008 17:56:20 +0000 (17:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Mar 2008 17:56:20 +0000 (17:56 +0000)
helm/software/components/ng_kernel/nCicReduction.ml
helm/software/components/ng_kernel/nCicReduction.mli

index 5bb6260ca57bb73a427b087c41a09129fb4c4b0f..64133384d5f9a511efa91439f8e3ae970bb53f64 100644 (file)
@@ -1,4 +1,5 @@
-(*  ||M||  This file is part of HELM, an Hypertextual, Electronic        
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
     ||A||  Library of Mathematics, developed at the Computer Science     
     ||T||  Department, University of Bologna, Italy.                     
     ||I||                                                                
@@ -497,27 +498,21 @@ let whd =
    profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
 *)
 
-(*
-
- (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
-  * fallbacks to structural equality *)
+(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+ * fallbacks to structural equality *)
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 module C = NCic
 
 (* t1, t2 must be well-typed *)
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
- let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 =
    let rec aux2 test_equality_only t1 t2 =
      if t1 === t2 then
        true
      else
        match (t1,t2) with
-       | (C.Rel n1, C.Rel n2) -> n1 = n2
-
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) when test_equality_only -> a=b
        | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
        | (C.Sort s1, C.Sort s2) -> s1 = s2
 
@@ -525,379 +520,99 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
            aux true context s1 s2 &&
            aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-          aux test_equality_only context s1 s2 && (* sure?! *)
-          aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
-
-       | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
-            if n1 = n2 then
-              let b2, ugraph1 = 
-                let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
-                let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
-                  List.fold_left2
-                    (fun (b,ugraph) t1 t2 ->
-                       if b then 
-                         match t1,t2 with
-                             None,_
-                           | _,None  -> true,ugraph
-                           | Some t1',Some t2' -> 
-                               aux test_equality_only context t1' t2' ugraph
-                       else
-                         false,ugraph
-                    ) (true,ugraph) l1 l2
-              in
-                if b2 then true,ugraph1 else false,ugraph 
-            else
-              false,ugraph
-        | C.Meta (n1,l1), _ ->
-           (try 
-              let _,term,_ = NCicUtils.lookup_subst n1 subst in
-              let term' = CicSubstitution.subst_meta l1 term in
-               aux test_equality_only context term' t2 ugraph
-            with  CicUtil.Subst_not_found _ -> false,ugraph)
-        | _, C.Meta (n2,l2) ->
-           (try 
-              let _,term,_ = CicUtil.lookup_subst n2 subst in
-              let term' = CicSubstitution.subst_meta l2 term in
-               aux test_equality_only context t1 term' ugraph
-            with  CicUtil.Subst_not_found _ -> false,ugraph)
-        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
-           if b' then
-            aux test_equality_only
-             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
-           else
-             false,ugraph
-        | (C.Appl l1, C.Appl l2) ->
-           (try
-             List.fold_right2
-               (fun  x y (b,ugraph) -> 
-                 if b then
-                   aux test_equality_only context x y ugraph
-                 else
-                   false,ugraph) l1 l2 (true,ugraph)
-            with
-             Invalid_argument _ -> false,ugraph
-           )
-        | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
-            let b' = U.eq uri1 uri2 in
-            if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  if b && U.eq uri1 uri2 then
-                    aux test_equality_only context x y ugraph 
-                  else
-                    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-            else
-              false,ugraph
-        | (C.MutInd (uri1,i1,exp_named_subst1),
-           C.MutInd (uri2,i2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-            if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  if b && U.eq uri1 uri2 then
-                    aux test_equality_only context x y ugraph
-                  else
-                   false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-            else 
-              false,ugraph
-        | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
-           C.MutConstruct (uri2,i2,j2,exp_named_subst2)
-          ) ->
-            let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
-            if b' then
-             (try
-               List.fold_right2
-                (fun (uri1,x) (uri2,y) (b,ugraph) ->
-                  if b && U.eq uri1 uri2 then
-                    aux test_equality_only context x y ugraph
-                  else
-                    false,ugraph
-                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
-              with
-               Invalid_argument _ -> false,ugraph
-             )
-            else
-              false,ugraph
-        | (C.MutCase (uri1,i1,outtype1,term1,pl1),
-           C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
-            let b' = U.eq uri1 uri2 && i1 = i2 in
-            if b' then
-             let b'',ugraph''=aux test_equality_only context 
-                 outtype1 outtype2 ugraph in
-             if b'' then 
-               let b''',ugraph'''= aux test_equality_only context 
-                   term1 term2 ugraph'' in
-               List.fold_right2
-                 (fun x y (b,ugraph) -> 
-                   if b then
-                     aux test_equality_only context x y ugraph 
-                   else 
-                     false,ugraph)
-                 pl1 pl2 (b''',ugraph''')
-             else
-               false,ugraph
-            else
-              false,ugraph
-        | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys,_ =
-              List.fold_left
-                (fun (types,len) (n,_,ty,_) ->
-                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-                    len+1)
-               ) ([],0) fl1
-            in
-            if i1 = i2 then
-             List.fold_right2
-              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
-                if b && recindex1 = recindex2 then
-                  let b',ugraph' = aux test_equality_only context ty1 ty2 
-                      ugraph in
-                  if b' then
-                    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-                  else
-                    false,ugraph
-                else
-                  false,ugraph)
-             fl1 fl2 (true,ugraph)
-            else
-              false,ugraph
-        | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-            let tys,_ =
-              List.fold_left
-                (fun (types,len) (n,ty,_) ->
-                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-                    len+1)
-               ) ([],0) fl1
-            in
-            if i1 = i2 then
-              List.fold_right2
-              (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
-                if b then
-                  let b',ugraph' = aux test_equality_only context ty1 ty2 
-                      ugraph in
-                  if b' then
-                    aux test_equality_only (tys@context) bo1 bo2 ugraph'
-                  else
-                    false,ugraph
-                else
-                  false,ugraph)
-             fl1 fl2 (true,ugraph)
-            else
-              false,ugraph
-        | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
-        | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
-        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
-        | (_,_) -> false,ugraph
+          aux true context s1 s2 && 
+          aux true ((name1, C.Decl s1)::context) t1 t2
+       | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+          aux test_equality_only context ty1 ty2 &&
+          aux test_equality_only context s1 s2 &&
+          aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2
+
+       | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2))) 
+          when n1 = n2 && s1 = s2 -> true
+       | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 -> 
+          let l1 = NCicUtils.expand_local_context l1 in
+          let l2 = NCicUtils.expand_local_context l2 in
+          (try List.for_all2 
+            (fun t1 t2 -> aux test_equality_only context 
+              (NCicSubstitution.lift s1 t1) 
+              (NCicSubstitution.lift s2 t2))  
+            l1 l2
+          with Invalid_argument _ -> false)
+
+       | C.Meta (n1,l1), _ ->
+          (try 
+             let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+             let term = NCicSubstitution.subst_meta l1 term in
+              aux test_equality_only context term t2
+           with NCicUtils.Subst_not_found _ -> false)
+       | _, C.Meta (n2,l2) ->
+          (try 
+             let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
+             let term = NCicSubstitution.subst_meta l2 term in
+              aux test_equality_only context t1 term
+           with NCicUtils.Subst_not_found _ -> false)
+
+       | (C.Appl l1, C.Appl l2) ->
+          (try List.for_all2 (aux test_equality_only context) l1 l2
+           with Invalid_argument _ -> false)
+
+       | (C.Match (ref1,outtype1,term1,pl1),
+          C.Match (ref2,outtype2,term2,pl2)) -> 
+           NReference.eq ref1 ref2 &&
+           aux test_equality_only context outtype1 outtype2 &&
+           aux test_equality_only context term1 term2 &&
+           (try List.for_all2 (aux test_equality_only context) pl1 pl2
+            with Invalid_argument _ -> false)
+
+       | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+       | (_,_) -> false
   in
-   let res =
-    if !heuristic then
-     aux2 test_equality_only t1 t2 ugraph
-    else
-     false,ugraph
-   in
-    if fst res = true then
-     res
-    else
-begin
-(*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
-   (* heuristic := false; *)
-   debug t1 [t2] "PREWHD";
-(*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
-(*
-prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
-   let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
-   let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
-    debug t1' [t2'] "POSTWHD";
-*)
-let rec convert_machines ugraph =
- function
-    [] -> true,ugraph
-  | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
-     let (b,ugraph) as res =
-      aux2 test_equality_only
-       (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
+   if aux2 test_equality_only t1 t2 then 
+     true
+   else
+     let rec convert_machines = function
+      | [] -> true
+      | ((k1,env1,h1,s1),(k2,env2,h2,s2))::tl ->
+          aux2 test_equality_only
+           (R.unwind (k1,env1,h1,[])) (R.unwind (k2,env2,h2,[])) &&
+          let problems =
+           let red_stack =
+             List.map
+               (fun si-> R.reduce ~delta:0 ~subst context(RS.from_stack si))
+           in
+           try Some (List.combine (red_stack s1) (red_stack s2) @ tl)
+           with Invalid_argument _ -> None
+          in
+          match problems with
+           | None -> false
+           | Some problems -> convert_machines problems
      in
-      if b then
-       let problems =
-        try
-         Some
-          (List.combine
-            (List.map
-              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
-              s1)
-            (List.map
-              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
-              s2)
-          @ tl)
-        with
-         Invalid_argument _ -> None
-       in
-        match problems with
-           None -> false,ugraph
-         | Some problems -> convert_machines ugraph problems
-      else
-       res
-in
- convert_machines 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');*)
-(*
-    aux2 test_equality_only t1' t2' ugraph
-*)
-end
+      convert_machines 
+       [R.reduce ~delta:0 ~subst context (0,[],t1,[]),
+        R.reduce ~delta:0 ~subst context (0,[],t2,[])]
  in
-  aux false (*c t1 t2 ugraph *)
+  aux false 
 ;;
-*)
 
-(* {{{ DEBUGGING ONLY
-let whd ?(delta=true) ?(subst=[]) context t = 
- let res = whd ~delta ~subst context t in
- let rescsc = CicReductionNaif.whd ~delta ~subst context t in
-  if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
-   begin
-    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
-    flush stderr ;
-    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
-    flush stderr ;
-    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
-    flush stderr ;
-fdebug := 0 ;
-let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
-    assert false ;
-   end
-  else 
-   res
+let are_convertible = are_convertible whd
+
+let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
+ match upto, t, l with
+  | 0, C.Appl l1, _ -> C.Appl (l1 @ l)
+  | 0, t, [] -> t
+  | 0, t, _ -> C.Appl (t::l)
+  | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
+  | _, C.Lambda(_,_,bo), arg::tl ->
+     let bo = NCicSubstitution.subst arg bo in
+     head_beta_reduce ~delta ~upto:(upto - 1) bo tl
+  | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _ 
+    when delta <= height ->
+      let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
+      head_beta_reduce ~upto ~delta bo l
+  | _, t, [] -> t
+  | _, t, _ -> C.Appl (t::l)
 ;;
- }}} *)
-
-(*let are_convertible = are_convertible whd*)
 
-(* {{{ let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
-let whd ?(delta=true) ?(subst=[]) context t = 
- let foo () =
-  whd ~delta ~subst context t
- in
-  profiler_other_whd.HExtlib.profile foo ()
- }}} *)
-
-(* {{{ 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
-  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) ->
-      (* the term is already in weak head normal form *)
-      assert false
-  | 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)
-(*CSC: to be completed, I suppose *)
-  | 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 ?(delta=false) ?(upto=(-1)) t =
- match upto with
-    0 -> t
-  | n ->
-    match t with
-       (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 ~delta ~upto:(upto - 1) he'''
-     | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
-     | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
-        let bo =
-         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-            Cic.Constant (_,bo,_,_,_) -> bo
-          | Cic.Variable _ -> raise ReferenceToVariable
-          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-        in
-         (match bo with
-             None -> t
-           | Some bo ->
-              head_beta_reduce ~upto
-               ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
-     | Cic.Const (uri,ens) as t when delta=true ->
-        let bo =
-         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-            Cic.Constant (_,bo,_,_,_) -> bo
-          | Cic.Variable _ -> raise ReferenceToVariable
-          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-        in
-         (match bo with
-             None -> t
-           | Some bo ->
-              head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
-     | t -> t
- }}} *)
-
-(* {{{
-let are_convertible ?subst ?metasenv context t1 t2 ugraph =
- let before = Unix.gettimeofday () in
- let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
- let after = Unix.gettimeofday () in
- let diff = after -. before in
-  if diff > 0.1 then
-   begin
-    let nc = List.map (function None -> None | Some (n,_) -> Some n) context in
-     prerr_endline
-      ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc);
-   end;
-  res
- }}} *)
+let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
 
 (* vim:set foldmethod=marker: *)
index 3677944bd6006290e6dcc2ba6bd796f5df65d282..a45d8422f8ead2bced870fb2a61f331803806233 100644 (file)
@@ -28,10 +28,9 @@ exception ReferenceToConstant
 exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
-(*
-val fdebug : int ref
+
 val whd : 
-  ?delta:bool -> ?subst:NCic.substitution -> 
+  ?delta:int -> ?subst:NCic.substitution -> 
   NCic.context -> NCic.term -> 
     NCic.term
 
@@ -39,11 +38,8 @@ val are_convertible :
   ?subst:NCic.substitution -> ?metasenv:NCic.metasenv -> 
   NCic.context -> NCic.term -> NCic.term -> 
   bool
-val normalize:
-  ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
+
 (* performs head beta/(delta)/cast reduction; the default is to not perform
    delta reduction; if provided, ~upto is the maximum number of beta redexes
    reduced *)
-val head_beta_reduce: ?delta:bool -> ?upto:int -> Cic.term -> Cic.term
-*)
+val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term