diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 45 | ||||
| -rw-r--r-- | checker/cic.mli | 18 | ||||
| -rw-r--r-- | checker/declarations.ml | 18 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 6 | ||||
| -rw-r--r-- | checker/modops.ml | 18 | ||||
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/univ.ml | 313 | ||||
| -rw-r--r-- | checker/univ.mli | 1 | ||||
| -rw-r--r-- | checker/values.ml | 9 |
9 files changed, 131 insertions, 299 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 7a69700d2..247a98e63 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open System -open Flags open Names open Check @@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -342,7 +341,7 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -366,15 +365,53 @@ let parse_args argv = (* To prevent from doing the initialization twice *) let initialized = ref false +(* XXX: At some point we need to either port the checker to use the + feedback system or to remove its use completely. *) +let init_feedback_listener () = + let open Format in + let pp_lvl fmt lvl = let open Feedback in match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let checker_feed (fb : Feedback.feedback) = let open Feedback in + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + (* Re-enable when we switch back to feedback-based error printing *) + | Message (lvl,loc,msg) -> + Format.eprintf "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + in ignore(Feedback.add_feeder checker_feed) + let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + init_feedback_listener (); try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); - if_verbose print_header (); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> diff --git a/checker/cic.mli b/checker/cic.mli index 59dd5bc4d..753fd0fc0 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -385,9 +385,9 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; @@ -395,13 +395,19 @@ and module_body = mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; - mod_retroknowledge : action list } + mod_retroknowledge : 'a module_retroknowledge; } + +and module_body = module_implementation generic_module_body (** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge] *) + implementation and also an empty [mod_retroknowledge] *) + +and module_type_body = unit generic_module_body -and module_type_body = module_body +and _ module_retroknowledge = +| ModBodyRK : + action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge (*************************************************************************) (** {4 From safe_typing.ml} *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 093d999a3..884a1ef18 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -583,24 +583,30 @@ let rec subst_expr sub = function | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) let rec subst_expression sub me = - functor_map (subst_module sub) (subst_expr sub) me + functor_map (subst_module_type sub) (subst_expr sub) me and subst_signature sub sign = - functor_map (subst_module sub) (subst_structure sub) sign + functor_map (subst_module_type sub) (subst_structure sub) sign and subst_structure sub struc = let subst_body = function | SFBconst cb -> SFBconst (subst_const_body sub cb) | SFBmind mib -> SFBmind (subst_mind sub mib) | SFBmodule mb -> SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb) + | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb) in List.map (fun (l,b) -> (l,subst_body b)) struc -and subst_module sub mb = +and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun subst_impl sub mb -> { mb with mod_mp = subst_mp sub mb.mod_mp; - mod_expr = - implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr; + mod_expr = subst_impl sub mb.mod_expr; mod_type = subst_signature sub mb.mod_type; mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } + +and subst_module sub mb = + subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb + +and subst_module_type sub mb = + subst_body (fun _ () -> ()) sub mb diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index b6816dd48..63e28448f 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -25,7 +25,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Feedback.msg_notice (str " checking cst:" ++ prcon kn); + Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with @@ -70,12 +70,12 @@ let lookup_module mp env = let mk_mtb mp sign delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; mod_delta = delta; - mod_retroknowledge = []; } + mod_retroknowledge = ModTypeRK; } let rec check_module env mp mb = let (_:module_signature) = diff --git a/checker/modops.ml b/checker/modops.ml index 79cd5c29f..f0abc39ea 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -49,7 +49,7 @@ let destr_functor = function | NoFunctor _ -> error_not_a_functor () let module_body_of_type mp mtb = - { mtb with mod_mp = mp; mod_expr = Abstract } + { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] } let rec add_structure mp sign resolver env = let add_one env (l,elem) = @@ -93,17 +93,19 @@ let strengthen_const mp_from l cb resolver = let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb - else strengthen_body true mp_from mp_to mb + else + let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in + strengthen_body mk_expr mp_from mp_to mb -and strengthen_body is_mod mp_from mp_to mb = +and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun mk_expr mp_from mp_to mb -> match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta in { mb with - mod_expr = - (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract); + mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } @@ -130,7 +132,7 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item::rest' let strengthen mtb mp = - strengthen_body false mtb.mod_mp mp mtb + strengthen_body ignore mtb.mod_mp mp mtb let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) @@ -138,9 +140,9 @@ let subst_and_strengthen mb mp = let module_type_of_module mp mb = let mtb = { mb with - mod_expr = Abstract; + mod_expr = (); mod_type_alg = None; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } in match mp with | Some mp -> strengthen {mtb with mod_mp = mp} mp diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 68a467bea..98a9c8250 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = mod_type = body_t1; mod_type_alg = None; mod_constraints = mtb1.mod_constraints; - mod_retroknowledge = []; + mod_retroknowledge = ModBodyRK []; mod_delta = mtb1.mod_delta} env in check_structure env body_t1 body_t2 equiv diff --git a/checker/univ.ml b/checker/univ.ml index 558315c2c..4f3131813 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -29,107 +29,6 @@ open Util union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -module type Hashconsed = -sig - type t - val hash : t -> int - val eq : t -> t -> bool - val hcons : t -> t -end - -module HashedList (M : Hashconsed) : -sig - type t = private Nil | Cons of M.t * int * t - val nil : t - val cons : M.t -> t -> t -end = -struct - type t = Nil | Cons of M.t * int * t - module Self = - struct - type _t = t - type t = _t - type u = (M.t -> M.t) - let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 - | _ -> false - let hashcons hc = function - | Nil -> Nil - | Cons (x, h, l) -> Cons (hc x, h, l) - end - module Hcons = Hashcons.Make(Self) - let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons - (** No recursive call: the interface guarantees that all HLists from this - program are already hashconsed. If we get some external HList, we can - still reconstruct it by traversing it entirely. *) - let nil = Nil - let cons x l = - let h = M.hash x in - let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in - let h = Hashset.Combine.combine h hl in - hcons (Cons (x, h, l)) -end - -module HList = struct - - module type S = sig - type elt - type t = private Nil | Cons of elt * int * t - val hash : t -> int - val nil : t - val cons : elt -> t -> t - val tip : elt -> t - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val map : (elt -> elt) -> t -> t - val smartmap : (elt -> elt) -> t -> t - val exists : (elt -> bool) -> t -> bool - val for_all : (elt -> bool) -> t -> bool - val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val to_list : t -> elt list - end - - module Make (H : Hashconsed) : S with type elt = H.t = - struct - type elt = H.t - include HashedList(H) - - let hash = function Nil -> 0 | Cons (_, h, _) -> h - - let tip e = cons e nil - - let rec fold f l accu = match l with - | Nil -> accu - | Cons (x, _, l) -> fold f l (f x accu) - - let rec map f = function - | Nil -> nil - | Cons (x, _, l) -> cons (f x) (map f l) - - let smartmap = map - (** Apriori hashconsing ensures that the map is equal to its argument *) - - let rec exists f = function - | Nil -> false - | Cons (x, _, l) -> f x || exists f l - - let rec for_all f = function - | Nil -> true - | Cons (x, _, l) -> f x && for_all f l - - let rec for_all2 f l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2 - | _ -> false - - let rec to_list = function - | Nil -> [] - | Cons (x, _, l) -> x :: to_list l - - end -end - module RawLevel = struct open Names @@ -167,24 +66,6 @@ struct | _, Level _ -> 1 | Var n, Var m -> Int.compare n m - let hequal x y = - x == y || - match x, y with - | Prop, Prop -> true - | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' - | Var n, Var n' -> n == n' - | _ -> false - - let hcons = function - | Prop as x -> x - | Set as x -> x - | Level (n,d) as x -> - let d' = Names.DirPath.hcons d in - if d' == d then x else Level (n,d') - | Var n as x -> x - open Hashset.Combine let hash = function @@ -216,24 +97,7 @@ module Level = struct let data x = x.data - (** Hashcons on levels + their hash *) - - module Self = struct - type _t = t - type t = _t - type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data - let hash x = x.hash - let hashcons () x = - let data' = RawLevel.hcons x.data in - if x.data == data' then x else { x with data = data' } - end - - let hcons = - let module H = Hashcons.Make(Self) in - Hashcons.simple_hcons H.generate H.hcons () - - let make l = hcons { hash = RawLevel.hash l; data = l } + let make l = { hash = RawLevel.hash l; data = l } let set = make Set let prop = make Prop @@ -270,7 +134,7 @@ module Level = struct let pr u = str (to_string u) - let make m n = make (Level (n, Names.DirPath.hcons m)) + let make m n = make (Level (n, m)) end @@ -303,48 +167,12 @@ struct module Expr = struct type t = Level.t * int - type _t = t - (* Hashing of expressions *) - module ExprHash = - struct - type t = _t - type u = Level.t -> Level.t - let hashcons hdir (b,n as x) = - let b' = hdir b in - if b' == b then x else (b',n) - let eq l1 l2 = - l1 == l2 || - match l1,l2 with - | (b,n), (b',n') -> b == b' && n == n' - - let hash (x, n) = n + Level.hash x - - end - - module HExpr = - struct - - module H = Hashcons.Make(ExprHash) - - type t = ExprHash.t - - let hcons = - Hashcons.simple_hcons H.generate H.hcons Level.hcons - let hash = ExprHash.hash - let eq x y = x == y || - (let (u,n) = x and (v,n') = y in - Int.equal n n' && Level.equal u v) - - end - - let hcons = HExpr.hcons - - let make l = hcons (l, 0) + let make l = (l, 0) - let prop = make Level.prop - let set = make Level.set - let type1 = hcons (Level.set, 1) + let prop = (Level.prop, 0) + let set = (Level.set, 0) + let type1 = (Level.set, 1) let is_prop = function | (l,0) -> Level.is_prop l @@ -363,13 +191,13 @@ struct let successor (u,n) = if Level.is_prop u then type1 - else hcons (u, n + 1) + else (u, n + 1) let addn k (u,n as x) = if k = 0 then x else if Level.is_prop u then - hcons (Level.set,n+k) - else hcons (u,n+k) + (Level.set,n+k) + else (u,n+k) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in @@ -394,31 +222,29 @@ struct let v' = f v in if v' == v then x else if Level.is_prop v' && n != 0 then - hcons (Level.set, n) - else hcons (v', n) + (Level.set, n) + else (v', n) end - - module Huniv = HList.Make(Expr.HExpr) - type t = Huniv.t - open Huniv - - let equal x y = x == y || - (Huniv.hash x == Huniv.hash y && - Huniv.for_all2 Expr.equal x y) - let make l = Huniv.tip (Expr.make l) - let tip x = Huniv.tip x - + type t = Expr.t list + + let tip u = [u] + let cons u v = u :: v + + let equal x y = x == y || List.equal Expr.equal x y + + let make l = tip (Expr.make l) + let pr l = match l with - | Cons (u, _, Nil) -> Expr.pr u + | [u] -> Expr.pr u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ + (prlist_with_sep pr_comma Expr.pr l) ++ str ")" let level l = match l with - | Cons (l, _, Nil) -> Expr.level l + | [l] -> Expr.level l | _ -> None (* The lower predicative level of the hierarchy that contains (impredicative) @@ -438,16 +264,16 @@ struct (* Returns the formal universe that lies juste above the universe variable u. Used to type the sort u. *) let super l = - Huniv.map (fun x -> Expr.successor x) l + List.map (fun x -> Expr.successor x) l let addn n l = - Huniv.map (fun x -> Expr.addn n x) l + List.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons (h1, _, t1), Cons (h2, _, t2) -> + | [], _ -> l2 + | _, [] -> l1 + | h1 :: t1, h2 :: t2 -> (match Expr.super h1 h2 with | Inl true (* h1 < h2 *) -> merge_univs t1 l2 | Inl false -> merge_univs l1 t2 @@ -459,28 +285,28 @@ struct let sort u = let rec aux a l = match l with - | Cons (b, _, l') -> + | b :: l' -> (match Expr.super a b with | Inl false -> aux a l' | Inl true -> l | Inr c -> if c <= 0 then cons a l else cons b (aux a l')) - | Nil -> cons a l + | [] -> cons a l in - fold (fun a acc -> aux a acc) u nil + List.fold_right (fun a acc -> aux a acc) u [] (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y - let empty = nil + let empty = [] - let exists = Huniv.exists + let exists = List.exists - let for_all = Huniv.for_all + let for_all = List.for_all - let smartmap = Huniv.smartmap + let smartmap = List.smartmap end @@ -768,9 +594,9 @@ let check_equal_expr g x y = let check_eq_univs g l1 l2 = let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in - Huniv.for_all (fun x1 -> exists x1 l2) l1 - && Huniv.for_all (fun x2 -> exists x2 l1) l2 + let exists x1 l = List.exists (fun x2 -> f x1 x2) l in + List.for_all (fun x1 -> exists x1 l2) l1 + && List.for_all (fun x2 -> exists x2 l1) l2 let check_eq g u v = Universe.equal u v || check_eq_univs g u v @@ -784,11 +610,11 @@ let check_smaller_expr g (u,n) (v,m) = | _ -> false let exists_bigger g ul l = - Huniv.exists (fun ul' -> + Universe.exists (fun ul' -> check_smaller_expr g ul ul') l let real_check_leq g u v = - Huniv.for_all (fun ul -> exists_bigger g ul v) u + Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = Universe.equal u v || @@ -1026,8 +852,8 @@ let check_univ_leq u v = let enforce_leq u v c = match v with - | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) -> - Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c + | [v] -> + List.fold_right (fun u -> constraint_add_leq u v) u c | _ -> anomaly (Pp.str"A universe bound can only be a variable.") let enforce_leq u v c = @@ -1080,63 +906,18 @@ end = struct type t = Level.t array - let empty : t = [||] - - module HInstancestruct = - struct - type _t = t - type t = _t - type u = Level.t -> Level.t - - let hashcons huniv a = - let len = Array.length a in - if Int.equal len 0 then empty - else begin - for i = 0 to len - 1 do - let x = Array.unsafe_get a i in - let x' = huniv x in - if x == x' then () - else Array.unsafe_set a i x' - done; - a - end - - let eq t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) - in aux 0) - - let hash a = - let accu = ref 0 in - for i = 0 to Array.length a - 1 do - let l = Array.unsafe_get a i in - let h = Level.hash l in - accu := Hashset.Combine.combine !accu h; - done; - (* [h] must be positive. *) - let h = !accu land 0x3FFFFFFF in - h - - end - - module HInstance = Hashcons.Make(HInstancestruct) - - let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons - - let empty = hcons [||] + let empty = [||] let is_empty x = Int.equal (Array.length x) 0 let subst_fn fn t = let t' = CArray.smartmap fn t in - if t' == t then t else hcons t' + if t' == t then t else t' let subst s t = let t' = CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t - in if t' == t then t else hcons t' + in if t' == t then t else t' let pr = prvect_with_sep spc Level.pr @@ -1296,7 +1077,7 @@ let subst_univs_expr_opt fn (l,n) = let subst_univs_universe fn ul = let subst, nosubst = - Universe.Huniv.fold (fun u (subst,nosubst) -> + List.fold_right (fun u (subst,nosubst) -> try let a' = subst_univs_expr_opt fn u in (a' :: subst, nosubst) with Not_found -> (subst, u :: nosubst)) @@ -1307,7 +1088,7 @@ let subst_univs_universe fn ul = let substs = List.fold_left Universe.merge_univs Universe.empty subst in - List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) + List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst let merge_context strict ctx g = diff --git a/checker/univ.mli b/checker/univ.mli index 0a21019b1..0eadc6801 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -164,7 +164,6 @@ sig val is_empty : t -> bool val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) diff --git a/checker/values.ml b/checker/values.ml index c95c3f1b2..86634fbd8 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 c802f941f368bedd96e931cda0559d67 checker/cic.mli +MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli *) @@ -54,6 +54,7 @@ let v_enum name n = Sum(name,n,[||]) let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 +let v_unit = v_enum "unit" 1 let v_ref v = v_tuple "ref" [|v|] let v_set v = @@ -98,7 +99,7 @@ let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;Int|] -let rec v_univ = Sum ("universe", 1, [| [|v_expr; Int; v_univ|] |]) +let v_univ = List v_expr let v_cstrs = Annot @@ -311,13 +312,13 @@ and v_impl = Sum ("module_impl",2, (* Abstract, FullStruct *) [|[|v_mexpr|]; (* Algebraic *) [|v_sign|]|]) (* Struct *) -and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) +and v_noimpl = v_unit and v_module = Tuple ("module_body", [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) (** kernel/safe_typing *) |