Commit 00e7ec53 authored by Hector Suzanne's avatar Hector Suzanne
Browse files

Cleanup et constructeurs n-aires

parent 90fc9f96
open Autobill
open Cst_intf
open Intern_intf
open Sort_intf
let version =
match Build_info.V1.version () with
......
......@@ -10,10 +10,10 @@ type ('tycons, 't) type_cons =
| Bottom
| ShiftPos of 't
| ShiftNeg of 't
| Prod of 't * 't
| Sum of 't * 't
| Fun of 't * 't
| Choice of 't * 't
| Prod of 't list
| Sum of 't list
| Fun of 't list * 't
| Choice of 't list
| Cons of 'tycons * 't list
let unit_t = Unit
......@@ -22,10 +22,10 @@ let top = Top
let bottom = Bottom
let shift_pos_t a = ShiftPos a
let shift_neg_t a = ShiftNeg a
let prod a b = Prod (a,b)
let sum a b = Sum (a,b)
let func a b = Fun (a,b)
let choice a b = Choice (a,b)
let prod a b = Prod [a;b]
let sum a b = Sum [a;b]
let func a b = Fun ([a],b)
let choice a b = Choice [a;b]
let typecons v args = Cons (v,args)
let string_of_type_cons kvar k cons =
......@@ -40,10 +40,10 @@ let string_of_type_cons kvar k cons =
| Bottom -> "bottom"
| ShiftPos a -> pp_texp "+" [k a]
| ShiftNeg a -> pp_texp "-" [k a]
| Prod (a,b) -> pp_texp "prod" [k a; k b]
| Sum (a,b) -> pp_texp "sum" [k a; k b]
| Fun (a,b) -> pp_texp "fun" [k a; k b]
| Choice (a,b) -> pp_texp "choice" [k a; k b]
| Prod ts -> pp_texp "prod" (List.map k ts)
| Sum ts -> pp_texp "sum" (List.map k ts)
| Fun (a,b) -> pp_texp "fun" (List.map k a @ [k b])
| Choice ts -> pp_texp "choice" (List.map k ts)
| Cons (var,args) -> pp_texp (kvar var) (List.map k args)
......@@ -52,24 +52,23 @@ let cons_names = ["unit"; "pair"; "left"; "right"]
type ('var, 'x) constructor =
| Unit
| ShiftPos of 'x
| Pair of 'x * 'x
| Left of 'x
| Right of 'x
| Tupple of 'x list
| Inj of int * int * 'x
| PosCons of 'var * 'x list
let unit = Unit
let pair a b = Pair (a,b)
let left a = Left a
let right b = Right b
let pair a b = Tupple [a;b]
let left a = Inj (0, 2, a)
let right b = Inj (1, 2, b)
let shift_pos a = ShiftPos a
let poscons c args = PosCons (c,args)
let string_of_constructor kvar k = function
| Unit -> "unit()"
| ShiftPos x -> "shift+(" ^ k x ^ ")"
| Pair (x,y) -> "pair" ^ (string_of_tupple k [x;y])
| Left x -> "left(" ^ k x ^ ")"
| Right x -> "right(" ^ k x ^ ")"
| Tupple t -> "pair" ^ (string_of_tupple k t)
| Inj (i,n,x) ->
"inj(" ^ string_of_int i ^ "/" ^ string_of_int n ^ ", " ^ k x ^ ")"
| PosCons (name, args) -> (kvar name) ^ (string_of_tupple k args)
let consvar_of_constructor = function
......@@ -79,22 +78,20 @@ let consvar_of_constructor = function
let destr_names = ["call"; "yes"; "no"]
type ('var, 'x ,'a) destructor =
| Call of 'x * 'a
| Yes of 'a
| No of 'a
| Call of 'x list * 'a
| Proj of int * int * 'a
| ShiftNeg of 'a
| NegCons of 'var * 'x list * 'a
let call x a = Call (x,a)
let yes a = Yes a
let no a = No a
let call x a = Call ([x],a)
let yes a = Proj (0, 2, a)
let no a = Proj (1, 2, a)
let shift_neg a = ShiftNeg a
let negcons c args cont = NegCons (c,args,cont)
let string_of_destructor kvar kx ka = function
| Call (x,a) -> Printf.sprintf ".call(%s)%s" (kx x) (ka a)
| Yes a -> ".yes()" ^ ka a
| No a -> ".no()" ^ ka a
| Call (x,a) -> Printf.sprintf ".call%s%s" (string_of_tupple kx x) (ka a)
| Proj (i, n, a) -> ".proj(" ^ string_of_int i ^ "/" ^ string_of_int n ^ ")." ^ ka a
| ShiftNeg a -> "shift-(" ^ ka a ^ ")"
| NegCons (name, args, a) ->
let cons = kvar name in
......
......@@ -10,10 +10,10 @@ type ('var, 't) type_cons =
| Bottom
| ShiftPos of 't
| ShiftNeg of 't
| Prod of 't * 't
| Sum of 't * 't
| Fun of 't * 't
| Choice of 't * 't
| Prod of 't list
| Sum of 't list
| Fun of 't list * 't
| Choice of 't list
| Cons of 'var * 't list
val unit_t : ('var, 'a) type_cons
......@@ -36,9 +36,8 @@ val cons_names : string list
type ('var, 'x) constructor =
| Unit
| ShiftPos of 'x
| Pair of 'x * 'x
| Left of 'x
| Right of 'x
| Tupple of 'x list
| Inj of int * int * 'x
| PosCons of 'var * 'x list
val unit : ('var, 'x) constructor
......@@ -55,9 +54,8 @@ val consvar_of_constructor : ('var, 'x) constructor -> 'var option
val destr_names : string list
type ('var, 'x ,'a) destructor =
| Call of 'x * 'a
| Yes of 'a
| No of 'a
| Call of 'x list * 'a
| Proj of int * int * 'a
| ShiftNeg of 'a
| NegCons of 'var * 'x list * 'a
......
......@@ -34,10 +34,14 @@ let rec pp_typ fmt t =
| Bottom -> pp_print_string fmt "bottom"
| ShiftPos a -> fprintf fmt "@[<hov 2>(shift+@ %a)@]" pp_typ a
| ShiftNeg a -> fprintf fmt "@[<hov 2>(shift-@ %a)@]" pp_typ a
| Prod (a,b) -> fprintf fmt "@[<hov 2>(prod@ %a@ %a)@]" pp_typ a pp_typ b
| Sum (a,b) -> fprintf fmt "@[<hov 2>(sum@ %a@ %a)@]" pp_typ a pp_typ b
| Fun (a,b) -> fprintf fmt "@[<hov 2>(fun@ %a@ %a)@]" pp_typ a pp_typ b
| Choice (a,b) -> fprintf fmt "@[<hov 2>(choice@ %a@ %a)@]" pp_typ a pp_typ b
| Prod bs -> fprintf fmt "@[<hov 2>(prod@ %a)@]"
(pp_print_list ~pp_sep:pp_print_space pp_typ) bs
| Sum bs -> fprintf fmt "@[<hov 2>(sum@ %a)@]"
(pp_print_list ~pp_sep:pp_print_space pp_typ) bs
| Fun (a,b) -> fprintf fmt "@[<hov 2>(fun@ %a@ %a)@]"
(pp_print_list ~pp_sep:pp_print_space pp_typ) a pp_typ b
| Choice bs -> fprintf fmt "@[<hov 2>(choice@ %a)@]"
(pp_print_list ~pp_sep:pp_print_space pp_typ) bs
| Cons (c,args) ->
if List.length args = 0 then
pp_tyvar fmt c
......@@ -49,9 +53,9 @@ let rec pp_typ fmt t =
let pp_constructor pp_kvar pp_k fmt cons =
match cons with
| Unit -> pp_print_string fmt "unit()"
| Pair (a,b) -> fprintf fmt "@[<hov 2>pair(@,%a,@ %a)@]" pp_k a pp_k b
| Left x -> fprintf fmt "left(%a)" pp_k x
| Right x -> fprintf fmt "right(%a)" pp_k x
| Tupple vs ->
fprintf fmt "@[<hov 2>tupple(%a)@]" (pp_print_list ~pp_sep:pp_comma_sep pp_k) vs
| Inj (i,n,x) -> fprintf fmt "inj(%n/%n, %a)" i n pp_k x
| ShiftPos x -> fprintf fmt "shift+(%a)" pp_k x
| PosCons (c, args) ->
fprintf fmt ":%a(@[<hov 2>%a@])"
......@@ -60,9 +64,9 @@ let pp_constructor pp_kvar pp_k fmt cons =
let pp_destructor pp_kvar pp_k pp_ka fmt destr =
match destr with
| Call (x,a) -> fprintf fmt ".call(%a)%a" pp_k x pp_ka a
| Yes a -> fprintf fmt ".yes()%a" pp_ka a
| No a -> fprintf fmt ".no()%a" pp_ka a
| Call (x,a) -> fprintf fmt ".call(%a)%a"
(pp_print_list ~pp_sep:pp_comma_sep pp_k) x pp_ka a
| Proj (i,n,a) -> fprintf fmt ".proj(%n/%n)%a" i n pp_ka a
| ShiftNeg a -> fprintf fmt ".shift-()%a" pp_ka a
| NegCons (c, args, a) ->
fprintf fmt ".%a(@[<hov 2>%a@])%a"
......
......@@ -4,6 +4,7 @@
exception Error of string
}
let num = ['0'-'9']*
let alphanum = ['a'-'z' 'A'-'Z' '0'-'9' '_']*
let meta = [^ '>']*
let name = ['a'-'z'] alphanum
......@@ -12,6 +13,9 @@ let newline = '\r' | '\n' | "\r\n"
rule token = parse
| "//" {line_comment lexbuf}
| "/*" {delim_comment lexbuf}
| '(' {LPAREN}
| ')' {RPAREN}
| ':' {COLUMN}
......@@ -21,6 +25,7 @@ rule token = parse
| '.' {DOT}
| ',' {COMMA}
| "->" {ARROW}
| '/' {SLASH}
| "ret" {RET}
| "this" {THIS}
......@@ -42,12 +47,14 @@ rule token = parse
| "aff" {AFFINE}
| "exp" {EXP}
| "pair" {PAIR}
| "tupple" {TUPPLE}
| "left" {LEFT}
| "right" {RIGHT}
| "inj" {INJ}
| "call" {CALL}
| "yes" {YES}
| "no" {NO}
| "proj" {PROJ}
| "shift" {SHIFT}
| "unit" {UNIT}
......@@ -67,9 +74,7 @@ rule token = parse
| "env" {ENV}
| "cmd" {CMD}
| "//" {line_comment lexbuf}
| "/*" {delim_comment lexbuf}
| num {NUM (int_of_string (Lexing.lexeme lexbuf))}
| name {VAR (Lexing.lexeme lexbuf)}
| '<' meta '>' {META}
| eof {EOF}
......
......@@ -9,14 +9,15 @@
module Autobill = struct end
%}
%token COLUMN PLUS EQUAL MINUS DOT ARROW COMMA META
%token COLUMN PLUS EQUAL MINUS DOT ARROW COMMA SLASH META
%token LPAREN RPAREN
%token STEP INTO WITH BIND BINDCC MATCH CASE RET END THIS IN DO
%token BOX UNBOX LINEAR AFFINE EXP
%token PAIR LEFT RIGHT CALL YES NO
%token TUPPLE INJ CALL PROJ LEFT RIGHT YES NO
%token UNIT ZERO PROD SUM FUN CHOICE TOP BOTTOM SHIFT
%token DECL TYPE DATA CODATA TERM ENV CMD
%token <string> VAR
%token <int> NUM
%token EOF
%start <program> prog
......@@ -156,16 +157,18 @@ destr:
| cons = destrvar LPAREN args = separated_list(COMMA, typed_var) RPAREN
DOT RET LPAREN RPAREN typ = typ_annot
{ negcons cons args typ }
| CALL LPAREN var = typed_var RPAREN DOT RET LPAREN RPAREN typ = typ_annot {call var typ}
| CALL LPAREN vars = separated_list(COMMA, typed_var) RPAREN DOT RET LPAREN RPAREN typ = typ_annot {Call (vars, typ)}
| YES LPAREN RPAREN DOT RET LPAREN RPAREN typ = typ_annot {yes typ}
| NO LPAREN RPAREN DOT RET LPAREN RPAREN typ = typ_annot {no typ}
| PROJ LPAREN i = NUM SLASH n = NUM RPAREN DOT RET LPAREN RPAREN typ = typ_annot {Proj (i,n,typ)}
| SHIFT MINUS LPAREN RPAREN DOT RET LPAREN RPAREN typ = typ_annot {shift_neg typ}
value_cons:
| UNIT LPAREN RPAREN { unit }
| PAIR LPAREN a = value COMMA b = value RPAREN {pair a b}
| TUPPLE LPAREN xs = separated_list(COMMA, value) RPAREN {Tupple xs}
| LEFT LPAREN a = value RPAREN {left a}
| RIGHT LPAREN b = value RPAREN {right b}
| INJ LPAREN i = NUM SLASH n = NUM COMMA a = value RPAREN {Inj (i,n,a)}
| SHIFT PLUS LPAREN a = value RPAREN {shift_pos a}
| cons = consvar LPAREN args = separated_list(COMMA,value) RPAREN {poscons cons args}
......@@ -175,12 +178,14 @@ stack:
stk_trail:
| RET LPAREN RPAREN
{S.ret ~loc:(position $symbolstartpos $endpos) ()}
| CALL LPAREN x = value RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (call x stk)}
| CALL LPAREN xs = separated_list(COMMA, value) RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (Call (xs, stk))}
| YES LPAREN RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (yes stk)}
| NO LPAREN RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (no stk)}
| PROJ LPAREN i = NUM SLASH n = NUM RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (Proj (i,n, stk))}
| SHIFT MINUS LPAREN RPAREN DOT stk = stk_trail
{S.destr ~loc:(position $symbolstartpos $endpos) (shift_neg stk)}
| cons = destrvar LPAREN args = separated_list(COMMA, value) RPAREN DOT stk = stk_trail
......@@ -201,9 +206,10 @@ cons:
| cons = consvar LPAREN args = separated_list(COMMA, typed_var) RPAREN
{ poscons cons args }
| UNIT {unit}
| PAIR LPAREN a = typed_var COMMA b = typed_var RPAREN { pair a b }
| TUPPLE LPAREN vs = separated_list(COMMA, typed_var) RPAREN { Tupple vs }
| LEFT LPAREN a = typed_var RPAREN {left a}
| RIGHT LPAREN b = typed_var RPAREN {right b}
| INJ LPAREN i = NUM SLASH n = NUM COMMA a = typed_var RPAREN { Inj (i,n,a) }
| SHIFT PLUS a = typed_var RPAREN {shift_pos a}
......
......@@ -156,10 +156,10 @@ let rec intern_type env = function
| Bottom -> aux bottom
| ShiftPos a -> aux (shift_pos_t (intern_type env a))
| ShiftNeg a -> aux (shift_neg_t (intern_type env a))
| Prod (a,b) -> aux (prod (intern_type env a) (intern_type env b))
| Sum (a,b) -> aux (sum (intern_type env a) (intern_type env b))
| Fun (a,b) -> aux (func (intern_type env a) (intern_type env b))
| Choice (a,b) -> aux (choice (intern_type env a) (intern_type env b))
| Prod ts -> aux (Prod (List.map (intern_type env) ts))
| Sum ts -> aux (Sum (List.map (intern_type env) ts))
| Fun (a,b) -> aux (Fun (List.map (intern_type env) a, intern_type env b))
| Choice ts -> aux (Choice (List.map (intern_type env) ts))
| Cons (cons, args) ->
let name =
try StringEnv.find cons env.tycons_vars
......@@ -174,3 +174,4 @@ let rec intern_type env = function
| TNeg t -> intern_type env t
| TBox {node; _} -> intern_type env node
......@@ -54,65 +54,3 @@ let internalize prog =
let prog, env = internalize_prelude prog in
let prog, env = intern_prog env prog in
prog, env
let polarity_inference ?debug env prog =
let env =
List.fold_left (Intern_pol_inference.unify_def ?debug) env prog in
let rec aux env acc = function
| [] -> env.prelude, List.rev acc
| h::t ->
let def,env = Intern_export.export_ast env h in
aux env (def::acc) t in
aux env [] prog
let intern_error_wrapper f =
let wrap ?loc str = begin
let loc = match loc with
| None -> ""
| Some loc ->"(" ^ Util.string_of_position loc ^ ")" in
print_endline ("FATAL" ^ loc ^ ": " ^ str);
exit 1 end in
try f () with
| Intern_common.Ambiguous_polarity loc ->
wrap ("ambiguous polarity at " ^ (Util.string_of_position loc))
| Intern_common.Double_definition name ->
wrap ("the name " ^ name ^ " is defined twice")
| Intern_common.Bad_sort {loc; actual; expected} ->
wrap ~loc ("conflicting sorts, expected "
^ Types.string_of_sort expected
^ ", got "
^ Types.string_of_sort actual)
| Intern_common.Undefined_type {name; loc} ->
wrap ~loc ("The type " ^ name ^ "is undefined")
| Intern_common.Bad_type_cons_arity {cons; loc} ->
wrap ~loc ("This type application has the wrong arity for" ^ cons)
| Intern_common.Bad_constructor_name {loc} ->
wrap ~loc ("This constructor/destructor name is reserved")
| Intern_common.Higher_order_type_argument {loc; name} ->
wrap ~loc ("Unsupported: the type argument "
^ name
^ " has a higher-order sort")
| Intern_common.Undefined_var (name, loc) ->
wrap ~loc ("Undefined variable " ^ name)
| Intern_common.Undefined_constructor (name, loc) ->
wrap ~loc ("Undefined constructor " ^ name)
| Intern_common.Undefined_destructor (name, loc) ->
wrap ~loc ("Undefined destructor " ^ name)
| Intern_common.Polarity_mismatch (loc1, loc2) ->
wrap ("The polarities of expressions at "
^ string_of_position loc1
^ " and "
^ string_of_position loc2
^ "disagree")
open Util
open Vars
open Types
open Intern_common
open Intern_prettyPrinter
open Format
open Ast
open InternAst
let get env polvar =
PolVarEnv.find polvar env.unifier
let get_opt env polvar =
PolVarEnv.find_opt polvar env.unifier
let get_loc env polvar =
try match get env polvar with
| Loc (loc, _) -> loc
| _ -> dummy_pos
with
| Not_found -> dummy_pos
let set upol env polvar =
let upol =
try match get env polvar with
| Loc (loc, _) -> Loc (loc, upol)
| _ -> upol
with Not_found -> upol in
{env with unifier = PolVarEnv.add polvar upol env.unifier}
let unify_upol env upol1 upol2 =
let acc = ref [] in
let add polvar = acc := polvar :: !acc in
let finalize p = List.fold_left (set p) env !acc in
let rec collect loc = function
| Litt p -> loc, Some p
| Loc (loc, v) -> collect loc v
| Redirect v -> begin
add v;
match get_opt env v with
| None -> loc, None
| Some upol -> collect loc upol
end in
let loc1, pol1 = collect dummy_pos upol1 in
let loc2, pol2 = collect dummy_pos upol2 in
match pol1, pol2 with
| Some p, None
| None, Some p -> finalize (Litt p)
| None, None -> finalize (Redirect (PolVar.fresh ()))
| Some p1, Some p2 when p1 = p2 -> finalize (Litt p1)
| _ -> fail_polarity_mismatch loc1 loc2
let unify_def ?debug env item =
let prelude = env.prelude in
let env = ref env in
let rec pp_upol fmt = function
| Litt p -> pp_pol fmt p
| Loc (loc,u) -> fprintf fmt "loc(%s)%a" (string_of_position loc) pp_upol u
| Redirect v -> pp_print_string fmt (PolVar.to_string v) in
let rec unify upol1 upol2 =
env := unify_upol !env upol1 upol2
and unify_typ upol1 typ =
let upol2 = match typ with
| TBox _ | TPos _ -> Litt positive
| TNeg _ -> Litt negative
| TCons {node;_} ->
begin match node with
| Unit | Zero | ShiftPos _ | Prod _ | Sum _ -> Litt positive
| Top | Bottom | ShiftNeg _ | Fun _ | Choice _ -> Litt negative
| Cons (cons, _) ->
let consdef = TyConsEnv.find cons prelude.tycons in
match consdef.ret_sort with
| Base p -> Litt p
| _ -> raise (Failure "FATAL type constructors has non-base type")
end
| TVar {node=var; _}| TInternal var ->
try TyVarEnv.find var !env.tyvarpols
with
| Not_found ->
let pol = Redirect (PolVar.fresh ()) in
env := {!env with tyvarpols = TyVarEnv.add var pol !env.tyvarpols};
pol
in unify upol1 upol2
and unify_bind upol (var, typ) loc =
let polvar =
try VarEnv.find var !env.varpols
with Not_found -> fail_undefined_var (Var.to_string var) loc in
unify upol (Loc (loc, Redirect polvar));
unify_typ upol typ
and unify_val upol valu loc =
match valu with
| Var v ->
let polvar =
try VarEnv.find v !env.varpols
with Not_found -> fail_undefined_var (Var.to_string v) loc in
unify upol (Loc (loc, Redirect polvar))
| Bindcc {bind = (pol1, typ); pol = pol2; cmd} ->
unify_typ upol typ;
unify upol (Loc (loc, pol1));
unify upol (Loc (loc, pol2));
unify_cmd upol cmd
| Box {bind=(pol,typ); cmd; _} ->
unify upol (Loc (loc, Litt positive));
unify_typ pol typ;
unify pol (Litt positive);
unify_cmd pol cmd
| Cons cons ->
unify upol (Loc (loc, Litt positive));
unify_cons cons
| Destr copatts ->
unify upol (Loc (loc, Litt negative));
let go (copatt, cmd) =
unify_copatt copatt loc;
unify_cmd upol cmd in
List.iter go copatts
and unify_stk upol final_upol loc stk =
match stk with
| Ret -> unify (Loc (loc, upol)) final_upol
| CoBind {bind=(var,typ); pol; cmd} ->
let polvar = PolVar.fresh () in
env := {!env with varpols = VarEnv.add var polvar !env.varpols};
unify upol (Loc (loc, pol));
unify_typ upol typ;
unify upol (Redirect polvar);
unify_cmd final_upol cmd
| CoBox {stk;_} ->
unify upol (Litt positive);
unify_meta_stk (Litt positive) final_upol stk
| CoDestr destr ->
unify upol (Loc (loc, Litt negative));
unify_destr final_upol destr
| CoCons patts ->
unify upol (Loc (loc, Litt positive));
let go (patt, cmd) =
unify_patt patt loc;
unify_cmd final_upol cmd in
List.iter go patts
and unify_cons cons =
let args, upol = match cons with
| Unit -> [], Litt positive
| Left x | Right x -> [x], Litt positive
| ShiftPos x -> [x], Litt negative
| Pair (a,b) -> [a;b], Litt positive
| PosCons (_, args) -> args, Litt positive in
List.iter (unify_meta_val upol) args
and unify_destr final_upol destr =
let args, cont, cont_pol = match destr with
| Call (x,a) -> [x], a, Litt negative
| Yes a | No a -> [], a, Litt negative
| ShiftNeg a -> [], a, Litt positive
| NegCons (_, args, cont) -> args, cont, Litt positive in
List.iter (unify_meta_val (Litt positive)) args;
unify_meta_stk cont_pol final_upol cont
and unify_patt patt loc = match patt with