Merge pull request #406 from mattam82/8.13-beta2

8.13 beta2

Author: mattam82

.travis.yml

@@ -3,6 +3,8 @@ Changes in Equations 1.3beta2:
 
 - Fix #399: allow simplification in indices when splitting a variable, 
   to expose the head of the index.
+- Fix #389: error derving EqDec in HoTT variant.
+- Allow universe binder annotations @{} on Equations definitions.
 - Fix "struct" parsing issue that required a reset of Coq sometimes
 - Pattern enhancements: no explicit shadowing of pattern variables 
   is allowed anymore. Fix numerous bugs where generated implicit names 

CHANGES.md

@@ -72,4 +72,5 @@ theories/HoTT/Telescopes.v
 theories/HoTT/WellFoundedInstances.v
 theories/HoTT/All.v
 
-test-suite/BasicsHoTT.v
+test-suite/BasicsHoTT.v
+test-suite/issues/issue389.v

_HoTTProject

@@ -23,7 +23,7 @@ \subsection{Syntax of programs}
   \texttt{mutual programs} & mutual & \Coloneqq & \coqdockw{with}~p `| where \\
   \texttt{where clause} & where & \Coloneqq & \coqdockw{where}~p `| \coqdockw{where}~not\\
   \texttt{notation} & not & \Coloneqq & \texttt{''}string\texttt{''}~\textcoloneq~t~(\texttt{:}~scope)?\\
