X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=b60abf25886ea34a60658fba9f21d7926a180e5d;hb=5edfd170706c91c5d3a9d3522360b748a2dc034f;hp=19b6c4b4bf4161ab4546d2f178fe9e13d2c117be;hpb=b029556cbcecb852dfc9cf25801f3dcc0bb762bb;p=helm.git diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index 19b6c4b4b..b60abf258 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -25,6 +25,8 @@ open Printf +module Ast = CicAst + let symbol_table = Hashtbl.create 1024 let sort_of_string = function @@ -32,14 +34,14 @@ 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 @@ -60,17 +62,18 @@ 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) 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, [])) + 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 @@ -78,17 +81,18 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = | 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)) @@ -181,7 +185,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = | _ -> assert false) with Not_found -> assert false in - idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, []))) + idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) | Cic.ACoFix (id, no, funs) -> let defs = List.map @@ -195,11 +199,13 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic = | _ -> assert false) with Not_found -> assert false in - idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, []))) + idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None))) and astsubst_of_cicsubst subst = - List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm)) - subst + Some + (List.map (fun (uri, annterm) -> + (UriManager.name_of_uri uri, aux annterm)) + subst) and astcontext_of_ciccontext context = List.map @@ -211,3 +217,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) +