Introducing rebindable toplevel definitions.

9 files changed, 144 insertions, 26 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 6822b8e7ba..ae7e255896 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -70,6 +70,7 @@ let tac2def_val = Gram.entry_create "tactic:tac2def_val"
 let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
 let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
 let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
+let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
 (** FUCK YOU API *)
@@ -90,7 +91,8 @@ let pattern_of_qualid loc id =
       CErrors.user_err ~loc (Pp.str "Syntax error")
 
 GEXTEND Gram
-  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
+  GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
+          tac2def_mut;
   tac2pat:
     [ "1" LEFTA
       [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" ->
@@ -158,6 +160,10 @@ GEXTEND Gram
     [ [ IDENT "rec" -> true
       | -> false ] ]
   ;
+  mut_flag:
+    [ [ IDENT "mutable" -> true
+      | -> false ] ]
+  ;
   typ_param:
     [ [ "'"; id = Prim.ident -> id ] ]
   ;
@@ -228,10 +234,13 @@ GEXTEND Gram
     ] ]
   ;
   tac2def_val:
-    [ [ isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
-        StrVal (isrec, l)
+    [ [ mut = mut_flag; isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
+        StrVal (mut, isrec, l)
     ] ]
   ;
+  tac2def_mut:
+    [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> StrMut (qid, e) ] ]
+  ;
   tac2typ_knd:
     [ [ t = tac2type -> CTydDef (Some t)
       | "["; ".."; "]" -> CTydOpn
@@ -253,7 +262,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   tac2rec_field:
-    [ [ mut = [ -> false | IDENT "mutable" -> true]; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
+    [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
   ;
   tac2rec_fieldexprs:
     [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l
@@ -653,11 +662,12 @@ PRINTED BY pr_ltac2entry
 | [ tac2def_typ(t) ] -> [ t ]
 | [ tac2def_ext(e) ] -> [ e ]
 | [ tac2def_syn(e) ] -> [ e ]
+| [ tac2def_mut(e) ] -> [ e ]
 END
 
 let classify_ltac2 = function
 | StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
-| StrVal _ | StrPrm _  | StrTyp _ -> Vernac_classifier.classify_as_sideeff
+| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernac_classifier.classify_as_sideeff
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
 | [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 91c8d10e2d..da7c07c134 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -42,20 +42,31 @@ end
 
 type tacdef = {
   tacdef_local : bool;
+  tacdef_mutable : bool;
   tacdef_expr : glb_tacexpr;
   tacdef_type : type_scheme;
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
   let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in
-  Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
+  let data = {
+    Tac2env.gdata_expr = def.tacdef_expr;
+    gdata_type = def.tacdef_type;
+    gdata_mutable = def.tacdef_mutable;
+  } in
+  Tac2env.define_global kn data
 
 let load_tacdef i obj = perform_tacdef (Until i) obj
 let open_tacdef i obj = perform_tacdef (Exactly i) obj
 
 let cache_tacdef ((sp, kn), def) =
   let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in
-  Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type)
+  let data = {
+    Tac2env.gdata_expr = def.tacdef_expr;
+    gdata_type = def.tacdef_type;
+    gdata_mutable = def.tacdef_mutable;
+  } in
+  Tac2env.define_global kn data
 
 let subst_tacdef (subst, def) =
   let expr' = subst_expr subst def.tacdef_expr in
@@ -296,7 +307,7 @@ let inline_rec_tactic tactics =
   in
   List.map map tactics
 
-let register_ltac ?(local = false) isrec tactics =
+let register_ltac ?(local = false) ?(mut = false) isrec tactics =
   let map ((loc, na), e) =
     let id = match na with
     | Anonymous ->
@@ -329,6 +340,7 @@ let register_ltac ?(local = false) isrec tactics =
   let iter (id, e, t) =
     let def = {
       tacdef_local = local;
+      tacdef_mutable = mut;
       tacdef_expr = e;
       tacdef_type = t;
     } in
@@ -423,6 +435,7 @@ let register_primitive ?(local = false) (loc, id) t ml =
   let e = GTacFun (bnd, GTacPrm (ml, arg)) in
   let def = {
     tacdef_local = local;
+    tacdef_mutable = false;
     tacdef_expr = e;
     tacdef_type = t;
   } in
@@ -659,13 +672,72 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
   } in
   Lib.add_anonymous_leaf (inTac2Notation ext)
 
+type redefinition = {
+  redef_kn : ltac_constant;
+  redef_body : glb_tacexpr;
+}
+
+let perform_redefinition (_, redef) =
+  let kn = redef.redef_kn in
+  let data, _ = Tac2env.interp_global kn in
+  let data = { data with Tac2env.gdata_expr = redef.redef_body } in
+  Tac2env.define_global kn data
+
+let subst_redefinition (subst, redef) =
+  let kn = Mod_subst.subst_kn subst redef.redef_kn in
+  let body = Tac2intern.subst_expr subst redef.redef_body in
+  if kn == redef.redef_kn && body == redef.redef_body then redef
+  else { redef_kn = kn; redef_body = body }
+
+let classify_redefinition o = Substitute o
+
+let inTac2Redefinition : redefinition -> obj =
+  declare_object {(default_object "TAC2-REDEFINITION") with
+     cache_function  = perform_redefinition;
+     open_function   = (fun _ -> perform_redefinition);
+     subst_function = subst_redefinition;
+     classify_function = classify_redefinition }
+
+let register_redefinition ?(local = false) (loc, qid) e =
+  let kn =
+    try Tac2env.locate_ltac qid
+    with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid)
+  in
+  let kn = match kn with
+  | TacConstant kn -> kn
+  | TacAlias _ ->
+    user_err ?loc (str "Cannot redefine syntactic abbreviations")
+  in
+  let (data, _) = Tac2env.interp_global kn in
+  let () =
+    if not (data.Tac2env.gdata_mutable) then
+      user_err ?loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable")
+  in
+  let (e, t) = intern e in
+  let () =
+    if not (is_value e) then
+      user_err ?loc (str "Tactic definition must be a syntactical value")
+  in
+  let () =
+    if not (Tac2intern.check_subtype t data.Tac2env.gdata_type) then
+      let name = int_name () in
+      user_err ?loc (str "Type " ++ pr_glbtype name (snd t) ++
+        str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type))
+  in
+  let def = {
+    redef_kn = kn;
+    redef_body = e;
+  } in
+  Lib.add_anonymous_leaf (inTac2Redefinition def)
+
 (** Toplevel entries *)
 
 let register_struct ?local str = match str with
-| StrVal (isrec, e) -> register_ltac ?local isrec e
+| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
+| StrMut (qid, e) -> register_redefinition ?local qid e
 
 (** Printing *)
 
@@ -685,7 +757,9 @@ let print_ltac ref =
     in
     match kn with
     | TacConstant kn ->
-      let (e, _, (_, t)) = Tac2env.interp_global kn in
+      let data, _ = Tac2env.interp_global kn in
+      let e = data.Tac2env.gdata_expr in
+      let (_, t) = data.Tac2env.gdata_type in
       let name = int_name () in
       Feedback.msg_notice (
         hov 0 (
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 2c5862b149..acb99a34b1 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -13,7 +13,7 @@ open Tac2expr
 
 (** {5 Toplevel definitions} *)
 
-val register_ltac : ?local:bool -> rec_flag ->
+val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
   (Name.t located * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 65276ec57f..59344e336b 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -12,6 +12,12 @@ open Names
 open Libnames
 open Tac2expr
 
+type global_data = {
+  gdata_expr : glb_tacexpr;
+  gdata_type : type_scheme;
+  gdata_mutable : bool;
+}
+
 type constructor_data = {
   cdata_prms : int;
   cdata_type : type_constant;
@@ -28,7 +34,7 @@ type projection_data = {
 }
 
 type ltac_state = {
-  ltac_tactics : (glb_tacexpr * type_scheme) KNmap.t;
+  ltac_tactics : global_data KNmap.t;
   ltac_constructors : constructor_data KNmap.t;
   ltac_projections : projection_data KNmap.t;
   ltac_types : glb_quant_typedef KNmap.t;
@@ -49,7 +55,7 @@ let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
 let rec eval_pure = function
 | GTacAtm (AtmInt n) -> ValInt n
 | GTacRef kn ->
-  let (e, _) =
+  let { gdata_expr = e } =
     try KNmap.find kn ltac_state.contents.ltac_tactics
     with Not_found -> assert false
   in
@@ -68,8 +74,8 @@ let define_global kn e =
   ltac_state := { state with ltac_tactics = KNmap.add kn e state.ltac_tactics }
 
 let interp_global kn =
-  let (e, t) = KNmap.find kn ltac_state.contents.ltac_tactics in
-  (e, eval_pure e, t)
+  let data = KNmap.find kn ltac_state.contents.ltac_tactics in
+  (data, eval_pure data.gdata_expr)
 
 let define_constructor kn t =
   let state = !ltac_state in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 20bf24d19d..8a5fb531d8 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -16,8 +16,14 @@ open Tac2expr
 
 (** {5 Toplevel definition of values} *)
 
-val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
-val interp_global : ltac_constant -> (glb_tacexpr * valexpr * type_scheme)
+type global_data = {
+  gdata_expr : glb_tacexpr;
+  gdata_type : type_scheme;
+  gdata_mutable : bool;
+}
+
+val define_global : ltac_constant -> global_data -> unit
+val interp_global : ltac_constant -> global_data * valexpr
 
 (** {5 Toplevel definition of types} *)
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 281ed6c81e..78611d51ca 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -154,7 +154,7 @@ type sexpr =
 (** {5 Toplevel statements} *)
 
 type strexpr =
-| StrVal of rec_flag * (Name.t located * raw_tacexpr) list
+| StrVal of mutable_flag * rec_flag * (Name.t located * raw_tacexpr) list
   (** Term definition *)
 | StrTyp of rec_flag * (qualid located * redef_flag * raw_quant_typedef) list
   (** Type definition *)
@@ -162,7 +162,8 @@ type strexpr =
   (** External definition *)
 | StrSyn of sexpr list * int option * raw_tacexpr
   (** Syntactic extensions *)
-
+| StrMut of qualid located * raw_tacexpr
+  (** Redefinition of mutable globals *)
 
 (** {5 Dynamic semantics} *)
 
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 765be92103..ef0763ff8e 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -360,20 +360,20 @@ let eq_or_tuple eq t1 t2 = match t1, t2 with
 | Other o1, Other o2 -> eq o1 o2
 | _ -> false
 
-let rec unify env t1 t2 = match kind env t1, kind env t2 with
+let rec unify0 env t1 t2 = match kind env t1, kind env t2 with
 | GTypVar id, t | t, GTypVar id ->
   unify_var env id t
 | GTypArrow (t1, u1), GTypArrow (t2, u2) ->
-  let () = unify env t1 t2 in
-  unify env u1 u2
+  let () = unify0 env t1 t2 in
+  unify0 env u1 u2
 | GTypRef (kn1, tl1), GTypRef (kn2, tl2) ->
   if eq_or_tuple KerName.equal kn1 kn2 then
-    List.iter2 (fun t1 t2 -> unify env t1 t2) tl1 tl2
+    List.iter2 (fun t1 t2 -> unify0 env t1 t2) tl1 tl2
   else raise (CannotUnify (t1, t2))
 | _ -> raise (CannotUnify (t1, t2))
 
 let unify ?loc env t1 t2 =
-  try unify env t1 t2
+  try unify0 env t1 t2
   with CannotUnify (u1, u2) ->
     user_err ?loc (str "This expression has type " ++ pr_glbtype env t1 ++
       str " but an expression was expected of type " ++ pr_glbtype env t2)
@@ -663,7 +663,7 @@ let rec intern_rec env = function
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
-    let (_, _, sch) = Tac2env.interp_global kn in
+    let { Tac2env.gdata_type = sch }, _ = Tac2env.interp_global kn in
     (GTacRef kn, fresh_type_scheme env sch)
   | ArgArg (TacAlias kn) ->
     let e = Tac2env.interp_alias kn in
@@ -1162,6 +1162,23 @@ let intern_open_type t =
   let t = normalize env (count, vars) t in
   (!count, t)
 
+(** Subtyping *)
+
+let check_subtype t1 t2 =
+  let env = empty_env () in
+  let t1 = fresh_type_scheme env t1 in
+  (** We build a substitution mimicking rigid variable by using dummy refs *)
+  let mb = MBId.make DirPath.empty (Id.of_string "_t") in
+  let rigid i =
+    let kn = KerName.make (MPbound mb) DirPath.empty (Label.make "_t") in
+    GTypRef (Other kn, [])
+  in
+  let (n, t2) = t2 in
+  let subst = Array.init n rigid in
+  let substf i = subst.(i) in
+  let t2 = subst_type substf t2 in
+  try unify0 env t1 t2; true with CannotUnify _ -> false
+
 (** Globalization *)
 
 let get_projection0 var = match var with
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
index 898df649ba..dac074a0eb 100644
--- a/src/tac2intern.mli
+++ b/src/tac2intern.mli
@@ -22,6 +22,10 @@ val intern_open_type : raw_typexpr -> type_scheme
 val is_value : glb_tacexpr -> bool
 val check_unit : ?loc:Loc.t -> type_scheme -> unit
 
+val check_subtype : type_scheme -> type_scheme -> bool
+(** [check_subtype t1 t2] returns [true] iff all values of intances of type [t1]
+    also have type [t2]. *)
+
 val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr
 val subst_expr : substitution -> glb_tacexpr -> glb_tacexpr
 val subst_quant_typedef : substitution -> glb_quant_typedef -> glb_quant_typedef
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index d3bc79957b..3e1a048d29 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -38,7 +38,7 @@ let get_var ist id =
     anomaly (str "Unbound variable " ++ Id.print id)
 
 let get_ref ist kn =
-  try pi2 (Tac2env.interp_global kn) with Not_found ->
+  try snd (Tac2env.interp_global kn) with Not_found ->
     anomaly (str "Unbound reference" ++ KerName.print kn)
 
 let return = Proofview.tclUNIT