Changeset 14830


Ignore:
Timestamp:
10/03/08 13:16:02 (5 years ago)
Author:
tarrach
Message:

patterns are now comments and will not interfere with syntax highlighting

Location:
src
Files:
30 edited

Legend:

Unmodified
Added
Removed

  • src/cg/genalpha.ml

    r14219 r14830  
    2626let gen config str =  
    2727    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    28     "<Types>", (String.concat "\r\n" (List.map (fun tcons -> generateRule "free_type" (genPatternT "\t| T" tcons)) config.type_constructors)); 
    29     "<Constructors>", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.constructors)); 
    30     "<SConstructors>", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.constructors)); 
    31     "<Destructors>", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.destr_types)); 
    32     "<SDestructors>", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.destr_types)); 
     28    "(*<Types>*)", (String.concat "\r\n" (List.map (fun tcons -> generateRule "free_type" (genPatternT "\t| T" tcons)) config.type_constructors)); 
     29    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.constructors)); 
     30    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.constructors)); 
     31    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_m'" (genPatternICA "\t| " cons)) config.destr_types)); 
     32    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateRule "free_s'" (genPatternS "\t| " cons)) config.destr_types)); 
    3333    ] 

  • src/cg/genckind.ml

    r14219 r14830  
    4545let gen config str =  
    4646    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    47     "<Types>", (String.concat "" (List.map generateRule config.type_constructors)); 
     47    "(*<Types>*)", (String.concat "" (List.map generateRule config.type_constructors)); 
    4848    ] 

  • src/cg/gencompile.ml

    r14219 r14830  
    2525let gen config str =  
    2626    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    27     "<Compile>", config.compile 
     27    "(*<Compile>*)", config.compile 
    2828    ] 

  • src/cg/genfunctions.ml

    r14589 r14830  
    4444let gen config str =  
    4545    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    46     "<Ground>", (String.concat "\r\n" (List.map generateGround config.type_constructors)); 
    47     "<Generative>", (String.concat "\r\n" (List.map generateGenerative (List.filter (fun tcons->tcons.generative) config.type_constructors))); 
    48     "<SConstructors>", (String.concat "\r\n" (List.map generateSConstructors config.constructors)); 
    49     "<SDestructors>", (String.concat "\r\n" (List.map generateSDestructors config.destr_types)) 
     46    "(*<Ground>*)", (String.concat "\r\n" (List.map generateGround config.type_constructors)); 
     47    "(*<Generative>*)", (String.concat "\r\n" (List.map generateGenerative (List.filter (fun tcons->tcons.generative) config.type_constructors))); 
     48    "(*<SConstructors>*)", (String.concat "\r\n" (List.map generateSConstructors config.constructors)); 
     49    "(*<SDestructors>*)", (String.concat "\r\n" (List.map generateSDestructors config.destr_types)) 
    5050    ] 

  • src/cg/genkinding.ml

    r14264 r14830  
    3535let gen config str =  
    3636    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    37     "<Kindings>", (String.concat "\r\n" (List.map generateRule config.type_constructors)); 
     37    "(*<Kindings>*)", (String.concat "\r\n" (List.map generateRule config.type_constructors)); 
    3838    ] 

  • src/cg/genlexer.ml

    r14219 r14830  
    2929let gen config str =  
    3030    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    31     "<Types>", (String.concat "\r\n" (List.map (fun x -> generateToken2 x.namet ("T"^x.namet)) config.type_constructors)); 
    32     "<Constructors>", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec)) config.constructors)); 
    33     "<Destructors>", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec)) config.destr_types)); 
    34     "<SDestructors>", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec^"h")) config.destr_types)) 
     31    "(*<Types>*)", (String.concat "\r\n" (List.map (fun x -> generateToken2 x.namet ("T"^x.namet)) config.type_constructors)); 
     32    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec)) config.constructors)); 
     33    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec)) config.destr_types)); 
     34    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun x -> generateToken (x.namec^"h")) config.destr_types)) 
    3535    ] 

  • src/cg/genparser.ml

    r14219 r14830  
    3939let gen config str =  
    4040    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    41     "<Tokens>", generateTokens config; 
    42     "<Types>", (String.concat "\r\n" (List.map (fun x -> generateRule "typedef" ("T"^x.namet) "" "" (List.length x.arguments)) config.type_constructors)); 
    43     "<Constructors>", (String.concat "\r\n" (List.map (fun x -> generateRuleConfArg "term" (x.namec) "C" "" (List.length x.domain)) config.constructors)); 
    44     "<Destructors>", (String.concat "\r\n" (List.map (fun x -> generateRuleConfArg "term" (x.namec) "C" "" (List.length x.domain)) config.destr_types)); 
    45     "<SConstructors>", (String.concat "\r\n" (List.map (fun x -> generateRule "stm" (x.namec) "S" "" (List.length x.domain)) config.constructors)); 
    46     "<SDestructors>", (String.concat "\r\n" (List.map (fun x -> generateRule "stm" (x.namec) "S" "H" (List.length x.domain)) config.destr_types)) 
     41    "(*<Tokens>*)", generateTokens config; 
     42    "(*<Types>*)", (String.concat "\r\n" (List.map (fun x -> generateRule "typedef" ("T"^x.namet) "" "" (List.length x.arguments)) config.type_constructors)); 
     43    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun x -> generateRuleConfArg "term" (x.namec) "C" "" (List.length x.domain)) config.constructors)); 
     44    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun x -> generateRuleConfArg "term" (x.namec) "C" "" (List.length x.domain)) config.destr_types)); 
     45    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun x -> generateRule "stm" (x.namec) "S" "" (List.length x.domain)) config.constructors)); 
     46    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun x -> generateRule "stm" (x.namec) "S" "H" (List.length x.domain)) config.destr_types)) 
    4747    ] 

  • src/cg/genprint.ml

    r14219 r14830  
    3434let gen config str =  
    3535    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    36     "<ConstructorTrans>", (String.concat "\r\n" (List.map generateSTrans config.constructors)); 
    37     "<DestructorTrans>", (String.concat "\r\n" (List.map generateSTrans config.destr_types)); 
    38     "<Types>", (String.concat "\r\n" (List.map (fun tcons -> generatePrint "print_type_b b" tcons.namet (genPatternT "\t| T" tcons)) config.type_constructors)); 
    39     "<Constructors>", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_term_b b" cons.namec (genPatternICA "\t| " cons)) config.constructors)); 
    40     "<Destructors>", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_term_b b" cons.namec (genPatternICA "\t| " cons)) config.destr_types)); 
    41     "<SConstructors>", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_stmt_b b" cons.namec (genPatternS "\t| " cons)) config.constructors)); 
    42     "<SDestructors>", (String.concat "\r\n" (List.map (fun cons -> generatePrintSDes "print_stmt_b b" cons.namec (genPatternS "\t| " cons)) config.destr_types)) 
     36    "(*<ConstructorTrans>*)", (String.concat "\r\n" (List.map generateSTrans config.constructors)); 
     37    "(*<DestructorTrans>*)", (String.concat "\r\n" (List.map generateSTrans config.destr_types)); 
     38    "(*<Types>*)", (String.concat "\r\n" (List.map (fun tcons -> generatePrint "print_type_b b" tcons.namet (genPatternT "\t| T" tcons)) config.type_constructors)); 
     39    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_term_b b" cons.namec (genPatternICA "\t| " cons)) config.constructors)); 
     40    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_term_b b" cons.namec (genPatternICA "\t| " cons)) config.destr_types)); 
     41    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generatePrint "print_stmt_b b" cons.namec (genPatternS "\t| " cons)) config.constructors)); 
     42    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generatePrintSDes "print_stmt_b b" cons.namec (genPatternS "\t| " cons)) config.destr_types)) 
    4343    ] 

  • src/cg/genreplace.ml

    r14597 r14830  
    2828let gen config str =  
    2929    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    30     "<SConstructors>", (String.concat "\r\n" (List.map (fun cons -> generateReplace "replaceab_stmt xs ys" ("S"^cons.namec) (genPatternS "\t| " cons)) config.constructors)); 
    31     "<SDestructors>", (String.concat "\r\n" (List.map (fun cons -> generateReplace "replaceab_stmt xs ys" ("S"^cons.namec) (genPatternS "\t| " cons)) config.destr_types)); 
    32     "<Types>", (String.concat "\r\n" (List.map (fun tcons -> generateReplace "rename_type old fresh" ("T"^tcons.namet) (genPatternT "\t| T" tcons)) config.type_constructors)); 
    33     "<Constructors>", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "rename_term old fresh" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.constructors)); 
    34     "<Destructors>", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "rename_term old fresh" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.destr_types)); 
    35     "<Types2>", (String.concat "\r\n" (List.map (fun tcons -> generateReplace "replace_stmt_in_type' x s free" ("T"^tcons.namet) (genPatternT "\t| T" tcons)) config.type_constructors)); 
    36     "<Constructors2>", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "replace_term x m" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.constructors)); 
     30    "(*<SConstructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateReplace "replaceab_stmt xs ys" ("S"^cons.namec) (genPatternS "\t| " cons)) config.constructors)); 
     31    "(*<SDestructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateReplace "replaceab_stmt xs ys" ("S"^cons.namec) (genPatternS "\t| " cons)) config.destr_types)); 
     32    "(*<Types>*)", (String.concat "\r\n" (List.map (fun tcons -> generateReplace "rename_type old fresh" ("T"^tcons.namet) (genPatternT "\t| T" tcons)) config.type_constructors)); 
     33    "(*<Constructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "rename_term old fresh" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.constructors)); 
     34    "(*<Destructors>*)", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "rename_term old fresh" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.destr_types)); 
     35    "(*<Types2>*)", (String.concat "\r\n" (List.map (fun tcons -> generateReplace "replace_stmt_in_type' x s free" ("T"^tcons.namet) (genPatternT "\t| T" tcons)) config.type_constructors)); 
     36    "(*<Constructors2>*)", (String.concat "\r\n" (List.map (fun cons -> generateReplaceCA "replace_term x m" ("C"^cons.namec) (genPatternCA "\t| " cons)) config.constructors)); 
    3737    ] 

  • src/cg/gensubtype.ml

    r14245 r14830  
    3434let gen config str =  
    3535    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    36     "<Typing>", (String.concat "\r\n" (List.map generateRule (List.filter (fun tcons -> List.length tcons.arguments >=1) config.type_constructors))); 
     36    "(*<Typing>*)", (String.concat "\r\n" (List.map generateRule (List.filter (fun tcons -> List.length tcons.arguments >=1) config.type_constructors))); 
    3737    ] 

  • src/cg/gensyntax.ml

    r14219 r14830  
    3232let gen config str =  
    3333    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    34     "<Types>", (String.concat "\r\n" (List.map generateTCons config.type_constructors)); 
    35     "<Constructors>", (String.concat "\r\n" (List.map generateCons config.constructors)); 
    36     "<Destructors>", (String.concat "\r\n" (List.map generateCons config.destr_types)); 
    37     "<SConstructors>", (String.concat "\r\n" (List.map generateSCons config.constructors)); 
    38     "<SDestructors>", (String.concat "\r\n" (List.map generateSCons config.destr_types)) 
     34    "(*<Types>*)", (String.concat "\r\n" (List.map generateTCons config.type_constructors)); 
     35    "(*<Constructors>*)", (String.concat "\r\n" (List.map generateCons config.constructors)); 
     36    "(*<Destructors>*)", (String.concat "\r\n" (List.map generateCons config.destr_types)); 
     37    "(*<SConstructors>*)", (String.concat "\r\n" (List.map generateSCons config.constructors)); 
     38    "(*<SDestructors>*)", (String.concat "\r\n" (List.map generateSCons config.destr_types)) 
    3939    ] 

  • src/cg/gentemplate.ml

    r14219 r14830  
    3434let gen config str =  
    3535    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    36     "<Constructors>", (String.concat ", " (List.map (genCons "") config.constructors)); 
    37     "<Destructors>", (String.concat ", " (List.map (genCons "h") config.destr_types)); 
    38     "<DestRules>", (String.concat "\r\n" (List.map genRule config.destructors)); 
     36    "(*<Constructors>*)", (String.concat ", " (List.map (genCons "") config.constructors)); 
     37    "(*<Destructors>*)", (String.concat ", " (List.map (genCons "h") config.destr_types)); 
     38    "(*<DestRules>*)", (String.concat "\r\n" (List.map genRule config.destructors)); 
    3939    ] 

  • src/cg/gentypeterm.ml

    r14219 r14830  
    4444let gen config str =  
    4545    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    46     "<ConsInput>", (String.concat "\r\n" (List.map generateInput config.constructors)); 
    47     "<ConsResult>", (String.concat "\r\n" (List.map generateResult config.constructors)); 
    48     "<ConsCompute>", (String.concat "\r\n" (List.map generateCompute config.constructors)); 
    49     "<DestInput>", (String.concat "\r\n" (List.map generateInput config.destr_types)); 
    50     "<DestResult>", (String.concat "\r\n" (List.map generateResult config.destr_types)); 
    51     "<DestCompute>", (String.concat "\r\n" (List.map generateCompute config.destr_types)); 
     46    "(*<ConsInput>*)", (String.concat "\r\n" (List.map generateInput config.constructors)); 
     47    "(*<ConsResult>*)", (String.concat "\r\n" (List.map generateResult config.constructors)); 
     48    "(*<ConsCompute>*)", (String.concat "\r\n" (List.map generateCompute config.constructors)); 
     49    "(*<DestInput>*)", (String.concat "\r\n" (List.map generateInput config.destr_types)); 
     50    "(*<DestResult>*)", (String.concat "\r\n" (List.map generateResult config.destr_types)); 
     51    "(*<DestCompute>*)", (String.concat "\r\n" (List.map generateCompute config.destr_types)); 
    5252    ] 

  • src/cg/genunify.ml

    r14219 r14830  
    4848let gen config str =  
    4949    List.fold_left (fun str1 (rep_from, rep_to) -> replace rep_from rep_to str1) str [ 
    50     "<Constraints>", (String.concat "" (List.map generateConstraint config.type_constructors)); 
    51     "<Applys>", (String.concat "\r\n" (List.map generateApply config.type_constructors)); 
     50    "(*<Constraints>*)", (String.concat "" (List.map generateConstraint config.type_constructors)); 
     51    "(*<Applys>*)", (String.concat "\r\n" (List.map generateApply config.type_constructors)); 
    5252    ] 

  • src/cg/main.ml

    r14264 r14830  
    7272let blindSig = ref false 
    7373 
    74 let blindSigStart = ">>blindSig>>" 
    75 let blindSigEnd = "<<blindSig<<" 
     74let blindSigStart = "(*>>blindSig>>*)" 
     75let blindSigEnd = "(*<<blindSig<<*)" 
    7676 
    7777(* read file, call f to replace strings, write string back to same file *) 

  • src/default.config

    r14589 r14830  
    1515*) 
    1616 
    17 type gen PrivKey(x1[0]) :: tnt if x1::pub, :: pub if x1::pub 
    18 type PubKey(x1[-]) :: pub, :: tnt if x1::pub 
    19 type PubEnc(x1[0]) :: pub, :: tnt if x1::tnt 
    20 type gen SigKey(x1[0]) :: tnt if x1::tnt, :: pub if x1::tnt 
    21 type VerKey(x1[+]) :: pub, :: tnt if x1::tnt 
    22 type Signed(x1[0]) :: tnt, :: pub if x1::pub 
    23 type Hash(x1[0]) :: pub, :: tnt if x1::tnt 
    24 type HashPrivate(x1[0]) :: pub if x1::pub and x1::tnt, :: tnt if x1::pub and x1::tnt  
     17type gen PrivKey(t1[0]) :: tnt if t1::pub, :: pub if t1::pub 
     18type PubKey(t1[-]) :: pub, :: tnt if t1::pub 
     19type PubEnc(t1[0]) :: pub, :: tnt if t1::tnt 
     20type gen SigKey(t1[0]) :: tnt if t1::tnt, :: pub if t1::tnt 
     21type VerKey(t1[+]) :: pub, :: tnt if t1::tnt 
     22type Signed(t1[0]) :: tnt, :: pub if t1::pub 
     23type Hash(t1[0]) :: pub, :: tnt if t1::tnt 
     24type HashPrivate(t1[0]) :: pub if t1::pub and t1::tnt, :: tnt if t1::pub and t1::tnt  
    2525 
    2626(* an artificial contravariant type constructor *) 
    27 type gen GMinus(x1[-]) :: pub if x1::tnt, :: tnt if x1::pub  
     27type gen GMinus(t1[-]) :: pub if t1::tnt, :: tnt if t1::pub  
    2828 
    29 fun pk[x] : PrivKey(x) -> PubKey(x) 
    30 fun enc[x] : (x,PubKey(x)) -> PubEnc(x) 
    31 fun vk[x] : SigKey(x) -> VerKey(x) 
    32 fun sign[x] : (x,SigKey(x)) -> Signed(x) 
    33 fun hash[x] : x -> Hash(x) 
    34 fun hashPrivate[x] : x -> HashPrivate(x) 
     29fun pk[t] : PrivKey(t) -> PubKey(t) 
     30fun enc[t] : (t,PubKey(t)) -> PubEnc(t) 
     31fun vk[t] : SigKey(t) -> VerKey(t) 
     32fun sign[t] : (t,SigKey(t)) -> Signed(t) 
     33fun hash[t] : t -> Hash(t) 
     34fun hashPrivate[t] : t -> HashPrivate(t) 
    3535 
    3636reduc [x,m] dec(enc(m,pk(x)),x) = m 
    3737reduc [x,m] check(sign(m,x),vk(x)) = m 
    3838 
    39 fun dec[x] : (PubEnc(x),PrivKey(x)) -> x 
    40 fun check[x] : (Signed(x),VerKey(x)) -> x 
     39fun dec[t] : (PubEnc(t),PrivKey(t)) -> t 
     40fun check[t] : (Signed(t),VerKey(t)) -> t 
    4141 
    4242compile: 

  • src/typechecker/alpha.ml

    r14264 r14830  
    9999        | TStm t1 -> free_type t1 bf 
    100100        | TVar _ -> bf 
    101 >>blindSig>> 
     101(*>>blindSig>>*) 
    102102        | TBlind t1 -> free_type t1 bf 
    103103        | TBlindSigKey t1 -> free_type t1 bf 
    … …  
    105105        | TBlindSigned t1 -> free_type t1 bf 
    106106        | TBlinder t1 -> free_type t1 bf 
    107 <<blindSig<< 
     107(*<<blindSig<<*) 
    108108        | TTop -> bf 
    109 <Types> 
     109(*<Types>*) 
    110110 
    111111and free_destr g bf = match g with 
    … …  
    118118        | Ver (_, _, _, _, m, l) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_m' m bf) l 
    119119        | Exercise  m -> free_m' m bf 
    120 >>blindSig>> 
     120(*>>blindSig>>*) 
    121121        | Unblind(t, m, n, o) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n; o] 
    122122        | Bcheck(t, m, n) -> List.fold_left (fun a b -> tupleat (free_m' b bf) a) (free_type t bf) [m; n] 
    123 <<blindSig<< 
     123(*<<blindSig<<*) 
    124124        | Id m -> free_m' m bf 
    125 <Destructors> 
     125(*<Destructors>*) 
    126126 
    127127and free_constr f ((bound, free) as bf) = match f with 
    … …  
    131131        | Zk (_, _, _, tl) ->  
    132132                List.fold_left (fun a b -> tupleat a (free_m' b bf)) bf tl 
    133 >>blindSig>> 
     133(*>>blindSig>>*) 
    134134        | Blind(m, n) -> tupleat (free_m' m bf) (free_m' n bf) 
    135135        | Bvk(m) -> free_m' m bf 
    136136        | Bsign(t, m, n) -> tupleat (free_type t bf) (tupleat (free_m' m bf) (free_m' n bf)) 
    137 <<blindSig<< 
    138 <Constructors> 
     137(*<<blindSig<<*) 
     138(*<Constructors>*) 
    139139 
    140140and free_m' m (bound, free) = match m with 
    … …  
    153153        | SPublic(_, _, m) -> free_s' m bf 
    154154        | SExercise  m -> free_s' m bf 
    155 >>blindSig>> 
     155(*>>blindSig>>*) 
    156156        | SUnblind(m, n, o) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n; o] 
    157157        | SBcheck(m, n) -> List.fold_left (fun a b -> tupleat (free_s' b bf) a) ([],[]) [m; n] 
    158 <<blindSig<< 
     158(*<<blindSig<<*) 
    159159        | SId m -> free_s' m bf 
    160 <SDestructors> 
     160(*<SDestructors>*) 
    161161 
    162162and free_sconstr sc ((bound, free) as bf) = match sc with 
    … …  
    166166        | SZk (_, _, _, tl) ->  
    167167                List.fold_left (fun a b -> tupleat a (free_s' b bf)) bf tl 
    168 >>blindSig>> 
     168(*>>blindSig>>*) 
    169169        | SBlind(m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    170170        | SBvk(m) -> free_s' m bf 
    171171        | SBsign(m, n) -> tupleat (free_s' m bf) (free_s' n bf) 
    172 <<blindSig<< 
    173 <SConstructors> 
     172(*<<blindSig<<*) 
     173(*<SConstructors>*) 
    174174 
    175175and free_s' s (bound, free) = match s with 

  • src/typechecker/ckind.ml

    r14219 r14830  
    7373                ckind t1 l f @ ckind (rename_type x fresh_name t2) l (EBind(fresh_name, t1) :: f) 
    7474        | TZKProof(_, _, _, t1), _ -> ckind t1 l f 
    75 >>blindSig>> 
     75(*>>blindSig>>*) 
    7676        | TBlind t, _ -> if well_formed f && subset (kft t) (dom f) then 
    7777                        [] 
    … …  
    8989        | TBlindVerKey t, Ktnt -> ckind t Ktnt f 
    9090        | TBlindSigKey t, _ -> ckind t Ktnt f 
    91 <<blindSig<< 
    92 <Types> 
     91(*<<blindSig<<*) 
     92(*<Types>*) 
    9393        | _ -> (Printf.printf "cannot ckind: "; print_type t; Printf.printf "\n";  
    9494                raise (Invalid_argument "ckind: got something it cannot kind")) 

  • src/typechecker/compile.ml

    r14589 r14830  
    150150                        EFormula(S_Symbol_Term(S_Or, [and_forms (forms gamma1); and_forms (forms gamma2)])) :: (join_gamma (binds gamma1) (binds gamma2))  
    151151                 
    152 <Compile> 
     152(*<Compile>*) 
    153153 
    154154                (* vm = fst(vn) *) 
    … …  
    176176                        | _ -> raise (DefaultCaseException (Printf.sprintf "The \"vm = exercise(vn)\" case does not apply because %s doesn't have an OK type\n" vn))) 
    177177 
    178 >>blindSig>> 
     178(*>>blindSig>>*) 
    179179                (* bcheck(vm,vk) = vn *) 
    180180                | SDestr(SEq(SDestr(SBcheck(SIdent vm, SIdent vk)), SIdent(vn))) 
    … …  
    196196                        | _ ->  
    197197                                raise (DefaultCaseException (Printf.sprintf "The \"bcheck(vm,vk) = vn\" case does not apply because %s doesn't have a Hash type\n" vk))) 
    198 <<blindSig<< 
     198(*<<blindSig<<*) 
    199199                (* default case *) 
    200200                | _ -> EFormula(create_form_from_stmt s) :: gamma' 

  • src/typechecker/functions.ml

    r14616 r14830  
    5454        | TStm t -> is_ground t 
    5555        | TVar _ -> false 
    56 >>blindSig>> 
     56(*>>blindSig>>*) 
    5757        | TBlind t -> is_ground t 
    5858        | TBlindSigKey t -> is_ground t 
    … …  
    6060        | TBlindSigned t -> is_ground t 
    6161        | TBlinder t -> is_ground t 
    62 <<blindSig<< 
     62(*<<blindSig<<*) 
    6363        | TTop -> true 
    64 <Ground> 
     64(*<Ground>*) 
    6565 
    6666let is_generative t = match t with 
    … …  
    6969        | TPrivate -> true 
    7070        | TUntainted -> true 
    71 >>blindSig>> 
     71(*>>blindSig>>*) 
    7272        | TBlinder _ -> true 
    7373        | TBlindSigKey _ -> true 
    74 <<blindSig<< 
    75 <Generative> 
     74(*<<blindSig<<*) 
     75(*<Generative>*) 
    7676        | _ -> (Printf.printf "t is not generative: "; print_type t; false) 
    7777 
    … …  
    109109                | STrue -> S_Symbol(S_Sym_Ident("true")) 
    110110                | SZk(n,m,_,stmlist) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "zk_%d_%d" n m), List.map create_form_from_stmt stmlist)  
    111         >>blindSig>> 
     111        (*>>blindSig>>*) 
    112112                | SBlind (s1, s2) -> S_Symbol_Term(S_Sym_Ident("blind"), [create_form_from_stmt s1; create_form_from_stmt s2]) 
    113113                | SBvk s1 -> S_Symbol_Term(S_Sym_Ident("bvk"), [create_form_from_stmt s1]) 
    114114                | SBsign (s1, s2) -> S_Symbol_Term(S_Sym_Ident("bsign"), [create_form_from_stmt s1; create_form_from_stmt s2]) 
    115         <<blindSig<< 
    116 <SConstructors> 
     115        (*<<blindSig<<*) 
     116(*<SConstructors>*) 
    117117 
    118118(* Taking modif as an argument is quite useless here (not passed recursively) *) 
    … …  
    125125                | SPublic (_,_,s1) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "public%s" modif), [create_form_from_stmt s1]) 
    126126                | SExercise s1 -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "exercise%s" modif), [create_form_from_stmt s1]) 
    127         >>blindSig>> 
     127        (*>>blindSig>>*) 
    128128                | SUnblind (s1,s2,s3) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "unblind%s" modif), 
    129129                        [create_form_from_stmt s1; create_form_from_stmt s2; create_form_from_stmt s3]) 
    130130                | SBcheck (s1,s2) -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "bcheck%s" modif), 
    131131                        [create_form_from_stmt s1; create_form_from_stmt s2]) 
    132         <<blindSig<< 
     132        (*<<blindSig<<*) 
    133133                | SId s1 -> S_Symbol_Term(S_Sym_Ident(Printf.sprintf "id%s" modif), [create_form_from_stmt s1]) 
    134 <SDestructors> 
     134(*<SDestructors>*) 
    135135 
    136136and create_form_from_sdestr d = create_form_from_sdestr' "h" d 

  • src/typechecker/kinding.ml

    r14268 r14830  
    3838                kind' t1 l f foo && kind' (rename_type x fresh_name t2) l (EBind(fresh_name,t1) :: f) foo 
    3939        | TZKProof(_, _, _, t), _ -> kind' t l f foo 
    40 >>blindSig>> 
     40(*>>blindSig>>*) 
    4141        | TBlind t, _ -> well_formed f && subset (kft t) (dom f) 
    4242        | TBlinder t, _ -> kind' t Kpub f foo && kind' t Ktnt f foo 
    … …  
    4545        | TBlindVerKey t, Ktnt -> kind' t Ktnt f foo 
    4646        | TBlindSigKey t, _ -> kind' t Ktnt f foo 
    47 <<blindSig<< 
    48 <Kindings> 
     47(*<<blindSig<<*) 
     48(*<Kindings>*) 
    4949        | _ -> false 
    5050 

  • src/typechecker/lexer.mll

    r14264 r14830  
    4747                "alpha", ALPHA; 
    4848                "beta", BETA; 
    49 >>blindSig>> 
     49(*>>blindSig>>*) 
    5050                "blind", BLIND; 
    5151                "bvk", BVK; 
    5252                "bsign", BSIGN; 
    53 <<blindSig<< 
     53(*<<blindSig<<*) 
    5454                "hashprivate", HASHPRIVATE; 
    55 <Constructors> 
     55(*<Constructors>*) 
    5656                 
    5757                "fst", FST; 
    … …  
    6363                "ver", VER; 
    6464                "exercise", EXERCISE; 
    65 >>blindSig>> 
     65(*>>blindSig>>*) 
    6666                "unblind", UNBLIND; 
    6767                "bcheck", BCHECK; 
    68 <<blindSig<< 
     68(*<<blindSig<<*) 
    6969                "id", ID; 
    70 <Destructors> 
     70(*<Destructors>*) 
    7171 
    7272                "fsth", FSTH; 
    … …  
    7777                "publich", PUBLICH; 
    7878                "exerciseh", EXERCISEH; 
    79 >>blindSig>> 
     79(*>>blindSig>>*) 
    8080                "unblindh", UNBLINDH; 
    8181                "bcheckh", BCHECKH; 
    82 <<blindSig<< 
     82(*<<blindSig<<*) 
    8383                "idh", IDH; 
    84 <SDestructors> 
     84(*<SDestructors>*) 
    8585 
    8686                "Un", TUN; 
    … …  
    9494                "Stm", TSTM; 
    9595                "Private", TPRIVATE; 
    96 >>blindSig>> 
     96(*>>blindSig>>*) 
    9797                "Blind", TBLIND; 
    9898                "BlindSigKey", TBLINDSIGKEY; 
    … …  
    100100                "BlindSigned", TBLINDSIGNED; 
    101101                "Blinder", TBLINDER; 
    102 <<blindSig<< 
    103 <Types> 
     102(*<<blindSig<<*) 
     103(*<Types>*) 
    104104 
    105105                "predicate", PREDICATE; 

  • src/typechecker/parser.mly

    r14817 r14830  
    6969%token TUN TBOOL TCH TOK TPAIR  THASHPRIVATE 
    7070%token TZKPROOF TSTM TPRIVATE TSECRET TUNTAINTED 
    71 >>blindSig>> 
     71(*>>blindSig>>*) 
    7272%token BLIND BVK BSIGN 
    7373%token UNBLIND BCHECK UNBLINDH BCHECKH 
    7474%token TBLIND TBLINDSIGKEY TBLINDVERKEY TBLINDSIGNED TBLINDER 
    75 <<blindSig<< 
    76 <Tokens> 
     75(*<<blindSig<<*) 
     76(*<Tokens>*) 
    7777 
    7878%start main 
    … …  
    125125        | OK                                                                                                                                                            { SOk } 
    126126        | TRUE          { STrue } 
    127 >>blindSig>>                                                                                                                                     
     127(*>>blindSig>>*)                                                                                                                                         
    128128        | BLIND LPAREN stm COMMA stm RPAREN                                     { SBlind($3, $5) } 
    129129        | BVK LPAREN stm RPAREN                                                                                 { SBvk($3) } 
    130130        | BSIGN LPAREN stm COMMA stm RPAREN                                     { SBsign($3, $5) } 
    131 <<blindSig<< 
    132 <SConstructors> 
     131(*<<blindSig<<*) 
     132(*<SConstructors>*) 
    133133; 
    134134 
    … …  
    155155                                                                                                                                                                                { SPublic($4, $6, $10) } 
    156156        | EXERCISEH LPAREN stm RPAREN                                                   { SExercise($3) } 
    157 >>blindSig>> 
     157(*>>blindSig>>*) 
    158158        | UNBLINDH LPAREN stm COMMA stm COMMA stm RPAREN         
    159159                                                                                                                                                                                { SUnblind($3, $5, $7) } 
    160160        | BCHECKH LPAREN stm COMMA stm RPAREN                   { SBcheck($3, $5) } 
    161 <<blindSig<< 
     161(*<<blindSig<<*) 
    162162        | IDH LPAREN stm RPAREN                                                                         { SId($3) } 
    163 <SDestructors> 
     163(*<SDestructors>*) 
    164164; 
    165165 
    … …  
    254254                { TZKProof($4, $6, $8, $12) } 
    255255        | TSTM LPAREN typedef RPAREN                                    { TStm($3) } 
    256 >>blindSig>> 
     256(*>>blindSig>>*) 
    257257        | TBLIND LPAREN typedef RPAREN                                  { TBlind($3) } 
    258258        | TBLINDSIGKEY LPAREN typedef RPAREN                    { TBlindSigKey($3) } 
    … …  
    260260        | TBLINDSIGNED LPAREN typedef RPAREN                    { TBlindSigned($3) } 
    261261        | TBLINDER LPAREN typedef RPAREN                                { TBlinder($3) } 
    262 <<blindSig<< 
     262(*<<blindSig<<*) 
    263263        | LANGLE RANGLE LBRACKET STAR c STAR RBRACKET                                           { TOk($5) } 
    264264        | LANGLE RANGLE                                                                                                                                                                 { TOk(parse_spass "true") } /* SPASS specific */ 
    265265        | LANGLE tytyty RANGLE LBRACKET STAR c STAR RBRACKET            { fun654 $2 (TOk($6))} 
    266266        | LANGLE tytyty RANGLE                                                                                                                                  { fun654 $2 (TOk(parse_spass "true"))} /* SPASS specific */ 
    267 <Types> 
     267(*<Types>*) 
    268268        | TYPE_NAME                                                                             { if Hashtbl.mem Preparser.named_types $1 then Hashtbl.find Preparser.named_types $1 else 
    269269                raise (Invalid_argument ("Parse Error: type name " ^ $1 ^ " used without declaration at " ^ pos_of_position (symbol_start_pos ()))) } 
    … …  
    285285                { Ver($4, $6, $8, $10, $14, $16) } 
    286286        | EXERCISE LPAREN term RPAREN                                   { Exercise($3) } 
    287 >>blindSig>> 
     287(*>>blindSig>>*) 
    288288        | UNBLIND LPAREN STAR COLON typedef STAR RPAREN LPAREN term COMMA term COMMA term RPAREN        { Unblind($5, $9, $11, $13) } 
    289289        | BCHECK LPAREN STAR COLON typedef STAR RPAREN LPAREN term COMMA term RPAREN                    {Bcheck($5, $9, $11) } 
    290 <<blindSig<< 
     290(*<<blindSig<<*) 
    291291        | ID LPAREN term RPAREN                                                 { Id($3) } 
    292 <Destructors> 
     292(*<Destructors>*) 
    293293        | error 
    294294        { raise (Invalid_argument ("parse error: cannot read destructor at " ^  
    … …  
    302302        | OK LPAREN STAR COLON typedef STAR RPAREN      { Ok($5) } 
    303303        | TRUE                                                                                                                                                  { True } 
    304 >>blindSig>> 
     304(*>>blindSig>>*) 
    305305        | BLIND LPAREN term COMMA term RPAREN                   { Blind($3, $5) } 
    306306        | BVK LPAREN term RPAREN                                                { Bvk($3) } 
    307307        | BSIGN LPAREN STAR COLON typedef STAR RPAREN LPAREN term COMMA term RPAREN                     { Bsign($5, $9, $11) } 
    308 <<blindSig<< 
     308(*<<blindSig<<*) 
    309309        | ZK LPAREN STAR NUMBER COMMA NUMBER COMMA IDENT STAR RPAREN LPAREN ttt RPAREN   
    310310                { Zk($4, $6, $8, $12) } 
    311 <Constructors> 
     311(*<Constructors>*) 
    312312        | error 
    313313        { raise (Invalid_argument ("parse error: cannot read constructor at " ^  

  • src/typechecker/print.ml

    r14559 r14830  
    2828        | True -> STrue 
    2929        | Zk (i1, i2, s, tlist) -> SZk (i1, i2, s, List.map term_to_stmt tlist) 
    30 >>blindSig>> 
     30(*>>blindSig>>*) 
    3131        | Blind (t1, t2) -> SBlind (term_to_stmt t1, term_to_stmt t2) 
    3232        | Bvk t -> SBvk (term_to_stmt t) 
    3333        | Bsign (ty, t1, t2) -> SBsign (term_to_stmt t1, term_to_stmt t2) 
    34 <<blindSig<< 
    35 <ConstructorTrans> 
     34(*<<blindSig<<*) 
     35(*<ConstructorTrans>*) 
    3636 
    3737and dstr_to_sdstr d = match d with 
    … …  
    4444        | Ver _ -> raise (Invalid_argument "dstr_to_sdstr: Ver destructor does not exists in statements") 
    4545        | Exercise t -> SExercise (term_to_stmt t) 
    46 >>blindSig>> 
     46(*>>blindSig>>*) 
    4747        | Unblind (ty, t1, t2, t3) -> SUnblind (term_to_stmt t1, term_to_stmt t2, term_to_stmt t3) 
    4848        | Bcheck (ty, t1, t2) -> SBcheck (term_to_stmt t1, term_to_stmt t2) 
    49 <<blindSig<< 
     49(*<<blindSig<<*) 
    5050        | Id t -> SId (term_to_stmt t) 
    51 <DestructorTrans> 
     51(*<DestructorTrans>*) 
    5252 
    5353let rec print_type_b b t = match t with 
    … …  
    6464        | TStm(t1) -> (Printf.bprintf b "Stm("; print_type_b b t1; Printf.bprintf b ")") 
    6565        | TVar x -> Printf.bprintf b "T%s" x 
    66 >>blindSig>> 
     66(*>>blindSig>>*) 
    6767        | TBlind x -> Printf.bprintf b "Blind("; print_type_b b x; Printf.bprintf b ")" 
    6868        | TBlindSigKey x -> Printf.bprintf b "BlindSigKey("; print_type_b b x; Printf.bprintf b ")" 
    … …  
    7070        | TBlindSigned x -> Printf.bprintf b "BlindSigned("; print_type_b b x; Printf.bprintf b ")" 
    7171        | TBlinder x -> Printf.bprintf b "Blinder("; print_type_b b x; Printf.bprintf b ")" 
    72 <<blindSig<< 
     72(*<<blindSig<<*) 
    7373        | TTop -> Printf.bprintf b "Top" 
    74 <Types> 
     74(*<Types>*) 
    7575 
    7676and print_term_b b t = match t with 
    … …  
    9292                                List.iter (fun x -> Printf.bprintf b ", "; print_term_b b x) ts; 
    9393                Printf.bprintf b ")") 
    94 >>blindSig>> 
     94(*>>blindSig>>*) 
    9595        | Blind(x, y) -> Printf.bprintf b "blind("; print_term_b b x;  
    9696                Printf.bprintf b ","; print_term_b b y;  
    … …  
    104104            Printf.bprintf b ","; print_term_b b y; 
    105105            Printf.bprintf b ")" 
    106 <<blindSig<< 
    107 <Constructors> 
     106(*<<blindSig<<*) 
     107(*<Constructors>*) 
    108108 
    109109(* this function now prints type annotations too *) 
    … …  
    118118                        List.iter (fun t -> print_term_b b t; Printf.bprintf b ", ") tl; Printf.bprintf b ")") 
    119119        | Exercise t -> (Printf.bprintf b "exercise("; print_term_b b t; Printf.bprintf b ")") 
    120 >>blindSig>> 
     120(*>>blindSig>>*) 
    121121        | Unblind(ty, t1, t2, t3) -> (Printf.bprintf b "unblind(*"; 
    122122                print_type_b b ty; 
    … …  
    132132                Printf.bprintf b ","; print_term_b b t2;  
    133133                Printf.bprintf b ")") 
    134 <<blindSig<< 
     134(*<<blindSig<<*) 
    135135        | Id t -> (Printf.bprintf b "id("; print_term_b b t; Printf.bprintf b ")") 
    136 <Destructors> 
     136(*<Destructors>*) 
    137137 
    138138let rec print_stmt_b b s = match s with 
    … …  
    150150                List.iter (fun x -> print_stmt_b b x; Printf.bprintf b ", ") tl; 
    151151                Printf.bprintf b ")") 
    152 >>blindSig>> 
     152(*>>blindSig>>*) 
    153153        | SBlind(x, y) -> Printf.bprintf b "blind("; print_stmt_b b x;  
    154154                Printf.bprintf b ","; print_stmt_b b y;  
    … …  
    161161            Printf.bprintf b ","; print_stmt_b b y; 
    162162            Printf.bprintf b ")" 
    163 <<blindSig<< 
    164 <SConstructors> 
     163(*<<blindSig<<*) 
     164(*<SConstructors>*) 
    165165 
    166166and print_sdestr_b b modif sd = match sd with 
    … …  
    173173        (* TODO Is there a bug here? Why is not exercise followed by an "h"? *) 
    174174        | SExercise t -> (Printf.bprintf b "exercise("; print_stmt_b b t; Printf.bprintf b ")") 
    175 >>blindSig>> 
     175(*>>blindSig>>*) 
    176176        | SUnblind(t1, t2, t3) -> (Printf.bprintf b "unblind%s(" modif;  
    177177                print_stmt_b b t1; 
    … …  
    183183                Printf.bprintf b ","; print_stmt_b b t2;  
    184184                Printf.bprintf b ")") 
    185 <<blindSig<< 
     185(*<<blindSig<<*) 
    186186        | SId t -> (Printf.bprintf b "id%s(" modif; print_stmt_b b t; Printf.bprintf b ")") 
    187 <SDestructors> 
     187(*<SDestructors>*) 
    188188         
    189189let rec print_process_b b p = match p with 

  • src/typechecker/replace.ml

    r14598 r14830  
    3232        | SPublic(a, b, t) -> SPublic(a, b, replaceab_stmt xs ys t) 
    3333        | SExercise t -> SExercise(replaceab_stmt xs ys t) 
    34 >>blindSig>> 
     34(*>>blindSig>>*) 
    3535        | SUnblind(m, n, o) -> SUnblind(replaceab_stmt xs ys m, replaceab_stmt xs ys n, replaceab_stmt xs ys o) 
    3636        | SBcheck(m, n) -> SBcheck(replaceab_stmt xs ys m, replaceab_stmt xs ys n) 
    37 <<blindSig<< 
     37(*<<blindSig<<*) 
    3838        | SId t -> SId(replaceab_stmt xs ys t) 
    39 <SDestructors> 
     39(*<SDestructors>*) 
    4040 
    4141and replaceab_sconstr xs ys f = match f with 
    … …  
    4444        | STrue -> STrue 
    4545        | SZk(a, b, c, tl) -> SZk(a, b, c, List.map (fun z -> replaceab_stmt xs ys z) tl) 
    46 >>blindSig>> 
     46(*>>blindSig>>*) 
    4747        | SBlind(m, n) -> SBlind(replaceab_stmt xs ys m, replaceab_stmt xs ys n) 
    4848        | SBvk(m) -> SBvk(replaceab_stmt xs ys m) 
    4949        | SBsign(m, n) -> SBsign(replaceab_stmt xs ys m, replaceab_stmt xs ys n) 
    50 <<blindSig<< 
    51 <SConstructors> 
     50(*<<blindSig<<*) 
     51(*<SConstructors>*) 
    5252 
    5353and replaceab_stmt xs ys s = match s with 
    … …  
    8080        | TStm t1 -> TStm(rename_type old fresh t1) 
    8181        | TVar _ -> t 
    82 >>blindSig>> 
     82(*>>blindSig>>*) 
    8383        | TBlind t1 -> TBlind(rename_type old fresh t1) 
    8484        | TBlindSigKey t1 -> TBlindSigKey(rename_type old fresh t1) 
    … …  
    8686        | TBlindSigned t1 -> TBlindSigned(rename_type old fresh t1) 
    8787        | TBlinder t1 -> TBlinder(rename_type old fresh t1) 
    88 <<blindSig<< 
    89 <Types> 
     88(*<<blindSig<<*) 
     89(*<Types>*) 
    9090 
    9191and rename_destr old fresh g = match g with 
    … …  
    9898        | Ver(a, b, c, d, m, l) -> Ver(a, b, c, d, rename_term old fresh m, List.map (fun a -> rename_term old fresh a) l) 
    9999        | Exercise m -> Exercise(rename_term old fresh m) 
    100 >>blindSig>> 
     100(*>>blindSig>>*) 
    101101        | Unblind(t, m, n, o) -> Unblind(rename_type old fresh t, rename_term old fresh m, rename_term old fresh n, rename_term old fresh o) 
    102102        | Bcheck(t, m, n) -> Bcheck(rename_type old fresh t, rename_term old fresh m, rename_term old fresh n) 
    103 <<blindSig<< 
     103(*<<blindSig<<*) 
    104104        | Id m -> Id(rename_term old fresh m) 
    105 <Destructors> 
     105(*<Destructors>*) 
    106106 
    107107and rename_constr old fresh f = match f with 
    … …  
    114114        | True -> f 
    115115        | Zk(a, b, c, tl) -> Zk(a, b, c, List.map (fun a -> rename_term old fresh a) tl) 
    116 >>blindSig>> 
     116(*>>blindSig>>*) 
    117117        | Blind(m, n) -> Blind(rename_term old fresh m, rename_term old fresh n) 
    118118        | Bvk(m) -> Bvk(rename_term old fresh m) 
    119119        | Bsign(t, m, n) -> Bsign(rename_type old fresh t, rename_term old fresh m, rename_term old fresh n) 
    120 <<blindSig<< 
    121 <Constructors> 
     120(*<<blindSig<<*) 
     121(*<Constructors>*) 
    122122 
    123123and rename_term old fresh m = match m with 
    … …  
    209209        | TStm t1 -> TStm(replace_stmt_in_type' x s free t1) 
    210210        | TVar _ -> t 
    211 >>blindSig>> 
     211(*>>blindSig>>*) 
    212212        | TBlind t1 -> TBlind(replace_stmt_in_type' x s free t1) 
    213213        | TBlindSigKey t1 -> TBlindSigKey(replace_stmt_in_type' x s free t1) 
    … …  
    215215        | TBlindSigned t1 -> TBlindSigned(replace_stmt_in_type' x s free t1) 
    216216        | TBlinder t1 -> TBlinder(replace_stmt_in_type' x s free t1) 
    217 <<blindSig<< 
    218 <Types2> 
     217(*<<blindSig<<*) 
     218(*<Types2>*) 
    219219        in 
    220220                Logmanager.log "results in $t\n" ~types:[res] ~loglevel:2; res 
    … …  
    229229        | True -> True 
    230230        | Zk(a, b, s, nl) -> Zk(a, b, s, List.map (fun a -> replace_term x m a) nl) 
    231 >>blindSig>> 
     231(*>>blindSig>>*) 
    232232        | Blind(m1, m2) -> Blind(replace_term x m m1, replace_term x m m2) 
    233233        | Bvk(m1) -> Bvk(replace_term x m m1) 
    234234        | Bsign(t, m1, m2) -> Bsign(replace_type x m t, replace_term x m m1, replace_term x m m2) 
    235 <<blindSig<< 
    236 <Constructors2> 
     235(*<<blindSig<<*) 
     236(*<Constructors2>*) 
    237237 
    238238and replace_term x m n = match n with 

  • src/typechecker/subtype.ml

    r14264 r14830  
    4141                        | TCh t, TCh u -> subtype t u f && subtype u t f 
    4242                        | TZKProof(_, _, _, t), TZKProof(_, _, _, u) -> subtype t u f 
    43 >>blindSig>> 
     43(*>>blindSig>>*) 
    4444                        | TBlind t, TBlind u -> subtype t u f && subtype u t f 
    4545                        | TBlinder t, TBlinder u -> subtype t u f && subtype u t f 
    … …  
    4747                        | TBlindSigKey t, TBlindSigKey u -> subtype t u f && subtype u t f 
    4848                        | TBlindVerKey t, TBlindVerKey u -> subtype t u f 
    49 <<blindSig<< 
    50 <Typing> 
     49(*<<blindSig<<*) 
     50(*<Typing>*) 
    5151                        | _ -> kind t1 Kpub f && kind t2 Ktnt f 
    5252in 

  • src/typechecker/syntax.ml

    r14817 r14830  
    3030        | TStm of types 
    3131        | TVar of string 
    32 >>blindSig>> 
     32(*>>blindSig>>*) 
    3333        | TBlind of types 
    3434        | TBlindSigKey of types 
    … …  
    3636        | TBlindSigned of types 
    3737        | TBlinder of types 
    38 <<blindSig<< 
     38(*<<blindSig<<*) 
    3939        | TTop 
    40 <Types> 
     40(*<Types>*) 
    4141 
    4242and destr = Fst of term 
    … …  
    4848        | Ver of int * int * int * string * term * term list 
    4949        | Exercise of term 
    50 >>blindSig>> 
     50(*>>blindSig>>*) 
    5151        | Unblind of types * term * term * term 
    5252        | Bcheck of types * term * term 
    53 <<blindSig<< 
     53(*<<blindSig<<*) 
    5454        | Id of term 
    55 <Destructors> 
     55(*<Destructors>*) 
    5656 
    5757and constr = Pair of term * term * term * types option 
    … …  
    5959        | True 
    6060        | Zk of int * int * string * term list 
    61 >>blindSig>> 
     61(*>>blindSig>>*) 
    6262        | Blind of term * term 
    6363        | Bvk of term 
    6464        | Bsign of types * term * term 
    65 <<blindSig<< 
    66 <Constructors> 
     65(*<<blindSig<<*) 
     66(*<Constructors>*) 
    6767 
    6868and term = Ident of name 
    … …  
    8383        | SPublic of int * int * stmt 
    8484        | SExercise of stmt 
    85 >>blindSig>> 
     85(*>>blindSig>>*) 
    8686        | SUnblind of stmt * stmt * stmt 
    8787        | SBcheck of stmt * stmt 
    88 <<blindSig<< 
     88(*<<blindSig<<*) 
    8989        | SId of stmt 
    90 <SDestructors> 
     90(*<SDestructors>*) 
    9191 
    9292and sconstr = SPair of stmt * stmt 
    … …  
    9494        | STrue 
    9595        | SZk of int * int * string * stmt list 
    96 >>blindSig>> 
     96(*>>blindSig>>*) 
    9797        | SBlind of stmt * stmt 
    9898        | SBvk of stmt 
    9999        | SBsign of stmt * stmt 
    100 <<blindSig<< 
    101 <SConstructors> 
     100(*<<blindSig<<*) 
     101(*<SConstructors>*) 
    102102 
    103103and kinding = Ktnt 

  • src/typechecker/template.spass

    r14264 r14830  
    2828  functions[ 
    2929    % constructors 
    30         (pair,2), (ok,0), <Constructors>,  
    31 >>blindSig>> 
     30        (pair,2), (ok,0), (*<Constructors>*),  
     31(*>>blindSig>>*) 
    3232        (blind,2), (bvk,1), (bsign,2),  
    33 <<blindSig<< 
     33(*<<blindSig<<*) 
    3434        % zk constructor - one for each zk arity 
    3535        $#ZKCONSTS$ 
    3636         
    3737        % destructors inside statements 
    38         (fsth,1), (sndh,1), (publich,1), (exerciseh,1), (idh,1), <Destructors>, 
    39 >>blindSig>> 
     38        (fsth,1), (sndh,1), (publich,1), (exerciseh,1), (idh,1), (*<Destructors>*), 
     39(*>>blindSig>>*) 
    4040        (exerciseh,1), (unblindh,3), (bcheckh,2), (idh,1), 
    41 <<blindSig<<     
     41(*<<blindSig<<*)         
    4242        % variables and names in Gamma (transformed to constants) 
    4343        % for some reason they really need the c in front of their name 
    … …  
    5757formula(forall([x,y], equal(sndh(pair(x,y)),y) )). 
    5858formula(forall([x], equal(exerciseh(x),x) )). 
    59 >>blindSig>> 
     59(*>>blindSig>>*) 
    6060formula(forall([x,y], equal(dech(enc(x,pk(y)),y),x) )). 
    6161formula(forall([x,y], equal(checkh(sign(x,y),vk(y)),x) )). 
    6262formula(forall([x,y,z], equal(unblindh(bsign(pair(blind(x,y), ok), z), y, bvk(z)), sign(pair(x, ok), z)))). 
    6363formula(forall([x,z], equal(bcheckh(sign(x, z), bvk(z)), x))). 
    64 <<blindSig<< 
     64(*<<blindSig<<*) 
    6565formula(forall([x], equal(idh(x), x))). 
    66 <DestRules> 
     66(*<DestRules>*) 
    6767 
    6868% Needed for tuples 

  • src/typechecker/typeterm.ml

    r14616 r14830  
    108108        | Public(n, m, _) -> [build_f_type n m] 
    109109        | Exercise(_) -> [TVar("x")] (* XXX correct? *) 
    110 >>blindSig>> 
     110(*>>blindSig>>*) 
    111111        | Unblind(TPair(Ident x, TBlind(tvar), _) as t, _, _, _) -> [TBlindSigned(t); TBlinder(tvar); TBlindVerKey(t)] 
    112112        | Bcheck(TPair(Ident z, TBlind(tvar), _) as t, _, _) -> [TSigned(tvar); TBlindVerKey(t)] 
    113 <<blindSig<< 
     113(*<<blindSig<<*) 
    114114        | Id(_) -> [TVar("x")] 
    115 <DestInput> 
     115(*<DestInput>*) 
    116116        | _ -> raise (Invalid_argument "get_types: type requested that should not be in this table") 
    117117 
    … …  
    124124        | Public(n, m, _) -> gen_pairs m (Spasssyntax.S_Symbol(Spasssyntax.S_True)) 
    125125        | Exercise(_) -> TVar("x") (* XXX correct? *) 
    126 >>blindSig>> 
     126(*>>blindSig>>*) 
    127127        | Unblind(TPair(_, TBlind(tvar), _), _, _, _) -> TSigned(tvar) 
    128128        | Bcheck(TPair(Ident z, TBlind(tvar), TOk c), _, _) -> let _, free = 
    … …  
    132132                TPair(Ident x, tvar, TOk(Spasssyntax.S_Term(Spasssyntax.S_Exists,  
    133133                        [S_Symbol(Spasssyntax.S_Sym_Ident y)], replace_formula z (F(Blind(Ident x, Ident y))) c))) 
    134 <<blindSig<< 
     134(*<<blindSig<<*) 
    135135        | Id(_) -> TVar("x") 
    136 <DestResult> 
     136(*<DestResult>*) 
    137137        | _ -> raise (Invalid_argument "get_type: type requested that should not be 
    138138         in this table") 
    … …  
    147147        | Ver(_, _, _, _, t1, tl) -> [type_term t1 f] @ (List.map (fun a -> type_term a f) tl) 
    148148        | Exercise(t) -> [type_term t f] 
    149 >>blindSig>> 
     149(*>>blindSig>>*) 
    150150        | Unblind(_, m, n, o) -> [type_term m f; type_term n f; type_term o f] 
    151151        | Bcheck(_, m, n) -> [type_term m f; type_term n f] 
    152 <<blindSig<< 
     152(*<<blindSig<<*) 
    153153        | Id(t) -> [type_term t f] 
    154 <DestCompute> 
     154(*<DestCompute>*) 
    155155 
    156156and get_input_types_f f = match f with 
    157157        True -> [] 
    158 >>blindSig>> 
     158(*>>blindSig>>*) 
    159159        | Blind(_, _) -> [TVar("x"); TBlinder(TVar("x"))] 
    160160        | Bvk _ -> [TBlindSigKey(TVar("x"))] 
    161161        | Bsign(TPair(Ident x, TBlind(tvar), _) as t, _, _) -> [t; TBlindSigKey(t)] 
    162 <<blindSig<< 
    163 <ConsInput> 
     162(*<<blindSig<<*) 
     163(*<ConsInput>*) 
    164164        | _ -> raise (Invalid_argument "get_type: type requested that should not be in this table") 
    165165         
    166166and get_result_type_f f = match f with 
    167167        True -> TBool 
    168 >>blindSig>> 
     168(*>>blindSig>>*) 
    169169        | Blind(m, n) -> TBlind(TVar("x")) 
    170170        | Bvk _ -> TBlindVerKey(TVar("x")) 
    171171        | Bsign(TPair(Ident x, TBlind(tvar), _) as t, _, _) -> TBlindSigned(t) 
    172 <<blindSig<< 
    173 <ConsResult> 
     172(*<<blindSig<<*) 
     173(*<ConsResult>*) 
    174174        | _ -> raise (Invalid_argument "get_type: type requested that should not be in this table") 
    175175 
    … …  
    177177        True -> [] 
    178178        | Zk(_, _, _, t) -> List.map (fun a -> type_term a f) t 
    179 >>blindSig>> 
     179(*>>blindSig>>*) 
    180180        | Blind(m1, m2) -> [type_term m1 f; type_term m2 f] 
    181181        | Bvk(m1) -> [type_term m1 f] 
    182182        | Bsign(t, m1, m2) -> [type_term m1 f; type_term m2 f] 
    183 <<blindSig<< 
    184 <ConsCompute> 
     183(*<<blindSig<<*) 
     184(*<ConsCompute>*) 
    185185 
    186186and alg_env u f = ( 

  • src/typechecker/unify.ml

    r14271 r14830  
    146146        | TZKProof(_, _, _, ts), TZKProof(_, _, _, ts'), _ ->  
    147147                generate_constraint ts ts' f b 
    148 >>blindSig>> 
     148(*>>blindSig>>*) 
    149149        | TBlind t, TBlind u, _-> 
    150150                generate_constraint t u f true @ generate_constraint t u f false 
    … …  
    157157        | TBlindVerKey t, TBlindVerKey u, n -> 
    158158                generate_constraint t u f n 
    159 <<blindSig<< 
    160 <Constraints> 
     159(*<<blindSig<<*) 
     160(*<Constraints>*) 
    161161 
    162162        | _, _, true -> con_gen_pub_tnt_plus t t' f 
    … …  
    191191                (TVar y, tr) -> if String.compare y x = 0 then tr else 
    192192                a) (TVar(x)) sigma 
    193 >>blindSig>> 
     193(*>>blindSig>>*) 
    194194        | TBlind t' -> TBlind(apply sigma t') 
    195195        | TBlindSigKey t' -> TBlindSigKey(apply sigma t') 
    … …  
    197197        | TBlindSigned t' -> TBlindSigned(apply sigma t') 
    198198        | TBlinder t' -> TBlinder(apply sigma t') 
    199 <<blindSig<< 
    200 <Applys> 
     199(*<<blindSig<<*) 
     200(*<Applys>*) 
Note: See TracChangeset for help on using the changeset viewer.