diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 593b6db07..d40455228 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -8,7 +8,7 @@ module GF.Compile.Compute.Concrete , EvalM, runEvalM, evalError , eval, apply, force, value2term, patternMatch , newThunk, newEvaluatedThunk - , newResiduation, newNarrowing + , newResiduation, newNarrowing, getVariables , getRef , getResDef, getInfo, getAllParamValues ) where @@ -387,16 +387,25 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 where bind gr k mt r s m [] = return (Success r) bind gr k mt r s m ((p, ctxt):ps) = do - tnks <- mapM (\(_,_,ty) -> newSTRef (Narrowing 0 ty)) ctxt + (mt',tnks) <- mkArgs mt ctxt let v = VApp (m,p) tnks writeSTRef i (Evaluated v) res <- case ki v of - EvalM f -> f gr k mt r + EvalM f -> f gr k mt' r writeSTRef i s case res of Fail msg -> return (Fail msg) Success r -> bind gr k mt r s m ps + mkArgs mt [] = return (mt,[]) + mkArgs mt ((_,_,ty):ctxt) = do + let i = case Map.maxViewWithKey mt of + Just ((i,_),_) -> i+1 + _ -> 0 + tnk <- newSTRef (Narrowing i ty) + (mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt + return (mt,tnk:tnks) + value2term i (VApp q tnks) = foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (QC q) tnks value2term i (VMeta m env tnks) = do @@ -619,6 +628,22 @@ newNarrowing i ty = EvalM $ \gr k mt r -> Nothing -> do tnk <- newSTRef (Narrowing i ty) k tnk (Map.insert i tnk mt) r +getVariables :: EvalM s [(LVar,LIndex)] +getVariables = EvalM $ \gr k mt r -> do + ps <- metas2params gr (Map.elems mt) + k ps mt r + where + metas2params gr [] = return [] + metas2params gr (tnk:tnks) = do + st <- readSTRef tnk + case st of + Narrowing i ty -> do let range = case allParamValues gr ty of + Ok ts -> length ts + Bad msg -> error msg + params <- metas2params gr tnks + return ((i,range):params) + _ -> metas2params gr tnks + getRef tnk = EvalM $ \gr k mt r -> readSTRef tnk >>= \st -> k st mt r force tnk = EvalM $ \gr k mt r -> do diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs index 80d63bbfb..1845fb472 100644 --- a/src/compiler/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/GF/Compile/GeneratePMCFG.hs @@ -52,7 +52,8 @@ pmcfgForm gr t ctxt ty = lins <- mapM str2lin lins (r,rs,_) <- compute params args <- zipWithM tnk2lparam args ctxt - return (Production args (LParam r rs) (reverse lins)) + vars <- getVariables + return (Production vars args (LParam r rs) (reverse lins)) where tnk2lparam tnk (_,_,ty) = do v <- force tnk diff --git a/src/compiler/GF/Grammar/Binary.hs b/src/compiler/GF/Grammar/Binary.hs index 782fcdae1..bba7e9f82 100644 --- a/src/compiler/GF/Grammar/Binary.hs +++ b/src/compiler/GF/Grammar/Binary.hs @@ -112,8 +112,8 @@ instance Binary PArg where get = get >>= \(x,y) -> return (PArg x y) instance Binary Production where - put (Production args res rules) = put (args,res,rules) - get = get >>= \(args,res,rules) -> return (Production args res rules) + put (Production ps args res rules) = put (ps,args,res,rules) + get = get >>= \(ps,args,res,rules) -> return (Production ps args res rules) instance Binary Info where put (AbsCat x) = putWord8 0 >> put x diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs index bdb510060..aa9b109a5 100644 --- a/src/compiler/GF/Grammar/Printer.hs +++ b/src/compiler/GF/Grammar/Printer.hs @@ -158,8 +158,11 @@ ppJudgement q (id, AnyInd cann mid) = Internal -> "ind" <+> id <+> '=' <+> (if cann then pp "canonical" else empty) <+> mid <+> ';' _ -> empty -ppPmcfgRule id arg_cats res_cat (Production args res lins) = +ppPmcfgRule id arg_cats res_cat (Production vars args res lins) = pp id <+> (':' <+> + (if null vars + then empty + else "∀{" <> hsep (punctuate ',' [ppLVar v <> '<' <> m | (v,m) <- vars]) <> '}' <+> '.') <+> (if null args then empty else hsep (intersperse (pp '*') (zipWith ppPArg arg_cats args)) <+> "->") <+> diff --git a/src/runtime/c/pgf/data.cxx b/src/runtime/c/pgf/data.cxx index 57741e3bd..660ac2dee 100644 --- a/src/runtime/c/pgf/data.cxx +++ b/src/runtime/c/pgf/data.cxx @@ -86,7 +86,9 @@ void PgfConcrLin::release(ref lin) PgfDB::free(lin->args); for (size_t i = 0; i < lin->res->len; i++) { - PgfDB::free(*vector_elem(lin->res, i)); + ref res = *vector_elem(lin->res, i); + PgfDB::free(res->vars); + PgfDB::free(res); } PgfDB::free(lin->res); diff --git a/src/runtime/c/pgf/data.h b/src/runtime/c/pgf/data.h index 3d708a12c..441f6cb4d 100644 --- a/src/runtime/c/pgf/data.h +++ b/src/runtime/c/pgf/data.h @@ -123,10 +123,20 @@ struct PGF_INTERNAL_DECL PgfLParam { } terms[]; }; +struct PGF_INTERNAL_DECL PgfVariableRange { + size_t var; + size_t range; +}; + struct PGF_INTERNAL_DECL PgfPArg { ref param; }; +struct PGF_INTERNAL_DECL PgfPResult { + ref> vars; + PgfLParam param; +}; + typedef object PgfSymbol; struct PGF_INTERNAL_DECL PgfSymbolCat { @@ -202,7 +212,7 @@ struct PGF_INTERNAL_DECL PgfConcrLin { ref absfun; ref> args; - ref>> res; + ref>> res; ref>>> seqs; PgfText name; diff --git a/src/runtime/c/pgf/pgf.cxx b/src/runtime/c/pgf/pgf.cxx index c81c32db0..c62b01b4e 100644 --- a/src/runtime/c/pgf/pgf.cxx +++ b/src/runtime/c/pgf/pgf.cxx @@ -821,6 +821,13 @@ PgfText *pgf_print_lin_sig_internal(object o, size_t i) printer.efun(&lin->name); printer.puts(" : "); + ref res = *vector_elem(lin->res, i); + + if (res->vars != 0) { + printer.lvar_ranges(res->vars); + printer.puts(" . "); + } + size_t n_args = lin->args->len / lin->res->len; for (size_t j = 0; j < n_args; j++) { if (j > 0) @@ -835,7 +842,7 @@ PgfText *pgf_print_lin_sig_internal(object o, size_t i) printer.efun(&ty->name); printer.puts("("); - printer.lparam(*vector_elem(lin->res, i)); + printer.lparam(ref::from_ptr(&res->param)); printer.puts(")"); return printer.get_text(); @@ -1198,6 +1205,7 @@ void pgf_drop_concrete(PgfDB *db, PgfRevision revision, class PGF_INTERNAL PgfLinBuilder : public PgfLinBuilderIface { ref lin; + size_t var_index; size_t arg_index; size_t res_index; size_t seq_index; @@ -1222,8 +1230,8 @@ public: ref> args = vector_new(n_prods*absfun->type->hypos->len); - ref>> res = - vector_new>(n_prods); + ref>> res = + vector_new>(n_prods); ref>>> seqs = vector_new>>(n_prods*lincat->fields->len); @@ -1235,6 +1243,7 @@ public: lin->res = res; lin->seqs = seqs; + this->var_index = 0; this->arg_index = 0; this->res_index = 0; this->seq_index = 0; @@ -1254,11 +1263,12 @@ public: PGF_API_BEGIN { if (res_index >= lin->res->len) throw pgf_error(builder_error_msg); + var_index = 0; *vector_elem(lin->res, res_index) = 0; } PGF_API_END } - void add_argument(size_t i0, size_t n_terms, size_t *terms, PgfExn *err) + void add_argument(size_t n_hypos, size_t i0, size_t n_terms, size_t *terms, PgfExn *err) { if (err->type != PGF_EXN_NONE) return; @@ -1283,7 +1293,7 @@ public: } PGF_API_END } - void set_result(size_t i0, size_t n_terms, size_t *terms, PgfExn *err) + void set_result(size_t n_vars, size_t i0, size_t n_terms, size_t *terms, PgfExn *err) { if (err->type != PGF_EXN_NONE) return; @@ -1292,16 +1302,45 @@ public: if (res_index >= lin->res->len) throw pgf_error(builder_error_msg); - ref param = PgfDB::malloc(n_terms*2*sizeof(size_t)); - param->i0 = i0; - param->n_terms = n_terms; + ref> vars = + (n_vars > 0) ? vector_new(n_vars) + : 0; + + ref res = PgfDB::malloc(n_terms*2*sizeof(size_t)); + res->vars = vars; + res->param.i0 = i0; + res->param.n_terms = n_terms; for (size_t i = 0; i < n_terms; i++) { - param->terms[i].factor = terms[2*i]; - param->terms[i].var = terms[2*i+1]; + res->param.terms[i].factor = terms[2*i]; + res->param.terms[i].var = terms[2*i+1]; } - *vector_elem(lin->res, res_index) = param; + *vector_elem(lin->res, res_index) = res; + } PGF_API_END + } + + void add_variable(size_t var, size_t range, PgfExn *err) + { + if (err->type != PGF_EXN_NONE) + return; + + PGF_API_BEGIN { + if (res_index >= lin->res->len) + throw pgf_error(builder_error_msg); + + ref res = + *vector_elem(lin->res, res_index); + + if (res->vars == 0 || var_index >= res->vars->len) + throw pgf_error(builder_error_msg); + + ref var_range = + vector_elem(res->vars, var_index); + var_range->var = var; + var_range->range = range; + + var_index++; } PGF_API_END } @@ -1623,7 +1662,9 @@ public: PgfDB::free(lin->args); for (size_t i = 0; i < res_index; i++) { - PgfDB::free(*vector_elem(lin->res, i)); + ref res = *vector_elem(lin->res, i); + PgfDB::free(res->vars); + PgfDB::free(res); } PgfDB::free(lin->res); diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h index 85a8fa6de..13accd30d 100644 --- a/src/runtime/c/pgf/pgf.h +++ b/src/runtime/c/pgf/pgf.h @@ -487,8 +487,9 @@ void pgf_drop_lincat(PgfDB *db, PgfConcrRevision revision, #ifdef __cplusplus struct PgfLinBuilderIface { virtual void start_production(PgfExn *err)=0; - virtual void add_argument(size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; - virtual void set_result(size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; + virtual void add_argument(size_t n_hypos, size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; + virtual void set_result(size_t n_vars, size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; + virtual void add_variable(size_t var, size_t range, PgfExn *err)=0; virtual void start_sequence(size_t n_syms, PgfExn *err)=0; virtual void add_symcat(size_t d, size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; virtual void add_symlit(size_t d, size_t i0, size_t n_terms, size_t *terms, PgfExn *err)=0; @@ -516,8 +517,9 @@ typedef struct PgfLinBuilderIface PgfLinBuilderIface; typedef struct { void (*start_production)(PgfLinBuilderIface *this, PgfExn *err); - void (*add_argument)(PgfLinBuilderIface *this, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); - void (*set_result)(PgfLinBuilderIface *this, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); + void (*add_argument)(PgfLinBuilderIface *this, size_t n_hypos, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); + void (*set_result)(PgfLinBuilderIface *this, size_t n_vars, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); + void (*add_variable)(PgfLinBuilderIface *this, size_t var, size_t range, PgfExn *err); void (*start_sequence)(PgfLinBuilderIface *this, size_t n_syms, PgfExn *err); void (*add_symcat)(PgfLinBuilderIface *this, size_t d, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); void (*add_symlit)(PgfLinBuilderIface *this, size_t d, size_t i0, size_t n_terms, size_t *terms, PgfExn *err); diff --git a/src/runtime/c/pgf/printer.cxx b/src/runtime/c/pgf/printer.cxx index 95120860e..d65cc6b83 100644 --- a/src/runtime/c/pgf/printer.cxx +++ b/src/runtime/c/pgf/printer.cxx @@ -445,6 +445,18 @@ void PgfPrinter::parg(ref ty, ref parg) puts(")"); } +void PgfPrinter::lvar(size_t var) +{ + char vars[] = "ijklmnopqr"; + size_t i = var / sizeof(vars); + size_t j = var % sizeof(vars); + + if (i == 0) + nprintf(32,"%c",vars[j]); + else + nprintf(32,"%c%ld",vars[j],i); +} + void PgfPrinter::lparam(ref lparam) { if (lparam->i0 != 0 || lparam->n_terms == 0) @@ -457,17 +469,22 @@ void PgfPrinter::lparam(ref lparam) puts("*"); } - char vars[] = "ijklmnopqr"; - size_t i = lparam->terms[k].var / sizeof(vars); - size_t j = lparam->terms[k].var % sizeof(vars); - - if (i == 0) - nprintf(32,"%c",vars[j]); - else - nprintf(32,"%c%ld",vars[j],i); + lvar(lparam->terms[k].var); } } +void PgfPrinter::lvar_ranges(ref> vars) +{ + puts("∀{"); + for (size_t i = 0; i < vars->len; i++) { + if (i > 0) + puts(", "); + lvar(vars->data[i].var); + nprintf(32,"<%ld",vars->data[i].range); + } + puts("}"); +} + void PgfPrinter::symbol(PgfSymbol sym) { switch (ref::get_tag(sym)) { diff --git a/src/runtime/c/pgf/printer.h b/src/runtime/c/pgf/printer.h index 185aa32b1..4cfdf0b81 100644 --- a/src/runtime/c/pgf/printer.h +++ b/src/runtime/c/pgf/printer.h @@ -51,7 +51,9 @@ public: void hypo(PgfTypeHypo *hypo, int prio); void parg(ref ty, ref parg); + void lvar(size_t var); void lparam(ref lparam); + void lvar_ranges(ref> vars); void symbol(PgfSymbol sym); void symbols(ref> syms); diff --git a/src/runtime/c/pgf/reader.cxx b/src/runtime/c/pgf/reader.cxx index 9743c78e7..c3938f589 100644 --- a/src/runtime/c/pgf/reader.cxx +++ b/src/runtime/c/pgf/reader.cxx @@ -388,11 +388,44 @@ ref PgfReader::read_lparam() return lparam; } +void PgfReader::read_variable_range(ref var_info) +{ + var_info->var = read_int(); + var_info->range = read_int(); +} + void PgfReader::read_parg(ref parg) { parg->param = read_lparam(); } +ref PgfReader::read_presult() +{ + ref> vars = 0; + size_t n_vars = read_len(); + if (n_vars > 0) { + vars = vector_new(n_vars); + for (size_t i = 0; i < n_vars; i++) { + read_variable_range(vector_elem(vars,i)); + } + } + + size_t i0 = read_int(); + size_t n_terms = read_len(); + ref res = + PgfDB::malloc(n_terms*sizeof(PgfLParam::terms[0])); + res->vars = vars; + res->param.i0 = i0; + res->param.n_terms = n_terms; + + for (size_t i = 0; i < n_terms; i++) { + res->param.terms[i].factor = read_int(); + res->param.terms[i].var = read_int(); + } + + return res; +} + template ref PgfReader::read_symbol_idx() { @@ -506,7 +539,7 @@ ref PgfReader::read_lin() lin->ref_count = 1; lin->absfun = namespace_lookup(abstract->funs, &lin->name); lin->args = read_vector(&PgfReader::read_parg); - lin->res = read_vector(&PgfReader::read_lparam); + lin->res = read_vector(&PgfReader::read_presult2); lin->seqs = read_vector(&PgfReader::read_seq2); return lin; } diff --git a/src/runtime/c/pgf/reader.h b/src/runtime/c/pgf/reader.h index 85e48be82..ad3fbf330 100644 --- a/src/runtime/c/pgf/reader.h +++ b/src/runtime/c/pgf/reader.h @@ -65,7 +65,9 @@ public: ref read_lincat(); ref read_lparam(); + void read_variable_range(ref var_info); void read_parg(ref parg); + ref read_presult(); PgfSymbol read_symbol(); ref read_lin(); ref read_printname(); @@ -85,6 +87,7 @@ private: void read_lparam(ref> r) { auto lparam = read_lparam(); *r = lparam; }; void read_symbol2(ref r) { auto sym = read_symbol(); *r = sym; }; void read_seq2(ref>> r) { auto seq = read_vector(&PgfReader::read_symbol2); *r = seq; } + void read_presult2(ref> r) { auto res = read_presult(); *r = res; } template ref read_symbol_idx(); diff --git a/src/runtime/c/pgf/writer.cxx b/src/runtime/c/pgf/writer.cxx index cd18a7e83..7ad272fdc 100644 --- a/src/runtime/c/pgf/writer.cxx +++ b/src/runtime/c/pgf/writer.cxx @@ -336,6 +336,12 @@ void PgfWriter::write_lincat(ref lincat) write_vector(lincat->fields, &PgfWriter::write_text); } +void PgfWriter::write_variable_range(ref var) +{ + write_int(var->var); + write_int(var->range); +} + void PgfWriter::write_lparam(ref lparam) { write_int(lparam->i0); @@ -351,6 +357,15 @@ void PgfWriter::write_parg(ref parg) write_lparam(parg->param); } +void PgfWriter::write_presult(ref pres) +{ + if (pres->vars != 0) + write_vector(pres->vars, &PgfWriter::write_variable_range); + else + write_len(0); + write_lparam(ref::from_ptr(&pres->param)); +} + void PgfWriter::write_symbol(PgfSymbol sym) { auto tag = ref::get_tag(sym); @@ -411,7 +426,7 @@ void PgfWriter::write_lin(ref lin) { write_name(&lin->name); write_vector(lin->args, &PgfWriter::write_parg); - write_vector(lin->res, &PgfWriter::write_lparam); + write_vector(lin->res, &PgfWriter::write_presult); write_vector(lin->seqs, &PgfWriter::write_seq); } diff --git a/src/runtime/c/pgf/writer.h b/src/runtime/c/pgf/writer.h index b0417a171..fda06dd33 100644 --- a/src/runtime/c/pgf/writer.h +++ b/src/runtime/c/pgf/writer.h @@ -39,8 +39,10 @@ public: void write_abstract(ref abstract); void write_lincat(ref lincat); + void write_variable_range(ref var); void write_lparam(ref lparam); void write_parg(ref linarg); + void write_presult(ref linres); void write_symbol(PgfSymbol sym); void write_seq(ref> seq); void write_lin(ref lin); @@ -58,6 +60,7 @@ private: void write_lparam(ref> r) { write_lparam(*r); }; void write_seq(ref>> r) { write_seq(*r); }; void write_symbol(ref r) { write_symbol(*r); }; + void write_presult(ref> r) { write_presult(*r); }; FILE *out; ref abstract; diff --git a/src/runtime/haskell/PGF2/FFI.hsc b/src/runtime/haskell/PGF2/FFI.hsc index a1196f92a..f3bd82365 100644 --- a/src/runtime/haskell/PGF2/FFI.hsc +++ b/src/runtime/haskell/PGF2/FFI.hsc @@ -179,7 +179,7 @@ foreign import ccall "dynamic" callLinBuilder1 :: Dynamic (Ptr PgfLinBuilderIfac foreign import ccall "dynamic" callLinBuilder2 :: Dynamic (Ptr PgfLinBuilderIface -> CSize -> CSize -> Ptr PgfExn -> IO ()) -foreign import ccall "dynamic" callLinBuilder3 :: Dynamic (Ptr PgfLinBuilderIface -> CSize -> CSize -> Ptr CSize -> Ptr PgfExn -> IO ()) +foreign import ccall "dynamic" callLinBuilder3 :: Dynamic (Ptr PgfLinBuilderIface -> CSize -> CSize -> CSize -> Ptr CSize -> Ptr PgfExn -> IO ()) foreign import ccall "dynamic" callLinBuilder4 :: Dynamic (Ptr PgfLinBuilderIface -> CSize -> CSize -> CSize -> Ptr CSize -> Ptr PgfExn -> IO ()) diff --git a/src/runtime/haskell/PGF2/Transactions.hsc b/src/runtime/haskell/PGF2/Transactions.hsc index ea23bac89..cd25c2aac 100644 --- a/src/runtime/haskell/PGF2/Transactions.hsc +++ b/src/runtime/haskell/PGF2/Transactions.hsc @@ -212,7 +212,7 @@ data Symbol data PArg = PArg [(LIndex,LIndex)] {-# UNPACK #-} !LParam deriving (Eq,Show) -data Production = Production [PArg] LParam [[Symbol]] +data Production = Production [(LVar,LIndex)] [PArg] LParam [[Symbol]] deriving (Eq,Show) createLincat :: Cat -> [String] -> Transaction Concr () @@ -253,14 +253,17 @@ createLin name prods = Transaction $ \c_db c_abstr c_revision c_exn -> build _ c_builder c_exn = do vtbl <- (#peek PgfLinBuilderIface, vtbl) c_builder - forM_ prods c_exn $ \(Production args res seqs) -> do + forM_ prods c_exn $ \(Production vars args res seqs) -> do fun <- (#peek PgfLinBuilderIfaceVtbl, start_production) vtbl callLinBuilder0 fun c_builder c_exn fun <- (#peek PgfLinBuilderIfaceVtbl, add_argument) vtbl - forM_ args c_exn $ \(PArg _ param) -> - callLParam (callLinBuilder3 fun c_builder) param c_exn + forM_ args c_exn $ \(PArg hypos param) -> + callLParam (callLinBuilder3 fun c_builder (fromIntegral (length hypos))) param c_exn fun <- (#peek PgfLinBuilderIfaceVtbl, set_result) vtbl - callLParam (callLinBuilder3 fun c_builder) res c_exn + callLParam (callLinBuilder3 fun c_builder (fromIntegral (length vars))) res c_exn + fun <- (#peek PgfLinBuilderIfaceVtbl, add_variable) vtbl + forM_ vars c_exn $ \(v,r) -> + callLinBuilder2 fun c_builder (fromIntegral v) (fromIntegral r) c_exn forM_ seqs c_exn $ \syms -> do fun <- (#peek PgfLinBuilderIfaceVtbl, start_sequence) vtbl callLinBuilder1 fun c_builder (fromIntegral (length syms)) c_exn diff --git a/src/runtime/haskell/tests/basic.pgf b/src/runtime/haskell/tests/basic.pgf index e718f7a2f..eacd46800 100644 Binary files a/src/runtime/haskell/tests/basic.pgf and b/src/runtime/haskell/tests/basic.pgf differ diff --git a/src/runtime/haskell/tests/basic.pmcfg b/src/runtime/haskell/tests/basic.pmcfg index ab7574652..c66799e0b 100644 --- a/src/runtime/haskell/tests/basic.pmcfg +++ b/src/runtime/haskell/tests/basic.pmcfg @@ -19,10 +19,10 @@ concrete basic_cnc { lincat S = [ "" ] - lin c : N(j) -> S(0) = [ + lin c : ∀{j<2} . N(j) -> S(0) = [ <0,0> ] - lin ind : P(0) * P(0) * N(j) -> P(0) = [ + lin ind : ∀{j<2} . P(0) * P(0) * N(j) -> P(0) = [ ] lin s : N(0) -> N(0) = [ <0,0> "+" "1"