From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 25 Sep 2008 15:39:26 +0000 (+0000)
Subject: beta expand
X-Git-Tag: make_still_working~4739
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84a5fc74efc30a2b2fca18726cf988edd356353e;p=helm.git

beta expand
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 29851b5d4..fa3ba4988 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -44,201 +44,69 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  =
  try
   match before_beta_expansion,after_beta_expansion_body with
-     Cic.Appl l, Cic.Appl l' ->
-      let rec all_but_last check_last =
-       function
-          [] -> assert false
-        | [Cic.Rel 1] -> []
+  | NCic.Appl l1, NCic.Appl l2 ->
+      let rec all_but_last check_last = function
+        | [] -> assert false
+        | [NCic.Rel 1] -> []
         | [_] -> if check_last then raise WrongShape else []
         | he::tl -> he::(all_but_last check_last tl)
       in
-       let all_but_last check_last l =
+      let all_but_last check_last l =
         match all_but_last check_last l with
-           [] -> assert false
-         | [he] -> he
-         | l -> Cic.Appl l
-       in
-       let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
-       let all_but_last = all_but_last false l in
-        (* here we should test alpha-equivalence; however we know by
-           construction that here alpha_equivalence is equivalent to = *)
-        if t = all_but_last then
-         all_but_last
-        else
-         after_beta_expansion
-   | _,_ -> after_beta_expansion
- with
-  WrongShape -> after_beta_expansion
+        | [] -> assert false
+        | [he] -> he
+        | l -> NCic.Appl l
+      in
+      let t = 
+        NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
+      let all_but_last = all_but_last false l in
+      if t = all_but_last then all_but_last else after_beta_expansion
+  | _ -> after_beta_expansion
+ with WrongShape -> after_beta_expansion
+;;
 
-let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
- let module S = CicSubstitution in
- let module C = Cic in
-let foo () =
-  let rec aux metasenv subst n context t' ugraph =
+let rec beta_expand num test_equality_only metasenv subst context t arg =
+  let rec aux (n,context as k) (metasenv, subst as acc) t' =
    try
-
-    let subst,metasenv,ugraph1 =
-     fo_unif_subst test_equality_only subst context metasenv 
-      (CicSubstitution.lift n arg) t' ugraph
-
+    let metasenv, subst =
+     unify (* test_equality_only *) metasenv subst context
+      (NCicSubstitution.lift n arg) t'
     in
-     subst,metasenv,C.Rel (1 + n),ugraph1
-   with
-      Uncertain _
-    | UnificationFailure _ ->
+     (metasenv, subst), C.Rel (1 + n)
+   with Uncertain _ | UnificationFailure _ ->
        match t' with
