From 5c9e1997848c2f74297a5a243679f4bcb6ae0dc7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Sep 2005 12:51:37 +0000 Subject: [PATCH] added universes --- helm/ocaml/cic_disambiguation/disambiguate.ml | 2 +- helm/ocaml/cic_notation/cicNotationParser.ml | 2 +- helm/ocaml/cic_notation/cicNotationPp.ml | 2 +- helm/ocaml/cic_notation/cicNotationPt.ml | 2 +- helm/ocaml/cic_notation/cicNotationRew.ml | 8 ++++---- helm/ocaml/cic_omdoc/cic2acic.ml | 20 +++++++------------ helm/ocaml/cic_omdoc/cic2acic.mli | 4 ++-- helm/ocaml/cic_omdoc/cic2content.ml | 10 +++++----- 8 files changed, 22 insertions(+), 28 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index e9ce2e81c..d267b52b1 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -318,7 +318,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = Cic.Meta (index, cic_subst) | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set - | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) + | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index bcfd6c9f6..4622f67a6 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -425,7 +425,7 @@ EXTEND sort: [ [ "Prop" -> `Prop | "Set" -> `Set - | "Type" -> `Type + | "Type" -> `Type (CicUniv.fresh ()) | "CProp" -> `CProp ] ]; diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 3e48d3679..1c3ad4386 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -116,7 +116,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Num (num, _) -> num | Ast.Sort `Set -> "Set" | Ast.Sort `Prop -> "Prop" - | Ast.Sort `Type -> "Type" + | Ast.Sort (`Type _) -> "Type" | Ast.Sort `CProp -> "CProp" | Ast.Symbol (name, _) -> "'" ^ name diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index ca00d3539..bce159937 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -27,7 +27,7 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] type fold_kind = [ `Left | `Right ] type location = Lexing.position * Lexing.position diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 3d684fe39..0029e3db5 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -116,7 +116,7 @@ let string_of_sort_kind = function | `Prop -> "Prop" | `Set -> "Set" | `CProp -> "CProp" - | `Type -> "Type" + | `Type _ -> "Type" let pp_ast0 t k = let rec aux = @@ -275,7 +275,7 @@ let ast_of_acic0 term_info acic k = Hashtbl.find term_info.sort id with Not_found -> prerr_endline (sprintf "warning: sort of id %s not found, using Type" id); - `Type + `Type (CicUniv.fresh ()) in let aux_substs substs = Some @@ -298,13 +298,13 @@ let ast_of_acic0 term_info acic k = | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context 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 u) ->idref id (Ast.Sort (`Type u)) | 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 _ -> `Pi | `Prop | `CProp -> `Forall in idref id (Ast.Binder (binder_kind, diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 69c91cdb3..0d3127c31 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -23,25 +23,18 @@ * http://cs.unibo.it/helm/. *) -type sort_kind = [ `Prop | `Set | `Type | `CProp ] - -let sort_of_string = function - | "Prop" -> `Prop - | "Set" -> `Set - | "Type" -> `Type - | "CProp" -> `CProp - | _ -> assert false +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] let string_of_sort = function | `Prop -> "Prop" | `Set -> "Set" - | `Type -> "Type" + | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) | `CProp -> "CProp" let sort_of_sort = function | Cic.Prop -> `Prop | Cic.Set -> `Set - | Cic.Type _ -> `Type + | Cic.Type u -> `Type u | Cic.CProp -> `CProp (* let hashtbl_add_time = ref 0.0;; *) @@ -134,8 +127,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts match CicReduction.whd context t with C.Sort C.Prop -> `Prop | C.Sort C.Set -> `Set - | C.Sort (C.Type _) - | C.Meta _ -> `Type + | C.Sort (C.Type u) -> `Type u + | C.Meta _ -> `Type (CicUniv.fresh()) | C.Sort C.CProp -> `CProp | t -> prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ; @@ -188,7 +181,8 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) with Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *) (* CSC: Type or Set? I can not tell *) - None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false + let u = CicUniv.fresh() in + None,Cic.Sort (Cic.Type u),`Type u,false (* TASSI non dovrebbe fare danni *) (* *) in diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index abe61f387..b5a194951 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -31,10 +31,10 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; -type sort_kind = [ `Prop | `Set | `Type | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] val string_of_sort: sort_kind -> string -val sort_of_string: string -> sort_kind +(*val sort_of_string: string -> sort_kind*) val sort_of_sort: Cic.sort -> sort_kind val acic_object_of_cic_object : diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index ff8080983..72699f7e3 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -345,7 +345,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts let sort = (try Hashtbl.find ids_to_inner_sorts idr - with Not_found -> `Type) in + with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then K.Premise { K.premise_id = gen_id premise_prefix seed; @@ -358,7 +358,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts let sort = (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> `Type) in + with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then K.Lemma { K.lemma_id = gen_id lemma_prefix seed; @@ -370,7 +370,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts let sort = (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> `Type) in + with Not_found -> `Type (CicUniv.fresh())) in if sort = `Prop then let inductive_types = (let o,_ = @@ -731,7 +731,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let idarg = get_id arg in let sortarg = (try (Hashtbl.find ids_to_inner_sorts idarg) - with Not_found -> `Type) in + with Not_found -> `Type (CicUniv.fresh())) in let hdarg = if sortarg = `Prop then let (co,bo) = @@ -816,7 +816,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = else let aid = get_id a in let asort = (try (Hashtbl.find ids_to_inner_sorts aid) - with Not_found -> `Type) in + with Not_found -> `Type (CicUniv.fresh())) in if asort = `Prop then K.ArgProof (aux a) else K.Term a in -- 2.39.2