From 84d6740581435cf93258643247eef53d58fabd14 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Feb 2020 11:28:12 +0100 Subject: [PATCH] wip TOYML --- elpi.opam | 1 + tests/sources/toyml/ast.ml | 31 ++++ tests/sources/toyml/dune | 8 ++ tests/sources/toyml/input | 10 ++ tests/sources/toyml/lexer.mll | 21 +++ tests/sources/toyml/output | 136 ++++++++++++++++++ tests/sources/toyml/parser.mly | 54 +++++++ tests/sources/toyml/pmap.ml | 28 ++++ tests/sources/toyml/toyml.ml | 253 +++++++++++++++++++++++++++++++++ tests/sources/toyml/w.elpi | 186 ++++++++++++++++++++++++ 10 files changed, 728 insertions(+) create mode 100644 tests/sources/toyml/ast.ml create mode 100644 tests/sources/toyml/dune create mode 100644 tests/sources/toyml/input create mode 100644 tests/sources/toyml/lexer.mll create mode 100644 tests/sources/toyml/output create mode 100644 tests/sources/toyml/parser.mly create mode 100644 tests/sources/toyml/pmap.ml create mode 100644 tests/sources/toyml/toyml.ml create mode 100644 tests/sources/toyml/w.elpi diff --git a/elpi.opam b/elpi.opam index 36bef824f..7c1c6f0ef 100644 --- a/elpi.opam +++ b/elpi.opam @@ -24,6 +24,7 @@ depends: [ "cmdliner" {with-test} "dune" {>= "1.6"} "conf-time" {with-test} + "ppx_import" {with-test} ] synopsis: "ELPI - Embeddable λProlog Interpreter" description: """ diff --git a/tests/sources/toyml/ast.ml b/tests/sources/toyml/ast.ml new file mode 100644 index 000000000..30d23b433 --- /dev/null +++ b/tests/sources/toyml/ast.ml @@ -0,0 +1,31 @@ +type pos = [%import: Lexing.position] [@@deriving show, ord, eq] +type position = pos * pos [@@deriving show, ord, eq] + +type term = + | Const of string (* global name or bound variable *) + | Int of int (* literals *) + | App of ast * ast + | Lam of string * ast + | Let of string * ast * ast + | Eq of ast * ast +and ast = { loc : position; v : term } +[@@deriving show] + +type tye = + | Var of string + | Integer + | Boolean + | Arrow of tye * tye + | List of tye + | Pair of tye * tye +[@@deriving show] + +type quantification = + | Any + | EqualityType +[@@deriving show] + +type typ = + | All of string * quantification * typ + | Mono of tye +[@@deriving show] diff --git a/tests/sources/toyml/dune b/tests/sources/toyml/dune new file mode 100644 index 000000000..c02f8e9ba --- /dev/null +++ b/tests/sources/toyml/dune @@ -0,0 +1,8 @@ +(executable + (name toyml) + (modules ast lexer parser pmap toyml) + (preprocess (per_module ((pps ppx_import ppx_deriving.std) ast))) + (libraries elpi ppx_import ppx_deriving.std)) + +(ocamllex lexer) +(ocamlyacc parser) \ No newline at end of file diff --git a/tests/sources/toyml/input b/tests/sources/toyml/input new file mode 100644 index 000000000..6bbb65c6e --- /dev/null +++ b/tests/sources/toyml/input @@ -0,0 +1,10 @@ +3 = 2 +(fun x -> x) = (fun x -> x) +let id x = x in id [] +let id x = x in (id [], id 1) +let refl x = x = x in refl [] +let refl x = x = x in refl (fun x -> x) +let card x = size (undup x) in card [] +let f y = let g x = (x,y) in g y in f 1 +size 1 +[1] = (1,1) diff --git a/tests/sources/toyml/lexer.mll b/tests/sources/toyml/lexer.mll new file mode 100644 index 000000000..3b83261ba --- /dev/null +++ b/tests/sources/toyml/lexer.mll @@ -0,0 +1,21 @@ +(* File lexer.mll *) +{ +open Parser (* The type token is defined in parser.mli *) +exception Eof +} +rule token = parse + [' ' '\t' '\n'] { token lexbuf } (* skip blanks *) + | ['0'-'9']+ as lxm { INT(int_of_string lxm) } + | "let" { LET } + | "in" { IN } + | "fun" { LAM } + | ['a'-'z']+ as lxm { IDENT lxm } + | '(' { LPAREN } + | ')' { RPAREN } + | '[' { LBRK } + | ']' { RBRK } + | '=' { EQ } + | ',' { COMMA } + | ';' { SEMICOLON } + | "->" { ARROW } + | eof { EOF } diff --git a/tests/sources/toyml/output b/tests/sources/toyml/output new file mode 100644 index 000000000..06aea1dcf --- /dev/null +++ b/tests/sources/toyml/output @@ -0,0 +1,136 @@ + +========= builtins ========== + + +external pred type-error % raise a fatal type inference error + i:any, % the term + i:any, % its type + i:any. % the type expected by its context + +external pred eqtype-error % raise a fatal equality type error + i:any. % the term + + + + + +============= W: 3 = 2 ============== +The term: + 3 = 2 + ^^^^^ +has type: mono boolean + + +============= W: (fun x -> x) = (fun x -> x) ============== +The term: + (fun x -> x) = (fun x -> x) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono boolean + +Equality type constraint unsatisfied at: + (fun x -> x) = (fun x -> x) + ^^^^^^^^^^ + +============= W: let id x = x in id [] ============== +The term: + let id x = x in id [] + ^^^^^^^^^^^^^^^^^^^^^ +has type: mono (list X0) + +The term: + let id x = x in id [] + ^^^^^ +has type: all any c0 \ mono (c0 ==> c0) + + +============= W: let id x = x in (id [], id 1) ============== +The term: + let id x = x in (id [], id 1) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono (pair (list X1) integer) + +The term: + let id x = x in (id [], id 1) + ^^^^^ +has type: all any c0 \ mono (c0 ==> c0) + + +============= W: let refl x = x = x in refl [] ============== +The term: + let refl x = x = x in refl [] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono boolean + +The term: + let refl x = x = x in refl [] + ^^^^^^^^^ +has type: all eqt c0 \ mono (c0 ==> boolean) + + +============= W: let refl x = x = x in refl (fun x -> x) ============== +The term: + let refl x = x = x in refl (fun x -> x) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono boolean + +The term: + let refl x = x = x in refl (fun x -> x) + ^^^^^^^^^ +has type: all eqt c0 \ mono (c0 ==> boolean) + +Equality type constraint unsatisfied at: + let refl x = x = x in refl (fun x -> x) + ^^^^ + +============= W: let card x = size (undup x) in card [] ============== +The term: + let card x = size (undup x) in card [] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono integer + +The term: + let card x = size (undup x) in card [] + ^^^^^^^^^^^^^^^^^^ +has type: all eqt c0 \ mono (list c0 ==> integer) + + +============= W: let f y = let g x = (x,y) in g y in f 1 ============== +The term: + let f y = let g x = (x,y) in g y in f 1 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: mono (pair integer integer) + +The term: + let f y = let g x = (x,y) in g y in f 1 + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +has type: all any c0 \ mono (c0 ==> pair c0 c0) + +The term: + let f y = let g x = (x,y) in g y in f 1 + ^^^^^^^^^ +has type: all any c0 \ mono (c0 ==> pair c0 X2) + + +============= W: size 1 ============== +The term: + size 1 + ^^^^^^ +has type: mono integer + +Type error: + size 1 + ^ +has type integer +but is expected to have type list X3 + +============= W: [1] = (1,1) ============== +The term: + [1] = (1,1) + ^^^^^^^^^^^ +has type: mono boolean + +Type error: + [1] = (1,1) + ^ +has type X4 ==> X5 ==> pair X4 X5 +but is expected to have type X6 ==> X7 ==> list integer diff --git a/tests/sources/toyml/parser.mly b/tests/sources/toyml/parser.mly new file mode 100644 index 000000000..80a35cd0d --- /dev/null +++ b/tests/sources/toyml/parser.mly @@ -0,0 +1,54 @@ + /* File parser.mly */ + %{ +open Ast + let mkloc i j = (Parsing.rhs_start_pos i, Parsing.rhs_end_pos j) + let rec mklam = function + | [] -> fun x -> x + | (loc,x)::xs -> fun b -> { loc = (fst loc, snd b.loc); v = Lam(x,mklam xs b) } + let rec mklist loc = function + | [] -> { loc; v = Const "[]" } + | (loc,x) :: xs -> { loc; v = App( { loc; v = App( { loc; v = Const "::" }, x) }, mklist loc xs) } + %} + %token INT + %token IDENT + %token LET IN LAM ARROW + %token LPAREN RPAREN EQ LBRK RBRK COMMA SEMICOLON + %token EOF + %start main /* the entry point */ + %type main + %% + main: term EOF { $1 } ; + + term0: + | INT { { loc = mkloc 1 1; + v = Int $1 }} + | LPAREN term RPAREN { $2 } + | LPAREN term COMMA term RPAREN + { { loc = mkloc 1 5; v = App( { loc = mkloc 1 3; v = App({ loc = mkloc 3 3; v = Const "," } ,$2) }, $4 ) } } + | LBRK term_list RBRK { mklist (mkloc 1 3) $2 } + | IDENT { { loc = mkloc 1 1; v = Const $1 } } + ; + + term_list: + | term SEMICOLON term_list { (mkloc 1 2, $1) :: $3 } + | term { [(mkloc 1 1, $1)] } + | { [] } + ; + + term: + | LET idlist EQ term IN term { { loc = mkloc 1 6; v = Let(snd (List.hd $2),mklam (List.tl $2) $4,$6) }} + | LAM IDENT ARROW term { { loc = mkloc 1 4; v = Lam($2,$4) }} + | term EQ term { { loc = mkloc 1 3; v = Eq($1,$3) } } + | app { $1 } + ; + app: + | app term0 { { loc = mkloc 1 2; v = App($1,$2) } } + | term0 { $1 } + ; + + idlist: + | IDENT { [(mkloc 1 1, $1)] } + | IDENT idlist { (mkloc 1 2, $1) :: $2 } + ; + + diff --git a/tests/sources/toyml/pmap.ml b/tests/sources/toyml/pmap.ml new file mode 100644 index 000000000..f4366d955 --- /dev/null +++ b/tests/sources/toyml/pmap.ml @@ -0,0 +1,28 @@ +module type T = sig + type t + val hash : t -> int +end + +module Make(X : T) = struct + module M = Map.Make(struct + type t = int + let compare x y = x - y + end) + type 'a t = (X.t * 'a) list M.t + let empty = M.empty + let add k v m = + let h = X.hash k in + try + let l = M.find h m in + let l = List.remove_assq k l in + M.add h ((k,v) :: l) m + with Not_found -> + M.add h [k,v] m + let find_opt k m = + try + let h = Hashtbl.hash k in + let l = M.find h m in + Some (List.assq k l) + with Not_found -> None + +end diff --git a/tests/sources/toyml/toyml.ml b/tests/sources/toyml/toyml.ml new file mode 100644 index 000000000..f0a3aee15 --- /dev/null +++ b/tests/sources/toyml/toyml.ml @@ -0,0 +1,253 @@ +open Ast + +open Elpi.API +module E = RawData +module C = Compile +module Pp = Pp +module M = Data.StrMap + +let position = let open OpaqueData in declare { + name = "position"; + doc = "locations in the input file"; + pp = pp_position; + compare = compare_position; + hash = Hashtbl.hash; + hconsed = false; + constants = []; +} + +(* types - elpi terms ************************************************** *) + +let ty_ctx = State.declare ~name:"toyml:ty_ctx" ~pp:(fun fmt _ -> Format.fprintf fmt "TODO") + ~init:(fun () -> []) + +let tye = let open AlgebraicData in declare { + ty = Conversion.TyName "tye"; + doc = "Monomorphic type expressions"; + pp = pp_tye; + constructors = [ + K("(==>)","function space",S(S N), + B (fun t1 t2 -> Arrow (t1, t2)), + M (fun ~ok ~ko -> function Arrow(t1,t2) -> ok t1 t2 | _ -> ko ())); + K("integer","",N, + B Integer, + M (fun ~ok ~ko -> function Integer -> ok | _ -> ko ())); + K("boolean","",N, + B Boolean, + M (fun ~ok ~ko -> function Boolean -> ok | _ -> ko ())); + K("list","",S N, + B (fun x -> List x), + M (fun ~ok ~ko -> function List x -> ok x | _ -> ko ())); + K("pair","",S (S N), + B (fun x y -> Pair(x,y)), + M (fun ~ok ~ko -> function Pair (x,y) -> ok x y | _ -> ko ())); + K("","",A(BuiltInData.string,N), + BS (fun s st -> st, Var s), + MS (fun ~ok ~ko -> function + | Var s -> ok s (fun st -> st, E.mkBound (List.assoc s (State.get ty_ctx st)), []) + | _ -> ko)) + ] +} |> ContextualConversion.(!<) + +let quantification = let open AlgebraicData in declare { + ty = Conversion.TyName "eq?"; + doc = "kind of quantification"; + pp = pp_quantification; + constructors = [ + K("eqt","",N, + B EqualityType, + M(fun ~ok ~ko -> function EqualityType -> ok | _ -> ko ())); + K("any","",N, + B Any, + M(fun ~ok ~ko -> function Any -> ok | _ -> ko ())); + ] +} |> ContextualConversion.(!<) + +let allc = E.Constants.declare_global_symbol "all" +let monoc = E.Constants.declare_global_symbol "mono" + +let rec embed_typ : typ Conversion.embedding = fun ~depth st -> function + | Mono m -> + let st, tye, gls = tye.Conversion.embed ~depth st m in + st, E.mkApp monoc tye [], gls + | All(q,rest) -> + let st, q, gls = quantification.Conversion.embed ~depth st q in + x + ;; + + +(* terms - elpi terms ************************************************** *) + +let appc = E.Constants.declare_global_symbol "app" +let lamc = E.Constants.declare_global_symbol "lam" +let letc = E.Constants.declare_global_symbol "let" +let eqc = E.Constants.declare_global_symbol "eq" +let literalc = E.Constants.declare_global_symbol "literal" +let globalc = E.Constants.declare_global_symbol "global" + +let nodec = E.Constants.declare_global_symbol "node" + +let rec lookup x = function + | [] -> E.mkApp globalc (RawOpaqueData.of_string x) [] + | y :: ys when x = y -> E.mkConst (List.length ys) + | _ :: ys -> lookup x ys + +let rec embed st ctx { v; loc } = begin + match v with + | Const s -> st, lookup s ctx + | Int n -> st, E.mkApp literalc (RawOpaqueData.of_int n) [] + | App(h,a) -> + let st, h = embed st ctx h in + let st, a = embed st ctx a in + st, E.mkApp appc h [a] + | Lam (n,t) -> + let st, t = embed st (n :: ctx) t in + st, E.mkApp lamc (E.mkLam t) [] + | Let(n, t, b) -> + let st, ty = FlexibleData.Elpi.make st t.loc in + let st, t = embed st ctx t in + let st, b = embed st (n :: ctx) b in + st, E.mkApp letc t [ty; E.mkLam b] + | Eq(lhs, rhs) -> + let st, lhs = embed st ctx lhs in + let st, rhs = embed st ctx rhs in + st, E.mkApp eqc lhs [rhs] +end + +let term = + let open Conversion in + { + ty = TyName "term"; + pp_doc = (fun fmt () -> Format.fprintf fmt "The data type of terms") + pp = Ast.pp_term; + embed = embed_term; + readback = readback_term; + } + +(* builtin *************************************************************** *) + +exception TypeError of { + assignments : E.term M.t; + state : State.t; + + t : E.term; + ty : E.term; + ety : E.term; +} +exception NotEqType of { + assignments : E.term M.t; + state : State.t; + + t : E.term; +} + +let extra_builtins = + let open BuiltInPredicate in + let open BuiltInData in + let open BuiltIn in + declare ~file_name:"toyml-builtin.elpi" [ + + MLCode(Pred("type-error", + In(any,"the term", + In(any,"its type", + In(any,"the type expected by its context", + Easy("raise a fatal type inference error")))), + (fun t ty ety ~depth:_ _ { assignments; state } -> + raise (TypeError{assignments; state; t; ty; ety }))), + DocNext); + + MLCode(Pred("eqtype-error", + In(any,"the term", + Easy("raise a fatal equality type error")), + (fun t ~depth:_ _ { assignments; state } -> + raise (NotEqType{assignments; state; t}))), + DocNext); + +] + +let _ = BuiltIn.document_file extra_builtins ;; + +(* w ********************************************************************* *) + +let subtext text fmt ( { Lexing.pos_cnum = a; _ } , { Lexing.pos_cnum = b; _ } ) = + let open String in + Format.fprintf fmt "@[ %s@;%s@]" text + (make a ' ' ^ make (b-a) '^' ^ make (length text - b) ' ') + +let pp_result text assignments state = + M.iter (fun k v -> + let loc = M.find k (State.get rs_output state) in + Format.printf "@[The term:@ %a@ has type: %a@]@\n@\n" + (subtext text) loc (Pp.term 0) v) + assignments + +let pp_type_err text t ty ety state = + let loc = P.find_opt t (State.get rs_positions state) in + match loc with + | Some loc -> + Format.printf "@[Type error:@ %a@ has type %a@ but is expected to have type %a@]@\n%!" (subtext text) loc (Pp.term 0) ty (Pp.term 0) ety + | None -> + Format.printf "@[Type error:@ the term: %a@ has type %a@ but is expected to have type %a@]@\n%!" (Pp.term 0) t (Pp.term 0) ty (Pp.term 0) ety + +let pp_eqtype_err text t state = + let loc = P.find_opt t (State.get rs_positions state) in + match loc with + | Some loc -> + Format.printf "@[Equality type constraint unsatisfied at:@ %a@]@\n%!" (subtext text) loc + | None -> + Format.printf "@[Equality type constraint unsatisfied at:@ %a@]@\n%!"(Pp.term 0) t + +let w = + (* load the elpi program *) + let elpi_flags = + try + let ic, _ as p = Unix.open_process "elpi -where 2>/dev/null" in + let w = input_line ic in + let _ = Unix.close_process p in ["-I";w] + with _ -> [] in + let builtins = [Elpi.Builtin.std_builtins; extra_builtins] in + let elpi, _ = Setup.init ~builtins ~basedir:"./" + (elpi_flags @ List.tl (Array.to_list Sys.argv)) in + + let p = Parse.program ~elpi ["w.elpi"] in + let p = Compile.program ~flags:Compile.default_flags ~elpi [p] in + +fun (text, ast) -> + (* run w on a term *) + let q = + let open Query in + let spec = Query { predicate = "main"; arguments = D(term,ast,Q(typ,"Q",N)) } in + compile p (Ast.Loc.initial "(query)") spec in + if Array.mem "-typecheck" Sys.argv then begin + if not (Compile.static_check ~checker:(Elpi.Builtin.default_checker ()) q) then + failwith "w.elpi does not type check"; + end; + + let exe = Compile.optimize q in + + Format.printf "\n============= W: %s ==============\n%!" text; + match Execute.once exe with + | Execute.Success { Data.assignments; state; _ } -> + pp_result text assignments state + | Failure -> failwith "w.elpi is buggy" + | NoMoreSteps -> assert false + | exception TypeError{assignments; state; t; ty; ety } -> + pp_result text assignments state; + pp_type_err text t ty ety state + | exception NotEqType{assignments; state; t } -> + pp_result text assignments state; + pp_eqtype_err text t state +;; + +(* main ****************************************************************** *) + +let parse s = s, Parser.main Lexer.token (Lexing.from_string s) + +let _ = + try + while true; do + w @@ parse @@ input_line stdin; + done + with End_of_file -> () + +(* vim:set foldmethod=marker: *) diff --git a/tests/sources/toyml/w.elpi b/tests/sources/toyml/w.elpi new file mode 100644 index 000000000..ad49c6e6d --- /dev/null +++ b/tests/sources/toyml/w.elpi @@ -0,0 +1,186 @@ +%%%%%%%%%%% datatypes %%%%%%%%%%%%%%% + +% terms +kind term type. + +type literal int -> term. +type global string -> term. + +type app term -> term -> term. +type lam (term -> term) -> term. +type let term -> ty -> (term -> term) -> term. +type eq term -> term -> term. + + +% type expressions +kind tye type. + +infixr ==> 50. + +type (==>) tye -> tye -> tye. +type integer tye. +type boolean tye. +type list tye -> tye. +type pair tye -> tye -> tye. + +% types +kind eq? type. +type any eq?. +type eqt eq?. + +kind ty type. + +type all eq? -> (tye -> ty) -> ty. +type mono tye -> ty. + +%%%%%%%%%%%% w %%%%%%%%%%%%%% + +pred w i:term, o:ty. + +% constants + +w (literal _) (mono integer). +w (global "plus") (mono (integer ==> integer ==> integer)). + +w (global "[]") (all any x\ mono (list x)). +w (global "::") (all any x\ mono (x ==> list x ==> list x)). +w (global "size") (all any x\ mono (list x ==> integer)). +w (global "undup") (all eqt x\ mono (list x ==> list x)). + +w (global ",") (all any x\ all any y\ mono (x ==> y ==> (pair x y))). + +% terms + +w (app H A) (mono T) :- + w H (mono (S ==> T)), + w A (mono S). + +w (lam F) (mono (S ==> T)) :- + pi x\ w x (mono S) => w (F x) (mono T). + +w (let E PT B) (mono TB) :- + w E (mono T), + gammabar (mono T) PT, + pi x\ w x PT => w (B x) (mono TB). + +w (eq LHS RHS) (mono boolean) :- + w LHS (mono T), + w RHS (mono T1), (T = T1 ; type-error RHS T1 T ), + eqbar LHS T. + +w X (mono T) :- w X (all E Poly), specialize X (all E Poly) T. + +pred err. + +w X (mono ETY) :- not err, err => w X (mono TY), type-error X TY ETY. + +% schemas +pred specialize i:term, i:ty, o:tye. + +specialize X (all any F) T :- specialize X (F E_) T. +specialize X (all eqt F) T :- specialize X (F E) T, (eqbar X E). +specialize _ (mono T) T. + +specialize X (mono TY) ETY :- type-error X TY ETY. + +% main +main T TY :- theta [], w T TY. + +%%%%%%%%%%%%% theta %%%%%%%%%%%%%%%% + +pred theta i:list tye. + +theta L :- new_constraint (theta L) [_]. + +constraint w gammabar eqbar theta { + +rule (eqbar _ V) \ (theta L) | (not(mem-theta L V)) <=> (theta (V :: L)). + +% 'uvar X L' is the frozen 'X' and its arguments 'L' +mem-theta (uvar X _ :: _) (uvar X _). +mem-theta (uvar _ _ :: XS) Y :- mem-theta XS Y. + +} + +%%%%%%%%%%%%% eqbar %%%%%%%%%%%%%%%% + +pred eqbar i:term, i:tye. + +eqbar _ boolean. +eqbar _ integer. +eqbar X (list A) :- eqbar X A. +eqbar X (pair A B) :- eqbar X A, eqbar X B. + +eqbar X T :- var T, new_constraint (eqbar X T) [T,_]. + +eqbar X _ :- eqtype-error X. + +%%%%%%%%%%%% gammabar %%%%%%%%%%%%% + +pred gammabar i:ty, o:ty. + +gammabar (mono T) TS :- + new_constraint (gammabar (mono T) TS) [_]. + +constraint w gammabar eqbar theta { + +rule (theta L) % matched + \ (G ?- gammabar T TS) % matched and removed + | (generalize L G T POLYT) % guard + syntesis + <=> (TS = POLYT). % new goal + +generalize Theta Gamma (mono T) PolyT :- + free-ty (mono T) [] VT, + free-gamma Gamma [] VGamma, + filter VT (x\ not(mem VGamma x)) ToQuantify, + bind ToQuantify Theta T PolyT. + +% computation of free (unification) variables +free-ty (mono X) L L1 :- free X L L1. +free-ty (all _ F) L L1 :- pi x\ free-ty (F x) L L1. + +free-gamma [] L L. +free-gamma [w _ T|X] L L2 :- free-ty T L L1, free-gamma X L1 L2. + +free (list A) L L1 :- free A L L1. +free (pair A B) L L2 :- free A L L1, free B L1 L2. +free (A ==> B) L L2 :- free A L L1, free B L1 L2. +free (uvar X _) L L1 :- if (mem L X) (L1 = L) (L1 = [X|L]). +free _ L L. + +% quantification (binding) of a list of variables +bind [] _ T (mono T1) :- copy T T1. +bind [X|XS] Theta T (all E x\ T2 x) :- + if (mem-theta Theta (uvar X _)) (E = eqt) (E = any), + bind XS Theta T T1, + pi c\ copy (uvar X _) c => copy-ty T1 (T2 c). + +copy-ty (mono X1) (mono X2) :- copy X1 X2. +copy-ty (all E F1) (all E F2) :- pi x\ copy x x => copy-ty (F1 x) (F2 x). + +copy integer integer. +copy boolean boolean. +copy (A ==> B) (A1 ==> B1) :- copy A A1, copy B B1. +copy (list A) (list A1) :- copy A A1. +copy (pair A B) (pair A1 B1) :- copy A A1, copy B B1. +copy (uvar U L) (uvar U L). + +} + +% {{{ stdlib: mem, filter, if... + +new_constraint P L :- declare_constraint P L. + +filter [] _ []. +filter [X|XS] P [X|YS] :- P X, !, filter XS P YS. +filter [_|XS] P YS :- filter XS P YS. + +mem [X|_] X :- !. +mem [_|XS] X :- mem XS X. + +if G T _ :- G, !, T. +if _ _ E :- E. + +% }}} + +% vim:set foldmethod=marker spelllang=: