diff --git a/src/redprl/inductive_spec.sig b/src/redprl/inductive_spec.sig index 980e1fee2..9f6d0171c 100644 --- a/src/redprl/inductive_spec.sig +++ b/src/redprl/inductive_spec.sig @@ -4,24 +4,31 @@ sig structure ConstrDict : DICT where type key = conid type decl = RedPrlAbt.abt (* XXX *) type constr = RedPrlAbt.abt (* XXX *) + type constrs = (conid * constr) list type decl_args = RedPrlAbt.abt RedPrlAbt.bview list type args = RedPrlAbt.abt list - type precomputedArity - val eqPrecomputedArity : precomputedArity * precomputedArity -> bool + type precomputed_valences + val eqPrecomputedValences : precomputed_valences * precomputed_valences -> bool (* Given a data declaration, generate a list of sequents for type-checking. *) val checkDecl : decl -> Sequent.jdg list (* Valence collectors. *) - val computeValences : RedPrlAst.ast -> precomputedArity - val getTypeValences : precomputedArity -> RedPrlArity.valence list - val getIntroValences : precomputedArity -> conid -> RedPrlArity.valence list - val getElimValences : precomputedArity -> RedPrlArity.valence list + val computeValences : RedPrlAst.ast -> precomputed_valences + val getTypeValences : precomputed_valences -> RedPrlArity.valence list + val getIntroValences : precomputed_valences -> conid -> RedPrlArity.valence list + val getElimValences : precomputed_valences -> RedPrlArity.valence list val computeAllSpecIntroValences : RedPrlAst.ast -> RedPrlArity.valence list ConstrDict.dict (* Used by the machine. *) - val realizeIntroBoundaries : MlId.t * precomputedArity * conid -> - decl_args -> decl -> args -> RedPrlAbt.abt SyntaxView.boundary list + val fillInFamily : decl -> RedPrlAbt.abt RedPrlAbt.bview list -> args * constrs * RedPrlAbt.abt RedPrlAbt.bview list + val realizeIntroBoundaries : MlId.t * (RedPrlArity.valence list * precomputed_valences) * (decl_args * args) + -> constr -> args -> RedPrlAbt.abt SyntaxView.boundary list + val fillInBranch : (RedPrlAbt.abt -> RedPrlAbt.abt) + -> constr -> Sym.t list * RedPrlAbt.abt -> args -> RedPrlAbt.abt + val stepCoeIntro : RedPrlAbt.abt * RedPrlAbt.abt + -> Sym.t * ((MlId.t * (RedPrlArity.valence list * precomputed_valences) * (decl_args * args)) * conid * constr) + -> args -> RedPrlAbt.abt (* Used by the refiner. *) (* val EqArgsForType : decl -> args * args -> Sequent.jdg list *) diff --git a/src/redprl/inductive_spec.sml b/src/redprl/inductive_spec.sml index 88e31dce5..1630e4fa1 100644 --- a/src/redprl/inductive_spec.sml +++ b/src/redprl/inductive_spec.sml @@ -13,6 +13,7 @@ struct type conid = string type decl = RedPrlAbt.abt (* XXX *) type constr = RedPrlAbt.abt (* XXX *) + type constrs = (conid * constr) list type decl_args = RedPrlAbt.abt RedPrlAbt.bview list type args = RedPrlAbt.abt list @@ -21,7 +22,6 @@ struct structure ConstrDict = StringListDict structure SpecCtx = Var.Ctx structure DimSet = ListSet (structure Elem = Sym.Ord) - type constrs = Abt.abt ConstrDict.dict type specctx = Abt.abt SpecCtx.dict type dimset = DimSet.set @@ -365,12 +365,12 @@ struct open ArityNotation infix ->> |: - type precomputedArity = + type precomputed_valences = {tyVls: RedPrlArity.valence list, introExtraVls: RedPrlArity.valence list ConstrDict.dict, elimExtraVls: RedPrlArity.valence list} - fun eqPrecomputedArity + fun eqPrecomputedValences ({tyVls=tyVls0, introExtraVls=introExtraVls0, elimExtraVls=elimExtraVls0}, {tyVls=tyVls1, introExtraVls=introExtraVls1, elimExtraVls=elimExtraVls1}) = tyVls0 = tyVls1 andalso @@ -472,55 +472,152 @@ struct | Ast.$ (O.IND_FAM_LINE, [Ast.\ (_, bx)]) => computeAllSpecIntroValences bx end + fun \\ t = Abt.\ ([], t) + + local + fun fillInFamily' varenv revTyArgs decl args = + case (Syn.out decl, args) of + (Syn.IND_FAM_BASE (_, l), _) => (List.rev revTyArgs, List.map (fn (conid, constr) => (conid, Abt.substVarenv varenv constr)) l, args) + | (Syn.IND_FAM_FUN (_,x,bx), Abt.\([],arg)::args) => + fillInFamily' (Var.Ctx.insert varenv x arg) (arg::revTyArgs) bx args + | (Syn.IND_FAM_LINE (x,bx), Abt.\([],arg)::args) => + fillInFamily' (Var.Ctx.insert varenv x arg) (arg::revTyArgs) bx args + in + fun fillInFamily decl args = fillInFamily' Var.Ctx.empty [] decl args + end + + (* XXX Maybe `opid` should be `tyid`? *) + + fun substSpan varenv (r0, r1) = (Abt.substVarenv varenv r0, Abt.substVarenv varenv r1) + + fun intoType (opid, (declVls, precomputedVls), (declArgs, tyArgs)) = + Abt.$$ (O.IND_TYPE (opid, SOME (declVls @ getTypeValences precomputedVls)), + declArgs @ List.map \\ tyArgs) + + fun intoIntro (opid, (declVls, precomputedVls), (declArgs, tyArgs)) conid introArgs = + Abt.$$ + (O.IND_INTRO (opid, conid, SOME (declVls @ getIntroValences precomputedVls conid)), + declArgs @ List.map \\ tyArgs @ List.map \\ introArgs) + + fun realizeSpecType meta varenv ty = + case Syn.out ty of + Syn.IND_SPECTYPE_SELF => intoType meta + | Syn.IND_SPECTYPE_FUN (a, x, bx) => Syn.into (Syn.FUN (Abt.substVarenv varenv a, x, realizeSpecType meta varenv bx)) + + fun realizeSpecTerm (meta as (opid, (declVls, precomputedVls), (declArgs, tyArgs))) varenv term = + case Syn.out term of + Syn.VAR (x, _) => Option.getOpt (Var.Ctx.find varenv x, term) + | Syn.IND_SPEC_INTRO (conid, args) => intoIntro meta conid (List.map (realizeSpecTerm meta varenv) args) + | Syn.IND_SPEC_FCOM {dir, cap, tubes} => + Syn.intoFcom + {dir = substSpan varenv dir, + cap = realizeSpecTerm meta varenv cap, + tubes = List.map (realizeTube meta varenv) tubes} + | _ => term (* we can avoid this case by checking the valences *) + + and realizeTube meta varenv (eq, (u, term)) = + (substSpan varenv eq, (u, realizeSpecTerm meta varenv term)) + + fun realizeSpecBoundary meta varenv (eq, term) = + (substSpan varenv eq, realizeSpecTerm meta varenv term) + + fun realizeSpecBoundaries meta varenv = + List.map (realizeSpecBoundary meta varenv) + local - (* XXX Maybe `opid` should be `tyid`? *) - - fun realizeSpecSpan varenv (r0, r1) = (Abt.substVarenv varenv r0, Abt.substVarenv varenv r1) - - fun realizeSpecTerm (opid, arity, revPrefix) varenv term = - case Syn.out term of - Syn.META _ => term - | Syn.VAR (x, _) => Option.getOpt (Var.Ctx.find varenv x, term) - | Syn.IND_SPEC_INTRO (conid, args) => Abt.$$ - (O.IND_INTRO (opid, conid, SOME (getIntroValences arity conid)), - List.revAppend (revPrefix, List.map (fn t => Abt.\ ([], realizeSpecTerm (opid, arity, revPrefix) varenv t)) args)) - | Syn.IND_SPEC_FCOM {dir, cap, tubes} => - Syn.intoFcom - {dir = realizeSpecSpan varenv dir, - cap = realizeSpecTerm (opid, arity, revPrefix) varenv cap, - tubes = List.map (realizeTube (opid, arity, revPrefix) varenv) tubes} - - and realizeTube (opid, arity, revPrefix) varenv (eq, (u, term)) = - (realizeSpecSpan varenv eq, (u, realizeSpecTerm (opid, arity, revPrefix) varenv term)) - - fun realizeSpecBoundary (opid, arity, revPrefix) varenv (eq, term) = - (realizeSpecSpan varenv eq, realizeSpecTerm (opid, arity, revPrefix) varenv term) - - fun realizeInternalIntroBoundaries (opid, arity, revPrefix) varenv constr args = + fun realizeIntroBoundaries' meta varenv constr args = case (Syn.out constr, args) of (Syn.IND_CONSTR_DISCRETE boundaries, []) => - List.map (realizeSpecBoundary (opid, arity, revPrefix) varenv) boundaries + realizeSpecBoundaries meta varenv boundaries | (Syn.IND_CONSTR_KAN boundaries, []) => - List.map (realizeSpecBoundary (opid, arity, revPrefix) varenv) boundaries + realizeSpecBoundaries meta varenv boundaries | (Syn.IND_CONSTR_FUN (_,x,bx), arg::args) => - realizeInternalIntroBoundaries (opid, arity, revPrefix) (Var.Ctx.insert varenv x arg) bx args + realizeIntroBoundaries' meta (Var.Ctx.insert varenv x arg) bx args | (Syn.IND_CONSTR_SPEC_FUN (_,x,bx), arg::args) => - realizeInternalIntroBoundaries (opid, arity, revPrefix) (Var.Ctx.insert varenv x arg) bx args + realizeIntroBoundaries' meta (Var.Ctx.insert varenv x arg) bx args | (Syn.IND_CONSTR_LINE (x,bx), arg::args) => - realizeInternalIntroBoundaries (opid, arity, revPrefix) (Var.Ctx.insert varenv x arg) bx args + realizeIntroBoundaries' meta (Var.Ctx.insert varenv x arg) bx args + in + fun realizeIntroBoundaries meta constr args = + realizeIntroBoundaries' meta Var.Ctx.empty constr args + end - fun realizeIntroBoundaries' (opid, arity, conid) revPrefix varenv decl args = - case (Syn.out decl, args) of - (Syn.IND_FAM_BASE (_, l), _) => - realizeInternalIntroBoundaries (opid, arity, revPrefix) varenv - (#2 (Option.valOf (List.find (fn (id, _) => id = conid) l))) args - | (Syn.IND_FAM_FUN (_,x,bx), arg::args) => - realizeIntroBoundaries' (opid, arity, conid) (Abt.\ ([], arg) :: revPrefix) (Var.Ctx.insert varenv x arg) bx args - | (Syn.IND_FAM_LINE (x,bx), arg::args) => - realizeIntroBoundaries' (opid, arity, conid) (Abt.\ ([], arg) :: revPrefix) (Var.Ctx.insert varenv x arg) bx args + local + fun recResult plug specTy arg = + case Syn.out specTy of + Syn.IND_SPECTYPE_SELF => plug arg + | Syn.IND_SPECTYPE_FUN (_,x,bx) => Syn.intoLam (x, recResult plug bx (Syn.intoApp (arg, VarKit.toExp x))) + + fun fillInBranch' plug varenv constr (vars, branch) introArgs = + case (Syn.out constr, vars, introArgs) of + (Syn.IND_CONSTR_DISCRETE _, [], []) => Abt.substVarenv varenv branch + | (Syn.IND_CONSTR_KAN _, [], []) => Abt.substVarenv varenv branch + | (Syn.IND_CONSTR_FUN (_,_,bx), var::vars, arg::introArgs) => + fillInBranch' plug (Var.Ctx.insert varenv var arg) bx (vars, branch) introArgs + | (Syn.IND_CONSTR_SPEC_FUN (a,_,bx), var::recvar::vars, arg::introArgs) => + let + val varenv = Var.Ctx.insert varenv var arg + val varenv = Var.Ctx.insert varenv recvar (recResult plug a arg) + in + fillInBranch' plug varenv bx (vars, branch) introArgs + end + | _ => E.raiseError (E.IMPOSSIBLE (Fpp.text "fillInBranch")) + in + fun fillInBranch plug constr branch introArgs = + fillInBranch' plug Var.Ctx.empty constr branch introArgs + end + + local + fun stepCoeIntro' (dir as (r, r')) (z, (meta, varenv, conid, constr)) revCoercedArgs introArgs = + case (Syn.out constr, introArgs) of + (Syn.IND_CONSTR_DISCRETE [], []) => intoIntro meta conid (List.rev revCoercedArgs) + | (Syn.IND_CONSTR_KAN boundaries, []) => + let + fun makeTube (eq, term) = + (substSpan varenv eq, + (z, + Syn.intoCoe + {dir = (VarKit.toDim z, r'), + ty = (z, intoType meta), + coercee = realizeSpecTerm meta varenv term})) + in + Syn.intoFcom + {dir = (r', r), + cap = intoIntro meta conid (List.rev revCoercedArgs), + tubes = List.map makeTube boundaries} + end + | (Syn.IND_CONSTR_FUN (a, x, bx), arg::introArgs) => + let + fun coe r' = Syn.intoCoe + {dir = (#1 dir, r'), + ty = (z, Abt.substVarenv varenv a), + coercee = arg} + val varenv' = Var.Ctx.insert varenv x (coe (VarKit.toDim z)) + val revCoercedArgs' = coe r' :: revCoercedArgs + in + stepCoeIntro' dir (z, (meta, varenv', conid, bx)) revCoercedArgs' introArgs + end + | (Syn.IND_CONSTR_SPEC_FUN (a, x, bx), arg::introArgs) => + let + fun coe r' = Syn.intoCoe + {dir = (#1 dir, r'), + ty = (z, realizeSpecType meta varenv a), + coercee = arg} + val varenv' = Var.Ctx.insert varenv x (coe (VarKit.toDim z)) + val revCoercedArgs' = coe r' :: revCoercedArgs + in + stepCoeIntro' dir (z, (meta, varenv', conid, bx)) revCoercedArgs' introArgs + end + | (Syn.IND_CONSTR_LINE (x, bx), arg::introArgs) => + let + val varenv' = Var.Ctx.insert varenv x arg + val revCoercedArgs' = Abt.substVar (r', z) arg :: revCoercedArgs + in + stepCoeIntro' dir (z, (meta, varenv', conid, bx)) revCoercedArgs' introArgs + end in - fun realizeIntroBoundaries (opid, arity, conid) declArgs decl args = - realizeIntroBoundaries' (opid, arity, conid) (List.rev declArgs) Var.Ctx.empty decl args + fun stepCoeIntro dir (z, (meta, conid, constr)) introArgs = + stepCoeIntro' dir (z, (meta, Var.Ctx.empty, conid, constr)) [] introArgs end end diff --git a/src/redprl/list_util.sml b/src/redprl/list_util.sml index 2e0b62fef..9ca64e331 100644 --- a/src/redprl/list_util.sml +++ b/src/redprl/list_util.sml @@ -92,4 +92,9 @@ struct in List.concat o enum end + + fun find p = + fn (nil, _) => NONE + | (_, nil) => NONE + | (x::xs, y::ys) => if p (x, y) then SOME (x, y) else find p (xs, ys) end diff --git a/src/redprl/machine.fun b/src/redprl/machine.fun index 3174c41c1..842846860 100644 --- a/src/redprl/machine.fun +++ b/src/redprl/machine.fun @@ -30,6 +30,8 @@ struct | S1_REC of (variable * abt) * hole * abt * (variable * abt) | PUSHOUT_REC of (variable * abt) * hole * (variable * abt) * (variable * abt) * (variable * variable * abt) | COEQUALIZER_REC of (variable * abt) * hole * (variable * abt) * (variable * variable * abt) + | IND_REC of (opid * RedPrlArity.valence list) * abt RedPrlAbt.bview list * abt list * (variable * abt) * hole * abt RedPrlAbt.bview list + | COE_IND of Syn.dir * (variable * (opid * RedPrlArity.valence list * abt RedPrlAbt.bview list)) * hole | DIM_APP of hole * abt | NAT_REC of (variable * abt) * hole * abt * (variable * variable * abt) | INT_REC of (variable * abt) * hole * (variable * abt) * (variable * abt) @@ -59,6 +61,9 @@ struct | TUPLE_UPDATE (lbl, n, HOLE) => Syn.into @@ Syn.TUPLE_UPDATE ((lbl, m), m) | PUSHOUT_REC ((x, tyx), HOLE, (y, left), (z, right), (u, w, glue)) => Syn.into @@ Syn.PUSHOUT_REC ((x, tyx), m, ((y, left), (z, right), (u, w, glue))) | COEQUALIZER_REC ((x, tyx), HOLE, (y, cod), (u, w, dom)) => Syn.into @@ Syn.COEQUALIZER_REC ((x, tyx), m, ((y, cod), (u, w, dom))) + | IND_REC ((opid, vls), declArgs, tyArgs, (x, tyx), HOLE, branches) => + Tm.$$ (O.IND_REC (opid, SOME vls), declArgs @ List.map (fn t => [] \ t) tyArgs @ [[x] \ tyx] @ [[] \ m] @ branches) + | COE_IND (dir, (x, (opid, vls, args)), HOLE) => Syn.intoCoe {dir = dir, ty = (x, Tm.$$ (O.IND_TYPE (opid, SOME vls), args)), coercee = m} | CAP (dir, tubes, HOLE) => Syn.into @@ Syn.CAP {dir = dir, tubes = tubes, coercee = m} | VPROJ (x, HOLE, f) => Syn.into @@ Syn.VPROJ (VarKit.toDim x, m, f) @@ -174,7 +179,26 @@ struct | CRITICAL of 'a | STEP of 'a - fun stepFCom stability ({dir = dir as (r, r'), cap, tubes} || (syms, stk)) = + fun pushFrameIntoFCom ((((x, tyx), frame), {dir = dir as (r, _), cap, tubes}) || (syms, stk)) = + let + val u = Sym.new() + val fcomu = + Syn.intoFcom + {dir = (r, VarKit.toDim u), + cap = cap, + tubes = tubes} + fun elim_ m = plug m frame + val com = + Syn.intoCom + {dir = dir, + ty = (u, substVar (fcomu, x) tyx), + cap = elim_ cap, + tubes = mapTubes_ elim_ tubes} + in + CRITICAL @@ com || (syms, stk) + end + + fun stepFCom stability ((params as {dir = dir as (r, r'), cap, tubes}) || (syms, stk)) = if dimensionsEqual stability syms dir then STEP @@ cap || (syms, stk) else @@ -183,41 +207,22 @@ struct | NONE => (case stk of [] => raise Final - | IF ((x, tyx), HOLE, t, f) :: stk => - let - val u = Sym.new() - val fcomu = - Syn.intoFcom - {dir = (r, VarKit.toDim u), - cap = cap, - tubes = tubes} - fun if_ m = Syn.into @@ Syn.IF ((x, tyx), m, (t, f)) - val com = - Syn.into @@ Syn.COM - {dir = dir, - ty = (u, substVar (fcomu, x) tyx), - cap = if_ cap, - tubes = mapTubes_ if_ tubes} - in - CRITICAL @@ com || (syms, stk) - end - | S1_REC ((x, tyx), HOLE, base, (v, loop)) :: stk => + | (frame as IF (motive, HOLE, _, _)) :: stk => + pushFrameIntoFCom (((motive, frame), params) || (syms, stk)) + | (frame as S1_REC (motive, HOLE, _, _)) :: stk => + pushFrameIntoFCom (((motive, frame), params) || (syms, stk)) + | (frame as PUSHOUT_REC (motive, HOLE, _, _, _)) :: stk => + pushFrameIntoFCom (((motive, frame), params) || (syms, stk)) + | (frame as COEQUALIZER_REC (motive, HOLE, _, _)) :: stk => + pushFrameIntoFCom (((motive, frame), params) || (syms, stk)) + | (frame as COE_IND _) :: stk => let - val u = Sym.new () - val fcomu = - Syn.intoFcom - {dir = (r, VarKit.toDim u), - cap = cap, - tubes = tubes} - fun s1rec m = Syn.into @@ Syn.S1_REC ((x, tyx), m, (base, (v, loop))) - val com = - Syn.into @@ Syn.COM - {dir = dir, - ty = (u, substVar (fcomu, x) tyx), - cap = s1rec cap, - tubes = mapTubes_ s1rec tubes} + val fcom = Syn.intoFcom + {dir = dir, + cap = plug cap frame, + tubes = mapTubes_ (fn m => plug m frame) tubes} in - CRITICAL @@ com || (syms, stk) + CRITICAL @@ fcom || (syms, stk) end | HCOM (hcomDir, HOLE, hcomCap, hcomTubes) :: stk => (* favonia: the version implemented below is different from the one @@ -391,6 +396,42 @@ struct end | _ => raise Stuck) + fun stepIntro sign stability ((opid, conid, vls, args) || (syms, stk)) = + let + val (declArgs, (decl, precomputedVls), nonDeclArgs) = Sig.dataDeclInfo sign opid args + val (tyArgs, constrs, introArgs) = InductiveSpec.fillInFamily decl nonDeclArgs + val declVls = List.take (vls, List.length declArgs) + val meta = (opid, (declVls, precomputedVls), (declArgs, tyArgs)) + val introArgs = List.map (fn _ \ t => t) introArgs + + val (conIndex, (_, constr)) = Option.valOf (ListUtil.findIndex (fn (id, _) => id = conid) constrs) + val boundaries = InductiveSpec.realizeIntroBoundaries meta constr introArgs + in + case findFirstWithTrueEquation stability syms boundaries of + SOME b => STEP @@ b || (syms, stk) + | NONE => + (case stk of + [] => raise Final + | (frame as IND_REC ((opid', _), _, _, _, HOLE, branches)) :: stk => + let + val () = if opid' = opid then () else raise Stuck + val Tm.\ branch = List.nth (branches, conIndex) + in + CRITICAL @@ InductiveSpec.fillInBranch (fn m => plug m frame) constr branch introArgs || (syms, stk) + end + | COE_IND (dir, (z, (opid', _, args')), HOLE) :: stk => + let + val () = if opid' = opid then () else raise Stuck + val (declArgs', (decl', _), nonDeclArgs') = Sig.dataDeclInfo sign opid args' + val (tyArgs', constrs', []) = InductiveSpec.fillInFamily decl' nonDeclArgs' + val meta' = (opid, (declVls, precomputedVls), (declArgs', tyArgs')) + val (_, constr') = List.nth (constrs', conIndex) + in + CRITICAL @@ InductiveSpec.stepCoeIntro dir (z, (meta', conid, constr')) introArgs || (syms, stk) + end + | _ => raise Stuck) + end + fun stepBox stability ({dir, cap, boundaries} || (syms, stk)) = if dimensionsEqual stability syms dir then STEP @@ cap || (syms, stk) @@ -879,6 +920,29 @@ struct CRITICAL @@ result || (SymSet.remove syms u, stk) end + | O.IND_TYPE _ $ _ || (_, []) => raise Final + | O.IND_INTRO (opid, conid, SOME vls) $ args || (syms, stk) => + stepIntro sign stability ((opid, conid, vls, args) || (syms, stk)) + | O.IND_REC (opid, vls) $ args || (syms, stk) => + let + val (declArgs, (decl, _), nonDeclArgs) = Sig.dataDeclInfo sign opid args + val (tyArgs, _, ([x] \ cx :: [] \ m :: branches)) = InductiveSpec.fillInFamily decl nonDeclArgs + in + COMPAT @@ m || (syms, IND_REC ((opid, Option.valOf vls), declArgs, tyArgs, (x, cx), HOLE, branches) :: stk) + end + | O.IND_TYPE _ $ _ || (syms, HCOM (dir, HOLE, cap, tubes) :: stk) => + let + val fcom = + Syn.intoFcom + {dir = dir, + cap = cap, + tubes = tubes} + in + CRITICAL @@ fcom || (syms, stk) + end + | O.IND_TYPE (opid, vls) $ args || (syms, COE (dir, (u, HOLE), coercee) :: stk) => + CRITICAL @@ coercee || (SymSet.remove syms u, COE_IND (dir, (u, (opid, Option.valOf vls, args)), HOLE) :: stk) + | O.BOX $ [_ \ r1, _ \ r2, _ \ cap, _ \ boundaries] || (syms, stk) => stepBox stability ({dir = (r1, r2), cap = cap, boundaries = Syn.outBoundaries boundaries} || (syms, stk)) | O.CAP $ [_ \ r1, _ \ r2, _ \ coercee, _ \ tubes] || (syms, stk) => diff --git a/src/redprl/metalanguage/elaborate.fun b/src/redprl/metalanguage/elaborate.fun index 3e3ce0ebb..ac5de4c03 100644 --- a/src/redprl/metalanguage/elaborate.fun +++ b/src/redprl/metalanguage/elaborate.fun @@ -273,7 +273,7 @@ struct val sequents' = fn env => InductiveSpec.checkDecl (decl' env) val script' = fn env => elabAst env R.dummy_spec_env (script, RedPrlSort.MTAC) val cmd = fn env => refineSequents (SOME name, sequents' env, script' env) - val result : elab_val = fn env => (ISyn.DATA_INFO (decl' env), Ty.DATA_INFO arity) + val result : elab_val = fn env => (ISyn.DATA_INFO (decl' env, arity), Ty.DATA_INFO arity) val resultAbs = elabBind (cmd, x, elabRet (elabAbs (elabMetas psi, result))) in elabNu (psi, resultAbs) diff --git a/src/redprl/metalanguage/evaluate.sml b/src/redprl/metalanguage/evaluate.sml index e083c55e7..339198d84 100644 --- a/src/redprl/metalanguage/evaluate.sml +++ b/src/redprl/metalanguage/evaluate.sml @@ -55,19 +55,13 @@ struct Err.raiseError @@ Err.GENERIC [Fpp.text "internal error: theoremSpec caled on non-theorem"] - fun dataDeclArgumentLen env (opid : MlId.t) = - let - val Sem.ABS (Sem.METAS psi, Sem.DATA_INFO _) = Sem.lookup env opid - in - List.length psi - end - fun dataDeclInfo env (opid : MlId.t) args = let - val Sem.ABS (Sem.METAS psi, Sem.DATA_INFO info) = Sem.lookup env opid - val rho = makeSubst (psi, args) + val Sem.ABS (Sem.METAS psi, Sem.DATA_INFO (info, precomputedVls)) = Sem.lookup env opid + val (declArgs, otherArgs) = ListUtil.splitAt (args, List.length psi) + val rho = makeSubst (psi, declArgs) in - Tm.substMetaenv rho info + (declArgs, (Tm.substMetaenv rho info, precomputedVls), otherArgs) end fun unfoldOpid env (opid : MlId.t) args = @@ -252,7 +246,7 @@ struct | Syn.TERM abt => Sem.TERM (Sem.term env abt) - | Syn.DATA_INFO abt => - Sem.DATA_INFO (Sem.term env abt) + | Syn.DATA_INFO (abt, arity) => + Sem.DATA_INFO (Sem.term env abt, arity) end diff --git a/src/redprl/metalanguage/semantics.sig b/src/redprl/metalanguage/semantics.sig index e83ce6350..463a26421 100644 --- a/src/redprl/metalanguage/semantics.sig +++ b/src/redprl/metalanguage/semantics.sig @@ -10,7 +10,7 @@ sig datatype value = THUNK of env * syn_cmd | THM of jdg * Tm.abs - | DATA_INFO of term (* XXX Seriously, we should have something better. -favonia *) + | DATA_INFO of term * InductiveSpec.precomputed_valences (* XXX Seriously, we should have something better. -favonia *) | TERM of term | ABS of value * value | METAS of metas diff --git a/src/redprl/metalanguage/semantics.sml b/src/redprl/metalanguage/semantics.sml index ca7b57968..1a80770e1 100644 --- a/src/redprl/metalanguage/semantics.sml +++ b/src/redprl/metalanguage/semantics.sml @@ -12,7 +12,7 @@ struct datatype value = THUNK of env * syn_cmd | THM of jdg * Tm.abs - | DATA_INFO of term + | DATA_INFO of term * InductiveSpec.precomputed_valences | TERM of term | ABS of value * value | METAS of metas @@ -60,7 +60,7 @@ struct | ABS (METAS psi, s) => ABS (METAS psi, go (List.foldr (fn ((X, _), ren) => Metavar.Ctx.remove ren X) ren psi) s) | METAS psi => METAS (List.map (fn (X, vl) => (Option.getOpt (Metavar.Ctx.find ren X, X), vl)) psi) | NIL => NIL - | DATA_INFO info => DATA_INFO (Tm.renameMetavars ren info) + | DATA_INFO (info, arity) => DATA_INFO (Tm.renameMetavars ren info, arity) in go ren s end diff --git a/src/redprl/metalanguage/syntax.sml b/src/redprl/metalanguage/syntax.sml index 53285a126..2e66cad24 100644 --- a/src/redprl/metalanguage/syntax.sml +++ b/src/redprl/metalanguage/syntax.sml @@ -63,7 +63,7 @@ struct | ABS of value * value | METAS of metas | TERM of term - | DATA_INFO of term + | DATA_INFO of term * InductiveSpec.precomputed_valences and cmd = BIND of cmd * id * cmd diff --git a/src/redprl/metalanguage/type.sig b/src/redprl/metalanguage/type.sig index 6edefd583..597aa2796 100644 --- a/src/redprl/metalanguage/type.sig +++ b/src/redprl/metalanguage/type.sig @@ -10,7 +10,7 @@ struct | THM of sort | ABS of valence list * vty | METAS of valence list - | DATA_INFO of InductiveSpec.precomputedArity + | DATA_INFO of InductiveSpec.precomputed_valences (* TODO: | SUM of (string * vty) list *) diff --git a/src/redprl/metalanguage/type.sml b/src/redprl/metalanguage/type.sml index dca4b901f..88b3bb4a4 100644 --- a/src/redprl/metalanguage/type.sml +++ b/src/redprl/metalanguage/type.sml @@ -16,7 +16,7 @@ struct | (ABS _, _) => false | (METAS vls0, METAS vls1) => vls0 = vls1 | (METAS _, _) => false - | (DATA_INFO ar0, DATA_INFO ar1) => InductiveSpec.eqPrecomputedArity (ar0, ar1) + | (DATA_INFO vls0, DATA_INFO vls1) => InductiveSpec.eqPrecomputedValences (vls0, vls1) | (DATA_INFO _, _) => false and eqCty = diff --git a/src/redprl/mini_signature.sig b/src/redprl/mini_signature.sig index fdb7ae705..33c862756 100644 --- a/src/redprl/mini_signature.sig +++ b/src/redprl/mini_signature.sig @@ -14,8 +14,7 @@ sig val isTheorem : sign -> opid -> bool - (* the length function is needed because we allow the user to write - * the arguments to the type and the ones to the constructors in the same list. *) - val dataDeclArgumentLen : sign -> opid -> int - val dataDeclInfo : sign -> opid -> abt RedPrlAbt.bview list -> abt + (* TODO explain the following function to someone other than favonia. *) + val dataDeclInfo : sign -> opid -> abt RedPrlAbt.bview list -> + abt RedPrlAbt.bview list * (abt * InductiveSpec.precomputed_valences) * abt RedPrlAbt.bview list end