-  \texttt{program} & p, prog & \Coloneqq & \coqdoccst{f}~Γ~\texttt{:}~τ~(\coqdockw{by}~\textit{annot})?~\textcoloneq~clauses \\
+  \texttt{program} & p, prog & \Coloneqq & \coqdoccst{f}(\texttt{@\{} univ\_decl \texttt{\}})?~Γ~\texttt{:}~τ~(\coqdockw{by}~\textit{annot})?~\textcoloneq~clauses \\
   \texttt{annotation} & annot & \Coloneqq & \kw{struct}~\var{x}? `| \kw{wf}~t~R? \\
   \texttt{user clauses} & clauses & \Coloneqq & \vecplus{cl} `| \texttt{\{}\,\vec{cl}\,\texttt{\}} \\
   \texttt{user clause} & cl & \Coloneqq & \coqdoccst{f}~\vec{up}~n?~\texttt{;} `|
@@ -44,11 +44,11 @@ \subsection{Syntax of programs}
 \label{fig:usergram}
 \end{figure}
 The syntax allows the definition of toplevel mutual (\kw{with}) and
-nested (\kw{where}) structurally recursive definitions. Notations can be
-used globally to attach a syntax to a recursive definition, or locally
-inside a user node. A single program is given as a tuple of a (globally
-fresh) identifier, a signature and a list of user clauses (order
-matters), along with an optional recursion annotation (see next
+nested (\kw{where}) structurally recursive definitions. 
+Notations can be used globally to attach a syntax to a 
+recursive definition, or locally inside a user node. A single program is given as a tuple of a (globally
+fresh) identifier, an optional universe annotation, 
+a signature and a list of user clauses (order matters), along with an optional recursion annotation (see next
 section). The signature is simply a list of bindings and a result
 type. The expected type of the function \cst{f} is then $∀~Γ, τ$.
 An empty set of clauses denotes that one of the variables has an empty type.

doc/equations.pdf

@@ -727,7 +727,7 @@ let compute_fixdecls_data env evd ?data programs =
     List.map2 (fun i (relevance, fixprot) -> of_tuple (make_annot (Name i) relevance, None, fixprot)) names fixprots in
   data, List.rev fixdecls, fixprots
 
-let interp_arity env evd ~poly ~is_rec ~with_evars notations (((loc,i),rec_annot,l,t,by),clauses as ieqs) =
+let interp_arity env evd ~poly ~is_rec ~with_evars notations (((loc,i),udecl,rec_annot,l,t,by),clauses as ieqs) =
   let ienv, ((env', sign), impls) = Equations_common.evd_comb1 (interp_context_evars env) evd l in
   let (arity, impls') =
     let ty = match t with
@@ -1523,7 +1523,7 @@ and interp_wheres env0 ctx evars path data s lets
     (w : (pre_prototype * pre_equation list) list * Vernacexpr.decl_notation list) =
   let notations = snd w in
   let aux (data,lets,nlets,coverings,env)
-      (((loc,id),nested,b,t,reca),clauses as eqs) =
+      (((loc,id),udecl,nested,b,t,reca),clauses as eqs) =
 
     let is_rec = is_recursive id ([eqs], notations) in
     let p = interp_arity env evars ~poly:false ~is_rec ~with_evars:true notations eqs in

doc/manual.tex

@@ -112,39 +112,42 @@ let derive_eq_dec ~pm env sigma ~poly ind =
     let app = 
       let xname = Context.nameR (Id.of_string "x") in
       let yname = Context.nameR (Id.of_string "y") in
-	mkProd (xname, indapp,
-	       mkProd (yname, lift 1 indapp,
-  		      mkApp (lift 2 app, [| mkRel 2; mkRel 1 |])))
+      mkProd (xname, indapp,
+            mkProd (yname, lift 1 indapp,
+                mkApp (lift 2 app, [| mkRel 2; mkRel 1 |])))
     in
     let typ = it_mkProd_or_LetIn app ind.ind_args in
     let full = it_mkNamedProd_or_LetIn typ ctx in
     let tc gr = 
       let b, ty = 
-	Typeclasses.instance_constructor
+      	Typeclasses.instance_constructor
           cl
           [indapp; mkapp (Global.env ()) evdref (Lazy.from_val gr)
              (Array.append (vars_of_pars ctx) argsvect) ] in
       let body = 
-	it_mkNamedLambda_or_LetIn 
-	  (it_mkLambda_or_LetIn (Option.get b) ind.ind_args) ctx
+        it_mkNamedLambda_or_LetIn 
+          (it_mkLambda_or_LetIn (Option.get b) ind.ind_args) ctx
       in
+      let types = it_mkNamedProd_or_LetIn (it_mkProd_or_LetIn ty ind.ind_args) ctx in
+      let evm, _ = Typing.solve_evars (Global.env ()) !evdref (mkCast (body, Constr.DEFAULTcast, types)) in
+      let () = evdref := evm in
+      let types = to_constr !evdref types in
+      let body = to_constr !evdref body in
       let univs = Evd.univ_entry ~poly !evdref in
-      let types = to_constr !evdref (it_mkNamedProd_or_LetIn (it_mkProd_or_LetIn ty ind.ind_args) ctx) in
-      let ce = Declare.definition_entry ~univs ~types (to_constr !evdref body) in
+      let ce = Declare.definition_entry ~univs ~types body in
       ce
     in full, tc
   in
   let indsl = Array.to_list info.mutind_inds in
   let indsl = List.map (fun ind -> ind, info_of ind) indsl in
   let hook { Declare.Hook.S.dref; _ } =
     List.iter (fun (ind, (stmt, tc)) ->
-	let ce = tc dref in
-        let kind = Decls.(IsDefinition Instance) in
-        let entry = Declare.DefinitionEntry ce in
-	let inst = Declare.declare_constant ~name:(add_suffix ind.ind_name "_EqDec") ~kind entry in
-        let inst =
-          Classes.mk_instance (fst cl) Hints.empty_hint_info true (GlobRef.ConstRef inst)
-	in Classes.add_instance inst)
+      let ce = tc dref in
+      let kind = Decls.(IsDefinition Instance) in
+      let entry = Declare.DefinitionEntry ce in
+      let inst = Declare.declare_constant ~name:(add_suffix ind.ind_name "_EqDec") ~kind entry in
+      let inst = Classes.mk_instance (fst cl) Hints.empty_hint_info true (GlobRef.ConstRef inst) in
+      Classes.add_instance inst)
     indsl
   in
   let hook = Declare.Hook.make hook in

src/covering.ml

@@ -145,8 +145,14 @@ let define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof opts eqs nt =
   let env = Global.env () in
   let flags = { polymorphic = poly; with_eqns; with_ind; allow_aliases = false; 
     tactic; open_proof } in
-  let evd = ref (Evd.from_env env) in
-  let programs = List.map (fun (((loc,i),rec_annot,l,t,by),clauses as ieqs) ->
+  let evm, udecl =
+    match eqs with
+    | (((loc, i), udecl, _, _, _, _), _) :: _ ->
+      Constrintern.interp_univ_decl_opt env udecl
+    | _ -> assert false
+  in
+  let evd = ref evm in
+  let programs = List.map (fun (((loc,i),udecl,rec_annot,l,t,by),clauses as ieqs) ->
       let is_rec = is_recursive i (eqs, nt) in
       interp_arity env evd ~poly ~is_rec ~with_evars:open_proof nt ieqs) eqs in
   let rec_type = compute_rec_type [] programs in
@@ -186,7 +192,7 @@ let define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof opts eqs nt =
     else pm
   in
   let hook ~pm i p info = (), hook ~pm i p info in
-  define_programs ~pm env evd rec_type fixdecls flags programs hook
+  define_programs ~pm env evd udecl rec_type fixdecls flags programs hook
 
 let interp_tactic = function
   | Some qid -> 
@@ -201,7 +207,7 @@ let interp_tactic = function
   | None -> !Declare.Obls.default_tactic
 
 let equations ~pm ~poly ~program_mode ?tactic opts eqs nt =
-  List.iter (fun (((loc, i), nested, l, t, by),eqs) -> Dumpglob.dump_definition CAst.(make ~loc i) false "def") eqs;
+  List.iter (fun (((loc, i), _udecl, nested, l, t, by),eqs) -> Dumpglob.dump_definition CAst.(make ~loc i) false "def") eqs;
   let tactic = interp_tactic tactic in
   let pm, pstate =
     define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof:false opts eqs nt in
@@ -211,7 +217,7 @@ let equations ~pm ~poly ~program_mode ?tactic opts eqs nt =
     CErrors.anomaly Pp.(str"Equation.equations leaving a proof open")
 
 let equations_interactive ~pm ~poly ~program_mode ?tactic opts eqs nt =
-  List.iter (fun (((loc, i), nested, l, t, by),eqs) -> Dumpglob.dump_definition CAst.(make ~loc i) false "def") eqs;
+  List.iter (fun (((loc, i), _udecl, nested, l, t, by),eqs) -> Dumpglob.dump_definition CAst.(make ~loc i) false "def") eqs;
   let tactic = interp_tactic tactic in
   let pm, lemma = define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof:true opts eqs nt in
   match lemma with

src/eqdec.ml

@@ -325,8 +325,8 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   proto:
-   [ [ id = lident; l = binders2; ":"; t = Constr.lconstr;
-       reca = wf_annot; ":="; eqs = sub_equations -> { (fun r -> ((id, r, l, Some t, reca), eqs)) }
+   [ [ id = lident; d = OPT univ_decl; l = binders2; ":"; t = Constr.lconstr;
+       reca = wf_annot; ":="; eqs = sub_equations -> { (fun r -> ((id, d, r, l, Some t, reca), eqs)) }
    ] ]
   ;
 

src/equations.ml

@@ -278,7 +278,7 @@ let derive_no_confusion_hom ~pm env sigma0 ~poly (ind,u as indu) =
       ~prefix:"Hom" ~tactic:(noconf_hom_tac ()) program_cst
  in
  let prog = Splitting.make_single_program env evd data.Covering.flags p ctxmap splitting None in
- Splitting.define_programs ~pm env evd [None] [] data.Covering.flags [prog] hook
+ Splitting.define_programs ~pm env evd UState.default_univ_decl [None] [] data.Covering.flags [prog] hook
 
 let () =
   let derive_no_confusion_hom ~pm env sigma ~poly v =