Change printing to show idents instead of uids

This commit is contained in:
Nicolas Chataing 2020-08-04 10:54:17 +02:00
parent e2879cc68d
commit a576682fac
7 changed files with 27 additions and 19 deletions

View File

@ -110,7 +110,8 @@ let driver (source_file : string) (debug : bool) (wrap_weaved_output : bool)
let exec_ctxt = Interpreter.execute_scope ctxt Interpreter.empty_exec_ctxt prgm scope in
Uid.UidMap.iter
(fun uid value ->
Printf.printf "Var %d:\t%s\n" uid (Lambda.print_term ((value, Pos.no_pos), None)))
Printf.printf "Var %s:\t%s\n" (Uid.get_ident uid)
(Lambda.print_term ((value, Pos.no_pos), None)))
exec_ctxt;
Printf.printf "\n")
prgm;

View File

@ -50,17 +50,17 @@ let unknown_identifier (ident : string) (loc : Pos.t) =
let context_error (msg : string) = raise (ContextError (Printf.sprintf "%s" msg))
let default_conflict (ident : int) (pos : Pos.t list) =
let default_conflict (ident : string) (pos : Pos.t list) =
if List.length pos = 0 then
raise
(DefaultConflict
(Printf.sprintf "Error conflict for variable %d, no justification is true." ident))
(Printf.sprintf "Error conflict for variable %s, no justification is true." ident))
else
let pos_str = pos |> List.map Pos.to_string |> String.concat "\n\t" in
raise
(DefaultConflict
(Printf.sprintf
"Conflict error for variable %d : following justifications are true without \
"Conflict error for variable %s : following justifications are true without \
precedences :\n\
\t%s"
ident pos_str))

View File

@ -109,7 +109,7 @@ let process_subscope_decl (scope : uid) (ctxt : context) (decl : Ast.scope_decl_
match IdentMap.find_opt name scope_ctxt.var_id_to_uid with
| Some _ -> assert false (* Variable is already used in this scope *)
| None ->
let sub_scope_uid = Uid.fresh () in
let sub_scope_uid = Uid.fresh name in
let scope_ctxt =
{
var_id_to_uid = IdentMap.add name sub_scope_uid scope_ctxt.var_id_to_uid;
@ -129,8 +129,8 @@ let process_subscope_decl (scope : uid) (ctxt : context) (decl : Ast.scope_decl_
(* Now duplicate all variables from the subscope *)
IdentMap.fold
(fun sub_var sub_uid ctxt ->
let fresh_uid = Uid.fresh () in
let fresh_varname = subscope_ident name sub_var in
let fresh_uid = Uid.fresh fresh_varname in
let scope_ctxt = UidMap.find scope ctxt.scopes in
let scope_ctxt =
{
@ -173,7 +173,7 @@ let process_data_decl (scope : uid) (ctxt : context) (decl : Ast.scope_decl_cont
| Some _ -> (* Variable is already used in this scope *) assert false
| None ->
(* We now can get a fresh uid for the data *)
let uid = Uid.fresh () in
let uid = Uid.fresh name in
let scope_ctxt =
{
var_id_to_uid = IdentMap.add name uid scope_ctxt.var_id_to_uid;
@ -200,7 +200,7 @@ let process_scope_decl (ctxt : context) (decl : Ast.scope_decl) : context =
match IdentMap.find_opt name ctxt.scope_id_to_uid with
| Some _ -> assert false
| None ->
let scope_uid = Uid.fresh () in
let scope_uid = Uid.fresh name in
let ctxt =
{
scope_id_to_uid = IdentMap.add name scope_uid ctxt.scope_id_to_uid;

View File

@ -81,7 +81,7 @@ let print_op (op : op) : string =
let rec print_term (((t, _), _) : term) : string =
match t with
| EVar uid -> Printf.sprintf "var(%n)" uid
| EVar uid -> Printf.sprintf "%s(%d)" (Uid.get_ident uid) uid
| EFun (binders, body) ->
let sbody = print_term body in
Printf.sprintf "fun %s -> %s"

View File

@ -14,15 +14,22 @@
type t = int
let counter = ref 0
let fresh () : t =
incr counter;
!counter
module UidSet = Set.Make (Int)
module UidMap = Map.Make (Int)
type ident = string
let ident_tbl = ref UidMap.empty
let counter = ref 0
let fresh (id : ident) : t =
incr counter;
ident_tbl := UidMap.add !counter id !ident_tbl;
!counter
let get_ident (uid : t) = UidMap.find uid !ident_tbl
let map_add_list (key : t) (item : 'a) (map : 'a list UidMap.t) =
match UidMap.find_opt key map with
| Some l -> UidMap.add key (item :: l) map

View File

@ -19,7 +19,7 @@ let subscope_ident (y : string) (x : string) : string = y ^ "::" ^ x
(** The optional argument subdef allows to choose between differents uids in case the expression is
a redefinition of a subvariable *)
let rec expr_to_lambda ?(subdef : uid option) (scope : Context.uid) (ctxt : Context.context)
let rec expr_to_lambda ?(subdef : Uid.t option) (scope : Uid.t) (ctxt : Context.context)
((expr, pos) : Ast.expression Pos.marked) : Lambda.term =
let rec_helper = expr_to_lambda ?subdef scope ctxt in
match expr with
@ -194,7 +194,7 @@ let process_rule (precond : Lambda.term option) (scope : uid) (ctxt : Context.co
in
UidMap.add scope scope_prgm prgm
let process_def (precond : Lambda.term option) (scope : uid) (ctxt : Context.context)
let process_def (precond : Lambda.term option) (scope : Uid.t) (ctxt : Context.context)
(prgm : Scope.program) (def : Ast.definition) : Scope.program =
(* For now we rule out functions *)
let () = match def.definition_parameter with Some _ -> assert false | None -> () in
@ -254,7 +254,7 @@ let process_def (precond : Lambda.term option) (scope : uid) (ctxt : Context.con
in
UidMap.add scope scope_prgm prgm
let process_scope_use_item (cond : Lambda.term option) (scope : uid) (ctxt : Context.context)
let process_scope_use_item (cond : Lambda.term option) (scope : Uid.t) (ctxt : Context.context)
(prgm : Scope.program) (item : Ast.scope_use_item Pos.marked) : Scope.program =
match Pos.unmark item with
| Ast.Rule rule -> process_rule cond scope ctxt prgm rule

View File

@ -213,7 +213,7 @@ let rec execute_scope (ctxt : Context.context) (exec_context : exec_context) (pr
let def = UidMap.find uid scope_prgm.scope_defs in
match eval_default_term exec_context def with
| Ok value -> UidMap.add uid (Lambda.untype value) exec_context
| Error pos -> Errors.default_conflict uid pos )
| Error pos -> Errors.default_conflict (Uid.get_ident uid) pos )
| IdSubScope sub_scope_ref ->
(* Merge the new definitions *)
let sub_scope_prgm = UidMap.find sub_scope_ref prgm in