+++ /dev/null
-(* 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);
- flush stderr ; *)
- (* cast e altra porcheria ???? *)
- 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 l ->
- prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te);
- flush stderr ;
- 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 aux ty tl res =
- (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty);
- flush stderr ; *)
- match ty with
- C.Rel _
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit ->
- (match tl with
- [] -> C.Appl res
- | _ ->
- prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
- flush stderr ;
- C.LetIn
- (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
- | C.Cast (v,t) -> aux v tl res
- | C.Prod (n,s,t) ->
- (match tl with
- [] ->
- prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res));
- flush stderr ;
- let res' = List.map (S.lift 1) res
- in
- C.Lambda
- (C.Name "x", (* Andrea: to do: generate a fresh name *)
- s,
- aux t [] (res'@[C.Rel 1]))
- | hd::tl' ->
- let hd' = fix_lambdas_wrt_type s hd
- in
- aux (S.subst hd' t) tl' (res@[hd']))
- | C.Lambda _ -> assert false
- | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
- | C.Appl _
- | C.Const _
- | C.MutInd _
- | C.MutConstruct _
- | C.MutCase _
- | C.Fix _
- | C.CoFix _ -> (* ???? *)
- (match tl with
- [] -> C.Appl res
- | _ -> (* Andrea: to do: generate a fresh name *)
- C.LetIn
- (C.Name "H",
- C.Appl res,
- C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
- in
- aux 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 ->
- 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
- fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
- | _ -> 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
-;;
-
projects / helm.git / blobdiff