(*
We would like to investigate the idea of directly using OCaml to produce Coq-readable language.
The idea would be to make heavy use of the advanced and higher-level features of OCaml to get around
the conceptual problems one encounters in dealing with complicated mathematical structures directly
in Coq.  
The present file is only the first part of this attempt. In it we set up a type of expressions,
do beta-reduction for these (with a parameter limiting the depth of the recurrence so it doesn't 
loop), construct a type_of function, and a printing function which outputs a string which is supposed
to be readable by Coq (and where the meaning in Coq is supposed to be what it looks like from the 
constructor names in the expression type).  These last may only hold if we apply it to expressions
that are "well-written"; just as in a natural language it is possible to have grammatical phrases
which don't have any meaning, here too it is possible to have expressions which don't have
any real meaning in Coq.  However we claim that one can write all meaningful expressions in
(the small subset of Coq which is implemented) by the printing function. The printing suggestion 
PrintDB yields a de Bruijn-style numbering of variables, whereas PrintAs allows one to specify the
string to be used.

At the end we begin to investigate how to generate expressions in a convivial manner. One remark
here is that it seems important to use the functional type unit -> expression rather than just expression,
in order to easily handle the problem of replacing variables in an expression (construction of lambda-terms).
Carlos Simpson
September 3 2002
*)

type suggestion = PrintDB | PrintAs of string;;

type expression = 
Type 
| New of string * expression 
| App of expression * expression 
| Prod of suggestion * expression * (expression -> expression)
| Lambda of suggestion * expression * (expression -> expression);;


let rec beta_reduce e i =
if i < 0 then e else
match e with
Type -> Type
| New(n,t) -> New(n, beta_reduce t (i-1))
| App(f,z) -> let g = (beta_reduce f (i-1)) in begin match g with 
			  Lambda(h,t,u) ->  beta_reduce (u z) (i-1) 
			| _ -> App(g, beta_reduce z (i-1)) end
| Prod(h,t,u) -> Prod (h,beta_reduce t (i-1), function w -> (beta_reduce (u w) (i-1)))
| Lambda(h,t,u) -> Lambda(h,beta_reduce t (i-1), function w -> (beta_reduce (u w) (i-1)));;

let namex i = "x"^(string_of_int i);;
let varx i t = New (namex i, t);;
let forall a b c = "("^a^": "^b^")"^c;;
let mapsto a b c = "["^a^": "^b^"]"^c;;

let rec ccprint e i = 
match e with 
Type -> "Type"
| New(n,t) -> n 
| App(f,z) -> "("^(ccprint f i) ^" " ^(ccprint z i) ^")"
| Prod(h,t,u) -> begin match h with 
			  PrintDB -> forall (namex i) (ccprint t (i + 1)) (ccprint (u (varx i t)) (i+1))
			| PrintAs n -> forall n (ccprint t i) (ccprint (u (New(n, t))) i) end
| Lambda(h,t,u) -> begin match h with
 			 PrintDB -> mapsto (namex i) (ccprint t (i + 1)) (ccprint (u (varx i t)) (i+1))
			| PrintAs n -> mapsto n (ccprint t i) (ccprint (u (New(n, t))) i) end;;

exception Function_not_in_product_type;;

let rec type_of e =
match e with
Type -> Type
| New(n,t) -> t
| App(f,z) -> begin match (type_of f) with 
			  Prod(h,t,u) ->(u z) 
			| _ ->raise Function_not_in_product_type end 
| Prod(h,t,u) -> Type
| Lambda(h,t,u) -> Prod(h,t, function x -> (type_of (u x)));;

(***** now we start trying to create expressions in a functional way ****)

type readvarflagtype = Read | DontRead | Suggest;;
let readvarflag = ref DontRead;;
let globalexp = ref Type;;
let globalsugg = ref PrintDB;;

class vari vsugg =
object (self)
val mutable currentexp = Type 
method the_var () = match !readvarflag with
Read -> currentexp <- !globalexp; currentexp
| Suggest -> globalsugg := vsugg; currentexp
| DontRead ->  currentexp
end;;

let newvariable nvsugg =
let x = new vari nvsugg in
x#the_var;;

let ttype = function () -> Type;;

let app f x = function () -> App (f(), x());;

let replace x e u =
function () -> 
begin
readvarflag := Read;
globalexp := e;
x();
readvarflag := DontRead;
u()
end;;

let get_sugg x =
begin
readvarflag := Suggest;
x ();
readvarflag := DontRead;
!globalsugg
end;;

let lambda x t u = function () ->
Lambda (get_sugg x, t(), function e -> replace x e u ());;

let prod x t u = function () ->
Prod (get_sugg x, t(), function e -> replace x e u ());;

let fprint a = ccprint (a ()) 0;;

let ftype_of a = function () -> (type_of (a ()));;

(*** note that the following expression is not actually well-typed 
but it looks pretty much like a standard coq expression ***)

let xx = newvariable (PrintAs "X");;
let aa = newvariable PrintDB;;

let test1 = lambda xx (prod aa ttype ttype)  (app xx xx);;
fprint test1;;    (* - : string = "[X: (x0: Type)Type](X X)" *)

let test2 = lambda xx (prod xx ttype ttype)  (app xx xx);;
fprint test2;;    (* - : string = "[X: (X: Type)Type](X X)" *)

let test3 = lambda aa (prod aa ttype ttype)  (app aa aa);;
fprint test3;;    (* - : string = "[x0: (x1: Type)Type](x0 x0)" *)

fprint (ftype_of test1);;    (* - : string = "(X: (x0: Type)Type)Type" *)
(* etc *)