X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;fp=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=0000000000000000000000000000000000000000;hp=1bc76ebb841176b185fde2c0052e2168b7130d0a;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml deleted file mode 100644 index 1bc76ebb8..000000000 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ /dev/null @@ -1,215 +0,0 @@ -(* Copyright (C) 2004, 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://helm.cs.unibo.it/ - *) - -open Printf - -let symbol_table = Hashtbl.create 1024 - -let sort_of_string = function - | "Prop" -> `Prop - | "Set" -> `Set - | "Type" -> `Type - | "CProp" -> `CProp - | _ -> assert false - -let get_types uri = - match CicEnvironment.get_obj uri with - | Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l - -let name_of_inductive_type uri i = - let types = get_types uri in - let (name, _, _, _) = try List.nth types i with Not_found -> assert false in - name - - (* returns pairs *) -let constructors_of_inductive_type uri i = - let types = get_types uri in - let (_, _, _, constructors) = - try List.nth types i with Not_found -> assert false - in - constructors - - (* returns name only *) -let constructor_of_inductive_type uri i j = - (try - fst (List.nth (constructors_of_inductive_type uri i) (j-1)) - with Not_found -> assert false) - -let ast_of_acic ids_to_inner_sorts ids_to_uris acic = - let register_uri id uri = Hashtbl.add ids_to_uris id uri in - let sort_of_id id = - try - sort_of_string (Hashtbl.find ids_to_inner_sorts id) - with Not_found -> assert false - in - let module Ast = CicAst in - let idref id t = Ast.AttributedTerm (`IdRef id, t) in - let rec aux = function - | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) - | Cic.AVar (id,uri,subst) -> - register_uri id (UriManager.string_of_uri uri); - idref id - (Ast.Ident (UriManager.name_of_uri uri, astsubst_of_cicsubst subst)) - | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l)) - | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) - | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) - | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *) - | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) - | Cic.AImplicit _ -> assert false - | Cic.AProd (id,n,s,t) -> - let binder_kind = - match sort_of_id id with - | `Set | `Type -> `Pi - | `Prop | `CProp -> `Forall - in - idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t)) - | Cic.ACast (id,v,t) -> idref id (aux v) - | Cic.ALambda (id,n,s,t) -> - idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t)) - | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t)) - | Cic.AAppl (aid,Cic.AConst (sid,uri,subst)::tl) -> - let uri_str = UriManager.string_of_uri uri in - register_uri sid uri_str; - (try - let f = Hashtbl.find symbol_table uri_str in - f aid sid tl aux - with Not_found -> - idref aid - (Ast.Appl (idref sid - (Ast.Ident (UriManager.name_of_uri uri, - astsubst_of_cicsubst subst)) :: (List.map aux tl)))) - | Cic.AAppl (aid,Cic.AMutInd (sid,uri,i,subst)::tl) -> - let name = name_of_inductive_type uri i in - let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in - register_uri sid puri_str; - (try - (let f = Hashtbl.find symbol_table puri_str in - f aid sid tl aux) - with Not_found -> - idref aid - (Ast.Appl (idref sid - (Ast.Ident (name, - astsubst_of_cicsubst subst)) :: (List.map aux tl)))) - | Cic.AAppl (id,li) -> idref id (Ast.Appl (List.map aux li)) - | Cic.AConst (id,uri,subst) -> - let uri_str = UriManager.string_of_uri uri in - register_uri id uri_str; - (try - let f = Hashtbl.find symbol_table uri_str in - f "dummy" id [] aux - with Not_found -> - idref id - (Ast.Ident - (UriManager.name_of_uri uri, astsubst_of_cicsubst subst))) - | Cic.AMutInd (id,uri,i,subst) -> - let name = name_of_inductive_type uri i in - let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in - register_uri id puri_str; - (try - let f = Hashtbl.find symbol_table puri_str in - f "dummy" id [] aux - with Not_found -> - idref id (Ast.Ident (name, astsubst_of_cicsubst subst))) - | Cic.AMutConstruct (id,uri,i,j,subst) -> - let name = constructor_of_inductive_type uri i j in - let uri_str = UriManager.string_of_uri uri in - let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in - register_uri id puri_str; - (try - let f = Hashtbl.find symbol_table puri_str in - f "dummy" id [] aux - with Not_found -> - idref id (Ast.Ident (name, astsubst_of_cicsubst subst))) - | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> - let name = name_of_inductive_type uri typeno in - let constructors = constructors_of_inductive_type uri typeno in - let rec eat_branch ty pat = - match (ty, pat) with - | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> - let (cv, rhs) = eat_branch t t' in - (name, Some (aux s)) :: cv, rhs - | _, _ -> [], aux pat - in - let patterns = - List.map2 - (fun (name, ty) pat -> - let (capture_variables, rhs) = eat_branch ty pat in - ((name, capture_variables), rhs)) - constructors patterns - in - idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns)) - | Cic.AFix (id, no, funs) -> - let defs = - List.map - (fun (_, n, decr_idx, ty, bo) -> - ((Cic.Name n, Some (aux ty)), aux bo, decr_idx)) - funs - in - let name = - try - (match List.nth defs no with - | (Cic.Name n, _), _, _ -> n - | _ -> assert false) - with Not_found -> assert false - in - idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) - | Cic.ACoFix (id, no, funs) -> - let defs = - List.map - (fun (_, n, ty, bo) -> ((Cic.Name n, Some (aux ty)), aux bo, 0)) - funs - in - let name = - try - (match List.nth defs no with - | (Cic.Name n, _), _, _ -> n - | _ -> assert false) - with Not_found -> assert false - in - idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None))) - - and astsubst_of_cicsubst subst = - Some - (List.map (fun (uri, annterm) -> - (UriManager.name_of_uri uri, aux annterm)) - subst) - - and astcontext_of_ciccontext context = - List.map - (function - | None -> None - | Some annterm -> Some (aux annterm)) - context - - in - aux acic, ids_to_uris -