Rewrite merge_var_redefs function

This commit is contained in:
Nicolas Chataing 2020-08-09 23:50:00 +02:00
parent 26e68e6f7a
commit 6acf49b6fe
2 changed files with 36 additions and 2 deletions

View File

@ -61,6 +61,10 @@ let get_typ ((_, typ) : term) : typ = typ
let map_untype (f : untyped_term -> untyped_term) (((term, pos), typ) : term) : term =
((f term, pos), typ)
let map_untype2 (f : untyped_term -> untyped_term -> untyped_term) (((t1, pos), typ) : term)
(((t2, _), _) : term) : term =
((f t1 t2, pos), typ)
let empty_default_term : default_term = { defaults = IntMap.empty; ordering = []; nb_defaults = 0 }
let add_default (just : term) (cons : term) (term : default_term) =

View File

@ -214,8 +214,38 @@ let build_scope_schedule (ctxt : Context.context) (scope : Scope.scope) : G.t =
scope.scope_sub_defs;
g
let merge_var_redefs (_subscope : Scope.scope) (_redefs : Scope.definition UidMap.t) : Scope.scope =
assert false
let merge_var_redefs (subscope : Scope.scope) (redefs : Scope.definition UidMap.t) : Scope.scope =
let merge_defaults : Lambda.term -> Lambda.term -> Lambda.term =
Lambda.map_untype2 (fun old_t new_t ->
match (old_t, new_t) with
| EDefault old_def, EDefault new_def ->
EDefault (Lambda.merge_default_terms old_def new_def)
| EFun ([ bind ], old_t), EFun (_, new_t) ->
let body =
Lambda.map_untype2
(fun old_t new_t ->
match (old_t, new_t) with
| EDefault old_def, EDefault new_def ->
EDefault (Lambda.merge_default_terms old_def new_def)
| _ -> assert false)
old_t new_t
in
EFun ([ bind ], body)
| _ -> assert false)
in
{
subscope with
scope_defs =
UidMap.fold
(fun uid new_def sub_defs ->
match UidMap.find_opt uid sub_defs with
| None -> UidMap.add uid new_def sub_defs
| Some old_def ->
let def = merge_defaults old_def new_def in
UidMap.add uid def sub_defs)
redefs subscope.scope_defs;
}
(*{ subscope with scope_defs = UidMap.fold (fun uid new_def sub_defs -> match UidMap.find_opt uid
sub_defs with | None -> UidMap.add uid new_def sub_defs | Some old_def -> let def =