lambda.ml

   1: (******************************************************************************
   2:  * Définitions du type lambda_term et utilitaires de bases
   3:  *****************************************************************************)
   4: 
   5: open List;;
   6: open Term_lexer;;
   7: 
   8: (*****************************************************************************
   9:  * Type des lambda-termes
  10:  *****************************************************************************)
  11: 
  12: type lambda_term = Var of int * string
  13:                  | App of lambda_term * lambda_term
  14:                  | Abs of string * lambda_term
  15:                  | Star
  16: ;;
  17: 
  18: 
  19: (*****************************************************************************
  20:  * Un normalisateur de lambda-termes basé sur la KAM
  21:  *****************************************************************************)
  22: 
  23: (* types utilisées par la KAM *)
  24: type closure    = Clos of lambda_term * closure list
  25:                 | Free of int
  26: and environment = closure list
  27: and       stack = closure list
  28: and       state = (lambda_term * environment * stack)
  29: ;;
  30: 
  31: type lambdas_list = (string * string) list 
  32: ;;
  33: 
  34: (* Affichage *)
  35: let rec string_of_lambda : lambda_term -> string =
  36:   function
  37:       Abs(x, t) -> "[" ^ x ^ "]" ^ (string_of_lambda t)
  38:     | App(f, a) -> "(" ^ (string_of_lambda f) ^")" ^ (string_of_lambda a)
  39:     | Var(_, x) -> x
  40:     | Star      -> "*"
  41: ;;
  42: 
  43: let max_depth_limit = 100000;;
  44: 
  45: (* Rend la forme normale du terme passé en argument *)
  46: let normalize : lambda_term -> lambda_term =
  47:   fun t ->
  48:     let rec kam : int -> lambdas_list -> state -> lambda_term =
  49:       fun depth lambdas ->
  50:         if depth > max_depth_limit then failwith "Max recursion depth exceeded"
  51:         else function
  52:             (App(u, v), e, s) ->
  53:               kam (depth + 1) lambdas (u, e, (Clos(v, e))::s)
  54:           | (Abs(_, u), e, c::s) -> kam (depth + 1) lambdas (u, c::e, s)
  55:           | (Abs(x, u), e, []) ->
  56:               let var_name = alpha lambdas x
  57:               and lambdas_count = length lambdas
  58:               in Abs(var_name,
  59:                      kam (depth + 1) ((x, var_name)::lambdas)
  60:                        (u, Free(lambdas_count + 1)::e, []))
  61:           | (Var(i, _), e, s) -> (
  62:               try
  63:                 match nth e i with
  64:                     Clos(vi, ei) -> kam (depth + 1) lambdas (vi, ei, s)
  65:                   | Free(lambda_index) ->
  66:                       let var_index = (length lambdas) - lambda_index
  67:                       in let (_, var_name) = nth lambdas var_index
  68:                       in fold_left
  69:                            (kam_arg depth lambdas)
  70:                            (Var(var_index, var_name)) s
  71:               with
  72:                   Failure("nth") -> failwith "Free variable"
  73:             )
  74:           | (Star, _, []) -> Star
  75:           | (Star, _, _) -> failwith "Arguments to constant *"
  76: 
  77:     and kam_arg: int -> lambdas_list -> lambda_term -> closure -> lambda_term =
  78:       fun depth lambdas f ->
  79:         function
  80:             (Clos(a, m)) -> App(f, kam (depth + 1) lambdas (a, m, []))
  81:           | _ -> failwith "Kam failure : invalid closure in stack"
  82: 
  83:     and alpha : lambdas_list -> string -> string =
  84:       fun lambdas var_name ->
  85:         let var_count = length (find_all (fun (x, _) -> x = var_name) lambdas)
  86:         in if var_count = 0
  87:           then var_name
  88:           else var_name ^ (string_of_int var_count)
  89: 
  90:     in kam 0 [] (t, [], [])
  91: ;;
  92: 
  93: 
  94: (*****************************************************************************
  95:  * Parser : lambda-termes
  96:  *****************************************************************************
  97:  *
  98:  * terme  = '$' ident | '#' ident
  99:  *        | var |'[' var ']' terme | '(' terme ')' terme
 100:  *
 101:  * define_lambda "delta" "[x](x)x";;
 102:  * define_lambda "deltadelta" "($delta)$delta"
 103:  * define_macro  "xx" "(x)x";;
 104:  * define_lambda "deltadelta" "([x]#xx)[x]#xx";;
 105:  *
 106:  *****************************************************************************)
 107: 
 108: (* Tables des termes et terme-macros prédéfinis *)
 109: let lambda_table : (string, lambda_term) Hashtbl.t = Hashtbl.create(17);;
 110: let lambda_macros_table : (string, string) Hashtbl.t = Hashtbl.create(17);;
 111: 
 112: let rec lambda_of_stream : token_stream -> lambda_term =
 113:   let rec parse_term (binders : string list) : token_stream -> lambda_term =
 114:     parser
 115:         [< 'Kwd '$'; 'Ident name >]       -> Hashtbl.find lambda_table name
 116:       | [< 'Kwd '#'; 'Ident name >]       ->
 117:           parse_term binders (term_lexer
 118:                                 (Hashtbl.find lambda_macros_table name))
 119:       | [< 'Kwd '[';
 120:            'Ident x ?? "no variable name in lambda";
 121:            'Kwd ']' ?? "lambda not terminated";
 122:            t = parse_term (x::binders) >] -> Abs(x, t)
 123:       | [< 'Kwd '(';
 124:            f = parse_term binders;
 125:            'Kwd ')' ?? "missing closing paren in application";
 126:            a = parse_term binders >]      -> App(f, a)
 127:       | [< 'Ident x >]                    -> Var(index_of x binders, x)
 128:       | [< 'Kwd '*' >]                    -> Star
 129:       | [< 'Kwd _ >]                      -> raise (Stream.Error
 130:                                                       "invalid char")
 131:       | [< 'Int _ >]                      -> raise (Stream.Error
 132:                                                       "invalid char")
 133:   in parse_term []
 134: 
 135: and lambda_of_string s = lambda_of_stream (term_lexer s)
 136: ;;
 137: 
 138: let define_lambda : ?dont_normalize : bool -> string -> string -> unit =
 139:   fun ?(dont_normalize = false) name term ->
 140:     Hashtbl.replace lambda_table name (
 141:       if dont_normalize
 142:       then lambda_of_string term
 143:       else normalize (lambda_of_string term)
 144:     )
 145: and define_macro : string -> string -> unit = fun name term ->
 146:   Hashtbl.replace lambda_macros_table name term
 147: ;;
 148: 
 149: (* Normalisation avec conversion de et vers les strings *)
 150: let exec : string -> string =
 151:   fun s -> string_of_lambda(normalize (lambda_of_string s))
 152: ;;
 153: 

This document was generated using caml2html