generate and store the ranges for all linearization rules

This commit is contained in:
krangelov
2021-11-26 14:05:03 +01:00
parent 794e15aca3
commit 4a68ea93b3
18 changed files with 203 additions and 43 deletions

View File

@@ -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

View File

@@ -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

View File

@@ -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

View File

@@ -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)) <+> "->") <+>

View File

@@ -86,7 +86,9 @@ void PgfConcrLin::release(ref<PgfConcrLin> lin)
PgfDB::free(lin->args);
for (size_t i = 0; i < lin->res->len; i++) {
PgfDB::free(*vector_elem(lin->res, i));
ref<PgfPResult> res = *vector_elem(lin->res, i);
PgfDB::free(res->vars);
PgfDB::free(res);
}
PgfDB::free(lin->res);

View File

@@ -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<PgfLParam> param;
};
struct PGF_INTERNAL_DECL PgfPResult {
ref<Vector<PgfVariableRange>> vars;
PgfLParam param;
};
typedef object PgfSymbol;
struct PGF_INTERNAL_DECL PgfSymbolCat {
@@ -202,7 +212,7 @@ struct PGF_INTERNAL_DECL PgfConcrLin {
ref<PgfAbsFun> absfun;
ref<Vector<PgfPArg>> args;
ref<Vector<ref<PgfLParam>>> res;
ref<Vector<ref<PgfPResult>>> res;
ref<Vector<ref<Vector<PgfSymbol>>>> seqs;
PgfText name;

View File

@@ -821,6 +821,13 @@ PgfText *pgf_print_lin_sig_internal(object o, size_t i)
printer.efun(&lin->name);
printer.puts(" : ");
ref<PgfPResult> 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<PgfLParam>::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<PgfConcrLin> lin;
size_t var_index;
size_t arg_index;
size_t res_index;
size_t seq_index;
@@ -1222,8 +1230,8 @@ public:
ref<Vector<PgfPArg>> args =
vector_new<PgfPArg>(n_prods*absfun->type->hypos->len);
ref<Vector<ref<PgfLParam>>> res =
vector_new<ref<PgfLParam>>(n_prods);
ref<Vector<ref<PgfPResult>>> res =
vector_new<ref<PgfPResult>>(n_prods);
ref<Vector<ref<Vector<PgfSymbol>>>> seqs =
vector_new<ref<Vector<PgfSymbol>>>(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<PgfLParam> param = PgfDB::malloc<PgfLParam>(n_terms*2*sizeof(size_t));
param->i0 = i0;
param->n_terms = n_terms;
ref<Vector<PgfVariableRange>> vars =
(n_vars > 0) ? vector_new<PgfVariableRange>(n_vars)
: 0;
ref<PgfPResult> res = PgfDB::malloc<PgfPResult>(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<PgfPResult> res =
*vector_elem(lin->res, res_index);
if (res->vars == 0 || var_index >= res->vars->len)
throw pgf_error(builder_error_msg);
ref<PgfVariableRange> 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<PgfPResult> res = *vector_elem(lin->res, i);
PgfDB::free(res->vars);
PgfDB::free(res);
}
PgfDB::free(lin->res);

View File

@@ -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);

View File

@@ -445,6 +445,18 @@ void PgfPrinter::parg(ref<PgfDTyp> ty, ref<PgfPArg> 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<PgfLParam> lparam)
{
if (lparam->i0 != 0 || lparam->n_terms == 0)
@@ -457,17 +469,22 @@ void PgfPrinter::lparam(ref<PgfLParam> 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<Vector<PgfVariableRange>> 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<PgfSymbol>::get_tag(sym)) {

View File

@@ -51,7 +51,9 @@ public:
void hypo(PgfTypeHypo *hypo, int prio);
void parg(ref<PgfDTyp> ty, ref<PgfPArg> parg);
void lvar(size_t var);
void lparam(ref<PgfLParam> lparam);
void lvar_ranges(ref<Vector<PgfVariableRange>> vars);
void symbol(PgfSymbol sym);
void symbols(ref<Vector<PgfSymbol>> syms);

View File

@@ -388,11 +388,44 @@ ref<PgfLParam> PgfReader::read_lparam()
return lparam;
}
void PgfReader::read_variable_range(ref<PgfVariableRange> var_info)
{
var_info->var = read_int();
var_info->range = read_int();
}
void PgfReader::read_parg(ref<PgfPArg> parg)
{
parg->param = read_lparam();
}
ref<PgfPResult> PgfReader::read_presult()
{
ref<Vector<PgfVariableRange>> vars = 0;
size_t n_vars = read_len();
if (n_vars > 0) {
vars = vector_new<PgfVariableRange>(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<PgfPResult> res =
PgfDB::malloc<PgfPResult>(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<class I>
ref<I> PgfReader::read_symbol_idx()
{
@@ -506,7 +539,7 @@ ref<PgfConcrLin> 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;
}

View File

@@ -65,7 +65,9 @@ public:
ref<PgfConcrLincat> read_lincat();
ref<PgfLParam> read_lparam();
void read_variable_range(ref<PgfVariableRange> var_info);
void read_parg(ref<PgfPArg> parg);
ref<PgfPResult> read_presult();
PgfSymbol read_symbol();
ref<PgfConcrLin> read_lin();
ref<PgfConcrPrintname> read_printname();
@@ -85,6 +87,7 @@ private:
void read_lparam(ref<ref<PgfLParam>> r) { auto lparam = read_lparam(); *r = lparam; };
void read_symbol2(ref<PgfSymbol> r) { auto sym = read_symbol(); *r = sym; };
void read_seq2(ref<ref<Vector<PgfSymbol>>> r) { auto seq = read_vector(&PgfReader::read_symbol2); *r = seq; }
void read_presult2(ref<ref<PgfPResult>> r) { auto res = read_presult(); *r = res; }
template<class I>
ref<I> read_symbol_idx();

View File

@@ -336,6 +336,12 @@ void PgfWriter::write_lincat(ref<PgfConcrLincat> lincat)
write_vector(lincat->fields, &PgfWriter::write_text);
}
void PgfWriter::write_variable_range(ref<PgfVariableRange> var)
{
write_int(var->var);
write_int(var->range);
}
void PgfWriter::write_lparam(ref<PgfLParam> lparam)
{
write_int(lparam->i0);
@@ -351,6 +357,15 @@ void PgfWriter::write_parg(ref<PgfPArg> parg)
write_lparam(parg->param);
}
void PgfWriter::write_presult(ref<PgfPResult> pres)
{
if (pres->vars != 0)
write_vector(pres->vars, &PgfWriter::write_variable_range);
else
write_len(0);
write_lparam(ref<PgfLParam>::from_ptr(&pres->param));
}
void PgfWriter::write_symbol(PgfSymbol sym)
{
auto tag = ref<PgfSymbol>::get_tag(sym);
@@ -411,7 +426,7 @@ void PgfWriter::write_lin(ref<PgfConcrLin> 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);
}

View File

@@ -39,8 +39,10 @@ public:
void write_abstract(ref<PgfAbstr> abstract);
void write_lincat(ref<PgfConcrLincat> lincat);
void write_variable_range(ref<PgfVariableRange> var);
void write_lparam(ref<PgfLParam> lparam);
void write_parg(ref<PgfPArg> linarg);
void write_presult(ref<PgfPResult> linres);
void write_symbol(PgfSymbol sym);
void write_seq(ref<Vector<PgfSymbol>> seq);
void write_lin(ref<PgfConcrLin> lin);
@@ -58,6 +60,7 @@ private:
void write_lparam(ref<ref<PgfLParam>> r) { write_lparam(*r); };
void write_seq(ref<ref<Vector<PgfSymbol>>> r) { write_seq(*r); };
void write_symbol(ref<PgfSymbol> r) { write_symbol(*r); };
void write_presult(ref<ref<PgfPResult>> r) { write_presult(*r); };
FILE *out;
ref<PgfAbstr> abstract;

View File

@@ -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 ())

View File

@@ -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

Binary file not shown.

View File

@@ -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"