From f0bc412fa3b9f3f2b6131fe5322d4916730efac1 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Fri, 13 Feb 2015 15:50:51 +0000 Subject: Actually use new dependency information in generation of lem/etc. Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass --- language/l2.lem | 3 ++- language/l2.ml | 3 ++- language/l2.ott | 6 ++++-- 3 files changed, 8 insertions(+), 4 deletions(-) (limited to 'language') diff --git a/language/l2.lem b/language/l2.lem index a4bc2545..86b947b5 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -256,7 +256,8 @@ and exp_aux 'a = (* Expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) - | E_internal_exp of annot 'a (* This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints *) + | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) and exp 'a = | E_aux of (exp_aux 'a) * annot 'a diff --git a/language/l2.ml b/language/l2.ml index ab0e7b66..dc96020d 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -264,7 +264,8 @@ type | E_assign of 'a lexp * 'a exp (* imperative assignment *) | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) - | E_internal_exp of 'a annot (* This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints *) + | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *) and 'a exp = E_aux of 'a exp_aux * 'a annot diff --git a/language/l2.ott b/language/l2.ott index f9309f99..ab3e2a88 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -639,8 +639,10 @@ exp :: 'E_' ::= {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }} | ( exp ) :: S :: paren {{ ichlo [[exp]] }} - | ( annot ) exp :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} - | annot :: :: internal_exp {{ com This is an internal use of an nexp (in the annot) for passing length information after resolution of constraints }} + | ( annot ) exp :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} + | annot :: :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} + | annot , annot' :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} + lexp :: 'LEXP_' ::= {{ com lvalue expression }} -- cgit v1.2.3