Changeset 1059 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 6, 2011, 6:09:39 PM (8 years ago)
Author:
mulligan
Message:

work from today, bit of a mess at the moment

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1057 r1059  
    88example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
    99example not_implemented: False. cases daemon qed.
    10  
     10
     11notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     12 with precedence 10
     13for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     14
     15let rec reduce
     16  (A: Type[0]) (left: list A) (right: list A) on left ≝
     17  match left with
     18  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
     19  | cons hd tl ⇒
     20    match right with
     21    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
     22    | cons hd' tl' ⇒
     23      let 〈cleft, cright〉 ≝ reduce A tl tl' in
     24      let 〈commonl, restl〉 ≝ cleft in
     25      let 〈commonr, restr〉 ≝ cright in
     26        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
     27    ]
     28  ].
     29
     30(*
     31let rec reduce_strong
     32  (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝
     33  match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
     34  [ nil ⇒
     35    match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
     36    [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ?
     37    | cons hd tl ⇒ λnil_cons_asrd_prf. ?
     38    ]
     39  | cons hd tl ⇒
     40    match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
     41    [ nil ⇒ λcons_nil_absrd_prf. ?
     42    | cons hd' tl' ⇒ λcons_cons_prf. ?
     43    ]
     44  ] prf.
     45*)
     46
     47axiom reduce_length:
     48  ∀A: Type[0].
     49  ∀left, right: list A.
     50  ∀prf: | left | = | right |.
     51    \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).
     52   
    1153let rec map2_opt
    1254  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     
    255297    | S o ⇒ f (iterate A f a o)
    256298    ].
    257    
    258 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    259  with precedence 10
    260 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    261299
    262300(* Yeah, I probably ought to do something more general... *)
Note: See TracChangeset for help on using the changeset viewer.