sort poly (with simple squashing model and no inductive output in qsort)

checker/checker.ml

@@ -245,7 +245,7 @@ let explain_exn = function
     let msg =
       if CDebug.(get_flag misc) then
         str "." ++ spc() ++
-          UGraph.explain_universe_inconsistency Univ.Level.raw_pr i
+          UGraph.explain_universe_inconsistency Sorts.QVar.raw_pr Univ.Level.raw_pr i
       else
         mt() in
       hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
@@ -287,11 +287,13 @@ let explain_exn = function
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
+      | UnsatisfiedQConstraints _ -> str"UnsatisfiedQConstraints"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
       | BadBinderRelevance _ -> str"BadBinderRelevance"
       | BadCaseRelevance _ -> str"BadCaseRelevance"
       | BadInvert -> str"BadInvert"
+      | UndeclaredQualities _ -> str"UndeclaredQualities"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"
       | BadVariance _ -> str "BadVariance"
       ))

checker/values.ml

@@ -94,6 +94,12 @@ let v_level = v_tuple "level" [|Int;v_raw_level|]
 let v_expr = v_tuple "levelexpr" [|v_level;Int|]
 let v_univ = List v_expr
 
+let v_qvar = v_sum "qvar" 0 [|[|Int|];[|String;Int|]|]
+
+let v_constant_quality = v_enum "constant_quality" 3
+
+let v_quality = v_sum "quality" 0 [|[|v_qvar|];[|v_constant_quality|]|]
+
 let v_cstrs =
   Annot
     ("Univ.constraints",
@@ -103,16 +109,16 @@ let v_cstrs =
 
 let v_variance = v_enum "variance" 3
 
-let v_instance = Annot ("instance", Array v_level)
-let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
+let v_instance = Annot ("instance", v_pair (Array v_quality) (Array v_level))
+let v_abs_context = v_tuple "abstract_universe_context" [|v_pair (Array v_name) (Array v_name); v_cstrs|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
 
-let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|]
+let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|];[|v_qvar;v_univ(*QSort*)|]|]
 let v_sortfam = v_enum "sorts_family" 4
 
-let v_relevance = v_sum "relevance" 2 [||]
+let v_relevance = v_sum "relevance" 2 [|[|v_qvar|]|]
 let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]

dev/include_printers

@@ -14,6 +14,7 @@
 #install_printer  (* univ context *) ppaucontext;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* qvar set *) ppqvarset;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;

dev/top_printers.dbg

@@ -69,6 +69,7 @@ install_printer Top_printers.ppuni
 install_printer Top_printers.ppesorts
 install_printer Top_printers.ppqvar
 install_printer Top_printers.ppuni_level
+install_printer Top_printers.ppqvarset
 install_printer Top_printers.ppuniverse_set
 install_printer Top_printers.ppuniverse_instance
 install_printer Top_printers.ppuniverse_context

dev/top_printers.ml

@@ -260,10 +260,12 @@ let ppuni_level u = pp (Level.raw_pr u)
 let ppqvar q = pp (QVar.raw_pr q)
 let ppesorts s = pp (Sorts.debug_print (Evd.MiniEConstr.ESorts.unsafe_to_sorts s))
 
-let prlev l = UnivNames.pr_with_global_universes l
+let prlev l = UnivNames.pr_level_with_global_universes l
+let prqvar q = Sorts.QVar.raw_pr q
+let ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc QVar.raw_pr (QVar.Set.elements l) ++ str "}"))
 let ppuniverse_set l = pp (Level.Set.pr prlev l)
-let ppuniverse_instance l = pp (Instance.pr prlev l)
-let ppuniverse_context l = pp (pr_universe_context prlev l)
+let ppuniverse_instance l = pp (Instance.pr prqvar prlev l)
+let ppuniverse_context l = pp (pr_universe_context prqvar prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)
 let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)
@@ -281,14 +283,16 @@ let ppnamedcontextval e =
   pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppaucontext auctx =
