path: root/parsing/termast.ml

(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Univ
open Names
open Term
open Inductive
open Sign
open Environ
open Declare
open Impargs
open Coqast
open Ast
open Rawterm
open Pattern
open Nametab

(* In this file, we translate rawconstr to ast, in order to print constr *)

(**********************************************************************)
(* Parametrization                                                    *)

(* This governs printing of local context of references *)
let print_arguments = ref false

(* If true, prints local context of evars, whatever print_arguments *)
let print_evar_arguments = ref false

(* This forces printing of cast nodes *)
let print_casts = ref true

(* This governs printing of implicit arguments.  When
   [print_implicits] is on then [print_implicits_explicit_args] tells
   how implicit args are printed. If on, implicit args are printed
   prefixed by "!" otherwise the function and not the arguments is
   prefixed by "!" *)
let print_implicits = ref false
let print_implicits_explicit_args = ref false

(* This forces printing of coercions *)
let print_coercions = ref false

(* This forces printing universe names of Type{.} *)
let print_universes = ref false


let with_option o f x =
  let old = !o in o:=true;
  try let r = f x in o := old; r
  with e -> o := old; raise e

let with_arguments f = with_option print_arguments f
let with_casts f = with_option print_casts f
let with_implicits f = with_option print_implicits f
let with_coercions f = with_option print_coercions f
let with_universes f = with_option print_universes f

(**********************************************************************)
(* conversion of references                                           *)

let ids_of_ctxt ctxt =
  Array.to_list
    (Array.map
       (function c -> match kind_of_term c with
	  | IsVar id -> id
	  | _ ->
       error
       "Termast: arbitrary substitution of references not yet implemented")
     ctxt)

let ast_of_ident id = nvar id

let ast_of_name = function 
  | Name id -> nvar id
  | Anonymous -> nvar wildcard

let idopt_of_name = function 
  | Name id -> Some id
  | Anonymous -> None

let ast_of_constant_ref sp =
  ope("CONST", [path_section dummy_loc sp])

let ast_of_existential_ref ev =
  ope("EVAR", [num ev])

let ast_of_constructor_ref ((sp,tyi),n) =
  ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n])

let ast_of_inductive_ref (sp,tyi) =
  ope("MUTIND", [path_section dummy_loc sp; num tyi])

let ast_of_ref = function
  | ConstRef sp -> ast_of_constant_ref sp
  | IndRef sp -> ast_of_inductive_ref sp
  | ConstructRef sp -> ast_of_constructor_ref sp
  | VarRef sp -> ast_of_ident (basename sp)

let ast_of_qualid p =
  let dir, s = repr_qualid p in
  let args = List.map nvar (dir@[s]) in
  ope ("QUALID", args)

(**********************************************************************)
(* conversion of patterns                                             *)

let rec ast_of_cases_pattern = function   (* loc is thrown away for printing *)
  | PatVar (loc,Name id) -> nvar id
  | PatVar (loc,Anonymous) -> nvar wildcard
  | PatCstr(loc,(cstrsp,_),args,Name id) ->
      let args = List.map ast_of_cases_pattern args in
      ope("PATTAS",
	  [nvar id;
	   ope("PATTCONSTRUCT", (ast_of_constructor_ref cstrsp)::args)])
  | PatCstr(loc,(cstrsp,_),args,Anonymous) ->
      ope("PATTCONSTRUCT",
	  (ast_of_constructor_ref cstrsp)
	  :: List.map ast_of_cases_pattern args)
	
let ast_dependent na aty =
  match na with
    | Name id -> occur_var_ast id aty
    | Anonymous -> false

let decompose_binder = function
  | RProd(_,na,ty,c) -> Some (BProd,na,ty,c)
  | RLambda(_,na,ty,c) -> Some (BLambda,na,ty,c)
  | RLetIn(_,na,b,c) -> Some (BLetIn,na,b,c)
  | _ -> None

(* Implicit args indexes are in ascending order *)
let explicitize =
  let rec exprec n lastimplargs impl = function
    | a::args ->
	(match impl with
	   | i::l when i=n ->
	       exprec (n+1) (ope("EXPL", [num i; a])::lastimplargs) l args
	   | _ ->
	       let tail = a::(exprec (n+1) [] impl args) in
	       if (!print_implicits & !print_implicits_explicit_args) then
		 List.rev_append lastimplargs tail
	       else tail)
    (* Tail impl args are always printed even if implicit printing is off *)
    | [] -> List.rev lastimplargs
  in exprec 1 []

let rec skip_coercion dest_ref (f,args as app) =
  if !print_coercions then app
  else
    try
      match dest_ref f with
	| Some r ->
	    (match Classops.hide_coercion r with
	       | Some n ->
		   if n >= List.length args then app
		   else (* We skip a coercion *)
		     let _,fargs = list_chop n args in
	       	     skip_coercion dest_ref (List.hd fargs,List.tl fargs)
	       | None -> app)
	| None -> app
    with Not_found -> app

