X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=76be244adf4c17c09b9451a74fef1f9880119100;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=1bc76ebb841176b185fde2c0052e2168b7130d0a;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index 1bc76ebb8..76be244ad 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -25,21 +25,15 @@ open Printf -let symbol_table = Hashtbl.create 1024 +module Ast = CicAst -let sort_of_string = function - | "Prop" -> `Prop - | "Set" -> `Set - | "Type" -> `Type - | "CProp" -> `CProp - | _ -> assert false +let symbol_table = Hashtbl.create 1024 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 @@ -60,16 +54,17 @@ let constructor_of_inductive_type uri i j = 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) + 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); @@ -84,11 +79,11 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = | 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.Cast (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)) @@ -213,3 +208,78 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = 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) +