From 61a408ee5571de54759a7efe4f9a5ccf2dd4d57a Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Thu, 4 Dec 2014 12:58:19 +0000 Subject: ott rules for type checking pattern match --- language/l2_rules.ott | 188 ++++++++++++++++++++++++++++---------------------- language/l2_typ.ott | 5 +- 2 files changed, 108 insertions(+), 85 deletions(-) diff --git a/language/l2_rules.ott b/language/l2_rules.ott index df6d16e9..5cdf762b 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -92,9 +92,8 @@ formula :: formula_ ::= {{ ichl ([[S_N1]] = [[S_N2]]) }} | id == 'id :: :: id_eq - | x1 NOTEQ x2 :: :: id_neq - + | lit1 NOTEQ lit2 :: ::lit_neq | I1 == I2 :: :: I_eqn {{ ichl ([[I1]] = [[I2]]) }} @@ -461,7 +460,7 @@ E_d |- range ~< range, { ne3 <= ne1, ne2 <= ne4 } E_d |- t ~< t', S_N ---------------------------------------------------------- :: vector -E_d |- vector ~< vector , {ne1=ne3,ne2=ne3} u+ S_N +E_d |- vector ~< vector , {ne1=ne3,ne2=ne3} u+ S_N E_k(x) gives K_Lam (k1 .. kn -> K_Typ) ,k1 |- t_arg1 ~< t_arg'1,S_N1 .. ,kn |- t_argn ~< t_arg'n,S_Nn @@ -504,16 +503,16 @@ E_d, (u1 , .. , un) |- exp : (t1 , .. , tn) gives (u1 , .. , un), exp', S_N1 u+ E_d |- u ~< t,S_N exp' == (annot) exp ------------------------------------------------- :: vectorUpdateStart -E_d, vector< ne1 ne2 ord t > |- exp : vector gives vector , exp', S_N u+ {ne2=ne4}, pure +E_d, vector< ne1 ne2 order t > |- exp : vector gives vector , exp', S_N u+ {ne2=ne4}, pure E_d |- u ~< bit, S_N exp' == to_num exp -------------------------------------------------- :: toNum -E_d, range |- exp : vector gives range, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure +E_d, range |- exp : vector gives range, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure exp' == to_vec exp -------------------------------------- :: fromNum -E_d, vector |- exp: range gives vector,exp', {ne3 = zero, ne4 <= 2** ne2}, pure +E_d, vector |- exp: range gives vector,exp', {ne3 = zero, ne4 <= 2** ne2}, pure E_d |- typ ~> t exp' == (typ) exp @@ -523,7 +522,7 @@ E_d, u |- exp : register gives t', exp'', S_N, {rreg} exp' == exp[numZero] -------------------------------------- :: accessVecBit -E_d, bit |- exp : vector gives bit,exp', { ne1=one},pure +E_d, bit |- exp : vector gives bit,exp', { ne1=one},pure E_d |- range ~< range,S_N exp' == switch exp { case bitzero -> numZero case bitone -> numOne} @@ -557,47 +556,45 @@ defns check_lit :: '' ::= defn -t |- lit : t' => lit' , S_N :: :: check_lit :: check_lit_ +t |- lit : t' => exp , S_N :: :: check_lit :: check_lit_ {{ com Typing literal constants, coercing to expected type t }} by - - ------------------------------------------------------------ :: true -bit |- true : bool => bitone, {} - - ------------------------------------------------------------ :: false -bit |- false : bool => bitzero, {} + ------------------------------------------------------------ :: num -range |- num : range < num, zero> => num , { nexp <= num, num <= nexp' } +range |- num : range < num num> => num , { ne <= num, num <= ne' } + + ------------------------------------------------------------ :: numToVec +vector |- num : range < num num> => to_vec num , { num + one <= 2**ne' } - num = 0 ------------------------------------------------------------ :: numbitzero - bit |- num : range < num, zero> => bitzero, {} + bit |- numZero : range < zero zero> => bitzero, {} - num = 1 ------------------------------------------------------------ :: numbitone - bit |- num : range < num, zero> => bitone, {} + bit |- numOne : range < one one> => bitone, {} ------------------------------------------------------------- :: string - string |- string : string, {} + string |- :L_string: string : :T_string_typ: string => :E_lit: string, {} - num = bitlength(hex) + ne == bitlength(hex) ------------------------------------------------------------ :: hex - |- hex : vector zero num inc :T_id: bit + vector |- hex : vector< ne1 ne order bit> => hex, {ne=ne2} - num = bitlength(bin) +ne == bitlength(bin) ------------------------------------------------------------ :: bin - |- bin : vector zero num inc :T_id: bit +vector |- bin : vector< ne1 ne order bit> => bin, {ne=ne2} ------------------------------------------------------------ :: unit - |- () : unit +unit |- () : unit => unit, {} ------------------------------------------------------------ :: bitzero - |- bitzero : bit +bit |- bitzero : bit => bitzero, {} ------------------------------------------------------------ :: bitone - |- bitone : bit +bit |- bitone : bit => bitzero, {} +------------------------------------------------------------ :: undef +t |- undefined : t => undefined, {} defns check_pat :: '' ::= @@ -607,88 +604,111 @@ E , t |- pat : t' gives pat' , E_t , S_N :: :: check_pat :: check_pat_ {{ com Typing patterns, building their binding environment }} by -|- lit : t +lit NOTEQ undefined +t |- lit : u => lit',S_N +E_d |- u ~< t,S_N' ------------------------------------------------------------ :: lit -E |- lit : t gives {}, {} +, t |- lit : u gives lit', {}, S_N u+ S_N' -E_k |-t t ok ------------------------------------------------------------ :: wild -> |- _ : t gives {}, {} +E, t |- _ : t gives _, {}, {} -E |- pat : t gives E_t1,S_N +E,t |- pat : u gives pat',E_t1,S_N id NOTIN dom(E_t1) ------------------------------------------------------------ :: as -E |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N +E,t |- (pat as id) : u gives (pat' as id), (E_t1 u+ {id|->t}),S_N - |- pat : t gives E_t1,S_N -E_t(id) gives {}, {}, Default, t ------------------------------------------------------------- :: as_default - |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N +,t' |- pat : t gives pat', E_t1,S_N +E_t(id) gives {}, {}, Default, t' +E_d |- t' ~< u,S_N' +------------------------------------------------------------ :: asDefault +,u |- (pat as id) : t gives (pat' as id), (E_t1 u+ {id|->t'}),S_N u+ S_N' E_d |- typ ~> t - |- pat : t gives E_t1,S_N +,t |- pat : t gives pat',E_t1,S_N ------------------------------------------------------------ :: typ - |- (typ) pat : t gives E_t1,S_N +,u |- (typ) pat : t gives pat',E_t1,S_N -E_t(id) gives (t1*..*tn) -> id t_args { } Ctor - |- pat1 : t1 gives E_t1,S_N1 .. |- patn : tn gives E_tn,S_Nn +E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, (u'1,..,u'n) -> x < t_arg1 .. t_argm > pure +(u1,..,un) -> x pure == (u'1,..,u'n) -> x pure [t_arg1/tid1 .. t_argm/tidm] +,u1 |- pat1 : t1 gives pat'1,E_t1,S_N1 .. ,un |- patn : tn gives pat'n,E_tn,S_Nn disjoint doms(E_t1,..,E_tn) ------------------------------------------------------------- :: ident_constr - |- id(pat1, .., patn) : id t_args gives u+ E_t1 .. E_tn, S_N1 u+ .. u+ S_Nn +E_d |- x ~< t, S_N +------------------------------------------------------------ :: constr +,t |- id(pat1, .., patn) : x gives id(pat'1, ..,pat'n), u+ E_t1 .. E_tn, S_N u+ S_N1 u+ .. u+ S_Nn -E_k |-t t ok ------------------------------------------------------------- :: var -> |- :P_id: id : t gives (E_t u+ {id|->t}),{} + +E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, unit -> x < t_arg1 .. t_argm > pure +unit -> x pure == unit -> x pure [t_arg1/tid1 .. t_argm/tidm] +E_d |- x ~< t, S_N +------------------------------------------------------------- :: identConstr +, t |- :P_id: id : t gives :P_id: id, {}, S_N E_t(id) gives {},{},Default,t ------------------------------------------------------------- :: var_default - |- :P_id: id : t gives (E_t u+ {id|->t}),{} +E_d |- t ~< u, S_N +------------------------------------------------------------ :: varDefault +,u |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),S_N -E_r() gives id t_args, () -> |- pati : ti gives E_ti,S_Ni//i/> +------------------------------------------------------------ :: var +,t |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),{} + +E_r() gives x< t_args>, () +>,ti |- pati : ui gives pat'i, E_ti,S_Ni//i/> disjoint doms() + |- x ~< t,S_N ------------------------------------------------------------ :: record -> |- { semi_opt } : id t_args gives :E_t_multi_union: u+ , u+ +>,t |- { semi_opt } : x gives { semi_opt }, :E_t_multi_union: u+ , S_N u+ -E |- pat1 : t gives E_t1,S_N1 .. E |- patn : t gives E_tn,S_Nn -disjoint doms(E_t1 , .. , E_tn) -length(pat1 .. patn) = num +,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn +disjoint doms(E_t1, ... ,E_tn) +E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n +ne4==length(pat1 ... patn) +S_N ==S_N1 u+ ... u+ S_Nn +S_N' == S_N'1 u+ ... u+ S_N'n ----------------------------------------------------------- :: vector -E |- [ pat1 , .. , patn ] : vector :t_arg_nexp: 'x num+'x inc t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn - -%E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn -%disjoint doms(E_t1 , ... , E_tn) -%num1 lt ... lt numn -%----------------------------------------------------------- :: indexedVectorInc -%E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn), {'x<=num1, 'x2 >= numn + (- num1)} u+ S_N1 u+ ... u+ S_Nn - -%E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn -%disjoint doms(E_t1 , ... , E_tn) -%num1 gt ... gt numn -%----------------------------------------------------------- :: indexedVectorDec -%E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: 'x :t_arg_nexp: 'x2 dec t gives (E_t1 u+ ... u+ E_tn), {'x>=num1,'x2<=num1 +(-numn)} u+ S_N1 u+ ... u+ S_Nn - -%E |- pat1 : vector ne1 ne'1 inc t gives E_t1,S_N1 ... E |- patn : vector nen ne'n inc t gives E_tn,S_Nn -%disjoint doms(E_t1 , ... , E_tn) -%S_N0 = consistent_increase ne1 ne'1 ... nen ne'n -%----------------------------------------------------------- :: vectorConcatInc -%E |- pat1 : ... : patn : vector :t_arg_nexp: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x<=ne1,'x2>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn - -%E |- pat1 : vector ne1 ne'1 dec t gives E_t1,S_N1 ... E |- patn : vector nen ne'n dec t gives E_tn,S_Nn -%disjoint doms(E_t1 , ... , E_tn) -%S_N0 = consistent_decrease ne1 ne'1 ... nen ne'n -%----------------------------------------------------------- :: vectorConcatDec -%E |- pat1 : ... : patn : vector :t_arg_nexp: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x>=ne1,'x2>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn - -E |- pat1 : t1 gives E_t1,S_N1 .... E |- patn : tn gives E_tn,S_Nn +, vector |- [ pat1, ..., patn ] : vector< ne3 ne4 order u> gives [ pat'1, ..., pat'n ], (E_t1 u+ ... u+ E_tn), S_N u+ S_N' u+ {ne2=ne4} + +,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn +E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n +ne4 == length(pat1 ... patn) +disjoint doms(E_t1 , ... , E_tn) +num1 lt ... lt numn +S_N == S_N1 u+ ... u+ S_Nn +S_N' == S_N'1 u+ ... u+ S_N'n +----------------------------------------------------------- :: indexedVectorInc +, vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 inc t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1<=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn + +,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn +E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n +ne4 == length(pat1 ... patn) +disjoint doms(E_t1 , ... , E_tn) +num1 gt ... gt numn +S_N == S_N1 u+ ... u+ S_Nn +S_N' == S_N'1 u+ ... u+ S_N'n +----------------------------------------------------------- :: indexedVectorDec +, vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 dec t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1>=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn + +, vector |- pat1 : vector< ne''1 ne'1 order u1> gives pat'1, E_t1,S_N1 ... , vector |- pat1 : vector< ne''n ne'n order u1> gives pat'n, E_tn,S_Nn +E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n +disjoint doms(E_t1 , ... , E_tn) +S_N == S_N1 u+ ... u+ S_Nn +S_N' == S_N'1 u+ ... u+ S_N'n +----------------------------------------------------------- :: vectorConcat +, vector |- pat1 : ... : patn : vector gives pat'1 : ... : pat'n, (E_t1 u+ ... u+ E_tn),{ne'1 + ... + ne'n <= ne2} u+ S_N u+ S_N' + +E,t1 |- pat1 : u1 gives pat'1,E_t1,S_N1 .... E,tn |- patn : un gives pat'n,E_tn,S_Nn disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------ :: tup -E |- (pat1, ...., patn) : (t1 * .... * tn) gives (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn +E,(t1, .... , tn) |- (pat1, ...., patn) : (u1 , .... , un) gives (pat'1, .... , pat'n), (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn -E |- pat1 : t gives E_t1,S_N1 .. E |- patn : t gives E_tn,S_Nn +,t |- pat1 : u1 gives pat'1,E_t1,S_N1 .. ,t |- patn : un gives pat'n,E_tn,S_Nn disjoint doms(E_t1,..,E_tn) +E_d |- u1 ~< t,S_N'1 .. E_d |- un ~< t,S_N'n +disjoint doms(E_t1 , .. , E_tn) +S_N == S_N1 u+ .. u+ S_Nn +S_N' == S_N'1 u+ .. u+ S_N'n ------------------------------------------------------------ :: list -E |- [||pat1, .., patn ||] : list t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn +, list |- [||pat1, .., patn ||] : list< t> gives [|| pat'1, .. , pat'n ||],(E_t1 u+ .. u+ E_tn),S_N u+ S_N' defns diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 5c17c3f6..65857331 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -50,8 +50,11 @@ t , u :: 'T_' ::= | t |-> t1 :: :: abbrev | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} - | vector < ne ne' ord t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} + | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} + | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} | bit :: S :: bit_typ {{ ichlo T_id "bit" }} + | string :: S :: string_typ {{ ichlo T_id "string" }} + | unit :: S :: unit_typ {{ ichlo T_id "unit" }} | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} -- cgit v1.2.3