# HG changeset patch # User wenzelm # Date 749745391 -3600 # Node ID 929ad32d63fcb337eac387386eb27fadf76f71b6 # Parent c9ec452ff08f5afc6215db388288bceb4be2d5f8 Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs; diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/NJ.ML --- a/src/Pure/NJ.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/NJ.ML Mon Oct 04 15:36:31 1993 +0100 @@ -28,7 +28,8 @@ fun pp pps obj = pprint obj (add_string pps, begin_block pps INCONSISTENT, - fn wd => add_break pps (wd, 0), fn () => end_block pps); + fn wd => add_break pps (wd, 0), fn () => add_newline pps, + fn () => end_block pps); in (path, pp) end; diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/POLY.ML --- a/src/Pure/POLY.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/POLY.ML Mon Oct 04 15:36:31 1993 +0100 @@ -32,7 +32,8 @@ (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) fun make_pp _ pprint (str, blk, brk, en) obj = - pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), en); + pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), + fn () => brk (99999, 0), en); (*** File information ***) diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/README --- a/src/Pure/README Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/README Mon Oct 04 15:36:31 1993 +0100 @@ -1,15 +1,18 @@ - Pure: The Pure Isabelle System + Pure: The Pure Isabelle System This directory contains the ML source files for Pure Isabelle, which is the -basis for all object-logics. Important files include +basis for all object-logics. Important files include: Makefile -- compiles the files under Poly/ML or SML of New Jersey -Syntax -- subdirectory containing the parser/prettyprinter generator +Syntax/ -- subdirectory containing the syntax module -ROOT.ML -- loads all source files. Enter ML and type: use "ROOT.ML"; +Thy/ -- subdirectory containing the thy file parser and loader + +ROOT.ML -- loads all source files. Enter ML and type: use "ROOT.ML"; -NJ.ML -- compatibility file for Standard ML of New Jersey. You may wish to - alter the parameter settings. +NJ.ML -- compatibility file for Standard ML of New Jersey. You may wish to + alter the parameter settings. -POLY.ML -- compatibility file for Poly/ML +POLY.ML -- compatibility file for Poly/ML + diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/ROOT.ML Mon Oct 04 15:36:31 1993 +0100 @@ -1,16 +1,14 @@ -(* Title: ROOT +(* Title: Pure/ROOT.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Root file for pure Isabelle: all modules in proper order for loading -Loads pure Isabelle into an empty database. +Root file for Pure Isabelle: all modules in proper order for loading. +Loads pure Isabelle into an empty database (see also Makefile). -To build system, use Makefile (Poly/ML) or Makefile.NJ (New Jersey ML) - -TO DO: +TO DO: instantiation of theorems can lead to inconsistent sorting of type vars if -'a::S is already present and 'a::T is introduced. +'a::S is already present and 'a::T is introduced. *) val banner = "Pure Isabelle"; @@ -22,13 +20,18 @@ use "term.ML"; use "symtab.ML"; -(*Used for building the parser generator*) structure Symtab = SymtabFun(); + +(*Syntax module*) cd "Syntax"; use "ROOT.ML"; cd ".."; -print_depth 1; +(*Theory parser*) +cd "Thy"; +use "ROOT.ML"; +cd ".."; + use "type.ML"; use "sign.ML"; use "sequence.ML"; @@ -50,23 +53,20 @@ structure Envir = EnvirFun(); structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir); structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir - and Sequence=Sequence and Pattern=Pattern); + and Sequence=Sequence and Pattern=Pattern); structure Net = NetFun(); structure Logic = LogicFun(structure Unify=Unify and Net=Net); structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net - and Pattern=Pattern); + and Pattern=Pattern); structure Drule = DruleFun(structure Logic=Logic and Thm=Thm); structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule); -structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule - and Tactical=Tactical and Net=Net); +structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule + and Tactical=Tactical and Net=Net); structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule - and Tactic=Tactic and Pattern=Pattern); -open Basic_Syntax Thm Drule Tactical Tactic Goals; + and Tactic=Tactic and Pattern=Pattern); +open BasicSyntax Thm Drule Tactical Tactic Goals; structure Pure = struct val thy = pure_thy end; -(* Theory parser *) -cd "Thy"; -use "ROOT.ML"; -cd ".."; +use "install_pp.ML"; diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/install_pp.ML --- a/src/Pure/install_pp.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/install_pp.ML Mon Oct 04 15:36:31 1993 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/install_pp +(* Title: Pure/install_pp.ML ID: $Id$ Set up automatic toplevel printing @@ -11,5 +11,5 @@ install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm); install_pp (make_pp ["typ"] pprint_typ); install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp); -install_pp (make_pp ["Ast", "ast"] Syntax.pprint_ast); +install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); diff -r c9ec452ff08f -r 929ad32d63fc src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Oct 04 15:30:49 1993 +0100 +++ b/src/Pure/sign.ML Mon Oct 04 15:36:31 1993 +0100 @@ -1,13 +1,13 @@ -(* Title: sign +(* Title: Pure/sign.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge the abstract types "sg" (signatures) and "cterm" (certified terms under a signature) *) -signature SIGN = +signature SIGN = sig structure Type: TYPE structure Symtab: SYMTAB @@ -20,25 +20,25 @@ val cterm_of: sg -> term -> cterm val ctyp_of: sg -> typ -> ctyp val extend: sg -> string -> - (class * class list) list * class list * - (string list * int) list * - (string list * (sort list * class)) list * - (string list * string)list * Syntax.sext option -> sg + (class * class list) list * class list * + (string list * int) list * + (string list * (sort list * class)) list * + (string list * string)list * Syntax.sext option -> sg val merge: sg * sg -> sg val pure: sg val read_cterm: sg -> string * typ -> cterm val read_ctyp: sg -> string -> ctyp val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option) - -> (indexname -> typ option) * (indexname -> sort option) - -> (string*string)list - -> (indexname*ctyp)list * (cterm*cterm)list + -> (indexname -> typ option) * (indexname -> sort option) + -> (string*string)list + -> (indexname*ctyp)list * (cterm*cterm)list val read_typ: sg * (indexname -> sort option) -> string -> typ val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int} val rep_ctyp: ctyp -> {T: typ, sign: sg} val rep_sg: sg -> {tsig: Type.type_sig, - const_tab: typ Symtab.table, - syn: Syntax.syntax, - stamps: string ref list} + const_tab: typ Symtab.table, + syn: Syntax.syntax, + stamps: string ref list} val string_of_cterm: cterm -> string val string_of_ctyp: ctyp -> string val pprint_cterm: cterm -> pprint_args -> unit @@ -53,7 +53,7 @@ end; -functor SignFun (structure Type:TYPE and Syntax:SYNTAX) : SIGN = +functor SignFun (structure Type:TYPE and Syntax:SYNTAX) : SIGN = struct structure Type = Type; structure Symtab = Type.Symtab; @@ -61,11 +61,11 @@ structure Pretty = Syntax.Pretty (*Signatures of theories. *) -datatype sg = - Sg of {tsig: Type.type_sig, (* order-sorted signature of types *) - const_tab: typ Symtab.table, (*types of constants*) - syn: Syntax.syntax, (*Parsing and printing operations*) - stamps: string ref list (*unique theory indentifier*) }; +datatype sg = + Sg of {tsig: Type.type_sig, (* order-sorted signature of types *) + const_tab: typ Symtab.table, (*types of constants*) + syn: Syntax.syntax, (*Parsing and printing operations*) + stamps: string ref list (*unique theory indentifier*) }; fun rep_sg (Sg args) = args; @@ -76,24 +76,24 @@ (*Is constant present in table with more generic type?*) fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of - Some U => Type.typ_instance(tsig,T,U) | _ => false; + Some U => Type.typ_instance(tsig,T,U) | _ => false; (*Check a term for errors. Are all constants and types valid in signature? Does not check that term is well-typed!*) -fun term_errors (sign as Sg{tsig,const_tab,...}) = +fun term_errors (sign as Sg{tsig,const_tab,...}) = let val showtyp = string_of_typ sign; fun terrs (Const (a,T), errs) = - if valid_const tsig const_tab (a,T) - then Type.type_errors (tsig,showtyp) (T,errs) - else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs + if valid_const tsig const_tab (a,T) + then Type.type_errors (tsig,showtyp) (T,errs) + else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs | terrs (Free (_,T), errs) = Type.type_errors (tsig,showtyp) (T,errs) | terrs (Var ((a,i),T), errs) = - if i>=0 then Type.type_errors (tsig,showtyp) (T,errs) - else ("Negative index for Var: " ^ a) :: errs + if i>=0 then Type.type_errors (tsig,showtyp) (T,errs) + else ("Negative index for Var: " ^ a) :: errs | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*) - | terrs (Abs (_,T,t), errs) = - Type.type_errors(tsig,showtyp)(T,terrs(t,errs)) + | terrs (Abs (_,T,t), errs) = + Type.type_errors(tsig,showtyp)(T,terrs(t,errs)) | terrs (f$t, errs) = terrs(f, terrs (t,errs)) in terrs end; @@ -102,7 +102,7 @@ (*Reset TVar indices to zero, renaming to preserve distinctness*) -fun zero_tvar_indices tsig T = +fun zero_tvar_indices tsig T = let val inxSs = typ_tvars T; val nms' = variantlist(map (#1 o #1) inxSs,[]); val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms') @@ -116,16 +116,16 @@ let val showtyp = Syntax.string_of_typ syn; fun read [] = [] | read((cs,s)::pairs) = - let val t = Syntax.read syn Syntax.typeT s handle ERROR => - error("The error above occurred in type " ^ s); - val S = Type.defaultS tsig; - val T = Type.varifyT(Syntax.typ_of_term (K S) t) - val T0 = zero_tvar_indices tsig T; - in (case Type.type_errors (tsig,showtyp) (T0,[]) of - [] => (cs,T0) :: read pairs - | errs => error (cat_lines - (("Error in type of constants " ^ space_implode " " cs) :: errs))) - end + let val t = Syntax.read syn Syntax.typeT s handle ERROR => + error("The error above occurred in type " ^ quote s); + val S = Type.defaultS tsig; + val T = Type.varifyT(Syntax.typ_of_term (K S) t) + val T0 = zero_tvar_indices tsig T; + in (case Type.type_errors (tsig,showtyp) (T0,[]) of + [] => (cs,T0) :: read pairs + | errs => error (cat_lines + (("Error in type of constants " ^ space_implode " " cs) :: errs))) + end in read end; @@ -134,11 +134,11 @@ The "ref" in stamps ensures that no two signatures are identical -- it is impossible to forge a signature. *) fun extend (Sg{tsig, const_tab, syn, stamps, ...}) signame - (newclasses, newdefault, otypes, newtypes, const_decs, osext) : sg = + (newclasses, newdefault, otypes, newtypes, const_decs, osext) : sg = let val tsig' = Type.extend(tsig,newclasses,newdefault,otypes,newtypes); val S = Type.defaultS tsig'; val roots = filter (Type.logical_type tsig') - (distinct(flat(map #1 newtypes))) + (distinct(flat(map #1 newtypes))) val xconsts = map #1 newclasses @ flat (map #1 otypes) @ flat (map #1 const_decs); val syn' = case osext of @@ -146,20 +146,20 @@ | None => if null roots andalso null xconsts then syn else Syntax.extend (syn, K S) (roots, xconsts, Syntax.empty_sext); val sconsts = case osext of - Some(sext) => Syntax.constants sext - | None => []; + Some(sext) => Syntax.constants sext + | None => []; val const_decs' = read_consts(tsig',syn') (sconsts @ const_decs) in Sg{tsig= tsig', const_tab= Symtab.st_of_declist (const_decs', const_tab) - handle Symtab.DUPLICATE(a) => - error("Constant '" ^ a ^ "' declared twice"), + handle Symtab.DUPLICATE(a) => + error("Constant " ^ quote a ^ " declared twice"), syn=syn', stamps= ref signame :: stamps} end; (* The empty signature *) val sg0 = Sg{tsig= Type.tsig0, const_tab= Symtab.null, - syn=Syntax.type_syn, stamps= []}; + syn=Syntax.type_syn, stamps= []}; (*The pure signature*) val pure : sg = extend sg0 "Pure" @@ -181,20 +181,20 @@ (*Update table with (a,x) providing any existing asgt to "a" equals x. *) fun update_eq ((a,x),tab) = case Symtab.lookup(tab,a) of - None => Symtab.update((a,x), tab) - | Some y => if x=y then tab - else raise TERM ("Incompatible types for constant: "^a, []); + None => Symtab.update((a,x), tab) + | Some y => if x=y then tab + else raise TERM ("Incompatible types for constant: "^a, []); (*Combine tables, updating tab2 by tab1 and checking.*) -fun merge_tabs (tab1,tab2) = +fun merge_tabs (tab1,tab2) = Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2)); (*Combine tables, overwriting tab2 with tab1.*) -fun smash_tabs (tab1,tab2) = +fun smash_tabs (tab1,tab2) = Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2)); (*Combine stamps, checking that theory names are disjoint. *) -fun merge_stamps (stamps1,stamps2) = +fun merge_stamps (stamps1,stamps2) = let val stamps = stamps1 union stamps2 in case findrep (map ! stamps) of a::_ => error ("Attempt to merge different versions of theory: " ^ a) @@ -203,14 +203,14 @@ (*Merge two signatures. Forms unions of tables. Prefers sign1. *) fun merge (sign1 as Sg{tsig=tsig1,const_tab=ctab1,stamps=stamps1,syn=syn1}, - sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) = + sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) = if stamps2 subset stamps1 then sign1 else if stamps1 subset stamps2 then sign2 else (*neither is union already; must form union*) - Sg{tsig= Type.merge(tsig1,tsig2), - const_tab= merge_tabs (ctab1, ctab2), - stamps= merge_stamps (stamps1,stamps2), - syn = Syntax.merge(syn1,syn2)}; + Sg{tsig= Type.merge(tsig1,tsig2), + const_tab= merge_tabs (ctab1, ctab2), + stamps= merge_stamps (stamps1,stamps2), + syn = Syntax.merge(syn1,syn2)}; (**** CERTIFIED TYPES ****) @@ -224,15 +224,15 @@ fun typ_of (Ctyp{sign,T}) = T; fun ctyp_of (sign as Sg{tsig,...}) T = - case Type.type_errors (tsig,string_of_typ sign) (T,[]) of - [] => Ctyp{sign= sign,T= T} - | errs => error (cat_lines ("Error in type:" :: errs)); + case Type.type_errors (tsig,string_of_typ sign) (T,[]) of + [] => Ctyp{sign= sign,T= T} + | errs => error (cat_lines ("Error in type:" :: errs)); (*The only use is a horrible hack in the simplifier!*) fun read_typ(Sg{tsig,syn,...}, defS) s = let val term = Syntax.read syn Syntax.typeT s; - val S0 = Type.defaultS tsig; - fun defS0 s = case defS s of Some S => S | None => S0; + val S0 = Type.defaultS tsig; + fun defS0 s = case defS s of Some S => S | None => S0; in Syntax.typ_of_term defS0 term end; fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None); @@ -274,19 +274,19 @@ (*Lexing, parsing, polymorphic typechecking of a term.*) fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts) - (a,T) = + (a,T) = let val showtyp = string_of_typ sign and showterm = string_of_term sign fun termerr [] = "" - | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n" - | termerr ts = "\nInvolving these terms:\n" ^ - cat_lines (map showterm ts) + | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n" + | termerr ts = "\nInvolving these terms:\n" ^ + cat_lines (map showterm ts) val t = Syntax.read syn T a; val (t',tye) = Type.infer_types (tsig, const_tab, types, - sorts, showtyp, T, t) - handle TYPE (msg, Ts, ts) => - error ("Type checking error: " ^ msg ^ "\n" ^ - cat_lines (map showtyp Ts) ^ termerr ts) + sorts, showtyp, T, t) + handle TYPE (msg, Ts, ts) => + error ("Type checking error: " ^ msg ^ "\n" ^ + cat_lines (map showtyp Ts) ^ termerr ts) in (cterm_of sign t', tye) end handle TERM (msg, _) => error ("Error: " ^ msg); @@ -297,7 +297,7 @@ (** reading of instantiations **) fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v - | _ => error("Lexical error in variable name: " ^ implode cs); + | _ => error("Lexical error in variable name " ^ quote (implode cs)); fun absent ixn = error("No such variable in term: " ^ Syntax.string_of_vname ixn); @@ -308,24 +308,24 @@ fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts = let fun split([],tvs,vs) = (tvs,vs) | split((sv,st)::l,tvs,vs) = (case explode sv of - "'"::cs => split(l,(indexname cs,st)::tvs,vs) - | cs => split(l,tvs,(indexname cs,st)::vs)); + "'"::cs => split(l,(indexname cs,st)::tvs,vs) + | cs => split(l,tvs,(indexname cs,st)::vs)); val (tvs,vs) = split(insts,[],[]); fun readT((a,i),st) = - let val ixn = ("'" ^ a,i); - val S = case rsorts ixn of Some S => S | None => absent ixn; - val T = read_typ (sign,sorts) st; - in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) - else inst_failure ixn - end + let val ixn = ("'" ^ a,i); + val S = case rsorts ixn of Some S => S | None => absent ixn; + val T = read_typ (sign,sorts) st; + in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) + else inst_failure ixn + end val tye = map readT tvs; fun add_cterm ((cts,tye), (ixn,st)) = - let val T = case rtypes ixn of - Some T => typ_subst_TVars tye T - | None => absent ixn; - val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T); - val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T)) - in ((cv,ct)::cts,tye2 @ tye) end + let val T = case rtypes ixn of + Some T => typ_subst_TVars tye T + | None => absent ixn; + val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T); + val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T)) + in ((cv,ct)::cts,tye2 @ tye) end val (cterms,tye') = foldl add_cterm (([],tye), vs); in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;