Permalink
Browse files

Definitions

  • Loading branch information...
andrejbauer committed Nov 5, 2012
1 parent 4eb5bb5 commit 0c0b6af9b6f55233a8042b07b362bd0c82421f29
Showing with 36 additions and 18 deletions.
  1. +1 −0 concrete.ml
  2. +2 −1 infer.ml
  3. +2 −0 lexer.mll
  4. +4 −2 parser.mly
  5. +1 −1 print.ml
  6. +9 −9 syntax.ml
  7. +17 −5 tt.ml
View
@@ -19,6 +19,7 @@ type directive =
| Help
| Context
| Parameter of variable * expr
+ | Definition of variable * expr
| Check of expr
| Eval of expr
View
@@ -7,7 +7,7 @@ let lookup_ty x ctx = fst (lookup x ctx)
let lookup_value x ctx = snd (lookup x ctx)
-let extend x t ?value lst = (x, (t, value)) :: lst
+let extend x t ?value ctx = (x, (t, value)) :: ctx
(* Normalization. *)
let rec normalize ctx = function
@@ -63,6 +63,7 @@ let rec infer_type ctx = function
| Lambda (x, t, e) ->
let _ = infer_universe ctx t in
let x = Concrete.fresh_var x in
+ (* XXX: bug, infer_type does not get called immediately. *)
let f v = infer_type (extend x t ~value:v ctx) (e (Var x)) in
Pi (x, t, f)
| App (e1, e2) ->
View
@@ -9,6 +9,7 @@
let directives = [
("Check", CHECK) ;
+ ("Definition", DEFINITION) ;
("Eval", EVAL) ;
("Help", HELP) ;
("Quit", QUIT) ;
@@ -41,6 +42,7 @@ rule token = parse
| ',' { COMMA }
| "->" { ARROW }
| "=>" { DARROW }
+ | ":=" { COLONEQUAL }
| eof { EOF }
View
@@ -6,9 +6,9 @@
%token <int> NUMERAL
%token <string> NAME
%token LPAREN RPAREN
-%token COLON COMMA PERIOD
+%token COLON COMMA PERIOD COLONEQUAL
%token ARROW DARROW
-%token QUIT HELP PARAMETER CHECK EVAL CONTEXT
+%token QUIT HELP PARAMETER CHECK EVAL CONTEXT DEFINITION
%token EOF
%start <Concrete.directive list> directives
@@ -34,6 +34,8 @@ directive:
{ Check e }
| EVAL e = expr
{ Eval e}
+ | DEFINITION x = NAME COLONEQUAL e = expr
+ { Definition (String x, e) }
| CONTEXT
{ Context }
View
@@ -19,7 +19,7 @@ let variable x ppf =
| Concrete.Gensym (x, k) -> print ppf "%s_%d" x k
let expr e ppf =
- let e = Syntax.uneval e in
+ let e = Syntax.uncompile e in
let rec expr ?max_level e ppf =
let print ?at_level = print ?max_level ?at_level ppf in
match e with
View
@@ -2,14 +2,14 @@ type variable = Concrete.variable
type universe = Concrete.universe
-type value =
+type expr =
| Var of variable
- | App of value * value
+ | App of expr * expr
| Universe of universe
| Pi of abstraction
| Lambda of abstraction
-and abstraction = variable * value * (value -> value)
+and abstraction = variable * expr * (expr -> expr)
(* Compilation from concrete. *)
let compile e =
@@ -25,13 +25,13 @@ let compile e =
compile [] e
(* Conversion back to concrete syntax, for pretty-printing. *)
-let rec uneval = function
+let rec uncompile = function
| Var x -> Concrete.Var x
- | App (e1, e2) -> Concrete.App (uneval e1, uneval e2)
+ | App (e1, e2) -> Concrete.App (uncompile e1, uncompile e2)
| Universe u -> Concrete.Universe u
- | Pi a -> Concrete.Pi (uneval_vabstraction a)
- | Lambda a -> Concrete.Lambda (uneval_vabstraction a)
+ | Pi a -> Concrete.Pi (uncompile_vabstraction a)
+ | Lambda a -> Concrete.Lambda (uncompile_vabstraction a)
-and uneval_vabstraction (x, t, f) =
+and uncompile_vabstraction (x, t, f) =
let x = Concrete.fresh_var x in
- (x, uneval t, uneval (f (Var x)))
+ (x, uncompile t, uncompile (f (Var x)))
View
22 tt.ml
@@ -5,10 +5,12 @@ let interactive_shell = ref true
let wrapper = ref (Some ["rlwrap"; "ledit"])
let help_text = "Toplevel commands:
-Parameter <ident> : <expr>. assume variable <ident> has type <expr>
-Context. print current contex
-Help. print this help
-Quit. exit" ;;
+Parameter <ident> : <expr>. assume variable <ident> has type <expr>
+Definition <indent> := <expr>. define <ident> to be <expr>
+Eval <expr>. normalize an expression
+Context. print current contex
+Help. print this help
+Quit. exit" ;;
(* A list of files to be loaded and run. *)
let files = ref []
@@ -68,7 +70,10 @@ let rec exec_cmd interactive ctx e =
ctx
| Concrete.Context ->
List.iter
- (fun (x, (t, _)) -> Format.printf "@[%t : @[%t@]@]@." (Print.variable x) (Print.expr t))
+ (function
+ | (x, (t, None)) -> Format.printf "@[%t : @[%t@]@]@." (Print.variable x) (Print.expr t)
+ | (x, (t, Some e)) -> Format.printf "@[%t = %t@]@\n : @[%t@]@."
+ (Print.variable x) (Print.expr e) (Print.expr t))
ctx ;
ctx
| Concrete.Parameter (x, t) ->
@@ -77,6 +82,13 @@ let rec exec_cmd interactive ctx e =
if interactive then
Format.printf "@[%t is assumed@]@." (Print.variable x) ;
Infer.extend x t ctx
+ | Concrete.Definition (x, e) ->
+ if List.mem_assoc x ctx then Error.typing "%t already exists" (Print.variable x) ;
+ let e = Syntax.compile e in
+ let t = Infer.infer_type ctx e in
+ if interactive then
+ Format.printf "@[%t is defined@]@." (Print.variable x) ;
+ Infer.extend x t ~value:e ctx
| Concrete.Check e ->
let e = Syntax.compile e in
let t = Infer.infer_type ctx e in

0 comments on commit 0c0b6af

Please sign in to comment.