open Printf
+module Ast = CicAst
+
let symbol_table = Hashtbl.create 1024
let sort_of_string = function
| "Set" -> `Set
| "Type" -> `Type
| "CProp" -> `CProp
+ | "?" -> `Meta
| _ -> 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 o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ | Cic.InductiveDefinition (l,_,_,_) -> l
+ | _ -> assert false
let name_of_inductive_type uri i =
let types = get_types uri in
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 ast_of_acic ids_to_inner_sorts acic =
+ let ids_to_uris = Hashtbl.create 503 in
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
+ 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);
| 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.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
+ | `Set | `Type | `Meta -> `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.ACast (id,v,t) ->
+ idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t])
| 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))
in
aux acic, ids_to_uris
+let _ = (** fill symbol_table *)
+ let add_symbol name uri =
+ Hashtbl.add symbol_table uri
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) ::
+ List.map acic2ast args)))
+ in
+ (* eq *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (
+ Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) ::
+ List.map acic2ast (List.tl args))));
+ (* exists *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
+ (fun aid sid args acic2ast ->
+ match (List.tl args) with
+ [Cic.ALambda (_,Cic.Name n,s,t)] ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Binder (`Exists, (Cic.Name n, Some (acic2ast s)), acic2ast t))
+ | _ -> raise Not_found);
+ add_symbol "and" HelmLibraryObjects.Logic.and_XURI;
+ add_symbol "or" HelmLibraryObjects.Logic.or_XURI;
+ add_symbol "iff" HelmLibraryObjects.Logic.iff_SURI;
+ add_symbol "not" HelmLibraryObjects.Logic.not_SURI;
+ add_symbol "inv" HelmLibraryObjects.Reals.rinv_SURI;
+ add_symbol "opp" HelmLibraryObjects.Reals.ropp_SURI;
+ add_symbol "leq" HelmLibraryObjects.Peano.le_XURI;
+ add_symbol "leq" HelmLibraryObjects.Reals.rle_SURI;
+ add_symbol "lt" HelmLibraryObjects.Peano.lt_SURI;
+ add_symbol "lt" HelmLibraryObjects.Reals.rlt_SURI;
+ add_symbol "geq" HelmLibraryObjects.Peano.ge_SURI;
+ add_symbol "geq" HelmLibraryObjects.Reals.rge_SURI;
+ add_symbol "gt" HelmLibraryObjects.Peano.gt_SURI;
+ add_symbol "gt" HelmLibraryObjects.Reals.rgt_SURI;
+ add_symbol "plus" HelmLibraryObjects.Peano.plus_SURI;
+ add_symbol "plus" HelmLibraryObjects.BinInt.zplus_SURI;
+ add_symbol "times" HelmLibraryObjects.Peano.mult_SURI;
+ add_symbol "times" HelmLibraryObjects.Reals.rmult_SURI;
+ add_symbol "minus" HelmLibraryObjects.Peano.minus_SURI;
+ add_symbol "minus" HelmLibraryObjects.Reals.rminus_SURI;
+ add_symbol "div" HelmLibraryObjects.Reals.rdiv_SURI;
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef sid, Ast.Num ("0", 0)));
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", 0)));
+ (* plus *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
+ (fun aid sid args acic2ast ->
+ let appl () =
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (
+ Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) ::
+ List.map acic2ast args))
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ (match n with
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Num (string_of_int (acc + 2), 0))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+