Skip to content

C
cpdt
Commit bdc1ccb6 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Port Interps

parent 355b7174
Hide whitespace changes
Inline Side-by-side
Showing with 13 additions and 12 deletions
src/Impure.v
View file @ bdc1ccb6
(* Copyright (c) 2008, Adam Chlipala (* Copyright (c) 2008-2009, Adam Chlipala
* *
* This work is licensed under a * This work is licensed under a
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
......
src/Intensional.v
View file @ bdc1ccb6
(* Copyright (c) 2008, Adam Chlipala (* Copyright (c) 2008-2009, Adam Chlipala
* *
* This work is licensed under a * This work is licensed under a
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
......
src/Interps.v
View file @ bdc1ccb6
(* Copyright (c) 2008, Adam Chlipala (* Copyright (c) 2008-2009, Adam Chlipala
* *
* This work is licensed under a * This work is licensed under a
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
...@@ -85,8 +85,8 @@ Module STLC. ...@@ -85,8 +85,8 @@ Module STLC.
| t1 --> t2 => typeDenote t1 -> typeDenote t2 | t1 --> t2 => typeDenote t1 -> typeDenote t2
end. end.
Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
match e in (exp _ t) return (typeDenote t) with match e with
| Var _ v => v | Var _ v => v
| Const n => n | Const n => n
...@@ -113,8 +113,8 @@ Module STLC. ...@@ -113,8 +113,8 @@ Module STLC.
Section cfold. Section cfold.
Variable var : type -> Type. Variable var : type -> Type.
Fixpoint cfold t (e : exp var t) {struct e} : exp var t := Fixpoint cfold t (e : exp var t) : exp var t :=
match e in exp _ t return exp _ t with match e with
| Var _ v => #v | Var _ v => #v
| Const n => ^n | Const n => ^n
...@@ -260,8 +260,8 @@ Module PSLC. ...@@ -260,8 +260,8 @@ Module PSLC.
| t1 ++ t2 => typeDenote t1 + typeDenote t2 | t1 ++ t2 => typeDenote t1 + typeDenote t2
end%type. end%type.
Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
match e in (exp _ t) return (typeDenote t) with match e with
| Var _ v => v | Var _ v => v
| Const n => n | Const n => n
...@@ -312,14 +312,15 @@ Module PSLC. ...@@ -312,14 +312,15 @@ Module PSLC.
| _ => tt | _ => tt
end. end.
Definition pairOut t1 t2 (e : exp var (t1 ** t2)) : option (exp var t1 * exp var t2) := Definition pairOut t1 t2 (e : exp var (t1 ** t2))
: option (exp var t1 * exp var t2) :=
match e in exp _ t return pairOutType t with match e in exp _ t return pairOutType t with
| Pair _ _ e1 e2 => Some (e1, e2) | Pair _ _ e1 e2 => Some (e1, e2)
| _ => pairOutDefault _ | _ => pairOutDefault _
end. end.
Fixpoint cfold t (e : exp var t) {struct e} : exp var t := Fixpoint cfold t (e : exp var t) : exp var t :=
match e in exp _ t return exp _ t with match e with
| Var _ v => #v | Var _ v => #v
| Const n => ^n | Const n => ^n
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment