Merge pull request MLanguage#147 from MLanguage/custom-chains

Support for custom M chains

Author: Raphaël Monat

mpp_specs/dgfip_base.mpp

@@ -108,7 +108,7 @@ sauve_base_HR():
 
 ENCH_TL():
   X = X
-#  outputs <- call_m(ENCH_TL)
+  outputs <- call_m(ENCH_TL)
 
 verif_calcul_primitive_isf():
   call_m_verif(isf,calculee)

src/mlang/m_frontend/format_mast.ml

@@ -42,6 +42,8 @@ let format_chaining fmt (c : chaining) = Format.fprintf fmt "%s" c
 let format_chain_tag fmt (t : chain_tag) =
   Format.pp_print_string fmt
     (match t with
+    | Custom name -> "\"" ^ name ^ "\""
+    | PrimCorr -> ""
     | Primitif -> "primitif"
     | Corrective -> "corrective"
     | Isf -> "isf"

src/mlang/m_frontend/mast.ml

@@ -35,6 +35,8 @@ type chaining = string
 (** "enchaineur" in the M source code, utility unknown *)
 
 type chain_tag =
+  | Custom of string (* Custom chain, not an actual rule tag *)
+  | PrimCorr (* empty tag *)
   | Primitif
   | Corrective
   | Isf
@@ -147,7 +149,7 @@ let chain_tag_of_string : string -> chain_tag = function
   | "base_stratemajo" -> Base_stratemajo
   | "non_auto_cc" -> Non_auto_cc
   | "horizontale" -> Horizontale
-  | _ -> raise Not_found
+  | s -> Custom s
 
 let number_and_tags_of_name (name : string Pos.marked list) :
     int Pos.marked * chain_tag Pos.marked list =
@@ -174,8 +176,10 @@ let number_and_tags_of_name (name : string Pos.marked list) :
   in
   let number, tags = aux [] name in
   if List.length tags = 0 then
-    (number, [ (Primitif, Pos.no_pos); (Corrective, Pos.no_pos) ])
-    (* No tags means both in primitive and corrective *)
+    ( number,
+      [
+        (PrimCorr, Pos.no_pos); (Primitif, Pos.no_pos); (Corrective, Pos.no_pos);
+      ] ) (* No tags means both in primitive and corrective *)
   else (number, tags)
 
 type variable_name = string

src/mlang/m_frontend/mast_to_mir.ml

@@ -1286,7 +1286,12 @@ let get_rules_and_var_data (idmap : Mir.idmap)
                             data_to_add)
                     ([], var_data, 0) r.Mast.rule_formulaes
                 in
-                let rule = (List.rev rule_vars, r.rule_number, r.rule_tags) in
+                let rule_tags =
+                  match r.rule_chaining with
+                  | None -> r.rule_tags
+                  | Some (chain, pos) -> (Mast.Custom chain, pos) :: r.rule_tags
+                in
+                let rule = (List.rev rule_vars, r.rule_number, rule_tags) in
                 ( Mir.RuleMap.add (Pos.unmark r.rule_number) rule rule_data,
                   var_data )
           | Mast.VariableDecl (Mast.ConstVar _) ->
@@ -1464,6 +1469,10 @@ let get_conds (error_decls : Mir.Error.t list)
                               (Mast.Primitif, Pos.no_pos);
                               (Mast.Corrective, Pos.no_pos);
                             ]
+                        | [ (Mast.Custom _, _) ] as l ->
+                            (Mast.Primitif, Pos.no_pos)
+                            :: (Mast.Corrective, Pos.no_pos)
+                            :: l
                         | l -> l);
                     }
                     conds)

src/mlang/m_ir/mir.ml

@@ -406,7 +406,10 @@ end)
 module TagMap = Map.Make (struct
   type t = Mast.chain_tag
 
-  let compare = compare
+  let compare t1 t2 =
+    match (t1, t2) with
+    | Mast.Custom s1, Mast.Custom s2 -> String.compare s1 s2
+    | _ -> Stdlib.compare t1 t2
 end)
 
 (**{1 Verification conditions}*)

src/mlang/m_ir/mir_dependency_graph.ml

@@ -184,9 +184,46 @@ let check_for_cycle (g : RG.t) (p : Mir.program) (print_debug : bool) : bool =
   end
   else false
 
-module RuleExecutionOrder = Graph.Topological.Make (RG)
-
 type rule_execution_order = Mir.rule_id list
 