-        | C.Rel m  -> subst,metasenv, 
-           (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
-        | C.Var (uri,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst',ugraph1 =
-            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
-           in
-            subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
-        | C.Meta (i,l) ->
-            (* andrea: in general, beta_expand can create badly typed
-             terms. This happens quite seldom in practice, UNLESS we
-             iterate on the local context. For this reason, we renounce
-             to iterate and just lift *)
-            let l = 
-              List.map 
-                (function
-                     Some t -> Some (CicSubstitution.lift 1 t)
-                   | None -> None) l in
-            subst, metasenv, C.Meta (i,l), ugraph
-        | C.Sort _
-        | C.Implicit _ as t -> subst,metasenv,t,ugraph
-        | C.Cast (te,ty) ->
-            let subst,metasenv,te',ugraph1 = 
-              aux metasenv subst n context te ugraph in
-            let subst,metasenv,ty',ugraph2 = 
-              aux metasenv subst n context ty ugraph1 in 
-            (* TASSI: sure this is in serial? *)
-            subst,metasenv,(C.Cast (te', ty')),ugraph2
-        | C.Prod (nn,s,t) ->
-           let subst,metasenv,s',ugraph1 = 
-             aux metasenv subst n context s ugraph in
-           let subst,metasenv,t',ugraph2 =
-             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t 
-               ugraph1
-           in
-           (* TASSI: sure this is in serial? *)
-           subst,metasenv,(C.Prod (nn, s', t')),ugraph2
-        | C.Lambda (nn,s,t) ->
-           let subst,metasenv,s',ugraph1 = 
-             aux metasenv subst n context s ugraph in
-           let subst,metasenv,t',ugraph2 =
-            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
-           in
-           (* TASSI: sure this is in serial? *)
-            subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
-        | C.LetIn (nn,s,ty,t) ->
-           let subst,metasenv,s',ugraph1 = 
-             aux metasenv subst n context s ugraph in
-           let subst,metasenv,ty',ugraph1 = 
-             aux metasenv subst n context ty ugraph in
-           let subst,metasenv,t',ugraph2 =
-            aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
-              ugraph1
-           in
-           (* TASSI: sure this is in serial? *)
-            subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
-        | C.Appl l ->
-           let subst,metasenv,revl',ugraph1 =
-            List.fold_left
-             (fun (subst,metasenv,appl,ugraph) t ->
-               let subst,metasenv,t',ugraph1 = 
-                 aux metasenv subst n context t ugraph in
-                subst,metasenv,(t'::appl),ugraph1
-             ) (subst,metasenv,[],ugraph) l
-           in
-            subst,metasenv,(C.Appl (List.rev revl')),ugraph1
-        | C.Const (uri,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst',ugraph1 =
-            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
-           in
-            subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
-        | C.MutInd (uri,i,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst',ugraph1 =
-            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
-           in
-            subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
-        | C.MutConstruct (uri,i,j,exp_named_subst) ->
-           let subst,metasenv,exp_named_subst',ugraph1 =
-            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
-           in
-            subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
-        | C.MutCase (sp,i,outt,t,pl) ->
-           let subst,metasenv,outt',ugraph1 = 
-             aux metasenv subst n context outt ugraph in
-           let subst,metasenv,t',ugraph2 = 
-             aux metasenv subst n context t ugraph1 in
-           let subst,metasenv,revpl',ugraph3 =
-            List.fold_left
-             (fun (subst,metasenv,pl,ugraph) t ->
-               let subst,metasenv,t',ugraph1 = 
-                 aux metasenv subst n context t ugraph in
-               subst,metasenv,(t'::pl),ugraph1
-             ) (subst,metasenv,[],ugraph2) pl
-           in
-           subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
-           (* TASSI: not sure this is serial *)
-        | C.Fix (i,fl) ->
-(*CSC: not implemented
-           let tylen = List.length fl in
-            let substitutedfl =
-             List.map
-              (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
-               fl
-            in
-             C.Fix (i, substitutedfl)
-*)
-            subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
-        | C.CoFix (i,fl) ->
-(*CSC: not implemented
-           let tylen = List.length fl in
-            let substitutedfl =
-             List.map
-              (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
-               fl
-            in
-             C.CoFix (i, substitutedfl)
+       | NCic.Rel m  -> 
+           (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
+       (* andrea: in general, beta_expand can create badly typed
+        terms. This happens quite seldom in practice, UNLESS we
+        iterate on the local context. For this reason, we renounce
+        to iterate and just lift *)
+       | NCic.Meta (i,(shift,lc)) ->
+           (metasenv,subst), NCic.Meta (i,(shift+1,lc))
+       | t -> 
+           NCicUntrusted.map_term_fold_a 
+             (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
 
-*) 
-            subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
-
-  and aux_exp_named_subst metasenv subst n context ens ugraph =
-   List.fold_right
-    (fun (uri,t) (subst,metasenv,l,ugraph) ->
-      let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
-       subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
   in
-  let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
-  let fresh_name =
-   FreshNamesGenerator.mk_fresh_name ~subst
-    metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
-  in
-   let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
-   let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
-   subst, metasenv, t'', ugraph2
-in profiler_beta_expand.HExtlib.profile foo ()
-
+  let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
+  let fresh_name = "Hbeta" ^ string_of_int num in
+  let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
+  let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
+  metasenv, subst, t
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
-  let _,subst,metasenv,hd,ugraph =
+  let _, subst, metasenv, hd =
     List.fold_right
-      (fun arg (num,subst,metasenv,t,ugraph) ->
-         let subst,metasenv,t,ugraph1 =
-           beta_expand num test_equality_only 
-             metasenv subst context t arg ugraph 
+      (fun arg (num,subst,metasenv,t) ->
+         let subst, metasenv, t =
+           beta_expand num test_equality_only metasenv subst context t arg
          in
-           num+1,subst,metasenv,t,ugraph1 
-      ) args (1,subst,metasenv,t,ugraph) 
+           num+1,subst,metasenv,t)
+      args (1,subst,metasenv,t) 
   in
-    subst,metasenv,hd,ugraph
-
-
+    metasenv, subst, hd
 
-let rec instantiate test_eq_only metasenv subst context n lc t swap =
+and instantiate test_eq_only metasenv subst context n lc t swap =
   let unif m s c t1 t2 =
     if swap then unify m s c t2 t1 else unify m s c t1 t2
   in