pretty-printers

parent 6d95d628
......@@ -48,7 +48,7 @@ OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
CAMLP4 = @CAMLP4O@
INCLUDES = -I src
INCLUDES = -I lib -I src
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
......@@ -88,7 +88,9 @@ check: $(BINARY) $(PRELUDE)
# why
#####
CMO = src/name.cmo src/hashcons.cmo src/term.cmo
LIBCMO = lib/pp.cmo
CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo
CMX = $(CMO:.cmo=.cmx)
bin/why.opt: $(CMX)
......@@ -372,7 +374,7 @@ otags:
otags src/*.mli src/*.ml c/*.mli c/*.ml intf/*.mli intf/*.ml
wc:
ocamlwc -p src/*.ml* jc/*.ml* c/*.ml* intf/*.ml* tools/*.ml* java/*.ml*
ocamlwc -p src/*.ml*
# distrib
#########
......@@ -548,7 +550,7 @@ coq-clean::
.PHONY: depend
.depend depend: $(GENERATED)
rm -f .depend
$(OCAMLDEP) -slash $(INCLUDES) src/*.ml src/*.mli jc/*.mli jc/*.ml c/*.mli c/*.ml java/*.mli java/*.ml intf/*.ml intf/*.mli tools/*.mli tools/*.ml mix/*.mli mix/*.ml ml/*.ml ml/*.mli > .depend
$(OCAMLDEP) -slash $(INCLUDES) lib/*.ml lib/*.mli src/*.ml src/*.mli > .depend
$(OCAMLDEP) -slash $(MLINCLUDES) ml/parsing/*.ml ml/parsing/*.mli ml/typing/*.ml ml/typing/*.mli ml/utils/*.ml ml/utils/*.mli >> .depend
ifeq ($(FRAMAC),yes)
# $(MAKE) -C $(JESSIE_PLUGIN_PATH) depend
......
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(*i $Id: pp.ml,v 1.22 2009-10-19 11:55:33 bobot Exp $ i*)
(*s Pretty-print library *)
open Format
let print_option f fmt = function
| None -> ()
| Some x -> f fmt x
let print_option_or_default default f fmt = function
| None -> fprintf fmt "%s" default
| Some x -> f fmt x
let rec print_list sep print fmt = function
| [] -> ()
| [x] -> print fmt x
| x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
let print_list_or_default default sep print fmt = function
| [] -> fprintf fmt "%s" default
| l -> print_list sep print fmt l
let print_list_par sep pr fmt l =
print_list sep (fun fmt x -> fprintf fmt "(%a)" pr x) fmt l
let print_list_delim start stop sep pr fmt = function
| [] -> ()
| l -> fprintf fmt "%a%a%a" start () (print_list sep pr) l stop ()
let print_pair_delim start sep stop pr1 pr2 fmt (a,b) =
fprintf fmt "%a%a%a%a%a" start () pr1 a sep () pr2 b stop ()
let comma fmt () = fprintf fmt ",@ "
let simple_comma fmt () = fprintf fmt ", "
let underscore fmt () = fprintf fmt "_"
let semi fmt () = fprintf fmt ";@ "
let space fmt () = fprintf fmt " "
let alt fmt () = fprintf fmt "|@ "
let newline fmt () = fprintf fmt "@\n"
let arrow fmt () = fprintf fmt "@ -> "
let lbrace fmt () = fprintf fmt "{"
let rbrace fmt () = fprintf fmt "}"
let lsquare fmt () = fprintf fmt "["
let rsquare fmt () = fprintf fmt "]"
let lparen fmt () = fprintf fmt "("
let rparen fmt () = fprintf fmt ")"
let lchevron fmt () = fprintf fmt "<"
let rchevron fmt () = fprintf fmt ">"
let nothing fmt _ = ()
let string fmt s = fprintf fmt "%s" s
let constant_string s fmt () = string fmt s
let print_pair pr1 = print_pair_delim lparen comma rparen pr1
let hov n fmt f x = pp_open_hovbox fmt n; f x; pp_close_box fmt ()
let open_formatter ?(margin=78) cout =
let fmt = formatter_of_out_channel cout in
pp_set_margin fmt margin;
pp_open_box fmt 0;
fmt
let close_formatter fmt =
pp_close_box fmt ();
pp_print_flush fmt ()
let open_file_and_formatter ?(margin=78) f =
let cout = open_out f in
let fmt = open_formatter ~margin cout in
cout,fmt
let close_file_and_formatter (cout,fmt) =
close_formatter fmt;
close_out cout
let print_in_file_no_close ?(margin=78) p f =
let cout,fmt = open_file_and_formatter ~margin f in
p fmt;
close_formatter fmt;
cout
let print_in_file ?(margin=78) p f =
let cout = print_in_file_no_close ~margin p f in
close_out cout
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(*i $Id: pp.mli,v 1.22 2009-10-19 11:55:33 bobot Exp $ i*)
open Format
val print_option : (formatter -> 'a -> unit) -> formatter -> 'a option -> unit
val print_option_or_default :
string -> (formatter -> 'a -> unit) -> formatter -> 'a option -> unit
val print_list :
(formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list_or_default :
string -> (formatter -> unit -> unit) ->
(formatter -> 'a -> unit) -> formatter -> 'a list -> unit
val print_list_par :
(Format.formatter -> unit -> 'a) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
val print_list_delim :
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
val print_pair_delim :
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> unit -> unit) ->
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
val print_pair :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) -> Format.formatter -> 'a * 'b -> unit
val space : formatter -> unit -> unit
val alt : formatter -> unit -> unit
val newline : formatter -> unit -> unit
val comma : formatter -> unit -> unit
val simple_comma : formatter -> unit -> unit
val semi : formatter -> unit -> unit
val underscore : formatter -> unit -> unit
val arrow : formatter -> unit -> unit
val lbrace : formatter -> unit -> unit
val rbrace : formatter -> unit -> unit
val lsquare : formatter -> unit -> unit
val rsquare : formatter -> unit -> unit
val lparen : formatter -> unit -> unit
val rparen : formatter -> unit -> unit
val lchevron : formatter -> unit -> unit
val rchevron : formatter -> unit -> unit
val nothing : formatter -> 'a -> unit
val string : formatter -> string -> unit
val constant_string : string -> formatter -> unit -> unit
val hov : int -> formatter -> ('a -> unit) -> 'a -> unit
val open_formatter : ?margin:int -> out_channel -> formatter
val close_formatter : formatter -> unit
val open_file_and_formatter : ?margin:int -> string -> out_channel * formatter
val close_file_and_formatter : out_channel * formatter -> unit
val print_in_file_no_close : ?margin:int -> (Format.formatter -> unit) -> string -> out_channel
val print_in_file : ?margin:int -> (Format.formatter -> unit) -> string -> unit
......@@ -14,47 +14,33 @@
(* *)
(**************************************************************************)
#load "hashcons.cmo";;
#load "name.cmo";;
#load "term.cmo";;
#load "pp.cmo";;
#load "pretty.cmo";;
#install_printer Name.print;;
#install_printer Pretty.print_ty;;
#install_printer Pretty.print_term;;
open Term
open Typing
let alpha = Name.from_string "alpha"
let talpha = Ty.var alpha
let aa = Ty.arrow talpha talpha
let a = Name.from_string "a"
let b = Name.from_string "b"
let t1 = lam a talpha (app (var a) (var b))
let t2 = lam a talpha (app (var a) (var b))
let ta = app (var a) (var b)
let tb = app (var a) (var b)
let g = Name.from_string "g"
let f = Name.from_string "f"
let h = Name.from_string "h"
let tk = lam g aa (lam f aa (app (var g) (var f)))
let var_alpha = Ty.ty_var alpha
let termfun t =
match t.node with
| App ({ node = Var v}, t2) when Name.equal v g -> app (var h) t2
| _ -> t
let list = Ty.create_tysymbol (Name.from_string "list") [alpha] None
let tl = map termfun tk
let list_alpha = Ty.ty_app list [var_alpha]
let list_list_alpha = Ty.ty_app list [list_alpha]
let _ =
Format.printf "%a = %a = %b@." print t1 print t2 (equal t1 t2);
Format.printf "%a = %a = %b@." print ta print tb (equal ta tb);
Format.printf "%a -> %a : %b@." print tk print tl (alpha_equal tk tl)
let nil = create_fsymbol (Name.from_string "nil") ([], list_alpha)
let t_nil = t_app nil [] list_alpha
let tt_nil = t_app nil [] list_list_alpha
let x = Name.from_string "x"
let y = Name.from_string "y"
let cons = create_fsymbol (Name.from_string "cons")
([var_alpha; list_alpha], list_alpha)
let pat = ptuple (pvar x) (pvar y)
let ap = app (var x) (var y)
let int_ = Ty.create_tysymbol (Name.from_string "int") [] None
let t = app (case tk pat [x;y] ap) (tuple ap ap)
let _ = t_app cons [t_nil; tt_nil] list_list_alpha
let _ =
Format.printf "%a@." print t;
Typing.theory [ Formula (close_polyterm [] t) ]
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Pp
open Term
open Ty
let rec print_ty fmt ty = match ty.ty_node with
| Tyvar n ->
fprintf fmt "'%a" Name.print n
| Tyapp (s, []) ->
Name.print fmt s.ty_name
| Tyapp (s, [t]) ->
fprintf fmt "%a %a" print_ty t Name.print s.ty_name
| Tyapp (s, l) ->
fprintf fmt "(%a) %a" (print_list comma print_ty) l Name.print s.ty_name
let rec print_term fmt t = match t.t_node with
| Tbvar n ->
assert false
| Tvar n ->
Name.print fmt n
| Tapp (s, tl) ->
fprintf fmt "(%a(%a) : %a)"
Name.print s.f_name (print_list comma print_term) tl
print_ty t.t_ty
| _ ->
assert false (*TODO*)
let rec print_fmla fmt f =
assert false (*TODO*)
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Term
val print_ty : formatter -> ty -> unit
val print_term : formatter -> term -> unit
val print_fmla : formatter -> fmla -> unit
......@@ -75,9 +75,21 @@ module Ty = struct
let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))
end
exception NoMatching
let rec matching s ty1 ty2 = match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ when Name.M.mem n1 s ->
if Name.M.find n1 s != ty2 then raise NoMatching;
s
| Tyvar n1, _ ->
Name.M.add n1 ty2 s
| Tyapp (f1, l1), Tyapp (f2, l2) when Name.equal f1.ty_name f2.ty_name ->
assert (List.length l1 = List.length l2);
List.fold_left2 matching s l1 l2
| _ ->
raise NoMatching
end
type tysymbol = Ty.tysymbol
type ty = Ty.ty
......@@ -485,7 +497,14 @@ let t_let v t1 t2 = t_let v t1 (abs_term 0 (name_map_singleton v) t2)
(* TODO: checks *)
let t_eps v ty f = t_eps v ty (abs_fmla 0 (name_map_singleton v) f)
let t_app f tl ty = assert false (*TODO*)
let t_app f tl ty =
let args, res = f.f_scheme in
let _ =
List.fold_left2
Ty.matching (Ty.matching Name.M.empty res ty)
args (List.map (fun t -> t.t_ty) tl)
in
t_app f tl ty
let varmap_for_pattern p =
let i = ref (-1) in
......@@ -519,7 +538,15 @@ let f_exists = f_quant Fexists
(* TODO: checks *)
let f_let v t1 f2 = f_let v t1 (abs_fmla 0 (name_map_singleton v) f2)
let f_app s tl = assert false (*TODO*)
let f_app f tl =
let args = f.p_scheme in
let _ =
List.fold_left2
Ty.matching Name.M.empty
args (List.map (fun t -> t.t_ty) tl)
in
f_app f tl
(* TODO: checks *)
let f_case t bl =
......@@ -567,7 +594,7 @@ let open_fbranch (pat, _, f) =
(subst_pat ns pat, vars, subst_fmla 0 s f)
(* TODO : substitution functions named variables -> terms
(* TODO: substitution functions (named variables -> terms)
performing typing *)
(* equality *)
......@@ -641,256 +668,3 @@ and fbranch_alpha_equal (pat1, _, f1) (pat2, _, f2) =
pat_alpha_equal pat1 pat2 && f_alpha_equal f1 f2
(********
type node =
| BVar of int * int
| Var of Name.t
| Tuple of t * t
| App of t * t
| Lam of Ty.t * varbind
| Case of t * case
and t = { tag : int ; node : node }
and varbind = Name.t list * t
and pattern =
| PBVar of int
| PVar of Name.t
| PTuple of pattern * pattern
| Wildcard
and case = pattern * varbind
type decl =
| Logic of Name.t * Ty.scheme
| Formula of poly_term
and poly_term = Name.t list * t
module TBase = struct
type node' = node
type node = node'
type t' = t
type t = t'
let rec equal n1 n2 =
match n1, n2 with
| BVar (i1,j1), BVar (i2,j2) -> i1 = i2 && j1 = j2
| App (ta1, ta2), App (tb1, tb2)
| Tuple (ta1, ta2), Tuple (tb1, tb2) ->
equal_t ta1 tb1 && equal_t ta2 tb2
| Lam (ty1, (n1,t1)), Lam (ty2, (n2,t2)) ->
equal_names n1 n2 && equal_t t1 t2 && Ty.hc_equal ty1 ty2
| Var n1, Var n2 -> Name.equal n1 n2
| Case (ta,(p1,(n1,t1))), Case (tb,(p2,(n2,t2))) ->
equal_t ta tb && equal_pattern p1 p2 &&
equal_names n1 n2 && equal_t t1 t2
| BVar _, _ | _, BVar _ -> false
| Var _, _ | _, Var _ -> false
| App _, _ | _, App _ -> false
| Tuple _, _ | _, Tuple _ -> false
| Lam _, _ | _, Lam _ -> false
and equal_t t1 t2 = t1 == t2
and equal_names l1 l2 = List.for_all2 Name.equal l1 l2
and equal_pattern p1 p2 =
match p1, p2 with
| Wildcard, Wildcard -> true
| PBVar i1, PBVar i2 -> i1 = i2
| PVar n1, PVar n2 -> Name.equal n1 n2
| PTuple (ta1, ta2), PTuple (tb1, tb2) ->
equal_pattern ta1 tb1 && equal_pattern ta2 tb2
| Wildcard, _ | _, Wildcard -> false
| PVar _, _ | _ , PVar _ -> false
| PBVar _, _| _ , PBVar _ -> false
let node t = t.node
open Misc
let rec hash_pattern p =
match p with
| PBVar i -> combine 7 (hash_int i)
| PVar n -> combine 8 (Name.hash n)
| PTuple (p1,p2) -> combine2 9 (hash_pattern p1) (hash_pattern p2)
| Wildcard -> combine 10 11
let hash_name_list =
List.fold_left (fun acc n -> combine2 4 (Name.hash n) acc)
let hash n =
match n with
| BVar (i,j) -> combine2 1 (hash_int i) (hash_int j)
| Var n -> combine 2 (Name.hash n)
| App (t1,t2) -> combine2 3 t1.tag t2.tag
| Lam (ty,(n,t)) -> combine2 12 (hash_name_list t.tag n) (Ty.hash ty)
| Tuple (t1,t2) -> combine2 5 t1.tag t2.tag
| Case (t,(p,(nl,t2))) ->
combine3 6 t.tag (hash_pattern p) (hash_name_list t2.tag nl)
end
module HTerms = Hashcons.Make(TBase)
let equal a b = a.tag = b.tag
let mk_t n t = { tag = t; node = n }
let var n = HTerms.hashcons (Var n) mk_t
let bvar i j = HTerms.hashcons (BVar (i,j)) mk_t
let app t1 t2 = HTerms.hashcons (App (t1,t2)) mk_t
let tuple t1 t2 = HTerms.hashcons (Tuple (t1,t2)) mk_t
let raw_lam t b = HTerms.hashcons (Lam (t,b)) mk_t
let raw_case t p b = HTerms.hashcons (Case (t, (p, b))) mk_t
let build_map nl =
let m,_ =
List.fold_left (fun (m, i) n -> Name.M.add n i m, i + 1)
(Name.M.empty, 0) nl in
m
let abstract nl t =
let m = build_map nl in
let rec aux i t =
match t.node with
| Var n' ->
begin try let j = Name.M.find n' m in bvar i j
with Not_found -> t end
| BVar _ -> t
| App (t1,t2) -> app (aux i t1) (aux i t2)
| Tuple (t1,t2) -> tuple (aux i t1) (aux i t2)
| Lam (ty, (nl,t)) -> raw_lam ty (nl, aux (i+1) t)
| Case (ta,(p,(nl,t))) -> raw_case (aux i ta) p (nl, aux (i+1) t) in
aux 0 t
let abstract_pattern nl p =
let m = build_map nl in
let rec aux p =
match p with
| PVar n ->
begin try let i = Name.M.find n m in PBVar i
with Not_found -> p end
| PBVar _ | Wildcard -> p
| PTuple (p1,p2) -> PTuple (aux p1, aux p2) in
aux p
let instantiate tl t =
let rec aux i t =
match t.node with
| BVar (i',j) when i = i' -> List.nth tl j
| BVar _ | Var _ -> t
| App (t1,t2) -> app (aux i t1) (aux i t2)
| Tuple (t1,t2) -> tuple (aux i t1) (aux i t2)
| Lam (ty, (n,t)) -> raw_lam ty (n, aux (i+1) t)
| Case (t1, (p,(nl,t2))) -> raw_case (aux i t1) p (nl, aux (i+1) t) in
aux 0 t
let instantiate_pattern pl p =
let rec aux p =
match p with
| PBVar i -> List.nth pl i
| PVar _ | Wildcard -> p
| PTuple (p1,p2) -> PTuple (aux p1, aux p2) in
aux p
open Format
let rec print env fmt t =
match t.node with
| BVar (i,j) ->
begin try Name.print fmt (List.nth (List.nth env i) j)
with Invalid_argument "List.nth" -> fprintf fmt "{{%d,%d}}" i j end
| Var n -> Name.print fmt n
| App (t1,t2) -> fprintf fmt "%a %a" (print env) t1 (paren env) t2
| Tuple (t1,t2) -> fprintf fmt "(%a, %a)" (print env) t1 (print env) t2
| Lam (ty, (n,t)) ->
fprintf fmt "(λ%a : %a . %a)"
(Misc.print_list Misc.comma Name.print) n
(Ty.print []) ty
(print (n::env)) t
| Case (t1, (p,(n,t2))) ->
fprintf fmt "case %a of %a -> %a" (print env) t1 (print_pattern n) p
(print (n::env)) t2
and paren env fmt t =
if is_compound t then fprintf fmt "(%a)" (print env) t else print env fmt t
and is_compound t =
(* decide if this term has to be printed with parens in some contexts *)
match t.node with
| BVar _ | Var _ | Lam _ | Tuple _ -> false
| App _ | Case _ -> true
and print_pattern l fmt p =
match p with
| PBVar i ->
begin try Name.print fmt (List.nth l i)
with Invalid_argument "List.nth" -> fprintf fmt "{{%d}}" i end
| PVar v -> Name.print fmt v
| PTuple (t1,t2) ->
fprintf fmt "(%a, %a)" (print_pattern l) t1 (print_pattern l) t2
| Wildcard -> fprintf fmt "_"
let print = print []
let rec alpha_equal a b =
if equal a b then true else
match a.node, b.node with
| BVar (i1,j1), BVar (i2,j2) -> i1 = i2 && j1 = j2
| Var n1, Var n2 -> Name.equal n1 n2
| App (ta1, ta2), App (tb1, tb2)
| Tuple (ta1, ta2), Tuple (tb1, tb2) ->
alpha_equal ta1 tb1 && alpha_equal ta2 tb2
| Lam (ty1, (_,t1)), Lam (ty2, (_,t2)) ->
Ty.equal ty1 ty2 && alpha_equal t1 t2
| Case (ta,(p1,(_,t1))), (Case (tb, (p2,(_,t2)))) ->
alpha_equal ta tb && TBase.equal_pattern p1 p2 && alpha_equal t1 t2
| BVar _, _ | _, BVar _ -> false
| Var _, _ | _, Var _ -> false
| App _, _ | _, App _ -> false
| Tuple _, _ | _, Tuple _ -> false
| Lam _, _ | _, Lam _ -> false
let unsafe_map ~tyfun ~termfun t =
let rec aux t =
let t = match t.node with
| BVar _ | Var _ -> t
| App (t1,t2) -> app (aux t1) (aux t2)
| Tuple (t1,t2) -> tuple (aux t1) (aux t2)
| Case (t1, (p,(n,t2))) -> raw_case (aux t1) p (n,aux t2)
| Lam (ty, (n,t)) -> raw_lam (tyfun ty) (n, aux t) in
termfun t in
aux t
let open_ (n,t) = n, instantiate (List.map var n) t
let close n t =
let n' = List.map Name.fresh n in
n', abstract n t
let lam n ty t = raw_lam ty (close [n] t)
let open_case (p,(nl,t)) =
let pl = List.map (fun n -> PVar n) nl in
let tl = List.map var nl in
instantiate_pattern pl p, nl, instantiate tl t
let close_case p nl t =
let nl' = List.map Name.fresh nl in
abstract_pattern nl p, (nl', abstract nl t)
let case t1 p nl t2 =
let p, b = close_case p nl t2 in
raw_case t1 p b
let wildcard = Wildcard
let pvar x = PVar x
let ptuple p1 p2 = PTuple (p1,p2)
let open_polyterm (nl,t) =
let tl = List.map Ty.var nl in
nl, unsafe_map ~tyfun:(Ty.instantiate tl) ~termfun:(fun x -> x) t
let close_polyterm nl t =
let nl' = List.map Name.fresh nl in
nl', unsafe_map ~tyfun:(Ty.abstract nl) ~termfun:(fun x -> x) t
let open_lam b =
let nl, t = open_ b in
List.hd nl, t
***********)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment