diff --git a/src/parse/GrammarSpecials.sig b/src/parse/GrammarSpecials.sig index 5c9ba1da2b..d6b8ee1ea8 100644 --- a/src/parse/GrammarSpecials.sig +++ b/src/parse/GrammarSpecials.sig @@ -34,6 +34,7 @@ sig val case_split_special : string val case_arrow_special : string val case_endbinding_special : string + val case_when_special : string val set_case_specials : ((Term.term -> Term.term) * diff --git a/src/parse/GrammarSpecials.sml b/src/parse/GrammarSpecials.sml index 0f92d1e593..ccf8ed5726 100644 --- a/src/parse/GrammarSpecials.sml +++ b/src/parse/GrammarSpecials.sml @@ -52,6 +52,7 @@ struct val case_split_special = "case_split__magic" val case_arrow_special = "case_arrow__magic" val case_endbinding_special = "case_endbinding__magic" + val case_when_special = "case_when__magic" open HolKernel val compilefn = ref (NONE : (term -> term) option) diff --git a/src/parse/Parse_support.sig b/src/parse/Parse_support.sig index 7de0c61af6..a98675d9e1 100644 --- a/src/parse/Parse_support.sig +++ b/src/parse/Parse_support.sig @@ -35,6 +35,13 @@ sig preterm_in_env -> preterm_in_env -> preterm_in_env + val pm_make_case_arrow : overload_info -> locn.locn -> + { bvs : Absyn.absyn option, + pat : preterm_in_env, + grd : preterm_in_env option, + rhs : preterm_in_env } -> + preterm_in_env + val binder_restrictions : unit -> (string * string) list val associate_restriction : locn.locn -> string * string -> unit val delete_restriction : locn.locn -> string -> unit diff --git a/src/parse/Parse_support.sml b/src/parse/Parse_support.sml index d010e97057..0b5542f718 100644 --- a/src/parse/Parse_support.sml +++ b/src/parse/Parse_support.sml @@ -467,6 +467,18 @@ fun make_set_const oinfo l fname s E = * will subsequently get bound in the set abstraction. *---------------------------------------------------------------------------*) +fun mk_one_vstruct oinfo l (qvs0:(string*pretype)list) = + let + val qvs = + map (fn (bnd as (Name,Ty)) => fn E => + ((fn b => Preterm.Abs{Bvar=Preterm.Var{Name=Name,Ty=Ty,Locn=l}, + Body=b, Locn=l}), + add_scope(bnd,E))) + (rev qvs0) + in + [make_vstruct oinfo l qvs NONE] + end + fun make_set_abs oinfo l (tm1,tm2) (E as {scope=scope0,...}:env) = let val (_,(e1:env)) = tm1 empty_env val (_,(e2:env)) = tm2 empty_env @@ -481,18 +493,12 @@ in case filter (fn (name,_) => mem name fv_names) init_fv of [] => raise ERRORloc "make_set_abs" l "no free variables in set abstraction" | quants => let - val quants' = map - (fn (bnd as (Name,Ty)) => - fn E => - ((fn b => Preterm.Abs{Bvar=Preterm.Var{Name=Name,Ty=Ty,Locn=l(*ugh*)}, - Body=b, Locn=l}), - add_scope(bnd,E))) - (rev quants) (* make_vstruct expects reverse occ. order *) fun comma E = (gen_overloaded_const oinfo l ",", E) in list_make_comb l [(make_set_const oinfo l "make_set_abs" "GSPEC"), - (bind_term l [make_vstruct oinfo l quants' NONE] + (bind_term l + (mk_one_vstruct oinfo l quants) (list_make_comb l [comma,tm1,tm2]))] E end end @@ -518,6 +524,61 @@ in Locn = loc}, E') end +(* ---------------------------------------------------------------------- + pm_make_case_arrow + + If the bvs are present, the Absyn should be parsed into a var-struct + that will bind the remaining components. If not, then the var-struct + should be built by extracting variables from the pat. If the grd is + absent, then it turns into combin$K bool$T (ignoring bvs even if + present). + ---------------------------------------------------------------------- *) + +fun to_vstruct oinfo a = + let + open Absyn + in + case a of + APP(l, APP(_, IDENT(_, ","), t1), t2) => + make_vstruct oinfo l (map (to_vstruct oinfo) [t1, t2]) NONE + | AQ (l,t) => make_aq_binding_occ l t + | IDENT(l,s) => make_binding_occ l s + | TYPED(l, t, pty) => make_vstruct oinfo l [to_vstruct oinfo t] (SOME pty) + | _ => raise ERRORloc "Parse_support" (locn_of_absyn a) + "Bad variable structure" + end + +val unit_pty = Pretype.Tyop{Thy = "one", Tyop = "one", Args = []} + +fun pm_make_case_arrow oinfo loc {bvs,pat:preterm_in_env,grd,rhs} = + let + val vstruct : bvar_in_env list = + case bvs of + NONE => + let + val (pat_ptm, patE) = pat empty_env + val pat_fv_names0 = #free patE + val qvs = case pat_fv_names0 of + [] => [("_",unit_pty)] + | vs => vs + in + mk_one_vstruct oinfo loc qvs + end + | SOME a => [to_vstruct oinfo a] + val guard = + case grd of + NONE => list_make_comb loc [make_qconst loc ("combin", "K"), + make_qconst loc ("bool", "T")] + | SOME g => bind_term loc vstruct g + in + list_make_comb loc [make_qconst loc ("patternMatches", "PMATCH_ROW"), + bind_term loc vstruct pat, + guard, + bind_term loc vstruct rhs] + end + + + (*--------------------------------------------------------------------------- * Sequence abstractions [| tm1 | tm2 |]. diff --git a/src/parse/TermParse.sml b/src/parse/TermParse.sml index ffee98c07a..284776cb68 100644 --- a/src/parse/TermParse.sml +++ b/src/parse/TermParse.sml @@ -197,14 +197,15 @@ local open Parse_support Absyn | _ => raise ERRORloc "Term" (locn_of_absyn t) "Bad variable-structure" in - fun absyn_to_preterm_in_env oinfo t = let + fun absyn_to_preterm_in_env TmG t = let + val oinfo = term_grammar.overload_info TmG fun binder(VIDENT (l,s)) = make_binding_occ l s | binder(VPAIR(l,v1,v2)) = make_vstruct oinfo l [binder v1, binder v2] NONE | binder(VAQ (l,x)) = make_aq_binding_occ l x | binder(VTYPED(l,v,pty)) = make_vstruct oinfo l [binder v] (SOME pty) open parse_term Absyn Parse_support - val to_ptmInEnv = absyn_to_preterm_in_env oinfo + val to_ptmInEnv = absyn_to_preterm_in_env TmG in case t of APP(l,APP(_,IDENT (_,"gspec special"), t1), t2) => @@ -216,23 +217,72 @@ in to_ptmInEnv (APP(l, QIDENT(l, "pred_set", "GSPEC"), LAM(l, to_vstruct t2, newbody))) end - | APP(l, APP(_, t0 as IDENT (_, caseform), t1), t2) => let + | APP(l, APP(_, t0 as IDENT (_, caseform), t1), t2) => + let + fun every_case sing cons base ab = + case ab of + APP(l, APP(_, t0 as IDENT (_, casesplit), t1), t2) => + let + in + if casesplit = GrammarSpecials.case_split_special then let + val t1' = base t1 + val t2' = every_case sing cons base t2 + in + list_make_comb l [cons, t1', t2'] + end + else sing (base ab) + end + | _ => sing (base ab) in - if caseform = GrammarSpecials.case_special then let - (* handle possible arrows in t2 *) - fun every_case base ab = + if caseform = GrammarSpecials.case_special then + if #pmatch_on (term_grammar.specials TmG) then + let + fun splitrow_opt_kR opn k ab = case ab of - APP(l, APP(_, t0 as IDENT (_, casesplit), t1), t2) => let - in - if casesplit = GrammarSpecials.case_split_special then let - val t1' = every_case base t1 - val t2' = every_case base t2 - in - list_make_comb l [to_ptmInEnv t0, t1', t2'] - end - else base ab - end - | _ => base ab + APP(_, APP(_, t0 as IDENT (_, row_opn), t1), t2) => + if row_opn = opn then (SOME t1, k t2) + else (NONE, k ab) + | _ => (NONE, k ab) + fun splitrow_opt_kL opn k ab = + case ab of + APP(_, APP(_, IDENT(_, row_opn), t1), t2) => + if row_opn = opn then (k t1, SOME t2) + else (k ab, NONE) + | _ => (k ab, NONE) + fun splitrow_kL opn k ab = + case ab of + APP(l, APP(_, IDENT(_, row_opn), t1), t2) => + if row_opn = opn then (k t1, t2) + else raise ERRORloc "Term" l + "Mal-formed case expression (no arrow)" + | _ => raise ERRORloc "Term" l + "Mal-formed case expression (no arrow)" + fun do_row a = + let + open GrammarSpecials + val (bvsopt, ((pat_a, grd_a), rhs_a)) = + splitrow_opt_kR case_endbinding_special + (splitrow_kL + case_arrow_special + (splitrow_opt_kL case_when_special I)) + a + in + pm_make_case_arrow + oinfo (locn_of_absyn a) + {bvs = bvsopt, pat = to_ptmInEnv pat_a, + grd = Option.map to_ptmInEnv grd_a, + rhs = to_ptmInEnv rhs_a} + end + val cons_pt = make_qconst l ("list", "CONS") + fun sing pt = + list_make_comb l [cons_pt, pt, make_qconst l ("list", "NIL")] + val rows = every_case sing cons_pt do_row t2 + val match_pt = make_qconst l ("patternMatches", "PMATCH") + in + list_make_comb l [match_pt, to_ptmInEnv t1, rows] + end + else let + (* handle possible arrows in t2 *) fun do_arrow ab = case ab of APP(l, APP(_, t0 as IDENT (_, casearrow), t1), t2) => let @@ -245,9 +295,11 @@ in end | _ => raise ERRORloc "Term" (locn_of_absyn ab) "Mal-formed case expression (no arrow)" + val row_cons = + to_ptmInEnv (IDENT(l, GrammarSpecials.case_split_special)) in list_make_comb l [to_ptmInEnv t0, to_ptmInEnv t1, - every_case do_arrow t2] + every_case (fn x => x) row_cons do_arrow t2] end else if String.isPrefix GrammarSpecials.recfupd_special caseform then let @@ -287,11 +339,8 @@ in end end; -fun absyn_to_preterm g a = let - val oinfo = term_grammar.overload_info g -in - a |> absyn_to_preterm_in_env oinfo |> Parse_support.make_preterm -end +fun absyn_to_preterm g a = + a |> absyn_to_preterm_in_env g |> Parse_support.make_preterm fun preterm g tyg q = q |> absyn g tyg |> absyn_to_preterm g diff --git a/src/pattern_matches/patternMatchesScript.sml b/src/pattern_matches/patternMatchesScript.sml index 0ddb3cb13d..8e6abf8214 100644 --- a/src/pattern_matches/patternMatchesScript.sml +++ b/src/pattern_matches/patternMatchesScript.sml @@ -1268,6 +1268,12 @@ val _ = add_rule{pp_elements = [HardSpace 1, TOK ".|", BreakSpace(1,2)], paren_style = OnlyIfNecessary, term_name = GrammarSpecials.case_endbinding_special} -val _ = set_pmatch_use true +val _ = add_rule{pp_elements = [HardSpace 1, TOK "when", BreakSpace(1,2)], + fixity = Infix(NONASSOC,14), + block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), + paren_style = OnlyIfNecessary, + term_name = GrammarSpecials.case_when_special} + +(* val _ = set_pmatch_use true *) val _ = export_theory();; diff --git a/src/pattern_matches/patternMatchesSyntax.sml b/src/pattern_matches/patternMatchesSyntax.sml index b402c06622..2e585e7b04 100644 --- a/src/pattern_matches/patternMatchesSyntax.sml +++ b/src/pattern_matches/patternMatchesSyntax.sml @@ -701,7 +701,7 @@ fun pmatch_printer GS backend sys (ppfns:term_pp_types.ppstream_funs) gravs d t not (free_in vars guard) andalso not (free_in vars rh)) then ( add_string "|||." >> add_break (1, 0) - ) else ( + ) else ( add_string "|||" >> add_break (1, 0) >> sys (Top, Top, Top) (d - 1) vars >> @@ -797,7 +797,7 @@ val PMATCH_ROW_magic_3_tm = mk_const("PMATCH_ROW_magic_3", val PMATCH_ROW_magic_4_tm = mk_const ("PMATCH_ROW_magic_4", ``:'a # bool # 'b -> 'a -> 'b option``); -val _ = temp_add_rule{pp_elements = [TOK "~>"], +(* val _ = temp_add_rule{pp_elements = [TOK "~>"], fixity = Infix (NONASSOC, 3), block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = OnlyIfNecessary, @@ -809,6 +809,7 @@ val _ = temp_add_rule{term_name = "PMATCH_ROW_magic_2", paren_style = OnlyIfNecessary, block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0))}; +*) val _ = temp_add_rule{term_name = "PMATCH_ROW_magic_1", fixity = Binder,