1(****************************************************************************
2*Copyright 2008
3*  Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
4****************************************************************************)
5(****************************************************************************
6* This file is part of Teyjus.
7*
8* Teyjus is free software: you can redistribute it and/or modify
9* it under the terms of the GNU General Public License as published by
10* the Free Software Foundation, either version 3 of the License, or
11* (at your option) any later version.
12*
13* Teyjus is distributed in the hope that it will be useful,
14* but WITHOUT ANY WARRANTY; without even the implied warranty of
15* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16* GNU General Public License for more details.
17*
18* You should have received a copy of the GNU General Public License
19* along with Teyjus.  If not, see <http://www.gnu.org/licenses/>.
20****************************************************************************)
21(*****************************************************************************)
22(* Module Processclauses:                                                    *)
23(* Transform the term representations of clauses into their clauses          *)
24(* representations.                                                          *)
25(* 1. Type environments associated with constants occurrences are trimmed    *)
26(*    according to the type skeleton optimization.                           *)
27(* 2. Lambda-bound variables are transformed into de Bruijn indexes and the  *)
28(*    list of binders in an abstraction term is removed.                     *)
29(* 3. Other variables (type variables) are transformed into logic (type)     *)
30(*    variables with a form suitable for variable annotations; their scope   *)
31(*    information are collected and recorded along with clauses and goals.   *)
32(* 4. Clauses defining a predicate are collected and associated with the     *)
33(*    predicate name being defined;                                          *)
34(* 5. String arguments are collected.                                        *)
35(*****************************************************************************)
36
37(** ********************************************************************** **)
38(** Global variables and access functions                                  **)
39(** ********************************************************************** **)
40
41(*********************************************************************)
42(* the string list of a module                                       *)
43(*********************************************************************)
44let modStr : Absyn.astringinfo list ref = ref []
45let addModStr strinfo = modStr := strinfo :: (!modStr)
46
47(*********************************************************************)
48(* a flag indicating whether the processing is under embedded clause *)
49(* context                                                           *)
50(*********************************************************************)
51let embeddedClause : bool ref = ref false
52let isEmbedded () = !embeddedClause
53let setEmbedded flag = embeddedClause := flag
54
55(*****************************************************************************)
56(*               Global variable (type variable) lists                       *)
57(*****************************************************************************)
58(*********************************************************************)
59(* 1.Term variables (the association of variable name and variable   *)
60(*   information) appearing free in a clause                         *)
61(*********************************************************************)
62let tVars : (Absyn.atypesymbol * Absyn.avar) list ref = ref []
63
64(*********************************************************************)
65(* 2.Type variables appearing free in a clause                       *)
66(*********************************************************************)
67let tyVars : (Absyn.atype * Absyn.atypevar) list ref = ref []
68
69(*********************************************************************)
70(* 3.Term variables (the association of variable name and variable   *)
71(*   information) that are (explicitly) quantified in the body of a  *)
72(*   clause                                                          *)
73(*********************************************************************)
74let qVars: (Absyn.atypesymbol * Absyn.avar) list ref = ref []
75
76(*********************************************************************)
77(* 4. Term variables that are explicitly quantified at the head of a *)
78(*    clause                                                         *)
79(*********************************************************************)
80let hqVars : (Absyn.atypesymbol * (Absyn.avar option ref)) list ref = ref []
81
82(*****************************************************************************)
83(* Global variable (type variable) lists access functions:                   *)
84(*****************************************************************************)
85(*********************************************************************)
86(* gListAdd: add a new item to the front of one of the global list   *)
87(*********************************************************************)
88let gListAdd index data glist = (glist := (index, data) :: !glist)
89
90(*********************************************************************)
91(* gListFind:                                                        *)
92(* find information associated with a given "index" in one of the    *)
93(* global list                                                       *)
94(* None is returned if the "index" does not occur.                   *)
95(* Note that the index is usually an address (of mutable structures) *)
96(* and so "==" is used for their comparison.                         *)
97(*********************************************************************)
98let gListFind index glist =
99  let rec find assocs =
100  match assocs with
101    [] -> None
102  | ((index' , data) :: rest) ->
103    if (index' == index) then Some(data)
104    else find rest
105  in (find (!glist))
106
107(*********************************************************************)
108(* gListsSet:                                                        *)
109(* destructively update tVars, tyVars, qVars and hqVars to           *)
110(* references to given lists.                                        *)
111(*********************************************************************)
112let gListsSet ntVars ntyVars nqVars nhqVars =
113  (tVars := ntVars; tyVars := ntyVars; qVars := nqVars; hqVars := nhqVars)
114
115
116(*********************************************************************)
117(* closed definition list : used in insert embedded clauses          *)
118(*********************************************************************)
119let closedDefs : ((Absyn.aconstant * Absyn.aterm) list) ref = ref []
120let setClosedDefs defs = closedDefs := defs
121
122let inClosedDefs const impterm =
123  let rec inClosedDefsAux defs =
124  match defs with
125    [] -> false
126  | (hc, def) :: rest ->
127    if (const == hc) && (Absyn.sameTermStructure impterm def) then true
128    else inClosedDefsAux rest
129  in
130  inClosedDefsAux (!closedDefs)
131
132
133(** ********************************************************************** **)
134(**                        PROCESS TYPES                                   **)
135(** ********************************************************************** **)
136(**************************************************************************)
137(* transType:                                                             *)
138(* Transforming a type into a form suitable for variable annotation:      *)
139(* a). the result type expression is reference free;                      *)
140(* b). the occurrences of free type variables and their actual variable   *)
141(*     data are seperated;                                                *)
142(* c). as a side effect, the association of the (original) type variable  *)
143(*     and the newly introduced type variable data is collected into      *)
144(*     tyVars.                                                            *)
145(**************************************************************************)
146let rec transType tyExp =
147  match tyExp with
148    Absyn.TypeVarType(typeVarInfo) ->
149      (* it is assumed the typeVarInfo here must take form of BindableTypeVar*)
150      (match (typeVarInfo) with
151         | Absyn.BindableTypeVar(binding) ->
152             if Option.isNone (!binding) then (*actually a free var *)
153               let tyVarData =
154                 match gListFind tyExp tyVars with
155                   | None -> (* not encountered yet *)
156                       let varData = Absyn.makeNewTypeVariableData () in
157                         gListAdd tyExp varData tyVars; (* add into tyVars *)
158                         varData
159                   | Some(varData) -> varData
160               in
161                 Absyn.makeNewTypeVariable tyVarData
162             else
163               (* It seems that this situation never happens, possibly
164                * due to a previous call to dereferenceType *)
165               transType (Option.get (!binding)) (* a type reference *)
166         | _ ->
167             (* Originally absyn types do not contain any FreeTypeVar *)
168             Errormsg.impossible
169                  Errormsg.none "transType: invalid type expression")
170  | Absyn.ArrowType(arg, target) ->
171      Absyn.ArrowType(transType arg, transType target)
172  | Absyn.ApplicationType(kind, args) ->
173      Absyn.ApplicationType(kind, List.map transType args)
174  | _ -> Errormsg.impossible Errormsg.none "transType: invalid type expression"
175
176(** ********************************************************************** **)
177(**                        PROCESS TERMS                                   **)
178(** ********************************************************************** **)
179(**************************************************************************)
180(* transTerm:                                                             *)
181(* transforming terms into a form suitable for variable annotation:       *)
182(* a). term variables are separated into term variable occurrences and    *)
183(*     term variable data which is based on a nameless representation;    *)
184(* b). type environment is trimmed for constant occurrences based on the  *)
185(*     type skeleton optimization result;                                 *)
186(* c). strings are transformed into a stringData, and the text is collect *)
187(*     into the module string list;                                       *)
188(* d). bound variables are transformed into de Bruijn indexes and the     *)
189(*     binder (name) list of abstractions are removed.                    *)
190(* Note it is assumed that the application and abstraction sub structures *)
191(* contained in the input term are unnested.                              *)
192(**************************************************************************)
193let rec transTerm bvs tm =
194  match tm with
195  Absyn.IntTerm(v, _)            -> Absyn.IntTerm(v, Errormsg.none)
196  | Absyn.RealTerm(v, _)           -> Absyn.RealTerm(v, Errormsg.none)
197  | Absyn.StringTerm(s, _)         -> (transTermStr s)
198  | Absyn.ConstantTerm(c, tyenv, _)-> (transTermConst c tyenv)
199  | Absyn.FreeVarTerm(varInfo, _)  -> (transTermFreeVar varInfo)
200  | Absyn.BoundVarTerm(varInfo, _) -> (transTermBoundVar varInfo bvs)
201  | Absyn.AbstractionTerm(abst, _) -> (transTermAbst bvs abst)
202  | Absyn.ApplicationTerm(app, _)  -> (transTermAppl bvs app)
203  | _ -> Errormsg.impossible Errormsg.none "transTerm: invalid term structure"
204
205(***********************************************************************)
206(* transform strings:                                                  *)
207(* relevant string information is added into the global string list as *)
208(* side effect.                                                        *)
209(***********************************************************************)
210and transTermStr s =
211  match s with
212  Absyn.StringLiteral(chs) ->
213    let strdata = Absyn.StringData(chs, ref None, ref None) in
214    (addModStr strdata);
215    Absyn.StringTerm(strdata, Errormsg.none)
216  | _ -> Errormsg.impossible Errormsg.none "transTermStr: invalid string rep"
217
218
219(**************************************************************************)
220(* transform constants:                                                   *)
221(* TO ADD: rearrange type environment according to information provided   *)
222(* by type reduction.                                                     *)
223(**************************************************************************)
224and transTermConst c tyenv =
225  (*  a general list function needed to truncate type environments here *)
226  let rec trunclist l n =
227  if n = 0 then []
228    else
229      match l with
230        (h::t) -> (h::(trunclist t (n-1)))
231      | _ -> Errormsg.impossible Errormsg.none
232               "Parse.trunclist: invalid arguments."
233  in
234  let skeletonNeededness =
235  Option.get (Absyn.getConstantSkeletonNeededness c)
236  in
237  let rec trimTypeEnvironment tyenv index newtyenv =
238  match tyenv with
239    [] -> List.rev newtyenv
240  | (ty :: rest) ->
241      if Array.get skeletonNeededness index then
242        trimTypeEnvironment rest (index + 1) ((transType ty) :: newtyenv)
243      else
244        trimTypeEnvironment rest (index + 1) newtyenv
245  in
246  if (Absyn.isPervasiveConstant c) then
247    Absyn.ConstantTerm(c, List.map transType
248           (trunclist tyenv (Absyn.getConstantTypeEnvSize false c)),
249           Errormsg.none)
250  else
251    Absyn.ConstantTerm(c, trimTypeEnvironment tyenv 0 [], Errormsg.none)
252
253(**************************************************************************)
254(* transform variables:                                                   *)
255(* The variable could be quantified in the following three situations:    *)
256(* 1. explicitly universal quantified at the head of the current clause;  *)
257(* 2. explicitly universal/exstential quantified in the body of the       *)
258(*    current clause;                                                     *)
259(* 3. explicitly or implicitly quantified at the embedding context for    *)
260(*    an embedded goal; implicitly quantified at the head for a top-level *)
261(*    goal.                                                               *)
262(**************************************************************************)
263and transTermVar tysy =
264  match gListFind tysy qVars with
265    | Some(qVarData) ->  qVarData (* body quantified *)
266    | None ->
267      match gListFind tysy hqVars with
268        | Some(hqVar) ->          (* exp head quant *)
269            (match !hqVar with
270               | Some(hqVarData) -> hqVarData
271               | None ->   (*exp head quant; but first encountered *)
272                   let hqVarData = Absyn.makeNewVariableData () in
273                     hqVar := Some(hqVarData);      (* update hqVars *)
274                     hqVarData)
275        | None ->
276            (* implicitly quantified at head of top-level clause or   *)
277            (* implicitly/explicitly quantified in embedding context of *)
278            (* embedded clauses.                                        *)
279            match (gListFind tysy tVars) with
280                Some(varData) -> varData
281              | None -> (* first encountered *)
282                  let myVarData = Absyn.makeNewVariableData () in
283                    gListAdd tysy myVarData tVars; (*add into tVars*)
284                    myVarData
285
286(**************************************************************************)
287(* transform free variables:                                              *)
288(* This variable could be implicitly quantified at the head of the top    *)
289(* level clause or could be an explicitly quantified one that appears as  *)
290(* the head of a flex goal.                                               *)
291(**************************************************************************)
292and transTermFreeVar var =
293  match var with
294    | Absyn.NamedFreeVar(tysy) ->
295        Absyn.FreeVarTerm(Absyn.FreeVar(transTermVar tysy, ref None),
296            Errormsg.none)
297    | _ -> Errormsg.impossible Errormsg.none
298             "transTermFreeVar: invalid var rep"
299
300(***************************************************************************)
301(* transform bound variables:                                              *)
302(* The variable must be bound explicitly in one of the three situtions:    *)
303(* 1. it is lambda bound.                                                  *)
304(* 2. it is (explicitly) universally bound at the head of the current      *)
305(*    clause; it is universally or existentially bound in the body of the  *)
306(*    current clause.                                                      *)
307(* 3. it is (explicitly) universally or existentially bound in the         *)
308(*    enclosing context of the current clause (only relevant for embedded  *)
309(*    clauses.                                                             *)
310(* In the first situation, the variable is transformed into a de Bruijn    *)
311(* index and in the latter two situations, the variable is transformed into*)
312(* a logic (free) variable representation which is suitable for variable   *)
313(* annotation.                                                             *)
314(***************************************************************************)
315and transTermBoundVar var bvs =
316  match var with
317  | Absyn.NamedBoundVar(tysy) ->
318    let rec ith tysys ind = match tysys with
319      |  [] -> (ind, false)
320      | (tysy' :: rest) ->
321        if (tysy' == tysy) then
322          (ind, true)
323        else ith rest (ind + 1)
324    in
325    let (dbInd, found) = ith bvs 1 in
326      if (found) then (* lambda-bound? *)
327        Absyn.BoundVarTerm(Absyn.DBIndex(dbInd), Errormsg.none)
328      else
329        Absyn.FreeVarTerm(Absyn.FreeVar(transTermVar tysy, ref None),
330              Errormsg.none)
331  | _ -> Errormsg.impossible Errormsg.none "transTermBoundVar: invalid var rep"
332
333
334(**************************************************************************)
335(* transform abstractions:                                                *)
336(**************************************************************************)
337and transTermAbst bvs abstTerm =
338  match abstTerm with
339  Absyn.UNestedAbstraction(binders, nabs, body) ->
340    (* Note the order of the binders are reversed in the collected list *)
341    let rec collectBinders mybds newbd =
342    match mybds with
343      [] -> newbd
344    | (bd::rest) -> collectBinders rest (bd::newbd)
345    in
346    let newbody = transTerm (collectBinders binders bvs) body in
347    Absyn.AbstractionTerm(Absyn.UNestedAbstraction([], nabs, newbody),
348              Errormsg.none)
349  | _ -> Errormsg.impossible Errormsg.none "transTermAbst: invalid abst rep"
350
351(**************************************************************************)
352(* transform applications:                                                *)
353(**************************************************************************)
354and transTermAppl bvs applTerm =
355  match applTerm with
356    Absyn.FirstOrderApplication(func, args, nargs) ->
357      Absyn.ApplicationTerm(
358      Absyn.FirstOrderApplication(transTerm bvs func,
359          List.map (transTerm bvs) args,
360          nargs), Errormsg.none)
361  | _ -> Errormsg.impossible Errormsg.none "transTermAppl: invalid app rep"
362
363(** ********************************************************************** **)
364(**                       PROCESS CLAUSES                                  **)
365(** ********************************************************************** **)
366(***************************************************************************)
367(* INSERT A CLAUSE INTO PREDICATE DEFINITION LIST:                         *)
368(***************************************************************************)
369(* Add the clause into the defintition block of its head predicate; a new  *)
370(* definition block is created if there exists none for the predicate, and *)
371(* if the clause is at top-level, the new defintition block is associated  *)
372(* with the predicate name constant itself too as its codeinfo.            *)
373(* Note that it is assumed the clauses being processed by this function are*)
374(* in an order reversed to their appearence in the program (their actual   *)
375(* order), and are reversed again in the process of insertion.             *)
376(***************************************************************************)
377let insertClause pred clause clDefs embedded closed =
378  (* looking for the clause block defining a predicate name from a given *)
379  (* definition list.                                                    *)
380  let rec findClBlock clDefs =
381  match clDefs with
382    [] -> None
383  | ((pred', clBlock)::rest) ->
384    if (pred == pred') then Some(clBlock)
385    else findClBlock rest
386  in
387
388  let clBlock = findClBlock clDefs in
389  match clBlock with
390    None -> (* has to create a new definition block *)
391      let newClBlock = Absyn.makeNewClauseBlock clause closed in
392      (* record the clause block into the code info field of the predicate *)
393      (* name if top-level *)
394      (if embedded then ()
395      else Absyn.setConstantCodeInfo pred (Some (Absyn.Clauses newClBlock)));
396      ((pred, newClBlock) :: clDefs)
397  | Some(cls, _, _, _) -> (* one exists: add one more clause *)
398      (*let rec show_clause cls =
399  match cls with
400  [] -> ()
401  | (cl :: rest) ->
402  print_string ("clauseName: " ^
403  (Absyn.getConstantName (Absyn.getClausePred cl)) ^
404  "\n");
405  show_clause rest
406  in*)
407      cls := clause :: !cls;
408      clDefs
409
410
411(**************************************************************************)
412(*               A PRE CLAUSE REPRESENTATION                              *)
413(**************************************************************************)
414(* (pred, term args, type args, number term args, number type args (, body)) *)
415type preclause =
416    Fact of Absyn.aconstant * Absyn.aterm list * Absyn.atype list * int * int
417  | Rule of Absyn.aconstant * Absyn.aterm list * Absyn.atype list * int * int
418    * Absyn.agoal
419
420(****************************************************************************)
421(*                         PROCESS CLAUSE                                   *)
422(****************************************************************************)
423(*  Transform term representation of a clause into a pre clause paired      *)
424(*  with the association lists of term variables and type variables         *)
425(*  appearing free in the clause and the list of universal variables        *)
426(*  explicitly quantified at the clause head.                               *)
427(*  The main action carried out here is to recurse over the top-level for   *)
428(*  all structures and records such variables into the global hqVars list.  *)
429(****************************************************************************)
430let rec processClause clauseTerm =
431  (* collect variable data of explicitly head quantified variables that are*)
432  (* used in the clause *)
433  let collectHQVars hqVarAssocs =
434  let rec collectHQVarsAux hqVarAssocs vars =
435    match hqVarAssocs with
436    [] -> vars
437    | ((tysy, varInfo):: rest) ->
438      match (!varInfo) with
439      None -> collectHQVarsAux rest vars (* not used *)
440      | Some(hqVarData) ->  collectHQVarsAux rest (hqVarData :: vars)
441  in
442  collectHQVarsAux hqVarAssocs []
443  in
444  (* function body of processClause *)
445  match clauseTerm with
446    Absyn.ConstantTerm(head, tyenv, _) -> (* proposition fact *)
447      let (preClause, freeVars, freeTyVars) = processFact head tyenv [] 0 in
448      (preClause, freeVars, freeTyVars, collectHQVars (!hqVars))
449  | Absyn.ApplicationTerm(_) ->
450      let func = Absyn.getTermApplicationHead clauseTerm in
451      let args = Absyn.getTermApplicationArguments clauseTerm in
452      let head = Absyn.getTermConstant func in
453      if (Pervasive.isallConstant head) then
454        let arg = List.hd args in
455        gListAdd (List.hd (Absyn.getTermAbstractionVars arg))
456          (ref None) hqVars;
457        processClause (Absyn.getTermAbstractionBody arg)
458      else
459        let (preClause, freeVars, freeTyVars) =
460          if (Pervasive.isimplConstant head) then (* process rule *)
461            processRule (List.hd (List.tl args)) (List.hd args)
462          else (* process fact *)
463            processFact head (Absyn.getTermMoleculeEnv func) args
464              (Absyn.getTermApplicationArity clauseTerm)
465        in
466        (preClause, freeVars, freeTyVars, collectHQVars (!hqVars))
467  | t ->
468      (Errormsg.impossible (Absyn.getTermPos t)
469         "Processclauses.processClause: invalid clause term.")
470
471(***************************************************************************)
472(* process clause head:                                                    *)
473(* Transform term arguments, type arguments of a clause head into a form   *)
474(* suitable for variable annotation.                                       *)
475(* Note the type skeleton reductions should have no effect for predicate   *)
476(* names, and so are not concerned here.                                   *)
477(***************************************************************************)
478and processClauseHead args tyargs =
479  (List.map (transTerm []) args, List.map transType tyargs)
480
481(***************************************************************************)
482(* process a fact:                                                         *)
483(* predicate name, predicate arguments, predicate type arguments, the      *)
484(* number of arguments (term and type), the number of term arguments are   *)
485(* collected for a fact.                                                   *)
486(***************************************************************************)
487and processFact pred tyargs tmargs ntmargs =
488  let (predArgs, predTyArgs) = processClauseHead tmargs tyargs in
489  (Fact(pred, predArgs, predTyArgs, ntmargs + (Absyn.getConstantTypeEnvSize false pred),
490    ntmargs), !tVars, !tyVars)
491
492(***************************************************************************)
493(* process a rule:                                                         *)
494(* predicate name, predicate arguments, predicate type arguments, the      *)
495(* number of arguments (term and type), the number of term arguments and   *)
496(* the goal representation of the clause body are collected for a rule.    *)
497(***************************************************************************)
498and processRule clauseHead clauseBody =
499  let (pred, tyenv, args, arity) =
500  match clauseHead with
501    (*proposition*)
502      Absyn.ConstantTerm(pred, tyenv, _) -> (pred, tyenv, [], 0)
503    | Absyn.ApplicationTerm(_) ->
504      let head = Absyn.getTermApplicationHead clauseHead in
505      (Absyn.getTermConstant head, Absyn.getTermMoleculeEnv head,
506       Absyn.getTermApplicationArguments clauseHead,
507       Absyn.getTermApplicationArity clauseHead)
508    | t ->
509      (Errormsg.impossible
510        (Absyn.getTermPos t)
511        "Processclauses.processRule: invalid clause term.")
512  in
513  let (predArgs, predTyArgs) = processClauseHead args tyenv in
514  let goal = processGoal clauseBody in
515  (Rule(pred, predArgs, predTyArgs, (Absyn.getConstantTypeEnvSize false pred) + arity,
516    arity, goal), !tVars, !tyVars)
517
518(*****************************************************************************)
519(* process a goal:                                                           *)
520(* transform a goal from its term representation into its goal representation*)
521(* Note that the goal that is introduced from closing off universal          *)
522(* variable's defintions gets special treatment and representation.          *)
523(*****************************************************************************)
524and processGoal gltm =
525  match gltm with
526    Absyn.ApplicationTerm(_) ->
527      if (gltm == Pervasiveutils.cutFailTerm) then Absyn.CutFailGoal
528      else
529  let head = Absyn.getTermApplicationHead gltm in
530  let args = Absyn.getTermApplicationArguments gltm in
531  (match head with
532    Absyn.ConstantTerm(pred, _, _) ->
533      if Pervasive.isandConstant pred then               (*and goal *)
534        processAndGoal (List.hd args) (List.hd (List.tl args))
535      else if Pervasive.issomeConstant pred then         (*some goal*)
536        processSomeGoal (List.hd args)
537      else if Pervasive.isallConstant pred then          (*all goal *)
538        processAllGoal (List.hd args)
539      else if Pervasive.isimplConstant pred then         (*imp goal *)
540        processImpGoal (List.hd args) (List.hd (List.tl args)) gltm
541      else                                     (* rigid atomic goal *)
542        processAtomicGoal gltm head
543    (Absyn.getTermApplicationArguments gltm)
544    (Absyn.getTermApplicationArity gltm)
545  | _ -> processAtomicGoal gltm head [] 0)     (* flex atomic goal *)
546  | _-> processAtomicGoal gltm gltm [] 0 (* proposition goal: flex or rig*)
547
548(**************************************************************************)
549(* process atomic goal:                                                   *)
550(* Note a flex goal of form (F t1... tn) is transformed into              *)
551(*      solve (F t1 ... tn)                                               *)
552(**************************************************************************)
553and processAtomicGoal gltm head args arity =
554  match head with
555    Absyn.FreeVarTerm(Absyn.NamedFreeVar(_), _) -> (* free var head *)
556      Absyn.AtomicGoal(Pervasive.solveConstant, 1, 1, [(transTerm [] gltm)],[])
557  | Absyn.ConstantTerm(pred, tyenv, _) ->
558      Absyn.AtomicGoal(pred,
559                       arity + (Absyn.getConstantTypeEnvSize false pred),
560                       arity,
561                       List.map (transTerm []) args, List.map transType tyenv)
562  | _ -> Errormsg.impossible Errormsg.none "processAtomicGoal: invalid pred"
563
564
565(***************************************************************************)
566(* process and goal:                                                       *)
567(***************************************************************************)
568and processAndGoal andl andr =
569  let l = processGoal andl in
570  let r = processGoal andr in
571  Absyn.AndGoal(l, r);
572
573
574
575(***************************************************************************)
576(* process some goal:                                                      *)
577(* The existential quantified variable is added into qVars as side effect, *)
578(* and its variable data information is recorded with the goal structure   *)
579(***************************************************************************)
580and processSomeGoal goalBody =
581  let tysy = List.hd (Absyn.getTermAbstractionVars goalBody) in
582  let varData = Absyn.makeNewVariableData () in
583  gListAdd tysy varData qVars; (* add into qVars *)
584  Absyn.SomeGoal(varData, processGoal (Absyn.getTermAbstractionBody goalBody))
585
586(***************************************************************************)
587(* process all goal:                                                       *)
588(* Contiguous unviersal quantifed variables are added into qVars as side   *)
589(* effect, and their variable data information paired with corresponding   *)
590(* hidden constants are collected and recorded  with the goal structure.   *)
591(***************************************************************************)
592and processAllGoal goalBody =
593
594  (* enter the given variable into the qVars list; and create a hidden     *)
595  (* constant variable association pair. *)
596  let collectHCpair tysy =
597    let hcData = Absyn.getTypeSymbolHiddenConstant tysy in
598    let varData = Absyn.makeNewVariableData () in
599    gListAdd tysy varData qVars; (* update qVars *)
600    (varData, hcData)
601  in
602
603  (* recurse over for-all structures, and collect universally quantified *)
604  (* variables into qVars.                                               *)
605  let rec processAllGoalAux goal hcPairs =
606    match goal with
607      Absyn.ApplicationTerm(_) ->
608        let head = Absyn.getTermApplicationHead goal in
609        let args = Absyn.getTermApplicationArguments goal in
610        if (Absyn.isTermConstant head) &&
611           (Pervasive.isallConstant (Absyn.getTermConstant head)) then
612          (*all goal*)
613          let arg = List.hd args in
614          let tysy = List.hd (Absyn.getTermAbstractionVars arg) in
615          processAllGoalAux (Absyn.getTermAbstractionBody arg)
616                            ((collectHCpair tysy)::hcPairs)
617        else (* other than all goal *)
618            Absyn.AllGoal(Absyn.HCVarAssocs(List.rev hcPairs), processGoal goal)
619    | _ -> (* other than all goal *)
620      Absyn.AllGoal(Absyn.HCVarAssocs(List.rev hcPairs), processGoal goal)
621  in
622
623  let tysy = List.hd (Absyn.getTermAbstractionVars goalBody) in
624  processAllGoalAux (Absyn.getTermAbstractionBody goalBody)
625                    [collectHCpair tysy]
626
627
628(****************************************************************************)
629(* process implication goal:                                                *)
630(* Actions carried out here are:                                            *)
631(* a). transform the body goal;                                             *)
632(* b). transform the clauses in the ancester and collect them into the      *)
633(*     definition list for the implication goal;                            *)
634(* c). collect list of term variables and type variables that should be     *)
635(*     initialized upon entering the implication goal (those variables      *)
636(*     having their scopes outside of the implication goal, but having      *)
637(*     their first appearence inside the ancester of the goal.              *)
638(****************************************************************************)
639and processImpGoal clauseTerm goalTerm impGoal =
640  (* recurse over the conjunctive structures *)
641  let rec processImpClauses clauseTerm clauseDefs varInits tyVarInits =
642    match clauseTerm with
643      Absyn.ApplicationTerm(_) ->
644        let args = Absyn.getTermApplicationArguments clauseTerm in
645        let head = Absyn.getTermApplicationHead clauseTerm in
646        if Absyn.isTermConstant head then
647          if Pervasive.isandConstant (Absyn.getTermConstant head) then
648            let (newClDefs, newVarInits, newTyVarInits) =
649            processImpClauses (List.hd args) clauseDefs varInits tyVarInits
650            in
651            processImpClauses (List.hd (List.tl args)) newClDefs newVarInits
652                              newTyVarInits
653          else
654            processImpClause clauseTerm clauseDefs varInits tyVarInits impGoal
655        else
656          Errormsg.impossible
657            (Absyn.getTermPos clauseTerm)
658            "Processclauses.processImpGoal: invalid (flexible) clause head."
659    | _ -> processImpClause clauseTerm clauseDefs varInits tyVarInits impGoal
660  in
661
662  let (clauseDefs, varInits, tyVarInits) =
663    processImpClauses clauseTerm [] [] []
664  in
665  Absyn.ImpGoal(Absyn.Definitions(clauseDefs),
666                Absyn.VarInits(List.rev varInits),
667                Absyn.TypeVarInits(List.rev tyVarInits),
668                processGoal goalTerm)
669
670(********************************************************************)
671(* processImpClause:                                                *)
672(* Processing a clause embedded in an implication goal:             *)
673(* a. transform into clause representation and insert it into the   *)
674(*    definition list of the implication goal;                      *)
675(* b. collect term and type variables with their scopes outside the *)
676(*    clause but with first appearence inside;                      *)
677(* c. generate mapping for type and term variables with their scopes*)
678(*    outside the clause; the scopes of free type variables are     *)
679(*    reflected by this mapping list: those occurring in the type   *)
680(*    association of a free term variable are assumed to have the   *)
681(*    same scopes the corresponding term variables and therefore    *)
682(*    are collected in the type variable mapping if the term        *)
683(*    variable has its scope outside; other free type variables     *)
684(*    are assumed to have their scopes at the head of the embedded  *)
685(*    clause.                                                       *)
686(********************************************************************)
687and processImpClause clauseTerm clauseDefs varInits tyVarInits impGoal =
688  (* process the embedded clause *)
689  let (ltVars, ltyVars, lqVars, lhqVars, lembedded) =    (* bookkeeping *)
690  (!tVars, !tyVars, !qVars, !hqVars, isEmbedded ())
691  in
692  gListsSet [] [] [] [];  (* set global (type) variable list to empty   *)
693  setEmbedded true;       (* set embedded flag to true                  *)
694  let (preClause, fvAssoc, tyfvAssoc, expHQVars) = processClause clauseTerm in
695
696  (* collect (type) variable mapping information for this clause and    *)
697  (* increment (type) variable initialization                           *)
698  gListsSet ltVars ltyVars lqVars lhqVars;   (* recover global lists    *)
699  setEmbedded lembedded;                     (* recover embedded flag   *)
700  let (fvMaps, tyfvMaps, newVarInits, newTyVarInits) =
701    mapFreeVars fvAssoc tyfvAssoc varInits tyVarInits
702  in
703  let fvMaps'   = Absyn.TermVarMap(fvMaps)   in
704  let tyfvMaps' = Absyn.TypeVarMap(tyfvMaps) in
705
706  (* create clause representation *)
707  let (pred, clause) =
708  match preClause with
709    Fact(pred, args, tyargs, nargs, ntargs) ->
710    (pred,
711     Absyn.Fact(pred, args, tyargs, nargs, ntargs, fvMaps', tyfvMaps',
712          expHQVars, ref None, []))
713  | Rule(pred, args, tyargs, nargs, ntargs, goal) ->
714    (pred,
715     Absyn.Rule(pred, args, tyargs, nargs, ntargs, fvMaps', tyfvMaps',
716          expHQVars, ref None, goal, ref (Absyn.GoalEnvAssoc []),
717          ref None, ref false, []))
718  in
719  let closed = inClosedDefs pred impGoal in
720  (* insert the new clause into the definition list of the impl goal *)
721  (insertClause pred clause clauseDefs true closed, newVarInits, newTyVarInits)
722
723
724(********************************************************************)
725(* mapFreeVars:                                                     *)
726(* Generate variable mappings for type and term variables free in   *)
727(* the embedded clause. Accumulate variable and type variable       *)
728(* initialization lists.                                            *)
729(********************************************************************)
730and mapFreeVars fvs tyfvs varInits tyVarInits =
731
732  (******************************************************************)
733  (* recurse over the given free variable (typesymbol,              *)
734  (* variable data association) list and                            *)
735  (* a). generate free variable mapping:                            *)
736  (*     looking for the variable's typesymbol from the current     *)
737  (*     qVar, hqVar and tyVar lists (which records the variables   *)
738  (*     of the enclosing clause). If the variable is found in      *)
739  (*     those lists and it does have an associated variable data   *)
740  (*     then use the variable data to form a variable mapping.     *)
741  (*     Otherwise, it implies the variable has a scope outside of  *)
742  (*     the current (embedded) clause but yet has an occurrence,   *)
743  (*     so that a new variable data is created for initialization, *)
744  (*     and a variable mapping is formed with this newly created   *)
745  (*     one.                                                       *)
746  (* b). increment variable initialization list for those with      *)
747  (*     scopes outside of the clause, but are not encountered      *)
748  (*     in the enclosing clause yet. Namely, all the variable data *)
749  (*     newly created in the previous step belongs to this category*)
750  (*     and should be collected.                                   *)
751  (* c). collect type variables appearing in the type environment   *)
752  (*     of the variables that are free in the current clause: this *)
753  (*     information is needed for deciding the scopes of type      *)
754  (*     variables appearing free in the current clause in          *)
755  (*     collectTyVarMaps.                                          *)
756  (******************************************************************)
757  let rec collectVarMaps fvs fvMaps varInits globalTyVars =
758    match fvs with
759      [] -> (fvMaps, varInits, globalTyVars)
760    | ((tysy, toVarData) :: rest) ->
761        (* collect global type variables *)
762        let newGlobalTyVars =
763          Types.freeTypeVars (Absyn.getTypeSymbolType tysy) globalTyVars
764        in
765        (* collect var map and var init *)
766        let (fromVarData, newVarInits) =
767          match gListFind tysy qVars with
768              Some(qVarData) -> (qVarData, varInits) (* body quantified     *)
769            | None ->
770                match gListFind tysy hqVars with
771                    Some(hqVarInfo) ->       (* exp head quantified *)
772                      (match (!hqVarInfo) with
773                           Some(hqVarData) -> (hqVarData, varInits)
774                         | None ->
775                             (*exp head quant with first occ in embedded cl:*)
776                             (*should be initiated*)
777                             let hqVarData = Absyn.makeNewVariableData () in
778                               hqVarInfo := Some(hqVarData); (*update hqVars *)
779                               (hqVarData, (hqVarData :: varInits)))
780                  | None ->
781                      (* implicitly quantified at head of top-level clause or
782                       * implicitly/explicitly quantified in embedding
783                       * context of embedded clauses. *)
784                       match gListFind tysy tVars with
785                          Some(varData) -> (varData, varInits)
786                        | None ->
787                            let varData = Absyn.makeNewVariableData () in
788                              gListAdd tysy varData tVars; (*update tyVars*)
789                              (varData,
790                               if not (isEmbedded ()) then
791                                 (varData :: varInits )
792                               else varInits)
793        in
794          collectVarMaps rest ((fromVarData, toVarData)::fvMaps) newVarInits
795            newGlobalTyVars
796  in
797
798  (******************************************************************)
799  (* recurse over the given free type variable (type - type variable*)
800  (* data association) list: if the free type variable is not       *)
801  (* contained in the feeding in globalTyVars list, then it has its *)
802  (* scope just over the embedded clause, and needs not be          *)
803  (* considered for type variable mapping and initialization;       *)
804  (* otherwise, the following actions are carried out:              *)
805  (* a). generate free type variable mapping:                       *)
806  (*     look for the type variable through the current tyVars list *)
807  (*     which is assumed to contain the encountered type variables *)
808  (*     in the enclosing clause. If one is found, then use the     *)
809  (*     associated type variable data to form a type variable      *)
810  (*     mapping; otherwise, the type variable has outside scope    *)
811  (*     but has first occurrence inside this embedded clause, and  *)
812  (*     a new type variable data is created, and used to form a    *)
813  (*     type variable mapping;                                     *)
814  (* b). the type variable initialization list is incremented by    *)
815  (*     those newly created type variable data in the previous step*)
816  (******************************************************************)
817  let rec collectTyVarMaps typeVars globalTyVars tyVarMaps tyVarInits =
818    match typeVars with
819        [] -> (tyVarMaps, tyVarInits)
820      | ((tyVar, toTyVarData)::rest) ->
821          if (List.mem tyVar globalTyVars) then
822            let (fromTyVarData, newTyVarInits) =
823              match gListFind tyVar tyVars with
824                  Some(tyVarData) -> (tyVarData, tyVarInits)
825                | None -> (* global, but not encountered outside yet *)
826                    let tyVarData = Absyn.makeNewTypeVariableData () in
827                      gListAdd tyVar tyVarData tyVars; (*update tyVars *)
828                      (tyVarData, tyVarData :: tyVarInits)
829            in
830              collectTyVarMaps rest globalTyVars
831                ((fromTyVarData, toTyVarData) :: tyVarMaps) newTyVarInits
832          else (* not really global *)
833            collectTyVarMaps rest globalTyVars tyVarMaps tyVarInits
834  in
835
836  (* function body of mapFreeVars *)
837  let (fvMaps, newVarInits, globalTyVars) =
838    collectVarMaps fvs [] varInits []
839  in
840  let (tyFvMaps, newTyVarInits) =
841    collectTyVarMaps tyfvs globalTyVars [] tyVarInits
842  in
843    (fvMaps, tyFvMaps, newVarInits, newTyVarInits)
844
845(****************************************************************************)
846(*      PROCESS TOP LEVEL (INCLUDING ANONYMOUS) CLAUSES                     *)
847(****************************************************************************)
848(* a) transform term representations of top-level clauses into their clause *)
849(*    representations;                                                      *)
850(* b) collect defintitions for predicates:                                  *)
851(*    NOTE: the order of definitions and clauses inside one definition are  *)
852(*          reversed from those of their appearence in the input term --    *)
853(*          THE INPUT TERMS SHOULD BE IN THE REVERSED ORDER OF THEIR        *)
854(*          APPEARENCES IN PROGRAM!                                         *)
855(****************************************************************************)
856let rec processTopLevelClauses clauseTerms impmods clauseDefs anonymous =
857  match clauseTerms with
858    [] -> clauseDefs
859  | (clauseTerm :: rest) ->
860      (* transform from term representation to clause representation      *)
861      gListsSet [] [] [] []; (* initialize global variable info lists *)
862      setEmbedded false;     (* initialize embeddedClause flag        *)
863      (* transfer a clause (varMap and tyVarMap for top-level modules are *)
864      (* always empty                                                     *)
865      let (preClause, _, _, expHQVars) = processClause clauseTerm in
866      (* term/type variable mapping is always empty for top-level clauses *)
867      let fvMaps = Absyn.TermVarMap([]) in
868      let tyfvMaps = Absyn.TypeVarMap([]) in
869      let (pred, clause) =
870        (* transfer preclause into clause:                           *)
871        (* the offset field for facts and rules and goalNum-envSize  *)
872        (* association, cutvar and hasenv fields for rules are left  *)
873        (* to be filled in the next phase.                           *)
874        match preClause with
875            Fact(pred, args, tyargs, nargs, ntermargs) ->
876              (pred, Absyn.Fact(pred, args, tyargs, nargs, ntermargs, fvMaps,
877                                tyfvMaps, expHQVars, ref None, impmods))
878          | Rule(pred, args, tyargs, nargs, ntermargs, goal) ->
879              (pred, Absyn.Rule(pred, args, tyargs, nargs, ntermargs, fvMaps,
880                                tyfvMaps, expHQVars, ref None, goal,
881                                ref (Absyn.GoalEnvAssoc([])), ref None,
882                                ref false, impmods))
883      in
884      (* collect this clause into the module definitions which is organized *)
885      (* around predicate names.                                            *)
886      let newClDefs = insertClause pred clause clauseDefs false anonymous in
887        processTopLevelClauses rest impmods newClDefs anonymous
888
889(** ********************************************************************** **)
890(**                       INTERFACE FUNCTION                               **)
891(** ********************************************************************** **)
892let processClauses amod clTerms newClTerms closeddefs =
893  match amod with
894    Absyn.Module(modname, modimps, modaccs, ctable, ktable, atable, _,
895     gkinds, lkinds, gconsts, lconsts, hconsts, skels, hskels, _)
896    ->
897      let () = Errormsg.log Errormsg.none
898                 "Procesclauses.processClauses: processing clauses..." in
899      setClosedDefs closeddefs;
900      (* process anonymous clauses (those introduced for deorification), and*)
901      (* increment them into the module definition list.                    *)
902      (* Note: 1) the import module field of anonymous clauses should be    *)
903      (*          empty;                                                    *)
904      (*       2) the definitions of anonymous clauses are always closed    *)
905      let clDefs =
906        processTopLevelClauses (List.rev newClTerms) [] [] true
907      in
908      (* process clauses *)
909      let newClDefs = processTopLevelClauses clTerms modimps clDefs false in
910      (* Insert the clauses definitions and the string list into the module *)
911      (* abstract syntax.                                                   *)
912      let () = Errormsg.log Errormsg.none
913                 "Procesclauses.processClauses: processed clauses" in
914        Absyn.Module(modname, modimps, modaccs, ctable, ktable, atable, !modStr,
915                     gkinds, lkinds, gconsts, lconsts, hconsts, skels, hskels,
916                     ref (Absyn.PreClauseBlocks(Absyn.Definitions(newClDefs))))
917  | _ -> Errormsg.impossible Errormsg.none "processClauses: invalid module"
918