From eda1c80730b099bafcf3c89ce1e8b4afbbfef4f7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:29:15 +0000 Subject: [PATCH] - attributes support - default instance is 0 (not -1 !) --- helm/ocaml/cic_transformations/acic2Ast.ml | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index b815d33bd..1e4914e7f 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -39,10 +39,8 @@ let sort_of_string = function let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - | Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l + | Cic.InductiveDefinition (l,_,_,_) -> l + | _ -> assert false let name_of_inductive_type uri i = let types = get_types uri in @@ -93,7 +91,7 @@ let ast_of_acic ids_to_inner_sorts acic = in idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t)) | Cic.ACast (id,v,t) -> - idref id (Ast.Appl [idref id (Ast.Symbol ("cast", -1)); aux v; aux 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)) @@ -223,7 +221,7 @@ let _ = (** fill symbol_table *) Hashtbl.add symbol_table uri (fun aid sid args acic2ast -> Ast.AttributedTerm (`IdRef aid, - Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, -1)) :: + Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) :: List.map acic2ast args))) in (* eq *) @@ -231,7 +229,7 @@ let _ = (** fill symbol_table *) (fun aid sid args acic2ast -> Ast.AttributedTerm (`IdRef aid, Ast.Appl ( - Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", -1)) :: + Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) :: List.map acic2ast (List.tl args)))); (* exists *) Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI @@ -264,17 +262,17 @@ let _ = (** fill symbol_table *) 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", -1))); + 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", -1))); + 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", -1)) :: + Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) :: List.map acic2ast args)) in let rec aux acc = function @@ -284,7 +282,7 @@ let _ = (** fill symbol_table *) | Cic.AConst (_, uri, []) when UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> Ast.AttributedTerm (`IdRef aid, - Ast.Num (string_of_int (acc + 2), -1)) + 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 -- 2.39.2