Cleanup repository by removing old and generated files

Rename l2.ott to sail.ott

1 files changed, 0 insertions, 451 deletions

diff --git a/language/sil.ott b/language/sil.ott
deleted file mode 100644
index 40adfc4d..00000000
--- a/language/sil.ott
+++ /dev/null
@@ -1,451 +0,0 @@
-%%% Sail Intermediate Language %%%
-
-% An attempt to precisely document the subset of sail that the
-% rewriter is capable of re-writing sail into. It is intended to be a
-% strict subset of the Sail AST, and be typecheckable with the full
-% typechecker.
-%
-% Notably, it lacks:
-% - Special (bit)vector syntax.
-% - Complex l-values.
-% - Existential types.
-% - Polymorphism, of any kind.
-
-indexvar n , m , i , j ::=
-  {{ phantom }}
-  {{ com Index variables for meta-lists }}
-
-metavar num,numZero,numOne ::=
-  {{ phantom }}
-  {{ lex numeric }}
-  {{ ocaml int }}
-  {{ hol num }}
-  {{ lem integer }}
-  {{ com Numeric literals }}
-
-metavar nat ::=
-  {{ phantom }}
-  {{ ocaml int }}
-  {{ lex numeric }}
-  {{ lem nat }}
-
-metavar string ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com String literals }}
-
-metavar real ::=
-  {{ phantom }}
-  {{ ocaml string }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com Real number literal }}
-
-embed
-{{ ocaml
-
-type text = string
-
-type l = Parse_ast.l
-
-type 'a annot = l * 'a
-
-type loop = While | Until
-
-}}
-
-embed
-{{ lem
-open import Pervasives
-open import Pervasives_extra
-open import Map
-open import Maybe
-open import Set_extra
-
-type l =
-  | Unknown
-  | Int of string * maybe l (*internal types, functions*)
-  | Range of string * nat * nat * nat * nat
-  | Generated of l (*location for a generated node, where l is the location of the closest original source*)
-
-type annot 'a = l * 'a
-
-val duplicates : forall 'a. list 'a -> list 'a
-
-val set_from_list : forall 'a. list 'a -> set 'a
-
-val subst : forall 'a. list 'a -> list 'a -> bool
-
-type loop = While | Until
-
-}}
-
-metavar x , y , z ::=
-  {{ ocaml text }}
-  {{ lem string }}
-  {{ hol string }}
-  {{ com identifier }}
-  {{ ocamlvar "[[x]]" }}
-  {{ lemvar "[[x]]" }}
-
-grammar
-
-l :: '' ::=                                     {{ phantom }}
-                                                {{ ocaml Parse_ast.l }}
-                                                {{ lem l }}
-                                                {{ hol unit }}
-  {{ com source location }}
-  |                                             :: :: Unknown
-    {{ ocaml Unknown }}
-    {{ lem Unknown }}
-    {{ hol () }}
-
-
-id :: '' ::=
-  {{ com Identifier }}
-  {{ aux _ l }}
-  | x                           :: :: id
-  | ( deinfix x )               :: D :: deIid {{ com remove infix status }}
-
-base_effect :: 'BE_' ::=
-  {{ com effect }}
-  {{ aux _ l }}
-  | rreg                                :: :: rreg   {{ com read register }}
-  | wreg                                :: :: wreg   {{ com write register }}
-  | rmem                                :: :: rmem   {{ com read memory }}
-  | rmemt                               :: :: rmemt  {{ com read memory and tag }}
-  | wmem                                :: :: wmem   {{ com write memory }}
-  | wmea				:: :: eamem  {{ com signal effective address for writing memory }}
-  | exmem                               :: :: exmem  {{ com determine if a store-exclusive (ARM) is going to succeed }}
-  | wmv					:: :: wmv    {{ com write memory, sending only value }}
-  | wmvt                                :: :: wmvt   {{ com write memory, sending only value and tag }}
-  | barr                                :: :: barr   {{ com memory barrier }}
-  | depend				:: :: depend {{ com dynamic footprint }}
-  | undef                               :: :: undef  {{ com undefined-instruction exception }}
-  | unspec                              :: :: unspec {{ com unspecified values }}
-  | nondet                              :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }}
-  | escape                              :: :: escape {{ com potential call of  $[[exit]]$ }}
-  | lset                                :: :: lset   {{ com local mutation; not user-writable }}
-  | lret                                :: :: lret   {{ com local return; not user-writable }}
-
-effect :: 'Effect_' ::=
-  {{ com effect set, of kind $[[Effect]]$ }}
-  {{ aux _ l }}
- | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }}
- | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
-   {{ lem (Effect_set [])  }} {{icho [[{}]] }}
- | effect1 u+ .. u+ effectn             :: M :: union {{ com union of sets of effects }} {{ icho [] }}
-   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Types                                                        %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-typ :: 'Typ_' ::=
-  {{ com type expressions, of kind $[[Type]]$ }}
-  {{ aux _ l }}
-  | id                                         :: :: id
-    {{ com defined type }}
-  | typ1 -> typ2 effectkw effect               :: :: fn
-    {{ com Function (first-order only in user code) }}
-  | ( typ1 , .... , typn )                     :: :: tup
-    {{ com Tuple }}
-  | id < typ_arg1 , .. , typ_argn >            :: :: app
-    {{ com type constructor application }}
-
-typ_arg :: 'Typ_arg_' ::=
-  {{ com type constructor arguments of all kinds }}
-  {{ aux _ l }} 
-  | typ        :: :: typ
-
-typquant :: 'TypQ_' ::= 
-  {{ com type quantifiers and constraints}}
-  {{ aux _ l }}
-  | ::  ::  no_forall     {{ com empty }}
-
-typschm :: 'TypSchm_' ::=
-  {{ com type scheme  }}
-  {{ aux _ l }}
-  |  typquant typ :: :: ts
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Type definitions                                             %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::=
-  {{ ocaml TD_aux of type_def_aux * 'a annot }}
-  {{ lem TD_aux of type_def_aux * annot 'a }}
-  | type_def_aux  :: :: aux
-
-type_def_aux  :: 'TD_' ::=
-  {{ com type definition body }}
-  | typedef id = typschm                                                  :: :: abbrev
-    {{ com type abbreviation }} {{ texlong }}
-  | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn }      :: :: record
-    {{ com struct type definition }} {{ texlong }}
-  | typedef id = const union typquant { type_union1 ; ... ; type_unionn } :: :: variant
-    {{ com tagged union type definition}} {{ texlong }}
-  | typedef id = enumerate { id1 ; ... ; idn }                            :: :: enum
-    {{ com enumeration type definition}} {{ texlong }}
-
-% This one is a bit unusual - I think all nexps here must be constant, so replace with num.
-  | typedef  id = register bits [ num : num' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-     :: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-type_union :: 'Tu_' ::=
-  {{ com type union constructors }}
-  {{ aux _ l }}
-  | id                                                  :: :: id
-  | typ id                                              :: :: ty_id
-
-index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} 
-  {{ aux _ l }}
-  | num :: :: 'single'  {{ com single index }}
-  | num1 '..' num2 :: :: range {{ com index range }}
-  | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Literals                                                     %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-lit :: 'L_' ::=
-  {{ com literal constant }}
-  {{ aux _ l }}
-  | ( )                                         :: :: unit  {{ com $() : [[unit]]$ }}
-  | bitzero                                     :: :: zero {{ com $[[bitzero]] : [[bit]]$ }}
-  | bitone                                      :: :: one {{ com $[[bitone]] : [[bit]]$ }}
-  | true                                        :: :: true  {{ com $[[true]] : [[bool]]$ }}
-  | false                                       :: :: false {{ com $[[false]] : [[bool]]$ }}
-  | num                                         :: :: num  {{ com natural number constant }}
-% Need to represent as a function call, e.g. sil#hex_string "0xFFFF".
-%  | hex                                         :: :: hex  {{ com bit vector constant, C-style }}
-%  | bin                                         :: :: bin  {{ com bit vector constant, C-style }}
-  | string                                      :: :: string {{ com string constant }}
-  | undefined					:: :: undef {{ com undefined-value constant }}
-  | real                                        :: :: real {{ com real number }}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Patterns                                                     %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-pat :: 'P_' ::= 
-  {{ com pattern }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | _                                                 :: :: wild
-    {{ com wildcard }}
-  | ( pat as id )                                     :: :: as
-    {{ com named pattern }}
-  | ( typ ) pat                                       :: :: typ
-    {{ com typed pattern }}
-  | id                                                :: :: id
-    {{ com identifier  }}
-  | id ( pat1 , .. , patn )                           :: :: app
-    {{ com union constructor pattern }}
-  | { fpat1 ; ... ; fpatn }                           :: :: record
-    {{ com struct pattern }}
-  | ( pat1 , .... , patn )                            :: :: tup
-    {{ com tuple pattern }}
-  | [|| pat1 , .. , patn ||]	                      :: :: list
-    {{ com list pattern }}
-  | ( pat )                                           :: S :: paren
-    {{ ichlo [[pat]] }}
-  | pat1 '::' pat2                                    :: :: cons
-    {{ com Cons patterns }}
-
-fpat :: 'FP_' ::=
-  {{ com field pattern }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = pat :: :: Fpat
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Expressions                                                  %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-loop :: loop ::= {{ phantom }}
-  | while ::  :: while
-  | until ::  :: until
-
-exp :: 'E_' ::=
-  {{ com expression }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | { exp1 ; ... ; expn }                               :: :: block {{ com sequential block }}
-  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com nondeterministic block }}
-  | id                                                  :: :: id
-    {{ com identifier }}
-  | lit                                                 :: :: lit
-    {{ com literal constant }}
-% Purely an annotation as all casting is resolved by type checker, can
-% be evaluated by simply dropping the type.
-  | ( typ ) exp                                         :: :: cast
-    {{ com cast }}
-  | id ( exp1 , .. , expn )                             :: :: app
-    {{ com function application }}
-  | ( exp1 , .... , expn )                              :: :: tuple
-    {{ com tuple }}
-  | if exp1 then exp2 else exp3                         :: :: if
-    {{ com conditional }}
-  | loop exp1 exp2                                      :: :: loop
-    {{ com while or until loop }}
-  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for
-    {{ com for loop }}
-  | [|| exp1 , ..  , expn ||]                           :: :: list
-    {{ com list }}
-  | exp1 '::' exp2                                      :: :: cons
-    {{ com cons }}
-  | { fexps }                                           :: :: record
-    {{ com struct }}
-  | { exp with fexps }                                  :: :: record_update
-    {{ com functional update of struct }}
-  | exp . id                                            :: :: field
-    {{ com field projection from struct  }}
-  | switch exp { case pexp1  ... case pexpn }           :: :: case
-    {{ com pattern matching }}
-  | letbind in exp                                      :: :: let
-    {{ com let expression }}
-  | lexp := exp                                         :: :: assign
-    {{ com imperative assignment }}
-  | return exp                                          :: :: return
-    {{ com  return $[[exp]]$ from current function }}
-  | exit exp						:: :: exit
-    {{ com halt all current execution }}
-  | value                                               :: I :: value
-    {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
-
-lexp :: 'LEXP_' ::= {{ com lvalue expression }}
-    {{ aux _ annot }} {{ auxparam 'a }}
-    | id                                                  :: :: id
-      {{ com identifier }}
-    | ( typ ) id					  :: :: cast
-      {{ com cast }}
-    | ( lexp0 , .. , lexpn )                              :: :: tup {{ com multiple (non-memory) assignment }}
-% SIL: Not sure how much to rewrite L-expressions.
-%    | lexp [ exp ]                                        :: :: vector  {{ com vector element }}
-%    | lexp [ exp1 '..' exp2 ]                             :: :: vector_range {{ com subvector }}
-%    | lexp . id                                           :: :: field {{ com struct field }}
-
-fexp :: 'FE_' ::=
-  {{ com field expression }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = exp                                   :: :: Fexp
-
-fexps :: 'FES_' ::=
-  {{ com field expression list }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | fexp1 ; ... ; fexpn                        :: :: Fexps
-
-pexp :: 'Pat_' ::=
-  {{ com pattern match }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | pat -> exp                          :: :: exp
-  | pat when exp1 -> exp                :: :: when
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Function definitions                                         %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-tannot_opt :: 'Typ_annot_opt_' ::=
-  {{ com optional type annotation for functions}}
-  {{ aux _ l }} 
-  |                                             :: :: none
-  | typquant typ                                :: :: some 
-
-rec_opt :: 'Rec_' ::=
-  {{ com optional recursive annotation for functions }}
-  {{ aux _ l }}
-  |                                             :: :: nonrec {{ com non-recursive }}
-  | rec                                         :: :: rec {{ com recursive }}
-
-effect_opt :: 'Effect_opt_' ::=
-  {{ com optional effect annotation for functions }}
-  {{ aux _ l }}
-  |                                             :: :: pure {{ com sugar for empty effect set }}
-  | effectkw effect                             :: :: effect
-
-funcl :: 'FCL_' ::=
-  {{ com function clause }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id pat = exp                   :: :: Funcl
-
-fundef :: 'FD_' ::=
-  {{ com function definition}}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }}
-
-letbind :: 'LB_' ::=
-  {{ com let binding }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | let pat = exp                                    :: :: val
-    {{ com let, implicit type ($[[pat]]$ must be total)}}
-
-val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::=
-   {{ ocaml VS_aux of val_spec_aux * 'a annot }}
-   {{ lem VS_aux of val_spec_aux * annot 'a }}
-  | val_spec_aux ::  :: aux
-
-val_spec_aux :: 'VS_' ::=
-  {{ com value type specification }}
-  {{ ocaml  VS_val_spec of typschm * id * (string -> string option) * bool }}
-  {{ lem VS_val_spec of typschm * id * maybe string * bool }}
-  | val typschm id                                  :: S :: val_spec
-    {{ com specify the type of an upcoming definition }}
-    {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }}
-
-default_spec :: 'DT_' ::=
-  {{ com default kinding or typing assumption }}
-  {{ aux _ l }}
-  | default Order order      :: :: order
-
-reg_id :: 'RI_' ::=
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id								:: :: id
-
-alias_spec :: 'AL_' ::=
-  {{ com register alias expression forms }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | reg_id . id							:: :: subreg
-  | reg_id [ exp ] 						:: :: bit
-  | reg_id [ exp '..' exp' ]					:: :: slice
-  | reg_id : reg_id'  	    					:: :: concat
-
-dec_spec :: 'DEC_' ::=
-  {{ com register declarations }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | register typ id                                             :: :: reg
-  | register alias id = alias_spec				:: :: alias
-  | register alias typ id = alias_spec				:: :: typ_alias
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Top-level definitions                                        %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-prec :: '' ::=
-   | infix :: :: Infix
-   | infixl :: :: InfixL
-   | infixr :: :: InfixR
-
-def :: 'DEF_' ::=
-  {{ com top-level definition }}
-  {{ auxparam 'a }}
-  | type_def                                             :: :: type
-    {{ com type definition }}
-  | fundef                                               :: :: fundef
-    {{ com function definition }}
-  | letbind                                              :: :: val
-    {{ com value definition }}
-  | val_spec                                             :: :: spec
-    {{ com top-level type constraint }}
-  | fix prec num id                                      :: :: fixity
-    {{ com fixity declaration }}
-  |  overload id [ id1 ; ... ; idn ]                     :: :: overload
-    {{ com operator overload specification }}
-  | default_spec                                         :: :: default
-    {{ com default kind and type assumptions }}
-  | dec_spec                                             :: :: reg_dec
-    {{ com register declaration }}
-
-defs :: '' ::=
-  {{ com definition sequence }}
-  {{ auxparam 'a }}
-  | def1  .. defn                 :: :: Defs