summaryrefslogtreecommitdiff
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml157
1 files changed, 10 insertions, 147 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index bcca937b..4970ca13 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Util
open Pp
@@ -19,19 +17,15 @@ open Ppextend
open Topconstr
open Term
open Pattern
-open Rawterm
+open Glob_term
open Constrextern
open Termops
(*i*)
-let sep_p = fun _ -> str"."
let sep_v = fun _ -> str"," ++ spc()
-let sep_pp = fun _ -> str":"
-let sep_bar = fun _ -> spc() ++ str"| "
let pr_tight_coma () = str "," ++ cut ()
let latom = 0
-let lannot = 100
let lprod = 200
let llambda = 200
let lif = 200
@@ -110,18 +104,14 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
-let pr_optc pr = function
- | None -> mt ()
- | Some x -> pr_sep_com spc pr x
-
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
let pr_universe = Univ.pr_uni
-let pr_rawsort = function
- | RProp Term.Null -> str "Prop"
- | RProp Term.Pos -> str "Set"
- | RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
+let pr_glob_sort = function
+ | GProp Term.Null -> str "Prop"
+ | GProp Term.Pos -> str "Set"
+ | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
let pr_id = pr_id
let pr_name = pr_name
@@ -187,6 +177,8 @@ let rec pr_patt sep inh p =
| CPatCstr (_,c,[]) -> pr_reference c, latom
| CPatCstr (_,c,args) ->
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+ | CPatCstrExpl (_,c,args) ->
+ str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
| CPatAtom (_,None) -> str "_", latom
| CPatAtom (_,Some r) -> pr_reference r, latom
| CPatOr (_,pl) ->
@@ -315,85 +307,6 @@ let split_product na' = function
rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
| _ -> anomaly "ill-formed fixpoint body"
-let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
- let na =
- match snd na1, snd na2 with
- Anonymous, Name id ->
- if occur_var_constr_expr id cofun then
- failwith "avoid capture"
- else na2
- | Name id, Anonymous ->
- if occur_var_constr_expr id codom then
- failwith "avoid capture"
- else na1
- | Anonymous, Anonymous -> na1
- | Name id1, Name id2 ->
- if id1 <> id2 then failwith "not same name" else na1 in
- let ty =
- match ty1, ty2 with
- CHole _, _ -> ty2
- | _, CHole _ -> ty1
- | _ ->
- Constrextern.check_same_type ty1 ty2;
- ty2 in
- (LocalRawAssum ([na],bk1,ty), codom)
-
-let rec strip_domain bvar cofun c =
- match c with
- | CArrow(loc,a,b) ->
- merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b
- | CProdN(loc,[([na],bk,ty)],c') ->
- merge_binders bvar cofun (na,bk,ty) c'
- | CProdN(loc,([na],bk,ty)::bl,c') ->
- merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c'))
- | CProdN(loc,(na::nal,bk,ty)::bl,c') ->
- merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c'))
- | _ -> failwith "not a product"
-
-(* Note: binder sharing is lost *)
-let rec strip_domains (nal,bk,ty) cofun c =
- match nal with
- [] -> assert false
- | [na] ->
- let bnd, c' = strip_domain (na,bk,ty) cofun c in
- ([bnd],None,c')
- | na::nal ->
- let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in
- let bnd, c1 = strip_domain (na,bk,ty) f c in
- (try
- let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in
- (bnd::bl, rest, c2)
- with Failure _ -> ([bnd],Some (nal,bk,ty), c1))
-
-(* Re-share binders *)
-let rec factorize_binders = function
- | ([] | [_] as l) -> l
- | LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') ->
- (try
- let _ = Constrextern.check_same_type ty ty' in
- factorize_binders (LocalRawAssum (nal@nal',k,ty)::l)
- with _ ->
- d :: factorize_binders l')
- | d :: l -> d :: factorize_binders l
-
-(* Extract lambdas when a type constraint occurs *)
-let rec extract_def_binders c ty =
- match c with
- | CLambdaN(loc,bvar::lams,b) ->
- (try
- let f = CLambdaN(loc,lams,b) in
- let bvar', rest, ty' = strip_domains bvar f ty in
- let c' =
- match rest, lams with
- None,[] -> b
- | None, _ -> f
- | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
- let (bl,c2,ty2) = extract_def_binders c' ty' in
- (factorize_binders (bvar'@bl), c2, ty2)
- with Failure _ ->
- ([],c,ty))
- | _ -> ([],c,ty)
-
let rec split_fix n typ def =
if n = 0 then ([],typ,def)
else
@@ -436,21 +349,6 @@ let pr_recursive pr_decl id = function
(pr_decl true) dl ++
fnl() ++ str "for " ++ pr_id id
-let is_var id = function
- | CRef (Ident (_,id')) when id=id' -> true
- | _ -> false
-
-let tm_clash = function
- | (CRef (Ident (_,id)), Some (CApp (_,_,nal)))
- when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
- nal
- -> Some id
- | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal)))
- when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
- nal
- -> Some id
- | _ -> None
-
let pr_asin pr (na,indnalopt) =
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
| Some na -> spc () ++ str "as " ++ pr_lname na
@@ -468,8 +366,6 @@ let pr_case_type pr po =
| Some p ->
spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
-let pr_return_type pr po = pr_case_type pr po
-
let pr_simple_return_type pr na po =
(match na with
| Some (_,Name id) ->
@@ -621,9 +517,9 @@ let pr pr sep inherited a =
| CHole _ -> str "_", latom
| CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
- | CSort (_,s) -> pr_rawsort s, latom
+ | CSort (_,s) -> pr_glob_sort s, latom
| CCast (_,a,CastConv (k,b)) ->
- let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in
+ let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in
hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
lcast
| CCast (_,a,CastCoerce) ->
@@ -636,44 +532,11 @@ let pr pr sep inherited a =
| CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
| CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
| CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
- | CDynamic _ -> str "<dynamic>", latom
in
let loc = constr_loc a in
pr_with_comments loc
(sep() ++ if prec_less prec inherited then strm else surround strm)
-
-let rec strip_context n iscast t =
- if n = 0 then
- [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
- else match t with
- | CLambdaN (loc,(nal,bk,t)::bll,c) ->
- let n' = List.length nal in
- if n' > n then
- let nal1,nal2 = list_chop n nal in
- [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c)
- else
- let bl', c = strip_context (n-n') iscast
- (if bll=[] then c else CLambdaN (loc,bll,c)) in
- LocalRawAssum (nal,bk,t) :: bl', c
- | CProdN (loc,(nal,bk,t)::bll,c) ->
- let n' = List.length nal in
- if n' > n then
- let nal1,nal2 = list_chop n nal in
- [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c)
- else
- let bl', c = strip_context (n-n') iscast
- (if bll=[] then c else CProdN (loc,bll,c)) in
- LocalRawAssum (nal,bk,t) :: bl', c
- | CArrow (loc,t,c) ->
- let bl', c = strip_context (n-1) iscast c in
- LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c
- | CCast (_,c,_) -> strip_context n false c
- | CLetIn (_,na,b,c) ->
- let bl', c = strip_context (n-1) iscast c in
- LocalRawDef (na,b) :: bl', c
- | _ -> anomaly "strip_context"
-
type term_pr = {
pr_constr_expr : constr_expr -> std_ppcmds;
pr_lconstr_expr : constr_expr -> std_ppcmds;