diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/environ.ml | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 6 | ||||
| -rw-r--r-- | checker/typeops.ml | 4 | ||||
| -rw-r--r-- | checker/validate.ml | 1 | ||||
| -rw-r--r-- | checker/values.ml | 15 | ||||
| -rw-r--r-- | checker/values.mli | 1 | ||||
| -rw-r--r-- | checker/votour.ml | 2 |
7 files changed, 22 insertions, 9 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index 74cf237763..b172acb126 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -183,7 +183,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined.") + Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8f11e01c33..1fd86bc368 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds = (************************************************************************) (************************************************************************) +let print_mutind ind = + let kn = MutInd.user ind in + str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn)) + let check_inductive env kn mib = - Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); + Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn); (* check mind_constraints: should be consistent with env *) let env0 = match mib.mind_universes with diff --git a/checker/typeops.ml b/checker/typeops.ml index 138fe8bc95..e4c3f4ae4b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif diff --git a/checker/validate.ml b/checker/validate.ml index f831875dd4..c214409a2c 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -85,6 +85,7 @@ let rec val_gen v ctx o = match v with | Fail s -> fail ctx o ("unexpected object " ^ s) | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o | Dyn -> val_dyn ctx o + | Proxy { contents = v } -> val_gen v ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the diff --git a/checker/values.ml b/checker/values.ml index 801874773a..35027d5bfb 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -45,6 +45,13 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref + +let fix (f : value -> value) : value = + let self = ref Any in + let ans = f (Proxy self) in + let () = self := ans in + ans (** Some pseudo-constructors *) @@ -347,18 +354,16 @@ let v_states = v_pair Any v_frozen let v_state = Tuple ("state", [|v_states; Any; v_bool|]) let v_vcs = - let data = Opt Any in - let vcs = + let vcs self = Tuple ("vcs", [|Any; Any; Tuple ("dag", [|Any; Any; v_map Any (Tuple ("state_info", - [|Any; Any; Opt v_state; v_pair data Any|])) + [|Any; Any; Opt v_state; v_pair (Opt self) Any|])) |]) |]) in - let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in - vcs + fix vcs let v_uuid = Any let v_request id doc = diff --git a/checker/values.mli b/checker/values.mli index 20b9d54a68..1b1437a469 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -20,6 +20,7 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref val v_univopaques : value val v_libsum : value diff --git a/checker/votour.ml b/checker/votour.ml index bc820e23dd..1ea0de456e 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -152,6 +152,7 @@ let rec get_name ?(extra=false) = function |String -> "string" |Annot (s,v) -> s^"/"^get_name ~extra v |Dyn -> "<dynamic>" + | Proxy v -> get_name ~extra !v (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) @@ -255,6 +256,7 @@ let rec get_children v o pos = match v with | _ -> raise Exit end |Fail s -> raise Forbidden + | Proxy v -> get_children !v o pos let get_children v o pos = try get_children v o pos |