Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
1483 lines (1310 sloc) 69.9 KB
embed
{{ tex
\makeatletter
\input ott-spec.ltx
\newcommand{\ottenvironmentappend}[2]{
\begingroup
\def\@tempa{#1}\def\@tempb{ \ottkw{empty} }
\ifx\@tempa\@tempb\def\@tempc{}\else\def\@tempc{#1,}\fi
\expandafter\endgroup
\@tempc#2
}
\newcommand{\ie}{ i.e., }
\newcommand{\eg}{ e.g., }
\makeatother
\title{QuaLiTyML}
\author{Raphael Proust}
\maketitle
\tableofcontents
\section{Introduction}
\label{sec.introduction}
TODO
}}
{{ coq
Require Ascii.
Require Import BinInt.
Require String.
Require Import Zdiv.
Require Import ott_list.
Require Import caml_lib_misc.
}}
{{ hol
local open integerTheory sortingTheory floatTheory integer_wordTheory in end;
val _ = wordsLib.mk_word_size 31;
}}
{{ tex
\section{Syntax}
\label{sec.syntax}
TODO
}}
%% Note: ott does not currently supports TeX embeddings inside the
%% grammar (any embedding except for the very first embed block they
%% is printed after the grammar).
indexvar index , i , j , k , l , m , n ::=
{{ lex numeral }}
{{ coq nat }}
{{ coq-equality }}
{{ hol num }}
{{ isa nat }}
{{ com index variables (subscripts) }}
%% 6.1 (Identifiers) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#ident
%% Our usage of [[ident]] is probably wrong: we should probably use
%% [[lowercase_ident]] instead. There are cases where the concrete
%% syntax lexes as alphanum though; these should be called [[ident]],
%% but I don't think we handle any of them (e.g., polmyorphic variants).
metavar ident ::=
{{ lex alphanum }}
{{ coq nat }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
%% 6.1 (Integer literals) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#integer-literal
metavar integer_literal ::=
{{ lex numeral }}
{{ coq Z }}
{{ coq-equality }}
{{ hol word31 }}
{{ holvar [[integer_literal]]w }}
{{ isa int }}
%% 6.1 (Floating-point literals) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#float-literal
metavar float_literal ::=
{{ coq nat }} % should be real
{{ coq-equality }}
{{ hol float }}
{{ isa nat }}
%% 6.1 (Character literals) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#char-literal
metavar char_literal ::=
{{ coq Ascii.ascii }}
{{ coq-equality }}
{{ hol char }}
{{ isa char }}
%% 6.1 (String literals) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#string-literal
metavar string_literal ::=
{{ coq String.string }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
%% 6.1 (Prefix and infix symbols) http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#infix-symbol
metavar infix_symbol ::=
{{ coq String.string }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
metavar prefix_symbol ::=
{{ coq String.string }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
%% Not in OCaml's syntax: Locations
metavar location , l {{ tex \ell }} ::=
{{ coq nat }}
{{ coq-equality }}
{{ hol num }}
{{ isa nat }}
{{ com store locations (not in the source syntax) }}
%% 6.3 (Names)
metavar lowercase_ident ::=
{{ lex alphanum0 }}
{{ coq String.string }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
metavar capitalized_ident ::=
{{ lex Alphanum }}
{{ coq String.string }}
{{ coq-equality }}
{{ hol string }}
{{ isa string }}
grammar
%% 6.3 (Naming objects) http://caml.inria.fr/pub/docs/manual-ocaml/manual011.html#value-name
value_name , x :: VN_ ::= {{ coq-equality }}
| lowercase_ident :: :: id
| ( operator_name ) :: :: op
operator_name :: ON_ ::= {{ coq-equality }}
| prefix_symbol :: :: symbol
| infix_op :: :: infix
infix_op :: IO_ ::= {{ coq-equality }}
| infix_symbol :: :: symbol
| * :: L :: star
| = :: L :: equal
%% "or" and "&" are obsolete syntactic sugar.
% | or :: :: or
% | & :: :: amp
| := :: L :: colonequal
%% The following 7 are integer operators (not handled at the moment).
% | mod :: :: mod
% | land :: :: land
% | lor :: :: lor
% | lxor :: :: lxor
% | lsl :: :: lsl
% | lsr :: :: lsr
% | asr :: :: asr
constr_name , C :: CN_ ::= {{ coq-equality }}
| capitalized_ident :: :: id
typeconstr_name, tcn :: TCN_ ::= {{ coq-equality }}
| lowercase_ident :: :: id
field_name , fn :: FN_ ::= {{ coq-equality }}
| lowercase_ident :: d :: id
%% 6.3 (Referring to named objects) http://caml.inria.fr/pub/docs/manual-ocaml/manual011.html#value-path
value_path :: VP_ ::= {{ coq-equality }}
| value_name :: :: name
constr :: C_ ::= {{ coq-equality }}
{{ com constructors: named, and built-in }}
| constr_name :: :: name
%% 19.1 (Built-in types) http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html
| None :: L :: none
| Some :: L :: some
typeconstr :: TC_ ::= {{ coq-equality }}
{{ com type constructors: named, and built-in }}
| typeconstr_name :: :: name
%% 19.1 (Built-in types) http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html
| int :: L :: int
| char :: L :: char
| string :: L :: string
| float :: L :: float
| bool :: L :: bool
| unit :: L :: unit
| list :: L :: list
| option :: L :: option
%% Pervasives http://caml.inria.fr/pub/docs/manual-ocaml/libref/Pervasives.html
| ref :: L :: ref
% %% QuaLiTy: user hints for Quality
% | lin :: L :: linear
% | obs :: L :: observer
% | nonlin :: L :: nonlinear
field :: F_ ::= {{ coq-equality }}
| field_name :: d :: name
% | module_path . field_name :: d :: path
idx, num :: '' ::=
{{ coq nat }}
{{ hol num }}
{{ isa nat }}
{{ com index arithmetic for the type system's deBruijn type variable representation }}
| 0 {{ tex 0 }} :: I :: 0
| 1 {{ tex 1 }} :: I :: 1
| 2 {{ tex 2 }} :: I :: 2
| m :: I :: N
{{ ich [[m]] }}
| idx1 + idx2 :: I :: Add
{{ ich ([[idx1]] + [[idx2]]) }}
| ( num ) :: S I :: paren
{{ ich [[num]] }}
Tsigma {{ tex \sigma^T }} :: Tsigma_ ::=
{{ coq list (typevar * typexpr) }}
{{ hol (typevar#typexpr) list }}
{{ isa (typevar*typexpr) list }}
{{ com multiple substitutions of types for type variables }}
| '<<' typevar1 <- typexpr1 , .. , typevarn <- typexprn '>>' :: I :: substs
{{ ich [[typevar1 typexpr1..typevarn typexprn]] }}
| shift num num' Tsigma :: M I :: shift
{{ ich (shiftTsig [[num]] [[num']] [[Tsigma]]) }}
{{ com shift the indices in the types in [[Tsigma]] by [[num]], ignoring indices lower than [[num']] }}
%% 6.4 (Type expressions) http://caml.inria.fr/pub/docs/manual-ocaml/manual012.html#typexpr
quality, qlt, q :: QLT_ ::= {{ com qualities for types }}
| linear {{ tex 1 }} :: :: linear
| observed {{ tex \delta }} :: :: observed
| nonlinear {{ tex \omega }} :: :: nonlinear
typexpr , t :: TE_ ::=
| typevar '[^' qlt '^]' :: :: var
| < idx , num > :: I :: idxvar
{{ com de Bruijn represenataion of type variables. [[num]] allows each binder (\ie a polymorphic $\ottkw{let}$) to introduce an arbitrary number of binders }}
| _ '[^' qlt '^]' :: :: any
| ( typexpr ) :: S :: paren
{{ ich [[typexpr]] }}
| typexpr1 -> '[^' qlt '^]' typexpr2 :: :: arrow
| ( typexpr1 * .... * typexprn ) '[^' qlt '^]' :: :: tuple
| typeconstr '[^' qlt '^]' :: S :: constr0
{{ coq (TE_constr nil [[typeconstr]]) }}
{{ hol (TE_constr [] [[typeconstr]]) }}
{{ isa (TE_constr [] [[typeconstr]]) }}
{{ com in the theorem prover models we use a uniform representation for 0-, 1-, and n-ary type constructor applications }}
| typexpr typeconstr '[^' qlt '^]' :: S :: constr1
{{ coq (TE_constr (cons [[typexpr]] nil) [[typeconstr]]) }}
{{ hol (TE_constr ([ [[typexpr]] ]) [[typeconstr]]) }}
{{ isa (TE_constr ([ [[typexpr]] ]) [[typeconstr]]) }}
| ( typexpr1 , ... , typexprn ) typeconstr '[^' qlt '^]' :: :: constr
% | typexpr as typevar :: ::
| shift num num' typexpr :: M :: shift
{{ ich (shiftt [[num]] [[num']] [[typexpr]]) }}
{{ com shifts as in $[[Tsigma]]$ above }}
% We do not provide n-ary curried functions because the parsing is difficult
% (too difficult for ott?). We might do some time in the future.
| Tsigma typexpr :: M I :: susbts
{{ ich (substs_typevar_typexpr [[Tsigma]] [[typexpr]]) }}
{{ com apply the substitution }}
src_typexpr , src_t :: STE_ ::= {{ com types that can appear in source programs }}
| typevar '[^' qlt '^]' :: :: var
| _ '[^' qlt '^]' :: :: any
| ( src_typexpr ) :: :: paren
| src_typexpr1 -> '[^' qlt '^]' src_typexpr2 :: :: arrow
| ( src_typexpr1 * .... * src_typexprn ) '[^' qlt '^]' :: :: tuple
| typeconstr '[^' qlt '^]' :: :: constr0
| src_typexpr typeconstr '[^' qlt '^]' :: :: constr1
| ( src_typexpr1 , ... , src_typexprn ) typeconstr '[^' qlt '^]' :: :: constr
| shift num num' src_typexpr :: :: shift
typevar {{ tex \alpha }} , tv {{ tex \alpha }} :: TV_ ::= {{ coq-equality }}
| ' ident :: :: ident
{{ tex {\ottkw{'}[[ident]]} }}
typescheme, ts :: TS_ ::=
| forall typexpr :: I :: forall
| shift num num' typescheme :: I M :: shift
{{ ich (shiftts [[num]] [[num']] [[typescheme]]) }}
{{ com shifts as in $[[Tsigma]]$ above }}
intn {{ tex \dot{n} }} :: Intn_ ::=
{{ coq integer_literal }}
{{ coq-equality }}
{{ hol word31 }}
{{ isa int }}
{{ com integer mathematical expressions, used to implement primitive operations and $\ottkw{for}$ loops }}
| integer_literal :: :: lit
{{ coq ([[integer_literal]])%Z }}
{{ hol [[integer_literal]] }}
{{ isa ( [[integer_literal]]) }} %% FIXME not sure about this
| ( intn ) :: M I :: paren
{{ ich [[intn]] }}
| intn1 .+ intn2 :: M I :: plus
{{ tex [[intn1]] \stackrel\centerdot+ [[intn2]] }}
{{ coq (([[intn1]] + [[intn2]])%Z) }}
{{ hol ([[intn1]] + [[intn2]]) }}
{{ isa ([[intn1]] + [[intn2]]) }}
| intn1 .- intn2 :: M I :: minus
{{ tex [[intn1]] \stackrel\centerdot- [[intn2]] }}
{{ coq (([[intn1]] - [[intn2]])%Z) }}
{{ hol ([[intn1]] - [[intn2]]) }}
{{ isa ([[intn1]] - [[intn2]]) }}
| intn1 .* intn2 :: M I :: times
{{ tex [[intn1]] \stackrel\centerdot* [[intn2]] }}
{{ coq (([[intn1]] * [[intn2]])%Z) }}
{{ hol ([[intn1]] * [[intn2]]) }}
{{ isa ([[intn1]] * [[intn2]]) }}
| intn1 ./ intn2 :: M I :: div
{{ tex [[intn1]] \stackrel\centerdot/ [[intn2]] }}
{{ coq (([[intn1]] / [[intn2]])%Z) }}
{{ hol ([[intn1]] / [[intn2]]) }}
{{ isa ([[intn1]] div [[intn2]]) }} %% FIXME not sure about this
%% 6.5 (Constants) http://caml.inria.fr/pub/docs/manual-ocaml/manual013.html#constant
constant :: CONST_ ::= {{ coq-equality }}
| intn :: L :: int
| float_literal :: L :: float
| char_literal :: L :: char
| string_literal :: L :: string
| equal_error_string :: M L :: equal_error_string
{{ hol (CONST_string "equal: functional value") }}
{{ isa (CONST_string ''equal: functional value'') }}
{{ coq (CONST_string string_equal_functional_value) }}
{{ com The string constant "equal: functional value" }}
| constr :: L :: constr
| false :: L :: false
| true :: L :: true
| [] :: L :: nil
| () :: L :: unit
%% 6.6 (Patterns) http://caml.inria.fr/pub/docs/manual-ocaml/patterns.html#pattern
pattern , pat :: P_ ::=
| value_name :: :: var
(+ xs = value_name +)
| _ :: :: any
(+ xs = {} +)
| constant :: :: constant
(+ xs = {} +)
| pattern as value_name :: :: alias
(+ xs = xs(pattern) union value_name +)
| ( pattern ) :: S :: paren
{{ ich [[pattern]] }}
| ( pattern : typexpr ) :: :: typed
(+ xs = xs(pattern) +)
| pattern1 '|' pattern2 :: :: or
(+ xs = xs(pattern1) +)
%% Comment out [construct_unary] when it can be given proper precedence wrt
%% [construct] and [construct_any].
% | constr pattern :: S :: construct_unary
% {{ ich (P_construct [[constr]] (cons [[pattern]] nil)) }}
| constr ( pattern1 , ... , patternn ) :: :: construct
(+ xs = xs(pattern1...patternn) +)
| constr _ :: :: construct_any
(+ xs = {} +)
| pattern1 , .... , patternn :: :: tuple
(+ xs = xs(pattern1....patternn) +)
| { field1 = pattern1 ; ... ; fieldn = patternn } :: d :: record
(+ xs = xs(pattern1...patternn) +)
| [ pattern1 ; ... ; patternn ] :: S L :: list
{{ coq (fold_right P_cons CONST_nil [[pattern1...patternn]]) }}
{{ hol (FOLDR P_cons e l (P_constant CONST_nil) [[pattern1...patternn]]) }}
{{ isa (foldr P_cons l e (P_constant CONST_nil) [[pattern1...patternn]]) }}
| pattern1 '::' pattern2 :: L :: cons
(+ xs = xs(pattern1) union xs(pattern2) +)
parsing
P_tuple <= P_construct
grammar
%% Important primitives from Pervasives http://caml.inria.fr/pub/docs/manual-ocaml/libref/Pervasives.html
unary_prim :: Uprim_ ::=
{{ com primitive functions with one argument }}
| not :: L I :: not
| ~- :: L I :: minus
| ref :: L I :: ref
| ! :: L I :: deref
binary_prim :: Bprim_ ::=
{{ com primitive functions with two arguments }}
| = :: L I :: equal
| + :: L I :: plus
| - :: L I :: minus
| * :: L I :: times
| / :: L I :: div
| := :: L I :: assign
%% 6.7 (Expressions) http://caml.inria.fr/pub/docs/manual-ocaml/expr.html#expr
expr , e :: Expr_ ::=
| ( %prim unary_prim ) :: L I :: uprim
{{ com a unary primitive function value }}
| ( %prim binary_prim ) :: L I :: bprim
{{ com a binary primitive function value }}
| value_name :: :: ident
| constant :: :: constant
| ( expr ) :: S :: paren
{{ ich [[expr]] }}
| begin expr end :: S :: parenb
{{ ich [[expr]] }}
| ( expr : typexpr ) :: :: typed
| expr1 , .... , exprn :: :: tuple
| constr ( expr1 , .. , exprn ) :: :: construct
{{ com potentially empty constructors to work around ott parser restriction }}
| expr1 '::' expr2 :: L :: cons
| [ expr1 ; ... ; exprn ] :: S L :: list
{{ coq (fold_right Expr_const CONST_nil [[expr1...exprn]]) }}
{{ hol (FOLDR Expr_cons (Expr_constant CONST_nil) [[expr1...exprn]]) }}
{{ isa (foldr Expr_cons [[expr1...exprn]] (Expr_constant CONST_nil)) }}
| { field1 = expr1 ; ... ; fieldn = exprn } :: d :: record
| { expr with field1 = expr1 ; ... ; fieldn = exprn } :: d :: override
| expr1 expr2 :: :: apply
| prefix_symbol expr :: S :: applyp
{{ ich (Expr_apply (Expr_ident (VP_name (VN_op [[prefix_symbol]]))) [[expr]]) }}
| expr1 infix_op expr2 :: S :: applyi
{{ ich (Expr_apply (Expr_apply (Expr_ident (VP_name (VN_op (ON_infix [[infix_op]])))) [[expr1]]) [[expr2]]) }}
| expr1 && expr2 :: L :: and
| AND ( expr1 && .. && exprn ) :: M I L :: multiand
{{ coq (fold_right Expr_and CONST_true [[expr1..exprn]]) }}
{{ hol (FOLDR Expr_and (Expr_constant CONST_true) [[expr1..exprn]]) }}
{{ isa (foldr Expr_and [[expr1..exprn]] (Expr_constant CONST_true)) }}
{{ com a delimited ``and'' operator with a list of arguments }}
| expr1 || expr2 :: L :: or
| expr . field :: d :: field
% | expr . field <- expr :: d :: setfield
| if expr0 then expr1 :: S :: ifthen
{{ ich (Expr_ifthenelse [[expr0]] [[expr1]] (Expr_constant CONST_unit)) }}
| if expr0 then expr1 else expr2 :: :: ifthenelse
| while expr1 do expr2 done :: :: while
| for x = expr1 for_dirn expr2 do expr3 done :: :: for
(+ bind x in expr3 +)
| expr1 ; expr2 :: :: sequence
| match expr with pattern_matching :: :: match
| function pattern_matching :: :: function
| fun pattern1 ... patternn -> expr :: S :: func
{{ ich (fold_pats [[pattern1...patternn]] [[expr]]) }}
| let let_binding in expr :: :: let
(+ bind xs(let_binding) in expr +)
{{ com omitting multiple bindings, i.e.\ $\ottkw{and}$ }}
| let rec letrec_bindings in expr :: :: letrec
(+ bind xs(letrec_bindings) in letrec_bindings +)
(+ bind xs(letrec_bindings) in expr +)
| location :: I :: location
| '<<' substs_x '>>' expr :: M I :: substs
{{ coq (substs_value_name_expr (substs_x_proj [[substs_x]]) [[expr]]) }}
{{ hol (substs_value_name_expr (case [[substs_x]] of substs_x_xs l -> l) [[expr]]) }}
{{ isa (substs_value_name_expr (case [[substs_x]] of substs_x_xs l => l) [[expr]]) }}
{{ com substitution of expressions for variables }}
| remv_tyvar expr :: M I :: rem_tyvar
{{ ich (remv_tyvar_expr [[expr]]) }}
{{ com replace the type variables in an expression's type annotations with $\ottkw{\_}$ }}
parsing
Expr_tuple <= Expr_construct
CONST_constr right Expr_apply
grammar
for_dirn {{ tex \ottkw{\relax{\sf[}down{\sf]}to} }} :: FD_ ::=
{{ coq-equality }}
| to :: :: upto
| downto :: :: downto
%% It would be nice for the theorem prover type for [[substs_x]]
%% to be exactly [list (value_name*expr)], but we cannot declare
%% type representation homs as ott would then stop generating
%% auxiliary functions.
substs_x :: substs_x_ ::=
{{ com substitutions of expressions for variables }}
| value_name1 <- expr1 , .. , value_namen <- exprn :: I :: xs
| substs_x1 @ .. @ substs_xn :: M I :: substs
{{ coq (substs_x_xs (flat_map substs_x_proj [[substs_x1..substs_xn]])) }}
{{ hol (substs_x_xs (FLAT (MAP (\x. case x of substs_x_xs l -> l) [[substs_x1..substs_xn]]))) }}
{{ isa (substs_x_xs (concat (map (%x. case x of substs_x_xs l => l) [[substs_x1..substs_xn]]))) }}
pattern_matching , pm :: PM_ ::=
| pat_exp1 '|' ... '|' pat_expn :: :: pm
| '|' pat_exp1 '|' ... '|' pat_expn :: S :: pm_extra_bar
{{ ich (PM_pm [[pat_exp1...pat_expn]]) }}
pat_exp :: PE_ ::=
| pattern -> expr :: :: inj (+ bind xs(pattern) in expr +)
let_binding :: LB_ ::=
| pattern = expr :: :: simple
(+ xs = xs(pattern) +)
| value_name pattern1 ... patternn = expr :: S :: func
{{ ich (LB_simple (P_var [[value_name]]) (fold_pats [[pattern1...patternn]] [[expr]])) }}
| value_name pattern1 ... patternn : typexpr = expr :: S :: typed
{{ ich (LB_simple (P_var [[value_name]]) (fold_pats [[pattern1...patternn]] (Expr_typed [[expr]] [[typexpr]]))) }}
| '<<' typevar1 <- typexpr1 , .. , typevarn <- typexprn '>>' let_binding :: M :: susbts
{{ ich (substs_typevar_let_binding [[typevar1 typexpr1..typevarn typexprn]] [[let_binding]]) }}
{{ com substitution of types for type variables }}
letrec_bindings :: LRBs_ ::=
| letrec_binding1 and ... and letrec_bindingn :: :: inj (+ xs = xs(letrec_binding1 ... letrec_bindingn) +)
| '<<' typevar1 <- typexpr1 , .. , typevarn <- typexprn '>>' letrec_bindings :: M :: susbts
{{ ich (substs_typevar_letrec_bindings [[typevar1 typexpr1..typevarn typexprn]] [[letrec_bindings]]) }}
{{ com substitution of types for type variables }}
%% We want to restrict recursive definitions to functions. We can do this
%% in the syntax or in the type system. We currently do it in the syntax.
letrec_binding :: LRB_ ::=
| value_name = function pattern_matching :: :: simple
(+ xs = value_name +)
| value_name = fun pattern pattern1 .. patternn -> expr :: S :: func
{{ ich (LRB_simple [[value_name]] (PM_pm [PE_inj [[pattern]] (fold_pats [[pattern1..patternn]] [[expr]])])) }}
| value_name pattern pattern1 .. patternn = expr :: S :: impl_fun
{{ ich (LRB_simple [[value_name]] (PM_pm [PE_inj [[pattern]] (fold_pats [[pattern1..patternn]] [[expr]])])) }}
| value_name pattern pattern1 .. patternn : typexpr = expr :: S :: typed
{{ ich (LRB_simple [[value_name]] (PM_pm [PE_inj [[pattern]] (fold_pats [[pattern1..patternn]] (Expr_typed [[expr]] [[typexpr]]))])) }}
>>
<<
%% 6.8.1 (Type definitions) http://caml.inria.fr/pub/docs/manual-ocaml/manual016.html#type-definition
type_definition {{ isa caml_type_definition }} :: TDF_ ::=
| type typedef1 and .. and typedefn :: d :: tdf
(+ type_names = type_names(typedef1..typedefn) +)
(+ constr_names = constr_names(typedef1..typedefn) +)
{{ com potentially empty definitions to work around Ott parser restrictions }}
typedef {{ isa caml_typedef }} :: TD_ ::=
| type_params_opt typeconstr_name type_information :: d :: td
(+ bind typevars(type_params_opt) in type_information +)
(+ type_names = typeconstr_name +)
(+ constr_names = constr_names(type_information) +)
type_information :: TI_ ::=
| type_equation :: d :: eq
(+ constr_names = {} +)
(+ field_names = {} +)
| type_representation :: d :: def
(+ constr_names = constr_names(type_representation) +)
(+ field_names = field_names(type_representation) +)
type_equation :: TE_ ::=
| = typexpr :: d :: te
type_representation :: TR_ ::=
| = constr_decl1 '|' ... '|' constr_decln :: d :: variant
(+ constr_names = constr_names(constr_decl1...constr_decln) +)
(+ field_names = {} +)
| = { field_decl1 ; ... ; field_decln } :: d :: record
(+ constr_names = {} +)
(+ field_names = field_names(field_decl1...field_decln) +)
type_params_opt :: TPS_ ::=
| :: S d :: nullary
{{ coq (TPS_nary nil) }}
{{ hol (TPS_nary []) }}
{{ isa (TPS_nary []) }}
{{ com in the theorem prover models we use a uniform representation for empty, singleton and multiple type paramaters }}
| type_param :: S d :: unary
{{ coq (TPS_nary (cons [[type_param]] nil)) }}
{{ hol (TPS_nary [ [[type_param]] ]) }}
{{ isa (TPS_nary [ [[type_param]] ]) }}
| ( type_param1 , ... , type_paramn ) :: d :: nary
(+ typevars = typevars(type_param1...type_paramn) +)
type_param , tp :: TP_ ::= {{ coq-equality }}
| typevar :: d :: var
(+ typevars = typevar +)
constr_decl :: CD_ ::=
| constr_name :: d :: nullary
(+ constr_names = constr_name +)
| constr_name of typexpr1 * ... * typexprn :: d :: nary
(+ constr_names = constr_name +)
parsing
TE_tuple <= CD_nary
STE_tuple <= CD_nary
grammar
field_decl :: FD_ ::=
| field_name : typexpr :: d :: immutable
(+ field_names = field_name +)
%% 6.11 (Module expressions (module implementations)) http://caml.inria.fr/pub/docs/manual-ocaml/manual019.html#definition
definition {{ isa caml_definition }} , d :: D_ ::=
| let let_binding :: d :: let
(+ xs = xs(let_binding) +)
{{ com omitting multiple bindings, i.e.\ $\ottkw{and}$ }}
| let rec letrec_bindings :: d :: letrec
(+ xs = xs(letrec_bindings) +)
(+ bind xs(letrec_bindings) in letrec_bindings +)
| type_definition :: d :: type
(+ xs = {} +)
definitions , ds :: Ds_ ::=
| :: d :: nil
| definition definitions :: d :: cons
(+ bind xs(definition) in definitions +)
| definition ;; definitions :: S d :: cons_semi
{{ ich (Ds_cons [[definition]] [[definitions]]) }}
| '<<' substs_x '>>' definitions :: M d :: substs
{{ coq (substs_value_name_definitions (substs_x_proj [[substs_x]]) [[definitions]]) }}
{{ hol (substs_value_name_definitions (case [[substs_x]] of substs_x_xs l -> l) [[definitions]]) }}
{{ isa (substs_value_name_definitions (case [[substs_x]] of substs_x_xs l => l) [[definitions]]) }}
{{ com substitution of expressions for variables }}
| definitions definition :: M d :: snoc
{{ ich (definitions_snoc [[definitions]] [[definition]]) }}
{{ com adding a definition to the end of a sequence }}
| definitions ;; definition :: M d :: snoc_semi
{{ ich (definitions_snoc [[definitions]] [[definition]]) }}
program :: Prog_ ::=
| definitions :: d :: defs
>>
<<
%% Gadgets for the type system and semantics that are not in the source syntax.
value {{ coq core_value }} , v :: V_ ::=
{{ com core value }}
| ( %prim unary_prim ) :: L I :: uprim
| ( %prim binary_prim ) :: L I :: bprim
| binary_prim_app_value value :: I :: bprim_app
{{ com partially applied binary primitive }}
| constant :: I :: constant
| ( value ) :: I :: paren
| value1 , .... , valuen :: I :: tuple
| constr ( value1 , .. , valuen ) :: I :: construct
| value1 '::' value2 :: I L :: cons
| [ value1 ; ... ; valuen ] :: I L :: list
| { field1 = value1 ; ... ; fieldn = valuen } :: I d :: record
| function pattern_matching :: I :: function
| fun pattern1 ... patternn -> expr :: I :: func
| location :: I :: location
binary_prim_app_value :: BPAV_ ::=
| ( %prim binary_prim ) :: I :: inj
parsing
V_tuple <= V_construct
grammar
>>
<<
definition_value , d_value :: DV_ ::=
| type_definition :: d I :: type
definitions_value , ds_value :: DsV_ ::=
| :: d I :: nil
| definition_value definitions_value :: d I :: cons
| definition_value ;; definitions_value :: d I :: cons_semi
>>
<<
non_expansive , nexp :: Nexp_ ::=
{{ com nonexpansive expression (allowed in a polymorphic let) }}
| ( %prim unary_prim ) :: I :: uprim
| ( %prim binary_prim ) :: I :: bprim
| binary_prim_app_value nexp :: I :: bprim_app
{{ com partially applied binary primitive }}
| value_name :: I :: ident
| constant :: I :: constant
| ( nexp ) :: I :: paren
| ( nexp : typexpr ) :: I :: typed
| nexp1 , .... , nexpn :: I :: tuple
| constr ( nexp1 , .. , nexpn ) :: I :: construct
| nexp1 '::' nexp2 :: I :: cons
| [ nexp1 ; ... ; nexpn ] :: I L :: list
| { field1 = nexp1 ; ... ; fieldn = nexpn } :: I d :: record
| let rec letrec_bindings in nexp :: I :: letrec
| function pattern_matching :: I :: function
| fun pattern1 ... patternn -> expr :: I :: func
| location :: I :: location
parsing
Nexp_tuple <= Nexp_construct
grammar
store , st :: STORE_ ::=
{{ hol (([[location]]#[[expr]]) list) }}
{{ isa (([[location]]*[[expr]]) list) }}
{{ coq list (location * expr)}}
| empty :: I :: empty
{{ hol [] }}
{{ isa [] }}
{{ coq (@nil (location*expr)) }}
| store , location |-> expr :: I :: map
{{ hol (([[location]], [[expr]])::[[store]]) }}
{{ isa (([[location]], [[expr]])#[[store]]) }}
{{ coq (cons ([[location]], [[expr]]) [[store]]) }}
| store , location |-> expr , store' :: M I :: middle
{{ hol ([[store']]++[([[location]], [[expr]])]++[[store]]) }}
{{ isa ([[store']]@[([[location]], [[expr]])]@[[store]]) }}
{{ coq (app [[store']] (cons ([[location]], [[expr]]) [[store]])) }}
kind :: K_ ::=
{{ coq nat }}
{{ hol num }}
{{ isa nat }}
| num -> Type :: I :: arity
{{ ich [[num]] }}
{{ tex \ottkw{Type}^{[[num]]}\rightarrow[[Type]] }}
| Type :: S I :: type
{{ ich 0 }}
name :: name_ ::= {{ coq-equality }}
{{ com environment lookup key }}
| TV :: I :: tv
| value_name :: I :: vn
| constr_name :: d I :: cn
| typeconstr_name :: d I :: tcn
| field_name :: d I :: fn
| location :: I :: l
names :: names_ ::=
{{ coq list name }}
{{ hol (name list) }}
{{ isa (name list) }}
| name1 .. namen :: I :: inj
{{ ich [[name1..namen]] }}
typexprs :: typexprs_ ::=
| typexpr1 , ... , typexprn :: I :: inj
| shift num num' typexprs :: M I :: shift
{{ ich (shifttes [[num]] [[num']] [[typexprs]]) }}
{{ com shift the indices in the types in [[typexprs]] by [[num]], ignoring indices lower than [[num']] }}
environment_binding , EB :: EB_ ::=
| TV :: I :: tv
{{ com type variable }}
| value_name : typescheme :: I :: vn
{{ com value binding }}
| value_name : typexpr :: M I :: vntype
{{ com value binding with no universal quantifier }}
{{ ich (EB_vn [[value_name]] (TS_forall (shiftt 0 1 [[typexpr]]))) }}
| constr_name of typeconstr :: d I :: cc
{{ com constant constructor }}
| constr_name of forall type_params_opt , ( typexprs ) : typeconstr :: d I :: pc
(+ bind typevars(type_params_opt) in typexprs +)
{{ com parameterised constructor }}
| field_name : forall type_params_opt , typeconstr_name -> typexpr :: d I :: fn
(+ bind typevars(type_params_opt) in typexpr +)
{{ com field name a record destructor }}
| typeconstr_name : kind :: d I :: td
{{ com type name, bound to a fresh type }}
| typeconstr_name : kind { field_name1 ; ... ; field_namen } :: d I :: tr
{{ com type name which is a record type definition }}
| type_params_opt typeconstr_name = typexpr :: d I :: ta
(+ bind typevars(type_params_opt) in typexpr +)
{{ com type name which is an abbreviation }}
| location : typexpr :: I :: l
{{ com location (memory cell) }}
| ( EB ) :: M I :: paren
{{ ich [[EB]] }}
| shift num num' EB :: M I :: shift
{{ ich (shiftEB [[num]] [[num']] [[EB]]) }}
{{ com shift the indices in the types in [[EB]] by [[num]], ignoring indices lower than [[num']] }}
environment , E :: Env_ ::=
{{ coq (list environment_binding) }}
{{ hol (environment_binding list) }}
{{ isa (environment_binding list) }}
| empty :: I :: nil
{{ coq (@nil environment_binding) }}
{{ hol [] }}
{{ isa [] }}
| E , EB :: I :: snoc
{{ tex \ottenvironmentappend{[[E]]}{[[EB]]} }}
{{ coq (cons [[EB]] [[E]]) }}
{{ hol ([[EB]]::[[E]]) }}
{{ isa ([[EB]]#[[E]]) }}
| EB1 , .. , EBn :: M I :: list
{{ coq (rev [[EB1 .. EBn]]) }}
{{ hol (REVERSE [[EB1 .. EBn]]) }}
{{ isa (rev [[EB1 .. EBn]]) }}
| E1 @ .. @ En :: M I :: tree
{{ coq (flatten (rev [[E1 .. En]])) }}
{{ hol (FLAT (REVERSE [[E1 .. En]])) }}
{{ isa (concat (rev [[E1 .. En]])) }}
trans_label , L :: Lab_ ::=
{{ com reduction label (denoting a side effect) }}
| :: I :: nil
| ref v = location :: I :: alloc
| ! location = v :: I :: deref
| location := v :: I :: assign
| ( L ) :: I M :: paren
{{ ich [[L]] }}
{{ tex [[L]] }}
labelled_arrow :: LA_ ::=
{{ ich trans_label }}
{{ tex \stackrel{\ottnt{L} }{\longrightarrow}\ottmaybebreakline }}
| --> L :: I :: inj
{{ ich [[L]] }}
{{ tex \stackrel{[[L]]}{\longrightarrow}\ottmaybebreakline }}
subrules
value <:: expr
binary_prim_app_value <:: expr
non_expansive <:: expr
src_typexpr <:: typexpr
>>
<<
subrules
definition_value <:: definition
definitions_value <:: definitions
>>
<<
freevars typexpr typevar :: ftv
freevars expr value_name :: fv
freevars expr location :: fl
substitutions
multiple typexpr typevar :: substs_typevar
multiple expr value_name :: substs_value_name
single expr value_name :: subst_value_name
grammar
formula :: formula_ ::=
{{ com semantic judgements and their side conditions }}
| judgement :: :: judgement
| formula1 .. formulan :: :: dots
| intn1 <= intn2 :: :: le_int
{{ coq (([[intn1]] <= [[intn2]])%Z) }}
{{ hol ([[intn1]] <= [[intn2]]) }}
{{ isa ([[intn1]] <= [[intn2]]) }}
{{ tex [[intn1]] \stackrel\centerdot\leq [[intn2]] }}
| intn1 > intn2 :: :: gt_int
{{ coq (([[intn1]] > [[intn2]])%Z) }}
{{ hol ([[intn1]] > [[intn2]]) }}
{{ isa ([[intn1]] <= [[intn2]]) }}
{{ tex [[intn1]] \stackrel\centerdot > [[intn2]] }}
| num1 < num2 :: :: lt_num
{{ coq (([[num1]] < [[num2]])%Z) }}
{{ hol ([[num1]] < [[num2]]) }}
{{ isa ([[num1]] < [[num2]]) }}
| E = E' :: :: eq_environment
{{ ich ([[E]] = [[E']]) }}
| expr = expr' :: :: eq_expr
{{ ich ([[expr]] = [[expr']]) }}
| typexpr = typexpr' :: :: eq_typexpr
{{ ich ([[typexpr]] = [[typexpr']]) }}
| typescheme = typescheme' :: :: eq_typescheme
{{ ich ([[typescheme]] = [[typescheme']]) }}
| type_params_opt = type_params_opt' :: :: eq_type_params_opt
{{ ich ([[type_params_opt]] = [[type_params_opt']]) }}
| letrec_bindings = letrec_bindings' :: :: eq_letrec_bindings
{{ ich ([[letrec_bindings]] = [[letrec_bindings']]) }}
{{ tex [[letrec_bindings]] = ([[letrec_bindings']]) }}
| length ( tp1 ) .. ( tpn ) = m :: :: length_list_type_param_eq
{{ coq ([[m]] = length [[tp1..tpn]]) }}
{{ hol ([[m]] = LENGTH ([[tp1..tpn]])) }}
{{ isa ([[m]] = length ([[tp1..tpn]])) }}
| length ( t1 ) .. ( tn ) = num :: :: length_list_typexpr_eq
{{ coq ([[num]] = length [[t1..tn]]) }}
{{ hol ([[num]] = LENGTH ([[t1..tn]])) }}
{{ isa ([[num]] = length ([[t1..tn]])) }}
| length ( t1 ) .. ( tn ) <= num :: :: length_list_typexpr_le
{{ coq (length [[t1..tn]] <= [[num]]) }}
{{ hol (LENGTH ([[t1..tn]]) <= [[num]]) }}
{{ isa (length ([[t1..tn]]) <= [[num]]) }}
| length ( t1 ) .. ( tn ) >= num :: :: length_list_typexpr_ge
{{ coq (length [[t1..tn]] >= [[num]]) }}
{{ hol (LENGTH ([[t1..tn]]) >= [[num]]) }}
{{ isa (length ([[t1..tn]]) >= [[num]]) }}
| length ( pat1 ) .. ( patn ) >= m :: :: length_list_pattern_ge
{{ coq (length [[pat1..patn]] >= [[m]]) }}
{{ hol (LENGTH ([[pat1..patn]]) >= [[m]]) }}
{{ isa (length ([[pat1..patn]]) >= [[m]]) }}
| length ( e1 ) .. ( en ) >= m :: :: length_list_expr_ge
{{ coq (length [[e1..en]] >= [[m]]) }}
{{ hol (LENGTH ([[e1..en]]) >= [[m]]) }}
{{ isa (length ([[e1..en]]) >= [[m]]) }}
| name notin names :: :: name_notin
{{ coq (~In [[name]] [[names]]) }}
{{ hol (~MEM [[name]] [[names]]) }}
{{ isa (~( [[name]] mem [[names]])) }}
| field_name in field_name1 .. field_namen :: d :: fn_in_fns
{{ coq (In [[field_name]] [[field_name1..field_namen]]) }}
{{ hol (MEM [[field_name]] [[field_name1..field_namen]]) }}
{{ isa ([[field_name]] mem [[field_name1..field_namen]]) }}
| type_param in type_params_opt :: :: typevar_in_typevars
{{ coq (In [[type_param]] (match [[type_params_opt]] with TPS_nary x => x end)) }}
{{ hol (MEM [[type_param]] (case [[type_params_opt]] of TPS_nary x -> x)) }}
{{ isa ([[type_param]] mem (case [[type_params_opt]] of TPS_nary x => x)) }}
| name1 .. namen distinct :: :: distinct_names
{{ coq (NoDup [[name1..namen]]) }}
{{ hol (ALL_DISTINCT ([[name1..namen]])) }}
{{ isa (distinct ([[name1..namen]])) }}
| tp1 .. tpn distinct :: :: distinct_type_param
{{ coq (NoDup [[tp1..tpn]]) }}
{{ hol (ALL_DISTINCT ([[tp1..tpn]])) }}
{{ isa (distinct ([[tp1..tpn]])) }}
| E PERMUTES E' :: :: permutes_env
{{ coq (Permutation [[E]] [[E']]) }}
{{ hol (PERM ([[E]]) ([[E']])) }}
{{ isa (perm ([[E]]) ([[E']])) }}
| fn1 .. fnn PERMUTES fn1' .. fnm' :: d :: permutes_field_name
{{ coq (Permutation [[fn1..fnn]] [[fn1'..fnm']]) }}
{{ hol (PERM ([[fn1..fnn]]) ([[fn1'..fnm']])) }}
{{ isa (perm ([[fn1..fnn]]) ([[fn1'..fnm']])) }}
| fn1 = e1 .. fnn = en PERMUTES fn1' = e1' .. fnm' = em' :: d :: permutes_field_name_expr
{{ coq (Permutation [[fn1 e1..fnn en]] [[fn1' e1'..fnm' em']]) }}
{{ hol (PERM ([[fn1 e1..fnn en]]) ([[fn1' e1'..fnm' em']])) }}
{{ isa (perm ([[fn1 e1..fnn en]]) ([[fn1' e1'..fnm' em']])) }}
| |- value notmatches pattern :: :: does_not_match
{{ tex \neg([[value]]~\ottkw{matches}~[[pattern]]) }}
{{ coq (~JM_matchP [[value]] [[pattern]]) }}
{{ hol (~JM_matchP [[value]] [[pattern]]) }}
{{ isa (~(([[value]], [[pattern]]) : JM_matchP)) }}
| constant noteq constant' :: :: different_consts
{{ ich (~([[constant]] = [[constant']])) }}
| name noteq name' :: :: different_names
{{ ich (~([[name]] = [[name']])) }}
| store ( location ) unallocated :: :: store_unallocated
{{ coq (forall v8, ~JSlookup [[store]] [[location]] v8) }}
{{ hol (!v8. ~JSlookup [[store]] [[location]] v8) }}
{{ isa (! v8. ~(([[store]], [[location]], v8) : JSlookup )) }}
| type_vars ( let_binding ) gives typevar1 , .. , typevarn :: :: typevars_of_let_gives
{{ ich (ftv_let_binding [[let_binding]] = [[typevar1..typevarn]]) }}
| type_vars ( letrec_bindings ) gives typevar1 , .. , typevarn :: :: typevars_of_letrec_gives
{{ ich (ftv_letrec_bindings [[letrec_bindings]] = [[typevar1..typevarn]]) }}
grammar
terminals :: terminals_ ::=
{{ com prettyprinting specifications }}
| %prim :: :: prim {{ tex \ottkw{\%prim} }}
| * :: :: star {{ tex \ast }}
| ---> :: :: vararrow {{ tex \rightarrow }}
| --> :: :: red {{ tex \longrightarrow }}
| -> :: :: arrow {{ tex \rightarrow }}
| <- :: :: leftarrow {{ tex \!\!\leftarrow\!\! }}
| '<<' :: :: substl {{ tex \{\!\!\{ }}
| <= :: :: le {{ tex \leq }}
| == :: :: equiv {{ tex \equiv }}
| >= :: :: ge {{ tex \geq }}
| '>>' :: :: substr {{ tex \}\!\!\} }}
| '[^' :: :: qltl {{ tex ^{ }}
| '^]' :: :: qltr {{ tex } }}
| forall :: :: forall {{ tex \forall }}
| gives :: :: gives {{ tex \;\vartriangleright\;\ottmaybebreakline }}
| notin :: :: notin {{ tex \notin }}
| noteq :: :: noteq {{ tex \not = }}
| |- :: :: turnstile {{ tex \vdash }}
| |-> :: :: mapsto {{ tex \mapsto }}
| ~- :: :: uminus {{ tex \mathrel{\sim\!\!-} }}
embed {{ hol
val _ = Define
`fold_pat pats expr = FOLDR (\p e. Expr_function (PM_pm [PE_inj p e])) expr pats`;
val _ = ottDefine "shiftt"
`([[:user_syntax__typexpr:shift m n typevar]] = [[:user_syntax__typexpr:typevar]]) /\
([[:user_syntax__typexpr:shift m n <idx, num>]] =
if [[idx < m]] then [[:user_syntax__typexpr:<idx, num>]] else [[:user_syntax__typexpr:<idx+n, num>]]) /\
([[:user_syntax__typexpr:shift m n _]] = [[:user_syntax__typexpr:_]]) /\
([[:user_syntax__typexpr:shift m n (typexpr1->typexpr2)]] =
[[:user_syntax__typexpr:(shift m n typexpr1)->(shift m n typexpr2)]]) /\
(shiftt m n (TE_tuple typexprs) = TE_tuple (MAP (shiftt m n) typexprs)) /\
(shiftt m n (TE_constr typexprs tc) = TE_constr (MAP (shiftt m n) typexprs) tc)`;
val _ = Define
`(shifttes m n (typexprs_inj tes) = typexprs_inj (MAP (shiftt m n) tes))`;
val _ = Define
`([[shift m n forall typexpr]] = [[forall shift (m + 1) n typexpr]])`;
val _ = Define
`([[:user_syntax__environment_binding:shift m n TV]] = [[:user_syntax__environment_binding:TV]]) /\
([[:user_syntax__environment_binding:shift m n value_name:typescheme]] =
[[:user_syntax__environment_binding:value_name : shift m n typescheme]]) /\
([[:user_syntax__environment_binding:shift m n constr_name of typeconstr]] =
[[:user_syntax__environment_binding:constr_name of typeconstr]]) /\
([[:user_syntax__environment_binding:shift m n constr_name of forall type_params_opt, (typexprs) : typeconstr]] =
[[:user_syntax__environment_binding:constr_name of forall type_params_opt, (shift m n typexprs) : typeconstr]]) /\
([[:user_syntax__environment_binding:shift m n field_name:forall type_params_opt, typeconstr_name -> typexpr]] =
[[:user_syntax__environment_binding:field_name:forall type_params_opt, typeconstr_name -> shift m n typexpr]]) /\
([[:user_syntax__environment_binding:shift m n typeconstr_name:kind]] =
[[:user_syntax__environment_binding:typeconstr_name:kind]]) /\
(shiftEB m n (EB_tr tcn k field_names) = EB_tr tcn k field_names) /\
([[:user_syntax__environment_binding:shift m n type_params_opt typeconstr_name = typexpr]] =
[[:user_syntax__environment_binding:type_params_opt typeconstr_name = shift m n typexpr]]) /\
([[:user_syntax__environment_binding:shift m n location: typexpr]] =
[[:user_syntax__environment_binding:location: shift m n typexpr]])`;
val num_tv_def = Define
`(num_tv [] = 0:num) /\
(num_tv (EB_tv::E) = 1 + num_tv E) /\
(num_tv (EB::E) = num_tv E)`;
val _ = Define
`(shiftE m n [] = []) /\
(shiftE m n (EB::E) = shiftEB (m + num_tv E) n EB::shiftE m n E)`;
val _ = Define
`(shiftTsig m n Tsig = MAP (\(tv, t). (tv, shiftt m n t)) Tsig)`;
val _ = Define
`(definitions_snoc Ds_nil d = Ds_cons d Ds_nil) /\
(definitions_snoc (Ds_cons d ds) d' = Ds_cons d (definitions_snoc ds d'))`;
val _ = ottDefine "remv_tyvar_typexpr"
`(remv_tyvar_typexpr (TE_var typevar) = TE_any) /\
(remv_tyvar_typexpr (TE_idxvar idx num) = TE_idxvar idx num) /\
(remv_tyvar_typexpr TE_any = TE_any) /\
(remv_tyvar_typexpr (TE_arrow typexpr1 typexpr2) =
TE_arrow (remv_tyvar_typexpr typexpr1) (remv_tyvar_typexpr typexpr2)) /\
(remv_tyvar_typexpr (TE_tuple (typexpr_list)) =
TE_tuple (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list)) /\
(remv_tyvar_typexpr (TE_constr (typexpr_list) typeconstr) =
TE_constr (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list) typeconstr)`;
val _ = ottDefine "remv_tyvar_pattern"
`(remv_tyvar_pattern (P_var value_name) = P_var value_name) /\
(remv_tyvar_pattern P_any = P_any) /\
(remv_tyvar_pattern (P_constant constant) = P_constant constant) /\
(remv_tyvar_pattern (P_alias pattern value_name) =
P_alias (remv_tyvar_pattern pattern) value_name) /\
(remv_tyvar_pattern (P_typed pattern typexpr) =
P_typed (remv_tyvar_pattern pattern) (remv_tyvar_typexpr typexpr)) /\
(remv_tyvar_pattern (P_or pattern1 pattern2) =
P_or (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)) /\
(remv_tyvar_pattern (P_construct constr (pattern_list)) =
P_construct constr (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\
(remv_tyvar_pattern (P_construct_any constr) = P_construct_any constr) /\
(remv_tyvar_pattern (P_tuple (pattern_list)) =
P_tuple (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\
(remv_tyvar_pattern (P_record (field_pattern_list)) =
P_record (MAP (\(field_,pattern_). (field_,(remv_tyvar_pattern pattern_))) field_pattern_list)) /\
(remv_tyvar_pattern (P_cons pattern1 pattern2) =
P_cons (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2))`;
val _ = ottDefine "remv_tyvar_letrec_binding"
`(remv_tyvar_letrec_binding (LRB_simple value_name pattern_matching) =
LRB_simple value_name (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_letrec_bindings (LRBs_inj (letrec_binding_list)) =
LRBs_inj (MAP (\letrec_binding_. (remv_tyvar_letrec_binding letrec_binding_)) letrec_binding_list)) /\
(remv_tyvar_let_binding (LB_simple pattern expr) =
LB_simple (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\
(remv_tyvar_pat_exp (PE_inj pattern expr) =
PE_inj (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\
(remv_tyvar_pattern_matching (PM_pm (pat_exp_list)) =
PM_pm (MAP (\pat_exp_. (remv_tyvar_pat_exp pat_exp_)) pat_exp_list)) /\
(remv_tyvar_expr (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\
(remv_tyvar_expr (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\
(remv_tyvar_expr (Expr_ident value_name) = Expr_ident value_name) /\
(remv_tyvar_expr (Expr_constant constant) = Expr_constant constant) /\
(remv_tyvar_expr (Expr_typed expr typexpr) =
Expr_typed (remv_tyvar_expr expr) (remv_tyvar_typexpr typexpr)) /\
(remv_tyvar_expr (Expr_tuple (expr_list)) =
Expr_tuple (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\
(remv_tyvar_expr (Expr_construct constr (expr_list)) =
Expr_construct constr (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\
(remv_tyvar_expr (Expr_cons expr1 expr2) =
Expr_cons (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_record (field_expr_list)) =
Expr_record (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\
(remv_tyvar_expr (Expr_override expr (field_expr_list)) =
Expr_override (remv_tyvar_expr expr)
(MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\
(remv_tyvar_expr (Expr_apply expr1 expr2) =
Expr_apply (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_and expr1 expr2) =
Expr_and (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_or expr1 expr2) =
Expr_or (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_field expr field) = Expr_field (remv_tyvar_expr expr) field) /\
(remv_tyvar_expr (Expr_ifthenelse expr0 expr1 expr2) =
Expr_ifthenelse (remv_tyvar_expr expr0) (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_while expr1 expr2) =
Expr_while (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_for x expr1 for_dirn expr2 expr3) =
Expr_for x (remv_tyvar_expr expr1) for_dirn (remv_tyvar_expr expr2) (remv_tyvar_expr expr3))/\
(remv_tyvar_expr (Expr_sequence expr1 expr2) =
Expr_sequence (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_match expr pattern_matching) =
Expr_match (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_expr (Expr_function pattern_matching) =
Expr_function (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_expr (Expr_let let_binding expr) =
Expr_let (remv_tyvar_let_binding let_binding) (remv_tyvar_expr expr)) /\
(remv_tyvar_expr (Expr_letrec letrec_bindings expr) =
Expr_letrec (remv_tyvar_letrec_bindings letrec_bindings) (remv_tyvar_expr expr)) /\
(remv_tyvar_expr (Expr_location location) = Expr_location location)`;
}}
embed {{ isa
constdefs fold_pat :: "pattern list => expr => expr"
"fold_pat pats expr == foldr (% p e. Expr_function (PM_pm [PE_inj p e])) pats expr"
consts shiftt :: "nat => nat => typexpr => typexpr"
(*
primrec
"([[:user_syntax__typexpr:shift m n typevar]] = [[:user_syntax__typexpr:typevar]])"
" ([[:user_syntax__typexpr:shift m n <idx, num>]] =
(if [[idx < m]] then [[:user_syntax__typexpr:<idx, num>]] else [[:user_syntax__typexpr:<idx+n, num>]]) "
" ([[:user_syntax__typexpr:shift m n _]] = [[:user_syntax__typexpr:_]])) "
" ([[:user_syntax__typexpr:shift m n (typexpr1->typexpr2)]] =
[[:user_syntax__typexpr:(shift m n typexpr1)->(shift m n typexpr2)]]) "
" (shiftt m n (TE_tuple typexprs) = TE_tuple (map (shiftt m n) typexprs)) "
" (shiftt m n (TE_constr typexprs tc) = TE_constr (map (shiftt m n) typexprs) tc)"
FIXMEdoesn't like recursive call in last clause
*)
consts shifttes :: "nat => nat => typexprs => typexprs"
(*
primrec
"(shifttes m n (typexprs_inj tes) == typexprs_inj (map (shiftt m n) tes))"
FIXME doesn't like rec call
*)
consts shiftts :: "nat => nat => typescheme => typescheme"
(*
primrec
"([[shift m n forall typexpr]] = [[forall shift (m + 1) n typexpr]])"
FIXME
*)
consts shiftEB :: "nat => nat => environment_binding => environment_binding"
primrec
"([[:user_syntax__environment_binding:shift m n TV]] = [[:user_syntax__environment_binding:TV]])"
"([[:user_syntax__environment_binding:shift m n value_name:typescheme]] =
[[:user_syntax__environment_binding:value_name : shift m n typescheme]])"
" ([[:user_syntax__environment_binding:shift m n constr_name of typeconstr]] =
[[:user_syntax__environment_binding:constr_name of typeconstr]]) "
" ([[:user_syntax__environment_binding:shift m n constr_name of forall type_params_opt, (typexprs) : typeconstr]] =
[[:user_syntax__environment_binding:constr_name of forall type_params_opt, (shift m n typexprs) : typeconstr]]) "
" ([[:user_syntax__environment_binding:shift m n field_name:forall type_params_opt, typeconstr_name -> typexpr]] =
[[:user_syntax__environment_binding:field_name:forall type_params_opt, typeconstr_name -> shift m n typexpr]]) "
" ([[:user_syntax__environment_binding:shift m n typeconstr_name:kind]] =
[[:user_syntax__environment_binding:typeconstr_name:kind]]) "
" (shiftEB m n (EB_tr tcn k field_names) = EB_tr tcn k field_names) "
" ([[:user_syntax__environment_binding:shift m n type_params_opt typeconstr_name = typexpr]] =
[[:user_syntax__environment_binding:type_params_opt typeconstr_name = shift m n typexpr]]) "
" ([[:user_syntax__environment_binding:shift m n location: typexpr]] =
[[:user_syntax__environment_binding:location: shift m n typexpr]])"
consts num_tv :: "environment => nat"
primrec
"(num_tv [] = (0::nat)) "
"(num_tv (eb#e) = (if eb = EB_tv then 1 else 0) + num_tv e)"
consts shiftE :: "nat => nat => environment => environment"
primrec
"(shiftE m n [] = []) "
" (shiftE m n (EB#E) = shiftEB (m + num_tv E) n EB#shiftE m n E)"
constdefs shiftTsig :: "nat => nat => ('a * typexpr) list => ('a * typexpr) list"
"(shiftTsig m n Tsig == map (%(tv, t). (tv, shiftt m n t)) Tsig)"
consts definitions_snoc :: "definitions => caml_definition => definitions"
primrec
"(definitions_snoc Ds_nil d = Ds_cons d Ds_nil) "
"(definitions_snoc (Ds_cons d ds) d' = Ds_cons d (definitions_snoc ds d'))"
consts remv_tyvar_typexpr :: "typexpr => typexpr"
(*
val _ = ottDefine "remv_tyvar_typexpr"
`(remv_tyvar_typexpr (TE_var typevar) = TE_any) /\
(remv_tyvar_typexpr (TE_idxvar idx num) = TE_idxvar idx num) /\
(remv_tyvar_typexpr TE_any = TE_any) /\
(remv_tyvar_typexpr (TE_arrow typexpr1 typexpr2) =
TE_arrow (remv_tyvar_typexpr typexpr1) (remv_tyvar_typexpr typexpr2)) /\
(remv_tyvar_typexpr (TE_tuple (typexpr_list)) =
TE_tuple (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list)) /\
(remv_tyvar_typexpr (TE_constr (typexpr_list) typeconstr) =
TE_constr (MAP (\typexpr_. (remv_tyvar_typexpr typexpr_)) typexpr_list) typeconstr)`;
*)
consts remv_tyvar_pattern :: "pattern => pattern"
(*
`(remv_tyvar_pattern (P_var value_name) = P_var value_name) /\
(remv_tyvar_pattern P_any = P_any) /\
(remv_tyvar_pattern (P_constant constant) = P_constant constant) /\
(remv_tyvar_pattern (P_alias pattern value_name) =
P_alias (remv_tyvar_pattern pattern) value_name) /\
(remv_tyvar_pattern (P_typed pattern typexpr) =
P_typed (remv_tyvar_pattern pattern) (remv_tyvar_typexpr typexpr)) /\
(remv_tyvar_pattern (P_or pattern1 pattern2) =
P_or (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2)) /\
(remv_tyvar_pattern (P_construct constr (pattern_list)) =
P_construct constr (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\
(remv_tyvar_pattern (P_construct_any constr) = P_construct_any constr) /\
(remv_tyvar_pattern (P_tuple (pattern_list)) =
P_tuple (MAP (\pattern_. (remv_tyvar_pattern pattern_)) pattern_list)) /\
(remv_tyvar_pattern (P_record (field_pattern_list)) =
P_record (MAP (\(field_,pattern_). (field_,(remv_tyvar_pattern pattern_))) field_pattern_list)) /\
(remv_tyvar_pattern (P_cons pattern1 pattern2) =
P_cons (remv_tyvar_pattern pattern1) (remv_tyvar_pattern pattern2))`;
*)
consts remv_tyvar_letrec_binding :: "letrec_binding => letrec_binding"
(*
`(remv_tyvar_letrec_binding (LRB_simple value_name pattern_matching) =
LRB_simple value_name (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_letrec_bindings (LRBs_inj (letrec_binding_list)) =
LRBs_inj (MAP (\letrec_binding_. (remv_tyvar_letrec_binding letrec_binding_)) letrec_binding_list)) /\
(remv_tyvar_let_binding (LB_simple pattern expr) =
LB_simple (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\
(remv_tyvar_pat_exp (PE_inj pattern expr) =
PE_inj (remv_tyvar_pattern pattern) (remv_tyvar_expr expr)) /\
(remv_tyvar_pattern_matching (PM_pm (pat_exp_list)) =
PM_pm (MAP (\pat_exp_. (remv_tyvar_pat_exp pat_exp_)) pat_exp_list)) /\
(remv_tyvar_expr (Expr_uprim unary_prim) = Expr_uprim unary_prim) /\
(remv_tyvar_expr (Expr_bprim binary_prim) = Expr_bprim binary_prim) /\
(remv_tyvar_expr (Expr_ident value_name) = Expr_ident value_name) /\
(remv_tyvar_expr (Expr_constant constant) = Expr_constant constant) /\
(remv_tyvar_expr (Expr_typed expr typexpr) =
Expr_typed (remv_tyvar_expr expr) (remv_tyvar_typexpr typexpr)) /\
(remv_tyvar_expr (Expr_tuple (expr_list)) =
Expr_tuple (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\
(remv_tyvar_expr (Expr_construct constr (expr_list)) =
Expr_construct constr (MAP (\expr_. (remv_tyvar_expr expr_)) expr_list)) /\
(remv_tyvar_expr (Expr_cons expr1 expr2) =
Expr_cons (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_record (field_expr_list)) =
Expr_record (MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\
(remv_tyvar_expr (Expr_override expr (field_expr_list)) =
Expr_override (remv_tyvar_expr expr)
(MAP (\(field_,expr_). (field_,(remv_tyvar_expr expr_))) field_expr_list)) /\
(remv_tyvar_expr (Expr_apply expr1 expr2) =
Expr_apply (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_and expr1 expr2) =
Expr_and (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_or expr1 expr2) =
Expr_or (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_field expr field) = Expr_field (remv_tyvar_expr expr) field) /\
(remv_tyvar_expr (Expr_ifthenelse expr0 expr1 expr2) =
Expr_ifthenelse (remv_tyvar_expr expr0) (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_while expr1 expr2) =
Expr_while (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_for x expr1 for_dirn expr2 expr3) =
Expr_for x (remv_tyvar_expr expr1) for_dirn (remv_tyvar_expr expr2) (remv_tyvar_expr expr3))/\
(remv_tyvar_expr (Expr_sequence expr1 expr2) =
Expr_sequence (remv_tyvar_expr expr1) (remv_tyvar_expr expr2)) /\
(remv_tyvar_expr (Expr_match expr pattern_matching) =
Expr_match (remv_tyvar_expr expr) (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_expr (Expr_function pattern_matching) =
Expr_function (remv_tyvar_pattern_matching pattern_matching)) /\
(remv_tyvar_expr (Expr_let let_binding expr) =
Expr_let (remv_tyvar_let_binding let_binding) (remv_tyvar_expr expr)) /\
(remv_tyvar_expr (Expr_letrec letrec_bindings expr) =
Expr_letrec (remv_tyvar_letrec_bindings letrec_bindings) (remv_tyvar_expr expr)) /\
(remv_tyvar_expr (Expr_location location) = Expr_location location)`;
*)
}}
{{ coq
(*** Coercions and syntactic sugar ***)
(* Names *)
Coercion VP_name : value_name >-> value_path.
Coercion C_name : constr_name >-> constr.
Coercion TC_name : typeconstr_name >-> typeconstr.
(* Constants *)
Coercion CONST_int : intn >-> constant.
Definition CONST_int' : Z -> constant := CONST_int.
Coercion CONST_int' : Z >-> constant.
Definition CONST_bool (b:bool) := if b then CONST_true else CONST_false.
Coercion CONST_bool : bool >-> constant.
Definition CONST_unit' (_:unit) := CONST_unit.
Coercion CONST_unit' : unit >-> constant.
(* Types *)
Definition TPS_proj (tpo:type_params_opt) := let (tvs) := tpo in tvs.
Coercion TPS_proj : type_params_opt >-> list.
Coercion TE_var : typevar >-> typexpr.
Definition TE_constr0 := TE_constr nil.
Coercion TE_constr0 : typeconstr >-> typexpr.
Definition typexprs_proj (tes:typexprs) := let (ts) := tes in ts.
Coercion typexprs_proj : typexprs >-> list.
(* Patterns *)
Coercion P_var : value_name >-> pattern.
Coercion P_constant : constant >-> pattern.
(* Expressions *)
Coercion Expr_uprim : unary_prim >-> expr.
Coercion Expr_bprim : binary_prim >-> expr.
Coercion Expr_ident : value_name >-> expr.
Coercion Expr_constant : constant >-> expr.
Definition subst_x x e := substs_x_xs (cons (x, e) nil).
(* Definitions *)
Fixpoint Ds_proj (ds:definitions) : list definition :=
match ds with
| Ds_nil => nil
| Ds_cons d dt => cons d (Ds_proj dt)
end.
Coercion Ds_proj : definitions >-> list.
Fixpoint Ds_list (ds:list definition) : definitions :=
match ds with
| nil => Ds_nil
| cons d dt => Ds_cons d (Ds_list dt)
end.
(* Semantic objects *)
Definition substs_x_proj (z:substs_x) := let (y) := z in y.
Coercion substs_x_proj : substs_x >-> list.
Coercion TE_te : typexpr >-> type_equation.
Coercion TI_eq : type_equation >-> type_information.
Coercion TI_def : type_representation >-> type_information.
(*** Strings ***)
Section string_literals.
Import String.
Open Local Scope string_scope.
Definition string_equal_functional_value := "equal: functional value".
End string_literals.
(*** Auxiliary functions ***)
Definition fold_pats pats e0 :=
fold_right (fun p e => Expr_function (PM_pm (PE_inj p e :: nil))) e0 pats.
Definition definitions_snoc (ds:definitions) (d:definition) : definitions :=
Ds_list (ds ++ d :: nil).
Fixpoint remv_tyvar_typexpr (t:typexpr) : typexpr :=
match t with
| TE_var tv => TE_any
| TE_idxvar k p => TE_idxvar k p
| TE_any => TE_any
| TE_arrow t1 t2 => TE_arrow (remv_tyvar_typexpr t1) (remv_tyvar_typexpr t2)
| TE_tuple ts => TE_tuple (map remv_tyvar_typexpr ts)
| TE_constr ts tc => TE_constr (map remv_tyvar_typexpr ts) tc
end.
Fixpoint remv_tyvar_pattern (p:pattern) : pattern :=
match p with
| P_var vn => P_var vn
| P_any => P_any
| P_constant c => P_constant c
| P_alias p vn => P_alias (remv_tyvar_pattern p) vn
| P_typed p t => P_typed (remv_tyvar_pattern p) (remv_tyvar_typexpr t)
| P_or p1 p2 => P_or (remv_tyvar_pattern p1) (remv_tyvar_pattern p2)
| P_construct cr ps => P_construct cr (map remv_tyvar_pattern ps)
| P_construct_any cr => P_construct_any cr
| P_tuple ps => P_tuple (map remv_tyvar_pattern ps)
| P_record fps => P_record (map (fun tmp => match tmp with (fi,pi) => (fi, remv_tyvar_pattern pi) end) fps)
| P_cons p1 p2 => P_cons (remv_tyvar_pattern p1) (remv_tyvar_pattern p2)
end.
Fixpoint remv_tyvar_letrec_binding (lrb:letrec_binding) : letrec_binding :=
match lrb with
| LRB_simple vn pm => LRB_simple vn (remv_tyvar_pattern_matching pm)
end
with remv_tyvar_letrec_bindings (lrbs:letrec_bindings) : letrec_bindings :=
match lrbs with
| LRBs_inj lrbs => LRBs_inj (map remv_tyvar_letrec_binding lrbs)
end
with remv_tyvar_let_binding (lb:let_binding) : let_binding :=
match lb with
| LB_simple p e => LB_simple (remv_tyvar_pattern p) (remv_tyvar_expr e)
end
with remv_tyvar_pat_exp (pe:pat_exp) : pat_exp :=
match pe with
| PE_inj p e => PE_inj (remv_tyvar_pattern p) (remv_tyvar_expr e)
end
with remv_tyvar_pattern_matching (pm:pattern_matching) : pattern_matching :=
match pm with
| PM_pm pes => PM_pm (map remv_tyvar_pat_exp pes)
end
with remv_tyvar_expr (e:expr) : expr :=
match e with
| Expr_uprim uprim => Expr_uprim uprim
| Expr_bprim bprim => Expr_bprim bprim
| Expr_ident vn => Expr_ident vn
| Expr_constant c => Expr_constant c
| Expr_typed e t => Expr_typed (remv_tyvar_expr e) (remv_tyvar_typexpr t)
| Expr_tuple es => Expr_tuple (map remv_tyvar_expr es)
| Expr_construct cr es => Expr_construct cr (map remv_tyvar_expr es)
| Expr_cons e1 e2 => Expr_cons (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_record fes => Expr_record (map (fun tmp => match tmp with (fi, ei) => (fi, remv_tyvar_expr ei) end) fes)
| Expr_override e fes => Expr_override (remv_tyvar_expr e) (map (fun tmp => match tmp with (fi, ei) => (fi, remv_tyvar_expr ei) end) fes)
| Expr_apply e1 e2 => Expr_apply (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_and e1 e2 => Expr_and (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_or e1 e2 => Expr_or (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_field e f => Expr_field (remv_tyvar_expr e) f
| Expr_ifthenelse e0 e1 e2 => Expr_ifthenelse (remv_tyvar_expr e0) (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_while e1 e2 => Expr_while (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_for x e1 fdn e2 e3 => Expr_for x (remv_tyvar_expr e1) fdn (remv_tyvar_expr e2) (remv_tyvar_expr e3)
| Expr_sequence e1 e2 => Expr_sequence (remv_tyvar_expr e1) (remv_tyvar_expr e2)
| Expr_match e pm => Expr_match (remv_tyvar_expr e) (remv_tyvar_pattern_matching pm)
| Expr_function pm => Expr_function (remv_tyvar_pattern_matching pm)
| Expr_let lb e => Expr_let (remv_tyvar_let_binding lb) (remv_tyvar_expr e)
| Expr_letrec lrbs e => Expr_letrec (remv_tyvar_letrec_bindings lrbs) (remv_tyvar_expr e)
| Expr_location loc => Expr_location loc
end.
(*** De Bruijn indices ***)
Fixpoint shiftt (m n:nat) (te:typexpr) {struct te} : typexpr :=
match te with
| TE_var tv => TE_var tv
| TE_idxvar k p => TE_idxvar (if le_lt_dec m k then n + k else k) p
| TE_any => TE_any
| TE_arrow te1 te2 => TE_arrow (shiftt m n te1) (shiftt m n te2)
| TE_tuple tes => TE_tuple (map (shiftt m n) tes)
| TE_constr tes tc => TE_constr (map (shiftt m n) tes) tc
end.
Definition shifttes m n (tes:typexprs) :=
typexprs_inj (map (shiftt m n) tes).
Definition shiftts m n (ts:typescheme) :=
match ts with
| TS_forall te => TS_forall (shiftt (S m) n te)
end.
Definition shiftEB m n (EB:environment_binding) :=
match EB with
| EB_tv => EB_tv
| EB_vn vn ts => EB_vn vn (shiftts m n ts)
| EB_cc cn tc => EB_cc cn tc
| EB_pc cn tpo tes tc => EB_pc cn tpo (shifttes m n tes) tc
| EB_fn fn tpo tcn te => EB_fn fn tpo tcn (shiftt m n te)
| EB_td tcn K => EB_td tcn K
| EB_tr tcn K fns => EB_tr tcn K fns
| EB_ta tpo tcn te => EB_ta tpo tcn (shiftt m n te)
| EB_l loc te => EB_l loc (shiftt m n te)
end.
Fixpoint count_E_typevars E :=
match E with
| nil => 0
| EB_tv :: E' => S (count_E_typevars E')
| _ :: E' => count_E_typevars E'
end.
Fixpoint shiftE (m n:nat) (E:environment) {struct E} : environment :=
match E with
| nil => nil
| EB :: E' => shiftEB (count_E_typevars E + m) n EB :: shiftE m n E'
end.
Definition shiftTsig m n (sigma:Tsigma) :=
map (fun tmp => match tmp with (tv, t) => (tv, shiftt m n t) end) sigma.
}}