+module Traversal = Graph.Traverse.Dfs (RG)
+
+let pull_rules_dependencies (g : RG.t) (rules : Mir.rule_id list) :
+    RG.t * rule_execution_order =
+  let order =
+    List.fold_left
+      (fun exec_order rule_id ->
+        let new_deps =
+          Traversal.fold_component
+            (fun dep new_deps ->
+              if List.mem dep exec_order then
+                (* We already added this dependency from another rule, and thus
+                   all its own dependencies *)
+                new_deps
+              else dep :: new_deps)
+            exec_order g rule_id
+        in
+        (* Here's a subtlety, we don't now in which order the rules given are,
+           only that their should not be any cycles. So we can have three cases:
+           The current rule we pull dependencies of is unrelated to previous
+           ones, this is trivialy correct. Or, the current rule is already a
+           dependency of previous ones, then nothing will be added, as seen
+           above. Or finally, the current rule has dependencies in common with
+           previous rules, in which case we know them to be already added, so to
+           be topologically ordered we have to put the new dependencies at the
+           end, it is safe since there is no cycles. *)
+        exec_order @ new_deps)
+      [] rules
+  in
+  let subgraph =
+    RG.fold_vertex
+      (fun rule_id subg ->
+        if List.mem rule_id order then subg else RG.remove_vertex subg rule_id)
+      g g
+  in
+  (subgraph, order)
+
+module RuleExecutionOrder = Graph.Topological.Make (RG)
+
 let get_rules_execution_order (dep_graph : RG.t) : rule_execution_order =
   RuleExecutionOrder.fold (fun var exec_order -> var :: exec_order) dep_graph []

src/mlang/m_ir/mir_dependency_graph.mli

@@ -36,4 +36,7 @@ val check_for_cycle : RG.t -> Mir.program -> bool -> bool
 
 type rule_execution_order = Mir.rule_id list
 
+val pull_rules_dependencies :
+  RG.t -> Mir.rule_id list -> RG.t * rule_execution_order
+
 val get_rules_execution_order : RG.t -> rule_execution_order

src/mlang/m_ir/mir_interface.ml

@@ -60,9 +60,9 @@ type full_program = {
 
 let to_full_program (program : program) (chains : Mast.chain_tag list) :
     full_program =
-  let chains_orders =
+  let chains_orders, _ =
     List.fold_left
-      (fun chains tag ->
+      (fun (chains, seen_customs) tag ->
         let vars_to_rules, chain_rules =
           Mir.RuleMap.fold
             (fun rule_id rule (vars, rules) ->
@@ -84,7 +84,73 @@ let to_full_program (program : program) (chains : Mast.chain_tag list) :
         let execution_order =
           Mir_dependency_graph.get_rules_execution_order dep_graph
         in
-        Mir.TagMap.add tag { dep_graph; execution_order } chains)
-      Mir.TagMap.empty chains
+        let customs, _ =
+          RuleMap.fold
+            (fun rule_id rule (customs, in_primcorr) ->
+              List.fold_left
+                (fun (customs, in_primcorr) tag ->
+                  match tag with
+                  | Mast.Custom _ -> (
+                      let ipc =
+                        Mast.are_tags_part_of_chain rule.rule_tags Mast.PrimCorr
+                      in
+                      if in_primcorr && not ipc then
+                        Errors.raise_error
+                          "Custom chain must be attributed to rules with all \
+                           the exact same tagging."
+                      else
+                        match TagMap.find_opt tag customs with
+                        | Some rs ->
+                            ( TagMap.add tag (rule_id :: rs) customs,
+                              ipc || in_primcorr )
+                        | None ->
+                            ( TagMap.add tag [ rule_id ] customs,
+                              ipc || in_primcorr ))
+                  | _ -> (customs, in_primcorr))
+                (customs, in_primcorr) rule.rule_tags)
+            chain_rules (TagMap.empty, false)
+        in
+        let customs =
+          TagMap.map
+            (fun rules ->
+              Mir_dependency_graph.pull_rules_dependencies dep_graph rules)
+            customs
+        in
+        let seen_customs =
+          TagMap.merge
+            (fun custom_tag seen curr ->
+              match (seen, curr) with
+              | None, None -> None
+              | Some _, None -> seen
+              | None, Some _ -> Some tag
+              | Some s, Some _ -> (
+                  match (s, tag) with
+                  | Mast.Primitif, Mast.Corrective
+                  | Mast.Corrective, Mast.Primitif ->
+                      (* ignore this case *) seen
+                  | _ ->
+                      let custom_tag =
+                        match custom_tag with
+                        | Mast.Custom s -> s
+                        | _ -> assert false
+                      in
+                      Errors.raise_error
+                        (Format.asprintf
+                           "Rules with custom chain %s found with incompatible \
+                            tags %a and %a."
+                           custom_tag Format_mast.format_chain_tag s
+                           Format_mast.format_chain_tag tag)))
+            seen_customs customs
+        in
+        let chains =
+          TagMap.fold
+            (fun tag (dep_graph, execution_order) chains ->
+              TagMap.add tag { dep_graph; execution_order } chains)
+            customs
+            (Mir.TagMap.add tag { dep_graph; execution_order } chains)
+        in
+        (chains, seen_customs))
+      (Mir.TagMap.empty, Mir.TagMap.empty)
+      chains
   in
   { program; chains_orders }