-  let nas = AbstractContext.names auctx in
-  let prlev l = match Level.var_index l with
+  let qnas, unas = AbstractContext.names auctx in
+  let prgen pr var_index nas l = match var_index l with
     | Some n -> (match nas.(n) with
-        | Anonymous -> prlev l
+        | Anonymous -> pr l
         | Name id -> Id.print id)
-    | None -> prlev l
+    | None -> pr l
   in
-  pp (pr_universe_context prlev (AbstractContext.repr auctx))
+  let prqvar l = prgen prqvar Sorts.QVar.var_index qnas l in
+  let prlev l = prgen prlev Level.var_index unas l in
+  pp (pr_universe_context prqvar prlev (AbstractContext.repr auctx))
 
 
 let ppenv e = pp
@@ -375,6 +379,9 @@ let constr_display csr =
   and univ_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Universe.raw_pr u ++ fnl ())
 
+  and quality_display q =
+    incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Sorts.Quality.raw_pr q ++ fnl ())
+
   and level_display u =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.raw_pr u ++ fnl ())
 
@@ -387,8 +394,15 @@ let constr_display csr =
     | QSort (q, u) -> univ_display u; Printf.sprintf "QSort(%s, %i)" (Sorts.QVar.to_string q) !cnt
 
   and universes_display l =
+    let qs, us = Instance.to_array l in
+    let qs = Array.fold_right (fun x i ->
+        quality_display x;
+        (string_of_int !cnt)^
+        (if not(i="") then (" "^i) else ""))
+        qs ""
+    in
     Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
-        then (" "^i) else "")) (Instance.to_array l) ""
+        then (" "^i) else "")) us (if qs = "" then "" else (qs^" | "))
 
   and name_display x = match x.binder_name with
     | Name id -> "Name("^(Id.to_string id)^")"
@@ -527,7 +541,9 @@ let print_pure_constr csr =
   and box_display c = open_hovbox 1; term_display c; close_box()
 
   and universes_display u =
-    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) (Instance.to_array u)
+    let qs, us = Instance.to_array u in
+    Array.iter (fun u -> print_space (); pp (Sorts.Quality.raw_pr u)) qs;
+    Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) us
 
   and sort_display = function
     | SProp -> print_string "SProp"

dev/top_printers.mli

@@ -147,6 +147,7 @@ val ppuni_level : Univ.Level.t -> unit (* raw *)
 val ppqvar : Sorts.QVar.t -> unit
 val ppesorts : EConstr.ESorts.t -> unit
 val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
+val ppqvarset : Sorts.QVar.Set.t -> unit
 val ppuniverse_set : Univ.Level.Set.t -> unit
 val ppuniverse_instance : UVars.Instance.t -> unit
 val ppuniverse_context : UVars.UContext.t -> unit

doc/sphinx/addendum/universe-polymorphism.rst

@@ -530,14 +530,15 @@ Explicit Universes
    universe_name ::= @qualid
    | Set
    | Prop
-   univ_annot ::= @%{ {* @universe_level } %}
-   universe_level ::= Set
+   univ_annot ::= @%{ {* @univ_level_or_quality } {? %| {* @univ_level_or_quality } } %}
+   univ_level_or_quality ::= Set
+   | SProp
    | Prop
    | Type
    | _
    | @qualid
