+++ /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 Impossible;;
-exception NotImplemented of int * string;;
-exception WrongUriToConstant;;
-exception WrongUriToVariable of string;;
-exception WrongUriToInductiveDefinition;;
-
-(* mem x lol is true if x is a member of one *)
-(* of the lists of the list of (int * list) lol *)
-let mem x lol =
- List.fold_right (fun (_,l) i -> i || List.mem x l) lol false
-;;
-
-(* cook var term *)
-let cook curi cookingsno var is_letin =
- let rec aux k =
- let module C = Cic in
- function
- C.Rel n as t ->
- (match n with
- n when n >= k -> C.Rel (n + 1)
- | _ -> C.Rel n
- )
- | C.Var uri as t ->
- if UriManager.eq uri var then
- C.Rel k
- else
- t
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te, ty) -> C.Cast (aux k te, aux k ty)
- | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
- | C.Appl (he::tl) ->
- (* Get rid of C.Appl (C.Appl l1) l2 *)
- let newtl = List.map (aux k) tl in
- (match aux k he with
- C.Appl (he'::tl') -> C.Appl (he'::(tl'@newtl))
- | t -> C.Appl (t::newtl)
- )
- | C.Appl [] -> raise Impossible
- | C.Const (uri,_) ->
- if not is_letin && match CicEnvironment.get_obj uri with
- C.Definition (_,_,_,params) when mem var params -> true
- | C.Definition _ -> false
- | C.Axiom (_,_,params) when mem var params -> true
- | C.Axiom _ -> false
- | C.CurrentProof _ ->
- raise (NotImplemented (2,(UriManager.string_of_uri uri)))
- | _ -> raise WrongUriToConstant
- then
- C.Appl
- ((C.Const (uri,UriManager.relative_depth curi uri cookingsno))::
- [C.Rel k])
- else
- C.Const (uri,UriManager.relative_depth curi uri cookingsno)
- | C.MutInd (uri,_,i) ->
- if not is_letin && match CicEnvironment.get_obj uri with
- C.InductiveDefinition (_,params,_) when mem var params -> true
- | C.InductiveDefinition _ -> false
- | _ -> raise WrongUriToInductiveDefinition
- then
- C.Appl ((C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i))::[C.Rel k])
- else
- C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i)
- | C.MutConstruct (uri,_,i,j) ->
- if not is_letin && match CicEnvironment.get_obj uri with
- C.InductiveDefinition (_,params,_) when mem var params -> true
- | C.InductiveDefinition _ -> false
- | _ -> raise WrongUriToInductiveDefinition
- then
- C.Appl ((C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j))::[C.Rel k])
- else
- C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j)
- | C.MutCase (uri,_,i,outt,term,pl) ->
- let substitutedfl =
- List.map (aux k) pl
- in
- C.MutCase (uri,UriManager.relative_depth curi uri cookingsno,i,
- aux k outt,aux k term, substitutedfl)
- | C.Fix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name,i,aux k ty, aux (k+len) bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let len = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name,aux k ty, aux (k+len) bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- in
- aux 1
-;;
-
-let cook_gen add_binder curi cookingsno ty vars =
- let module C = Cic in
- let module U = UriManager in
- let rec cookrec ty =
- function
- var::tl ->
- let (varname, varbody, vartype) =
- match CicEnvironment.get_obj var with
- C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype)
- | _ -> raise (WrongUriToVariable (U.string_of_uri var))
- in
- let cooked_once =
- add_binder (C.Name varname) varbody vartype
- (match varbody with
- Some _ -> cook curi cookingsno var true ty
- | None -> cook curi cookingsno var false ty
- )
- in
- cookrec cooked_once tl
- | _ -> ty
- in
- cookrec ty vars
-;;
-
-let cook_prod =
- cook_gen (fun n b s t ->
- match b with
- None -> Cic.Prod (n,s,t)
- | Some b -> Cic.LetIn (n,b,t)
- )
-and cook_lambda =
- cook_gen (fun n b s t ->
- match b with
- None -> Cic.Lambda (n,s,t)
- | Some b -> Cic.LetIn (n,b,t)
- )
-;;
-
-(*CSC: sbagliato da rifare e completare *)
-let cook_one_level obj curi cookingsno vars =
- let module C = Cic in
- match obj with
- C.Definition (id,te,ty,params) ->
- let ty' = cook_prod curi cookingsno ty vars in
- let te' = cook_lambda curi cookingsno te vars in
- C.Definition (id,te',ty',params)
- | C.Axiom (id,ty,parameters) ->
- let ty' = cook_prod curi cookingsno ty vars in
- C.Axiom (id,ty',parameters)
- | C.Variable _ as obj -> obj
- | C.CurrentProof (id,conjs,te,ty) ->
- let ty' = cook_prod curi cookingsno ty vars in
- let te' = cook_lambda curi cookingsno te vars in
- C.CurrentProof (id,conjs,te',ty')
- | C.InductiveDefinition (dl, params, n_ind_params) ->
- let dl' =
- List.map
- (fun (name,inductive,arity,constructors) ->
- let constructors' =
- List.map
- (fun (name,ty,r) ->
- let r' =
- match !r with
- None -> raise Impossible
- | Some r -> List.map (fun _ -> false) vars @ r
- in
- (name,cook_prod curi cookingsno ty vars,ref (Some r'))
- ) constructors
- in
- (name,inductive,cook_prod curi cookingsno arity vars,constructors')
- ) dl
- in
- let number_of_variables_without_a_body =
- let is_not_letin uri =
- match CicEnvironment.get_obj uri with
- C.Variable (_,None,_) -> true
- | C.Variable (_,Some _,_) -> false
- | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
- in
- List.fold_left
- (fun i uri -> if is_not_letin uri then i + 1 else i) 0 vars
- in
- C.InductiveDefinition
- (dl', params, n_ind_params + number_of_variables_without_a_body)
-;;
-
-let cook_obj obj uri =
- let module C = Cic in
- let params =
- match obj with
- C.Definition (_,_,_,params) -> params
- | C.Axiom (_,_,params) -> params
- | C.Variable _ -> []
- | C.CurrentProof _ -> []
- | C.InductiveDefinition (_,params,_) -> params
- in
- let rec cook_all_levels obj =
- function
- [] -> []
- | (n,vars)::tl ->
- let cooked_obj = cook_one_level obj uri (n + 1) (List.rev vars) in
- (n,cooked_obj)::(cook_all_levels cooked_obj tl)
- in
- cook_all_levels obj (List.rev params)
-;;
-
-let init () =
- CicEnvironment.set_cooking_function cook_obj
-;;
projects / helm.git / blobdiff