(*** first we parse into a sequence of symbols ****)

#load "str.cma";;

let rec channel_to_list c =
try 
let next_char = (input_char c) in
next_char::(channel_to_list c)
with 
_-> [];;

let file_to_list filename =
let look_input_channel = open_in filename in
let answer = channel_to_list look_input_channel in
close_in look_input_channel;
answer;;

let rec split_periods clist =
match clist with 
[] -> []
| head::tail ->
let tail_answer = (split_periods tail) in
if head = '.' then []::tail_answer else
(match tail_answer with 
[] -> [[head]]
| thead::ttail -> (head::thead)::ttail );;


let rec clist_to_string clist =
match clist with
[] -> ""
| head::tail -> (String.make 1 head)^(clist_to_string tail);;

let input_string_list () =
let file_list = (file_to_list "input.v") in
let per_split = (split_periods file_list) in
let answer = (List.map clist_to_string per_split) in
answer;;


(****** note from the above code that the program will read the file "input.v"
in the directory from which it is run *****************************************)

let string_to_token_list s = Str.full_split (Str.regexp "[ \t\n\r()]") s;;

type symbol =
| Openpar
| Closepar
| Word of string
;;

let rec token_list_to_symbol_list tlist = 
match tlist with
| [] -> []
| head::tail -> 
  (match head with 
  | Str.Text w -> (Word w) :: (token_list_to_symbol_list tail) 
  | Str.Delim "(" -> Openpar :: (token_list_to_symbol_list tail) 
  | Str.Delim ")" -> Closepar :: (token_list_to_symbol_list tail) 
  | _ -> (token_list_to_symbol_list tail) 
  )
;;
 
let string_to_backward_symbol_list s = 
let tlist = string_to_token_list s in
(List.rev (token_list_to_symbol_list tlist));;


(*** now we assume that we have cut off a leading Closepar from the bslist,
and we look for the place where the corresponding Openpar is ***)

exception Openpar_Not_Found;;

let rec in_front_of_corresp_openpar i bslist =
match bslist with 
| [] -> raise Openpar_Not_Found
| (Word s)::tail -> (Word s)::(in_front_of_corresp_openpar i tail)
| Openpar::tail -> if i=0 then [] else Openpar::(in_front_of_corresp_openpar (i-1) tail)
| Closepar::tail -> Closepar::(in_front_of_corresp_openpar (i+1) tail)
;;

let rec behind_corresp_openpar i bslist =
match bslist with 
| [] -> raise Openpar_Not_Found
| (Word s)::tail -> (behind_corresp_openpar i tail)
| Openpar::tail -> if i=0 then tail else (behind_corresp_openpar (i-1) tail)
| Closepar::tail -> (behind_corresp_openpar (i+1) tail)
;;





type expr =
| Erreur of string
| Ident of string 
| Apl of expr * expr;;



let rec bslist_to_expr bslist = 
match bslist with 
| [] -> Erreur "empty_expression"
| head::[] -> (match head with | Word s -> Ident s |_ -> Erreur "wrong_expression_as_singleton")
| head::tail -> 
   (match head with 
   | Word s -> Apl (bslist_to_expr tail, Ident s) 
   | Closepar -> (try 
                 let y = (behind_corresp_openpar 0 tail) in
                 let z = (in_front_of_corresp_openpar 0 tail) in 
      (match y with | [] -> bslist_to_expr z | head::tail -> Apl (bslist_to_expr y,bslist_to_expr z))
                 with Openpar_Not_Found -> Erreur "openpar_not_found")
   | Openpar -> Erreur "misplaced_openpar"
   )
;;

let string_to_expr s = try bslist_to_expr (string_to_backward_symbol_list s)
with _ -> Erreur "exception in string_to_expr";;

let input_bslist () = 
(List.map string_to_backward_symbol_list (input_string_list ()));;

let input_expr_list () =
(List.map string_to_expr (input_string_list ()));;



(**********************************************************)




type kind = 
Ens |
Prop |
Arr of kind * kind;;


type obj =
Prim of kind * string |
Var of int |
App of obj * obj |
Imp of obj * obj |
Lambda of kind * obj |
Prod of kind * obj 
;;

let rec lift j x =
match x with
| Prim (k,s) -> Prim (k,s)
| Var i -> if i < j then (Var i) else (Var (i+1))
| App (a,b) -> App (lift j a, lift j b)
| Imp (a,b) -> Imp (lift j a, lift j b)
| Lambda (k,a) -> Lambda (k,lift (j+1) a)
| Prod (k,a) -> Prod (k, lift (j+1) a)
;;

exception Ill_Typed;;

