From 8b1a49bbee9eea86eb74c040defe701370ca5893 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 21 Sep 2009 10:01:28 +0000 Subject: [PATCH] huge commit regarding universes: - only Type[foo] can be declare with a strict (<) constraint among other Type[bar] - CProp[foo] is automatically available for Type[foo] - The CProp hierarchy can be collapsed (hopefully in a consistent way) to both Prop OR Type: - You cannot eliminate CProp to build a Type like for Prop/Type - You cannot eliminate Prop to build a CProp, like for Prop/Type - Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >= of CProp[i] to allow collapsing them (while < whould be violated). New function to delift a type w.r.t. a term list, to potentially build a dependent type, used in lambda_intro and Letin expected type propagation. --- .../content_pres/cicNotationParser.ml | 4 +- .../software/components/grafite/grafiteAst.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 50 ++--- .../grafite_parser/grafiteParser.ml | 23 +-- .../ng_disambiguation/nCicDisambiguate.ml | 15 +- helm/software/components/ng_kernel/check.ml | 19 +- helm/software/components/ng_kernel/nCic.ml | 4 +- .../components/ng_kernel/nCic2OCic.ml | 2 +- .../components/ng_kernel/nCicEnvironment.ml | 172 +++++++++++++----- .../components/ng_kernel/nCicEnvironment.mli | 54 ++++-- .../components/ng_kernel/nCicLibrary.ml | 8 +- .../components/ng_kernel/nCicLibrary.mli | 2 +- helm/software/components/ng_kernel/nCicPp.ml | 11 +- .../components/ng_kernel/nCicReduction.ml | 8 +- .../components/ng_kernel/nCicTypeChecker.ml | 30 ++- .../components/ng_kernel/oCic2NCic.ml | 6 +- .../components/ng_paramodulation/paramod.ml | 2 +- .../components/ng_refiner/.depend.opt | 6 +- helm/software/components/ng_refiner/check.ml | 19 +- .../components/ng_refiner/nCicRefiner.ml | 13 +- .../components/ng_refiner/nCicUnification.ml | 34 ++-- .../components/ng_refiner/nCicUnification.mli | 2 +- helm/software/components/ng_tactics/.depend | 6 +- .../components/ng_tactics/.depend.opt | 6 +- helm/software/components/ng_tactics/Makefile | 4 +- .../components/ng_tactics/nCicElim.ml | 29 +-- .../components/ng_tactics/nCicElim.mli | 2 + .../components/ng_tactics/nTacStatus.ml | 2 +- .../components/ng_tactics/nTactics.ml | 48 ++--- .../contribs/formal_topology/overlap/depends | 16 +- .../matita/nlibrary/logic/connectives.ma | 16 +- helm/software/matita/nlibrary/logic/pts.ma | 13 +- .../matita/nlibrary/sets/partitions.ma | 17 +- helm/software/matita/nlibrary/sets/sets.ma | 24 ++- 34 files changed, 374 insertions(+), 295 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 1a664d525..829e78b6d 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -581,9 +581,9 @@ EXTEND 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 ()) ] ]; diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 5c8f461c1..68350ac75 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -219,7 +219,7 @@ type ('term,'obj) command = 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 * diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ec9f3866f..482a138a6 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -501,25 +501,25 @@ let eval_unification_hint status t n = 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 [] ;; @@ -774,9 +774,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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 = @@ -791,17 +791,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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 @@ -857,8 +861,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = [] -> 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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index c9ece6dba..bf34fc283 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -817,26 +817,15 @@ EXTEND in G.NObj (loc, N.Inductive (params, ind_types)) | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; - strict = [ SYMBOL <:unicode> -> true - | SYMBOL <:unicode> -> false ]; - u2 = tactic_term -> - let u1 = - match u1 with + SYMBOL <:unicode> ; 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; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4bfeab669..6bf1c05ba 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -64,7 +64,7 @@ let refine_term ;; let refine_obj - ~rdb metasenv subst context _uri + ~rdb metasenv subst _context _uri ~use_coercions obj _ _ugraph ~localization_tbl = assert (metasenv=[]); @@ -72,7 +72,6 @@ let refine_obj 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 @@ -322,7 +321,7 @@ let interpretate_term_and_interpretate_term_option 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 @@ -344,15 +343,15 @@ let interpretate_term_and_interpretate_term_option 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 []) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index f5fb6841c..8f014d4d2 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -53,15 +53,15 @@ let logger = 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")] ;; @@ -151,16 +151,9 @@ let _ = 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 diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index e52042216..c531d1c2b 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -13,7 +13,9 @@ (********************************* 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 *) diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 5f8279d7e..1006d03c6 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -15,7 +15,7 @@ let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);; 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 diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index b3b1eda16..893e514b1 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -29,91 +29,177 @@ let set_get_obj f = get_obj := f;; 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 = @@ -144,10 +230,10 @@ let invalidate_item item = 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 ;; diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 778931706..35b97aa59 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -14,7 +14,6 @@ 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 @@ -25,21 +24,6 @@ val check_and_add_obj: 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 @@ -56,10 +40,46 @@ val get_checked_fixes_or_cofixes: (* 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 *) diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 9a2842e0e..e7d7c3b11 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -74,7 +74,7 @@ let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; 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 @@ -310,9 +310,9 @@ let add_obj status ((u,_,_,_,_) as obj) = 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) ;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index d89db9d71..6dc7dde43 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -30,7 +30,7 @@ class status : (* 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) *) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 2f4b694de..12227b4b1 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -173,16 +173,7 @@ let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = (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 ;; diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 432ea9a45..a88a1aaf3 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -213,12 +213,8 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 = 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 && diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 6dbaf3e5d..0b4b95eba 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -395,16 +395,11 @@ let rec typeof ~subst ~metasenv context term = 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 = @@ -664,9 +659,10 @@ and check_allowed_sort_elimination ~subst ~metasenv r = (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 @@ -684,8 +680,8 @@ and check_allowed_sort_elimination ~subst ~metasenv r = is_non_informative ~metasenv ~subst leftno constrty)) then raise (TypeCheckerFailure (lazy - ("Sort elimination not allowed"))); - | _,_ -> ()) + ("Sort elimination not allowed")))) + | _ -> ()) | _,_ -> () in aux @@ -742,7 +738,9 @@ and is_non_informative ~metasenv ~subst paramsno c = 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 diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 225269b70..7bfb6c39c 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -16,14 +16,14 @@ module Ref = NReference 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 = diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index d98aa8b18..0dbd6260a 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -350,7 +350,7 @@ module Paramod (B : Orderings.Blob) = struct ;; 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 diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index dc9a46fb3..35146bcc8 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -2,7 +2,7 @@ nDiscriminationTree.cmi: 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 @@ -15,8 +15,8 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.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 \ diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index f544d8dae..4cb188170 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -53,15 +53,15 @@ let logger = 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")] ;; @@ -151,16 +151,9 @@ let _ = 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 diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 8dc94e9e4..a1ce81470 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -145,11 +145,12 @@ let rec typeof rdb 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 @@ -238,7 +239,7 @@ let rec typeof rdb | 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 diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 2f6332d51..dff242970 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -98,11 +98,13 @@ let pp s = 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 @@ -153,7 +155,8 @@ let rec lambda_intros rdb metasenv subst context t args = 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 @@ -163,7 +166,8 @@ let rec lambda_intros rdb metasenv subst context t args = 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 = @@ -181,8 +185,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = (* 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 = @@ -194,8 +198,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = 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) @@ -251,7 +255,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = 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 @@ -276,7 +280,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = 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 @@ -661,9 +665,9 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); | 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) @@ -681,4 +685,4 @@ let unify rdb ?(test_eq_only=false) = 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"));; diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 944b4c187..c442306d7 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -32,7 +32,7 @@ val unify : (* 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 -> diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 636e38f58..7c97b8cfa 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,12 +1,12 @@ 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 diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index 636e38f58..7c97b8cfa 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,12 +1,12 @@ 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 diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index 139f27288..e5a613439 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -3,8 +3,8 @@ PACKAGE = ng_tactics INTERFACE_FILES = \ nCicTacReduction.mli \ nTacStatus.mli \ - nTactics.mli \ - nCicElim.mli + nCicElim.mli \ + nTactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index d5cbca892..4117c4ffa 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -154,19 +154,24 @@ let mk_elim uri leftno it (outsort,suffix) = ;; 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) = diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli index e8b4c7a8d..bbb96facb 100644 --- a/helm/software/components/ng_tactics/nCicElim.mli +++ b/helm/software/components/ng_tactics/nCicElim.mli @@ -13,3 +13,5 @@ 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 diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 25beed259..0bb0d846e 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -14,7 +14,7 @@ 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 _ diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0ba8e4b44..01a57f0c4 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -477,33 +477,31 @@ let analyze_indty_tac ~what indtyref = 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 @@ -512,23 +510,11 @@ let elim_tac ~what:(txt,len,what) ~where = 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 diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index c6d981528..b67a2e7c1 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,26 +1,26 @@ -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 diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma index a149bc9dd..34661dc80 100644 --- a/helm/software/matita/nlibrary/logic/connectives.ma +++ b/helm/software/matita/nlibrary/logic/connectives.ma @@ -14,38 +14,38 @@ 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 }. diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma index d895b59e7..e4f0815ff 100644 --- a/helm/software/matita/nlibrary/logic/pts.ma +++ b/helm/software/matita/nlibrary/logic/pts.ma @@ -12,17 +12,6 @@ (* *) (**************************************************************************) -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 + diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 7affc517f..61173c78e 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -18,24 +18,21 @@ include "nat/compare.ma". 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 ≝ @@ -153,7 +150,9 @@ nlemma partition_splits_card: 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 diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index c8a19354c..4e7418fd9 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -228,9 +228,31 @@ nlemma first_omomorphism_theorem_functions3: #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 ] ). + + ; + }. +*) -- 2.39.2