- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.

  This allows to easily implement elim using apply and it makes the auto
  tactic much more powerful.
- CicMetaSubst.apply_subst semantics changed: it now always performs
  beta-reduction when a meta in head-position in an application is istantiated
  with a lambda-abstraction.
- CicMetaSubst.apply_subst_reducing no longer in use: removed.

diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile
index 457286589e7ae0365c59acfadf7f681465c04a0a..4f19b765f8a3645c3d7d8baec342e8c04b6a7623 100644 (file)
--- a/helm/ocaml/cic_unification/Makefile
+++ b/helm/ocaml/cic_unification/Makefile
@@ -5,8 +5,8 @@ PREDICATES =
 INTERFACE_FILES = \
        cicMkImplicit.mli \
        cicMetaSubst.mli \
-       cicUnification.mli \
        freshNamesGenerator.mli \
+       cicUnification.mli \
        cicRefine.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 9695d714b7658940392fc4401af71d3701d7298f..512c65d986fa2c48015309faca2a908c7501a654 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -96,6 +96,7 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
+(* CSC: old code that never performs beta reduction
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
       begin
@@ -105,19 +106,7 @@ let apply_subst =
       end
   in
   apply_subst_gen ~appl_fun
-;;
-
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
-(* performs as (apply_subst subst t) until it finds an application of   *)
-(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
-(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
-(* beta-reductions are performed.                                       *)
-(* Hint: this function is usually called when [reductions_no]           *)
-(*  eta-expansions have been performed and the head of the new          *)
-(*  application has been unified with (META [meta_to_reduce]):          *)
-(*  during the unwinding the eta-expansions are undone.                 *)
-
-let apply_subst_reducing meta_to_reduce =
+*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -126,23 +115,24 @@ let apply_subst_reducing meta_to_reduce =
       | he' -> Cic.Appl (he'::tl')
     in
      begin
-      match meta_to_reduce, he with
-         Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
+      match he with
+         Cic.Meta (m,_) ->
           let rec beta_reduce =
            function
-              (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
+              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
                 let he'' = CicSubstitution.subst he' t in
                  if tl' = [] then
                   he''
                  else
-                  beta_reduce (n-1,Cic.Appl(he''::tl'))
-            | (_,t) -> t
+                  beta_reduce (Cic.Appl(he''::tl'))
+            | t -> t
           in
-           beta_reduce (reductions_no,t')
-       | _,_ -> t'
+           beta_reduce t'
+       | _ -> t'
      end
   in
   apply_subst_gen ~appl_fun
+;;
 
 let rec apply_subst_context subst context =
   List.fold_right

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index b1e34757ec6e0564b32f8d050215808f1dd65fe8..4f055f1f876631fbd8f282b849b0ab9f2acbea87 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -36,19 +36,6 @@ type substitution = (int * Cic.term) list
 (* [subst] must be already unwinded        *)
 val apply_subst : substitution -> Cic.term -> Cic.term
 
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
-(* performs as (apply_subst subst t) until it finds an application of   *)
-(* (META [mtr]) that, once unwinding is performed, creates a new        *)
-(* beta-redex; in this case up to [reductions_no] consecutive           *)
-(* beta-reductions are performed.                                       *)
-(* Hint: this function is usually called when [reductions_no]           *)
-(*  eta-expansions have been performed and the head of the new          *)
-(*  application has been unified with (META [meta_to_reduce]):          *)
-(*  during the unwinding the eta-expansions are undone.                 *)
-(* [subst] must be already unwinded                                     *)
-val apply_subst_reducing :
- (int * int) option -> substitution -> Cic.term -> Cic.term
-
 val apply_subst_context : substitution -> Cic.context -> Cic.context
 val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
 

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 395799b3137c29058dc65abced41b8f8dd6d6b83..c239f8e1f5ff77a2b551fe0a05ee6cf7d66dff17 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -29,7 +29,7 @@ exception AssertFailure of string;;
 
 (* type_of_aux' metasenv context term                        *)
 (* refines [term] and returns the refined form of [term],    *)
-(* its type, the computed substitution and the new metasenv. *)
+(* its type the new metasenv. *)
 val type_of_aux':
  Cic.metasenv -> Cic.context -> Cic.term ->
   Cic.term * Cic.term * Cic.metasenv

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 35eb18f450974d61fc238b77d3f985203b249d6b..8a1f4c43e8aef1d5fd25feb63f3a92c2ce829dcf 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -43,6 +43,134 @@ let type_of_aux' metasenv subst context term =
         (CicMetaSubst.ppcontext subst context)
         (CicMetaSubst.ppmetasenv metasenv subst) msg)))
 
+let rec eta_expand test_equality_only metasenv subst context t arg =
+ let module T = CicTypeChecker in
+ let module S = CicSubstitution in
+ let module C = Cic in
+  let rec aux metasenv subst n context t' =
+   try
+    let subst,metasenv =
+     fo_unif_subst test_equality_only subst context metasenv arg t'
+    in
+     subst,metasenv,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)
+        | C.Var (uri,exp_named_subst) ->
+           let subst,metasenv,exp_named_subst' =
+            aux_exp_named_subst metasenv subst n context exp_named_subst
+           in
+            subst,metasenv,C.Var (uri,exp_named_subst')
+        | C.Meta (i,l) as t->
+           (try
+             let t' = List.assoc i subst in
+              aux metasenv subst n context t'
+            with
+             Not_found -> subst,metasenv,t)
+        | C.Sort _
+        | C.Implicit _ as t -> subst,metasenv,t
+        | C.Cast (te,ty) ->
+           let subst,metasenv,te' = aux metasenv subst n context te in
+           let subst,metasenv,ty' = aux metasenv subst n context ty in
+           subst,metasenv,C.Cast (te', ty')
+        | C.Prod (nn,s,t) ->
+           let subst,metasenv,s' = aux metasenv subst n context s in
+           let subst,metasenv,t' =
+            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+           in
+            subst,metasenv,C.Prod (nn, s', t')
+        | C.Lambda (nn,s,t) ->
+           let subst,metasenv,s' = aux metasenv subst n context s in
+           let subst,metasenv,t' =
+            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+           in
+            subst,metasenv,C.Lambda (nn, s', t')
+        | C.LetIn (nn,s,t) ->
+           let subst,metasenv,s' = aux metasenv subst n context s in
+           let subst,metasenv,t' =
+            aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+           in
+            subst,metasenv,C.LetIn (nn, s', t')
+        | C.Appl l ->
+           let subst,metasenv,revl' =
+            List.fold_left
+             (fun (subst,metasenv,appl) t ->
+               let subst,metasenv,t' = aux metasenv subst n context t in
+                subst,metasenv,t'::appl
+             ) (subst,metasenv,[]) l
+           in
+            subst,metasenv,C.Appl (List.rev revl')
+        | C.Const (uri,exp_named_subst) ->
+           let subst,metasenv,exp_named_subst' =
+            aux_exp_named_subst metasenv subst n context exp_named_subst
+           in
+            subst,metasenv,C.Const (uri,exp_named_subst')
+        | C.MutInd (uri,i,exp_named_subst) ->
+           let subst,metasenv,exp_named_subst' =
+            aux_exp_named_subst metasenv subst n context exp_named_subst
+           in
+            subst,metasenv,C.MutInd (uri,i,exp_named_subst')
+        | C.MutConstruct (uri,i,j,exp_named_subst) ->
+           let subst,metasenv,exp_named_subst' =
+            aux_exp_named_subst metasenv subst n context exp_named_subst
+           in
+            subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
+        | C.MutCase (sp,i,outt,t,pl) ->
+           let subst,metasenv,outt' = aux metasenv subst n context outt in
+           let subst,metasenv,t' = aux metasenv subst n context t in
+           let subst,metasenv,revpl' =
+            List.fold_left
+             (fun (subst,metasenv,pl) t ->
+               let subst,metasenv,t' = aux metasenv subst n context t in
+                subst,metasenv,t'::pl
+             ) (subst,metasenv,[]) pl
+           in
+           subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
+        | 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,CicMetaSubst.lift subst 1 t'
+        | 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)
+*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+
+  and aux_exp_named_subst metasenv subst n context ens =
+   List.fold_right
+    (fun (uri,t) (subst,metasenv,l) ->
+      let subst,metasenv,t' = aux metasenv subst n context t in
+       subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
+  in
+   let argty =
+    T.type_of_aux' metasenv context arg
+ in
+  let fresh_name =
+   FreshNamesGenerator.mk_fresh_name
+    metasenv context (Cic.Name "Heta") ~typ:argty
+  in
+   let subst,metasenv,t' = aux metasenv subst 0 context t in
+    subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+
+and eta_expand_many test_equality_only metasenv subst context t =
+ List.fold_left
+  (fun (subst,metasenv,t) arg ->
+    eta_expand test_equality_only metasenv subst context t arg
+  ) (subst,metasenv,t)
+
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
    metavariable i with its body.
@@ -52,7 +180,7 @@ let type_of_aux' metasenv subst context term =
    a new substitution which is _NOT_ unwinded. It must be unwinded before
    applying it. *)
 
-let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =  
+and fo_unif_subst test_equality_only subst context metasenv t1 t2 =  
  let module C = Cic in
  let module R = CicMetaSubst in
  let module S = CicSubstitution in
@@ -203,25 +331,48 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        fo_unif_subst 
         test_equality_only subst context metasenv t2 (S.subst s1 t1)
    | (C.Appl l1, C.Appl l2) -> 
-       let lr1 = List.rev l1 in
-       let lr2 = List.rev l2 in
-       let rec fo_unif_l test_equality_only subst metasenv =
-        function
-           [],_
-         | _,[] -> assert false
-         | ([h1],[h2]) ->
-             fo_unif_subst test_equality_only subst context metasenv h1 h2
-         | ([h],l) 
-         | (l,[h]) ->
-             fo_unif_subst 
-             test_equality_only subst context metasenv h (C.Appl (List.rev l))
-         | ((h1::l1),(h2::l2)) -> 
-            let subst', metasenv' = 
-             fo_unif_subst test_equality_only subst context metasenv h1 h2
-            in 
-             fo_unif_l test_equality_only subst' metasenv' (l1,l2)
+       let subst,metasenv,t1',t2' =
+        match l1,l2 with
+         (* In the first two cases when we reach the next begin ... end
+            section useless work is done since, by construction, the list
+            of arguments will be equal.
+         *)
+           C.Meta (i,l)::args, _ ->
+            let subst,metasenv,t2' =
+             eta_expand_many test_equality_only metasenv subst context t2 args
+            in
+             subst,metasenv,t1,t2'
+         | _, C.Meta (i,l)::args ->
+            let subst,metasenv,t1' =
+             eta_expand_many test_equality_only metasenv subst context t1 args
+            in
+             subst,metasenv,t1',t2
+         | _,_ -> subst,metasenv,t1,t2
        in
-        fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
+        begin
+         match t1',t2' with
+            C.Appl l1, C.Appl l2 ->
+             let lr1 = List.rev l1 in
+             let lr2 = List.rev l2 in
+             let rec fo_unif_l test_equality_only subst metasenv =
+              function
+                 [],_
+               | _,[] -> assert false
+               | ([h1],[h2]) ->
+                   fo_unif_subst test_equality_only subst context metasenv h1 h2
+               | ([h],l) 
+               | (l,[h]) ->
+                  fo_unif_subst 
+                  test_equality_only subst context metasenv h (C.Appl (List.rev l))
+               | ((h1::l1),(h2::l2)) -> 
+                  let subst', metasenv' = 
+                   fo_unif_subst test_equality_only subst context metasenv h1 h2
+                  in 
+                   fo_unif_l test_equality_only subst' metasenv' (l1,l2)
+             in
+              fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
+          | _ -> assert false
+        end
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv' = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in