sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
- | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+ | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+ | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
| "CProp" -> `CProp (CicUniv.fresh ())
]
];
type ncommand =
| UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
| NObj of loc * CicNotationPt.term CicNotationPt.obj
- | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
+ | NUnivConstraint of loc * NUri.uri * NUri.uri
| NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
| NCoercion of loc * string *
CicNotationPt.term * CicNotationPt.term *
status,`New []
;;
-let basic_eval_add_constraint (s,u1,u2) status =
- NCicLibrary.add_constraint status s u1 u2
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
;;
let inject_constraint =
- let basic_eval_add_constraint (s,u1,u2)
+ let basic_eval_add_constraint (u1,u2)
~refresh_uri_in_universe
~refresh_uri_in_term
=
let u1 = refresh_uri_in_universe u1 in
let u2 = refresh_uri_in_universe u2 in
- basic_eval_add_constraint (s,u1,u2)
+ basic_eval_add_constraint (u1,u2)
in
NRstatus.Serializer.register "constraints" basic_eval_add_constraint
;;
-let eval_add_constraint status s u1 u2 =
- let status = basic_eval_add_constraint (s,u1,u2) status in
- let dump = inject_constraint (s,u1,u2)::status#dump in
+let eval_add_constraint status u1 u2 =
+ let status = basic_eval_add_constraint (u1,u2) status in
+ let dump = inject_constraint (u1,u2)::status#dump in
let status = status#set_dump dump in
status,`Old []
;;
in
status, concat_nuris uris nuris
with
- NCicTypeChecker.TypeCheckerFailure msg
- when Lazy.force msg =
- "Sort elimination not allowed" ->
+ | MultiPassDisambiguator.DisambiguationError _
+ | NCicTypeChecker.TypeCheckerFailure _ ->
+ HLog.warn "error in generating projection/eliminator";
status,uris
) (status,`New [] (* uris *)) boxml in
let coercions =
let status,uris =
List.fold_left
(fun (status,uris) (name,cpos,arity) ->
- let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] []
- ("",0,CicNotationPt.Ident (name,None)) in
- assert (metasenv = [] && subst = []);
- let status, nuris =
- NCicCoercDeclaration.
- basic_eval_and_record_ncoercion_from_t_cpos_arity
- status (name,t,cpos,arity)
- in
- let uris = concat_nuris nuris uris in
- status, uris)
+ try
+ let metasenv,subst,status,t =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+ ("",0,CicNotationPt.Ident (name,None)) in
+ assert (metasenv = [] && subst = []);
+ let status, nuris =
+ NCicCoercDeclaration.
+ basic_eval_and_record_ncoercion_from_t_cpos_arity
+ status (name,t,cpos,arity)
+ in
+ let uris = concat_nuris nuris uris in
+ status, uris
+ with MultiPassDisambiguator.DisambiguationError _->
+ HLog.warn ("error in generating coercion: "^name);
+ status, uris)
(status,uris) coercions
in
status,uris
[] ->
eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
| _ -> status,`New [])
- | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
- eval_add_constraint status strict [false,u1] [false,u2]
+ | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
+ eval_add_constraint status [`Type,u1] [`Type,u2]
;;
let rec eval_command = {ec_go = fun ~disambiguate_command opts status
in
G.NObj (loc, N.Inductive (params, ind_types))
| IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
- strict = [ SYMBOL <:unicode<lt>> -> true
- | SYMBOL <:unicode<leq>> -> false ];
- u2 = tactic_term ->
- let u1 =
- match u1 with
+ SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
+ let urify = function
| CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
- NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
- | _ -> raise (Failure "only a sort can be constrained")
+ | _ -> raise (Failure "only a Type[…] sort can be constrained")
in
- let u2 =
- match u2 with
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
- NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
- | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
- NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
- | _ -> raise (Failure "only a sort can be constrained")
- in
- G.NUnivConstraint (loc, strict,u1,u2)
+ let u1 = urify u1 in
+ let u2 = urify u2 in
+ G.NUnivConstraint (loc,u1,u2)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
| IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
;;
let refine_obj
- ~rdb metasenv subst context _uri
+ ~rdb metasenv subst _context _uri
~use_coercions obj _ _ugraph ~localization_tbl
=
assert (metasenv=[]);
let localise t =
try NCicUntrusted.NCicHash.find localization_tbl t
with Not_found ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
(*assert false*)HExtlib.dummy_floc
in
try
with Not_found ->
try NCic.Const (List.assoc name obj_context)
with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+ Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
| CicNotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
NCic.Meta (index, (0, NCic.Ctx cic_subst))
| CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
- [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+ [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
- [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
+ [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
| CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
- [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+ [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
- [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
+ [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
- [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
+ [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| CicNotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
let mk_type n =
if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let mk_cprop n =
if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
try
let rec aux = function
| a::(b::_ as tl) ->
- NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
- NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
- NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
- NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
- NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
- NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+ NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+ NCicEnvironment.add_lt_constraint (mk_type a) (mk_cprop b);
aux tl
- | [a] ->
- NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
- NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
| _ -> ()
in
aux lll
(********************************* TERMS ************************************)
-type universe = (bool * NUri.uri) list
+type univ_algebra = [ `Type | `Succ | `CProp ]
+
+type universe = (univ_algebra * NUri.uri) list
(* Max of non-empty list of named universes, or their successor (when true)
* The empty list represents type0 *)
let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;;
-let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+let cprop = [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")];;
let nn_2_on = function
| "_" -> Cic.Anonymous
let type0 = []
-let max l1 l2 =
- HExtlib.list_uniq ~eq:(fun (b1,u1) (b2,u2) -> b1=b2 && NUri.eq u1 u2)
- (List.sort (fun (b1,u1) (b2,u2) ->
- let res = compare b1 b2 in if res = 0 then NUri.compare u1 u2 else res)
- (l1 @ l2))
+module F = Format
+
+let rec ppsort f = function
+ | C.Prop -> F.fprintf f "Prop"
+ | (C.Type []) -> F.fprintf f "Type0"
+ | (C.Type [`Type, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
+ | (C.Type [`Succ, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
+ | (C.Type [`CProp, u]) -> F.fprintf f "P(%s)" (NUri.name_of_uri u)
+ | (C.Type l) ->
+ F.fprintf f "Max(";
+ ppsort f ((C.Type [List.hd l]));
+ List.iter (fun x -> F.fprintf f ",";ppsort f ((C.Type [x]))) (List.tl l);
+ F.fprintf f ")"
+;;
-let le_constraints = ref [] (* strict,a,b *)
+let string_of_univ u =
+ let b = Buffer.create 100 in
+ let f = Format.formatter_of_buffer b in
+ ppsort f (NCic.Type u);
+ Format.fprintf f "@?";
+ Buffer.contents b
+;;
-let rec le_path_uri avoid strict a b =
- (not strict && NUri.eq a b) ||
- List.exists
- (fun (strict',x,y) ->
- NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
- le_path_uri (x::avoid) (strict && not strict') a x
- ) !le_constraints
+let eq_univ (b1,u1) (b2,u2) = b1=b2 && NUri.eq u1 u2;;
+
+let max (l1:NCic.universe) (l2:NCic.universe) =
+ match l2 with
+ | x::tl ->
+ let rest = List.filter (fun y -> not (eq_univ x y)) (l1@tl) in
+ x :: HExtlib.list_uniq ~eq:eq_univ
+ (List.sort (fun (b1,u1) (b2,u2) ->
+ let res = compare b1 b2 in
+ if res = 0 then NUri.compare u1 u2 else res)
+ rest)
+ | [] ->
+ match l1 with
+ | [] -> []
+ | ((`Type|`Succ), _)::_ -> l1
+ | (`CProp, u)::tl -> (`Type, u)::tl
;;
-let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
+let lt_constraints = ref [] (* a,b := a < b *)
-let universe_leq a b =
- match a, b with
- | a,[(false,b)] -> List.for_all (fun a -> leq_path a b) a
- | _,_ ->
- raise (BadConstraint
- (lazy "trying to check if a universe is less or equal than an inferred universe"))
+let rec lt_path_uri avoid a b =
+ List.exists
+ (fun (x,y) ->
+ NUri.eq y b &&
+ (NUri.eq a x ||
+ (not (List.exists (NUri.eq x) avoid) &&
+ lt_path_uri (x::avoid) a x))
+ ) !lt_constraints
+;;
+
+let lt_path a b = lt_path_uri [b] a b;;
let universe_eq a b =
match a,b with
- | [(false,_)], [(false,_)] -> universe_leq b a && universe_leq a b
- | _, [(false,_)]
- | [(false,_)],_ -> false
+ | [(`Type|`CProp) as b1, u1], [(`Type|`CProp) as b2, u2] ->
+ b1 = b2 && NUri.eq u1 u2
+ | _, [(`Type|`CProp),_]
+ | [(`Type|`CProp),_],_ -> false
| _ ->
raise (BadConstraint
(lazy "trying to check if two inferred universes are equal"))
;;
-let pp_constraint b x y =
- NUri.name_of_uri x ^ (if b then " < " else " <= ") ^ NUri.name_of_uri y
+let universe_leq a b =
+ match a, b with
+ | (((`Type|`Succ),_)::_ | []) , [`CProp,_] -> false
+ | l, [((`Type|`CProp),b)] ->
+ List.for_all
+ (function
+ | `Succ,a -> lt_path a b
+ | _, a -> NUri.eq a b || lt_path a b) l
+ | _, ([] | [`Succ,_] | _::_::_) ->
+ raise (BadConstraint (lazy (
+ "trying to check if "^string_of_univ a^
+ " is leq than the inferred universe " ^ string_of_univ b)))
+;;
+
+let are_sorts_convertible ~test_eq_only s1 s2 =
+ match s1,s2 with
+ | C.Type a, C.Type b when not test_eq_only -> universe_leq a b
+ | C.Type a, C.Type b -> universe_eq a b
+ | C.Prop,C.Type _ -> (not test_eq_only)
+ | C.Prop, C.Prop -> true
+ | _ -> false
+;;
+
+let pp_constraint x y =
+ NUri.name_of_uri x ^ " < " ^ NUri.name_of_uri y
;;
let pp_constraints () =
- String.concat "\n" (List.map (fun (b,x,y) -> pp_constraint b x y) !le_constraints)
+ String.concat "\n" (List.map (fun (x,y) -> pp_constraint x y) !lt_constraints)
;;
let universes = ref [];;
-let get_universes () = List.map (fun x -> [false,x]) !universes;;
+let get_universes () =
+ List.map (fun x -> [`Type,x]) !universes @
+ List.map (fun x -> [`CProp,x]) !universes
+;;
let is_declared u =
match u with
- [false,x] -> List.exists (fun y -> NUri.eq x y) !universes
- | _ -> assert false
+ | [(`CProp|`Type),x] -> List.exists (fun y -> NUri.eq x y) !universes
+ | _ -> assert false
+;;
+
+exception UntypableSort of string Lazy.t
+exception AssertFailure of string Lazy.t
+
+let typeof_sort = function
+ | C.Type ([(`Type|`CProp),u] as univ) ->
+ if is_declared univ then (C.Type [`Succ, u])
+ else
+ raise (UntypableSort (lazy ("undeclared universe " ^
+ NUri.string_of_uri u ^ "\ndeclared ones are: " ^
+ String.concat ", " (List.map NUri.string_of_uri !universes)
+ )))
+ | C.Type t ->
+ raise (AssertFailure (lazy (
+ "Cannot type an inferred type: "^ string_of_univ t)))
+ | C.Prop -> (C.Type type0)
;;
-let add_constraint strict a b =
+let add_lt_constraint a b =
match a,b with
- | [false,a2],[false,b2] ->
- if not (le_path_uri [] strict a2 b2) then (
- if le_path_uri [] (not strict) b2 a2 then
- (raise(BadConstraint(lazy("universe inconsistency adding "^pp_constraint strict a2 b2
+ | [`Type,a2],[`Type,b2] ->
+ if not (lt_path_uri [] a2 b2) then (
+ if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+ (raise(BadConstraint(lazy("universe inconsistency adding "^
+ pp_constraint a2 b2
^ " to:\n" ^ pp_constraints ()))));
universes := a2 :: b2 ::
List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
- le_constraints := (strict,a2,b2) :: !le_constraints);
- history := (`Constr (strict,a,b))::!history;
+ lt_constraints := (a2,b2) :: !lt_constraints);
+ history := (`Constr (a,b))::!history;
| _ -> raise (BadConstraint
(lazy "trying to add a constraint on an inferred universe"))
;;
let sup l =
match l with
- | [false,_] -> Some l
+ | [(`Type|`CProp),_] -> Some l
| l ->
- let bigger_than acc (s1,n1) = List.filter (le_path_uri [] s1 n1) acc in
+ let bigger_than acc (_s1,n1) =
+ List.filter (fun x -> lt_path_uri [] n1 x || NUri.eq n1 x) acc
+ in
let solutions = List.fold_left bigger_than !universes l in
+ let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in
let rec aux = function
| [] -> None
| u :: tl ->
- if List.exists (fun x -> le_path_uri [] true x u) solutions then aux tl
- else Some [false,u]
+ if List.exists (fun x -> lt_path_uri [] x u) solutions then aux tl
+ else Some [fam,u]
in
aux solutions
;;
+let allowed_sort_elimination s1 s2 =
+ match s1, s2 with
+ | C.Type (((`Type|`Succ),_)::_ | []), C.Type (((`Type|`Succ),_)::_ | [])
+ | C.Type _, C.Type ((`CProp,_)::_)
+ | C.Type _, C.Prop
+ | C.Prop, C.Prop -> `Yes
+ | C.Type ((`CProp,_)::_), C.Type (((`Type|`Succ),_)::_ | [])
+ | C.Prop, C.Type _ -> `UnitOnly
+;;
let typecheck_obj,already_set = ref (fun _ -> assert false), ref false;;
let set_typecheck_obj f =
List.iter
(function
| `Obj (uri,_) -> NUri.UriHash.remove cache uri
- | `Constr (strict,[_,u1],[_,u2]) as c ->
- let w = strict,u1,u2 in
+ | `Constr ([_,u1],[_,u2]) as c ->
+ let w = u1,u2 in
if not(List.mem c !history) then
- le_constraints := List.filter ((<>) w) !le_constraints;
+ lt_constraints := List.filter ((<>) w) !lt_constraints;
| `Constr _ -> assert false
) to_be_deleted
;;
exception CircularDependency of string Lazy.t;;
exception ObjectNotFound of string Lazy.t;;
exception BadDependency of string Lazy.t * exn;;
-exception BadConstraint of string Lazy.t;;
exception AlreadyDefined of string Lazy.t;;
val set_get_obj: (NUri.uri -> NCic.obj) -> unit
val get_relevance: NReference.reference -> bool list
-val type0: NCic.universe
-val get_universes: unit -> NCic.universe list
-val is_declared: NCic.universe -> bool
-val max: NCic.universe -> NCic.universe -> NCic.universe
-(* universe_* raise BadConstraints if the second arg. is an inferred universe *)
-val universe_eq: NCic.universe -> NCic.universe -> bool
-val universe_leq: NCic.universe -> NCic.universe -> bool
-(* add_constraint raise BadConstraint in case of universe inconsistency
- or if the second argument is an inferred universe
- true -> strict check (<); false -> loose check (<=)
-*)
-val add_constraint: bool -> NCic.universe -> NCic.universe -> unit
-val sup : NCic.universe -> NCic.universe option
-val pp_constraints: unit -> string
-
val get_checked_def:
NReference.reference ->
NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
(* invalidate the object and all those that entered the environment after it *)
val invalidate_item:
[ `Obj of NUri.uri * NCic.obj
- | `Constr of bool * NCic.universe * NCic.universe ] -> unit
+ | `Constr of NCic.universe * NCic.universe ] -> unit
val invalidate: unit -> unit
val set_typecheck_obj: (NCic.obj -> unit) -> unit
+(* =========== universes ============= *)
+
+(* utils *)
+val ppsort : Format.formatter -> NCic.sort -> unit
+val pp_constraints: unit -> string
+val get_universes: unit -> NCic.universe list
+
+(* The type of Prop, smaller than any other type *)
+val type0: NCic.universe
+
+(* use to type products *)
+val max: NCic.universe -> NCic.universe -> NCic.universe
+
+(* raise BadConstraints if the second arg. is an inferred universe or
+ * if the added constraint gives circularity *)
+exception BadConstraint of string Lazy.t;;
+val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val universe_eq: NCic.universe -> NCic.universe -> bool
+val universe_leq: NCic.universe -> NCic.universe -> bool
+
+(* checks if s1 <= s2 *)
+val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
+
+(* to type a Match *)
+val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
+
+(* algebraic successor function *)
+exception UntypableSort of string Lazy.t
+exception AssertFailure of string Lazy.t
+val typeof_sort: NCic.sort -> NCic.sort
+
+(* looks for a declared universe that is the least one above the input *)
+val sup : NCic.universe -> NCic.universe option
+
+(* =========== /universes ============= *)
+
(* EOF *)
type timestamp =
[ `Obj of NUri.uri * NCic.obj
- | `Constr of bool * NCic.universe * NCic.universe] list *
+ | `Constr of NCic.universe * NCic.universe] list *
(NUri.uri * string * NReference.reference) list *
NCic.obj NUri.UriMap.t *
NUri.uri list
status#set_timestamp (!storage,!local_aliases,!cache,!includes)
;;
-let add_constraint status strict u1 u2 =
- NCicEnvironment.add_constraint strict u1 u2;
- storage := (`Constr (strict,u1,u2)) :: !storage;
+let add_constraint status u1 u2 =
+ NCicEnvironment.add_lt_constraint u1 u2;
+ storage := (`Constr (u1,u2)) :: !storage;
status#set_timestamp (!storage,!local_aliases,!cache,!includes)
;;
(* it also checks it and add it to the environment *)
val add_obj: #status as 'status -> NCic.obj -> 'status
val add_constraint:
- #status as 'status -> bool -> NCic.universe -> NCic.universe -> 'status
+ #status as 'status -> NCic.universe -> NCic.universe -> 'status
val aliases_of: NUri.uri -> NReference.reference list
val resolve: string -> NReference.reference list
(* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
(List.map (NCicSubstitution.lift shift) (List.tl l));
end;
F.fprintf f "])"
- | C.Sort C.Prop -> F.fprintf f "Prop"
- | C.Sort (C.Type []) -> F.fprintf f "Type0"
- | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
- | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
- | C.Sort (C.Type l) ->
- F.fprintf f "Max(";
- aux ctx (C.Sort (C.Type [List.hd l]));
- List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
- (List.tl l);
- F.fprintf f ")"
+ | C.Sort s -> NCicEnvironment.ppsort f s
in
aux ~toplevel:true (List.map fst context) t
;;
true
else
match (t1,t2) with
- | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
- NCicEnvironment.universe_leq a b
- | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
- NCicEnvironment.universe_eq a b
- | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only)
- | (C.Sort C.Prop, C.Sort C.Prop) -> true
+ | C.Sort s1, C.Sort s2 ->
+ NCicEnvironment.are_sorts_convertible ~test_eq_only s1 s2
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux true context s1 s2 &&
with Failure _ ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
- | C.Sort (C.Type ([false,u] as univ)) ->
- if NCicEnvironment.is_declared univ then
- C.Sort (C.Type [true, u])
- else
- raise (TypeCheckerFailure (lazy ("undeclared universe " ^
- NUri.string_of_uri u)))
- | C.Sort (C.Type _) ->
- raise (AssertFailure (lazy ("Cannot type an inferred type: "^
- NCicPp.ppterm ~subst ~metasenv ~context t)))
- | C.Sort _ -> C.Sort (C.Type NCicEnvironment.type0)
+ | C.Sort s ->
+ (try C.Sort (NCicEnvironment.typeof_sort s)
+ with
+ | NCicEnvironment.UntypableSort msg -> raise (TypeCheckerFailure msg)
+ | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
| C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
| C.Meta (n,l) as t ->
let canonical_ctx,ty =
(PP.ppterm ~subst ~metasenv ~context so)
)));
(match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
- | (C.Sort C.Type _, C.Sort _)
- | (C.Sort C.Prop, C.Sort C.Prop) -> ()
- | (C.Sort C.Prop, C.Sort C.Type _) ->
+ | C.Sort s1, C.Sort s2 ->
+ (match NCicEnvironment.allowed_sort_elimination s1 s2 with
+ | `Yes -> ()
+ | `UnitOnly ->
(* TODO: we should pass all these parameters since we
* have them already *)
let _,leftno,itl,_,i = E.get_checked_indtys r in
is_non_informative ~metasenv ~subst leftno constrty))
then
raise (TypeCheckerFailure (lazy
- ("Sort elimination not allowed")));
- | _,_ -> ())
+ ("Sort elimination not allowed"))))
+ | _ -> ())
| _,_ -> ()
in
aux
match R.whd ~subst context c with
| C.Prod (n,so,de) ->
let s = typeof ~metasenv ~subst context so in
- s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
+ (s = C.Sort C.Prop ||
+ match s with C.Sort (C.Type ((`CProp,_)::_)) -> true | _ -> false) &&
+ aux ((n,(C.Decl so))::context) de
| _ -> true in
let context',dx = NCicReduction.split_prods ~subst [] paramsno c in
aux context' dx
let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
let mk_type n =
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let mk_cprop n =
if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let is_proof_irrelevant context ty =
;;
let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
- let initial_timestamp = Unix.gettimeofday () in
+ let _initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
in
nCicMetaSubst.cmi:
nCicUnifHint.cmi:
nCicCoercion.cmi: nCicUnifHint.cmi
-nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi
+nRstatus.cmi: nCicCoercion.cmi
nCicUnification.cmi: nRstatus.cmi
nCicRefiner.cmi: nRstatus.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nCicCoercion.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
nCicCoercion.cmi
-nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi
-nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi
+nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi
+nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi
nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
nCicCoercion.cmi nCicUnification.cmi
nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
let mk_type n =
if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
let mk_cprop n =
if n = 0 then
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
else
- [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+ [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
;;
try
let rec aux = function
| a::(b::_ as tl) ->
- NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
- NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
- NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
- NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
- NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
- NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+ NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+ NCicEnvironment.add_lt_constraint (mk_cprop a) (mk_cprop b);
aux tl
- | [a] ->
- NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
- NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
| _ -> ()
in
aux lll
raise (RefineFailure (lazy (localise t,"unbound variable"))))
in
metasenv, subst, t, infty
- | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
- | C.Sort (C.Type _) ->
- raise (AssertFailure (lazy ("Cannot type an inferred type: "^
- NCicPp.ppterm ~subst ~metasenv ~context t)))
- | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+ | C.Sort s ->
+ (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+ with
+ | NCicEnvironment.UntypableSort msg ->
+ raise (RefineFailure (lazy (localise t, Lazy.force msg)))
+ | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
| C.Implicit infos ->
let metasenv,_,t,ty =
exp_implicit ~localise metasenv context expty t infos
| None -> metasenv, subst, None
| Some x ->
let m, s, x =
- NCicUnification.delift_term_wrt_terms
+ NCicUnification.delift_type_wrt_terms
rdb metasenv subst context x [t]
in
m, s, Some x
let pp _ = ();;
-let ppcontext = NCicPp.ppcontext;;
-let ppmetasenv = NCicPp.ppmetasenv;;
+let ppcontext ~metasenv ~subst c =
+ "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
+;;
+let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
-let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "...";;
-let ppmetasenv ~subst:_subst _metasenv = "...";;
+let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
+let ppmetasenv ~subst:_subst _metasenv = "";;
let fix_sorts swap exc t =
let rec aux () = function
metasenv, subst, bo
| (arg,ty)::tail ->
let metasenv, subst, telescopic_ty =
- delift_term_wrt_terms rdb metasenv subst context_of_args ty
+(* XXX if processed_args = [] then metasenv, subst, ty else *)
+ delift_type_wrt_terms rdb metasenv subst context_of_args ty
(List.rev processed_args)
in
let name = "HBeta"^string_of_int n in
in
metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
in
- mk_lambda metasenv subst context 0 [] argsty
+ let rc = mk_lambda metasenv subst context 0 [] argsty in
+ rc
and instantiate rdb test_eq_only metasenv subst context n lc t swap =
(*D*) inside 'I'; try let rc =
(* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
| _ ->
pp (lazy (
- "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
- ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+ "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+ ppcontext ~metasenv ~subst context ^
ppmetasenv ~subst metasenv));
let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
let t, ty_t =
if ft == t then
(prerr_endline ( ("ILLTYPED: " ^
NCicPp.ppterm ~metasenv ~subst ~context t
- ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
- ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+ ^ "\nBECAUSE:" ^ Lazy.force msg ^
+ ppcontext ~metasenv ~subst context ^
ppmetasenv ~subst metasenv
));
assert false)
in
pp (lazy(string_of_int n ^ " := 222 = "^
NCicPp.ppterm ~metasenv ~subst ~context:ctx t
- ^ "\n" ^ ppmetasenv ~subst metasenv));
+ ^ ppmetasenv ~subst metasenv));
(* Unifying the types may have already instantiated n. *)
try
let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
let fo_unif test_eq_only metasenv subst t1 t2 =
(*D*) inside 'F'; try let rc =
pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
- NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ ppmetasenv
+ NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
~subst metasenv));
if t1 === t2 then
metasenv, subst
| Uncertain _ -> raise exn
(*D*) in outside(); rc with exn -> outside (); raise exn
-and delift_term_wrt_terms rdb metasenv subst context t args =
+and delift_type_wrt_terms rdb metasenv subst context t args =
let metasenv, _, instance, _ =
- NCicMetaSubst.mk_meta metasenv context `Term in
+ NCicMetaSubst.mk_meta metasenv context `Type in
let meta_applied = NCicUntrusted.mk_appl instance args in
let metasenv,subst,meta_applied,_ =
!refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db)
indent := "";
unify rdb test_eq_only;;
-let fix_sorts = fix_sorts false (UnificationFailure (lazy "no sup"));;
+let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));;
(* this should be moved elsewhere *)
val fix_sorts: NCic.term -> NCic.term
-val delift_term_wrt_terms:
+val delift_type_wrt_terms:
#NRstatus.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term list ->
nCicTacReduction.cmi:
nTacStatus.cmi:
-nTactics.cmi: nTacStatus.cmi
nCicElim.cmi:
+nTactics.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi
-nTactics.cmo: nTacStatus.cmi nTactics.cmi
-nTactics.cmx: nTacStatus.cmx nTactics.cmi
nCicElim.cmo: nCicElim.cmi
nCicElim.cmx: nCicElim.cmi
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi
nCicTacReduction.cmi:
nTacStatus.cmi:
-nTactics.cmi: nTacStatus.cmi
nCicElim.cmi:
+nTactics.cmi: nTacStatus.cmi
nCicTacReduction.cmo: nCicTacReduction.cmi
nCicTacReduction.cmx: nCicTacReduction.cmi
nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi
-nTactics.cmo: nTacStatus.cmi nTactics.cmi
-nTactics.cmx: nTacStatus.cmx nTactics.cmi
nCicElim.cmo: nCicElim.cmi
nCicElim.cmx: nCicElim.cmi
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi
INTERFACE_FILES = \
nCicTacReduction.mli \
nTacStatus.mli \
- nTactics.mli \
- nCicElim.mli
+ nCicElim.mli \
+ nTactics.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
;;
let ast_of_sort s =
+ let headrm prefix s =
+ try
+ let len_prefix = String.length prefix in
+ assert (String.sub s 0 len_prefix = prefix);
+ String.sub s len_prefix (String.length s - len_prefix)
+ with Invalid_argument _ -> assert false
+ in
match s with
- NCic.Prop -> `Prop,"ind"
- | NCic.Type u ->
- let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
- (try
- if String.sub u 0 4 = "Type" then
- `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
- else if String.sub u 0 5 = "CProp" then
- `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
- else
- (prerr_endline u;
- assert false)
- with Failure _ -> assert false)
+ | NCic.Prop -> `Prop,"ind"
+ | NCic.Type [] -> `NType "", "rect_Type"
+ | NCic.Type ((`Type,u) :: _) ->
+ let name = NUri.name_of_uri u in
+ `NType (headrm "Type" name), "rect_" ^ name
+ | NCic.Type ((`CProp,u) :: _) ->
+ let name = NUri.name_of_uri u in
+ `NCProp (headrm "Type" name),
+ "rect_" ^ Str.replace_first (Str.regexp "Type") "CProp" name
+ | _ -> assert false
;;
let mk_elims (uri,_,_,_,obj) =
val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
+val ast_of_sort :
+ NCic.sort -> [> `NCProp of string | `NType of string | `Prop ] * string
exception Error of string lazy_t * exn option
let fail ?exn msg = raise (Error (msg,exn))
-let wrap f x =
+let wrap f x =
try f x
with
| MultiPassDisambiguator.DisambiguationError _
exec id_tac status goal)
;;
+let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
+ let goalty = get_goalty status goal in
+ let status,sort = typeof status (ctx_of goalty) goalty in
+ let sort = fix_sorts sort in
+ let status, sort = term_of_cic_term status sort (ctx_of goalty) in
+ sortref := sort;
+ status)
+;;
+
let elim_tac ~what:(txt,len,what) ~where =
let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
let indtyinfo = ref None in
- let sort = ref None in
- let compute_goal_sort_tac = distribute_tac (fun status goal ->
- let goalty = get_goalty status goal in
- let status, goalsort = typeof status (ctx_of goalty) goalty in
- let goalsort = fix_sorts goalsort in
- sort := Some goalsort;
- exec id_tac status goal)
- in
+ let sort = ref (NCic.Rel 1) in
atomic_tac (block_tac [
analyze_indty_tac ~what indtyinfo;
(fun s -> select_tac
~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
- compute_goal_sort_tac;
+ sort_of_goal_tac sort;
(fun status ->
- let sort = HExtlib.unopt !sort in
let ity = HExtlib.unopt !indtyinfo in
let NReference.Ref (uri, _) = ity.reference in
- let status, sort = term_of_cic_term status sort (ctx_of sort) in
- let name = NUri.name_of_uri uri ^
- match sort with
- | NCic.Sort NCic.Prop -> "_ind"
- | NCic.Sort NCic.Type u ->
- "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] sort
- | _ -> assert false
+ let name =
+ NUri.name_of_uri uri ^ "_" ^
+ snd (NCicElim.ast_of_sort
+ (match !sort with NCic.Sort x -> x | _ -> assert false))
in
let eliminator =
let _,_,w = what in
exact_tac ("",0,eliminator) status) ])
;;
-let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
- let goalty = get_goalty status goal in
- let status,sort = typeof status (ctx_of goalty) goalty in
- let status,sort = term_of_cic_term status sort (ctx_of goalty) in
- sortref := sort;
- status)
-;;
-
let rewrite_tac ~dir ~what:(_,_,what) ~where status =
let sortref = ref (NCic.Rel 1) in
let status = sort_of_goal_tac sortref status in
- let suffix =
- match !sortref with
- | NCic.Sort NCic.Prop -> "_ind"
- | NCic.Sort NCic.Type u ->
- "_rect_" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] !sortref
- | _ -> assert false
+ let suffix = "_" ^ snd (NCicElim.ast_of_sort
+ (match !sortref with NCic.Sort x -> x | _ -> assert false))
in
let name =
match dir with
-o-basic_pairs.ma notation.ma o-algebra.ma
basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
-o-saturations.ma o-algebra.ma
-saturations.ma relations.ma
+o-basic_pairs.ma notation.ma o-algebra.ma
o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
basic_pairs.ma notation.ma relations.ma
-formal_topologies.ma basic_topologies.ma
+saturations.ma relations.ma
+o-saturations.ma o-algebra.ma
o-algebra.ma categories.ma
categories.ma cprop_connectives.ma
+formal_topologies.ma basic_topologies.ma
o-formal_topologies.ma o-basic_topologies.ma
saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
-subsets.ma categories.ma
basic_topologies.ma relations.ma saturations.ma
concrete_spaces.ma basic_pairs.ma
-r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma
+subsets.ma categories.ma
relations.ma subsets.ma
+r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma o-basic_pairs_to_o-basic_topologies.ma
concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma
o-basic_topologies.ma o-algebra.ma o-saturations.ma
notation.ma
basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
-apply_functor.ma categories.ma
+apply_functor.ma categories.ma notation.ma
cprop_connectives.ma logic/connectives.ma
-relations_to_o-algebra.ma o-algebra.ma relations.ma
o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
+relations_to_o-algebra.ma o-algebra.ma relations.ma
logic/connectives.ma
include "logic/pts.ma".
-ninductive True: CProp ≝
+ninductive True: CProp[0] ≝
I : True.
-ninductive False: CProp ≝.
+ninductive False: CProp[0] ≝.
-ndefinition Not: CProp → CProp ≝
+ndefinition Not: CProp[0] → CProp[0] ≝
λA. A → False.
interpretation "logical not" 'not x = (Not x).
-ninductive And (A,B:CProp) : CProp ≝
+ninductive And (A,B:CProp[0]) : CProp[0] ≝
conj : A → B → And A B.
interpretation "logical and" 'and x y = (And x y).
-ninductive Or (A,B:CProp) : CProp ≝
+ninductive Or (A,B:CProp[0]) : CProp[0] ≝
or_introl : A → Or A B
| or_intror : B → Or A B.
interpretation "logical or" 'or x y = (Or x y).
-ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
+ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
ex_intro: ∀x:A. P x → Ex A P.
-ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
ex_intro1: ∀x:A. P x → Ex1 A P.
interpretation "exists1" 'exists x = (Ex1 ? x).
interpretation "exists" 'exists x = (Ex ? x).
-nrecord iff (A,B: CProp) : CProp ≝
+nrecord iff (A,B: CProp[0]) : CProp[0] ≝
{ if: A → B;
fi: B → A
}.
(* *)
(**************************************************************************)
-universe constraint Type[0] ≤ CProp[0].
-universe constraint CProp[0] ≤ Type[0].
-
-universe constraint Type[1] ≤ CProp[1].
-universe constraint CProp[1] ≤ Type[1].
-
-universe constraint Type[2] ≤ CProp[2].
-universe constraint CProp[2] ≤ Type[2].
-
universe constraint Type[0] < Type[1].
-universe constraint CProp[0] < CProp[1].
-
universe constraint Type[1] < Type[2].
-universe constraint CProp[1] < CProp[2].
\ No newline at end of file
+
include "nat/minus.ma".
include "datatypes/pairs.ma".
-alias symbol "eq" (instance 2) = "leibnitz's equality".
-alias symbol "eq" (instance 1) = "setoid eq".
alias symbol "eq" = "setoid eq".
+
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
inhabited: ∀i. i ∈ indexes → class i ≬ class i;
- disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i=j;
- covers: big_union support ? ? (λx.class x) = full_set A
- }. napply indexes; nqed.
-
+ disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
+ covers: big_union support ? indexes (λx.class x) = full_set A
+ }.
+
naxiom daemon: False.
nlet rec iso_nat_nat_union (s: nat → nat) m index on index : pair nat nat ≝
ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2;
ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2;
ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ?
- [##2: napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
+ [##2: alias symbol "refl" = "refl".
+alias symbol "prop1" = "prop11".
+napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
napply (ex_intro … xxx); napply conj
#A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
nqed.
-nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝
{ iso_f:> unary_morphism A B;
f_closed: ∀x. x ∈ S → iso_f x ∈ T;
f_sur: surjective … S T iso_f;
f_inj: injective … S iso_f
}.
+
+(*
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+ { iso_f:> unary_morphism A B;
+ f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}.
+
+
+ncheck (λA:?.
+ λB:?.
+ λS:?.
+ λT:?.
+ λxxx:isomorphism A B S T.
+ match xxx
+ return λxxx:isomorphism A B S T.
+ ∀x: carr A.
+ ∀x_72: mem (carr A) (pc A S) x.
+ mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x)
+ with [ mk_isomorphism _ yyy ⇒ yyy ] ).
+
+ ;
+ }.
+*)
projects / helm.git / commitdiff