From a4a2334c7074974db8baf2666ba161702ff9e112 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 25 Oct 2002 15:15:02 +0000 Subject: [PATCH] cicCooking.ml* forgot in the previous commit --- helm/ocaml/cic_proof_checking/cicCooking.ml | 235 ------------------- helm/ocaml/cic_proof_checking/cicCooking.mli | 34 --- 2 files changed, 269 deletions(-) delete mode 100644 helm/ocaml/cic_proof_checking/cicCooking.ml delete mode 100644 helm/ocaml/cic_proof_checking/cicCooking.mli diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml deleted file mode 100644 index 2c5d0b439..000000000 --- a/helm/ocaml/cic_proof_checking/cicCooking.ml +++ /dev/null @@ -1,235 +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 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 -;; diff --git a/helm/ocaml/cic_proof_checking/cicCooking.mli b/helm/ocaml/cic_proof_checking/cicCooking.mli deleted file mode 100644 index 960fb6fae..000000000 --- a/helm/ocaml/cic_proof_checking/cicCooking.mli +++ /dev/null @@ -1,34 +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 Impossible -exception NotImplemented of int * string -exception WrongUriToConstant -exception WrongUriToVariable of string -exception WrongUriToInductiveDefinition - -(* init register the cooking function defined in this module so that it *) -(* will be used to retrieve the cooked objects from the environment *) -val init : unit -> unit -- 2.39.2