Commit 7a7b8f13 authored by Hector Suzanne's avatar Hector Suzanne
Browse files

Sauvegarde

parent 3a8e7723
......@@ -2,6 +2,7 @@ open Autobill
open Cst_intf
open Intern_intf
open Sort_intf
open Reduction_intf
let version =
match Build_info.V1.version () with
......@@ -17,13 +18,15 @@ type subcommand =
| Version
| Parse
| Intern
| PolInfer
| SortInfer
| Simplify
let parse_command = function
| "version" -> Version
| "parse" -> Parse
| "intern" -> Intern
| "polinfer" -> PolInfer
| "polinfer" -> SortInfer
| "simplify" -> Simplify
| _ -> print_endline usage_spiel; exit 1
let parse_cli_invocation () =
......@@ -54,8 +57,11 @@ let () =
let prog, env = intern_error_wrapper (fun () -> internalize cst) in
stop_if_cmd Intern (fun () -> print_endline (string_of_intern_ast (env.prelude, prog)));
let prelude, prog = intern_error_wrapper (fun () -> polarity_inference env prog) in
stop_if_cmd PolInfer (fun () -> print_endline (string_of_full_ast (prelude, prog)));
let prog = intern_error_wrapper (fun () -> polarity_inference env prog) in
stop_if_cmd SortInfer (fun () -> print_endline (string_of_full_ast prog));
let prog = interpret_prog prog in
stop_if_cmd Simplify (fun () -> print_endline (string_of_full_ast prog));
print_endline "Not yet implemented.";
exit 1
......@@ -39,7 +39,7 @@ exception Undefined_constructor of string * position
exception Undefined_destructor of string * position
exception Polarity_mismatch of position * position
exception Polarity_mismatch of string * string * position * position
let fail_double_def mess loc =
raise (Double_definition
......@@ -47,6 +47,16 @@ let fail_double_def mess loc =
(Util.string_of_position loc)
mess))
type upol =
| Loc of position * upol
| Litt of Types.polarity
| Redirect of PolVar.t
let rec string_of_upol = function
| Loc (pos, upol) -> Printf.sprintf "%s@\"%s\"" (string_of_upol upol) (string_of_position pos)
| Litt pol -> string_of_polarity pol
| Redirect var -> PolVar.to_string var
let fail_bad_sort loc expected actual =
raise (Bad_sort {loc; actual; expected})
......@@ -70,14 +80,10 @@ let fail_undefined_cons cons loc = raise (Undefined_constructor (cons, loc))
let fail_undefined_destr destr loc = raise (Undefined_destructor (destr, loc))
let fail_polarity_mismatch pos1 pos2 = raise (Polarity_mismatch (pos1, pos2))
let fail_polarity_mismatch upol1 upol2 pos1 pos2 =
raise (Polarity_mismatch (string_of_upol upol1, string_of_upol upol2, pos1, pos2))
type upol =
| Loc of position * upol
| Litt of Types.polarity
| Redirect of PolVar.t
module InternAstParams = struct
include FullAstParams
type polarity = upol
......
......@@ -44,10 +44,11 @@ let string_of_intern_ast prog =
Format.flush_str_formatter ()
let intern_prog env prog =
let go (prog, env) item =
let item, env = intern_definition env item in
(item :: prog, env) in
let prog, env = List.fold_left go ([],env) prog in
let go (prog, env, decl) item =
let decl, item, env = intern_definition env decl item in
(item :: prog, env, decl) in
let decl = StringEnv.empty in
let prog, env,_ = List.fold_left go ([],env,decl) prog in
List.rev prog, env
let internalize prog =
......
......@@ -54,7 +54,7 @@ let visit_destr vars env loc kx ka = function
let vars, cont = ka vars cont in
vars, NegCons (destr, List.rev args_rev, cont)
let intern_definition env def =
let intern_definition env declared_vars def =
let env = ref env in
......@@ -65,14 +65,13 @@ let intern_definition env def =
let rec intern_val vars = function
| Cst.Var {node; loc} ->
begin
try
let var = StringEnv.find node vars in
let val_typ = TInternal (TyVar.fresh ()) in
MetaVal {node = Var var; loc; val_typ}
with
| Not_found -> fail_undefined_var node loc
end
let var =
try StringEnv.find node vars
with Not_found ->
try StringEnv.find node declared_vars
with Not_found -> fail_undefined_var node loc in
let val_typ = TInternal (TyVar.fresh ()) in
MetaVal {node = Var var; loc; val_typ}
| Cst.CoTop {loc} -> MetaVal {node = CoTop; loc; val_typ = cons top}
......@@ -102,9 +101,10 @@ let intern_definition env def =
| Cst.Destr {node; loc} ->
let val_typ = TInternal (TyVar.fresh ()) in
let final_typ = TInternal (TyVar.fresh ()) in
let go_one (destr, cmd) =
let vars, destr = intern_copatt vars loc destr in
let cmd = intern_cmd vars val_typ cmd in
let cmd = intern_cmd vars final_typ cmd in
(destr, cmd) in
MetaVal {loc; val_typ; node = Destr (List.map go_one node)}
......@@ -201,7 +201,7 @@ let intern_definition env def =
let vars = StringEnv.empty in
let def = match def with
let def' = match def with
| Cst.Term_declaration {name; typ; loc} ->
let var = Var.of_string name in
Value_declaration {
......@@ -223,7 +223,7 @@ let intern_definition env def =
let final_type = TInternal (TyVar.fresh ()) in
let var = match name with
| Some name -> Var.of_string name
| None -> Var.of_string "cmd" in
| None -> Var.of_string "anon" in
Command_execution {
name = var;
typ = intern_type_annot env typ;
......@@ -236,4 +236,9 @@ let intern_definition env def =
a prelude definition has found its way \
in the term internalizer") in
(def, !env)
let declared_vars = match def, def' with
| Cst.Term_declaration {name = old_name;_}, Value_declaration {name = new_name; _} ->
StringEnv.add old_name new_name declared_vars
| _ -> declared_vars in
(declared_vars, def', !env)
......@@ -17,10 +17,10 @@ exception Malformed_program of runtime_prog
exception Malformed_case of runtime_prog
let initial_runtime_env declared curr = {
let initial_runtime_env curr = {
cont = [];
env = VarEnv.empty;
declared;
declared = VarEnv.empty;
curr;
}
......@@ -152,79 +152,3 @@ let head_normal_form prog =
prog := reduct_head_once !prog;
loop () in
try loop () with Internal_No_root_reduction -> !prog
let rec val_nf prog v = match v with
| Var _ | CoTop -> v
| Bindcc {bind; pol; cmd} ->
let prog' = cmd_nf {prog with cont = []; curr = cmd} in
Bindcc {bind; pol; cmd = prog'.curr}
| Box {bind; kind; cmd} ->
let prog' = cmd_nf {prog with cont = []; curr = cmd} in
Box {bind; kind; cmd = prog'.curr}
| Cons cons -> Cons (cons_nf prog cons)
| Destr copatts -> Destr (List.map (copatt_nf prog) copatts)
and stack_nf prog stk = match stk with
| Ret | CoZero -> stk
| CoBind {bind; pol; cmd} ->
let prog' = cmd_nf
{prog with curr = cmd;
declared = VarEnv.add (fst bind) () prog.declared} in
CoBind {bind; pol; cmd = prog'.curr}
| CoBox {kind; stk = (MetaStack stk)} ->
CoBox {kind; stk =
MetaStack {stk with node = stack_nf prog stk.node}}
| CoDestr destr -> CoDestr (destr_nf prog destr)
| CoCons patts -> CoCons (List.map (patt_nf prog) patts)
and cons_nf prog cons = match cons with
| Unit -> Unit
| ShiftPos (MetaVal v) -> ShiftPos (MetaVal {v with node = val_nf prog v.node})
| Tupple vs ->
let aux = fun (MetaVal v) -> MetaVal {v with node = val_nf prog v.node} in
Tupple (List.map aux vs)
| Inj (i,n,MetaVal v) -> Inj (i,n,(MetaVal {v with node = val_nf prog v.node}))
| PosCons (cons, args) ->
let aux = fun (MetaVal v) -> MetaVal {v with node = val_nf prog v.node} in
PosCons (cons, List.map aux args)
and destr_nf prog destr = match destr with
| Call (vs, MetaStack s) ->
let aux = fun (MetaVal v) -> MetaVal {v with node = val_nf prog v.node} in
Call (List.map aux vs, MetaStack {s with node = stack_nf prog s.node})
| Proj (i,n, MetaStack s) -> Proj (i, n, MetaStack {s with node = stack_nf prog s.node})
| ShiftNeg (MetaStack s) -> ShiftNeg (MetaStack {s with node = stack_nf prog s.node})
| NegCons (destr, vs, (MetaStack s)) ->
let aux = fun (MetaVal v) -> MetaVal {v with node = val_nf prog v.node} in
NegCons (destr, List.map aux vs, MetaStack {s with node = stack_nf prog s.node})
and patt_nf prog (patt, cmd) =
let binds = match patt with
| Unit -> []
| ShiftPos b | Inj (_,_,b) -> [b]
| Tupple bs | PosCons (_, bs)-> bs in
let declared =
List.fold_right (fun (x,_) decl -> VarEnv.add x () decl) binds prog.declared in
let prog' = cmd_nf {prog with curr = cmd; declared} in
patt, prog'.curr
and copatt_nf prog (copatt, cmd) =
let binds = match copatt with
| Call (xs, _) | NegCons (_, xs, _) -> xs
| Proj _ | ShiftNeg _ -> []
in
let declared =
List.fold_right (fun (x,_) decl -> VarEnv.add x () decl) binds prog.declared in
let prog' = cmd_nf {prog with curr = cmd; cont = []; declared} in
copatt, prog'.curr
and cmd_nf prog =
let prog = head_normal_form prog in
let (Command cmd) = prog.curr in
let (MetaVal v) = cmd.valu in
let (MetaStack s) = cmd.stk in
let v = MetaVal {v with node = val_nf prog v.node}
and s = MetaStack {s with node = stack_nf prog s.node} in
let cmd = Command {cmd with valu = v; stk = s} in
{prog with curr = cmd}
open Ast
open Constructors
open FullAst
open HeadNormalForm
let rec val_nf prog v = match v with
| Var x ->
begin match VarEnv.find_opt x prog.env with
| Some (MetaVal v) -> val_nf prog v.node
| None -> v
end
| CoTop -> CoTop
| Bindcc {bind; pol; cmd} ->
let prog' = cmd_nf {prog with cont = []; curr = cmd} in
Bindcc {bind; pol; cmd = prog'.curr}
| Box {bind; kind; cmd} ->
let prog' = cmd_nf {prog with cont = []; curr = cmd} in
Box {bind; kind; cmd = prog'.curr}
| Cons cons -> Cons (cons_nf prog cons)
| Destr copatts -> Destr (List.map (copatt_nf prog) copatts)
and stack_nf prog stk = match stk with
| Ret -> begin match prog.cont with
| [] -> Ret
| (MetaStack h) :: t -> stack_nf {prog with cont = t} h.node
end
| CoZero -> CoZero
| CoBind {bind; pol; cmd} ->
let prog' =
cmd_nf {prog with
curr = cmd;
declared = VarEnv.add (fst bind) () prog.declared} in
CoBind {bind; pol; cmd = prog'.curr}
| CoBox {kind; stk} -> CoBox {kind; stk = metastack_nf prog stk}
| CoDestr destr -> CoDestr (destr_nf prog destr)
| CoCons patts -> CoCons (List.map (patt_nf prog) patts)
and cons_nf prog cons = match cons with
| Unit -> Unit
| ShiftPos v -> ShiftPos (metaval_nf prog v)
| Tupple vs ->
Tupple (List.map (metaval_nf prog) vs)
| Inj (i, n, v) -> Inj (i, n, metaval_nf prog v)
| PosCons (cons, args) -> PosCons (cons, List.map (metaval_nf prog) args)
and destr_nf prog destr = match destr with
| Call (vs, s) ->
Call (List.map (metaval_nf prog) vs, metastack_nf prog s)
| Proj (i, n, s) -> Proj (i, n, metastack_nf prog s)
| ShiftNeg s -> ShiftNeg (metastack_nf prog s)
| NegCons (destr, vs, s) ->
NegCons (destr, List.map (metaval_nf prog) vs, metastack_nf prog s)
and patt_nf prog (patt, cmd) =
let binds = match patt with
| Unit -> []
| ShiftPos b | Inj (_,_,b) -> [b]
| Tupple bs | PosCons (_, bs)-> bs in
let declared =
List.fold_right (fun (x,_) decl -> VarEnv.add x () decl) binds prog.declared in
let prog' = cmd_nf {prog with curr = cmd; declared} in
patt, prog'.curr
and copatt_nf prog (copatt, cmd) =
let binds = match copatt with
| Call (xs, _) | NegCons (_, xs, _) -> xs
| Proj _ | ShiftNeg _ -> []
in
let declared =
List.fold_right (fun (x,_) decl -> VarEnv.add x () decl) binds prog.declared in
let prog' = cmd_nf {prog with curr = cmd; cont = []; declared} in
copatt, prog'.curr
and metaval_nf prog (MetaVal v) =
MetaVal {v with node = val_nf prog v.node}
and metastack_nf prog (MetaStack s) =
MetaStack {s with node = stack_nf prog s.node}
and cmd_nf prog =
let prog = head_normal_form prog in
let (Command cmd) = prog.curr in
let cmd = Command
{cmd with
valu = metaval_nf prog cmd.valu;
stk = metastack_nf prog cmd.stk} in
{prog with curr = cmd}
open Ast
open FullAst
open HeadNormalForm
open NormalForm
let interpret_prog (prelude, prog_items) =
let do_once declared env prog_item = match prog_item with
| Value_declaration {name; _} ->
(VarEnv.add name () declared, env, prog_item)
| Value_definition def ->
let cmd = FullAst.Command
{pol = def.pol;
loc = def.loc;
mid_typ = def.typ;
valu = def.content;
stk = S.ret;
} in
let Command cmd = (cmd_nf {
curr = cmd;
cont = [];
declared;
env;
}).curr in
(declared,
VarEnv.add def.name cmd.valu env,
Value_definition {def with content = cmd.valu})
| Command_execution exec ->
let cmd = (cmd_nf {
curr = exec.content;
cont = [];
declared;
env;
}).curr in
(declared,
env,
Command_execution {exec with content = cmd}) in
let rec loop declared env prog_items =
match prog_items with
| [] -> (declared, env, [])
| h :: t ->
let declared, env, h = do_once declared env h in
let declared, env, t = loop declared env t in
declared, env, h::t in
let declared = VarEnv.empty in
let env = VarEnv.empty in
let _, _, prog_items = loop declared env prog_items in
(prelude, prog_items)
......@@ -53,7 +53,8 @@ let unify_upol env upol1 upol2 =
| 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
| Some _, Some _ ->
fail_polarity_mismatch upol1 upol2 loc1 loc2
let unify_def ?debug env item =
......@@ -89,8 +90,8 @@ let unify_def ?debug env item =
| Not_found ->
let pol = Redirect (PolVar.fresh ()) in
env := {!env with tyvarpols = TyVarEnv.add var pol !env.tyvarpols};
pol
in unify upol1 upol2
pol in
unify upol1 upol2
and unify_bind upol (var, typ) loc =
let polvar =
......@@ -123,8 +124,7 @@ let unify_def ?debug env item =
| Destr copatts ->
unify upol (Loc (loc, Litt negative));
let go (copatt, cmd) =
unify_copatt copatt loc;
unify_cmd upol cmd in
unify_copatt copatt cmd loc in
List.iter go copatts
and unify_stk upol final_upol loc stk =
......@@ -172,27 +172,34 @@ let unify_def ?debug env item =
and unify_patt patt loc = match patt with
| Unit -> ()
| Inj (_, _, bind) -> unify_bind (Litt positive) bind loc
| ShiftPos bind -> unify_bind (Litt positive) bind loc
| ShiftPos bind -> unify_bind (Litt negative) bind loc
| Tupple xs ->
List.iter (fun x -> unify_bind (Litt positive) x loc) xs
| PosCons (_, args) ->
List.iter (fun bind -> unify_bind (Litt positive) bind loc) args
and unify_copatt copatt loc = match copatt with
and unify_copatt copatt cmd loc = match copatt with
| Call (bindxs, binda) ->
List.iter (fun x -> unify_bind (Litt positive) x loc) bindxs;
unify_typ (Litt negative) binda
| Proj (_, _, binda)
| ShiftNeg binda -> unify_typ (Litt negative) binda
unify_typ (Litt negative) binda;
unify_cmd (Litt negative) cmd
| Proj (_, _, binda) ->
unify_typ (Litt negative) binda;
unify_cmd (Litt negative) cmd
| ShiftNeg binda ->
unify_typ (Litt positive) binda;
unify_cmd (Litt positive) cmd;
| NegCons (_, args, cont) ->
List.iter (fun bind -> unify_bind (Litt positive) bind loc) args;
unify_typ (Litt negative) cont
unify_typ (Litt negative) cont;
unify_cmd (Litt negative) cmd;
and unify_meta_val pol (MetaVal {node; val_typ; loc}) =
begin match debug with
| Some fmt ->
fprintf fmt "value with(%a) %a"
fprintf fmt "value with(%a,%a) %a"
pp_upol pol
pp_typ val_typ
pp_pre_value node;
dump_env std_formatter !env
| None -> ()
......@@ -200,13 +207,15 @@ let unify_def ?debug env item =
Format.pp_print_flush Format.std_formatter ();
unify_val pol node loc;
unify_typ pol val_typ
unify_typ pol val_typ;
and unify_meta_stk cont_pol final_pol (MetaStack {node; cont_typ; final_typ; loc}) =
begin match debug with
| Some fmt ->
fprintf fmt "stack with(%a) final(%a) %a"
fprintf fmt "stack with(%a:%a) final(%a:%a) %a"
pp_typ cont_typ
pp_upol cont_pol
pp_typ final_typ
pp_upol final_pol
pp_pre_stack node;
dump_env std_formatter !env;
......@@ -215,7 +224,8 @@ let unify_def ?debug env item =
end ;
unify_typ cont_pol cont_typ;
unify_typ final_pol final_typ;
unify_stk cont_pol final_pol loc node
unify_stk cont_pol final_pol loc node;
and unify_cmd final_pol (Command cmd) =
begin match debug with
......@@ -226,16 +236,29 @@ let unify_def ?debug env item =
dump_env std_formatter !env
| None -> ()
end ;
(* unify_typ cmd.pol cmd.loc cmd.mid_typ; *)
unify_meta_val cmd.pol cmd.valu;
unify_meta_stk cmd.pol final_pol cmd.stk
unify_meta_val cmd.pol cmd.valu;
unify_meta_stk cmd.pol final_pol cmd.stk;
unify_typ cmd.pol cmd.mid_typ;
in
begin match item with
| Value_declaration item -> unify_typ item.pol item.typ;
| Value_declaration item -> unify_typ item.pol item.typ
| Value_definition item -> unify_meta_val item.pol item.content
| Command_execution item -> unify_cmd (Litt negative) item.content
| Command_execution item ->
let upol = Redirect (PolVar.fresh ()) in
unify_cmd upol item.content;
unify_typ upol item.typ;
unify upol item.pol;
unify_typ (Litt Negative) item.cont
end;
begin match item with
| Value_declaration {name; pol; loc; _} | Value_definition {name; pol; loc; _} ->
let polvar = PolVar.fresh () in
env := {!env with varpols = VarEnv.add name polvar !env.varpols};
unify pol (Loc (loc, Redirect polvar));
| _ -> ()
end;
!env
......@@ -77,10 +77,10 @@ let export_ast env item =
and export_val loc = function
| Var v -> FullAst.Var v
| CoTop -> FullAst.CoTop
| Bindcc {bind=(pol2,_) as bind ;pol=pol1; cmd} ->
let pol1 = export_upol ~loc pol1 in
let pol2 = export_upol ~loc pol2 in
if pol1 <> pol2 then fail_polarity_mismatch loc loc;
| Bindcc {bind=(upol2,_) as bind ;pol=upol1; cmd} ->
let pol1 = export_upol ~loc upol1 in
let pol2 = export_upol ~loc upol2 in
if pol1 <> pol2 then fail_polarity_mismatch upol1 upol2 loc loc;
let bind = export_cobind bind in
FullAst.Bindcc {bind = bind; pol = pol1; cmd = export_cmd cmd}
| Box {kind; bind; cmd} ->
......
......@@ -30,7 +30,7 @@ let intern_error_wrapper f =
| Intern_common.Bad_sort {loc; actual; expected} ->
wrap ~loc ("conflicting sorts, expected "
^ Types.string_of_sort expected
^ ", got "
^ ", got "
^ Types.string_of_sort actual)
| Intern_common.Undefined_type {name; loc} ->
......@@ -56,9 +56,9 @@ let intern_error_wrapper f =
| 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
| Intern_common.Polarity_mismatch (pol1, pol2, loc1, loc2) ->
wrap ("The polarities of expressions "
^ pol1 ^ " at " ^ string_of_position loc1
^ " and "
^ string_of_position loc2
^ pol2 ^ " at " ^ string_of_position loc2
^ "disagree")
......@@ -100,8 +100,7 @@ let pp_bind_def fmt (v, t) =
pp_custom_binding ~prefix:"" ~suffix:"" fmt pp_defvar v pp_typ t
let pp_bind_def_with_cont fmt (v, t, cont) =
pp_custom_binding ~prefix:"" ~suffix:"" fmt pp_defvar v pp_typ t;
fprintf fmt "@ returns %a" pp_typ cont
pp_custom_binding ~prefix:"" ~suffix:"" fmt pp_defvar v pp_typ cont
let pp_bind_paren fmt (v, t) =
pp_custom_binding ~prefix:"(" ~suffix:")" fmt pp_var v pp_typ t
......
Test that reduction works works
$ autobill simplify <<EOF