X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;fp=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=8407f8357e04d3f7f8603759cbeb7432060d58b3;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
deleted file mode 100644
index 8407f8357..000000000
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ /dev/null
@@ -1,252 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-exception ReferenceToVariable;;
-exception RferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-
-(* 
-let rec fix_lambdas_wrt_type ty te =
- let module C = Cic in
- let module S = CicSubstitution in
-(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-   match ty with
-     C.Prod (_,_,ty') ->
-       (match CicReduction.whd [] te with
-          C.Lambda (n,s,te') ->
-            C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
-        | t ->
-            let rec get_sources =
-              function 
-                C.Prod (_,s,ty) -> s::(get_sources ty)
-              | _ -> [] in
-            let sources = get_sources ty in
-            let no_sources = List.length sources in
-            let rec mk_rels n shift =
-              if n = 0 then []
-            else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
-            let t' = S.lift no_sources t in
-            let t2 = 
-              match t' with
-                C.Appl l -> 
-                  C.LetIn 
-                     (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
-              | _ -> 
-                  C.Appl (t'::(mk_rels no_sources 0)) in
-                   List.fold_right
-                     (fun source t -> C.Lambda (C.Name "y",source,t)) 
-                      sources t2)
-   | _ -> te
-;; *)
-
-let rec fix_lambdas_wrt_type ty te =
- let module C = Cic in
- let module S = CicSubstitution in
-(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-   match ty,te with
-     C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
-       C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
-   | C.Prod (_,s,ty'), t -> 
-      let rec get_sources =
-        function 
-            C.Prod (_,s,ty) -> s::(get_sources ty)
-          | _ -> [] in
-      let sources = get_sources ty in
-      let no_sources = List.length sources in
-      let rec mk_rels n shift =
-        if n = 0 then []
-        else (C.Rel (n + shift))::(mk_rels (n - 1) shift) in
-      let t' = S.lift no_sources t in
-      let t2 = 
-         match t' with
-           C.Appl l -> 
-             C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
-         | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
-      List.fold_right
-        (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
-   | _, _ -> te
-;;
-
-(*
-let rec fix_lambdas_wrt_type ty te =
- let module C = Cic in
- let module S = CicSubstitution in
-(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-   match ty,te with
-     C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
-       C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
-   | C.Prod (_,s,ty'), ((C.Appl (C.Const _ ::_)) as t) -> 
-      (* const have a fixed arity *)
-      (* prerr_endline ("******** fl - eta expansion 0: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-       let t' = S.lift 1 t in
-       C.Lambda (C.Name "x",s,
-         C.LetIn 
-          (C.Name "H", fix_lambdas_wrt_type ty' t', 
-            C.Appl [C.Rel 1;C.Rel 2])) 
-   | C.Prod (_,s,ty'), C.Appl l ->
-       (* prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-       let l' = List.map (S.lift 1) l in
-        C.Lambda (C.Name "x",s,
-         fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
-   | C.Prod (_,s,ty'), _ ->
-       (* prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); *)
-       flush stderr ;
-       let te' = S.lift 1 te in
-        C.Lambda (C.Name "x",s,
-          fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
-   | _, _ -> te
-;;*) 
-
-let fix_according_to_type ty hd tl =
- let module C = Cic in
- let module S = CicSubstitution in
-   let rec count_prods =
-     function
-       C.Prod (_,_,t) -> 1 + (count_prods t)
-       | _ -> 0 in
-  let expected_arity = count_prods ty in
-  let rec aux n ty tl res =
-    if n = 0 then
-      (match tl with 
-         [] -> C.Appl res
-       | _ -> 
-          match res with
-            [] -> assert false
-          | [a] -> C.Appl (a::tl)
-          | _ ->
-              (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
-              C.LetIn 
-                (C.Name "H", 
-                  C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
-    else 
-      let name,source,target =
-        (match ty with
-           C.Prod (C.Name _ as n,s,t) -> n,s,t
-         | C.Prod (C.Anonymous, s,t) -> C.Name "z",s,t
-         | _ -> (* prods number may only increase for substitution *) 
-           assert false) in
-      match tl with 
-         [] ->
-           (* prerr_endline ("******* too few args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
-           let res' = List.map (S.lift 1) res in 
-           C.Lambda 
-            (name, source, aux (n-1) target [] (res'@[C.Rel 1]))
-        | hd::tl' -> 
-           let hd' = fix_lambdas_wrt_type source hd in
-            (*  (prerr_endline ("++++++prima :" ^(CicPp.ppterm hd)); 
-              prerr_endline ("++++++dopo :" ^(CicPp.ppterm hd'))); *)
-           aux (n-1) (S.subst hd' target) tl' (res@[hd']) in
-  aux expected_arity ty tl [hd]
-;;
-
-let eta_fix metasenv t =
- let rec eta_fix' t = 
-(*  prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
-  flush stderr ; *)
-  let module C = Cic in
-  match t with
-     C.Rel n -> C.Rel n 
-   | C.Var (uri,exp_named_subst) ->
-      let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' t)) exp_named_subst
-      in
-      C.Var (uri,exp_named_subst')
-   | C.Meta (n,l) ->
-      let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> n = m) metasenv
-       in
-       let l' =
-        List.map2
-         (fun ct t ->
-          match (ct, t) with
-            None, _ -> None
-          | _, Some t -> Some (eta_fix' t)
-          | Some _, None -> assert false (* due to typing rules *))
-        canonical_context l
-       in
-       C.Meta (n,l')
-   | C.Sort s -> C.Sort s
-   | C.Implicit -> C.Implicit
-   | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t)
-   | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
-   | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
-   | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
-   | C.Appl l as appl -> 
-       let l' =  List.map eta_fix' l 
-       in 
-       (match l' with
-         C.Const(uri,exp_named_subst)::l'' ->
-           let constant_type =
-             (match CicEnvironment.get_obj uri with
-               C.Constant (_,_,ty,_) -> ty
-             | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
-             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-             )
-           in
-           let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
-           if not (CicReduction.are_convertible [] appl result) then 
-             (prerr_endline ("prima :" ^(CicPp.ppterm appl)); 
-              prerr_endline ("dopo :" ^(CicPp.ppterm result)));
-           result
-        | _ -> C.Appl l' )
-   | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' t)) exp_named_subst
-       in
-       C.Const (uri,exp_named_subst')
-   | C.MutInd (uri,tyno,exp_named_subst) ->
-       let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' t)) exp_named_subst
-       in
-        C.MutInd (uri, tyno, exp_named_subst')
-   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-       List.map
-        (function i,t -> i, (eta_fix' t)) exp_named_subst
-       in
-        C.MutConstruct (uri, tyno, consno, exp_named_subst')
-   | C.MutCase (uri, tyno, outty, term, patterns) ->
-       C.MutCase (uri, tyno, eta_fix' outty,
-              eta_fix' term, List.map eta_fix' patterns)
-   | C.Fix (funno, funs) ->
-       C.Fix (funno,
-        List.map
-         (fun (name, no, ty, bo) ->
-           (name, no, eta_fix' ty, eta_fix' bo)) funs)
-   | C.CoFix (funno, funs) ->
-       C.CoFix (funno,
-        List.map
-         (fun (name, ty, bo) ->
-           (name, eta_fix' ty, eta_fix' bo)) funs)
-   in
-   eta_fix' t
-;;
-
-
-