Commit 99d1849f authored by François Bobot's avatar François Bobot

core : use supermap to make some rewritting

parent ac0c4f10
......@@ -234,11 +234,10 @@ let check_termination ldl =
in
let syms = List.fold_left add Mls.empty ldl in
Mls.iter (build_call_graph cgr syms) syms;
let check ls _ acc =
let check ls _ =
let cl = build_call_list cgr ls in
Mls.add ls (check_call_list ls cl) acc
in
Mls.fold check syms Mls.empty
check_call_list ls cl in
Mls.mapi check syms
(** Inductive predicate declaration *)
......
......@@ -67,28 +67,32 @@ module Compile (X : Action) = struct
in
(* dispatch every case to a primitive constructor/wild case *)
let cases,wilds =
let add_case fs pl a cases =
let rl = Mls.find_default fs [] cases in
Mls.add fs ((pl,a)::rl) cases
in
let add_wild pl a fs ql cases =
let add pl q = pat_wild q.pat_ty :: pl in
add_case fs (List.fold_left add pl ql) a cases
in
let change_case fs pl a cases =
Mls.change fs (function
| None -> Some [pl,a]
| Some rl -> Some ((pl,a)::rl)) cases in
let union_cases pl a types cases =
let make_wild pl a ql =
let add pl q = pat_wild q.pat_ty :: pl in
[List.fold_left add pl ql,a]
in
let types = Mls.map (make_wild pl a) types in
Mls.union (fun _ pla rl -> Some (List.append pla rl))
types cases in
let rec dispatch (pl,a) (cases,wilds) =
let p = List.hd pl in let pl = List.tl pl in
match p.pat_node with
| Papp (fs,pl') ->
add_case fs (List.rev_append pl' pl) a cases, wilds
change_case fs (List.rev_append pl' pl) a cases, wilds
| Por (p,q) ->
dispatch (p::pl, a) (dispatch (q::pl, a) (cases,wilds))
| Pas (p,x) ->
dispatch (p::pl, mk_let x t a) (cases,wilds)
| Pvar x ->
let a = mk_let x t a in
Mls.fold (add_wild pl a) types cases, (pl,a)::wilds
union_cases pl a types cases, (pl,a)::wilds
| Pwild ->
Mls.fold (add_wild pl a) types cases, (pl,a)::wilds
union_cases pl a types cases, (pl,a)::wilds
in
List.fold_right dispatch rl (Mls.empty,[])
in
......@@ -125,7 +129,7 @@ module Compile (X : Action) = struct
if Mls.mem cs types then comp_cases cs al else comp_wilds ()
| _ ->
let base =
if Sls.for_all (fun cs -> Mls.mem cs types) css
if Mls.submap (fun _ () _ -> true) css types
then [] else [mk_branch (pat_wild ty) (comp_wilds ())]
in
let add cs ql acc =
......
......@@ -142,14 +142,16 @@ let remove_prop pr =
let get_syntax_map task =
let add_ts td m = match td.td_node with
| Meta (_,[MAts ts; MAstr s]) ->
if Mid.mem ts.ts_name m then raise (KnownTypeSyntax ts);
Mid.add ts.ts_name s m
Mid.change ts.ts_name (function
| None -> Some s
| Some _ -> raise (KnownTypeSyntax ts)) m
| _ -> assert false
in
let add_ls td m = match td.td_node with
| Meta (_,[MAls ls; MAstr s]) ->
if Mid.mem ls.ls_name m then raise (KnownLogicSyntax ls);
Mid.add ls.ls_name s m
Mid.change ls.ls_name (function
| None -> Some s
| Some _ -> raise (KnownLogicSyntax ls)) m
| _ -> assert false
in
let m = Mid.empty in
......@@ -176,8 +178,7 @@ let get_remove_set task =
let s = Stdecl.fold add_pr (find_meta task meta_remove_prop).tds_set s in
s
let query_syntax sm id =
try Some (Mid.find id sm) with Not_found -> None
let query_syntax sm id = Mid.find_option id sm
(** {2 exceptions to use in transformations and printers} *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment