Merge remote-tracking branch 'origin/develop' into probability_dev

src/datatype/Datatype.sig

@@ -34,6 +34,7 @@ sig
  (* into their tyinfo to do inequality resolution.                            *)
  (*---------------------------------------------------------------------------*)
 
+ val typecheck_listener : (string Symtab.table -> ParseDatatype.pretype -> hol_type -> unit) ref
  val build_tyinfos : typeBase
                          -> {induction:thm, recursion:thm}
                            -> tyinfo list

src/datatype/Datatype.sml

@@ -179,6 +179,8 @@ fun ast_tyvar_strings (dAQ ty) = map dest_vartype $ type_vars ty
   | ast_tyvar_strings (dTyop {Args, ...}) =
       List.concat (map ast_tyvar_strings Args)
 
+val typecheck_listener = ref (fn _: string Symtab.table => fn _: pretype => fn _:hol_type => ())
+
 local
   fun strvariant avoids s = if mem s avoids then strvariant avoids (s ^ "a")
                             else s
@@ -221,6 +223,7 @@ fun to_tyspecs ASTs =
                                        Args = map (mk_hol_ty d) Args}
      fun mk_hol_type d pty = let
        val ty = mk_hol_ty d pty
+       val _ = !typecheck_listener d pty ty
      in
        if Theory.uptodate_type ty then ty
        else let val tyname = #1 (dest_type ty)

src/parse/Absyn.sml

@@ -94,9 +94,9 @@ end;
 val nolocn = locn.Loc_None  (* i.e., compiler-generated text *)
 fun mk_AQ x        = AQ   (nolocn,x)
 fun mk_ident s     = IDENT(nolocn,s)
-fun mk_app (M,N)   = APP  (nolocn,M,N)
-fun mk_lam (v,M)   = LAM  (nolocn,v,M)
-fun mk_typed(M,ty) = TYPED(nolocn,M,ty);
+fun mk_app (M,N)   = APP  (locn.between (locn_of_absyn M) (locn_of_absyn N),M,N)
+fun mk_lam (v,M)   = LAM  (locn.between (locn_of_vstruct v) (locn_of_absyn M),v,M)
+fun mk_typed(M,ty) = TYPED(locn.near (locn_of_absyn M),M,ty);
 
 fun binAQ f x locn err = let val (t1,t2) = f x
                          in
@@ -121,13 +121,13 @@ fun dest_AQ (AQ (_,x)) = x
 fun dest_typed (TYPED (_,M,ty)) = (M,ty)
   | dest_typed  t = raise ERRloc "dest_typed" (locn_of_absyn t) "Expected a typed thing";
 
-fun tuple_to_vstruct tm =
+fun tuple_to_vstruct locn tm =
   if Term.is_var tm
-  then VIDENT(nolocn,fst(Term.dest_var tm))
+  then VIDENT(locn,fst(Term.dest_var tm))
   else let val (M,N) = dest_comb tm
            val (M1,M2) = dest_comb M
        in if fst(Term.dest_const M1) = ","
-            then VPAIR(nolocn,tuple_to_vstruct M2,tuple_to_vstruct N)
+            then VPAIR(locn,tuple_to_vstruct locn M2,tuple_to_vstruct locn N)
             else raise ERR "tuple_to_vstruct" ""
        end;
 
@@ -139,7 +139,7 @@ fun dest_lam (LAM (_,v,M)) = (v,M)
            in (VIDENT (locn,id), AQ (locn,Body))
            end
       else let val (vstr,body) = dest_pabs x
-           in (tuple_to_vstruct vstr, AQ (locn,body))
+           in (tuple_to_vstruct locn vstr, AQ (locn,body))
            end
   | dest_lam t = raise ERRloc "dest_lam" (locn_of_absyn t) "Expected an abstraction"
 
@@ -214,17 +214,17 @@ val list_mk_exists1 = list_mk_binder mk_exists1
 val list_mk_select  = list_mk_binder mk_select;
 
 local fun err0 str locn = ERRloc "dest_binder" locn ("Expected a "^Lib.quote str)
-      fun dest_term_binder s tm ex =
+      fun dest_term_binder s locn tm ex =
        let val (c,lam) = dest_comb tm
        in if fst(Term.dest_const c) <> s
             then raise ex
-            else dest_lam (AQ (nolocn,lam))
+            else dest_lam (AQ (locn, lam))
        end handle HOL_ERR _ => raise ex
 in
 fun dest_binder str =
  let fun err locn = err0 str locn
      fun dest (APP(_,IDENT (locn,s),M)) = if s=str then dest_lam M else raise err locn
-       | dest (AQ (locn,x)) = dest_term_binder str x (err locn)
+       | dest (AQ (locn,x)) = dest_term_binder str locn x (err locn)
        | dest  t = raise err (locn_of_absyn t)
  in dest end
 end;

src/parse/ParseDatatype.sig

@@ -41,4 +41,6 @@ val hparse : type_grammar.grammar -> Type.hol_type Portable.quotation ->
   or a type-constant of arity 0, or one of the types being defined.
 *)
 
+val parse_listener : (AST list -> unit) ref
+
 end

src/parse/ParseDatatype.sml

@@ -350,11 +350,13 @@ end
 fun hide_tynames q G0 =
   List.foldl (uncurry type_grammar.hide_tyop) G0 (extract_tynames q)
 
+val parse_listener = ref (fn _: (string * datatypeForm) list => ())
 
 fun core_parse G0 phrase_p q = let
   val G = hide_tynames q G0
   val qb = qbuf.new_buffer q
   val result = termsepby1 ";" base_tokens.BT_EOI (parse_g G phrase_p) qb
+  val _ = !parse_listener result
 in
   case qbuf.current qb of
       (base_tokens.BT_EOI,_) => result

src/parse/Pretype.sig

@@ -34,6 +34,7 @@ val fromType : Type.hol_type -> pretype
 val remove_made_links : pretype -> pretype in_env
 val replace_null_links :
     pretype -> (Env.t * string list, pretype, error) errormonad.t
+val typecheck_listener : (pretype -> Env.t -> unit) ref
 val clean : pretype -> Type.hol_type
 val toTypeM : pretype -> Type.hol_type in_env
 val toType : pretype -> Type.hol_type

src/parse/Pretype.sml

@@ -184,10 +184,15 @@ fun clean ty =
       Type.mk_thy_type{Tyop = s, Thy = Thy, Args = map clean Args}
   | _ => raise Fail "Don't expect to see links remaining at this stage"
 
+val typecheck_listener = ref (fn _:pretype => fn _:Env.t => ());
+
 fun toTypeM ty : Type.hol_type in_env =
   remove_made_links ty >-
   (fn ty => tyvars ty >-
-  (fn vs => lift (clean o #2) (addState vs (replace_null_links ty))))
+  (fn vs => addState vs (replace_null_links ty) >-
+  (fn (_, pty) => fn e => (
+    !typecheck_listener pty e;
+    return (clean pty) e))))
 
 fun toType pty =
   case toTypeM pty Env.empty of

src/tfl/src/Defn.sml

@@ -1778,8 +1778,9 @@ fun defn_absyn_to_term a = let
     in
       overloading_resolution ptm >- (fn (pt,b) =>
       report_ovl_ambiguity b     >>
-      to_term pt                 >- (fn t =>
-      return (t |> remove_case_magic |> !post_process_term)))
+      to_term pt                 >- (fn t => fn e => (
+      !Preterm.typecheck_listener pt e;
+      return (t |> remove_case_magic |> !post_process_term) e)))
     end
   val M =
     ptsM >-