--- /dev/null
+(* 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 <name, type> 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, []))
+ | 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)
+ | 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, 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, [])))
+ | 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, [])))
+
+ and astsubst_of_cicsubst subst =
+ 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
+
projects / helm.git / blobdiff