(*** this is also supposed to type_check by raising Ill_Typed whenever the term doesn't check ***)
let rec kind_of_obj cxt x =
match x with
| Prim (k,s) -> k 
| Var i  -> 
  (match cxt with [] -> (raise Ill_Typed) | head::tail -> (if i = 0 then head else (kind_of_obj tail (Var (i-1)))))
| App (a,b) -> 
  (match (kind_of_obj cxt a) with  
  | Arr (u,v) -> if (kind_of_obj cxt b) = u then v else (raise Ill_Typed)  
  | _ -> (raise Ill_Typed)
  )
| Imp (a,b) -> 
  (match (kind_of_obj cxt a,kind_of_obj cxt b) with 
  | (Prop,Prop) -> Prop 
  | _ -> raise Ill_Typed
  )
| Lambda (k,a) -> 
  Arr (k,(kind_of_obj (k::cxt) a))
| Prod (k,a) -> 
  (match (kind_of_obj (k::cxt) a) with  
  | Prop -> Prop 
  | _ -> raise Ill_Typed
  )
;;
    

let rec substitute u j x = 
match x with 
| Prim (k,s) -> Prim (k,s)
| Var i -> (if i = j then u else if i < j then Var i else Var (i-1))
| App (a,b) -> App (substitute u j a,substitute u j b)
| Imp (a,b) -> Imp (substitute u j a, substitute u j b)
| Lambda (k,a) -> Lambda (k, substitute u (j+1) a)
| Prod (k,a) -> Prod (k,substitute u (j+1) a)
;;

let rec beta_reduce cxt x = 
kind_of_obj cxt x; (*** to raise an exception if ill-typed ***)
match x with 
| Prim (k,s) -> Prim (k,s)
| Var i -> Var i
| App (a,b) -> 
   (match (beta_reduce cxt a) with
   | Lambda (m,t) -> (substitute (beta_reduce cxt b) 0 t)
   | y -> App (y,(beta_reduce cxt b)))
| Imp (a,b) -> Imp (beta_reduce cxt a, beta_reduce cxt b)
| Lambda (k,a) -> Lambda (k,beta_reduce (k::cxt) a)
| Prod (k,a) -> Prod (k,beta_reduce (k::cxt) a)
;;

(*** next we define a module for sets of objects; we call it LemSet because it is destined for
sets of lemmas ************)

module OrderedObj =
struct
type t = obj
let compare = Pervasives.compare
end;;

module LemSet  =  Set.Make(OrderedObj);;
(******************************************* this defines, among other things:
LemSet.t = the type of sets of hypotheses
LemSet.elt = obj is the type of elements
LemSet.empty = the empty hypset
LemSet.mem x s : bool tests whether x:obj is a member of s:HypSet.t
LemSet.add x s : HypSet.t is the set obtained by adding x:obj to s
***********************************************************************) 

type proof =
Axiom of obj |
Prove of obj * proof |
Recall of obj |
Cut of proof * proof |
Suppose of obj * proof |
Generalize of obj * proof |
Introduce of kind * proof
;;

exception Invalid_Proof;;

(** in the following, cxt is a list of kinds (the variable context); hyps is a list of objects
(the local hypotheses depending on the context); and lems is in LemSet.t, it is the set of known 
lemmas up to there ***************************************************************************)


let rec proved_by cxt hyps lems p =
match p with
| Axiom a -> 
  (if (kind_of_obj cxt a) = Prop then a else raise Invalid_Proof)
| Prove (a,q) -> 
  (if (beta_reduce cxt a) = (beta_reduce cxt (proved_by cxt hyps lems q)) then a else raise Invalid_Proof)
| Recall a ->
  (if (kind_of_obj cxt a) = Prop then 
  (if (LemSet.mem a lems) || (List.mem a hyps) then a else raise Invalid_Proof)
   else raise Invalid_Proof)
| Cut (q,r) ->
  (match (proved_by cxt hyps lems q) with 
  | Imp (a,b) -> (if (proved_by cxt hyps lems r) = a then b else raise Invalid_Proof)
  | _ -> raise Invalid_Proof
  )
| Suppose (a,q) -> 
  (if (kind_of_obj cxt a) = Prop then Imp (a,proved_by cxt (a::hyps) lems q) else raise Invalid_Proof)
| Generalize (a,q) -> 
  (match (proved_by cxt hyps lems q) with 
  | Prod (m,b) -> (if m = (kind_of_obj cxt a) then (substitute a 0 b) else raise Invalid_Proof)
  | _ -> raise Invalid_Proof
  )
| Introduce (k,q) -> 
  Prod (k, proved_by (k::cxt) (List.map (lift 0) hyps) lems q)
;;
  


(***** now we use the expr type of peProc to process expressions into proofs ***)

exception Invalid_Expression;;

let rec expr_to_kind x = 
match x with 
| Ident "E" -> Ens 
| Ident "P" -> Prop
| Apl (a,b) -> Arr (expr_to_kind b,expr_to_kind a)
| _ -> raise Invalid_Expression
;;

(*** bindings is a list of strings saying what the variables are called; k is the
kind of the resulting object; this allows us to infer the kinds of the terms without
having to specify them except in prod and app; for app the default is Ens,
other argument types need to be specified   ********************************************************)

exception Unbound_Variable;;

let rec bound_variable bindings v =
match bindings with 
| [] -> raise Unbound_Variable 
| head :: tail -> if head = v then 0 else ((bound_variable tail v) + 1)
;;


let rec expr_to_obj bindings k x = 
match x with 
| Apl (Apl (Apl (Ident "forall", m), Ident v), p) -> 
  Prod (expr_to_kind m, expr_to_obj (v::bindings) Prop p)
| Apl (Apl (Ident "function", Ident v), p) -> 
  (match k with 
  | Arr (m,n) -> Lambda (m, expr_to_obj (v::bindings) n p)
  | _ -> raise Invalid_Expression
  )
| Apl (Apl (Ident "if", a),b) ->
  if k = Prop then 
  Imp (expr_to_obj bindings Prop a, expr_to_obj bindings Prop b)
  else raise Invalid_Expression
| Apl (Apl (Apl (a,Ident "of"), m),b) ->
  let n = expr_to_kind m in 
  App (expr_to_obj bindings (Arr (n,k)) a, expr_to_obj bindings n b)
| Apl (a,b) ->   (* assume if not specified as in the previous line that b is of type Ens *)
  App (expr_to_obj bindings (Arr (Ens,k)) a, expr_to_obj bindings Ens b)
| Ident s -> 
  (try (Var (bound_variable bindings s)) with Unbound_Variable -> Prim (k,s))
| Erreur e -> Prim (Ens, "erroneous_expression: "^e)
;;

exception Invalid_Proof;;

let rec expr_to_proof bindings x =
match x with 
| Apl (Ident "axiom", a) -> 
  Axiom (expr_to_obj bindings Prop a)
| Apl (Apl (Ident "prove", a),p) ->
  Prove (expr_to_obj bindings Prop a, expr_to_proof bindings p)
| Apl (Ident "recall", a) -> 
  Recall (expr_to_obj bindings Prop a)
| Apl (Apl (Ident "cut", p),q) ->
  Cut (expr_to_proof bindings p, expr_to_proof bindings q)
| Apl (Apl (Ident "suppose", a),p) ->
  Suppose (expr_to_obj bindings Prop a, expr_to_proof bindings p)
| Apl (Apl (Apl (Ident "generalize", k),a),p)  ->
  Generalize (expr_to_obj bindings (expr_to_kind k) a, expr_to_proof bindings p)
| Apl (Apl (Apl (Ident "introduce", k),Ident v),p)  ->
  Introduce (expr_to_kind k, expr_to_proof (v::bindings) p)
| Erreur e -> raise Invalid_Proof
| _ -> raise Invalid_Proof
;;

type proof_attempt =
Success of proof * obj |
ReadFailure of expr  |
ProofFailure of proof |
DocumentOK ;;

let expr_to_proof_attempt bindings lems x = 
try let p = (expr_to_proof bindings x) in
(
try let a = (proved_by [] [] lems p) in 
Success (p,a) 
with Invalid_Proof -> (ProofFailure p)
)
with 
Invalid_Proof -> ReadFailure x;;


type status = 
Current of (proof_attempt list) * LemSet.t;;

let initialstatus = Current ([],LemSet.empty);;

(** a document is a list of expressions ***)

let rec document_to_status stat doc =
match stat with
Current (palist, lems) -> 
(match doc with
| [] -> stat
| head::tail -> let pa = (expr_to_proof_attempt [] lems head) in 
  (match pa with | Success (p,a) -> Current (pa::palist, LemSet.add a lems)
  | _ -> Current (pa::palist, lems))
);;

let rec first_failure rev_palist =
match rev_palist with 
| [] -> DocumentOK 
| head::tail -> 
(match head with 
| ReadFailure x -> ReadFailure x
| ProofFailure p -> ProofFailure p
| _ -> (first_failure tail)
);;

let check_document doc =
let stat = (document_to_status initialstatus doc) in 
match stat with Current (palist,lems) ->
first_failure (List.rev palist);;





let check_input_document () = 
check_document (input_expr_list());;

let status_of_input_document () = document_to_status initialstatus (input_expr_list ());;


(********** to use the program, launch the ocaml shell with the command "ocaml"
and then type #use "emotor.ml";; 
then type check_input_document();;
it should read the file input.v (from the directory in which you started the ocaml)
and report on what happened....??????????
this very preliminary version of May 16th, 2003 has not yet been debugged...
CS
********************************************************************************)