aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml76
1 files changed, 38 insertions, 38 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 74a4d5e5d..80e1eb144 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id$ *)
(*i*)
open Util
@@ -94,14 +94,14 @@ let pr_delimiters key strm =
let pr_generalization bk ak c =
let hd, tl =
- match bk with
+ match bk with
| Implicit -> "{", "}"
| Explicit -> "(", ")"
- in (* TODO: syntax Abstraction Kind *)
+ in (* TODO: syntax Abstraction Kind *)
str "`" ++ str hd ++ c ++ str tl
let pr_com_at n =
- if Flags.do_beautify() && n <> 0 then comment n
+ if Flags.do_beautify() && n <> 0 then comment n
else mt()
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
@@ -114,7 +114,7 @@ let pr_optc pr = function
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-let pr_universe = Univ.pr_uni
+let pr_universe = Univ.pr_uni
let pr_rawsort = function
| RProp Term.Null -> str "Prop"
@@ -130,7 +130,7 @@ let pr_expl_args pr (a,expl) =
| None -> pr (lapp,L) a
| Some (_,ExplByPos (n,_id)) ->
anomaly("Explicitation by position not implemented")
- | Some (_,ExplByName id) ->
+ | Some (_,ExplByName id) ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
let pr_opt_type pr = function
@@ -164,7 +164,7 @@ let pr_evar pr n l =
(match l with
| Some l ->
spc () ++ pr_in_comment
- (fun l ->
+ (fun l ->
str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]")
(List.rev l)
| None -> mt()))
@@ -200,7 +200,7 @@ let pr_eqn pr (loc,pl,rhs) =
spc() ++ hov 4
(pr_with_comments loc
(str "| " ++
- hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
+ hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
@@ -213,22 +213,22 @@ let begin_of_binders = function
| b::_ -> begin_of_binder b
| _ -> 0
-let surround_impl k p =
+let surround_impl k p =
match k with
| Explicit -> str"(" ++ p ++ str")"
| Implicit -> str"{" ++ p ++ str"}"
-let surround_binder k p =
+let surround_binder k p =
match k with
| Default b -> hov 1 (surround_impl b p)
- | Generalized (b, b', t) ->
+ | Generalized (b, b', t) ->
hov 1 (surround_impl b' (surround_impl b p))
-
+
let surround_implicit k p =
match k with
| Default Explicit -> p
| Default Implicit -> (str"{" ++ p ++ str"}")
- | Generalized (b, b', t) ->
+ | Generalized (b, b', t) ->
surround_impl b' (surround_impl b p)
let pr_binder many pr (nal,k,t) =
@@ -281,7 +281,7 @@ let rec extract_lam_binders = function
let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
LocalRawAssum (nal,bk,t) :: bl, c
| c -> [], c
-
+
let split_lambda = function
| CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
| CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
@@ -293,7 +293,7 @@ let rename na na' t c =
| (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
| (_,Name id), (_,Anonymous) -> (na,t,c)
| _ -> (na',t,c)
-
+
let split_product na' = function
| CArrow (loc,t,c) -> (na',t,c)
| CProdN (loc,[[na],bk,t],c) -> rename na na' t c
@@ -324,7 +324,7 @@ let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
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) ->
@@ -401,13 +401,13 @@ let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
let annot =
match ro with
CStructRec ->
- if List.length bl > 1 && n <> None then
+ if List.length bl > 1 && n <> None then
spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
- else mt()
+ else mt()
| CWfRec c ->
spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
| CMeasureRec (m,r) ->
- spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++
+ spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++
(match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}"
in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
@@ -428,11 +428,11 @@ let is_var id = function
| _ -> false
let tm_clash = function
- | (CRef (Ident (_,id)), Some (CApp (_,_,nal)))
+ | (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)))
+ | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal)))
when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
nal
-> Some id
@@ -445,7 +445,7 @@ let pr_asin pr (na,indnalopt) =
(match indnalopt with
| None -> mt ()
| Some t -> spc () ++ str "in " ++ pr lsimple t)
-
+
let pr_case_item pr (tm,asin) =
hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
@@ -474,7 +474,7 @@ let pr_appexpl pr f l =
let pr_app pr a l =
hov 2 (
- pr (lapp,L) a ++
+ pr (lapp,L) a ++
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
let pr_forall () =
@@ -554,28 +554,28 @@ let pr pr sep inherited a =
let c,l1 = list_sep_last l1 in
assert (snd c = None);
let p = pr_proj (pr mt) pr_app (fst c) f l1 in
- if l2<>[] then
+ if l2<>[] then
p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
else
p, lproj
| CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
| CRecord (_,w,l) ->
- let beg =
+ let beg =
match w with
- | None -> spc ()
+ | None -> spc ()
| Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
in
- hv 0 (str"{" ++ beg ++
+ hv 0 (str"{" ++ beg ++
prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
(fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
l), latom
| CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
hv 0 (
- str "let '" ++
- hov 0 (pr_patt ltop p ++
+ str "let '" ++
+ hov 0 (pr_patt ltop p ++
pr_asin (pr_dangling_with_for mt pr) asin ++
- str " :=" ++ pr spc ltop c ++
+ str " :=" ++ pr spc ltop c ++
pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
str " in" ++ pr spc ltop b)),
lletpattern
@@ -608,7 +608,7 @@ let pr pr sep inherited a =
hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
lif
-
+
| CHole _ -> str "_", latom
| CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
@@ -645,7 +645,7 @@ let rec strip_context n iscast t =
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
+ LocalRawAssum (nal,bk,t) :: bl', c
| CProdN (loc,(nal,bk,t)::bll,c) ->
let n' = List.length nal in
if n' > n then
@@ -654,12 +654,12 @@ let rec strip_context n iscast t =
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
+ 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) ->
+ | CLetIn (_,na,b,c) ->
let bl', c = strip_context (n-1) iscast c in
LocalRawDef (na,b) :: bl', c
| _ -> anomaly "strip_context"
@@ -704,7 +704,7 @@ let pr_with_occurrences_with_trailer pr occs trailer =
(if nowhere_except_in then mt() else str "- ") ++
hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer)
-let pr_with_occurrences pr occs =
+let pr_with_occurrences pr occs =
pr_with_occurrences_with_trailer pr occs (mt())
let pr_red_flag pr r =
@@ -725,13 +725,13 @@ let pr_metaid id = str"?" ++ pr_id id
let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
| Red false -> str "red"
| Hnf -> str "hnf"
- | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o
+ | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o
| Cbv f ->
if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
str "compute"
else
hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
- | Lazy f ->
+ | Lazy f ->
hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
| Unfold l ->
hov 1 (str "unfold" ++ spc() ++
@@ -740,7 +740,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
| Pattern l ->
hov 1 (str "pattern" ++
pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
-
+
| Red true -> error "Shouldn't be accessible from user."
| ExtraRedExpr s -> str s
| CbvVm -> str "vm_compute"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 18:13:21 +0000