-   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
-   cumul_univ_decl ::= @%{ {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   univ_decl ::= @%{ {? {* @ident } %| } {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {? {* @ident } %| } {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
    univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 The syntax has been extended to allow users to explicitly bind names

doc/sphinx/language/core/sorts.rst

@@ -17,7 +17,7 @@ Sorts
    | SProp
    | Type
    | Type @%{ _ %}
-   | Type @%{ @universe %}
+   | Type @%{ {? @qualid %| } @universe %}
    universe ::= max ( {+, @universe_expr } )
    | @universe_expr
    universe_expr ::= @universe_name {? + @natural }

doc/tools/docgram/common.edit_mlg

@@ -163,6 +163,7 @@ DELETE: [
 | test_variance_ident
 | test_ident_with_or_lpar_or_rbrac
 | test_leftsquarebracket_equal
+| test_sort_qvar
 
 (* unused *)
 | constr_comma_sequence'
@@ -326,6 +327,12 @@ scope_delimiter: [
 | WITH "%" scope
 ]
 
+sort: [
+| REPLACE "Type" "@{" reference "|" universe "}"
+| WITH "Type" "@{" OPT [ qualid "|" ] universe "}"
+| DELETE "Type" "@{" universe "}"
+]
+
 term100: [
 | REPLACE term99 "<:" term200
 | WITH term99 "<:" type
@@ -624,13 +631,15 @@ inline: [
 ]
 
 univ_decl: [
-| REPLACE "@{" LIST0 identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
-| WITH    "@{" LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| REPLACE "@{" test_univ_decl LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
+| WITH    "@{" OPT [ LIST0 identref "|" ] LIST0 identref  OPT "+"  OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| DELETE "@{" LIST0 identref [ "+" | ] univ_decl_constraints
 ]
 
 cumul_univ_decl: [
-| REPLACE "@{" LIST0 variance_identref [ "+" | ]     [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
-| WITH "@{" LIST0 variance_identref    OPT "+"   OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| REPLACE "@{" test_cumul_univ_decl LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
+| WITH "@{" OPT [ LIST0 identref "|" ] LIST0 variance_identref    OPT "+"   OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| DELETE "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
 ]
 
 of_type: [

doc/tools/docgram/fullGrammar

@@ -27,6 +27,7 @@ sort: [
 | "SProp"
 | "Type"
 | "Type" "@{" "_" "}"
+| "Type" "@{" test_sort_qvar reference "|" universe "}"
 | "Type" "@{" universe "}"
 ]
 
@@ -182,12 +183,13 @@ evar_instance: [
 ]
 
 univ_annot: [
-| "@{" LIST0 universe_level "}"
+| "@{" LIST0 univ_level_or_quality OPT [ "|" LIST0 univ_level_or_quality ] "}"
 |
 ]
 
-universe_level: [
+univ_level_or_quality: [
 | "Set"
+| "SProp"
 | "Prop"
 | "Type"
 | "_"
@@ -862,8 +864,14 @@ univ_constraint: [
 | universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
+univ_decl_constraints: [
+| "|" LIST0 univ_constraint SEP "," [ "+" | ] "}"
+| [ "}" | bar_cbrace ]
+]
+
 univ_decl: [
-| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| "@{" test_univ_decl LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
+| "@{" LIST0 identref [ "+" | ] univ_decl_constraints
 ]
 
 variance: [
@@ -878,7 +886,8 @@ variance_identref: [
 ]
 
 cumul_univ_decl: [
-| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+| "@{" test_cumul_univ_decl LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
+| "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
 ]
 
 ident_decl: [

doc/tools/docgram/orderedGrammar

@@ -281,7 +281,7 @@ sort: [
 | "SProp"
 | "Type"
 | "Type" "@{" "_" "}"
-| "Type" "@{" universe "}"
+| "Type" "@{" OPT [ qualid "|" ] universe "}"
 ]
 
 universe: [
@@ -300,29 +300,35 @@ universe_name: [
 ]
 
 univ_annot: [
-| "@{" LIST0 universe_level "}"
+| "@{" LIST0 univ_level_or_quality OPT [ "|" LIST0 univ_level_or_quality ] "}"
 ]
 
-universe_level: [
+univ_level_or_quality: [
 | "Set"
+| "SProp"
 | "Prop"
 | "Type"
 | "_"
 | qualid
 ]
 
 univ_decl: [
-| "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| "@{" OPT [ LIST0 ident "|" ] LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
 cumul_univ_decl: [
-| "@{" LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
+| "@{" OPT [ LIST0 ident "|" ] LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}"
 ]
 
 univ_constraint: [
 | universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
+univ_decl_constraints: [
+| "|" LIST0 univ_constraint SEP "," [ "+" | ] "}"
+| [ "}" | "|}" ]
+]
+
 term_fix: [
 | "let" "fix" fix_decl "in" term
 | "fix" fix_decl OPT ( LIST1 ( "with" fix_decl ) "for" ident )