let ast_of_app impl f args =
  if !print_implicits & not !print_implicits_explicit_args then 
    ope("APPLISTEXPL", f::args)
  else
    let args = explicitize impl args in
    if args = [] then f else ope("APPLIST", f::args)

let rec ast_of_raw = function
  | RRef (_,ref) -> ast_of_ref ref
  | RVar (_,id) -> ast_of_ident id
  | REvar (_,n) -> ast_of_existential_ref n
  | RMeta (_,n) -> ope("META",[num n])
  | RApp (_,f,args) ->
      let (f,args) =
	skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in
      let astf = ast_of_raw f in
      let astargs = List.map ast_of_raw args in
      (match f with 
	 | REvar (_,ev) -> ast_of_existential_ref ev (* we drop args *)
	 | RRef (_,ref) -> ast_of_app (implicits_of_global ref) astf astargs
	 | _       -> ast_of_app [] astf astargs)

  | RProd (_,Anonymous,t,c) ->
      (* Anonymous product are never factorized *)
      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])

  | RLetIn (_,na,t,c) ->
      ope("LETIN",[ast_of_raw t; slam(idopt_of_name na,ast_of_raw c)])

  | RProd (_,na,t,c) ->
      let (n,a) = factorize_binder 1 BProd na (ast_of_raw t) c in
      (* PROD et PRODLIST doivent être distingués à cause du cas *)
      (* non dépendant, pour isoler l'implication; peut-être un *)
      (* constructeur ARROW serait-il plus justifié ? *) 
      let tag = if n=1 then "PROD" else "PRODLIST" in
      ope(tag,[ast_of_raw t;a])

  | RLambda (_,na,t,c) ->
      let (n,a) = factorize_binder 1 BLambda na (ast_of_raw t) c in
      (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
      (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
      ope("LAMBDALIST",[ast_of_raw t;a])

  | RCases (_,printinfo,typopt,tml,eqns) ->
      let pred = ast_of_rawopt typopt in
      let tag = match printinfo with
	| PrintIf -> "FORCEIF"
	| PrintLet -> "FORCELET"
	| PrintCases -> "CASES" 
      in
      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
      let asteqns = List.map ast_of_eqn eqns in 
      ope(tag,pred::asttomatch::asteqns)
	
  | ROldCase (_,isrec,typopt,tm,bv) ->
      (* warning "Old Case syntax"; *)
      ope("CASE",(ast_of_rawopt typopt)
	    ::(ast_of_raw tm)
	    ::(Array.to_list (Array.map ast_of_raw bv)))
  | RRec (_,fk,idv,tyv,bv) ->
      let alfi = Array.map ast_of_ident idv in
      (match fk with
	 | RFix (nv,n) ->
             let rec split_lambda binds = function
	       | (0, t) -> (binds,ast_of_raw t)
	       | (n, RLambda (_,na,t,b)) ->
		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
		   split_lambda (bind::binds) (n-1,b)
	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
	     let rec split_product = function
	       | (0, t) -> ast_of_raw t
	       | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
	     let listdecl = 
	       Array.mapi
		 (fun i fi ->
		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
		    ope("FDECL",
		       	[fi; ope ("BINDERS",List.rev lparams); 
			 asttyp; astdef]))
		 alfi
	     in 
	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
	 | RCoFix n -> 
	     let listdecl =
               Array.mapi 
		 (fun i fi ->
		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
		 alfi
	     in 
	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))

  | RSort (_,s) ->
      (match s with
	 | RProp Null -> ope("PROP",[])
	 | RProp Pos -> ope("SET",[])
	 | RType (Some u) when !print_universes -> ope("TYPE",[ide(Univ.string_of_univ u)])
	 | RType _ -> ope("TYPE",[]))
  | RHole _ -> ope("ISEVAR",[])
  | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
	
and ast_of_eqn (_,ids,pl,c) =
  ope("EQN", (ast_of_raw c)::(List.map ast_of_cases_pattern pl))

and ast_of_rawopt = function
  | None -> (str "SYNTH")
  | Some p -> ast_of_raw p

and factorize_binder n oper na aty c =
  let (p,body) = match decompose_binder c with
    | Some (oper',na',ty',c')
	when (oper = oper') & (aty = ast_of_raw ty')
	  & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
	  & not (na' = Anonymous & oper = BProd)
	  -> factorize_binder (n+1) oper na' aty c'
    | _ -> (n,ast_of_raw c)
  in
  (p,slam(idopt_of_name na, body))

let ast_of_rawconstr = ast_of_raw

(******************************************************************)
(* Main translation function from constr -> ast *)
       
let ast_of_constr at_top env t =
  let t' =
    if !print_casts then t
    else Reduction.local_strong strip_outer_cast t in
  let avoid = if at_top then ids_of_context env else [] in
  ast_of_raw 
    (Detyping.detype avoid (names_of_rel_context env) t')

let ast_of_constant env (sp,ids) =
  let a = ast_of_constant_ref sp in
  if !print_arguments then
    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
  else a

let ast_of_existential env (ev,ids) =
  let a = ast_of_existential_ref ev in
  if !print_arguments or !print_evar_arguments then
    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
  else a

let ast_of_constructor env (cstr_sp,ids) =
  let a = ast_of_constructor_ref cstr_sp in
  if !print_arguments then
    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
  else a

let ast_of_inductive env (ind_sp,ids) =
  let a = ast_of_inductive_ref ind_sp in
  if !print_arguments then
    ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
  else a

let decompose_binder_pattern = function
  | PProd(na,ty,c) -> Some (BProd,na,ty,c)
  | PLambda(na,ty,c) -> Some (BLambda,na,ty,c)
  | PLetIn(na,b,c) -> Some (BLetIn,na,b,c)
  | _ -> None

let rec ast_of_pattern env = function
  | PRef ref -> ast_of_ref ref

  | PVar id -> ast_of_ident id

  | PEvar n -> ast_of_existential_ref n

  | PRel n ->
      (try match lookup_name_of_rel n env with
	 | Name id   -> ast_of_ident id
	 | Anonymous ->
	     anomaly "ast_of_pattern: index to an anonymous variable"
       with Not_found ->
	 nvar (id_of_string ("[REL "^(string_of_int n)^"]")))

  | PApp (f,args) ->
      let (f,args) = 
	skip_coercion (function PRef r -> Some r | _ -> None)
	  (f,Array.to_list args) in
      let astf = ast_of_pattern env f in
      let astargs = List.map (ast_of_pattern env) args in
      (match f with 
	 | PRef ref -> ast_of_app (implicits_of_global ref) astf astargs
	 | _        -> ast_of_app [] astf astargs)

  | PSoApp (n,args) ->
      ope("SOAPP",(ope ("META",[num n])):: 
		  (List.map (ast_of_pattern env) args))

  | PLetIn (na,b,c) ->
      let c' = ast_of_pattern (add_name na env) c in
      ope("LETIN",[ast_of_pattern env b;slam(idopt_of_name na,c')])
		
  | PProd (Anonymous,t,c) ->
      ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
  | PProd (na,t,c) ->
      let env' = add_name na env in
      let (n,a) =
	factorize_binder_pattern env' 1 BProd na (ast_of_pattern env t) c in
      (* PROD et PRODLIST doivent être distingués à cause du cas *)
      (* non dépendant, pour isoler l'implication; peut-être un *)
      (* constructeur ARROW serait-il plus justifié ? *) 
      let tag = if n=1 then "PROD" else "PRODLIST" in
      ope(tag,[ast_of_pattern env t;a])
  | PLambda (na,t,c) ->
      let env' = add_name na env in
      let (n,a) =
	factorize_binder_pattern env' 1 BLambda na (ast_of_pattern env t) c in
      (* LAMBDA et LAMBDALIST se comportent pareil *)
      let tag = if n=1 then "LAMBDA" else "LAMBDALIST" in
      ope(tag,[ast_of_pattern env t;a])

  | PCase (typopt,tm,bv) ->
      warning "Old Case syntax";
      ope("MUTCASE",(ast_of_patopt env typopt)
	    ::(ast_of_pattern env tm)
	    ::(Array.to_list (Array.map (ast_of_pattern env) bv)))

  | PSort s ->
      (match s with
	 | RProp Null -> ope("PROP",[])
	 | RProp Pos -> ope("SET",[])
	 | RType _ -> ope("TYPE",[]))

  | PMeta (Some n) -> ope("META",[num n])
  | PMeta None -> ope("ISEVAR",[])
  | PFix f -> ast_of_raw (Detyping.detype [] env (mkFix f))
  | PCoFix c -> ast_of_raw (Detyping.detype [] env (mkCoFix c))
	
and ast_of_patopt env = function
  | None -> (str "SYNTH")
  | Some p -> ast_of_pattern env p

and factorize_binder_pattern env n oper na aty c =
  let (p,body) = match decompose_binder_pattern c with
    | Some (oper',na',ty',c')
	when (oper = oper') & (aty = ast_of_pattern env ty')
	  & not (na' = Anonymous & oper = BProd)
	  ->
	factorize_binder_pattern (add_name na' env) (n+1) oper na' aty c'
    | _ -> (n,ast_of_pattern env c)
  in
  (p,slam(idopt_of_name na, body))